Library UniMath.Foundations.Sets
Generalities on hSet. Vladimir Voevodsky. Feb. - Sep. 2011
Contents
- The type of sets i.e. of types of h-level 2 in UU
- hProp as a set
- Booleans as a set
- Types X which satisfy "weak" axiom of choice for all families P : X -> UU
- The type of monic subtypes of a type (subsets of the set of connected
components)
- General definitions
- Direct product of two subtypes
- A subtype with paths between any two elements is an hProp
- Relations on types (or equivalently relations on the sets of connected
components)
- Relations and boolean relations
- Standard properties of relations
- Elementary implications between properties of relations
- Standard properties of relations and logical equivalences
- Preorderings, partial orderings, and associated types
- Equivalence relations and associated types
- Direct product of two relations
- Negation of a relation and its properties
- Boolean representation of decidable equality
- Boolean representation of decidable relations
- Restriction of a relation to a subtype
- Equivalence classes with respect to a given relation
- Direct product of equivalence classes
- Surjections to sets are epimorphisms
- Epimorphisms are surjections
- Universal property enjoyed by surjections
- Set quotients of types
- Set quotients defined in terms of equivalence classes
- Universal property of setquot R for functions to sets satisfying compatibility condition iscomprelfun
- Functoriality of setquot for functions mapping one relation to another
- Universal property of setquot for predicates of one and several variables
- The case when the function between quotients defined by setquotfun is a surjection, inclusion or a weak equivalence
- setquot with respect to the product of two relations
- Universal property of setquot for functions of two variables
- Functoriality of setquot for functions of two variables mapping one relation to another
- Set quotients with respect to decidable equivalence relations have decidable equality
- Relations on quotient sets
- Subtypes of quotients and quotients of subtypes
- The set of connected components of a type
- Set quotients. Construction 2 (Unfinished)
- Consequences of univalence
Preamble
The type of sets i.e. of types of h-level 2 in UU
Definition hSet : UU := total2 (λ X : UU, isaset X).
Definition make_hSet (X : UU) (i : isaset X) := tpair isaset X i : hSet.
Definition pr1hSet : hSet -> UU := @pr1 UU (λ X : UU, isaset X).
Coercion pr1hSet: hSet >-> UU.
Definition eqset {X : hSet} (x x' : X) : hProp
:= make_hProp (x = x') (pr2 X x x').
Notation "a = b" := (eqset a b) (at level 70, no associativity) : logic.
Definition neqset {X : hSet} (x x' : X) : hProp
:= make_hProp (x != x') (isapropneg _). Notation "a != b" := (neqset a b) (at level 70, no associativity) : logic.
Definition setproperty (X : hSet) := pr2 X.
Definition setdirprod (X Y : hSet) : hSet.
Show proof.
Definition setcoprod (X Y : hSet) : hSet.
Show proof.
Lemma isaset_total2_hSet (X : hSet) (Y : X -> hSet) : isaset (∑ x, Y x).
Show proof.
Definition total2_hSet {X : hSet} (Y : X -> hSet) : hSet
:= make_hSet (∑ x, Y x) (isaset_total2_hSet X Y).
Definition hfiber_hSet {X Y : hSet} (f : X → Y) (y : Y) : hSet
:= make_hSet (hfiber f y) (isaset_hfiber f y (pr2 X) (pr2 Y)).
Declare Scope set.
Delimit Scope set with set.
Notation "'∑' x .. y , P" := (total2_hSet (λ x,.. (total2_hSet (λ y, P))..))
(at level 200, x binder, y binder, right associativity) : set.
Lemma isaset_forall_hSet (X : UU) (Y : X -> hSet) : isaset (∏ x, Y x).
Show proof.
Definition forall_hSet {X : UU} (Y : X -> hSet) : hSet
:= make_hSet (∏ x, Y x) (isaset_forall_hSet X Y).
Notation "'∏' x .. y , P" := (forall_hSet (λ x,.. (forall_hSet (λ y, P))..))
(at level 200, x binder, y binder, right associativity) : set.
Definition unitset : hSet := make_hSet unit isasetunit.
Definition dirprod_hSet (X Y : hSet) : hSet.
Show proof.
Notation "A × B" := (dirprod_hSet A B) (at level 75, right associativity) : set.
hProp as a set
Definition hPropset : hSet := tpair _ hProp isasethProp.
Definition hProp_to_hSet (P : hProp) : hSet
:= make_hSet P (isasetaprop (propproperty P)).
Definition boolset : hSet := make_hSet bool isasetbool.
Definition isInjectiveFunction {X Y : hSet} (f : X -> Y) : hProp.
Show proof.
intros. exists (∏ (x x': X), f x = f x' -> x = x').
abstract (
intros; apply impred; intro x; apply impred; intro y;
apply impred; intro e; apply setproperty)
using isaprop_isInjectiveFunction.
abstract (
intros; apply impred; intro x; apply impred; intro y;
apply impred; intro e; apply setproperty)
using isaprop_isInjectiveFunction.
Types X which satisfy "weak" axiom of choice for all families P : X -> UU
Definition ischoicebase_uu1 (X : UU)
:= ∏ P : X -> UU, (∏ x : X, ishinh (P x)) -> ishinh (∏ x : X, P x).
Uses RR1
Lemma isapropischoicebase (X : UU) : isaprop (ischoicebase_uu1 X).
Show proof.
Definition ischoicebase (X : UU) : hProp := make_hProp _ (isapropischoicebase X).
Lemma ischoicebaseweqf {X Y : UU} (w : X ≃ Y) (is : ischoicebase X) :
ischoicebase Y.
Show proof.
Lemma ischoicebaseweqb {X Y : UU} (w : X ≃ Y) (is : ischoicebase Y) :
ischoicebase X.
Show proof.
Lemma ischoicebaseunit : ischoicebase unit.
Show proof.
Lemma ischoicebasecontr {X : UU} (is : iscontr X) : ischoicebase X.
Show proof.
Lemma ischoicebaseempty : ischoicebase empty.
Show proof.
Lemma ischoicebaseempty2 {X : UU} (is : ¬ X) : ischoicebase X.
Show proof.
Lemma ischoicebasecoprod {X Y : UU}
(isx : ischoicebase X) (isy : ischoicebase Y) : ischoicebase (coprod X Y).
Show proof.
Show proof.
Definition ischoicebase (X : UU) : hProp := make_hProp _ (isapropischoicebase X).
Lemma ischoicebaseweqf {X Y : UU} (w : X ≃ Y) (is : ischoicebase X) :
ischoicebase Y.
Show proof.
intros. unfold ischoicebase.
intros Q fs.
apply (hinhfun (invweq (weqonsecbase Q w))).
apply (is (funcomp w Q) (λ x : X, fs (w x))).
intros Q fs.
apply (hinhfun (invweq (weqonsecbase Q w))).
apply (is (funcomp w Q) (λ x : X, fs (w x))).
Lemma ischoicebaseweqb {X Y : UU} (w : X ≃ Y) (is : ischoicebase Y) :
ischoicebase X.
Show proof.
Lemma ischoicebaseunit : ischoicebase unit.
Show proof.
Lemma ischoicebasecontr {X : UU} (is : iscontr X) : ischoicebase X.
Show proof.
Lemma ischoicebaseempty : ischoicebase empty.
Show proof.
Lemma ischoicebaseempty2 {X : UU} (is : ¬ X) : ischoicebase X.
Show proof.
Lemma ischoicebasecoprod {X Y : UU}
(isx : ischoicebase X) (isy : ischoicebase Y) : ischoicebase (coprod X Y).
Show proof.
intros. unfold ischoicebase.
intros P fs. apply (hinhfun (invweq (weqsecovercoprodtoprod P))).
apply hinhand.
apply (isx _ (λ x : X, fs (ii1 x))).
apply (isy _ (λ y : Y, fs (ii2 y))).
intros P fs. apply (hinhfun (invweq (weqsecovercoprodtoprod P))).
apply hinhand.
apply (isx _ (λ x : X, fs (ii1 x))).
apply (isy _ (λ y : Y, fs (ii2 y))).
The type of monic subtypes of a type (subsets of the set of connected components)
General definitions
Definition hsubtype (X : UU) : UU := X -> hProp.
Identity Coercion id_hsubtype : hsubtype >-> Funclass.
Definition carrier {X : UU} (A : hsubtype X) := total2 A.
Coercion carrier : hsubtype >-> Sortclass.
Definition make_carrier {X : UU} (A : hsubtype X) :
∏ t : X, A t → ∑ x : X, A x := tpair A.
Definition pr1carrier {X : UU} (A : hsubtype X) := @pr1 _ _ : carrier A -> X.
Lemma isaset_carrier_subset (X : hSet) (Y : hsubtype X) : isaset (∑ x, Y x).
Show proof.
Definition carrier_subset {X : hSet} (Y : hsubtype X) : hSet
:= make_hSet (∑ x, Y x) (isaset_carrier_subset X Y).
Declare Scope subset.
Notation "'∑' x .. y , P"
:= (carrier_subset (λ x,.. (carrier_subset (λ y, P))..))
(at level 200, x binder, y binder, right associativity) : subset.
Delimit Scope subset with subset.
Lemma isinclpr1carrier {X : UU} (A : hsubtype X) : isincl (@pr1carrier X A).
Show proof.
Lemma isasethsubtype (X : UU) : isaset (hsubtype X).
Show proof.
Definition totalsubtype (X : UU) : hsubtype X := λ x, htrue.
Definition weqtotalsubtype (X : UU) : totalsubtype X ≃ X.
Show proof.
Definition weq_subtypes {X Y : UU} (w : X ≃ Y)
(S : hsubtype X) (T : hsubtype Y) :
(∏ x, S x <-> T (w x)) -> carrier S ≃ carrier T.
Show proof.
intros eq. apply (weqbandf w). intro x. apply weqiff.
- apply eq.
- apply propproperty.
- apply propproperty.
- apply eq.
- apply propproperty.
- apply propproperty.
Definition subtypesdirprod {X Y : UU} (A : hsubtype X) (B : hsubtype Y) :
hsubtype (X × Y) := λ xy : _, hconj (A (pr1 xy)) (B (pr2 xy)).
Definition fromdsubtypesdirprodcarrier {X Y : UU}
(A : hsubtype X) (B : hsubtype Y)
(xyis : subtypesdirprod A B) : dirprod A B.
Show proof.
intros.
set (xy := pr1 xyis). set (is := pr2 xyis).
set (x := pr1 xy). set (y := pr2 xy).
simpl in is. simpl in y.
apply (make_dirprod (tpair A x (pr1 is)) (tpair B y (pr2 is))).
set (xy := pr1 xyis). set (is := pr2 xyis).
set (x := pr1 xy). set (y := pr2 xy).
simpl in is. simpl in y.
apply (make_dirprod (tpair A x (pr1 is)) (tpair B y (pr2 is))).
Definition tosubtypesdirprodcarrier {X Y : UU}
(A : hsubtype X) (B : hsubtype Y)
(xisyis : dirprod A B) : subtypesdirprod A B.
Show proof.
intros.
set (xis := pr1 xisyis). set (yis := pr2 xisyis).
set (x := pr1 xis). set (isx := pr2 xis).
set (y := pr1 yis). set (isy := pr2 yis).
simpl in isx. simpl in isy.
apply (tpair (subtypesdirprod A B) (make_dirprod x y) (make_dirprod isx isy)).
set (xis := pr1 xisyis). set (yis := pr2 xisyis).
set (x := pr1 xis). set (isx := pr2 xis).
set (y := pr1 yis). set (isy := pr2 yis).
simpl in isx. simpl in isy.
apply (tpair (subtypesdirprod A B) (make_dirprod x y) (make_dirprod isx isy)).
Lemma weqsubtypesdirprod {X Y : UU} (A : hsubtype X) (B : hsubtype Y) :
subtypesdirprod A B ≃ A × B.
Show proof.
intros.
set (f := fromdsubtypesdirprodcarrier A B).
set (g := tosubtypesdirprodcarrier A B).
split with f.
assert (egf : ∏ a : _, paths (g (f a)) a).
{
intro a.
induction a as [ xy is ].
induction xy as [ x y ].
induction is as [ isx isy ].
apply idpath.
}
assert (efg : ∏ a : _, paths (f (g a)) a).
{
intro a.
induction a as [ xis yis ].
induction xis as [ x isx ].
induction yis as [ y isy ].
apply idpath.
}
apply (isweq_iso _ _ egf efg).
set (f := fromdsubtypesdirprodcarrier A B).
set (g := tosubtypesdirprodcarrier A B).
split with f.
assert (egf : ∏ a : _, paths (g (f a)) a).
{
intro a.
induction a as [ xy is ].
induction xy as [ x y ].
induction is as [ isx isy ].
apply idpath.
}
assert (efg : ∏ a : _, paths (f (g a)) a).
{
intro a.
induction a as [ xis yis ].
induction xis as [ x isx ].
induction yis as [ y isy ].
apply idpath.
}
apply (isweq_iso _ _ egf efg).
Lemma ishinhsubtypedirprod {X Y : UU} (A : hsubtype X) (B : hsubtype Y)
(isa : ishinh A) (isb : ishinh B) : ishinh (subtypesdirprod A B).
Show proof.
A subtype with paths between any two elements is an hProp.
Lemma isapropsubtype {X : UU} (A : hsubtype X)
(is : ∏ (x1 x2 : X), A x1 -> A x2 -> x1 = x2) : isaprop (carrier A).
Show proof.
intros. apply invproofirrelevance.
intros x x'.
assert (X0 : isincl (@pr1 _ A)).
{
apply isinclpr1.
intro x0.
apply (pr2 (A x0)).
}
apply (invmaponpathsincl (@pr1 _ A) X0).
induction x as [ x0 is0 ].
induction x' as [ x0' is0' ].
simpl.
apply (is x0 x0' is0 is0').
intros x x'.
assert (X0 : isincl (@pr1 _ A)).
{
apply isinclpr1.
intro x0.
apply (pr2 (A x0)).
}
apply (invmaponpathsincl (@pr1 _ A) X0).
induction x as [ x0 is0 ].
induction x' as [ x0' is0' ].
simpl.
apply (is x0 x0' is0 is0').
Definition squash_pairs_to_set {Y : UU} (F : Y -> UU) :
(isaset Y) -> (∏ y y', F y -> F y' -> y = y') -> (∃ y, F y) -> Y.
Show proof.
intros is e.
set (P := ∑ y, ∥ F y ∥).
assert (iP : isaprop P).
{
apply isapropsubtype. intros y y' f f'.
apply (squash_to_prop f). apply is. clear f; intro f.
apply (squash_to_prop f'). apply is. clear f'; intro f'.
apply e.
- assumption.
- assumption.
}
intros w.
assert (p : P).
{
apply (squash_to_prop w). exact iP. clear w; intro w.
exact (pr1 w,,hinhpr (pr2 w)).
}
clear w.
exact (pr1 p).
set (P := ∑ y, ∥ F y ∥).
assert (iP : isaprop P).
{
apply isapropsubtype. intros y y' f f'.
apply (squash_to_prop f). apply is. clear f; intro f.
apply (squash_to_prop f'). apply is. clear f'; intro f'.
apply e.
- assumption.
- assumption.
}
intros w.
assert (p : P).
{
apply (squash_to_prop w). exact iP. clear w; intro w.
exact (pr1 w,,hinhpr (pr2 w)).
}
clear w.
exact (pr1 p).
Definition squash_to_set {X Y : UU} (is : isaset Y) (f : X -> Y) :
(∏ x x', f x = f x') -> ∥ X ∥ -> Y.
Show proof.
intros e w.
set (P := ∑ y, ∃ x, f x = y).
assert (j : isaprop P).
{
apply isapropsubtype; intros y y' j j'.
apply (squash_to_prop j). apply is. clear j; intros [j k].
apply (squash_to_prop j'). apply is. clear j'; intros [j' k'].
intermediate_path (f j). exact (!k).
intermediate_path (f j'). apply e. exact k'.
}
assert (p : P).
{
apply (squash_to_prop w). exact j. intro x0.
exists (f x0). apply hinhpr. exists x0. apply idpath.
}
exact (pr1 p).
set (P := ∑ y, ∃ x, f x = y).
assert (j : isaprop P).
{
apply isapropsubtype; intros y y' j j'.
apply (squash_to_prop j). apply is. clear j; intros [j k].
apply (squash_to_prop j'). apply is. clear j'; intros [j' k'].
intermediate_path (f j). exact (!k).
intermediate_path (f j'). apply e. exact k'.
}
assert (p : P).
{
apply (squash_to_prop w). exact j. intro x0.
exists (f x0). apply hinhpr. exists x0. apply idpath.
}
exact (pr1 p).
Relations on types (or equivalently relations on the sets of connected components)
Relations and boolean relations
Definition hrel (X : UU) : UU := X -> X -> hProp.
Identity Coercion idhrel : hrel >-> Funclass.
Definition brel (X : UU) : UU := X -> X -> bool.
Identity Coercion idbrel : brel >-> Funclass.
Definition istrans {X : UU} (R : hrel X) : UU
:= ∏ (x1 x2 x3 : X), R x1 x2 -> R x2 x3 -> R x1 x3.
Definition isrefl {X : UU} (R : hrel X) : UU
:= ∏ x : X, R x x.
Definition issymm {X : UU} (R : hrel X) : UU
:= ∏ (x1 x2 : X), R x1 x2 -> R x2 x1.
Definition ispreorder {X : UU} (R : hrel X) : UU := istrans R × isrefl R.
Definition iseqrel {X : UU} (R : hrel X) := ispreorder R × issymm R.
Definition iseqrelconstr {X : UU} {R : hrel X}
(trans0 : istrans R) (refl0 : isrefl R) (symm0 : issymm R) :
iseqrel R := make_dirprod (make_dirprod trans0 refl0) symm0.
Definition isirrefl {X : UU} (R : hrel X) : UU := ∏ x : X, ¬ R x x.
Definition isasymm {X : UU} (R : hrel X) : UU
:= ∏ (x1 x2 : X), R x1 x2 -> R x2 x1 -> empty.
Definition iscoasymm {X : UU} (R : hrel X) : UU := ∏ x1 x2, ¬ R x1 x2 -> R x2 x1.
Definition istotal {X : UU} (R : hrel X) : UU := ∏ x1 x2, R x1 x2 ∨ R x2 x1.
Definition isdectotal {X : UU} (R : hrel X) : UU := ∏ x1 x2, R x1 x2 ⨿ R x2 x1.
Definition iscotrans {X : UU} (R : hrel X) : UU
:= ∏ x1 x2 x3, R x1 x3 -> R x1 x2 ∨ R x2 x3.
Definition isdeccotrans {X : UU} (R : hrel X) : UU
:= ∏ x1 x2 x3, R x1 x3 -> R x1 x2 ⨿ R x2 x3.
Definition isdecrel {X : UU} (R : hrel X) : UU := ∏ x1 x2, R x1 x2 ⨿ ¬ R x1 x2.
Definition isnegrel {X : UU} (R : hrel X) : UU
:= ∏ x1 x2, ¬ ¬ R x1 x2 -> R x1 x2.
Note that the property of being (co-)antisymmetric is different from other
properties of relations which we consider due to the presence of paths in
its formulation. As a consequence it behaves differently relative to the
quotients of types - the quotient relation can be (co-)antisymmetric while
the original relation was not.
Definition isantisymm {X : UU} (R : hrel X) : UU
:= ∏ (x1 x2 : X), R x1 x2 -> R x2 x1 -> x1 = x2.
Definition isPartialOrder {X : UU} (R : hrel X) : UU
:= ispreorder R × isantisymm R.
Ltac unwrap_isPartialOrder i :=
induction i as [transrefl antisymm]; induction transrefl as [trans refl].
Definition isantisymmneg {X : UU} (R : hrel X) : UU
:= ∏ (x1 x2 : X), ¬ R x1 x2 -> ¬ R x2 x1 -> x1 = x2.
Definition iscoantisymm {X : UU} (R : hrel X) : UU
:= ∏ x1 x2, ¬ R x1 x2 -> R x2 x1 ⨿ (x1 = x2).
Note that the following condition on a relation is different from all the
other which we have considered since it is not a property but a structure,
i.e. it is in general unclear whether isaprop (neqchoice R) is provable.
proofs that the properties are propositions
Lemma isaprop_istrans {X : hSet} (R : hrel X) : isaprop (istrans R).
Show proof.
Lemma isaprop_isrefl {X : hSet} (R : hrel X) : isaprop (isrefl R).
Show proof.
Lemma isaprop_istotal {X : hSet} (R : hrel X) : isaprop (istotal R).
Show proof.
Lemma isaprop_isantisymm {X : hSet} (R : hrel X) : isaprop (isantisymm R).
Show proof.
intros. unfold isantisymm. apply impred; intro x. apply impred; intro y.
apply impred; intro r. apply impred; intro s. apply setproperty.
apply impred; intro r. apply impred; intro s. apply setproperty.
Lemma isaprop_ispreorder {X : hSet} (R : hrel X) : isaprop (ispreorder R).
Show proof.
intros.
unfold ispreorder.
apply isapropdirprod.
{ apply isaprop_istrans. }
{ apply isaprop_isrefl. }
unfold ispreorder.
apply isapropdirprod.
{ apply isaprop_istrans. }
{ apply isaprop_isrefl. }
Lemma isaprop_isPartialOrder {X : hSet} (R : hrel X) :
isaprop (isPartialOrder R).
Show proof.
intros.
unfold isPartialOrder.
apply isapropdirprod.
{ apply isaprop_ispreorder. }
{ apply isaprop_isantisymm. }
unfold isPartialOrder.
apply isapropdirprod.
{ apply isaprop_ispreorder. }
{ apply isaprop_isantisymm. }
the relations on a set form a set
Definition isaset_hrel (X : hSet) : isaset (hrel X).
intros. unfold hrel.
apply impred_isaset; intro x.
apply impred_isaset; intro y.
exact isasethProp.
Defined.
Lemma istransandirrefltoasymm {X : UU} {R : hrel X}
(is1 : istrans R) (is2 : isirrefl R) : isasymm R.
Show proof.
intros. intros a b rab rba. apply (is2 _ (is1 _ _ _ rab rba)).
Lemma istotaltoiscoasymm {X : UU} {R : hrel X} (is : istotal R) : iscoasymm R.
Show proof.
Lemma isdecreltoisnegrel {X : UU} {R : hrel X} (is : isdecrel R) : isnegrel R.
Show proof.
intros. intros x1 x2.
induction (is x1 x2) as [ r | nr ].
- intro. apply r.
- intro nnr. induction (nnr nr).
induction (is x1 x2) as [ r | nr ].
- intro. apply r.
- intro nnr. induction (nnr nr).
Lemma isantisymmnegtoiscoantisymm {X : UU} {R : hrel X}
(isdr : isdecrel R) (isr : isantisymmneg R) : iscoantisymm R.
Show proof.
intros. intros x1 x2 nrx12.
induction (isdr x2 x1) as [ r | nr ].
apply (ii1 r). apply ii2. apply (isr _ _ nrx12 nr).
induction (isdr x2 x1) as [ r | nr ].
apply (ii1 r). apply ii2. apply (isr _ _ nrx12 nr).
Lemma rtoneq {X : UU} {R : hrel X} (is : isirrefl R) {a b : X} (r : R a b) :
a != b.
Show proof.
intros. intro e. rewrite e in r. apply (is b r).
Definition hrellogeq {X : UU} (L R : hrel X) : UU
:= ∏ x1 x2, (L x1 x2 <-> R x1 x2).
Definition istranslogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : istrans L) : istrans R.
Show proof.
intros. intros x1 x2 x3 r12 r23.
apply ((pr1 (lg _ _)) (isl _ _ _ ((pr2 (lg _ _)) r12) ((pr2 (lg _ _)) r23))).
apply ((pr1 (lg _ _)) (isl _ _ _ ((pr2 (lg _ _)) r12) ((pr2 (lg _ _)) r23))).
Definition isrefllogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : isrefl L) : isrefl R.
Show proof.
Definition issymmlogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : issymm L) : issymm R.
Show proof.
Definition ispologeqf {X : UU} {L R : hrel X} (lg : ∏ x1 x2, L x1 x2 <-> R x1 x2)
(isl : ispreorder L) : ispreorder R.
Show proof.
Definition iseqrellogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : iseqrel L) : iseqrel R.
Show proof.
Definition isirrefllogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : isirrefl L) : isirrefl R.
Show proof.
Definition isasymmlogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : isasymm L) : isasymm R.
Show proof.
Definition iscoasymmlogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : iscoasymm L) : iscoasymm R.
Show proof.
Definition istotallogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : istotal L) : istotal R.
Show proof.
intros. intros x1 x2. set (int := isl x1 x2).
generalize int. clear int. simpl. apply hinhfun.
apply (coprodf (pr1 (lg x1 x2)) (pr1 (lg x2 x1))).
generalize int. clear int. simpl. apply hinhfun.
apply (coprodf (pr1 (lg x1 x2)) (pr1 (lg x2 x1))).
Definition iscotranslogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : iscotrans L) : iscotrans R.
Show proof.
intros. intros x1 x2 x3 r13.
set (int := isl x1 x2 x3 (pr2 (lg _ _) r13)). generalize int.
clear int. simpl. apply hinhfun.
apply (coprodf (pr1 (lg x1 x2)) (pr1 (lg x2 x3))).
set (int := isl x1 x2 x3 (pr2 (lg _ _) r13)). generalize int.
clear int. simpl. apply hinhfun.
apply (coprodf (pr1 (lg x1 x2)) (pr1 (lg x2 x3))).
Definition isdecrellogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : isdecrel L) : isdecrel R.
Show proof.
intros. intros x1 x2.
induction (isl x1 x2) as [ l | nl ].
- apply (ii1 (pr1 (lg _ _) l)).
- apply (ii2 (negf (pr2 (lg _ _)) nl)).
induction (isl x1 x2) as [ l | nl ].
- apply (ii1 (pr1 (lg _ _) l)).
- apply (ii2 (negf (pr2 (lg _ _)) nl)).
Definition isnegrellogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : isnegrel L) : isnegrel R.
Show proof.
Definition isantisymmlogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : isantisymm L) :
isantisymm R.
Show proof.
Definition isantisymmneglogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : isantisymmneg L) :
isantisymmneg R.
Show proof.
intros. intros x1 x2 nr12 nr21.
apply (isl _ _ (negf (pr1 (lg _ _)) nr12) (negf (pr1 (lg _ _)) nr21)).
apply (isl _ _ (negf (pr1 (lg _ _)) nr12) (negf (pr1 (lg _ _)) nr21)).
Definition iscoantisymmlogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : iscoantisymm L) :
iscoantisymm R.
Show proof.
intros. intros x1 x2 r12.
set (int := isl _ _ (negf (pr1 (lg _ _)) r12)). generalize int. clear int.
simpl. apply (coprodf (pr1 (lg _ _)) (idfun _)).
set (int := isl _ _ (negf (pr1 (lg _ _)) r12)). generalize int. clear int.
simpl. apply (coprodf (pr1 (lg _ _)) (idfun _)).
Definition neqchoicelogeqf {X : UU} {L R : hrel X}
(lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : neqchoice L) : neqchoice R.
Show proof.
Definition po (X : UU) : UU := ∑ R : hrel X, ispreorder R.
Definition make_po {X : UU} (R : hrel X) (is : ispreorder R) : po X
:= tpair ispreorder R is.
Definition carrierofpo (X : UU) : po X -> (X -> X -> hProp) := @pr1 _ ispreorder.
Coercion carrierofpo : po >-> Funclass.
Definition PreorderedSet : UU := ∑ X : hSet, po X.
Definition PreorderedSetPair (X : hSet) (R :po X) : PreorderedSet
:= tpair _ X R.
Definition carrierofPreorderedSet : PreorderedSet -> hSet := pr1.
Coercion carrierofPreorderedSet : PreorderedSet >-> hSet.
Definition PreorderedSetRelation (X : PreorderedSet) : hrel X := pr1 (pr2 X).
Definition PartialOrder (X : hSet) : UU := ∑ R : hrel X, isPartialOrder R.
Definition make_PartialOrder {X : hSet} (R : hrel X) (is : isPartialOrder R) :
PartialOrder X
:= tpair isPartialOrder R is.
Definition carrierofPartialOrder {X : hSet} : PartialOrder X -> hrel X := pr1.
Coercion carrierofPartialOrder : PartialOrder >-> hrel.
Definition Poset : UU := ∑ X, PartialOrder X.
Definition make_Poset (X : hSet) (R : PartialOrder X) : Poset
:= tpair PartialOrder X R.
Definition carrierofposet : Poset -> hSet := pr1.
Coercion carrierofposet : Poset >-> hSet.
Definition posetRelation (X : Poset) : hrel X := pr1 (pr2 X).
Lemma isrefl_posetRelation (X : Poset) : isrefl (posetRelation X).
Show proof.
Lemma istrans_posetRelation (X : Poset) : istrans (posetRelation X).
Show proof.
Lemma isantisymm_posetRelation (X : Poset) : isantisymm (posetRelation X).
Show proof.
Declare Scope poset.
Delimit Scope poset with poset.
Notation "m ≤ n" := (posetRelation _ m n) (no associativity, at level 70) :
poset.
Definition isaposetmorphism {X Y : Poset} (f : X -> Y)
:= (∏ x x' : X, x ≤ x' -> f x ≤ f x')%poset.
Definition posetmorphism (X Y : Poset) : UU
:= total2 (fun f : X -> Y => isaposetmorphism f).
Definition make_posetmorphism (X Y : Poset) :
∏ t : X → Y, isaposetmorphism t → ∑ f : X → Y, isaposetmorphism f
:= tpair (fun f : X -> Y => isaposetmorphism f).
Definition carrierofposetmorphism (X Y : Poset) : posetmorphism X Y -> (X -> Y)
:= @pr1 _ _.
Coercion carrierofposetmorphism : posetmorphism >-> Funclass.
Definition isdec_ordering (X : Poset) : UU
:= ∏ (x y : X), decidable (x ≤ y)%poset.
Lemma isaprop_isaposetmorphism {X Y : Poset} (f : X -> Y) :
isaprop (isaposetmorphism f).
Show proof.
the preorders on a set form a set
Definition isaset_po (X : hSet) : isaset (po X).
intros.
unfold po.
apply (isofhleveltotal2 2).
{ apply isaset_hrel. }
intros x. apply hlevelntosn. apply isaprop_ispreorder.
Defined.
the partial orders on a set form a set
Definition isaset_PartialOrder X : isaset (PartialOrder X).
intros.
unfold PartialOrder.
apply (isofhleveltotal2 2).
{ apply isaset_hrel. }
intros x. apply hlevelntosn. apply isaprop_isPartialOrder.
Defined.
poset equivalences
Definition isPosetEquivalence {X Y : Poset} (f : X ≃ Y) :=
isaposetmorphism f × isaposetmorphism (invmap f).
Lemma isaprop_isPosetEquivalence {X Y : Poset} (f : X ≃ Y) :
isaprop (isPosetEquivalence f).
Show proof.
Definition isPosetEquivalence_idweq (X : Poset) : isPosetEquivalence (idweq X).
Show proof.
intros. split.
- intros x y le. exact le.
- intros x y le. exact le.
- intros x y le. exact le.
- intros x y le. exact le.
Definition PosetEquivalence (X Y : Poset) : UU
:= ∑ f : X ≃ Y, isPosetEquivalence f.
Local Open Scope poset.
Notation "X ≅ Y" := (PosetEquivalence X Y) (at level 60, no associativity) :
poset.
Definition posetUnderlyingEquivalence {X Y : Poset} : X ≅ Y -> X ≃ Y := pr1.
Coercion posetUnderlyingEquivalence : PosetEquivalence >-> weq.
Definition identityPosetEquivalence (X : Poset) : PosetEquivalence X X.
Show proof.
Lemma isincl_pr1_PosetEquivalence (X Y : Poset) : isincl (pr1 : X ≅ Y -> X ≃ Y).
Show proof.
Lemma isinj_pr1_PosetEquivalence (X Y : Poset) :
isInjective (pr1 : X ≅ Y -> X ≃ Y).
Show proof.
poset concepts
Notation "m < n" := (m ≤ n × m != n)%poset (only parsing) : poset.
Definition isMinimal {X : Poset} (x : X) : UU := ∏ y, x ≤ y.
Definition isMaximal {X : Poset} (x : X) : UU := ∏ y, y ≤ x.
Definition consecutive {X : Poset} (x y : X) : UU
:= x < y × ∏ z, ¬ (x < z × z < y).
Lemma isaprop_isMinimal {X : Poset} (x : X) : isaprop (isMaximal x).
Show proof.
Lemma isaprop_isMaximal {X : Poset} (x : X) : isaprop (isMaximal x).
Show proof.
Lemma isaprop_consecutive {X : Poset} (x y : X) : isaprop (consecutive x y).
Show proof.
intros. unfold consecutive. apply isapropdirprod.
- apply isapropdirprod. { apply pr2. } simpl. apply isapropneg.
- apply impred; intro z. apply isapropneg.
- apply isapropdirprod. { apply pr2. } simpl. apply isapropneg.
- apply impred; intro z. apply isapropneg.
Definition eqrel (X : UU) : UU := total2 (λ R : hrel X, iseqrel R).
Definition make_eqrel {X : UU} (R : hrel X) (is : iseqrel R) : eqrel X
:= tpair (λ R : hrel X, iseqrel R) R is.
Definition eqrelconstr {X : UU} (R : hrel X)
(is1 : istrans R) (is2 : isrefl R) (is3 : issymm R) : eqrel X
:= make_eqrel R (make_dirprod (make_dirprod is1 is2) is3).
Definition pr1eqrel (X : UU) : eqrel X -> (X -> (X -> hProp)) := @pr1 _ _.
Coercion pr1eqrel : eqrel >-> Funclass.
Definition eqreltrans {X : UU} (R : eqrel X) : istrans R := pr1 (pr1 (pr2 R)).
Definition eqrelrefl {X : UU} (R : eqrel X) : isrefl R := pr2 (pr1 (pr2 R)).
Definition eqrelsymm {X : UU} (R : eqrel X) : issymm R := pr2 (pr2 R).
Definition hreldirprod {X Y : UU} (RX : hrel X) (RY : hrel Y) :
hrel (X × Y)
:= λ xy xy' : dirprod X Y, hconj (RX (pr1 xy) (pr1 xy'))
(RY (pr2 xy) (pr2 xy')).
Definition istransdirprod {X Y : UU} (RX : hrel X) (RY : hrel Y)
(isx : istrans RX) (isy : istrans RY) :
istrans (hreldirprod RX RY)
:= λ xy1 xy2 xy3 : _,
λ is12 : _ ,
λ is23 : _,
make_dirprod (isx _ _ _ (pr1 is12) (pr1 is23))
(isy _ _ _ (pr2 is12) (pr2 is23)).
Definition isrefldirprod {X Y : UU} (RX : hrel X) (RY : hrel Y)
(isx : isrefl RX) (isy : isrefl RY) : isrefl (hreldirprod RX RY)
:= λ xy : _, make_dirprod (isx _) (isy _).
Definition issymmdirprod {X Y : UU} (RX : hrel X) (RY : hrel Y)
(isx : issymm RX) (isy : issymm RY) : issymm (hreldirprod RX RY)
:= λ xy1 xy2 : _, λ is12 : _, make_dirprod (isx _ _ (pr1 is12))
(isy _ _ (pr2 is12)).
Definition eqreldirprod {X Y : UU} (RX : eqrel X) (RY : eqrel Y) :
eqrel (X × Y)
:= eqrelconstr (hreldirprod RX RY)
(istransdirprod _ _ (eqreltrans RX) (eqreltrans RY))
(isrefldirprod _ _ (eqrelrefl RX) (eqrelrefl RY))
(issymmdirprod _ _ (eqrelsymm RX) (eqrelsymm RY)).
Definition negrel {X : UU} (R : hrel X) : hrel X
:= λ x x', make_hProp (¬ R x x') (isapropneg _).
Lemma istransnegrel {X : UU} (R : hrel X) (isr : iscotrans R) :
istrans (negrel R).
Show proof.
intros. intros x1 x2 x3 r12 r23.
apply (negf (isr x1 x2 x3)).
apply (toneghdisj (make_dirprod r12 r23)).
apply (negf (isr x1 x2 x3)).
apply (toneghdisj (make_dirprod r12 r23)).
Lemma isasymmnegrel {X : UU} (R : hrel X) (isr : iscoasymm R) :
isasymm (negrel R).
Show proof.
intros. intros x1 x2 r12 r21. apply (r21 (isr _ _ r12)).
Lemma iscoasymmgenrel {X : UU} (R : hrel X) (isr : isasymm R) :
iscoasymm (negrel R).
Show proof.
Lemma isdecnegrel {X : UU} (R : hrel X) (isr : isdecrel R) :
isdecrel (negrel R).
Show proof.
intros. intros x1 x2.
induction (isr x1 x2) as [ r | nr ].
- apply ii2. apply (todneg _ r).
- apply (ii1 nr).
induction (isr x1 x2) as [ r | nr ].
- apply ii2. apply (todneg _ r).
- apply (ii1 nr).
Lemma isnegnegrel {X : UU} (R : hrel X) : isnegrel (negrel R).
Show proof.
Lemma isantisymmnegrel {X : UU} (R : hrel X) (isr : isantisymmneg R) :
isantisymm (negrel R).
Show proof.
intros. apply isr.
Definition eqh {X : UU} (is : isdeceq X) : hrel X
:= λ x x', make_hProp (booleq is x x' = true)
(isasetbool (booleq is x x') true).
Definition neqh {X : UU} (is : isdeceq X) : hrel X
:= λ x x', make_hProp (booleq is x x' = false)
(isasetbool (booleq is x x') false).
Lemma isrefleqh {X : UU} (is : isdeceq X) : isrefl (eqh is).
Show proof.
intros. unfold eqh. unfold booleq.
intro x. induction (is x x) as [ e | ne ].
- simpl. apply idpath.
- induction (ne (idpath x)).
intro x. induction (is x x) as [ e | ne ].
- simpl. apply idpath.
- induction (ne (idpath x)).
Definition weqeqh {X : UU} (is : isdeceq X) (x x' : X) :
(x = x') ≃ (eqh is x x').
Show proof.
intros. apply weqimplimpl.
- intro e. induction e. apply isrefleqh.
- intro e. unfold eqh in e. unfold booleq in e.
induction (is x x') as [ e' | ne' ].
+ apply e'.
+ induction (nopathsfalsetotrue e).
- unfold isaprop. unfold isofhlevel. apply (isasetifdeceq X is x x').
- unfold eqh. simpl. unfold isaprop. unfold isofhlevel.
apply (isasetbool _ true).
- intro e. induction e. apply isrefleqh.
- intro e. unfold eqh in e. unfold booleq in e.
induction (is x x') as [ e' | ne' ].
+ apply e'.
+ induction (nopathsfalsetotrue e).
- unfold isaprop. unfold isofhlevel. apply (isasetifdeceq X is x x').
- unfold eqh. simpl. unfold isaprop. unfold isofhlevel.
apply (isasetbool _ true).
Definition weqneqh {X : UU} (is : isdeceq X) (x x' : X) :
(x != x') ≃ (neqh is x x').
Show proof.
intros. unfold neqh. unfold booleq. apply weqimplimpl.
- induction (is x x') as [ e | ne ].
+ intro ne. induction (ne e).
+ intro ne'. simpl. apply idpath.
- induction (is x x') as [ e | ne ].
+ intro tf. induction (nopathstruetofalse tf).
+ intro. exact ne.
- apply (isapropneg).
- simpl. unfold isaprop. unfold isofhlevel. apply (isasetbool _ false).
- induction (is x x') as [ e | ne ].
+ intro ne. induction (ne e).
+ intro ne'. simpl. apply idpath.
- induction (is x x') as [ e | ne ].
+ intro tf. induction (nopathstruetofalse tf).
+ intro. exact ne.
- apply (isapropneg).
- simpl. unfold isaprop. unfold isofhlevel. apply (isasetbool _ false).
Definition decrel (X : UU) : UU := total2 (λ R : hrel X, isdecrel R).
Definition pr1decrel (X : UU) : decrel X -> hrel X := @pr1 _ _.
Definition make_decrel {X : UU} {R : hrel X} (is : isdecrel R) : decrel X
:= tpair _ R is.
Coercion pr1decrel : decrel >-> hrel.
Definition decreltobrel {X : UU} (R : decrel X) : brel X.
Show proof.
Definition breltodecrel {X : UU} (B : brel X) : decrel X
:= @make_decrel _ (λ x x', make_hProp ((B x x') = true) (isasetbool _ _))
(λ x x', (isdeceqbool _ _)).
Definition pathstor {X : UU} (R : decrel X) (x x' : X)
(e : decreltobrel R x x' = true) : R x x'.
Show proof.
unfold decreltobrel in e.
induction (pr2 R x x') as [ e' | ne ].
- apply e'.
- induction (nopathsfalsetotrue e).
induction (pr2 R x x') as [ e' | ne ].
- apply e'.
- induction (nopathsfalsetotrue e).
Definition rtopaths {X : UU} (R : decrel X) (x x' : X) (r : R x x') :
decreltobrel R x x' = true.
Show proof.
unfold decreltobrel. intros. induction ((pr2 R) x x') as [ r' | nr ].
- apply idpath.
- induction (nr r).
- apply idpath.
- induction (nr r).
Definition pathstonegr {X : UU} (R : decrel X) (x x' : X)
(e : decreltobrel R x x' = false) : neg (R x x').
Show proof.
unfold decreltobrel in e. induction (pr2 R x x') as [ e' | ne ].
- induction (nopathstruetofalse e).
- apply ne.
- induction (nopathstruetofalse e).
- apply ne.
Definition negrtopaths {X : UU} (R : decrel X) (x x' : X) (nr : neg (R x x')) :
decreltobrel R x x' = false.
Show proof.
unfold decreltobrel. intros.
induction (pr2 R x x') as [ r | nr' ].
- induction (nr r).
- apply idpath.
induction (pr2 R x x') as [ r | nr' ].
- induction (nr r).
- apply idpath.
The following construction of "ct" ("canonical term") is inspired by the
ideas of George Gonthier. The expression ct (R, x, y) where R is in
hrel X for some X and has a canonical structure of a decidable relation
and x, y are closed terms of type X such that R x y is inhabited is the
term of type R x y which relizes the canonical term in isdecrel R x y.
Definition pathstor_comp {X : UU} (R : decrel X) (x x' : X)
(e : (decreltobrel R x x') = true) : R x x'.
Proof. unfold decreltobrel. intros. induction (pr2 R x x') as e' | ne .
apply e'. induction (nopathsfalsetotrue e).
Defined.
Notation " 'ct' (R, x, y) " := ((pathstor_comp _ x y (idpath true)) : R x y)
(at level 70).
Definition ctlong {X : UU} (R : hrel X) (is : isdecrel R) (x x' : X)
(e : decreltobrel (make_decrel is) x x' = true) : R x x'.
Show proof.
unfold decreltobrel in e. simpl in e. induction (is x x') as [ e' | ne ].
- apply e'.
- induction (nopathsfalsetotrue e).
- apply e'.
- induction (nopathsfalsetotrue e).
Notation " 'ct' ( R , is , x , y ) " := (ctlong R is x y (idpath true))
(at level 70).
Definition deceq_to_decrel {X:UU} : isdeceq X -> decrel X.
Show proof.
Definition confirm_equal {X : UU} (i : isdeceq X) (x x' : X)
(e : decreltobrel (deceq_to_decrel i) x x' = true) : x = x'.
Show proof.
Definition confirm_not_equal {X : UU} (i : isdeceq X) (x x' : X)
(e : decreltobrel (deceq_to_decrel i) x x' = false) : x != x'.
Show proof.
Ltac confirm_yes d x y := exact_op (pathstor d x y (idpath true)).
Ltac confirm_no d x y := exact_op (pathstonegr d x y (idpath false)).
Ltac confirm_equal i := match goal with |- ?x = ?y => confirm_yes (deceq_to_decrel i) x y end.
Ltac confirm_not_equal i := match goal with |- ?x != ?y => confirm_no (deceq_to_decrel i) x y end.
Ltac confirm_equal_absurd i := match goal with |- ?x = ?y → ∅ => confirm_no (deceq_to_decrel i) x y end.
Definition resrel {X : UU} (L : hrel X) (P : hsubtype X) : hrel P
:= λ p1 p2, L (pr1 p1) (pr1 p2).
Definition istransresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : istrans L) : istrans (resrel L P).
Show proof.
Definition isreflresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : isrefl L) : isrefl (resrel L P).
Show proof.
intros. intro x. apply isl.
Definition issymmresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : issymm L) : issymm (resrel L P).
Show proof.
intros. intros x1 x2 r12. apply isl. apply r12.
Definition isporesrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : ispreorder L) : ispreorder (resrel L P).
Show proof.
Definition iseqrelresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : iseqrel L) : iseqrel (resrel L P).
Show proof.
Definition isirreflresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : isirrefl L) : isirrefl (resrel L P).
Show proof.
intros. intros x r. apply (isl _ r).
Definition isasymmresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : isasymm L) : isasymm (resrel L P).
Show proof.
intros. intros x1 x2 r12 r21. apply (isl _ _ r12 r21).
Definition iscoasymmresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : iscoasymm L) : iscoasymm (resrel L P).
Show proof.
intros. intros x1 x2 r12. apply (isl _ _ r12).
Definition istotalresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : istotal L) : istotal (resrel L P).
Show proof.
intros. intros x1 x2. apply isl.
Definition iscotransresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : iscotrans L) : iscotrans (resrel L P).
Show proof.
intros. intros x1 x2 x3 r13. apply (isl _ _ _ r13).
Definition isdecrelresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : isdecrel L) : isdecrel (resrel L P).
Show proof.
intros. intros x1 x2. apply isl.
Definition isnegrelresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : isnegrel L) : isnegrel (resrel L P).
Show proof.
intros. intros x1 x2 nnr. apply (isl _ _ nnr).
Definition isantisymmresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : isantisymm L) : isantisymm (resrel L P).
Show proof.
intros. intros x1 x2 r12 r21.
apply (invmaponpathsincl _ (isinclpr1carrier _) _ _ (isl _ _ r12 r21)).
apply (invmaponpathsincl _ (isinclpr1carrier _) _ _ (isl _ _ r12 r21)).
Definition isantisymmnegresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : isantisymmneg L) : isantisymmneg (resrel L P).
Show proof.
intros. intros x1 x2 nr12 nr21.
apply (invmaponpathsincl _ (isinclpr1carrier _) _ _ (isl _ _ nr12 nr21)).
apply (invmaponpathsincl _ (isinclpr1carrier _) _ _ (isl _ _ nr12 nr21)).
Definition iscoantisymmresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : iscoantisymm L) : iscoantisymm (resrel L P).
Show proof.
intros. intros x1 x2 r12. induction (isl _ _ r12) as [ l | e ].
- apply (ii1 l).
- apply ii2. apply (invmaponpathsincl _ (isinclpr1carrier _) _ _ e).
- apply (ii1 l).
- apply ii2. apply (invmaponpathsincl _ (isinclpr1carrier _) _ _ e).
Definition neqchoiceresrel {X : UU} (L : hrel X) (P : hsubtype X)
(isl : neqchoice L) : neqchoice (resrel L P).
Show proof.
intros. intros x1 x2 ne.
set (int := negf (invmaponpathsincl _ (isinclpr1carrier P) _ _) ne).
apply (isl _ _ int).
set (int := negf (invmaponpathsincl _ (isinclpr1carrier P) _ _) ne).
apply (isl _ _ int).
Definition iseqclass {X : UU} (R : hrel X) (A : hsubtype X) : UU
:= dirprod (ishinh (carrier A))
(dirprod (∏ x1 x2 : X, R x1 x2 -> A x1 -> A x2)
(∏ x1 x2 : X, A x1 -> A x2 -> R x1 x2)).
Definition iseqclassconstr {X : UU} (R : hrel X) {A : hsubtype X}
(ax0 : ishinh (carrier A))
(ax1 : ∏ x1 x2 : X, R x1 x2 -> A x1 -> A x2)
(ax2 : ∏ x1 x2 : X, A x1 -> A x2 -> R x1 x2) : iseqclass R A
:= make_dirprod ax0 (make_dirprod ax1 ax2).
Definition eqax0 {X : UU} {R : hrel X} {A : hsubtype X} :
iseqclass R A -> ishinh (carrier A) := λ is : iseqclass R A, pr1 is.
Definition eqax1 {X : UU} {R : hrel X} {A : hsubtype X} :
iseqclass R A -> ∏ x1 x2 : X, R x1 x2 -> A x1 -> A x2
:= λ is : iseqclass R A, pr1 (pr2 is).
Definition eqax2 {X : UU} {R : hrel X} {A : hsubtype X} :
iseqclass R A -> ∏ x1 x2 : X, A x1 -> A x2 -> R x1 x2
:= λ is : iseqclass R A, pr2 (pr2 is).
Lemma isapropiseqclass {X : UU} (R : hrel X) (A : hsubtype X) :
isaprop (iseqclass R A).
Show proof.
apply isofhleveldirprod.
- exact (isapropishinh (carrier A)).
- apply isofhleveldirprod.
+ repeat (apply impred; intro).
exact (pr2 (A t0)).
+ repeat (apply impred; intro).
exact (pr2 (R t t0)).
- exact (isapropishinh (carrier A)).
- apply isofhleveldirprod.
+ repeat (apply impred; intro).
exact (pr2 (A t0)).
+ repeat (apply impred; intro).
exact (pr2 (R t t0)).
Lemma iseqclassdirprod {X Y : UU} {R : hrel X} {Q : hrel Y}
{A : hsubtype X} {B : hsubtype Y}
(isa : iseqclass R A) (isb : iseqclass Q B) :
iseqclass (hreldirprod R Q) (subtypesdirprod A B).
Show proof.
intros.
set (XY := dirprod X Y).
set (AB := subtypesdirprod A B).
set (RQ := hreldirprod R Q).
set (ax0 := ishinhsubtypedirprod A B (eqax0 isa) (eqax0 isb)).
assert (ax1 : ∏ xy1 xy2 : XY, RQ xy1 xy2 -> AB xy1 -> AB xy2).
{
intros xy1 xy2 rq ab1.
apply (make_dirprod (eqax1 isa _ _ (pr1 rq) (pr1 ab1))
(eqax1 isb _ _ (pr2 rq) (pr2 ab1))).
}
assert (ax2 : ∏ xy1 xy2 : XY, AB xy1 -> AB xy2 -> RQ xy1 xy2).
{
intros xy1 xy2 ab1 ab2.
apply (make_dirprod (eqax2 isa _ _ (pr1 ab1) (pr1 ab2))
(eqax2 isb _ _ (pr2 ab1) (pr2 ab2))).
}
apply (iseqclassconstr _ ax0 ax1 ax2).
set (XY := dirprod X Y).
set (AB := subtypesdirprod A B).
set (RQ := hreldirprod R Q).
set (ax0 := ishinhsubtypedirprod A B (eqax0 isa) (eqax0 isb)).
assert (ax1 : ∏ xy1 xy2 : XY, RQ xy1 xy2 -> AB xy1 -> AB xy2).
{
intros xy1 xy2 rq ab1.
apply (make_dirprod (eqax1 isa _ _ (pr1 rq) (pr1 ab1))
(eqax1 isb _ _ (pr2 rq) (pr2 ab1))).
}
assert (ax2 : ∏ xy1 xy2 : XY, AB xy1 -> AB xy2 -> RQ xy1 xy2).
{
intros xy1 xy2 ab1 ab2.
apply (make_dirprod (eqax2 isa _ _ (pr1 ab1) (pr1 ab2))
(eqax2 isb _ _ (pr2 ab1) (pr2 ab2))).
}
apply (iseqclassconstr _ ax0 ax1 ax2).
Theorem surjectionisepitosets {X Y Z : UU} (f : X -> Y) (g1 g2 : Y -> Z)
(is1 : issurjective f) (is2 : isaset Z)
(isf : ∏ x : X, g1 (f x) = g2 (f x)) : ∏ y : Y, g1 y = g2 y.
Show proof.
intros.
set (P1:= make_hProp (paths (g1 y) (g2 y)) (is2 (g1 y) (g2 y))).
unfold issurjective in is1.
assert (s1: (hfiber f y)-> paths (g1 y) (g2 y)).
{
intro X1. induction X1 as [t x ]. induction x. apply (isf t).
}
assert (s2: ishinh (paths (g1 y) (g2 y)))
by apply (hinhfun s1 (is1 y)).
set (is3 := is2 (g1 y) (g2 y)).
simpl in is3.
apply (@hinhuniv (paths (g1 y) (g2 y)) (make_hProp _ is3)).
- intro X1. assumption.
- assumption.
set (P1:= make_hProp (paths (g1 y) (g2 y)) (is2 (g1 y) (g2 y))).
unfold issurjective in is1.
assert (s1: (hfiber f y)-> paths (g1 y) (g2 y)).
{
intro X1. induction X1 as [t x ]. induction x. apply (isf t).
}
assert (s2: ishinh (paths (g1 y) (g2 y)))
by apply (hinhfun s1 (is1 y)).
set (is3 := is2 (g1 y) (g2 y)).
simpl in is3.
apply (@hinhuniv (paths (g1 y) (g2 y)) (make_hProp _ is3)).
- intro X1. assumption.
- assumption.
Epimorphisms are surjections to sets
TODO find a proof without univalence for propositions (if possible)
Lemma epiissurjectiontosets {A B : UU} (p : A -> B) (isB:isaset B)
(epip : ∏ (C:hSet) (g1 g2:B->C), (∏ x : A, g1 (p x) = g2 (p x)) ->
(∏ y : B, g1 y = g2 y)) : issurjective p.
Show proof.
(epip : ∏ (C:hSet) (g1 g2:B->C), (∏ x : A, g1 (p x) = g2 (p x)) ->
(∏ y : B, g1 y = g2 y)) : issurjective p.
Show proof.
intros.
assert(pred_set : isaset (B -> hProp)).
{ apply (isaset_set_fun_space _ (make_hSet _ isasethProp)). }
specialize (epip (make_hSet _ pred_set)
(λ b x, ∥ ∑ y : hfiber p b, x = p (pr1 y) ∥ )
(λ b x, make_hProp (x = b) (isB x b))
).
lapply epip.
- intro h.
intro y.
specialize (h y).
apply toforallpaths in h.
specialize (h y).
cbn in h.
match type of h with _ = ?type_witn => set (typ:= type_witn) in h end.
assert (witness:typ ).
{ apply idpath. }
revert witness.
rewrite <- h.
apply hinhfun.
intro h'.
exact (pr1 h').
- intro b.
apply funextfun.
intro x; cbn.
apply weqtopathshProp.
apply logeqweq.
+ apply hinhuniv.
intros [y eqx].
rewrite eqx.
apply (hfiberpr2 _ _ y).
+ intro eqx.
apply hinhpr.
use tpair.
* exists b. apply idpath.
* exact eqx.
assert(pred_set : isaset (B -> hProp)).
{ apply (isaset_set_fun_space _ (make_hSet _ isasethProp)). }
specialize (epip (make_hSet _ pred_set)
(λ b x, ∥ ∑ y : hfiber p b, x = p (pr1 y) ∥ )
(λ b x, make_hProp (x = b) (isB x b))
).
lapply epip.
- intro h.
intro y.
specialize (h y).
apply toforallpaths in h.
specialize (h y).
cbn in h.
match type of h with _ = ?type_witn => set (typ:= type_witn) in h end.
assert (witness:typ ).
{ apply idpath. }
revert witness.
rewrite <- h.
apply hinhfun.
intro h'.
exact (pr1 h').
- intro b.
apply funextfun.
intro x; cbn.
apply weqtopathshProp.
apply logeqweq.
+ apply hinhuniv.
intros [y eqx].
rewrite eqx.
apply (hfiberpr2 _ _ y).
+ intro eqx.
apply hinhpr.
use tpair.
* exists b. apply idpath.
* exact eqx.
Universal property enjoyed by surjections
f A ---> C | | p | v B
Section LiftSurjection.
Context {A B C :UU}.
Hypothesis hsc:isaset C.
Variables (p : A -> B ) (f: A -> C ).
Hypothesis comp_f_epi: ∏ x y, p x = p y -> f x = f y.
Hypothesis surjectivep : issurjective p.
Lemma surjective_iscontr_im : ∏ b : B, iscontr
(image (λ (x:hfiber p b), f (pr1 x))).
Show proof.
Definition univ_surj : B -> C :=
λ b, (pr1 (pr1 (surjective_iscontr_im b))).
Lemma univ_surj_ax : ∏ x, univ_surj (p x) = f x.
Show proof.
Lemma univ_surj_unique : ∏ (g : B -> C) (H : ∏ a : A, g (p a) = f a)
(b : B), g b = univ_surj b.
Show proof.
End LiftSurjection.
Context {A B C :UU}.
Hypothesis hsc:isaset C.
Variables (p : A -> B ) (f: A -> C ).
Hypothesis comp_f_epi: ∏ x y, p x = p y -> f x = f y.
Hypothesis surjectivep : issurjective p.
Lemma surjective_iscontr_im : ∏ b : B, iscontr
(image (λ (x:hfiber p b), f (pr1 x))).
Show proof.
intro b.
apply (squash_to_prop (surjectivep b)).
{ apply isapropiscontr. }
intro H.
apply iscontraprop1.
- apply isapropsubtype.
intros x1 x2.
apply (@hinhuniv2 _ _ (make_hProp _ (hsc _ _))).
simpl; intros y1 y2; simpl.
induction y1 as [ [z1 h1] h1' ].
induction y2 as [ [z2 h2] h2' ].
rewrite <- h1' ,<-h2'.
apply comp_f_epi;simpl.
rewrite h1,h2.
apply idpath.
- apply prtoimage. apply H.
apply (squash_to_prop (surjectivep b)).
{ apply isapropiscontr. }
intro H.
apply iscontraprop1.
- apply isapropsubtype.
intros x1 x2.
apply (@hinhuniv2 _ _ (make_hProp _ (hsc _ _))).
simpl; intros y1 y2; simpl.
induction y1 as [ [z1 h1] h1' ].
induction y2 as [ [z2 h2] h2' ].
rewrite <- h1' ,<-h2'.
apply comp_f_epi;simpl.
rewrite h1,h2.
apply idpath.
- apply prtoimage. apply H.
Definition univ_surj : B -> C :=
λ b, (pr1 (pr1 (surjective_iscontr_im b))).
Lemma univ_surj_ax : ∏ x, univ_surj (p x) = f x.
Show proof.
intro x.
apply pathsinv0.
apply path_to_ctr.
apply (squash_to_prop (surjectivep (p x))).
{ apply isapropishinh. }
intro r. apply hinhpr.
exists r.
apply comp_f_epi.
apply (pr2 r).
apply pathsinv0.
apply path_to_ctr.
apply (squash_to_prop (surjectivep (p x))).
{ apply isapropishinh. }
intro r. apply hinhpr.
exists r.
apply comp_f_epi.
apply (pr2 r).
Lemma univ_surj_unique : ∏ (g : B -> C) (H : ∏ a : A, g (p a) = f a)
(b : B), g b = univ_surj b.
Show proof.
intros g H b.
apply (surjectionisepitosets p); [assumption|assumption|].
intro x.
rewrite H,univ_surj_ax. apply idpath.
apply (surjectionisepitosets p); [assumption|assumption|].
intro x.
rewrite H,univ_surj_ax. apply idpath.
End LiftSurjection.
Set quotients of types.
Setquotient defined in terms of equivalence classes
Definition setquot {X : UU} (R : hrel X) : UU
:= total2 (λ A : _, iseqclass R A).
Definition make_setquot {X : UU} (R : hrel X) (A : hsubtype X)
(is : iseqclass R A) : setquot R := tpair _ A is.
Definition pr1setquot {X : UU} (R : hrel X) : setquot R -> (hsubtype X)
:= @pr1 _ (λ A : _, iseqclass R A).
Coercion pr1setquot : setquot >-> hsubtype.
Lemma isinclpr1setquot {X : UU} (R : hrel X) : isincl (pr1setquot R).
Show proof.
Theorem isasetsetquot {X : UU} (R : hrel X) : isaset (setquot R).
Show proof.
apply (isasetsubset (@pr1 _ _) (isasethsubtype X)).
apply isinclpr1; intro x.
apply isapropiseqclass.
apply isinclpr1; intro x.
apply isapropiseqclass.
Definition setquotinset {X : UU} (R : hrel X) : hSet :=
make_hSet _ (isasetsetquot R).
Theorem setquotpr {X : UU} (R : eqrel X) : X -> setquot R.
Show proof.
intros X0.
set (rax := eqrelrefl R).
set (sax := eqrelsymm R).
set (tax := eqreltrans R).
apply (tpair _ (λ x : X, R X0 x)).
split.
- exact (hinhpr (tpair _ X0 (rax X0))).
- split; intros x1 x2 X1 X2.
+ exact (tax X0 x1 x2 X2 X1).
+ exact (tax x1 X0 x2 (sax X0 x1 X1) X2).
set (rax := eqrelrefl R).
set (sax := eqrelsymm R).
set (tax := eqreltrans R).
apply (tpair _ (λ x : X, R X0 x)).
split.
- exact (hinhpr (tpair _ X0 (rax X0))).
- split; intros x1 x2 X1 X2.
+ exact (tax X0 x1 x2 X2 X1).
+ exact (tax x1 X0 x2 (sax X0 x1 X1) X2).
Lemma setquotl0 {X : UU} (R : eqrel X) (c : setquot R) (x : c) :
setquotpr R (pr1 x) = c.
Show proof.
apply (invmaponpathsincl _ (isinclpr1setquot R)).
apply funextsec; intro x0.
apply hPropUnivalence; intro r.
- exact (eqax1 (pr2 c) (pr1 x) x0 r (pr2 x)).
- exact (eqax2 (pr2 c) (pr1 x) x0 (pr2 x) r).
apply funextsec; intro x0.
apply hPropUnivalence; intro r.
- exact (eqax1 (pr2 c) (pr1 x) x0 r (pr2 x)).
- exact (eqax2 (pr2 c) (pr1 x) x0 (pr2 x) r).
Theorem issurjsetquotpr {X : UU} (R : eqrel X) : issurjective (setquotpr R).
Show proof.
intros. unfold issurjective.
intro c. apply (@hinhuniv (carrier (pr1 c))).
intro x. apply hinhpr.
split with (pr1 x).
- apply setquotl0.
- apply (eqax0 (pr2 c)).
intro c. apply (@hinhuniv (carrier (pr1 c))).
intro x. apply hinhpr.
split with (pr1 x).
- apply setquotl0.
- apply (eqax0 (pr2 c)).
Lemma iscompsetquotpr {X : UU} (R : eqrel X) (x x' : X) (a : R x x') :
setquotpr R x = setquotpr R x'.
Show proof.
intros. apply (invmaponpathsincl _ (isinclpr1setquot R)).
simpl. apply funextsec.
intro x0. apply hPropUnivalence.
intro r0. apply (eqreltrans R _ _ _ (eqrelsymm R _ _ a) r0).
intro x0'. apply (eqreltrans R _ _ _ a x0').
simpl. apply funextsec.
intro x0. apply hPropUnivalence.
intro r0. apply (eqreltrans R _ _ _ (eqrelsymm R _ _ a) r0).
intro x0'. apply (eqreltrans R _ _ _ a x0').
Universal property of seqtquot R for functions to sets satisfying compatibility condition iscomprelfun
Definition iscomprelfun {X Y : UU} (R : hrel X) (f : X -> Y) : UU
:= ∏ x x' : X, R x x' -> f x = f x'.
Lemma iscomprelfunlogeqf {X Y : UU} {R L : hrel X} (lg : hrellogeq L R)
(f : X -> Y) (is : iscomprelfun L f) : iscomprelfun R f.
Show proof.
Lemma isapropimeqclass {X : UU} (R : hrel X) (Y : hSet) (f : X -> Y)
(is : iscomprelfun R f) (c : setquot R) :
isaprop (image (λ x : c, f (pr1 x))).
Show proof.
intros. apply isapropsubtype.
intros y1 y2. simpl.
apply (@hinhuniv2 _ _ (make_hProp (y1 = y2) (pr2 Y y1 y2))).
intros x1 x2. simpl.
induction c as [ A iseq ].
induction x1 as [ x1 is1 ]. induction x2 as [ x2 is2 ].
induction x1 as [ x1 is1' ]. induction x2 as [ x2 is2' ].
simpl in is1. simpl in is2. simpl in is1'. simpl in is2'.
assert (r : R x1 x2) by apply (eqax2 iseq _ _ is1' is2').
apply (pathscomp0 (pathsinv0 is1) (pathscomp0 (is _ _ r) is2)).
Global Opaque isapropimeqclass.intros y1 y2. simpl.
apply (@hinhuniv2 _ _ (make_hProp (y1 = y2) (pr2 Y y1 y2))).
intros x1 x2. simpl.
induction c as [ A iseq ].
induction x1 as [ x1 is1 ]. induction x2 as [ x2 is2 ].
induction x1 as [ x1 is1' ]. induction x2 as [ x2 is2' ].
simpl in is1. simpl in is2. simpl in is1'. simpl in is2'.
assert (r : R x1 x2) by apply (eqax2 iseq _ _ is1' is2').
apply (pathscomp0 (pathsinv0 is1) (pathscomp0 (is _ _ r) is2)).
Theorem setquotuniv {X : UU} (R : hrel X) (Y : hSet) (f : X -> Y)
(is : iscomprelfun R f) (c : setquot R) : Y.
Show proof.
intros.
apply (pr1image (λ x : c, f (pr1 x))).
apply (@hinhuniv (pr1 c) (make_hProp _ (isapropimeqclass R Y f is c))
(prtoimage (λ x : c, f (pr1 x)))).
apply (eqax0 (pr2 c)).
apply (pr1image (λ x : c, f (pr1 x))).
apply (@hinhuniv (pr1 c) (make_hProp _ (isapropimeqclass R Y f is c))
(prtoimage (λ x : c, f (pr1 x)))).
apply (eqax0 (pr2 c)).
Note : the axioms rax, sax and trans are not used in the proof of
setquotuniv. If we consider a relation which is not an equivalence relation
then setquot will still be the set of subsets which are equivalence classes.
Now however such subsets need not to cover all of the type. In fact their set
can be empty. Nevertheless setquotuniv will apply.
Theorem setquotunivcomm {X : UU} (R : eqrel X) (Y : hSet) (f : X -> Y)
(is : iscomprelfun R f) :
∏ x : X, setquotuniv R Y f is (setquotpr R x) = f x.
Show proof.
Theorem weqpathsinsetquot {X : UU} (R : eqrel X) (x x' : X) :
R x x' ≃ setquotpr R x = setquotpr R x'.
Show proof.
intros. split with (iscompsetquotpr R x x').
apply isweqimplimpl.
- intro e.
set (e' := maponpaths (pr1setquot R) e).
unfold pr1setquot in e'. unfold setquotpr in e'. simpl in e'.
set (e'' := maponpaths (λ f : _, f x') e'). simpl in e''.
apply (eqweqmaphProp (pathsinv0 e'') (eqrelrefl R x')).
- apply (pr2 (R x x')).
- set (int := isasetsetquot R (setquotpr R x) (setquotpr R x')). assumption.
apply isweqimplimpl.
- intro e.
set (e' := maponpaths (pr1setquot R) e).
unfold pr1setquot in e'. unfold setquotpr in e'. simpl in e'.
set (e'' := maponpaths (λ f : _, f x') e'). simpl in e''.
apply (eqweqmaphProp (pathsinv0 e'') (eqrelrefl R x')).
- apply (pr2 (R x x')).
- set (int := isasetsetquot R (setquotpr R x) (setquotpr R x')). assumption.
Functoriality of setquot for functions mapping one relation to another
Definition iscomprelrelfun {X Y : UU} (RX : hrel X) (RY : hrel Y) (f : X -> Y)
: UU := ∏ x x' : X, RX x x' -> RY (f x) (f x').
Lemma iscomprelfunlogeqf1 {X Y : UU} {LX RX : hrel X} (RY : hrel Y)
(lg : hrellogeq LX RX) (f : X -> Y) (is : iscomprelrelfun LX RY f) :
iscomprelrelfun RX RY f.
Show proof.
Lemma iscomprelfunlogeqf2 {X Y : UU} (RX : hrel X) {LY RY : hrel Y}
(lg : hrellogeq LY RY) (f : X -> Y) (is : iscomprelrelfun RX LY f) :
iscomprelrelfun RX RY f.
Show proof.
Definition setquotfun {X Y : UU} (RX : hrel X) (RY : eqrel Y) (f : X -> Y)
(is : iscomprelrelfun RX RY f) (cx : setquot RX) : setquot RY.
Show proof.
intros.
set (ff := funcomp f (setquotpr RY)).
assert (isff : iscomprelfun RX ff).
{
intros x x'. intro r.
apply (weqpathsinsetquot RY (f x) (f x')).
apply is. apply r.
}
apply (setquotuniv RX (setquotinset RY) ff isff cx).
set (ff := funcomp f (setquotpr RY)).
assert (isff : iscomprelfun RX ff).
{
intros x x'. intro r.
apply (weqpathsinsetquot RY (f x) (f x')).
apply is. apply r.
}
apply (setquotuniv RX (setquotinset RY) ff isff cx).
Definition setquotfuncomm {X Y : UU} (RX : eqrel X) (RY : eqrel Y)
(f : X -> Y) (is : iscomprelrelfun RX RY f) :
∏ x : X, setquotfun RX RY f is (setquotpr RX x) = setquotpr RY (f x).
Show proof.
Universal property of setquot for predicates of one and several variables
Theorem setquotunivprop {X : UU} (R : eqrel X) (P : setquot (pr1 R) -> hProp)
(ps : ∏ x : X, pr1 (P (setquotpr R x))) : ∏ c : setquot (pr1 R), pr1 (P c).
Show proof.
intros c.
apply (@hinhuniv (carrier (pr1 c)) (P c)).
- intro x.
set (e := setquotl0 R c x).
apply (eqweqmaphProp (maponpaths P e)).
exact (ps (pr1 x)).
- exact (eqax0 (pr2 c)).
apply (@hinhuniv (carrier (pr1 c)) (P c)).
- intro x.
set (e := setquotl0 R c x).
apply (eqweqmaphProp (maponpaths P e)).
exact (ps (pr1 x)).
- exact (eqax0 (pr2 c)).
Theorem setquotuniv2prop {X : UU} (R : eqrel X)
(P : setquot R -> setquot R -> hProp)
(is : ∏ x x' : X, P (setquotpr R x) (setquotpr R x')) :
∏ c c' : setquot R, P c c'.
Show proof.
intros.
assert (int1 : ∏ c0' : _, P c c0').
{
apply (setquotunivprop R (λ c0', P c c0')).
intro x. apply (setquotunivprop R (λ c0 : _, P c0 (setquotpr R x))).
intro x0. apply (is x0 x).
}
apply (int1 c').
assert (int1 : ∏ c0' : _, P c c0').
{
apply (setquotunivprop R (λ c0', P c c0')).
intro x. apply (setquotunivprop R (λ c0 : _, P c0 (setquotpr R x))).
intro x0. apply (is x0 x).
}
apply (int1 c').
Theorem setquotuniv3prop {X : UU} (R : eqrel X)
(P : setquot R -> setquot R -> setquot R -> hProp)
(is : ∏ x x' x'' : X, P (setquotpr R x) (setquotpr R x')
(setquotpr R x'')) :
∏ c c' c'' : setquot R, P c c' c''.
Show proof.
intros.
assert (int1 : ∏ c0' c0'' : _, P c c0' c0'').
{
apply (setquotuniv2prop R (λ c0' c0'', P c c0' c0'')).
intros x x'.
apply (setquotunivprop R (λ c0 : _, P c0 (setquotpr R x)
(setquotpr R x'))).
intro x0. apply (is x0 x x').
}
apply (int1 c' c'').
assert (int1 : ∏ c0' c0'' : _, P c c0' c0'').
{
apply (setquotuniv2prop R (λ c0' c0'', P c c0' c0'')).
intros x x'.
apply (setquotunivprop R (λ c0 : _, P c0 (setquotpr R x)
(setquotpr R x'))).
intro x0. apply (is x0 x x').
}
apply (int1 c' c'').
Theorem setquotuniv4prop {X : UU} (R : eqrel X)
(P : setquot R -> setquot R -> setquot R -> setquot R -> hProp)
(is : ∏ x x' x'' x''' : X, P (setquotpr R x) (setquotpr R x')
(setquotpr R x'') (setquotpr R x''')) :
∏ c c' c'' c''' : setquot R, P c c' c'' c'''.
Show proof.
intros.
assert (int1 : ∏ c0 c0' c0'' : _, P c c0 c0' c0'').
{
apply (setquotuniv3prop R (λ c0 c0' c0'', P c c0 c0' c0'')).
intros x x' x''.
apply (setquotunivprop R (λ c0 : _, P c0 (setquotpr R x) (setquotpr R x')
(setquotpr R x''))).
intro x0. apply (is x0 x x' x'').
}
apply (int1 c' c'' c''').
assert (int1 : ∏ c0 c0' c0'' : _, P c c0 c0' c0'').
{
apply (setquotuniv3prop R (λ c0 c0' c0'', P c c0 c0' c0'')).
intros x x' x''.
apply (setquotunivprop R (λ c0 : _, P c0 (setquotpr R x) (setquotpr R x')
(setquotpr R x''))).
intro x0. apply (is x0 x x' x'').
}
apply (int1 c' c'' c''').
Important note : theorems proved above can not be used (al least at the
moment) to construct terms whose complete normalization (evaluation) is
important. For example they should not be used * directly * to construct
isdeceq property of setquot since isdeceq is in turn used to construct
boolean equality booleq and evaluation of booleq x y is important for
computational purposes. Terms produced using these universality theorems will
not fully normalize even in simple cases due to the following steps in the
proof of setquotunivprop. As a part of the proof term of this theorem there
appears the composition of an application of hPropUnivalence, transfer of
the resulting term of the identity type by maponpaths along P followed by
the reconstruction of a equivalence (two directional implication) between the
corresponding propositions through eqweqmaphProp. The resulting
implications are "opaque" and the proofs of disjunctions P \/ Q produced
with the use of such implications can not be evaluated to one of the summands
of the disjunction. An example is given by the following theorem
isdeceqsetquot_non_constr which, as simple experiments show, can not be used
to compute the value of isdeceqsetquot. Below we give another proof of
isdeceq (setquot R) using the same assumptions which is "constructive"
i.e. usable for the evaluation purposes.
The case when setquotfun is a surjection, inclusion or a weak equivalence
Lemma issurjsetquotfun {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X -> Y)
(is : issurjective f) (is1 : iscomprelrelfun RX RY f) :
issurjective (setquotfun RX RY f is1).
Show proof.
intros. apply (issurjtwooutof3b (setquotpr RX)).
apply (issurjcomp f (setquotpr RY) is (issurjsetquotpr RY)).
apply (issurjcomp f (setquotpr RY) is (issurjsetquotpr RY)).
Lemma isinclsetquotfun {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X -> Y)
(is1 : iscomprelrelfun RX RY f)
(is2 : ∏ x x' : X, RY (f x) (f x') -> RX x x') :
isincl (setquotfun RX RY f is1).
Show proof.
intros. apply isinclbetweensets.
- apply isasetsetquot.
- apply isasetsetquot.
- assert (is : ∏ (x x' : setquot RX),
isaprop (paths (setquotfun RX RY f is1 x)
(setquotfun RX RY f is1 x') -> x = x')).
{
intros.
apply impred. intro.
apply isasetsetquot.
}
apply (setquotuniv2prop RX (λ x x', make_hProp _ (is x x'))).
simpl. intros x x'. intro e.
set (e' := invweq (weqpathsinsetquot RY (f x) (f x')) e).
apply (weqpathsinsetquot RX _ _ (is2 x x' e')).
- apply isasetsetquot.
- apply isasetsetquot.
- assert (is : ∏ (x x' : setquot RX),
isaprop (paths (setquotfun RX RY f is1 x)
(setquotfun RX RY f is1 x') -> x = x')).
{
intros.
apply impred. intro.
apply isasetsetquot.
}
apply (setquotuniv2prop RX (λ x x', make_hProp _ (is x x'))).
simpl. intros x x'. intro e.
set (e' := invweq (weqpathsinsetquot RY (f x) (f x')) e).
apply (weqpathsinsetquot RX _ _ (is2 x x' e')).
Definition setquotincl {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X -> Y)
(is1 : iscomprelrelfun RX RY f)
(is2 : ∏ x x' : X, RY (f x) (f x') -> RX x x') :
incl (setquot RX) (setquot RY)
:= make_incl (setquotfun RX RY f is1) (isinclsetquotfun RX RY f is1 is2).
Definition weqsetquotweq {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X ≃ Y)
(is1 : iscomprelrelfun RX RY f)
(is2 : ∏ x x' : X, RY (f x) (f x') -> RX x x') :
(setquot RX) ≃ (setquot RY).
Show proof.
intros.
set (ff := setquotfun RX RY f is1). split with ff.
assert (is2' : ∏ y y' : Y, RY y y' -> RX (invmap f y) (invmap f y')).
intros y y'.
rewrite (pathsinv0 (homotweqinvweq f y)).
rewrite (pathsinv0 (homotweqinvweq f y')).
rewrite (homotinvweqweq f (invmap f y)).
rewrite (homotinvweqweq f (invmap f y')).
apply (is2 _ _). set (gg := setquotfun RY RX (invmap f) is2').
assert (egf : ∏ a, paths (gg (ff a)) a).
{
apply (setquotunivprop
RX (λ a0, make_hProp _ (isasetsetquot RX (gg (ff a0)) a0))).
simpl. intro x. unfold ff. unfold gg.
apply (maponpaths (setquotpr RX) (homotinvweqweq f x)).
}
assert (efg : ∏ a, paths (ff (gg a)) a).
{
apply (setquotunivprop
RY (λ a0, make_hProp _ (isasetsetquot RY (ff (gg a0)) a0))).
simpl. intro x. unfold ff. unfold gg.
apply (maponpaths (setquotpr RY) (homotweqinvweq f x)).
}
apply (isweq_iso _ _ egf efg).
set (ff := setquotfun RX RY f is1). split with ff.
assert (is2' : ∏ y y' : Y, RY y y' -> RX (invmap f y) (invmap f y')).
intros y y'.
rewrite (pathsinv0 (homotweqinvweq f y)).
rewrite (pathsinv0 (homotweqinvweq f y')).
rewrite (homotinvweqweq f (invmap f y)).
rewrite (homotinvweqweq f (invmap f y')).
apply (is2 _ _). set (gg := setquotfun RY RX (invmap f) is2').
assert (egf : ∏ a, paths (gg (ff a)) a).
{
apply (setquotunivprop
RX (λ a0, make_hProp _ (isasetsetquot RX (gg (ff a0)) a0))).
simpl. intro x. unfold ff. unfold gg.
apply (maponpaths (setquotpr RX) (homotinvweqweq f x)).
}
assert (efg : ∏ a, paths (ff (gg a)) a).
{
apply (setquotunivprop
RY (λ a0, make_hProp _ (isasetsetquot RY (ff (gg a0)) a0))).
simpl. intro x. unfold ff. unfold gg.
apply (maponpaths (setquotpr RY) (homotweqinvweq f x)).
}
apply (isweq_iso _ _ egf efg).
Definition weqsetquotsurj {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X -> Y)
(is : issurjective f) (is1 : iscomprelrelfun RX RY f)
(is2 : ∏ x x' : X, RY (f x) (f x') -> RX x x') :
(setquot RX) ≃ (setquot RY).
Show proof.
intros.
set (ff := setquotfun RX RY f is1).
split with ff.
apply (@isweqinclandsurj (setquotinset RX) (setquotinset RY) ff).
apply (isinclsetquotfun RX RY f is1 is2).
apply (issurjsetquotfun RX RY f is is1).
set (ff := setquotfun RX RY f is1).
split with ff.
apply (@isweqinclandsurj (setquotinset RX) (setquotinset RY) ff).
apply (isinclsetquotfun RX RY f is1 is2).
apply (issurjsetquotfun RX RY f is is1).
setquot with respect to the product of two relations
Definition setquottodirprod {X Y : UU} (RX : eqrel X) (RY : eqrel Y)
(cc : setquot (eqreldirprod RX RY)) :
(setquot RX) × (setquot RY).
Show proof.
intros.
set (RXY := eqreldirprod RX RY).
apply (make_dirprod
(setquotuniv RXY (setquotinset RX)
(funcomp (@pr1 _ (λ x : _, Y)) (setquotpr RX))
(λ xy xy' : dirprod X Y,
λ rr : RXY xy xy',
iscompsetquotpr RX _ _ (pr1 rr)) cc)
(setquotuniv RXY (setquotinset RY) (funcomp (@pr2 _ (λ x : _, Y))
(setquotpr RY))
(λ xy xy' : dirprod X Y,
λ rr : RXY xy xy',
iscompsetquotpr RY _ _ (pr2 rr)) cc)).
set (RXY := eqreldirprod RX RY).
apply (make_dirprod
(setquotuniv RXY (setquotinset RX)
(funcomp (@pr1 _ (λ x : _, Y)) (setquotpr RX))
(λ xy xy' : dirprod X Y,
λ rr : RXY xy xy',
iscompsetquotpr RX _ _ (pr1 rr)) cc)
(setquotuniv RXY (setquotinset RY) (funcomp (@pr2 _ (λ x : _, Y))
(setquotpr RY))
(λ xy xy' : dirprod X Y,
λ rr : RXY xy xy',
iscompsetquotpr RY _ _ (pr2 rr)) cc)).
Definition dirprodtosetquot {X Y : UU} (RX : hrel X) (RY : hrel Y)
(cd : (setquot RX) × (setquot RY)) :
setquot (hreldirprod RX RY)
:= make_setquot _ _ (iseqclassdirprod (pr2 (pr1 cd)) (pr2 (pr2 cd))).
Theorem weqsetquottodirprod {X Y : UU} (RX : eqrel X) (RY : eqrel Y) :
weq (setquot (eqreldirprod RX RY)) ((setquot RX) × (setquot RY)).
Show proof.
intros.
set (f := setquottodirprod RX RY).
set (g := dirprodtosetquot RX RY).
split with f.
assert (egf : ∏ a : _, paths (g (f a)) a).
{
apply (setquotunivprop _ (λ a : _, (make_hProp _ (isasetsetquot _ (g (f a))
a)))).
intro xy. induction xy as [ x y ]. simpl.
apply (invmaponpathsincl _ (isinclpr1setquot _)).
simpl. apply funextsec. intro xy'.
induction xy' as [ x' y' ]. apply idpath.
}
assert (efg : ∏ a : _, paths (f (g a)) a).
{
intro a. induction a as [ ax ay ]. apply pathsdirprod.
generalize ax. clear ax.
apply (setquotunivprop RX (λ ax : _, (make_hProp _ (isasetsetquot _ _ _)))).
intro x. simpl. generalize ay. clear ay.
apply (setquotunivprop RY (λ ay : _, (make_hProp _ (isasetsetquot _ _ _)))).
intro y. simpl.
apply (invmaponpathsincl _ (isinclpr1setquot _)). apply funextsec.
intro x0. simpl. apply idpath. generalize ax. clear ax.
apply (setquotunivprop RX (λ ax : _, (make_hProp _ (isasetsetquot _ _ _)))).
intro x. simpl. generalize ay. clear ay.
apply (setquotunivprop RY (λ ay : _, (make_hProp _ (isasetsetquot _ _ _)))).
intro y. simpl.
apply (invmaponpathsincl _ (isinclpr1setquot _)). apply funextsec.
intro x0. simpl. apply idpath.
}
apply (isweq_iso _ _ egf efg).
set (f := setquottodirprod RX RY).
set (g := dirprodtosetquot RX RY).
split with f.
assert (egf : ∏ a : _, paths (g (f a)) a).
{
apply (setquotunivprop _ (λ a : _, (make_hProp _ (isasetsetquot _ (g (f a))
a)))).
intro xy. induction xy as [ x y ]. simpl.
apply (invmaponpathsincl _ (isinclpr1setquot _)).
simpl. apply funextsec. intro xy'.
induction xy' as [ x' y' ]. apply idpath.
}
assert (efg : ∏ a : _, paths (f (g a)) a).
{
intro a. induction a as [ ax ay ]. apply pathsdirprod.
generalize ax. clear ax.
apply (setquotunivprop RX (λ ax : _, (make_hProp _ (isasetsetquot _ _ _)))).
intro x. simpl. generalize ay. clear ay.
apply (setquotunivprop RY (λ ay : _, (make_hProp _ (isasetsetquot _ _ _)))).
intro y. simpl.
apply (invmaponpathsincl _ (isinclpr1setquot _)). apply funextsec.
intro x0. simpl. apply idpath. generalize ax. clear ax.
apply (setquotunivprop RX (λ ax : _, (make_hProp _ (isasetsetquot _ _ _)))).
intro x. simpl. generalize ay. clear ay.
apply (setquotunivprop RY (λ ay : _, (make_hProp _ (isasetsetquot _ _ _)))).
intro y. simpl.
apply (invmaponpathsincl _ (isinclpr1setquot _)). apply funextsec.
intro x0. simpl. apply idpath.
}
apply (isweq_iso _ _ egf efg).
Universal property of setquot for functions of two variables
Definition iscomprelfun2 {X Y : UU} (R : hrel X) (f : X -> X -> Y) : UU
:= ∏ x x' x0 x0' : X, R x x' -> R x0 x0' -> f x x0 = f x' x0'.
Lemma iscomprelfun2if {X Y : UU} (R : hrel X) (f : X -> X -> Y)
(is1 : ∏ x x' x0 : X, R x x' -> f x x0 = f x' x0)
(is2 : ∏ x x0 x0' : X, R x0 x0' -> f x x0 = f x x0') : iscomprelfun2 R f.
Show proof.
intros. intros x x' x0 x0'. intros r r'.
set (e := is1 x x' x0 r).
set (e' := is2 x' x0 x0' r').
apply (pathscomp0 e e').
set (e := is1 x x' x0 r).
set (e' := is2 x' x0 x0' r').
apply (pathscomp0 e e').
Lemma iscomprelfun2logeqf {X Y : UU} {L R : hrel X} (lg : hrellogeq L R)
(f : X -> X -> Y) (is : iscomprelfun2 L f) : iscomprelfun2 R f.
Show proof.
Local Lemma setquotuniv2_iscomprelfun {X : UU} (R : hrel X) (Y : hSet) (f : X -> X -> Y)
(is : iscomprelfun2 R f) (c c0 : setquot R) :
iscomprelfun (hreldirprod R R) (λ xy : dirprod X X, f (pr1 xy) (pr2 xy)).
Show proof.
intros xy x'y'. simpl. intro dp. induction dp as [ r r'].
apply (is _ _ _ _ r r').
Global Opaque setquotuniv2_iscomprelfun.apply (is _ _ _ _ r r').
Definition setquotuniv2 {X : UU} (R : hrel X) (Y : hSet) (f : X -> X -> Y)
(is : iscomprelfun2 R f) (c c0 : setquot R) : Y.
Show proof.
intros.
set (ff := λ xy : dirprod X X, f (pr1 xy) (pr2 xy)).
set (RR := hreldirprod R R).
apply (setquotuniv RR Y ff (setquotuniv2_iscomprelfun R Y f is c c0)
(dirprodtosetquot R R (make_dirprod c c0))).
set (ff := λ xy : dirprod X X, f (pr1 xy) (pr2 xy)).
set (RR := hreldirprod R R).
apply (setquotuniv RR Y ff (setquotuniv2_iscomprelfun R Y f is c c0)
(dirprodtosetquot R R (make_dirprod c c0))).
Theorem setquotuniv2comm {X : UU} (R : eqrel X) (Y : hSet) (f : X -> X -> Y)
(is : iscomprelfun2 R f) :
∏ x x' : X, setquotuniv2 R Y f is (setquotpr R x) (setquotpr R x') = f x x'.
Show proof.
Functoriality of setquot for functions of two variables mapping one relation to another
Definition iscomprelrelfun2 {X Y : UU} (RX : hrel X) (RY : hrel Y)
(f : X -> X -> Y) : UU
:= ∏ x x' x0 x0' : X, RX x x' -> RX x0 x0' -> RY (f x x0) (f x' x0').
Lemma iscomprelrelfun2if {X Y : UU} (RX : hrel X) (RY : eqrel Y)
(f : X -> X -> Y)
(is1 : ∏ x x' x0 : X, RX x x' -> RY (f x x0) (f x' x0))
(is2 : ∏ x x0 x0' : X, RX x0 x0' -> RY (f x x0) (f x x0')) :
iscomprelrelfun2 RX RY f.
Show proof.
intros. intros x x' x0 x0'. intros r r'.
set (e := is1 x x' x0 r). set (e' := is2 x' x0 x0' r').
apply (eqreltrans RY _ _ _ e e').
set (e := is1 x x' x0 r). set (e' := is2 x' x0 x0' r').
apply (eqreltrans RY _ _ _ e e').
Lemma iscomprelrelfun2logeqf1 {X Y : UU} {LX RX : hrel X} (RY : hrel Y)
(lg : hrellogeq LX RX) (f : X -> X -> Y) (is : iscomprelrelfun2 LX RY f) :
iscomprelrelfun2 RX RY f.
Show proof.
Lemma iscomprelrelfun2logeqf2 {X Y : UU} (RX : hrel X) {LY RY : hrel Y}
(lg : hrellogeq LY RY) (f : X -> X -> Y) (is : iscomprelrelfun2 RX LY f) :
iscomprelrelfun2 RX RY f.
Show proof.
Local Lemma setquotfun2_iscomprelfun2 {X Y : UU} (RX : hrel X) (RY : eqrel Y)
(f : X -> X -> Y) (is : iscomprelrelfun2 RX RY f)
(cx cx0 : setquot RX) : iscomprelfun2 RX (λ x x0 : X, setquotpr RY (f x x0)).
Show proof.
intros x x' x0 x0'. intros r r0.
apply (weqpathsinsetquot RY (f x x0) (f x' x0')).
apply is. apply r. apply r0.
Global Opaque setquotfun2_iscomprelfun2.apply (weqpathsinsetquot RY (f x x0) (f x' x0')).
apply is. apply r. apply r0.
Definition setquotfun2 {X Y : UU} (RX : hrel X) (RY : eqrel Y)
(f : X -> X -> Y) (is : iscomprelrelfun2 RX RY f)
(cx cx0 : setquot RX) : setquot RY.
Show proof.
intros.
set (ff := λ x x0 : X, setquotpr RY (f x x0)).
exact (setquotuniv2 RX (setquotinset RY) ff (setquotfun2_iscomprelfun2 RX RY f is cx cx0) cx cx0).
set (ff := λ x x0 : X, setquotpr RY (f x x0)).
exact (setquotuniv2 RX (setquotinset RY) ff (setquotfun2_iscomprelfun2 RX RY f is cx cx0) cx cx0).
Theorem setquotfun2comm {X Y : UU} (RX : eqrel X) (RY : eqrel Y)
(f : X -> X -> Y) (is : iscomprelrelfun2 RX RY f) :
∏ (x x' : X), setquotfun2 RX RY f is (setquotpr RX x) (setquotpr RX x')
= setquotpr RY (f x x').
Show proof.
Theorem isdeceqsetquot_non_constr {X : UU} (R : eqrel X)
(is : ∏ x x' : X, isdecprop (R x x')) : isdeceq (setquot R).
Show proof.
intros. apply isdeceqif. intros x x'.
apply (setquotuniv2prop
R (λ x0 x0', make_hProp _ (isapropisdecprop (x0 = x0')))).
intros x0 x0'. simpl.
apply (isdecpropweqf (weqpathsinsetquot R x0 x0') (is x0 x0')).
apply (setquotuniv2prop
R (λ x0 x0', make_hProp _ (isapropisdecprop (x0 = x0')))).
intros x0 x0'. simpl.
apply (isdecpropweqf (weqpathsinsetquot R x0 x0') (is x0 x0')).
Definition setquotbooleqint {X : UU} (R : eqrel X)
(is : ∏ x x' : X, isdecprop (R x x')) (x x' : X) : bool.
Show proof.
Lemma setquotbooleqintcomp {X : UU} (R : eqrel X)
(is : ∏ x x' : X, isdecprop (R x x')) :
iscomprelfun2 R (setquotbooleqint R is).
Show proof.
intros. unfold iscomprelfun2.
intros x x' x0 x0' r r0. unfold setquotbooleqint.
induction (pr1 (is x x0)) as [ r1 | nr1 ].
- induction (pr1 (is x' x0')) as [ r1' | nr1' ].
+ apply idpath.
+ induction (nr1' (eqreltrans
R _ _ _ (eqreltrans
R _ _ _ (eqrelsymm R _ _ r) r1) r0)).
- induction (pr1 (is x' x0')) as [ r1' | nr1' ].
+ induction (nr1 (eqreltrans
R _ _ _ r (eqreltrans
R _ _ _ r1' (eqrelsymm R _ _ r0)))).
+ apply idpath.
intros x x' x0 x0' r r0. unfold setquotbooleqint.
induction (pr1 (is x x0)) as [ r1 | nr1 ].
- induction (pr1 (is x' x0')) as [ r1' | nr1' ].
+ apply idpath.
+ induction (nr1' (eqreltrans
R _ _ _ (eqreltrans
R _ _ _ (eqrelsymm R _ _ r) r1) r0)).
- induction (pr1 (is x' x0')) as [ r1' | nr1' ].
+ induction (nr1 (eqreltrans
R _ _ _ r (eqreltrans
R _ _ _ r1' (eqrelsymm R _ _ r0)))).
+ apply idpath.
Definition setquotbooleq {X : UU} (R : eqrel X)
(is : ∏ x x' : X, isdecprop (R x x')) :
setquot R -> setquot R -> bool
:= setquotuniv2 R (make_hSet _ (isasetbool)) (setquotbooleqint R is)
(setquotbooleqintcomp R is).
Lemma setquotbooleqtopaths {X : UU} (R : eqrel X)
(is : ∏ x x' : X, isdecprop (R x x')) (x x' : setquot R) :
setquotbooleq R is x x' = true -> x = x'.
Show proof.
revert x x'.
assert (isp : ∏ (x x' : setquot R),
isaprop ((setquotbooleq R is x x') = true -> x = x')).
{
intros x x'. apply impred. intro. apply (isasetsetquot R x x').
}
apply (setquotuniv2prop R (λ x x', make_hProp _ (isp x x'))). simpl.
intros x x'.
change ((setquotbooleqint R is x x') = true
-> paths (setquotpr R x) (setquotpr R x')).
unfold setquotbooleqint. induction (pr1 (is x x')) as [ i1 | i2 ].
- intro. apply (weqpathsinsetquot R _ _ i1).
- intro H. induction (nopathsfalsetotrue H).
assert (isp : ∏ (x x' : setquot R),
isaprop ((setquotbooleq R is x x') = true -> x = x')).
{
intros x x'. apply impred. intro. apply (isasetsetquot R x x').
}
apply (setquotuniv2prop R (λ x x', make_hProp _ (isp x x'))). simpl.
intros x x'.
change ((setquotbooleqint R is x x') = true
-> paths (setquotpr R x) (setquotpr R x')).
unfold setquotbooleqint. induction (pr1 (is x x')) as [ i1 | i2 ].
- intro. apply (weqpathsinsetquot R _ _ i1).
- intro H. induction (nopathsfalsetotrue H).
Lemma setquotpathstobooleq {X : UU} (R : eqrel X)
(is : ∏ x x' : X, isdecprop (R x x')) (x x' : setquot R) :
x = x' -> setquotbooleq R is x x' = true.
Show proof.
intros e. induction e. generalize x.
apply (setquotunivprop
R (λ x, make_hProp _ (isasetbool (setquotbooleq R is x x) true))).
simpl. intro x0.
change ((setquotbooleqint R is x0 x0) = true).
unfold setquotbooleqint. induction (pr1 (is x0 x0)) as [ i1 | i2 ].
- apply idpath.
- induction (i2 (eqrelrefl R x0)).
apply (setquotunivprop
R (λ x, make_hProp _ (isasetbool (setquotbooleq R is x x) true))).
simpl. intro x0.
change ((setquotbooleqint R is x0 x0) = true).
unfold setquotbooleqint. induction (pr1 (is x0 x0)) as [ i1 | i2 ].
- apply idpath.
- induction (i2 (eqrelrefl R x0)).
Definition isdeceqsetquot {X : UU} (R : eqrel X)
(is : ∏ x x' : X, isdecprop (R x x')) : isdeceq (setquot R).
Show proof.
intros. intros x x'.
induction (boolchoice (setquotbooleq R is x x')) as [ i | ni ].
- apply (ii1 (setquotbooleqtopaths R is x x' i)).
- apply ii2. intro e.
induction (falsetonegtrue _ ni (setquotpathstobooleq R is x x' e)).
induction (boolchoice (setquotbooleq R is x x')) as [ i | ni ].
- apply (ii1 (setquotbooleqtopaths R is x x' i)).
- apply ii2. intro e.
induction (falsetonegtrue _ ni (setquotpathstobooleq R is x x' e)).
Relations on quotient sets
Definition iscomprelrel {X : UU} (R : hrel X) (L : hrel X) : UU
:= iscomprelfun2 R L.
Lemma iscomprelrelif {X : UU} {R : hrel X} (L : hrel X) (isr : issymm R)
(i1 : ∏ x x' y, R x x' -> L x y -> L x' y)
(i2 : ∏ x y y', R y y' -> L x y -> L x y') : iscomprelrel R L.
Show proof.
intros. intros x x' y y' rx ry.
set (rx' := isr _ _ rx). set (ry' := isr _ _ ry).
apply hPropUnivalence.
- intro lxy. set (int1 := i1 _ _ _ rx lxy). apply (i2 _ _ _ ry int1).
- intro lxy'. set (int1 := i1 _ _ _ rx' lxy'). apply (i2 _ _ _ ry' int1).
set (rx' := isr _ _ rx). set (ry' := isr _ _ ry).
apply hPropUnivalence.
- intro lxy. set (int1 := i1 _ _ _ rx lxy). apply (i2 _ _ _ ry int1).
- intro lxy'. set (int1 := i1 _ _ _ rx' lxy'). apply (i2 _ _ _ ry' int1).
Lemma iscomprelrellogeqf1 {X : UU} {R R' : hrel X} (L : hrel X)
(lg : hrellogeq R R') (is : iscomprelrel R L) : iscomprelrel R' L.
Show proof.
Lemma iscomprelrellogeqf2 {X : UU} (R : hrel X) {L L' : hrel X}
(lg : hrellogeq L L') (is : iscomprelrel R L) : iscomprelrel R L'.
Show proof.
intros. intros x x' x0 x0' r r0.
assert (e : paths (L x x0) (L' x x0)).
{
apply hPropUnivalence.
- apply (pr1 (lg _ _)).
- apply (pr2 (lg _ _)).
}
assert (e' : paths (L x' x0') (L' x' x0')).
{
apply hPropUnivalence.
- apply (pr1 (lg _ _)).
- apply (pr2 (lg _ _)).
}
induction e. induction e'.
apply (is _ _ _ _ r r0).
assert (e : paths (L x x0) (L' x x0)).
{
apply hPropUnivalence.
- apply (pr1 (lg _ _)).
- apply (pr2 (lg _ _)).
}
assert (e' : paths (L x' x0') (L' x' x0')).
{
apply hPropUnivalence.
- apply (pr1 (lg _ _)).
- apply (pr2 (lg _ _)).
}
induction e. induction e'.
apply (is _ _ _ _ r r0).
Definition quotrel {X : UU} {R L : hrel X} (is : iscomprelrel R L) :
hrel (setquot R) := setquotuniv2 R hPropset L is.
Lemma istransquotrel {X : UU} {R : eqrel X} {L : hrel X}
(is : iscomprelrel R L) (isl : istrans L) : istrans (quotrel is).
Show proof.
intros. unfold istrans.
assert (int : ∏ (x1 x2 x3 : setquot R),
isaprop (quotrel is x1 x2 -> quotrel is x2 x3
-> quotrel is x1 x3)).
{
intros x1 x2 x3.
apply impred. intro.
apply impred. intro.
apply (pr2 (quotrel is x1 x3)).
}
apply (setquotuniv3prop R (λ x1 x2 x3, make_hProp _ (int x1 x2 x3))).
intros x x' x''. intros r r'.
apply (isl x x' x'' r r').
assert (int : ∏ (x1 x2 x3 : setquot R),
isaprop (quotrel is x1 x2 -> quotrel is x2 x3
-> quotrel is x1 x3)).
{
intros x1 x2 x3.
apply impred. intro.
apply impred. intro.
apply (pr2 (quotrel is x1 x3)).
}
apply (setquotuniv3prop R (λ x1 x2 x3, make_hProp _ (int x1 x2 x3))).
intros x x' x''. intros r r'.
apply (isl x x' x'' r r').
Lemma issymmquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L)
(isl : issymm L) : issymm (quotrel is).
Show proof.
intros. unfold issymm.
assert (int : ∏ (x1 x2 : setquot R),
isaprop (quotrel is x1 x2 -> quotrel is x2 x1)).
{
intros x1 x2.
apply impred. intro.
apply (pr2 (quotrel is x2 x1)).
}
apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))).
intros x x'. intros r.
apply (isl x x' r).
assert (int : ∏ (x1 x2 : setquot R),
isaprop (quotrel is x1 x2 -> quotrel is x2 x1)).
{
intros x1 x2.
apply impred. intro.
apply (pr2 (quotrel is x2 x1)).
}
apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))).
intros x x'. intros r.
apply (isl x x' r).
Lemma isreflquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L)
(isl : isrefl L) : isrefl (quotrel is).
Show proof.
Lemma ispoquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L)
(isl : ispreorder L) : ispreorder (quotrel is).
Show proof.
Lemma iseqrelquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L)
(isl : iseqrel L) : iseqrel (quotrel is).
Show proof.
Lemma isirreflquotrel {X : UU} {R : eqrel X} {L : hrel X}
(is : iscomprelrel R L) (isl : isirrefl L) : isirrefl (quotrel is).
Show proof.
intros. unfold isirrefl.
apply (setquotunivprop R (λ x, make_hProp _ (isapropneg (quotrel is x x)))).
intro x. apply (isl x).
apply (setquotunivprop R (λ x, make_hProp _ (isapropneg (quotrel is x x)))).
intro x. apply (isl x).
Lemma isasymmquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L)
(isl : isasymm L) : isasymm (quotrel is).
Show proof.
intros. unfold isasymm.
assert (int : ∏ (x1 x2 : setquot R),
isaprop (quotrel is x1 x2 -> quotrel is x2 x1 -> empty)).
{
intros x1 x2.
apply impred. intro.
apply impred. intro.
apply isapropempty.
}
apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))).
intros x x'. intros r r'.
apply (isl x x' r r').
assert (int : ∏ (x1 x2 : setquot R),
isaprop (quotrel is x1 x2 -> quotrel is x2 x1 -> empty)).
{
intros x1 x2.
apply impred. intro.
apply impred. intro.
apply isapropempty.
}
apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))).
intros x x'. intros r r'.
apply (isl x x' r r').
Lemma iscoasymmquotrel {X : UU} {R : eqrel X} {L : hrel X}
(is : iscomprelrel R L) (isl : iscoasymm L) : iscoasymm (quotrel is).
Show proof.
intros. unfold iscoasymm.
assert (int : ∏ (x1 x2 : setquot R),
isaprop (neg (quotrel is x1 x2) -> quotrel is x2 x1)).
{
intros x1 x2.
apply impred. intro.
apply (pr2 _).
}
apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))).
intros x x'. intros r.
apply (isl x x' r).
assert (int : ∏ (x1 x2 : setquot R),
isaprop (neg (quotrel is x1 x2) -> quotrel is x2 x1)).
{
intros x1 x2.
apply impred. intro.
apply (pr2 _).
}
apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))).
intros x x'. intros r.
apply (isl x x' r).
Lemma istotalquotrel {X : UU} {R : eqrel X} {L : hrel X}
(is : iscomprelrel R L) (isl : istotal L) : istotal (quotrel is).
Show proof.
intros. unfold istotal.
apply (setquotuniv2prop R (λ x1 x2, hdisj _ _)).
intros x x'. intros r r'.
apply (isl x x' r r').
apply (setquotuniv2prop R (λ x1 x2, hdisj _ _)).
intros x x'. intros r r'.
apply (isl x x' r r').
Lemma iscotransquotrel {X : UU} {R : eqrel X} {L : hrel X}
(is : iscomprelrel R L) (isl : iscotrans L) : iscotrans (quotrel is).
Show proof.
intros. unfold iscotrans.
assert (int : ∏ (x1 x2 x3 : setquot R),
isaprop (quotrel is x1 x3 -> hdisj (quotrel is x1 x2)
(quotrel is x2 x3))).
{
intros.
apply impred. intro.
apply (pr2 _).
}
apply (setquotuniv3prop R (λ x1 x2 x3, make_hProp _ (int x1 x2 x3))).
intros x x' x''. intros r.
apply (isl x x' x'' r).
assert (int : ∏ (x1 x2 x3 : setquot R),
isaprop (quotrel is x1 x3 -> hdisj (quotrel is x1 x2)
(quotrel is x2 x3))).
{
intros.
apply impred. intro.
apply (pr2 _).
}
apply (setquotuniv3prop R (λ x1 x2 x3, make_hProp _ (int x1 x2 x3))).
intros x x' x''. intros r.
apply (isl x x' x'' r).
Lemma isantisymmquotrel {X : UU} {R : eqrel X} {L : hrel X}
(is : iscomprelrel R L) (isl : isantisymm L) : isantisymm (quotrel is).
Show proof.
intros. unfold isantisymm.
assert (int : ∏ (x1 x2 : setquot R),
isaprop (quotrel is x1 x2 -> quotrel is x2 x1 -> x1 = x2)).
{
intros x1 x2.
apply impred. intro.
apply impred. intro.
apply (isasetsetquot R x1 x2).
}
apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))).
intros x x'. intros r r'.
apply (maponpaths (setquotpr R) (isl x x' r r')).
assert (int : ∏ (x1 x2 : setquot R),
isaprop (quotrel is x1 x2 -> quotrel is x2 x1 -> x1 = x2)).
{
intros x1 x2.
apply impred. intro.
apply impred. intro.
apply (isasetsetquot R x1 x2).
}
apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))).
intros x x'. intros r r'.
apply (maponpaths (setquotpr R) (isl x x' r r')).
Lemma isantisymmnegquotrel {X : UU} {R : eqrel X} {L : hrel X}
(is : iscomprelrel R L) (isl : isantisymmneg L) :
isantisymmneg (quotrel is).
Show proof.
intros. unfold isantisymmneg.
assert (int : ∏ (x1 x2 : setquot R),
isaprop (neg (quotrel is x1 x2) -> neg (quotrel is x2 x1)
-> x1 = x2)).
{
intros x1 x2.
apply impred. intro.
apply impred. intro.
apply (isasetsetquot R x1 x2).
}
apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))).
intros x x'. intros r r'.
apply (maponpaths (setquotpr R) (isl x x' r r')).
assert (int : ∏ (x1 x2 : setquot R),
isaprop (neg (quotrel is x1 x2) -> neg (quotrel is x2 x1)
-> x1 = x2)).
{
intros x1 x2.
apply impred. intro.
apply impred. intro.
apply (isasetsetquot R x1 x2).
}
apply (setquotuniv2prop R (λ x1 x2, make_hProp _ (int x1 x2))).
intros x x'. intros r r'.
apply (maponpaths (setquotpr R) (isl x x' r r')).
We do not have a lemma for neqchoicequotrel since neqchoice is not a
property and since even when it is a property such as under the additional
condition isasymm on the relation it still carrier computational content
(similarly to isdec) which would be lost under our current approach of taking
quotients. How to best define neqchoicequotrel remains at the moment an open
question.
Lemma quotrelimpl {X : UU} {R : eqrel X} {L L' : hrel X} (is : iscomprelrel R L)
(is' : iscomprelrel R L') (impl : ∏ x x', L x x' -> L' x x')
(x x' : setquot R) (ql : quotrel is x x') : quotrel is' x x'.
Show proof.
intros. generalize x x' ql.
assert (int : ∏ (x0 x0' : setquot R),
isaprop (quotrel is x0 x0' -> quotrel is' x0 x0')).
{
intros x0 x0'.
apply impred. intro.
apply (pr2 _).
}
apply (setquotuniv2prop _ (λ x0 x0', make_hProp _ (int x0 x0'))).
intros x0 x0'. change (L x0 x0' -> L' x0 x0').
apply (impl x0 x0').
assert (int : ∏ (x0 x0' : setquot R),
isaprop (quotrel is x0 x0' -> quotrel is' x0 x0')).
{
intros x0 x0'.
apply impred. intro.
apply (pr2 _).
}
apply (setquotuniv2prop _ (λ x0 x0', make_hProp _ (int x0 x0'))).
intros x0 x0'. change (L x0 x0' -> L' x0 x0').
apply (impl x0 x0').
Lemma quotrellogeq {X : UU} {R : eqrel X} {L L' : hrel X}
(is : iscomprelrel R L) (is' : iscomprelrel R L')
(lg : ∏ x x', L x x' <-> L' x x') (x x' : setquot R) :
(quotrel is x x') <-> (quotrel is' x x').
Show proof.
intros. split.
- apply (quotrelimpl is is' (λ x0 x0', pr1 (lg x0 x0')) x x').
- apply (quotrelimpl is' is (λ x0 x0', pr2 (lg x0 x0')) x x').
- apply (quotrelimpl is is' (λ x0 x0', pr1 (lg x0 x0')) x x').
- apply (quotrelimpl is' is (λ x0 x0', pr2 (lg x0 x0')) x x').
Constructive proof of decidability of the quotient relation
Definition quotdecrelint {X : UU} {R : hrel X} (L : decrel X)
(is : iscomprelrel R (pr1 L)) : brel (setquot R).
Show proof.
intros.
set (f := decreltobrel L). unfold brel.
apply (setquotuniv2 R boolset f).
intros x x' x0 x0' r r0. unfold f. unfold decreltobrel in *.
induction (pr2 L x x0') as [ l | nl ].
- induction (pr2 L x' x0') as [ l' | nl' ].
+ induction (pr2 L x x0) as [ l'' | nl'' ].
* apply idpath.
* set (e := is x x' x0 x0' r r0).
induction e. induction (nl'' l').
+ induction (pr2 L x x0) as [ l'' | nl'' ].
* set (e := is x x' x0 x0' r r0). induction e. induction (nl' l'').
* apply idpath.
- induction (pr2 L x x0) as [ l' | nl' ].
+ induction (pr2 L x' x0') as [ l'' | nl'' ].
* apply idpath.
* set (e := is x x' x0 x0' r r0). induction e. induction (nl'' l').
+ induction (pr2 L x' x0') as [ l'' | nl'' ].
* set (e := is x x' x0 x0' r r0). induction e. induction (nl' l'').
* apply idpath.
set (f := decreltobrel L). unfold brel.
apply (setquotuniv2 R boolset f).
intros x x' x0 x0' r r0. unfold f. unfold decreltobrel in *.
induction (pr2 L x x0') as [ l | nl ].
- induction (pr2 L x' x0') as [ l' | nl' ].
+ induction (pr2 L x x0) as [ l'' | nl'' ].
* apply idpath.
* set (e := is x x' x0 x0' r r0).
induction e. induction (nl'' l').
+ induction (pr2 L x x0) as [ l'' | nl'' ].
* set (e := is x x' x0 x0' r r0). induction e. induction (nl' l'').
* apply idpath.
- induction (pr2 L x x0) as [ l' | nl' ].
+ induction (pr2 L x' x0') as [ l'' | nl'' ].
* apply idpath.
* set (e := is x x' x0 x0' r r0). induction e. induction (nl'' l').
+ induction (pr2 L x' x0') as [ l'' | nl'' ].
* set (e := is x x' x0 x0' r r0). induction e. induction (nl' l'').
* apply idpath.
Definition quotdecrelintlogeq {X : UU} {R : eqrel X} (L : decrel X)
(is : iscomprelrel R (pr1 L)) (x x' : setquot R) :
breltodecrel (quotdecrelint L is) x x' <-> quotrel is x x'.
Show proof.
revert x x'.
assert (int : ∏ (x x' : setquot R),
isaprop ((quotdecrelint L is x x') = true
<-> (quotrel is x x'))).
{
intros x x'. apply isapropdirprod.
- apply impred. intro. apply (pr2 (quotrel _ _ _)).
- apply impred. intro. apply isasetbool.
}
apply (setquotuniv2prop R (λ x x', make_hProp _ (int x x'))).
intros x x'. simpl. split.
- apply (pathstor L x x').
- apply (rtopaths L x x').
assert (int : ∏ (x x' : setquot R),
isaprop ((quotdecrelint L is x x') = true
<-> (quotrel is x x'))).
{
intros x x'. apply isapropdirprod.
- apply impred. intro. apply (pr2 (quotrel _ _ _)).
- apply impred. intro. apply isasetbool.
}
apply (setquotuniv2prop R (λ x x', make_hProp _ (int x x'))).
intros x x'. simpl. split.
- apply (pathstor L x x').
- apply (rtopaths L x x').
Lemma isdecquotrel {X : UU} {R : eqrel X} {L : hrel X}
(is : iscomprelrel R L) (isl : isdecrel L) : isdecrel (quotrel is).
Show proof.
intros.
apply (isdecrellogeqf
(quotdecrelintlogeq (make_decrel isl) is)
(pr2 (breltodecrel (quotdecrelint (make_decrel isl) is)))).
apply (isdecrellogeqf
(quotdecrelintlogeq (make_decrel isl) is)
(pr2 (breltodecrel (quotdecrelint (make_decrel isl) is)))).
Definition decquotrel {X : UU} {R : eqrel X} (L : decrel X)
(is : iscomprelrel R L) : decrel (setquot R)
:= make_decrel (isdecquotrel is (pr2 L)).
Definition reseqrel {X : UU} (R : eqrel X) (P : hsubtype X) : eqrel P :=
make_eqrel _ (iseqrelresrel R P (pr2 R)).
Lemma iseqclassresrel {X : UU} (R : hrel X) (P Q : hsubtype X)
(is : iseqclass R Q) (is' : ∏ x, Q x -> P x) :
iseqclass (resrel R P) (λ x : P, Q (pr1 x)).
Show proof.
intros. split.
- set (l1 := pr1 is). generalize l1. clear l1. simpl. apply hinhfun.
intro q. split with (make_carrier P (pr1 q) (is' (pr1 q) (pr2 q))).
apply (pr2 q).
- split.
+ intros p1 p2 r12 q1. apply ((pr1 (pr2 is)) _ _ r12 q1).
+ intros p1 p2 q1 q2. apply ((pr2 (pr2 is)) _ _ q1 q2).
- set (l1 := pr1 is). generalize l1. clear l1. simpl. apply hinhfun.
intro q. split with (make_carrier P (pr1 q) (is' (pr1 q) (pr2 q))).
apply (pr2 q).
- split.
+ intros p1 p2 r12 q1. apply ((pr1 (pr2 is)) _ _ r12 q1).
+ intros p1 p2 q1 q2. apply ((pr2 (pr2 is)) _ _ q1 q2).
Definition fromsubquot {X : UU} (R : eqrel X) (P : hsubtype (setquot R))
(p : P) : setquot (resrel R (funcomp (setquotpr R) P)).
Show proof.
intros.
split with (fun rp : carrier (funcomp (setquotpr R) P) => (pr1 p) (pr1 rp)).
apply (iseqclassresrel R (funcomp (setquotpr R) P) _ (pr2 (pr1 p))).
intros x px. set (e := setquotl0 R _ (make_carrier _ x px)).
simpl in e. unfold funcomp. rewrite e. apply (pr2 p).
split with (fun rp : carrier (funcomp (setquotpr R) P) => (pr1 p) (pr1 rp)).
apply (iseqclassresrel R (funcomp (setquotpr R) P) _ (pr2 (pr1 p))).
intros x px. set (e := setquotl0 R _ (make_carrier _ x px)).
simpl in e. unfold funcomp. rewrite e. apply (pr2 p).
Definition tosubquot {X : UU} (R : eqrel X) (P : hsubtype (setquot R)) :
setquot (resrel R (funcomp (setquotpr R) P)) -> P.
Show proof.
assert (int : isaset P).
{
apply (isasetsubset (@pr1 _ P)).
- apply (setproperty (setquotinset R)).
- refine (isinclpr1carrier _).
}
apply (setquotuniv _ (make_hSet _ int) (λ xp, make_carrier
P (setquotpr R (pr1 xp))
(pr2 xp))).
intros xp1 xp2 rp12.
apply (invmaponpathsincl _ (isinclpr1carrier P) _ _).
simpl. apply (iscompsetquotpr). apply rp12.
{
apply (isasetsubset (@pr1 _ P)).
- apply (setproperty (setquotinset R)).
- refine (isinclpr1carrier _).
}
apply (setquotuniv _ (make_hSet _ int) (λ xp, make_carrier
P (setquotpr R (pr1 xp))
(pr2 xp))).
intros xp1 xp2 rp12.
apply (invmaponpathsincl _ (isinclpr1carrier P) _ _).
simpl. apply (iscompsetquotpr). apply rp12.
Definition weqsubquot {X : UU} (R : eqrel X) (P : hsubtype (setquot R)) :
weq P (setquot (resrel R (funcomp (setquotpr R) P))).
Show proof.
intros.
set (f := fromsubquot R P). set (g := tosubquot R P). split with f.
assert (int0 : isaset P).
{
apply (isasetsubset (@pr1 _ P)).
- apply (setproperty (setquotinset R)).
- refine (isinclpr1carrier _).
}
assert (egf : ∏ (a : P), paths (g (f a)) a).
{
intros a. induction a as [ p isp ].
generalize isp. generalize p. clear isp. clear p.
assert (int : ∏ (p : setquot R),
isaprop (∏ isp : P p, paths (g (f (tpair _ p isp)))
(tpair _ p isp))).
{
intro p.
apply impred. intro.
apply (int0 _ _).
}
apply (setquotunivprop _ (λ a, make_hProp _ (int a))).
simpl. intros x isp. apply (invmaponpathsincl _ (isinclpr1carrier P) _ _).
apply idpath.
}
assert (efg : ∏ (a : setquot (resrel R (P ∘ setquotpr R))),
paths (f (g a)) a).
{
assert (int : ∏ a, isaprop (paths (f (g a)) a)).
{
intro a.
apply (setproperty (setquotinset (resrel R (funcomp (setquotpr R) P)))).
}
set (Q := reseqrel R (funcomp (setquotpr R) P)).
apply (setquotunivprop
Q (fun a : setquot (resrel R (funcomp (setquotpr R) P)) =>
make_hProp _ (int a))).
intro a. simpl. unfold f. unfold g. unfold fromsubquot. unfold tosubquot.
apply (invmaponpathsincl _ (isinclpr1 _ (λ a, isapropiseqclass _ a))).
apply idpath.
}
apply (isweq_iso _ _ egf efg).
set (f := fromsubquot R P). set (g := tosubquot R P). split with f.
assert (int0 : isaset P).
{
apply (isasetsubset (@pr1 _ P)).
- apply (setproperty (setquotinset R)).
- refine (isinclpr1carrier _).
}
assert (egf : ∏ (a : P), paths (g (f a)) a).
{
intros a. induction a as [ p isp ].
generalize isp. generalize p. clear isp. clear p.
assert (int : ∏ (p : setquot R),
isaprop (∏ isp : P p, paths (g (f (tpair _ p isp)))
(tpair _ p isp))).
{
intro p.
apply impred. intro.
apply (int0 _ _).
}
apply (setquotunivprop _ (λ a, make_hProp _ (int a))).
simpl. intros x isp. apply (invmaponpathsincl _ (isinclpr1carrier P) _ _).
apply idpath.
}
assert (efg : ∏ (a : setquot (resrel R (P ∘ setquotpr R))),
paths (f (g a)) a).
{
assert (int : ∏ a, isaprop (paths (f (g a)) a)).
{
intro a.
apply (setproperty (setquotinset (resrel R (funcomp (setquotpr R) P)))).
}
set (Q := reseqrel R (funcomp (setquotpr R) P)).
apply (setquotunivprop
Q (fun a : setquot (resrel R (funcomp (setquotpr R) P)) =>
make_hProp _ (int a))).
intro a. simpl. unfold f. unfold g. unfold fromsubquot. unfold tosubquot.
apply (invmaponpathsincl _ (isinclpr1 _ (λ a, isapropiseqclass _ a))).
apply idpath.
}
apply (isweq_iso _ _ egf efg).
Comment: unfortunetely weqsubquot is not as useful as it should be at
moment due to the failure of the following code to work:
Lemma test (X : UU) (R : eqrel X) (P : hsubtype (setquot R)) (x : X)
(is : P (setquotpr R x)) :
paths (setquotpr (reseqrel R (funcomp (setquotpr R) P)) (tpair _ x is))
(fromsubquot R P (tpair _ (setquotpr R x) is)).
Show proof.
As one of the consequences we are forced to use a "hack" in the definition of
multiplicative inverses for rationals in hqmultinv.
The issue which arises here is the same one which arises in several other
places in the work with quotients. It can be traced back first to the failure
of invmaponpathsincl to map idpath to idpath and then to the fact that
for (X : UU) (is : isaprop X) the term
t := proofirrelevance is : ∏ x1 x2 : X, x1 = x2 does not satisfy
(definitionally) the condition t x x == idpath x.
It can and probably should be fixed by the addition of a new componenet to
CIC in the form of a term constructor:
tfc (X : UU) (E : X -> UU) (is : ∏ x, iscontr (E x)) (x0 : X) (e0 : E x0) :
∏ x : X, E x.
and a computation rule
tfc_comp (tfc X E is x0 e0 x0) == e0
(with both tfc and tfc_comp definable in an arbitrary context)
Such an extension will be compatible with the univalent models and should not,
as far as I can see, provide any problems for normalization or for the
decidability of typing. Using tfc one can give a construction of
proofirrelevance as follows (recall that
isaprop := ∏ x1 x2, iscontr (x1 = x2)) :
Lemma proofirrelevance {X : UU} (is : isaprop X) : ∏ x1 x2, x1 = x2.
Proof.
intros X is x1.
apply (tfc X (λ x2, x1 = x2) is x1 (idpath x1)).
Defined.
Defined in this way proofirrelevance will have the required property and
will enable to define invmaponpathsincl in such a way that the existing
proofs of setquotl0 and fromsubquot and weqsubquot will provide the
desired behavior of fromsubquot on terms of the form
(tpair _ (setquotpr R x) is).
The set of connected components of type.
Definition pathshrel (X : UU) : X → X → hProp := λ x x' : X, ishinh (x = x').
Definition istranspathshrel (X : UU) : istrans (pathshrel X)
:= λ x x' x'' : _,
λ a : _,
λ b : _,
hinhfun2 (fun e1 : x = x' => fun e2 : x' = x'' => e1 @ e2) a b.
Definition isreflpathshrel (X : UU) : isrefl (pathshrel X)
:= λ x : _, hinhpr (idpath x).
Definition issymmpathshrel (X : UU) : issymm (pathshrel X)
:= λ x x': _, λ a : _, hinhfun (fun e : x = x' => ! e) a.
Definition pathseqrel (X : UU) : eqrel X
:= eqrelconstr (pathshrel X) (istranspathshrel X) (isreflpathshrel X)
(issymmpathshrel X).
Definition pi0 (X : UU) : UU := setquot (pathshrel X).
Definition pi0pr (X : UU) : X -> setquot (pathseqrel X)
:= setquotpr (pathseqrel X).
Set quotients. Construction 2.
Functions compatible with a relation
Definition compfun {X : UU} (R : hrel X) (S : UU) : UU
:= total2 (fun F : X -> S => iscomprelfun R F).
Definition make_compfun {X : UU} (R : hrel X) {S : UU} (f : X -> S)
(is : iscomprelfun R f) : compfun R S := tpair _ f is.
Definition pr1compfun (X : UU) (R : hrel X) (S : UU) :
@compfun X R S -> (X -> S) := @pr1 _ _.
Coercion pr1compfun : compfun >-> Funclass.
Definition compevmapset {X : UU} (R : hrel X) :
X -> ∏ S : hSet, (compfun R S) -> S
:= λ x : X, λ S : _, λ f : compfun R S, pr1 f x.
Definition compfuncomp {X : UU} (R : hrel X) {S S' : UU} (f : compfun R S)
(g : S -> S') : compfun R S'.
Show proof.
Tests
Definition F (X Y : UU) (R : hrel X) := (compfun R Y) -> Y.
Definition Fi (X Y : UU) (R : hrel X) : X -> F X Y R := λ x, λ f, f x.
Lemma iscompFi {X Y : UU} (R : hrel X) : iscomprelfun R (Fi X Y R).
Proof.
intros. intros x x' r. unfold Fi. apply funextfun.
intro f. apply (pr2 f x x' r).
Defined.
Definition Fv {X Y : UU} (R : hrel X) (f : compfun R Y) (phi : F X Y R) : Y
:= phi f.
Definition qeq {X Y : UU} (R : hrel X)
:= total2 (λ phi : F X Y R,
∏ psi : F X Y R -> Y,
paths (psi phi)
(Fv R (compfuncomp
R (make_compfun R _ (iscompFi R)) psi)
phi)).
Lemma isinclpr1qeq {X : UU} (R : hrel X) (Y : hSet) :
isincl (@pr1 _ (λ phi : F X Y R,
∏ psi : F X Y R -> Y,
paths
(psi phi)
(Fv R (compfuncomp
R (make_compfun R _ (iscompFi R))
psi) phi))).
Proof.
intros. apply isinclpr1.
intro phi.
apply impred. intro psi.
apply (pr2 Y).
Defined.
Definition toqeq {X Y : UU} (R : hrel X) (x : X) : @qeq X Y R.
Proof.
intros. split with (Fi X Y R x). intro psi. apply idpath.
Defined.
Lemma iscomptoqeq {X : UU} (Y : hSet) (R : hrel X) :
iscomprelfun R (@toqeq X Y R).
Proof.
intros. intros x x' r. unfold toqeq.
apply (invmaponpathsincl _ (isinclpr1qeq R Y)).
apply (@iscompFi X Y R x x' r).
Defined.
Definition qequniv {X : UU} (Y : hSet) (R : hrel X) (f : compfun R Y)
(phi : @qeq X Y R) : Y.
Proof.
intros. apply (Fv R f (pr1 phi)).
Defined.
Lemma qequnivandpr {X : UU} (Y : hSet) (R : hrel X) (f : compfun R Y)
(x : X) : paths (qequniv Y R f (toqeq R x)) (f x).
Proof.
intros. apply idpath.
Defined.
Lemma etaqeq {X : UU} (Y : hSet) (R : hrel X) (psi : qeq R -> Y)
(phi : qeq R) : paths (psi phi)
(qequniv Y R (compfuncomp
R (make_compfun
R _ (iscomptoqeq Y R))
psi) phi).
Proof.
intros. apply (pr2 phi psi).
Definition Fd1 {X Y : UU} : F X Y R -> (F (F X Y) Y) := Fi (F X Y) Y.
Definition Fd2 {X Y : UU} (R : hrel X) (phi : F X Y R) (psi : F X Y R -> Y) :
Y := (Fv R (funcomp (Fi X Y R) psi) phi).
Definition Ffunct {X1 X2 : UU} (f : X1 -> X2) (Y : UU) : F X1 Y -> F X2 Y
:= λ phi, λ g, phi (funcomp f g).
Lemma testd1 {X Y : UU} (psi : F X Y -> Y) (phi : F X Y) :
paths (psi phi) (Fd1 phi psi).
Proof.
intros. apply idpath.
Defined.
Lemma testd2 {X Y : UU} (psi : F X Y -> Y) (phi : F X Y) :
paths (Fv (funcomp (Fi X Y) psi) phi) (Fd2 phi psi).
Proof.
intros. apply idpath.
Defined.
Definition F (X Y : UU) := (X -> Y) -> Y.
Definition Ffunct {X1 X2 : UU} (f : X1 -> X2) (Y : UU) : F X1 Y -> F X2 Y
:= λ phi, λ g, phi (funcomp f g).
Definition Fi (X Y : UU) : X -> F X Y := λ x, λ f, f x.
Definition Fd1 {X Y : UU} : F X Y -> (F (F X Y) Y) := Fi (F X Y) Y.
Definition Fd2 {X Y : UU} : F X Y -> (F (F X Y) Y) := Ffunct (Fi X Y) Y.
Definition Fv {X Y : UU} (f : X -> Y) (phi : F X Y) : Y := phi f.
Lemma testd1 {X Y : UU} (psi : F X Y -> Y) (phi : F X Y) :
paths (psi phi) (Fd1 phi psi).
Proof.
intros. apply idpath.
Defined.
Lemma testd2 {X Y : UU} (psi : F X Y -> Y) (phi : F X Y) :
paths (Fv (funcomp (Fi X Y) psi) phi) (Fd2 phi psi).
Proof.
intros. apply idpath.
Defined.
Lemma Xineq (X Y : UU) (x : X) : paths (Fd1 (Fi X Y x)) (Fd2 (Fi X Y x)).
Proof.
intros. apply idpath.
Defined.
Lemma test (X Y : UU) (phi : F X Y) (f : X -> Y) :
paths (Fd1 phi (Fi (X -> Y) Y f)) (Fd2 phi (Fi (X -> Y) Y f)).
Proof.
intros. unfold Fd1. unfold Fd2. unfold Fi. unfold Ffunct. unfold funcomp.
simpl. apply (maponpaths phi). apply etacorrection.
Defined.
Inductive try0 (T : UU) (t : T) :
∏ (t1 t2 : T) (e1 : t = t1) (e2 : t = t2), UU
:= idconstr : ∏ (t' : T) (e' : t = t'), try0 T t t' t' e' e'.
Definition try0map1 (T : UU) (t : T) (t1 t2 : T) (e1 : t = t1)
(e2 : t = t2) (X : try0 T t t1 t2 e1 e2) : t1 = t2.
Proof.
intros. induction X. apply idpath.
Defined.
Definition try0map2 (T : UU) (t : T) (t1 t2 : T) (e1 : t = t1)
(e2 : t = t2) : try0 T t t1 t2 e1 e2.
Proof.
Lemma test (X : UU) (t : X) :
paths (pr2 (iscontrcoconustot X t) (pr1 (iscontrcoconustot X t)))
(idpath _).
Proof.
intros. apply idpath.
Lemma test {X : UU} (is : iscontr X) :
paths (pr2 (iscontrcor is) (pr1 (iscontrcor is))) (idpath _).
Proof.
intros. apply idpath.
Lemma test {X : UU} (R : eqrel X) (Y : hSet) (f : setquot R -> Y) :
paths f (setquotuniv R Y (funcomp (setquotpr R) f)
(λ x x' : X, λ r : R x x',
maponpaths f (iscompsetquotpr R x x' r))).
Proof.
intros. apply funextfun. intro c. simpl. induction c as A iseq . simpl.
The quotient set of a type by a relation.
Definition setquot2 {X : UU} (R : hrel X) : UU := image (compevmapset R).
Theorem isasetsetquot2 {X : UU} (R : hrel X) : isaset (setquot2 R).
Show proof.
intros.
assert (is1: isofhlevel 2 (∏ S : hSet, (compfun R S) -> S)).
{
apply impred. intro.
apply impred. intro X0.
apply (pr2 t).
}
apply (isasetsubset _ is1 (isinclpr1image _)).
assert (is1: isofhlevel 2 (∏ S : hSet, (compfun R S) -> S)).
{
apply impred. intro.
apply impred. intro X0.
apply (pr2 t).
}
apply (isasetsubset _ is1 (isinclpr1image _)).
Definition setquot2inset {X : UU} (R : hrel X) : hSet
:= make_hSet _ (isasetsetquot2 R).
We will be asuming below that setquot2 is in UU. In the future it should
be proved using issurjsetquot2pr below and a resizing axiom. The
appropriate resizing axiom for this should say that if X -> Y is a surjection,
Y is an hset and X : UU then Y : UU.
Definition setquot2pr {X : UU} (R : hrel X) : X -> setquot2 R
:= λ x : X, make_image (compevmapset R) _
(hinhpr (make_hfiber (compevmapset R) x (idpath _))).
Lemma issurjsetquot2pr {X : UU} (R : hrel X) : issurjective (setquot2pr R).
Show proof.
Lemma iscompsetquot2pr {X : UU} (R : hrel X) : iscomprelfun R (setquot2pr R).
Show proof.
intros. intros x x' r.
assert (e1: paths (compevmapset R x) (compevmapset R x')).
{
apply funextsec. intro S.
apply funextsec. intro f.
unfold compfun in f.
apply (pr2 f x x' r).
}
apply (invmaponpathsincl _ (isinclpr1image (compevmapset R))
(setquot2pr R x) (setquot2pr R x') e1).
assert (e1: paths (compevmapset R x) (compevmapset R x')).
{
apply funextsec. intro S.
apply funextsec. intro f.
unfold compfun in f.
apply (pr2 f x x' r).
}
apply (invmaponpathsincl _ (isinclpr1image (compevmapset R))
(setquot2pr R x) (setquot2pr R x') e1).
Universal property of seqtquot2 R for functions to sets satisfying compatibility condition iscomprelfun
Definition setquot2univ {X : UU} (R : hrel X) (Y : hSet) (F : X -> Y)
(is : iscomprelfun R F) (c : setquot2 R) : Y
:= pr1 c Y (make_compfun _ F is).
Theorem setquot2univcomm {X : UU} (R : hrel X) (Y : hSet) (F : X -> Y)
(iscomp : iscomprelfun R F) (x : X) :
setquot2univ _ _ F iscomp (setquot2pr R x) = F x.
Show proof.
Weak equivalence from R x x' to paths (setquot2pr R x) (setquot2pr R x')
Lemma weqpathssetquot2l1 {X : UU} (R : eqrel X) (x : X) :
iscomprelfun R (λ x', R x x').
Show proof.
intros. intros x' x''. intro r.
apply hPropUnivalence.
intro r'.
apply (eqreltrans R _ _ _ r' r).
intro r''.
apply (eqreltrans R _ _ _ r'' (eqrelsymm R _ _ r)).
apply hPropUnivalence.
intro r'.
apply (eqreltrans R _ _ _ r' r).
intro r''.
apply (eqreltrans R _ _ _ r'' (eqrelsymm R _ _ r)).
Theorem weqpathsinsetquot2 {X : UU} (R : eqrel X) (x x' : X) :
(R x x') ≃ (setquot2pr R x = setquot2pr R x').
Show proof.
intros. apply weqimplimpl. apply iscompsetquot2pr.
set (int := setquot2univ R hPropset (λ x'', R x x'')
(weqpathssetquot2l1 R x)).
intro e. change (pr1 (int (setquot2pr R x'))). induction e.
change (R x x). apply (eqrelrefl R). apply (pr2 (R x x')).
apply (isasetsetquot2).
set (int := setquot2univ R hPropset (λ x'', R x x'')
(weqpathssetquot2l1 R x)).
intro e. change (pr1 (int (setquot2pr R x'))). induction e.
change (R x x). apply (eqrelrefl R). apply (pr2 (R x x')).
apply (isasetsetquot2).
Definition setquottosetquot2 (X : UU) (R : hrel X) (is : iseqrel R) :
setquot R -> setquot2 R.
Show proof.
intros X0.
apply (setquotuniv R (make_hSet _ (isasetsetquot2 R)) (setquot2pr R)
(iscompsetquot2pr R) X0).
apply (setquotuniv R (make_hSet _ (isasetsetquot2 R)) (setquot2pr R)
(iscompsetquot2pr R) X0).
Require Import UniMath.Foundations.UnivalenceAxiom.
Definition hSet_univalence_map (X Y : hSet) : (X = Y) -> (pr1 X ≃ pr1 Y).
Show proof.
Theorem hSet_univalence (X Y : hSet) : (X = Y) ≃ (X ≃ Y).
Show proof.
Set Printing Coercions.
intros.
set (f := hSet_univalence_map X Y).
exists f.
set (g := @eqweqmap (pr1 X) (pr1 Y)).
set (h := λ e : X = Y, maponpaths pr1hSet e).
assert (comp : f = g ∘ h).
{
apply funextfun; intro e. induction e. apply idpath.
}
induction (!comp). apply twooutof3c.
- apply isweqonpathsincl. apply isinclpr1. exact isapropisaset.
- apply univalenceAxiom.
Unset Printing Coercions.
intros.
set (f := hSet_univalence_map X Y).
exists f.
set (g := @eqweqmap (pr1 X) (pr1 Y)).
set (h := λ e : X = Y, maponpaths pr1hSet e).
assert (comp : f = g ∘ h).
{
apply funextfun; intro e. induction e. apply idpath.
}
induction (!comp). apply twooutof3c.
- apply isweqonpathsincl. apply isinclpr1. exact isapropisaset.
- apply univalenceAxiom.
Unset Printing Coercions.
Theorem hSet_rect (X Y : hSet) (P : X ≃ Y -> UU) :
(∏ e : X=Y, P (hSet_univalence _ _ e)) -> ∏ f, P f.
Show proof.
intros ih ?.
Set Printing Coercions.
set (p := ih (invmap (hSet_univalence _ _) f)).
set (h := homotweqinvweq (hSet_univalence _ _) f).
exact (transportf P h p).
Unset Printing Coercions.
Set Printing Coercions.
set (p := ih (invmap (hSet_univalence _ _) f)).
set (h := homotweqinvweq (hSet_univalence _ _) f).
exact (transportf P h p).
Unset Printing Coercions.
Ltac hSet_induction f e := generalize f; apply UU_rect; intro e; clear f.