Library UniMath.MoreFoundations.Sets
Contents
- (More entries need to be added here...)
- Other universal properties for setquot
- The equivalence relation of being in the same fiber
- Subsets
- Binary relations
Local Open Scope logic.
Definition hProp_set : hSet := make_hSet _ isasethProp.
Definition isconst {X:UU} {Y:hSet} (f : X -> Y) : hProp := ∀ x x', f x = f x'.
Definition squash_to_hSet {X : UU} {Y : hSet} (f : X -> Y) : isconst f -> ∥ X ∥ -> Y.
Show proof.
Definition isconst_2 {X Y:UU} {Z:hSet} (f : X -> Y -> Z) : hProp :=
∀ x x' y y', f x y = f x' y'.
Definition squash_to_hSet_2 {X Y : UU} {Z : hSet} (f : X -> Y -> Z) :
isconst_2 f -> ∥ X ∥ -> ∥ Y ∥ -> Z.
Show proof.
intros c. use squash_to_set.
{ apply isaset_forall_hSet. }
{ intros x. use squash_to_hSet. exact (f x). intros y y'. exact (c x x y y'). }
{ intros x x'. apply funextfun; intros yn.
apply (squash_to_prop yn).
{ apply setproperty. }
intros y. assert (e : hinhpr y = yn).
{ apply propproperty. }
induction e. change ( f x y = f x' y ). exact (c x x' y y). }
{ apply isaset_forall_hSet. }
{ intros x. use squash_to_hSet. exact (f x). intros y y'. exact (c x x y y'). }
{ intros x x'. apply funextfun; intros yn.
apply (squash_to_prop yn).
{ apply setproperty. }
intros y. assert (e : hinhpr y = yn).
{ apply propproperty. }
induction e. change ( f x y = f x' y ). exact (c x x' y y). }
Definition isconst_2' {X Y:UU} {Z:hSet} (f : X -> Y -> Z) : hProp :=
(∀ x x' y, f x y = f x' y)
∧
(∀ x y y', f x y = f x y').
Definition squash_to_hSet_2' {X Y : UU} {Z : hSet} (f : X -> Y -> Z) :
isconst_2' f -> ∥ X ∥ -> ∥ Y ∥ -> Z.
Show proof.
intros [c d]. use squash_to_set.
{ apply isaset_forall_hSet. }
{ intros x. use squash_to_hSet. exact (f x). intros y y'. exact (d x y y'). }
{ intros x x'. apply funextfun; intros yn.
apply (squash_to_prop yn).
{ apply setproperty. }
intros y. assert (e : hinhpr y = yn).
{ apply propproperty. }
induction e. change ( f x y = f x' y ). exact (c x x' y). }
{ apply isaset_forall_hSet. }
{ intros x. use squash_to_hSet. exact (f x). intros y y'. exact (d x y y'). }
{ intros x x'. apply funextfun; intros yn.
apply (squash_to_prop yn).
{ apply setproperty. }
intros y. assert (e : hinhpr y = yn).
{ apply propproperty. }
induction e. change ( f x y = f x' y ). exact (c x x' y). }
Definition eqset_to_path {X:hSet} (x y:X) : eqset x y -> paths x y := λ e, e.
Lemma isapropiscomprelfun {X : UU} {Y : hSet} (R : hrel X) (f : X -> Y) : isaprop (iscomprelfun R f).
Show proof.
Lemma iscomprelfun_funcomp {X Y Z : UU} {R : hrel X} {S : hrel Y}
{f : X → Y} {g : Y → Z} (Hf : iscomprelrelfun R S f) (Hg : iscomprelfun S g) :
iscomprelfun R (g ∘ f).
Show proof.
intros x x' r. exact (Hg _ _ (Hf x x' r)).
Definition fun_hrel_comp {X Y : UU} (f : X → Y) (gt : hrel Y) : hrel X :=
λ x y : X, gt (f x) (f y).
Other universal properties for setquot
Theorem setquotunivprop' {X : UU} {R : eqrel X} (P : setquot (pr1 R) -> UU)
(H : ∏ x, isaprop (P x)) (ps : ∏ x : X, P (setquotpr R x)) : ∏ c : setquot (pr1 R), P c.
Show proof.
Theorem setquotuniv2prop' {X : UU} {R : eqrel X} (P : setquot (pr1 R) → setquot (pr1 R) → UU)
(H : ∏ x1 x2, isaprop (P x1 x2))
(ps : ∏ x1 x2, P (setquotpr R x1) (setquotpr R x2)) : ∏ c1 c2 : setquot (pr1 R), P c1 c2.
Show proof.
Theorem setquotuniv3prop' {X : UU} {R : eqrel X}
(P : setquot (pr1 R) → setquot (pr1 R) → setquot (pr1 R) → UU)
(H : ∏ x1 x2 x3, isaprop (P x1 x2 x3))
(ps : ∏ x1 x2 x3, P (setquotpr R x1) (setquotpr R x2) (setquotpr R x3)) :
∏ c1 c2 c3 : setquot (pr1 R), P c1 c2 c3.
Show proof.
Theorem setquotuniv4prop' {X : UU} {R : eqrel X}
(P : setquot (pr1 R) → setquot (pr1 R) → setquot (pr1 R) → setquot (pr1 R) → UU)
(H : ∏ x1 x2 x3 x4, isaprop (P x1 x2 x3 x4))
(ps : ∏ x1 x2 x3 x4,
P (setquotpr R x1) (setquotpr R x2) (setquotpr R x3) (setquotpr R x4)) :
∏ c1 c2 c3 c4 : setquot (pr1 R), P c1 c2 c3 c4.
Show proof.
Definition same_fiber_eqrel {X Y : hSet} (f : X → Y) : eqrel X.
Show proof.
use make_eqrel.
- intros x y.
exact ((f x) = (f y)).
- use iseqrelconstr.
+ intros ? ? ? xy yz; exact (xy @ yz).
+ intro; reflexivity.
+ intros ? ? eq; exact (!eq).
- intros x y.
exact ((f x) = (f y)).
- use iseqrelconstr.
+ intros ? ? ? xy yz; exact (xy @ yz).
+ intro; reflexivity.
+ intros ? ? eq; exact (!eq).
Definition pi0 (X : UU) : hSet := setquotinset (pathseqrel X).
Section Pi0.
Definition π₀ : Type -> hSet := pi0.
Definition component {X:Type} : X -> π₀ X := setquotpr (pathseqrel X).
Definition π₀_map {X Y:Type} : (X -> Y) -> (π₀ X -> π₀ Y)
:= λ f, setquotfun (pathseqrel X) (pathseqrel Y) f (λ x x', hinhfun (maponpaths f)).
Definition π₀_universal_property {X:Type} {Y:hSet} : (π₀ X -> Y) ≃ (X -> Y).
Show proof.
exists (λ h, h ∘ component). intros f. apply iscontraprop1.
- apply isaproptotal2.
+ intros h. use (_ : isaset _). apply impred_isaset. intros x. apply setproperty.
+ intros h h' e e'. apply funextsec. intro w.
{ apply (surjectionisepitosets component).
- apply issurjsetquotpr.
- apply setproperty.
- intros x. exact (maponpaths (λ k, k x) (e @ ! e')). }
- now exists (setquotuniv _ _ f (λ x y e, squash_to_prop e (setproperty Y (f x) (f y)) (maponpaths f))).
Definition π₀_universal_map {X:Type} {Y:hSet} : (X -> Y) -> (π₀ X -> Y) := invmap π₀_universal_property.- apply isaproptotal2.
+ intros h. use (_ : isaset _). apply impred_isaset. intros x. apply setproperty.
+ intros h h' e e'. apply funextsec. intro w.
{ apply (surjectionisepitosets component).
- apply issurjsetquotpr.
- apply setproperty.
- intros x. exact (maponpaths (λ k, k x) (e @ ! e')). }
- now exists (setquotuniv _ _ f (λ x y e, squash_to_prop e (setproperty Y (f x) (f y)) (maponpaths f))).
Lemma π₀_universal_map_eqn {X:Type} {Y:hSet} (f : X -> Y) :
∏ (x:X), π₀_universal_map f (component x) = f x.
Show proof.
reflexivity.
Lemma π₀_universal_map_uniq {X:Type} {Y:hSet} (h h' : π₀ X -> Y) :(∏ x, h (component x) = h' (component x)) -> h ~ h'.
Show proof.
intros e x. apply (surjectionisepitosets component).
- apply issurjsetquotpr.
- apply setproperty.
- exact e.
End Pi0.- apply issurjsetquotpr.
- apply setproperty.
- exact e.
Section mineqrel.
Close Scope set.
Context {A : UU} (R0 : hrel A).
Lemma isaprop_eqrel_from_hrel a b :
isaprop (∏ R : eqrel A, (∏ x y, R0 x y -> R x y) -> R a b).
Show proof.
Definition eqrel_from_hrel : hrel A :=
λ a b, make_hProp _ (isaprop_eqrel_from_hrel a b).
Lemma iseqrel_eqrel_from_hrel : iseqrel eqrel_from_hrel.
Show proof.
Lemma eqrel_impl a b : R0 a b -> eqrel_from_hrel a b.
Show proof.
Lemma minimal_eqrel_from_hrel (R : eqrel A) (H : ∏ a b, R0 a b -> R a b) :
∏ a b, eqrel_from_hrel a b -> R a b.
Show proof.
End mineqrel.
Lemma eqreleq {A : UU} (R : eqrel A) (x y : A) : x = y → R x y.
Show proof.
Close Scope set.
Context {A : UU} (R0 : hrel A).
Lemma isaprop_eqrel_from_hrel a b :
isaprop (∏ R : eqrel A, (∏ x y, R0 x y -> R x y) -> R a b).
Show proof.
Definition eqrel_from_hrel : hrel A :=
λ a b, make_hProp _ (isaprop_eqrel_from_hrel a b).
Lemma iseqrel_eqrel_from_hrel : iseqrel eqrel_from_hrel.
Show proof.
repeat split.
- intros x y z H1 H2 R HR. exact (eqreltrans _ _ _ _ (H1 _ HR) (H2 _ HR)).
- now intros x R _; apply (eqrelrefl R).
- intros x y H R H'. exact (eqrelsymm _ _ _ (H _ H')).
- intros x y z H1 H2 R HR. exact (eqreltrans _ _ _ _ (H1 _ HR) (H2 _ HR)).
- now intros x R _; apply (eqrelrefl R).
- intros x y H R H'. exact (eqrelsymm _ _ _ (H _ H')).
Lemma eqrel_impl a b : R0 a b -> eqrel_from_hrel a b.
Show proof.
now intros H R HR; apply HR.
Lemma minimal_eqrel_from_hrel (R : eqrel A) (H : ∏ a b, R0 a b -> R a b) :
∏ a b, eqrel_from_hrel a b -> R a b.
Show proof.
now intros a b H'; apply (H' _ H).
End mineqrel.
Lemma eqreleq {A : UU} (R : eqrel A) (x y : A) : x = y → R x y.
Show proof.
Lemma isaprop_isirrefl {X : UU} (rel : hrel X) :
isaprop (isirrefl rel).
Show proof.
Lemma isaprop_issymm {X : UU} (rel : hrel X) :
isaprop (issymm rel).
Show proof.
Lemma isaprop_iscotrans {X : UU} (rel : hrel X) :
isaprop (iscotrans rel).
Show proof.
apply impred_isaprop ; intro x.
apply impred_isaprop ; intro y.
apply impred_isaprop ; intro z.
apply isapropimpl.
now apply pr2.
apply impred_isaprop ; intro y.
apply impred_isaprop ; intro z.
apply isapropimpl.
now apply pr2.
Useful functions for when using univalence of sets
Definition univalence_hSet
{X Y : hSet}
(w : X ≃ Y)
: X = Y
:= invmap (hSet_univalence _ _) w.
Definition hSet_univalence_map_univalence_hSet
{X Y : hSet}
(w : X ≃ Y)
: hSet_univalence_map X Y (univalence_hSet w) = w.
Show proof.
Definition hSet_univalence_univalence_hSet_map
{X Y : hSet}
(p : X = Y)
: univalence_hSet (hSet_univalence_map X Y p) = p.
Show proof.
Definition univalence_hSet_idweq
(X : hSet)
: univalence_hSet (idweq X) = idpath X.
Show proof.
Definition hSet_univalence_map_inv
{X Y : hSet}
(p : X = Y)
: hSet_univalence_map _ _ (!p) = invweq (hSet_univalence_map _ _ p).
Show proof.
Definition univalence_hSet_inv
{X Y : hSet}
(w : X ≃ Y)
: !(univalence_hSet w) = univalence_hSet (invweq w).
Show proof.
{X Y : hSet}
(w : X ≃ Y)
: X = Y
:= invmap (hSet_univalence _ _) w.
Definition hSet_univalence_map_univalence_hSet
{X Y : hSet}
(w : X ≃ Y)
: hSet_univalence_map X Y (univalence_hSet w) = w.
Show proof.
Definition hSet_univalence_univalence_hSet_map
{X Y : hSet}
(p : X = Y)
: univalence_hSet (hSet_univalence_map X Y p) = p.
Show proof.
Definition univalence_hSet_idweq
(X : hSet)
: univalence_hSet (idweq X) = idpath X.
Show proof.
Definition hSet_univalence_map_inv
{X Y : hSet}
(p : X = Y)
: hSet_univalence_map _ _ (!p) = invweq (hSet_univalence_map _ _ p).
Show proof.
Definition univalence_hSet_inv
{X Y : hSet}
(w : X ≃ Y)
: !(univalence_hSet w) = univalence_hSet (invweq w).
Show proof.
refine (!(hSet_univalence_univalence_hSet_map _) @ _).
apply maponpaths.
rewrite hSet_univalence_map_inv.
rewrite hSet_univalence_map_univalence_hSet.
apply idpath.
apply maponpaths.
rewrite hSet_univalence_map_inv.
rewrite hSet_univalence_map_univalence_hSet.
apply idpath.