Library UniMath.Foundations.PartB
Univalent Foundations. Vladimir Voevodsky. Feb. 2010 - Sep. 2011.
Port to coq trunk (8.4-8.5) in March 2014. The second part of the original uu0 file, created on Dec. 3, 2014.Contents
- Basics about h-levels
- h-levels of types
- h-levels of functions
- h-levelf of pr1
- h-level of the total space of total2
- Basics on propositions, inclusions and sets
- Propositions, types of h-level 1
- Inclusions, functions of h-level 1
- Sets, types of h-level 2
Preamble
Fixpoint isofhlevel (n : nat) (X : UU) : UU
:= match n with
| O => iscontr X
| S m => ∏ x : X, ∏ x' : X, (isofhlevel m (x = x'))
end.
Theorem hlevelretract (n : nat) {X Y : UU} (p : X -> Y) (s : Y -> X)
(eps : ∏ y : Y , paths (p (s y)) y) : isofhlevel n X -> isofhlevel n Y.
Show proof.
revert X Y p s eps.
induction n as [ | n IHn ].
- intros X Y p s eps X0. unfold isofhlevel.
apply (iscontrretract p s eps X0).
- unfold isofhlevel. intros X Y p s eps X0 x x'. unfold isofhlevel in X0.
assert (is: isofhlevel n (paths (s x) (s x'))) by apply X0.
set (s':= @maponpaths _ _ s x x'). set (p':= pathssec2 s p eps x x').
set (eps':= @pathssec3 _ _ s p eps x x'). simpl.
apply (IHn _ _ p' s' eps' is).
induction n as [ | n IHn ].
- intros X Y p s eps X0. unfold isofhlevel.
apply (iscontrretract p s eps X0).
- unfold isofhlevel. intros X Y p s eps X0 x x'. unfold isofhlevel in X0.
assert (is: isofhlevel n (paths (s x) (s x'))) by apply X0.
set (s':= @maponpaths _ _ s x x'). set (p':= pathssec2 s p eps x x').
set (eps':= @pathssec3 _ _ s p eps x x'). simpl.
apply (IHn _ _ p' s' eps' is).
Corollary isofhlevelweqf (n : nat) {X Y : UU} (f : X ≃ Y) :
isofhlevel n X -> isofhlevel n Y.
Show proof.
Corollary isofhlevelweqb (n : nat) {X Y : UU} (f : X ≃ Y) :
isofhlevel n Y -> isofhlevel n X.
Show proof.
Lemma isofhlevelsn (n : nat) {X : UU} (f : X -> isofhlevel (S n) X) :
isofhlevel (S n) X.
Show proof.
intros. simpl. intros x x'. apply (f x x x').
Lemma isofhlevelssn (n : nat) {X : UU}
(is : ∏ x : X, isofhlevel (S n) (x = x)) : isofhlevel (S (S n)) X.
Show proof.
intros. simpl. intros x x'.
change (∏ (x0 x'0 : x = x'), isofhlevel n (x0 = x'0))
with (isofhlevel (S n) (x = x')).
assert (X1 : x = x' -> isofhlevel (S n) (x = x'))
by (intro X2; induction X2; apply (is x)).
apply (isofhlevelsn n X1).
change (∏ (x0 x'0 : x = x'), isofhlevel n (x0 = x'0))
with (isofhlevel (S n) (x = x')).
assert (X1 : x = x' -> isofhlevel (S n) (x = x'))
by (intro X2; induction X2; apply (is x)).
apply (isofhlevelsn n X1).
Definition isofhlevelf (n : nat) {X Y : UU} (f : X -> Y) : UU
:= ∏ y : Y, isofhlevel n (hfiber f y).
Theorem isofhlevelfhomot (n : nat) {X Y : UU} (f f' : X -> Y)
(h : ∏ x : X, paths (f x) (f' x)) :
isofhlevelf n f -> isofhlevelf n f'.
Show proof.
Theorem isofhlevelfpmap (n : nat) {X Y : UU} (f : X -> Y) (Q : Y -> UU) :
isofhlevelf n f -> isofhlevelf n (fpmap f Q).
Show proof.
intros X0.
unfold isofhlevelf. unfold isofhlevelf in X0.
intro y.
set (yy := pr1 y).
set (g := hfiberfpmap f Q y).
set (is := isweqhfiberfp f Q y).
set (isy := X0 yy).
apply (isofhlevelweqb n (make_weq g is) isy).
unfold isofhlevelf. unfold isofhlevelf in X0.
intro y.
set (yy := pr1 y).
set (g := hfiberfpmap f Q y).
set (is := isweqhfiberfp f Q y).
set (isy := X0 yy).
apply (isofhlevelweqb n (make_weq g is) isy).
Theorem isofhlevelfffromZ (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z)
(fs : fibseqstr f g z) (isz : isofhlevel (S n) Z) : isofhlevelf n f.
Show proof.
intros. intro y.
assert (w : (hfiber f y) ≃ ((g y) = z)).
apply (invweq (ezweq1 f g z fs y)).
apply (isofhlevelweqb n w (isz (g y) z)).
assert (w : (hfiber f y) ≃ ((g y) = z)).
apply (invweq (ezweq1 f g z fs y)).
apply (isofhlevelweqb n w (isz (g y) z)).
Theorem isofhlevelXfromg (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z)
(fs : fibseqstr f g z) : isofhlevelf n g -> isofhlevel n X.
Show proof.
intros isf.
assert (w : X ≃ (hfiber g z)).
apply (make_weq _ (pr2 fs)).
apply (isofhlevelweqb n w (isf z)).
assert (w : X ≃ (hfiber g z)).
apply (make_weq _ (pr2 fs)).
apply (isofhlevelweqb n w (isf z)).
Theorem isofhlevelffromXY (n : nat) {X Y : UU} (f : X -> Y) :
isofhlevel n X -> isofhlevel (S n) Y -> isofhlevelf n f.
Show proof.
revert X Y f.
induction n as [ | n IHn ].
- intros X Y f X0 X1.
assert (is1 : isofhlevel O Y).
{
split with (f (pr1 X0)).
intro t. unfold isofhlevel in X1.
set (is := X1 t (f (pr1 X0))).
apply (pr1 is).
}
apply (isweqcontrcontr f X0 is1).
- intros X Y f X0 X1. unfold isofhlevelf. simpl.
assert (is1 : ∏ x' x : X, isofhlevel n (x' = x))
by (simpl in X0; assumption).
assert (is2 : ∏ y' y : Y, isofhlevel (S n) (y' = y))
by (simpl in X1; simpl; assumption).
assert (is3 : ∏ (y : Y) (x : X) (xe' : hfiber f y),
isofhlevelf n (d2g f x xe'))
by (intros; apply (IHn _ _ (d2g f x xe') (is1 (pr1 xe') x)
(is2 (f x) y))).
assert (is4 : ∏ (y : Y) (x : X) (xe' : hfiber f y) (e : (f x) = y),
isofhlevel n ((make_hfiber f x e) = xe'))
by (intros; apply (isofhlevelweqb n (ezweq3g f x xe' e) (is3 y x xe' e))).
intros y xe xe'. induction xe as [ t x ].
apply (is4 y t xe' x).
induction n as [ | n IHn ].
- intros X Y f X0 X1.
assert (is1 : isofhlevel O Y).
{
split with (f (pr1 X0)).
intro t. unfold isofhlevel in X1.
set (is := X1 t (f (pr1 X0))).
apply (pr1 is).
}
apply (isweqcontrcontr f X0 is1).
- intros X Y f X0 X1. unfold isofhlevelf. simpl.
assert (is1 : ∏ x' x : X, isofhlevel n (x' = x))
by (simpl in X0; assumption).
assert (is2 : ∏ y' y : Y, isofhlevel (S n) (y' = y))
by (simpl in X1; simpl; assumption).
assert (is3 : ∏ (y : Y) (x : X) (xe' : hfiber f y),
isofhlevelf n (d2g f x xe'))
by (intros; apply (IHn _ _ (d2g f x xe') (is1 (pr1 xe') x)
(is2 (f x) y))).
assert (is4 : ∏ (y : Y) (x : X) (xe' : hfiber f y) (e : (f x) = y),
isofhlevel n ((make_hfiber f x e) = xe'))
by (intros; apply (isofhlevelweqb n (ezweq3g f x xe' e) (is3 y x xe' e))).
intros y xe xe'. induction xe as [ t x ].
apply (is4 y t xe' x).
Theorem isofhlevelXfromfY (n : nat) {X Y : UU} (f : X -> Y) :
isofhlevelf n f -> isofhlevel n Y -> isofhlevel n X.
Show proof.
revert X Y f.
induction n as [ | n IHn ].
- intros X Y f X0 X1.
apply (iscontrweqb (make_weq f X0) X1).
- intros X Y f X0 X1. simpl.
assert (is1 : ∏ (y : Y) (xe xe': hfiber f y), isofhlevel n (xe = xe'))
by (intros; apply (X0 y)).
assert (is2 : ∏ (y : Y) (x : X) (xe' : hfiber f y),
isofhlevelf n (d2g f x xe')).
{
intros. unfold isofhlevel. intro y0.
apply (isofhlevelweqf n (ezweq3g f x xe' y0)
(is1 y (make_hfiber f x y0) xe')).
}
assert (is3 : ∏ (y' y : Y), isofhlevel n (y' = y))
by (simpl in X1; assumption).
intros x' x.
set (y := f x'). set (e' := idpath y). set (xe' := make_hfiber f x' e').
apply (IHn _ _ (d2g f x xe') (is2 y x xe') (is3 (f x) y)).
induction n as [ | n IHn ].
- intros X Y f X0 X1.
apply (iscontrweqb (make_weq f X0) X1).
- intros X Y f X0 X1. simpl.
assert (is1 : ∏ (y : Y) (xe xe': hfiber f y), isofhlevel n (xe = xe'))
by (intros; apply (X0 y)).
assert (is2 : ∏ (y : Y) (x : X) (xe' : hfiber f y),
isofhlevelf n (d2g f x xe')).
{
intros. unfold isofhlevel. intro y0.
apply (isofhlevelweqf n (ezweq3g f x xe' y0)
(is1 y (make_hfiber f x y0) xe')).
}
assert (is3 : ∏ (y' y : Y), isofhlevel n (y' = y))
by (simpl in X1; assumption).
intros x' x.
set (y := f x'). set (e' := idpath y). set (xe' := make_hfiber f x' e').
apply (IHn _ _ (d2g f x xe') (is2 y x xe') (is3 (f x) y)).
Theorem isofhlevelffib (n : nat) {X : UU} (P : X -> UU) (x : X)
(is : ∏ x' : X, isofhlevel n (x' = x)) : isofhlevelf n (tpair P x).
Show proof.
Theorem isofhlevelfhfiberpr1y (n : nat) {X Y : UU} (f : X -> Y) (y : Y)
(is : ∏ y' : Y, isofhlevel n (y' = y)) :
isofhlevelf n (hfiberpr1 f y).
Show proof.
Theorem isofhlevelfsnfib (n : nat) {X : UU} (P : X -> UU) (x : X)
(is : isofhlevel (S n) (x = x)) : isofhlevelf (S n) (tpair P x).
Show proof.
intros. unfold isofhlevelf. intro xp.
apply (isofhlevelweqf (S n) (ezweq1pr1 P x xp)).
apply isofhlevelsn. intro X1. induction X1. assumption.
apply (isofhlevelweqf (S n) (ezweq1pr1 P x xp)).
apply isofhlevelsn. intro X1. induction X1. assumption.
Theorem isofhlevelfsnhfiberpr1 (n : nat) {X Y : UU} (f : X -> Y) (y : Y)
(is : isofhlevel (S n) (y = y)) : isofhlevelf (S n) (hfiberpr1 f y).
Show proof.
intros. unfold isofhlevelf. intro x.
apply (isofhlevelweqf (S n) ( ezweq1g f y x)). apply isofhlevelsn.
intro X1. induction X1. assumption.
apply (isofhlevelweqf (S n) ( ezweq1g f y x)). apply isofhlevelsn.
intro X1. induction X1. assumption.
Corollary isofhlevelfhfiberpr1 (n : nat) {X Y : UU} (f : X -> Y) (y : Y)
(is : isofhlevel (S n) Y) : isofhlevelf n (hfiberpr1 f y).
Show proof.
Theorem isofhlevelff (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) :
isofhlevelf n (λ x : X, g (f x)) -> isofhlevelf (S n) g -> isofhlevelf n f.
Show proof.
intros X0 X1. unfold isofhlevelf. intro y.
set (ye := make_hfiber g y (idpath (g y))).
apply (isofhlevelweqb n ( ezweqhf f g (g y) ye)
(isofhlevelffromXY n _ (X0 (g y)) (X1 (g y)) ye)).
set (ye := make_hfiber g y (idpath (g y))).
apply (isofhlevelweqb n ( ezweqhf f g (g y) ye)
(isofhlevelffromXY n _ (X0 (g y)) (X1 (g y)) ye)).
Theorem isofhlevelfgf (n : nat) {X Y Z : UU} (f : X -> Y) (g : Y -> Z) :
isofhlevelf n f -> isofhlevelf n g -> isofhlevelf n (λ x : X, g (f x)).
Show proof.
intros X0 X1. unfold isofhlevelf. intro z.
assert (is1 : isofhlevelf n (hfibersgftog f g z)).
{
unfold isofhlevelf. intro ye.
apply (isofhlevelweqf n (ezweqhf f g z ye) (X0 (pr1 ye))).
}
assert (is2 : isofhlevel n (hfiber g z))
by apply (X1 z).
apply (isofhlevelXfromfY n _ is1 is2).
assert (is1 : isofhlevelf n (hfibersgftog f g z)).
{
unfold isofhlevelf. intro ye.
apply (isofhlevelweqf n (ezweqhf f g z ye) (X0 (pr1 ye))).
}
assert (is2 : isofhlevel n (hfiber g z))
by apply (X1 z).
apply (isofhlevelXfromfY n _ is1 is2).
Theorem isofhlevelfgwtog (n : nat) {X Y Z : UU} (w : X ≃ Y) (g : Y -> Z)
(is : isofhlevelf n (λ x : X, g (w x))) : isofhlevelf n g.
Show proof.
intros. intro z.
assert (is' : isweq (hfibersgftog w g z)).
{
intro ye.
apply (iscontrweqf (ezweqhf w g z ye) (pr2 w (pr1 ye))).
}
apply (isofhlevelweqf _ (make_weq _ is') (is _)).
assert (is' : isweq (hfibersgftog w g z)).
{
intro ye.
apply (iscontrweqf (ezweqhf w g z ye) (pr2 w (pr1 ye))).
}
apply (isofhlevelweqf _ (make_weq _ is') (is _)).
Theorem isofhlevelfgtogw (n : nat) {X Y Z : UU} (w : X ≃ Y) (g : Y -> Z)
(is : isofhlevelf n g) : isofhlevelf n (λ x : X, g (w x)).
Show proof.
intros. intro z.
assert (is' : isweq (hfibersgftog w g z)).
{
intro ye.
apply (iscontrweqf (ezweqhf w g z ye) (pr2 w (pr1 ye))).
}
apply (isofhlevelweqb _ (make_weq _ is') (is _)).
assert (is' : isweq (hfibersgftog w g z)).
{
intro ye.
apply (iscontrweqf (ezweqhf w g z ye) (pr2 w (pr1 ye))).
}
apply (isofhlevelweqb _ (make_weq _ is') (is _)).
Corollary isofhlevelfhomot2 (n : nat) {X X' Y : UU} (f : X -> Y) (f' : X' -> Y)
(w : X ≃ X') (h : ∏ x : X, paths (f x) (f' (w x))) :
isofhlevelf n f -> isofhlevelf n f'.
Show proof.
intros X0.
assert (X1 : isofhlevelf n (λ x : X, f' (w x)))
by apply (isofhlevelfhomot n _ _ h X0).
apply (isofhlevelfgwtog n w f' X1).
assert (X1 : isofhlevelf n (λ x : X, f' (w x)))
by apply (isofhlevelfhomot n _ _ h X0).
apply (isofhlevelfgwtog n w f' X1).
Theorem isofhlevelfonpaths (n : nat) {X Y : UU} (f : X -> Y) (x x' : X) :
isofhlevelf (S n) f -> isofhlevelf n (@maponpaths _ _ f x x').
Show proof.
intros X0.
set (y := f x'). set (xe' := make_hfiber f x' (idpath _)).
assert (is1 : isofhlevelf n (d2g f x xe')).
{
unfold isofhlevelf. intro y0.
apply (isofhlevelweqf n (ezweq3g f x xe' y0)
(X0 y (make_hfiber f x y0) xe')).
}
assert (h : ∏ ee : x' = x, paths (d2g f x xe' ee)
(maponpaths f (pathsinv0 ee))).
{
intro.
assert (e0: paths (pathscomp0 (maponpaths f (pathsinv0 ee)) (idpath _))
(maponpaths f (pathsinv0 ee)))
by (induction ee; simpl; apply idpath).
apply (e0).
}
apply (isofhlevelfhomot2 n _ _ (make_weq (@pathsinv0 _ x' x)
(isweqpathsinv0 _ _)) h is1).
set (y := f x'). set (xe' := make_hfiber f x' (idpath _)).
assert (is1 : isofhlevelf n (d2g f x xe')).
{
unfold isofhlevelf. intro y0.
apply (isofhlevelweqf n (ezweq3g f x xe' y0)
(X0 y (make_hfiber f x y0) xe')).
}
assert (h : ∏ ee : x' = x, paths (d2g f x xe' ee)
(maponpaths f (pathsinv0 ee))).
{
intro.
assert (e0: paths (pathscomp0 (maponpaths f (pathsinv0 ee)) (idpath _))
(maponpaths f (pathsinv0 ee)))
by (induction ee; simpl; apply idpath).
apply (e0).
}
apply (isofhlevelfhomot2 n _ _ (make_weq (@pathsinv0 _ x' x)
(isweqpathsinv0 _ _)) h is1).
Theorem isofhlevelfsn (n : nat) {X Y : UU} (f : X -> Y) :
(∏ x x' : X, isofhlevelf n (@maponpaths _ _ f x x')) -> isofhlevelf (S n) f.
Show proof.
intros X0. unfold isofhlevelf. intro y. simpl.
intros x x'.
induction x as [ x e ]. induction x' as [ x' e' ]. induction e'.
set (xe' := make_hfiber f x' (idpath _)).
set (xe := make_hfiber f x e).
set (d3 := d2g f x xe'). simpl in d3.
assert (is1 : isofhlevelf n (d2g f x xe')).
assert (h : ∏ ee : x' = x, paths (maponpaths f (pathsinv0 ee))
(d2g f x xe' ee)).
{
intro. unfold d2g. simpl.
apply (pathsinv0 (pathscomp0rid _)).
}
assert (is2 : isofhlevelf n (λ ee: x' = x, maponpaths f (pathsinv0 ee)))
by apply (isofhlevelfgtogw n ( make_weq _ (isweqpathsinv0 _ _))
(@maponpaths _ _ f x x') (X0 x x')).
apply (isofhlevelfhomot n _ _ h is2).
apply (isofhlevelweqb n (ezweq3g f x xe' e) (is1 e)).
intros x x'.
induction x as [ x e ]. induction x' as [ x' e' ]. induction e'.
set (xe' := make_hfiber f x' (idpath _)).
set (xe := make_hfiber f x e).
set (d3 := d2g f x xe'). simpl in d3.
assert (is1 : isofhlevelf n (d2g f x xe')).
assert (h : ∏ ee : x' = x, paths (maponpaths f (pathsinv0 ee))
(d2g f x xe' ee)).
{
intro. unfold d2g. simpl.
apply (pathsinv0 (pathscomp0rid _)).
}
assert (is2 : isofhlevelf n (λ ee: x' = x, maponpaths f (pathsinv0 ee)))
by apply (isofhlevelfgtogw n ( make_weq _ (isweqpathsinv0 _ _))
(@maponpaths _ _ f x x') (X0 x x')).
apply (isofhlevelfhomot n _ _ h is2).
apply (isofhlevelweqb n (ezweq3g f x xe' e) (is1 e)).
Theorem isofhlevelfssn (n : nat) {X Y : UU} (f : X -> Y) :
(∏ x : X, isofhlevelf (S n) (@maponpaths _ _ f x x))
-> isofhlevelf (S (S n)) f.
Show proof.
intros X0. unfold isofhlevelf. intro y.
assert (∏ xe0 : hfiber f y, isofhlevel (S n) (xe0 = xe0)).
{
intro. induction xe0 as [ x e ]. induction e.
set (e':= idpath (f x)).
set (xe':= make_hfiber f x e').
set (xe:= make_hfiber f x e').
set (d3:= d2g f x xe'). simpl in d3.
assert (is1: isofhlevelf (S n) (d2g f x xe')).
{
assert (h : ∏ ee: x = x, paths (maponpaths f (pathsinv0 ee))
(d2g f x xe' ee)).
{
intro. unfold d2g. simpl.
apply (pathsinv0 (pathscomp0rid _)).
}
assert (is2 : isofhlevelf (S n) (fun ee : x = x
=> maponpaths f (pathsinv0 ee)))
by apply (isofhlevelfgtogw (S n) (make_weq _ (isweqpathsinv0 _ _))
(@maponpaths _ _ f x x) (X0 x)).
apply (isofhlevelfhomot (S n) _ _ h is2).
}
apply (isofhlevelweqb (S n) (ezweq3g f x xe' e') (is1 e')).
}
apply (isofhlevelssn).
assumption.
assert (∏ xe0 : hfiber f y, isofhlevel (S n) (xe0 = xe0)).
{
intro. induction xe0 as [ x e ]. induction e.
set (e':= idpath (f x)).
set (xe':= make_hfiber f x e').
set (xe:= make_hfiber f x e').
set (d3:= d2g f x xe'). simpl in d3.
assert (is1: isofhlevelf (S n) (d2g f x xe')).
{
assert (h : ∏ ee: x = x, paths (maponpaths f (pathsinv0 ee))
(d2g f x xe' ee)).
{
intro. unfold d2g. simpl.
apply (pathsinv0 (pathscomp0rid _)).
}
assert (is2 : isofhlevelf (S n) (fun ee : x = x
=> maponpaths f (pathsinv0 ee)))
by apply (isofhlevelfgtogw (S n) (make_weq _ (isweqpathsinv0 _ _))
(@maponpaths _ _ f x x) (X0 x)).
apply (isofhlevelfhomot (S n) _ _ h is2).
}
apply (isofhlevelweqb (S n) (ezweq3g f x xe' e') (is1 e')).
}
apply (isofhlevelssn).
assumption.
Theorem isofhlevelfpr1 (n : nat) {X : UU} (P : X -> UU)
(is : ∏ x : X, isofhlevel n (P x)) : isofhlevelf n (@pr1 X P).
Show proof.
Lemma isweqpr1 {Z : UU} (P : Z -> UU) (is1 : ∏ z : Z, iscontr (P z)) :
isweq (@pr1 Z P).
Show proof.
Definition weqpr1 {Z : UU} (P : Z -> UU) (is : ∏ z : Z , iscontr (P z)) :
weq (total2 P) Z := make_weq _ (isweqpr1 P is).
h-level of the total space total2
Theorem isofhleveltotal2 (n : nat) {X : UU} (P : X -> UU) (is1 : isofhlevel n X)
(is2 : ∏ x : X, isofhlevel n (P x)) : isofhlevel n (total2 P).
Show proof.
Corollary isofhleveldirprod (n : nat) (X Y : UU) (is1 : isofhlevel n X)
(is2 : isofhlevel n Y) : isofhlevel n (X × Y).
Show proof.
Definition isaprop := isofhlevel 1.
Definition isPredicate {X : UU} (Y : X -> UU) := ∏ x : X, isaprop (Y x).
Definition isapropunit : isaprop unit := iscontrpathsinunit.
Definition isapropdirprod (X Y : UU) : isaprop X -> isaprop Y -> isaprop (X × Y)
:= isofhleveldirprod 1 X Y.
Lemma isapropifcontr {X : UU} (is : iscontr X) : isaprop X.
Show proof.
intros. set (f := λ x : X, tt).
assert (isw : isweq f)
by (apply isweqcontrtounit; assumption).
apply (isofhlevelweqb (S O) (make_weq f isw)).
intros x x'.
apply iscontrpathsinunit.
assert (isw : isweq f)
by (apply isweqcontrtounit; assumption).
apply (isofhlevelweqb (S O) (make_weq f isw)).
intros x x'.
apply iscontrpathsinunit.
Theorem hlevelntosn (n : nat) (T : UU) (is : isofhlevel n T) : isofhlevel (S n) T.
Show proof.
revert T is.
induction n as [ | n IHn ].
- intro. apply isapropifcontr.
- intro. intro X.
change (∏ t1 t2 : T, isofhlevel (S n) (t1 = t2)).
intros t1 t2.
change (∏ t1 t2 : T, isofhlevel n (t1 = t2)) in X.
set (XX := X t1 t2).
apply (IHn _ XX).
induction n as [ | n IHn ].
- intro. apply isapropifcontr.
- intro. intro X.
change (∏ t1 t2 : T, isofhlevel (S n) (t1 = t2)).
intros t1 t2.
change (∏ t1 t2 : T, isofhlevel n (t1 = t2)) in X.
set (XX := X t1 t2).
apply (IHn _ XX).
Corollary isofhlevelcontr (n : nat) {X : UU} (is : iscontr X) : isofhlevel n X.
Show proof.
revert X is.
induction n as [ | n IHn ].
- intros X X0. assumption.
- intros X X0. simpl. intros x x'.
assert (is : iscontr (x = x')).
apply (isapropifcontr X0 x x').
apply (IHn _ is).
induction n as [ | n IHn ].
- intros X X0. assumption.
- intros X X0. simpl. intros x x'.
assert (is : iscontr (x = x')).
apply (isapropifcontr X0 x x').
apply (IHn _ is).
Lemma isofhlevelfweq (n : nat) {X Y : UU} (f : X ≃ Y) : isofhlevelf n f.
Show proof.
Corollary isweqfinfibseq {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z)
(fs : fibseqstr f g z) (isz : iscontr Z) : isweq f.
Show proof.
Corollary weqhfibertocontr {X Y : UU} (f : X -> Y) (y : Y) (is : iscontr Y) :
weq (hfiber f y) X.
Show proof.
Corollary weqhfibertounit (X : UU) : (hfiber (λ x : X, tt) tt) ≃ X.
Show proof.
Corollary isofhleveltofun (n : nat) (X : UU) :
isofhlevel n X -> isofhlevelf n (λ x : X, tt).
Show proof.
Corollary isofhlevelfromfun (n : nat) (X : UU) :
isofhlevelf n (λ x : X, tt) -> isofhlevel n X.
Show proof.
Definition weqhfiberunit {X Z : UU} (i : X -> Z) (z : Z) :
(∑ x, hfiber (λ _ : unit, z) (i x)) ≃ hfiber i z.
Show proof.
intros. use weq_iso.
+ intros [x [t e]]. exact (x,,!e).
+ intros [x e]. exact (x,,tt,,!e).
+ intros [x [t e]]. apply maponpaths. simple refine (two_arg_paths_f _ _).
* apply isapropunit.
* simpl. induction e. rewrite pathsinv0inv0. induction t. apply idpath.
+ intros [x e]. apply maponpaths. apply pathsinv0inv0.
+ intros [x [t e]]. exact (x,,!e).
+ intros [x e]. exact (x,,tt,,!e).
+ intros [x [t e]]. apply maponpaths. simple refine (two_arg_paths_f _ _).
* apply isapropunit.
* simpl. induction e. rewrite pathsinv0inv0. induction t. apply idpath.
+ intros [x e]. apply maponpaths. apply pathsinv0inv0.
Lemma isofhlevelsnprop (n : nat) {X : UU} (is : isaprop X) : isofhlevel (S n) X.
Show proof.
A proposition that is inhabited is contractible.
Lemma iscontraprop1 {X : UU} (is : isaprop X) (x : X) : iscontr X.
Show proof.
Lemma iscontraprop1inv {X : UU} (f : X -> iscontr X) : isaprop X.
Show proof.
Definition isProofIrrelevant (X:UU) := ∏ x y:X, x = y.
Lemma proofirrelevance (X : UU) : isaprop X -> isProofIrrelevant X.
Show proof.
Lemma invproofirrelevance (X : UU) : isProofIrrelevant X -> isaprop X.
Show proof.
Lemma isProofIrrelevant_paths {X} (irr:isProofIrrelevant X) {x y:X} : isProofIrrelevant (x=y).
Show proof.
Lemma isapropcoprod (P Q : UU) :
isaprop P -> isaprop Q -> (P -> Q -> ∅) -> isaprop (P ⨿ Q).
Show proof.
Lemma isweqimplimpl {X Y : UU} (f : X -> Y) (g : Y -> X) (isx : isaprop X)
(isy : isaprop Y) : isweq f.
Show proof.
Definition weqimplimpl {X Y : UU} (f : X -> Y) (g : Y -> X) (isx : isaprop X)
(isy : isaprop Y) := make_weq _ (isweqimplimpl f g isx isy).
Definition weqiff {X Y : UU} : (X <-> Y) -> isaprop X -> isaprop Y -> X ≃ Y
:= λ f i j, make_weq _ (isweqimplimpl (pr1 f) (pr2 f) i j).
Definition weq_to_iff {X Y : UU} : X ≃ Y -> (X <-> Y)
:= λ f, (pr1weq f ,, invmap f).
Theorem isapropempty: isaprop empty.
Show proof.
Theorem isapropifnegtrue {X : UU} (a : X -> empty) : isaprop X.
Show proof.
Lemma isapropretract {P Q : UU} (i : isaprop Q) (f : P -> Q) (g : Q -> P)
(h : g ∘ f ~ idfun _) : isaprop P.
Show proof.
Lemma isapropcomponent1 (P Q : UU) : isaprop (P ⨿ Q) -> isaprop P.
Show proof.
Lemma isapropcomponent2 (P Q : UU) : isaprop (P ⨿ Q) -> isaprop Q.
Show proof.
Show proof.
intros. unfold iscontr. split with x. intro t.
unfold isofhlevel in is.
set (is' := is t x).
apply (pr1 is').
unfold isofhlevel in is.
set (is' := is t x).
apply (pr1 is').
Lemma iscontraprop1inv {X : UU} (f : X -> iscontr X) : isaprop X.
Show proof.
Definition isProofIrrelevant (X:UU) := ∏ x y:X, x = y.
Lemma proofirrelevance (X : UU) : isaprop X -> isProofIrrelevant X.
Show proof.
Lemma invproofirrelevance (X : UU) : isProofIrrelevant X -> isaprop X.
Show proof.
Lemma isProofIrrelevant_paths {X} (irr:isProofIrrelevant X) {x y:X} : isProofIrrelevant (x=y).
Show proof.
Lemma isapropcoprod (P Q : UU) :
isaprop P -> isaprop Q -> (P -> Q -> ∅) -> isaprop (P ⨿ Q).
Show proof.
intros i j n. apply invproofirrelevance.
intros a b. apply inv_equality_by_case.
induction a as [a|a].
- induction b as [b|b].
+ apply i.
+ contradicts (n a) b.
- induction b as [b|b].
+ contradicts (n b) a.
+ apply j.
intros a b. apply inv_equality_by_case.
induction a as [a|a].
- induction b as [b|b].
+ apply i.
+ contradicts (n a) b.
- induction b as [b|b].
+ contradicts (n b) a.
+ apply j.
Lemma isweqimplimpl {X Y : UU} (f : X -> Y) (g : Y -> X) (isx : isaprop X)
(isy : isaprop Y) : isweq f.
Show proof.
intros.
assert (isx0: ∏ x : X, paths (g (f x)) x)
by (intro; apply proofirrelevance; apply isx).
assert (isy0 : ∏ y : Y, paths (f (g y)) y)
by (intro; apply proofirrelevance; apply isy).
apply (isweq_iso f g isx0 isy0).
assert (isx0: ∏ x : X, paths (g (f x)) x)
by (intro; apply proofirrelevance; apply isx).
assert (isy0 : ∏ y : Y, paths (f (g y)) y)
by (intro; apply proofirrelevance; apply isy).
apply (isweq_iso f g isx0 isy0).
Definition weqimplimpl {X Y : UU} (f : X -> Y) (g : Y -> X) (isx : isaprop X)
(isy : isaprop Y) := make_weq _ (isweqimplimpl f g isx isy).
Definition weqiff {X Y : UU} : (X <-> Y) -> isaprop X -> isaprop Y -> X ≃ Y
:= λ f i j, make_weq _ (isweqimplimpl (pr1 f) (pr2 f) i j).
Definition weq_to_iff {X Y : UU} : X ≃ Y -> (X <-> Y)
:= λ f, (pr1weq f ,, invmap f).
Theorem isapropempty: isaprop empty.
Show proof.
Theorem isapropifnegtrue {X : UU} (a : X -> empty) : isaprop X.
Show proof.
Lemma isapropretract {P Q : UU} (i : isaprop Q) (f : P -> Q) (g : Q -> P)
(h : g ∘ f ~ idfun _) : isaprop P.
Show proof.
intros.
apply invproofirrelevance; intros p p'.
refine (_ @ (_ : g (f p) = g (f p')) @ _).
- apply pathsinv0. apply h.
- apply maponpaths. apply proofirrelevance. exact i.
- apply h.
apply invproofirrelevance; intros p p'.
refine (_ @ (_ : g (f p) = g (f p')) @ _).
- apply pathsinv0. apply h.
- apply maponpaths. apply proofirrelevance. exact i.
- apply h.
Lemma isapropcomponent1 (P Q : UU) : isaprop (P ⨿ Q) -> isaprop P.
Show proof.
intros i. apply invproofirrelevance; intros p p'.
exact (equality_by_case (proofirrelevance _ i (ii1 p) (ii1 p'))).
exact (equality_by_case (proofirrelevance _ i (ii1 p) (ii1 p'))).
Lemma isapropcomponent2 (P Q : UU) : isaprop (P ⨿ Q) -> isaprop Q.
Show proof.
intros i. apply invproofirrelevance; intros q q'.
exact (equality_by_case (proofirrelevance _ i (ii2 q) (ii2 q'))).
exact (equality_by_case (proofirrelevance _ i (ii2 q) (ii2 q'))).
Definition isincl {X Y : UU} (f : X -> Y) := isofhlevelf 1 f.
Definition incl (X Y : UU) := total2 (fun f : X -> Y => isincl f).
Definition make_incl {X Y : UU} (f : X -> Y) (is : isincl f) :
incl X Y := tpair _ f is.
Definition pr1incl (X Y : UU) : incl X Y -> (X -> Y) := @pr1 _ _.
Coercion pr1incl : incl >-> Funclass.
Lemma isinclweq (X Y : UU) (f : X -> Y) : isweq f -> isincl f.
Show proof.
Coercion isinclweq : isweq >-> isincl.
Lemma isofhlevelfsnincl (n : nat) {X Y : UU} (f : X -> Y) (is : isincl f) :
isofhlevelf (S n) f.
Show proof.
Definition weqtoincl {X Y : UU} : X ≃ Y -> incl X Y
:= λ w, make_incl (pr1weq w) (pr2 w).
Lemma isinclcomp {X Y Z : UU} (f : incl X Y) (g : incl Y Z) :
isincl (funcomp (pr1 f) (pr1 g)).
Show proof.
Definition inclcomp {X Y Z : UU} (f : incl X Y) (g : incl Y Z) :
incl X Z := make_incl (funcomp (pr1 f) (pr1 g)) (isinclcomp f g).
Lemma isincltwooutof3a {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isg : isincl g)
(isgf : isincl (funcomp f g)) : isincl f.
Show proof.
Lemma isinclgwtog {X Y Z : UU} (w : X ≃ Y) (g : Y -> Z)
(is : isincl (funcomp w g)) : isincl g.
Show proof.
Lemma isinclgtogw {X Y Z : UU} (w : X ≃ Y) (g : Y -> Z) (is : isincl g) :
isincl (funcomp w g).
Show proof.
Lemma isinclhomot {X Y : UU} (f g : X -> Y) (h : homot f g) (isf : isincl f) :
isincl g.
Show proof.
Definition isofhlevelsninclb (n : nat) {X Y : UU} (f : X -> Y) (is : isincl f) :
isofhlevel (S n) Y -> isofhlevel (S n) X
:= isofhlevelXfromfY (S n) f (isofhlevelfsnincl n f is).
Definition isapropinclb {X Y : UU} (f : X -> Y) (isf : isincl f) :
isaprop Y -> isaprop X := isofhlevelXfromfY 1 _ isf.
Lemma iscontrhfiberofincl {X Y : UU} (f : X -> Y) :
isincl f -> (∏ x : X, iscontr (hfiber f (f x))).
Show proof.
intros X0 x. unfold isofhlevelf in X0.
set (isy := X0 (f x)).
apply (iscontraprop1 isy (make_hfiber f _ (idpath (f x)))).
set (isy := X0 (f x)).
apply (iscontraprop1 isy (make_hfiber f _ (idpath (f x)))).
Definition isInjective {X Y : UU} (f : X -> Y)
:= ∏ (x x' : X), isweq (maponpaths f : x = x' -> f x = f x').
Definition Injectivity {X Y : UU} (f : X -> Y) :
isInjective f -> ∏ (x x' : X), x = x' ≃ f x = f x'.
Show proof.
Lemma isweqonpathsincl {X Y : UU} (f : X -> Y) : isincl f -> isInjective f.
Show proof.
Definition weqonpathsincl {X Y : UU} (f : X -> Y) (is : isincl f) (x x' : X)
:= make_weq _ (isweqonpathsincl f is x x').
Definition invmaponpathsincl {X Y : UU} (f : X -> Y) :
isincl f -> ∏ x x', f x = f x' -> x = x'.
Show proof.
Lemma isinclweqonpaths {X Y : UU} (f : X -> Y) : isInjective f -> isincl f.
Show proof.
Definition isinclpr1 {X : UU} (P : X -> UU) (is : ∏ x : X, isaprop (P x)) :
isincl (@pr1 X P):= isofhlevelfpr1 (S O) P is.
Theorem subtypeInjectivity {A : UU} (B : A -> UU) :
isPredicate B -> ∏ (x y : total2 B), (x = y) ≃ (pr1 x = pr1 y).
Show proof.
Corollary subtypePath {A : UU} {B : A -> UU} (is : isPredicate B)
{s s' : total2 (λ x, B x)} : pr1 s = pr1 s' -> s = s'.
Show proof.
Corollary subtypePath' {A : UU} {B : A -> UU}
{s s' : total2 (λ x, B x)} : pr1 s = pr1 s' -> isaprop (B (pr1 s')) -> s = s'.
Show proof.
Corollary unique_exists {A : UU} {B : A -> UU} (x : A) (b : B x)
(h : ∏ y, isaprop (B y)) (H : ∏ y, B y -> y = x) :
iscontr (total2 (λ t : A, B t)).
Show proof.
use make_iscontr.
- exact (x,,b).
- intros t. apply subtypePath.
+ exact h.
+ apply (H (pr1 t)). exact (pr2 t).
- exact (x,,b).
- intros t. apply subtypePath.
+ exact h.
+ apply (H (pr1 t)). exact (pr2 t).
Definition subtypePairEquality {X : UU} {P : X -> UU} (is : isPredicate P)
{x y : X} {p : P x} {q : P y} :
x = y -> (x,,p) = (y,,q).
Show proof.
Definition subtypePairEquality' {X : UU} {P : X -> UU}
{x y : X} {p : P x} {q : P y} :
x = y -> isaprop(P y) -> (x,,p) = (y,,q).
Show proof.
Theorem samehfibers {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (is1 : isincl g)
(y : Y) : hfiber f y ≃ hfiber (g ∘ f) (g y).
Show proof.
intros. exists (hfibersftogf f g (g y) (make_hfiber g y (idpath _))).
set (z := g y). set (ye := make_hfiber g y (idpath _)). intro xe.
apply (iscontrweqf (X := hfibersgftog f g z xe = ye)).
{ exists (ezmap _ _ _ (fibseq1 _ _ _ (fibseqhf f g z ye) _)).
exact (isweqezmap1 _ _ _ _ _). }
apply isapropifcontr. apply iscontrhfiberofincl. exact is1.
set (z := g y). set (ye := make_hfiber g y (idpath _)). intro xe.
apply (iscontrweqf (X := hfibersgftog f g z xe = ye)).
{ exists (ezmap _ _ _ (fibseq1 _ _ _ (fibseqhf f g z ye) _)).
exact (isweqezmap1 _ _ _ _ _). }
apply isapropifcontr. apply iscontrhfiberofincl. exact is1.
Definition isaset (X : UU) : UU := ∏ x x' : X, isaprop (x = x').
Notation isasetdirprod := (isofhleveldirprod 2).
Lemma isasetunit : isaset unit.
Show proof.
Lemma isasetempty : isaset empty.
Show proof.
Lemma isasetifcontr {X : UU} (is : iscontr X) : isaset X.
Show proof.
Lemma isasetaprop {X : UU} (is : isaprop X) : isaset X.
Show proof.
Corollary isaset_total2 {X : UU} (P : X->UU) :
isaset X -> (∏ x, isaset (P x)) -> isaset (∑ x, P x).
Show proof.
Corollary isaset_dirprod {X Y : UU} : isaset X -> isaset Y -> isaset (X × Y).
Show proof.
Corollary isaset_hfiber {X Y : UU} (f : X -> Y) (y : Y) : isaset X -> isaset Y -> isaset (hfiber f y).
Show proof.
The following lemma asserts "uniqueness of identity proofs" (uip) for
sets.
For the theorem about the coproduct of two sets see isasetcoprod
below.
Lemma isofhlevelssnset (n : nat) (X : UU) (is : isaset X) :
isofhlevel (S (S n)) X.
Show proof.
Lemma isasetifiscontrloops (X : UU) : (∏ x : X, iscontr (x = x)) -> isaset X.
Show proof.
intros X0. unfold isaset. unfold isofhlevel. intros x x' x0 x0'.
induction x0.
apply isapropifcontr.
exact (X0 x).
induction x0.
apply isapropifcontr.
exact (X0 x).
Lemma iscontrloopsifisaset (X : UU) :
(isaset X) -> (∏ x : X, iscontr (x = x)).
Show proof.
intros X0 x. unfold isaset in X0. unfold isofhlevel in X0.
change (∏ (x x' : X) (x0 x'0 : x = x'), iscontr (x0 = x'0))
with (∏ (x x' : X), isaprop (x = x')) in X0.
apply (iscontraprop1 (X0 x x) (idpath x)).
change (∏ (x x' : X) (x0 x'0 : x = x'), iscontr (x0 = x'0))
with (∏ (x x' : X), isaprop (x = x')) in X0.
apply (iscontraprop1 (X0 x x) (idpath x)).
A monic subtype of a set is a set.
Theorem isasetsubset {X Y : UU} (f : X -> Y) (is1 : isaset Y) (is2 : isincl f) :
isaset X.
Show proof.
The morphism from hfiber of a map to a set is an inclusion.
Theorem isinclfromhfiber {X Y : UU} (f: X -> Y) (is : isaset Y) (y : Y) :
@isincl (hfiber f y) X (@pr1 _ _).
Show proof.
Criterion for a function between sets being an inclusion.
Theorem isinclbetweensets {X Y : UU} (f : X -> Y)
(isx : isaset X) (isy : isaset Y)
(inj : ∏ x x' : X , (paths (f x) (f x') -> x = x')) : isincl f.
Show proof.
intros. apply isinclweqonpaths. intros x x'.
apply (isweqimplimpl (@maponpaths _ _ f x x') (inj x x') (isx x x')
(isy (f x) (f x'))).
apply (isweqimplimpl (@maponpaths _ _ f x x') (inj x x') (isx x x')
(isy (f x) (f x'))).
A map from unit to a set is an inclusion.
Theorem isinclfromunit {X : UU} (f : unit -> X) (is : isaset X) : isincl f.
Show proof.
intros.
apply (isinclbetweensets f (isofhlevelcontr 2 (iscontrunit)) is).
intros. induction x. induction x'. apply idpath.
apply (isinclbetweensets f (isofhlevelcontr 2 (iscontrunit)) is).
intros. induction x. induction x'. apply idpath.
Corollary set_bijection_to_weq {X Y : UU} (f : X -> Y) :
UniqueConstruction f -> isaset Y -> isweq f.
Show proof.
intros bij i y. set (sur := pr1 bij); set (inj := pr2 bij).
use tpair.
- exists (pr1 (sur y)). exact (pr2 (sur y)).
- intro w.
use total2_paths_f.
+ simpl. apply inj. intermediate_path y.
* exact (pr2 w).
* exact (! pr2 (sur y)).
+ induction w as [x e]; simpl. induction e.
apply i.
use tpair.
- exists (pr1 (sur y)). exact (pr2 (sur y)).
- intro w.
use total2_paths_f.
+ simpl. apply inj. intermediate_path y.
* exact (pr2 w).
* exact (! pr2 (sur y)).
+ induction w as [x e]; simpl. induction e.
apply i.
Complementary types
Definition complementary P Q := (P -> Q -> ∅) × (P ⨿ Q).
Definition complementary_to_neg_iff {P Q} : complementary P Q -> ¬P <-> Q.
Show proof.
intros c.
induction c as [n c]. split.
- intro np. induction c as [p|q].
* contradicts p np.
* exact q.
- intro q. induction c as [p|_].
* intros _. exact (n p q).
* intros p. exact (n p q).
induction c as [n c]. split.
- intro np. induction c as [p|q].
* contradicts p np.
* exact q.
- intro q. induction c as [p|_].
* intros _. exact (n p q).
* intros p. exact (n p q).
Definition decidable (X:UU) := X ⨿ ¬X.
Definition decidable_to_complementary {X} : decidable X -> complementary X (¬X).
Show proof.
intros d. split.
- intros x n. exact (n x).
- exact d.
- intros x n. exact (n x).
- exact d.
Definition decidable_dirprod (X Y : UU) :
decidable X -> decidable Y -> decidable (X × Y).
Show proof.
intros b c.
induction b as [b|b'].
- induction c as [c|c'].
+ apply ii1. exact (b,,c).
+ apply ii2. clear b. intro k. apply c'. exact (pr2 k).
- clear c. apply ii2. intro k. apply b'. exact (pr1 k).
induction b as [b|b'].
- induction c as [c|c'].
+ apply ii1. exact (b,,c).
+ apply ii2. clear b. intro k. apply c'. exact (pr2 k).
- clear c. apply ii2. intro k. apply b'. exact (pr1 k).
Decidable propositions isdecprop
Definition isdecprop (P:UU) := (P ⨿ ¬P) × isaprop P.
Definition isdecproptoisaprop ( X : UU ) ( is : isdecprop X ) : isaprop X := pr2 is.
Coercion isdecproptoisaprop : isdecprop >-> isaprop .
Lemma isdecpropif ( X : UU ) : isaprop X -> X ⨿ ¬ X -> isdecprop X.
Show proof.
Lemma isdecpropfromiscontr {P} : iscontr P -> isdecprop P.
Show proof.
Lemma isdecpropempty : isdecprop ∅.
Show proof.
Lemma isdecpropweqf {X Y} : X≃Y -> isdecprop X -> isdecprop Y.
Show proof.
intros w i. unfold isdecprop in *. induction i as [xnx i]. split.
- clear i. induction xnx as [x|nx].
* apply ii1. apply w. assumption.
* apply ii2. intro x'. apply nx. apply (invmap w). assumption.
- apply (isofhlevelweqf 1 (X:=X)).
{ exact w. }
{ exact i. }
- clear i. induction xnx as [x|nx].
* apply ii1. apply w. assumption.
* apply ii2. intro x'. apply nx. apply (invmap w). assumption.
- apply (isofhlevelweqf 1 (X:=X)).
{ exact w. }
{ exact i. }
Lemma isdecpropweqb {X Y} : X≃Y -> isdecprop Y -> isdecprop X.
Show proof.
intros w i. unfold isdecprop in *. induction i as [yny i]. split.
- clear i. induction yny as [y|ny].
* apply ii1. apply (invmap w). assumption.
* apply ii2. intro x. apply ny. apply w. assumption.
- apply (isofhlevelweqb 1 (Y:=Y)).
{ exact w. }
{ exact i. }
- clear i. induction yny as [y|ny].
* apply ii1. apply (invmap w). assumption.
* apply ii2. intro x. apply ny. apply w. assumption.
- apply (isofhlevelweqb 1 (Y:=Y)).
{ exact w. }
{ exact i. }
Lemma isdecproplogeqf {X Y : UU} (isx : isdecprop X) (isy : isaprop Y)
(lg : X <-> Y) : isdecprop Y.
Show proof.
Lemma isdecproplogeqb {X Y : UU} (isx : isaprop X) (isy : isdecprop Y)
(lg : X <-> Y) : isdecprop X.
Show proof.
Lemma isdecpropfromneg {P : UU} : ¬P -> isdecprop P.
Show proof.
Definition isdeceq (X:UU) : UU := ∏ (x x':X), decidable (x=x').
Lemma isdeceqweqf {X Y : UU} (w : X ≃ Y) (is : isdeceq X) : isdeceq Y.
Show proof.
intros. intros y y'.
set (w' := weqonpaths (invweq w) y y').
set (int := is ((invweq w) y) ((invweq w) y')).
induction int as [ i | ni ].
- apply (ii1 ((invweq w') i)).
- apply (ii2 ((negf w') ni)).
set (w' := weqonpaths (invweq w) y y').
set (int := is ((invweq w) y) ((invweq w) y')).
induction int as [ i | ni ].
- apply (ii1 ((invweq w') i)).
- apply (ii2 ((negf w') ni)).
Lemma isdeceqweqb {X Y : UU} (w : X ≃ Y) (is : isdeceq Y) : isdeceq X.
Show proof.
Theorem isdeceqinclb {X Y : UU} (f : X -> Y) (is : isdeceq Y) (is' : isincl f) :
isdeceq X.
Show proof.
intros. intros x x'.
set (w := weqonpathsincl f is' x x'). set (int := is (f x) (f x')).
induction int as [ i | ni ].
- apply (ii1 ((invweq w) i)).
- apply (ii2 ((negf w) ni)).
set (w := weqonpathsincl f is' x x'). set (int := is (f x) (f x')).
induction int as [ i | ni ].
- apply (ii1 ((invweq w) i)).
- apply (ii2 ((negf w) ni)).
Lemma isdeceqifisaprop (X : UU) : isaprop X -> isdeceq X.
Show proof.
Definition booleq {X : UU} (is : isdeceq X) (x x' : X) : bool.
Show proof.
Lemma eqfromdnegeq (X : UU) (is : isdeceq X) (x x' : X) :
dneg (x = x') -> x = x'.
Show proof.
intros X0. induction (is x x') as [ y | n ].
- assumption.
- induction (X0 n).
- assumption.
- induction (X0 n).
Lemma isdecequnit : isdeceq unit.
Show proof.
Theorem isdeceqbool: isdeceq bool.
Show proof.
unfold isdeceq. intros x' x. induction x.
- induction x'.
+ apply (ii1 (idpath true)).
+ apply (ii2 nopathsfalsetotrue).
- induction x'.
+ apply (ii2 nopathstruetofalse).
+ apply (ii1 (idpath false)).
- induction x'.
+ apply (ii1 (idpath true)).
+ apply (ii2 nopathsfalsetotrue).
- induction x'.
+ apply (ii2 nopathstruetofalse).
+ apply (ii1 (idpath false)).
Lemma isdeceqcoprod {A B : UU} (h1 : isdeceq A) (h2 : isdeceq B) :
isdeceq (A ⨿ B).
Show proof.
intros ab ab'.
induction ab as [a|b]; induction ab' as [a'|b'].
- induction (h1 a a') as [p|p].
+ apply inl, (maponpaths (@ii1 A B) p).
+ apply inr; intro H; apply (p (ii1_injectivity _ _ H)).
- apply inr, negpathsii1ii2.
- apply inr, negpathsii2ii1.
- induction (h2 b b') as [p|p].
+ apply inl, (maponpaths (@ii2 A B) p).
+ apply inr; intro H; apply (p (ii2_injectivity _ _ H)).
induction ab as [a|b]; induction ab' as [a'|b'].
- induction (h1 a a') as [p|p].
+ apply inl, (maponpaths (@ii1 A B) p).
+ apply inr; intro H; apply (p (ii1_injectivity _ _ H)).
- apply inr, negpathsii1ii2.
- apply inr, negpathsii2ii1.
- induction (h2 b b') as [p|p].
+ apply inl, (maponpaths (@ii2 A B) p).
+ apply inr; intro H; apply (p (ii2_injectivity _ _ H)).
Definition isisolated (X:UU) (x:X) := ∏ x':X, (x = x') ⨿ (x != x').
Definition isolated ( T : UU ) := ∑ t:T, isisolated _ t.
Definition make_isolated ( T : UU ) (t:T) (i:isisolated _ t) : isolated T
:= (t,,i).
Definition pr1isolated ( T : UU ) (x:isolated T) : T := pr1 x.
Theorem isaproppathsfromisolated (X : UU) (x : X) (is : isisolated X x) :
∏ x', isaprop(x = x').
Show proof.
intros. apply iscontraprop1inv. intro e. induction e.
set (f := λ e : x = x, coconusfromtpair _ e).
assert (is' : isweq f)
by apply (onefiber (λ x' : X, x = x') (x : X) (λ x' : X, is x')).
assert (is2 : iscontr (coconusfromt _ x))
by apply iscontrcoconusfromt.
apply (iscontrweqb (make_weq f is')).
assumption.
set (f := λ e : x = x, coconusfromtpair _ e).
assert (is' : isweq f)
by apply (onefiber (λ x' : X, x = x') (x : X) (λ x' : X, is x')).
assert (is2 : iscontr (coconusfromt _ x))
by apply iscontrcoconusfromt.
apply (iscontrweqb (make_weq f is')).
assumption.
Local Open Scope transport.
Theorem isaproppathstoisolated (X : UU) (x : X) (is : isisolated X x) :
∏ x' : X, isaprop (x' = x).
Show proof.
Lemma isisolatedweqf { X Y : UU } (f : X ≃ Y) (x:X) : isisolated X x -> isisolated Y (f x).
Show proof.
intros is. unfold isisolated. intro y.
induction (is (invmap f y)) as [ eq | ne ].
{ apply ii1. apply pathsweq1'. assumption. }
{ apply ii2. intro eq. apply ne; clear ne. apply pathsweq1. assumption. }
induction (is (invmap f y)) as [ eq | ne ].
{ apply ii1. apply pathsweq1'. assumption. }
{ apply ii2. intro eq. apply ne; clear ne. apply pathsweq1. assumption. }
Theorem isisolatedinclb {X Y : UU} (f : X -> Y) (is : isincl f) (x : X)
(is0 : isisolated _ (f x)) : isisolated _ x.
Show proof.
intros. unfold isisolated. intro x'. set (a := is0 (f x')).
induction a as [ a1 | a2 ]. apply (ii1 (invmaponpathsincl f is _ _ a1)).
apply (ii2 ((negf (@maponpaths _ _ f _ _)) a2)).
induction a as [ a1 | a2 ]. apply (ii1 (invmaponpathsincl f is _ _ a1)).
apply (ii2 ((negf (@maponpaths _ _ f _ _)) a2)).
Lemma disjointl1 (X : UU) : isisolated (coprod X unit) (ii2 tt).
Show proof.
intros. unfold isisolated. intros x'. induction x' as [ x | u ].
apply (ii2 (negpathsii2ii1 x tt)). induction u.
apply (ii1 (idpath _)).
apply (ii2 (negpathsii2ii1 x tt)). induction u.
apply (ii1 (idpath _)).
Lemma isdeceq_total2 {X : UU} {P : X -> UU}
: isdeceq X -> (∏ x : X, isdeceq (P x)) → isdeceq (∑ x : X, P x).
Show proof.
: isdeceq X -> (∏ x : X, isdeceq (P x)) → isdeceq (∑ x : X, P x).
Show proof.
intros HX HP.
intros xp yq.
induction (HX (pr1 xp) (pr1 yq)) as [e_xy | ne_xy].
- induction ((HP _) (transportf _ e_xy (pr2 xp)) (pr2 yq)) as [e_pq | ne_pq].
+ apply inl. exact (total2_paths_f e_xy e_pq).
+ apply inr. intro e_xpyq. apply ne_pq.
set (e_pq := fiber_paths e_xpyq).
refine (_ @ e_pq).
refine (maponpaths (λ e, transportf _ e _) _).
apply isasetifdeceq, HX.
- apply inr. intros e_xypq. apply ne_xy, base_paths, e_xypq.
intros xp yq.
induction (HX (pr1 xp) (pr1 yq)) as [e_xy | ne_xy].
- induction ((HP _) (transportf _ e_xy (pr2 xp)) (pr2 yq)) as [e_pq | ne_pq].
+ apply inl. exact (total2_paths_f e_xy e_pq).
+ apply inr. intro e_xpyq. apply ne_pq.
set (e_pq := fiber_paths e_xpyq).
refine (_ @ e_pq).
refine (maponpaths (λ e, transportf _ e _) _).
apply isasetifdeceq, HX.
- apply inr. intros e_xypq. apply ne_xy, base_paths, e_xypq.
Definition isolfun1 {X Y:UU} (x1:X) (i1 : isisolated _ x1) (y1 y':Y) : X → Y.
Show proof.
intros x.
induction (i1 x).
- exact y1.
- exact y'.
induction (i1 x).
- exact y1.
- exact y'.
Definition decfun1 {X Y:UU} (i : isdeceq X) (x1:X) : ∏ (y1 y':Y), X → Y.
Show proof.
Definition isolfun2 {X Y:UU} (x1 x2:X) (i1 : isisolated _ x1) (i2 : isisolated _ x2) (y1 y2 y':Y) : X → Y.
Show proof.
intros x.
induction (i1 x).
- exact y1.
- induction (i2 x).
+ exact y2.
+ exact y'.
induction (i1 x).
- exact y1.
- induction (i2 x).
+ exact y2.
+ exact y'.
Definition decfun2 {X Y:UU} (i : isdeceq X) (x1 x2:X) (y1 y2 y':Y) : X → Y.
Show proof.
Definition isolfun3 {X Y:UU} (x1 x2 x3:X) (i1 : isisolated _ x1) (i2 : isisolated _ x2) (i3 : isisolated _ x3) (y1 y2 y3 y':Y) : X → Y.
Show proof.
intros x.
induction (i1 x).
- exact y1.
- induction (i2 x).
+ exact y2.
+ induction (i3 x).
* exact y3.
* exact y'.
induction (i1 x).
- exact y1.
- induction (i2 x).
+ exact y2.
+ induction (i3 x).
* exact y3.
* exact y'.
Definition decfun3 {X Y:UU} (i : isdeceq X) (x1 x2 x3:X) (y1 y2 y3 y':Y) : X → Y.
revert y1 y2 y3 y'.
exact (isolfun3 x1 x2 x3 (i x1) (i x2) (i x3)).
Defined.
bool is a set
Definition subsetsplit {X : UU} (f : X -> bool) (x : X) :
(hfiber f true) ⨿ (hfiber f false).
Show proof.
intros. induction (boolchoice (f x)) as [ a | b ].
- apply (ii1 (make_hfiber f x a)).
- apply (ii2 (make_hfiber f x b)).
- apply (ii1 (make_hfiber f x a)).
- apply (ii2 (make_hfiber f x b)).
Definition subsetsplitinv {X : UU} (f : X -> bool)
(ab : (hfiber f true) ⨿ (hfiber f false)) : X
:= match ab with ii1 xt => pr1 xt | ii2 xf => pr1 xf end.
Theorem weqsubsetsplit {X : UU} (f : X -> bool) :
weq X ((hfiber f true) ⨿ (hfiber f false)).
Show proof.
intros.
set (ff := subsetsplit f). set (gg := subsetsplitinv f).
split with ff.
assert (egf : ∏ a : _, paths (gg (ff a)) a).
{
intros. unfold ff. unfold subsetsplit.
induction (boolchoice (f a)) as [ et | ef ]. simpl. apply idpath. simpl.
apply idpath.
}
assert (efg : ∏ a : _, paths (ff (gg a)) a).
{
intros. induction a as [ et | ef ].
- induction et as [ x et' ]. simpl. unfold ff. unfold subsetsplit.
induction (boolchoice (f x)) as [ e1 | e2 ].
+ apply (maponpaths (@ii1 _ _ )). apply (maponpaths (make_hfiber f x)).
apply uip. apply isasetbool.
+ induction (nopathstruetofalse (pathscomp0 (pathsinv0 et') e2)).
- induction ef as [ x et' ]. simpl. unfold ff. unfold subsetsplit.
induction (boolchoice (f x)) as [ e1 | e2 ].
+ induction (nopathsfalsetotrue (pathscomp0 (pathsinv0 et') e1)).
+ apply (maponpaths (@ii2 _ _ )). apply (maponpaths (make_hfiber f x)).
apply uip. apply isasetbool.
}
apply (isweq_iso _ _ egf efg).
set (ff := subsetsplit f). set (gg := subsetsplitinv f).
split with ff.
assert (egf : ∏ a : _, paths (gg (ff a)) a).
{
intros. unfold ff. unfold subsetsplit.
induction (boolchoice (f a)) as [ et | ef ]. simpl. apply idpath. simpl.
apply idpath.
}
assert (efg : ∏ a : _, paths (ff (gg a)) a).
{
intros. induction a as [ et | ef ].
- induction et as [ x et' ]. simpl. unfold ff. unfold subsetsplit.
induction (boolchoice (f x)) as [ e1 | e2 ].
+ apply (maponpaths (@ii1 _ _ )). apply (maponpaths (make_hfiber f x)).
apply uip. apply isasetbool.
+ induction (nopathstruetofalse (pathscomp0 (pathsinv0 et') e2)).
- induction ef as [ x et' ]. simpl. unfold ff. unfold subsetsplit.
induction (boolchoice (f x)) as [ e1 | e2 ].
+ induction (nopathsfalsetotrue (pathscomp0 (pathsinv0 et') e1)).
+ apply (maponpaths (@ii2 _ _ )). apply (maponpaths (make_hfiber f x)).
apply uip. apply isasetbool.
}
apply (isweq_iso _ _ egf efg).