Library uu0

Univalent Basics. Vladimir Voevodsky. Feb. 2010 - Sep. 2011



This file contains results which form a basis of the univalent approach and which do not require the use of universes as types. Fixpoints with values in a universe are used only once in the definition isofhlevel . Many results in this file do not require any axioms. The first axiom we use is funextempty which is the functional extensionality axiom for functions with values in the empty type. Closer to the end of the file we use general functional extensionality funextfunax asserting that two homotopic functions are equal. Since funextfunax itself is not an "axiom" in our sense i.e. its type is not of h-level 1 we show that it is logically equivalent to a real axiom funcontr which asserts that the space of sections of a family with contractible fibers is contractible.


Preambule


Settings

Add Rec LoadPath "../Generalities".

Unset Automatic Introduction.
Imports

Require Export uuu.

Universe structure

Definition UU := Type .


Some standard constructions not using identity types (paths)


Canonical functions from empty and to unit


Definition fromempty { X : UU } : empty -> X.
Proof. intros X H. destruct H. Defined.

Definition tounit { X : UU } : X -> unit := fun x : X => tt .

Functions from unit corresponding to terms


Definition termfun { X : UU } ( x : X ) : unit -> X := fun t : unit => x .

Identity functions and function composition


Definition idfun ( T : UU ) := fun t : T => t .

Definition funcomp { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) := fun x : X => g ( f x ) .

Iteration of an endomorphism


Fixpoint iteration { T : UU } ( f : T -> T ) ( n : nat ) : T -> T := match n with
O => idfun T |
S m => funcomp ( iteration f m ) f
end .

Basic constructions related to the adjoint evaluation function X -> ( ( X -> Y ) -> Y )


Definition adjev { X Y : UU } ( x : X ) ( f : X -> Y ) : Y := f x.

Definition adjev2 { X Y : UU } ( phi : ( ( X -> Y ) -> Y ) -> Y ) : X -> Y := (fun x : X => phi ( fun f : X -> Y => f x ) ) .

Pairwise direct products


Definition dirprod ( X Y : UU ) := total2 ( fun x : X => Y ) .
Definition dirprodpair { X Y : UU } := tpair ( fun x : X => Y ) .

Definition dirprodadj { X Y Z : UU } ( f : dirprod X Y -> Z ) : X -> Y -> Z := fun x : X => fun y : Y => f ( dirprodpair x y ) .

Definition dirprodf { X Y X' Y' : UU } ( f : X -> Y ) ( f' : X' -> Y' ) ( xx' : dirprod X X' ) : dirprod Y Y' := match xx' with tpair x x' => dirprodpair (f x) (f' x') end.

Definition ddualand { X Y P : UU } (xp : ( X -> P ) -> P ) ( yp : ( Y -> P ) -> P ) : ( dirprod X Y -> P ) -> P.
Proof. intros X Y P xp yp X0 . set ( int1 := fun ypp : ( ( Y -> P ) -> P ) => fun x : X => yp ( fun y : Y => X0 ( dirprodpair x y) ) ) . apply ( xp ( int1 yp ) ) . Defined .

Negation and double negation


Definition neg ( X : UU ) : UU := X -> empty.

Definition negf { X Y : UU } ( f : X -> Y ) : neg Y -> neg X := fun phi : Y -> empty => fun x : X => phi ( f x ) .

Definition dneg ( X : UU ) : UU := ( X -> empty ) -> empty .

Definition dnegf { X Y : UU } ( f : X -> Y ) : dneg X -> dneg Y := negf ( negf f ) .

Definition todneg ( X : UU ) : X -> dneg X := adjev .

Definition dnegnegtoneg { X : UU } : dneg ( neg X ) -> neg X := adjev2 .

Lemma dneganddnegl1 { X Y : UU } ( dnx : dneg X ) ( dny : dneg Y ) : neg ( X -> neg Y ) .
Proof. intros. intro X2. assert ( X3 : dneg X -> neg Y ) . apply ( fun xx : dneg X => dnegnegtoneg ( dnegf X2 xx ) ) . apply ( dny ( X3 dnx ) ) . Defined.

Definition dneganddnegimpldneg { X Y : UU } ( dnx : dneg X ) ( dny : dneg Y ) : dneg ( dirprod X Y ) := ddualand dnx dny.


Operations on paths


Composition of paths and inverse paths



Definition pathscomp0 { X : UU } { a b c : X } ( e1 : paths a b ) ( e2 : paths b c ) : paths a c .
Proof. intros. destruct e1. apply e2 . Defined.
Hint Resolve @pathscomp0 : pathshints .

Definition pathscomp0rid { X : UU } { a b : X } ( e1 : paths a b ) : paths ( pathscomp0 e1 ( idpath b ) ) e1 .
Proof. intros. destruct e1. simpl. apply idpath. Defined.

Note that we do no need pathscomp0lid since the corresponding two terms are convertible to each other due to our definition of pathscomp0 . If we defined it by destructing e2 and applying e1 then pathsinv0rid would be trivial but pathsinv0lid would require a proof. Similarly we do not need a lemma to connect pathsinv0 ( idpath _ ) to idpath

Definition pathsinv0 { X : UU } { a b : X } ( e : paths a b ) : paths b a .
Proof. intros. destruct e. apply idpath. Defined.
Hint Resolve @pathsinv0 : pathshints .

Definition pathsinv0l { X : UU } { a b : X } ( e : paths a b ) : paths ( pathscomp0 ( pathsinv0 e ) e ) ( idpath _ ) .
Proof. intros. destruct e. apply idpath. Defined.

Definition pathsinv0r { X : UU } { a b : X } ( e : paths a b ) : paths ( pathscomp0 e ( pathsinv0 e ) ) ( idpath _ ) .
Proof. intros. destruct e. apply idpath. Defined.

Definition pathsinv0inv0 { X : UU } { x x' : X } ( e : paths x x' ) : paths ( pathsinv0 ( pathsinv0 e ) ) e .
Proof. intros. destruct e. apply idpath. Defined.

Direct product of paths


Definition pathsdirprod { X Y : UU } { x1 x2 : X } { y1 y2 : Y } ( ex : paths x1 x2 ) ( ey : paths y1 y2 ) : paths ( dirprodpair x1 y1 ) ( dirprodpair x2 y2 ) .
Proof . intros . destruct ex . destruct ey . apply idpath . Defined .

The function maponpaths between paths types defined by a function between abmbient paths and its behavior relative to pathscomp0 and pathsinv0


Definition maponpaths { T1 T2 : UU } ( f : T1 -> T2 ) { t1 t2 : T1 } ( e: paths t1 t2 ) : paths ( f t1 ) ( f t2 ) .
Proof. intros . destruct e . apply idpath. Defined.

Definition maponpathscomp0 { X Y : UU } { x1 x2 x3 : X } ( f : X -> Y ) ( e1 : paths x1 x2 ) ( e2 : paths x2 x3 ) : paths ( maponpaths f ( pathscomp0 e1 e2 ) ) ( pathscomp0 ( maponpaths f e1 ) ( maponpaths f e2 ) ) .
Proof. intros. destruct e1. destruct e2. simpl. apply idpath. Defined.

Definition maponpathsinv0 { X Y : UU } ( f : X -> Y ) { x1 x2 : X } ( e : paths x1 x2 ) : paths ( maponpaths f ( pathsinv0 e ) ) ( pathsinv0 ( maponpaths f e ) ) .
Proof. intros . destruct e . apply idpath . Defined .

maponpaths for the identity functions and compositions of functions


Lemma maponpathsidfun { X : UU } { x x' : X } ( e : paths x x' ) : paths ( maponpaths ( idfun X ) e ) e .
Proof. intros. destruct e. apply idpath . Defined.

Lemma maponpathscomp { X Y Z : UU } { x x' : X } ( f : X -> Y ) ( g : Y -> Z ) ( e : paths x x' ) : paths ( maponpaths g ( maponpaths f e ) ) ( maponpaths ( funcomp f g ) e) .
Proof. intros. destruct e. apply idpath. Defined.

The following four statements show that maponpaths defined by a function f which is homotopic to the identity is "surjective". It is later used to show that the maponpaths defined by a function which is a weak equivalence is itself a weak equivalence.

Definition maponpathshomidinv { X : UU } (f:X -> X) ( h: forall x:X, paths (f x) x) ( x x' : X ) : paths (f x) (f x') -> paths x x' := (fun e: paths (f x) (f x') => pathscomp0 (pathsinv0 (h x)) (pathscomp0 e (h x'))).

Lemma maponpathshomid1 { X : UU } (f:X -> X) (h: forall x:X, paths (f x) x) { x x' : X } (e:paths x x'): paths (maponpaths f e) (pathscomp0 (h x) (pathscomp0 e (pathsinv0 (h x')))).
Proof. intros. destruct e. change (pathscomp0 (idpath x) (pathsinv0 (h x))) with (pathsinv0 (h x)). assert (ee: paths (maponpaths f (idpath x)) (idpath (f x))). apply idpath .
assert (eee: paths (idpath (f x)) (pathscomp0 (h x) (pathsinv0 (h x)))). apply (pathsinv0 (pathsinv0r (h x))). apply (pathscomp0 ee eee). Defined.

Lemma maponpathshomid12 { X : UU } { x x' fx fx' : X } (e:paths fx fx') (hx:paths fx x) (hx':paths fx' x') : paths (pathscomp0 hx (pathscomp0 (pathscomp0 (pathsinv0 hx) (pathscomp0 e hx')) (pathsinv0 hx'))) e.
Proof. intros. destruct hx. destruct hx'. destruct e. simpl. apply idpath. Defined.

Lemma maponpathshomid2 { X : UU } (f:X->X) (h: forall x:X, paths (f x) x) ( x x' : X ) (e:paths (f x) (f x')) : paths (maponpaths f (maponpathshomidinv f h _ _ e)) e.
Proof. intros. assert (ee: paths (pathscomp0 (h x) (pathscomp0 (pathscomp0 (pathsinv0 (h x)) (pathscomp0 e (h x'))) (pathsinv0 (h x')))) e). apply (maponpathshomid12 e (h x) (h x')). assert (eee: paths (maponpaths f (pathscomp0 (pathsinv0 (h x)) (pathscomp0 e (h x')))) (pathscomp0 (h x) (pathscomp0 (pathscomp0 (pathsinv0 (h x)) (pathscomp0 e (h x'))) (pathsinv0 (h x'))))). apply maponpathshomid1. apply (pathscomp0 eee ee). Defined.

Here we consider the behavior of maponpaths in the case of a projection p with a section s .

Definition pathssec1 { X Y : UU } ( s : X -> Y ) ( p : Y -> X ) ( eps : forall x:X , paths ( p ( s x ) ) x ) ( x : X ) ( y : Y ) ( e : paths (s x) y ) : paths x (p y) := pathscomp0 ( pathsinv0 ( eps x ) ) ( maponpaths p e ) .

Definition pathssec2 { X Y : UU } ( s : X -> Y ) ( p : Y -> X ) ( eps : forall x : X , paths ( p ( s x ) ) x ) ( x x' : X ) ( e : paths ( s x ) ( s x' ) ) : paths x x'.
Proof. intros . set ( e' := pathssec1 s p eps _ _ e ) . apply ( pathscomp0 e' ( eps x' ) ) . Defined .

Definition pathssec2id { X Y : UU } ( s : X -> Y ) ( p : Y -> X ) ( eps : forall x : X , paths ( p ( s x ) ) x ) ( x : X ) : paths ( pathssec2 s p eps _ _ ( idpath ( s x ) ) ) ( idpath x ) .
Proof. intros. unfold pathssec2. unfold pathssec1. simpl. assert (e: paths (pathscomp0 (pathsinv0 (eps x)) (idpath (p (s x)))) (pathsinv0 (eps x))). apply pathscomp0rid. assert (ee: paths
(pathscomp0 (pathscomp0 (pathsinv0 (eps x)) (idpath (p (s x)))) (eps x))
(pathscomp0 (pathsinv0 (eps x)) (eps x))).
apply (maponpaths (fun e0: _ => pathscomp0 e0 (eps x)) e). assert (eee: paths (pathscomp0 (pathsinv0 (eps x)) (eps x)) (idpath x)). apply (pathsinv0l (eps x)). apply (pathscomp0 ee eee). Defined.

Definition pathssec3 { X Y : UU } (s:X-> Y) (p:Y->X) (eps: forall x:X, paths (p (s x)) x) { x x' : X } ( e : paths x x' ) : paths (pathssec2 s p eps _ _ (maponpaths s e)) e.
Proof. intros. destruct e. simpl. unfold pathssec2. unfold pathssec1. simpl. apply pathssec2id. Defined.


Fibrations and paths


Definition tppr { T : UU } { P : T -> UU } ( x : total2 P ) : paths x ( tpair _ (pr21 x) (pr22 x) ) .
Proof. intros. destruct x. apply idpath. Defined.

Definition constr1 { X : UU } ( P : X -> UU ) { x x' : X } ( e : paths x x' ) : total2 (fun f: P x -> P x' => ( total2 ( fun ee : forall p : P x, paths (tpair _ x p) (tpair _ x' ( f p ) ) => forall pp : P x, paths (maponpaths ( @pr21 _ _ ) ( ee pp ) ) e ) ) ) .
Proof. intros. destruct e. split with ( idfun ( P x ) ). simpl. split with (fun p : P x => idpath _ ) . unfold maponpaths. simpl. apply (fun pp : P x => idpath _ ) . Defined.

Definition transportf { X : UU } ( P : X -> UU ) { x x' : X } ( e : paths x x' ) : P x -> P x' := pr21 ( constr1 P e ) .

Definition transportb { X : UU } ( P : X -> UU ) { x x' : X } ( e : paths x x' ) : P x' -> P x := transportf P ( pathsinv0 e ) .

Lemma functtransportf { X Y : UU } ( f : X -> Y ) ( P : Y -> UU ) { x x' : X } ( e : paths x x' ) ( p : P ( f x ) ) : paths ( transportf ( funcomp f P ) e p ) ( transportf P ( maponpaths f e ) p ) .
Proof. intros. destruct e. apply idpath. Defined.

First homotopy notions


Homotopy between functions


Definition homot { X Y : UU } ( f g : X -> Y ) := forall x : X , paths ( f x ) ( g x ) .

Contractibility, homotopy fibers etc.


Contractible types.

Definition iscontr (T:UU) : UU := total2 (fun cntr:T => forall t:T, paths t cntr).
Definition iscontrpair { T : UU } := tpair (fun cntr:T => forall t:T, paths t cntr).
Definition iscontrpr21 { T : UU } := @pr21 T ( fun cntr:T => forall t:T, paths t cntr ) .

Lemma iscontrretract { X Y : UU } ( p : X -> Y ) ( s : Y -> X ) ( eps : forall y : Y, paths ( p ( s y ) ) y ) ( is : iscontr X ) : iscontr Y.
Proof . intros . destruct is as [ x fe ] . set ( y := p x ) . split with y . intro y' . apply ( pathscomp0 ( pathsinv0 ( eps y' ) ) ( maponpaths p ( fe ( s y' ) ) ) ) . Defined .

Lemma proofirrelevancecontr { X : UU }(is: iscontr X) ( x x' : X ): paths x x'.
Proof. intros. unfold iscontr in is. destruct is as [ t x0 ]. set (e:= x0 x). set (e':= pathsinv0 (x0 x')). apply (pathscomp0 e e'). Defined.

Coconuses - spaces of paths which begin or end at a given point.

Definition coconustot ( T : UU ) ( t : T ) := total2 (fun t':T => paths t' t).
Definition coconustotpair ( T : UU ) { t t' : T } (e: paths t' t) : coconustot T t := tpair (fun t':T => paths t' t) t' e.
Definition coconustotpr21 ( T : UU ) ( t : T ) := @pr21 _ (fun t':T => paths t' t) .

Lemma connectedcoconustot { T : UU } { t : T } ( c1 c2 : coconustot T t ) : paths c1 c2.
Proof. intros. destruct c1 as [ x0 x ]. destruct x. destruct c2 as [ x1 x ]. destruct x. apply idpath. Defined.

Lemma iscontrcoconustot ( T : UU ) (t:T) : iscontr (coconustot T t).
Proof. intros. unfold iscontr. set (t0:= tpair (fun t':T => paths t' t) t (idpath t)). split with t0. intros. apply connectedcoconustot. Defined.

Definition coconusfromt ( T : UU ) (t:T) := total2 (fun t':T => paths t t').
Definition coconusfromtpair ( T : UU ) { t t' : T } (e: paths t t') : coconusfromt T t := tpair (fun t':T => paths t t') t' e.
Definition coconusfromtpr21 ( T : UU ) ( t : T ) := @pr21 _ (fun t':T => paths t t') .

Lemma connectedcoconusfromt { T : UU } { t : T } ( e1 e2 : coconusfromt T t ) : paths e1 e2.
Proof. intros. destruct e1 as [x0 x]. destruct x. destruct e2 as [ x1 x ]. destruct x. apply idpath. Defined.

Lemma iscontrcoconusfromt ( T : UU ) (t:T) : iscontr (coconusfromt T t).
Proof. intros. unfold iscontr. set (t0:= tpair (fun t':T => paths t t') t (idpath t)). split with t0. intros. apply connectedcoconusfromt. Defined.

Pathsspace of a type.

Definition pathsspace (T:UU) := total2 (fun t:T => coconusfromt T t).
Definition pathsspacetriple ( T : UU ) { t1 t2 : T } (e: paths t1 t2): pathsspace T := tpair _ t1 (coconusfromtpair T e).

Definition deltap ( T : UU ) : T -> pathsspace T := (fun t:T => pathsspacetriple T (idpath t)).

Definition pathsspace' ( T : UU ) := total2 (fun xy : dirprod T T => (match xy with tpair x y => paths x y end)).

Homotopy fibers.

Definition hfiber { X Y : UU } (f:X -> Y) (y:Y) : UU := total2 (fun pointover:X => paths (f pointover) y).
Definition hfiberpair { X Y : UU } (f:X -> Y) { y : Y } ( x : X ) ( e : paths ( f x ) y ) := tpair (fun pointover:X => paths (f pointover) y) x e .
Definition hfiberpr21 { X Y : UU } ( f : X -> Y ) ( y : Y ) := @pr21 _ (fun pointover:X => paths (f pointover) y) .

Paths in homotopy fibers.

Lemma hfibertriangle1 { X Y : UU } (f:X -> Y) { y : Y } { xe1 xe2: hfiber f y } (e: paths xe1 xe2): paths (pr22 xe1) (pathscomp0 (maponpaths f (maponpaths ( @pr21 _ _ ) e)) (pr22 xe2)).
Proof. intros. destruct e. simpl. apply idpath. Defined.

Lemma hfibertriangle1inv0 { X Y : UU } (f:X -> Y) { y : Y } { xe1 xe2: hfiber f y } (e: paths xe1 xe2) : paths ( pathscomp0 ( maponpaths f ( pathsinv0 ( maponpaths ( @pr21 _ _ ) e ) ) ) ( pr22 xe1 ) ) ( pr22 xe2 ) .
Proof . intros . destruct e . apply idpath . Defined .

Lemma hfibertriangle2 { X Y : UU } (f:X -> Y) { y : Y } (xe1 xe2: hfiber f y) (ee: paths (pr21 xe1) (pr21 xe2))(eee: paths (pr22 xe1) (pathscomp0 (maponpaths f ee) (pr22 xe2))): paths xe1 xe2.
Proof. intros. destruct xe1 as [ t e1 ]. destruct xe2. simpl in eee. simpl in ee. destruct ee. simpl in eee. apply (maponpaths (fun e: paths (f t) y => hfiberpair f t e) eee). Defined.

Coconus of a function - the total space of the family of h-fibers.

Definition coconusf { X Y : UU } (f: X -> Y):= total2 (fun y:_ => hfiber f y).
Definition fromcoconusf { X Y : UU } (f: X -> Y) : coconusf f -> X := fun yxe:_ => pr21 (pr22 yxe).
Definition tococonusf { X Y:UU } (f: X -> Y) : X -> coconusf f := fun x:_ => tpair _ (f x) (hfiberpair f x (idpath _ ) ).

Weak equivalences


Basics


Definition isweq { X Y : UU } ( f : X -> Y) : UU := forall y:Y, iscontr (hfiber f y) .

Lemma idisweq (T:UU) : isweq (fun t:T => t).
Proof. intros.
unfold isweq.
intro y .
assert (y0: hfiber (fun t : T => t) y). apply (tpair (fun pointover:T => paths ((fun t:T => t) pointover) y) y (idpath y)).
split with y0. intro t.
destruct y0 as [x0 e0]. destruct t as [x1 e1]. destruct e0. destruct e1. apply idpath. Defined.

Definition weq ( X Y : UU ) : UU := total2 (fun f:X->Y => isweq f) .
Definition pr21weq ( X Y : UU):= @pr21 _ _ : weq X Y -> (X -> Y).
Coercion pr21weq : weq >-> Funclass.
Definition weqpair { X Y : UU } (f:X-> Y) (is: isweq f) : weq X Y := tpair (fun f:X->Y => isweq f) f is.
Definition idweq (X:UU) : weq X X := tpair (fun f:X->X => isweq f) (fun x:X => x) ( idisweq X ) .

Definition isweqtoempty { X : UU } (f : X -> empty ) : isweq f.
Proof. intros. intro y. apply (fromempty y). Defined.

Definition weqtoempty { X : UU } ( f : X -> empty ) := weqpair _ ( isweqtoempty f ) .

Lemma isweqtoempty2 { X Y : UU } ( f : X -> Y ) ( is : neg Y ) : isweq f .
Proof. intros . intro y . destruct ( is y ) . Defined .

Definition weqtoempty2 { X Y : UU } ( f : X -> Y ) ( is : neg Y ) := weqpair _ ( isweqtoempty2 f is ) .

Definition invmap { X Y : UU } ( w : weq X Y ) : Y -> X .
Proof. intros X Y w y . apply (pr21 (pr21 ( pr22 w y ))). Defined.

We now define different homotopies and maps between the paths spaces corresponding to a weak equivalence. What may look like unnecessary complexity in the definition of weqgf is due to the fact that the "naive" definition, that of weqgf00 , needs to be corrected in order for lemma weqfgf to hold.

Definition homotweqinvweq { T1 T2 : UU } ( w : weq T1 T2 ) : forall t2:T2, paths ( w ( invmap w t2 ) ) t2.
Proof. intros. unfold invmap. simpl. apply (pr22 (pr21 ( pr22 w t2 ) ) ) . Defined.

Definition homotinvweqweq0 { X Y : UU } ( w : weq X Y ) ( x : X ) : paths x ( invmap w ( w x ) ) .
Proof. intros. set (isfx:= ( pr22 w ( w x ) ) ). set (pr21fx:= @pr21 X (fun x':X => paths ( w x' ) ( w x ))).
set (xe1:= (hfiberpair w x (idpath ( w x)))). apply (maponpaths pr21fx (pr22 isfx xe1)). Defined.

Definition homotinvweqweq { X Y : UU } ( w : weq X Y ) ( x : X ) : paths (invmap w ( w x ) ) x := pathsinv0 (homotinvweqweq0 w x).

Lemma diaglemma2 { X Y : UU } (f:X -> Y) { x x':X } (e1: paths x x')(e2: paths (f x') (f x)) (ee: paths (idpath (f x)) (pathscomp0 (maponpaths f e1) e2)): paths (maponpaths f (pathsinv0 e1)) e2.
Proof. intros. destruct e1. simpl. simpl in ee. assumption. Defined.

Definition homotweqinvweqweq { X Y : UU } ( w : weq X Y ) ( x : X ) : paths (maponpaths w (homotinvweqweq w x)) (homotweqinvweq w ( w x)).
Proof. intros. set (xe1:= hfiberpair w x (idpath (w x))). set (isfx:= ( pr22 w ) (w x)). set (xe2:= pr21 isfx). set (e:= pr22 isfx xe1). set (ee:=hfibertriangle1 w e). simpl in ee.
apply (diaglemma2 w (homotinvweqweq0 w x) ( homotweqinvweq w ( w x ) ) ee ). Defined.

Definition invmaponpathsweq { X Y : UU } ( w : weq X Y ) ( x x' : X ) : paths (w x) (w x') -> paths x x':= pathssec2 w (invmap w ) (homotinvweqweq w ) _ _ .

Definition invmaponpathsweqid { X Y : UU } ( w : weq X Y ) ( x : X ) : paths (invmaponpathsweq w _ _ (idpath (w x))) (idpath x):= pathssec2id w (invmap w ) (homotinvweqweq w ) x.

Definition pathsweq1 { X Y : UU } ( w : weq X Y ) ( x : X ) ( y : Y ) : paths (w x) y -> paths x (invmap w y) := pathssec1 w (invmap w ) (homotinvweqweq w ) _ _ .

Definition pathsweq1' { X Y : UU } ( w : weq X Y ) ( x : X ) ( y : Y ) : paths x (invmap w y) -> paths ( w x ) y := fun e:_ => pathscomp0 (maponpaths w e) (homotweqinvweq w y).

Definition pathsweq3 { X Y : UU } ( w : weq X Y ) { x x' : X } ( e : paths x x' ) : paths (invmaponpathsweq w x x' (maponpaths w e)) e:= pathssec3 w (invmap w ) (homotinvweqweq w ) _ .

Definition pathsweq4 { X Y : UU } ( w : weq X Y ) ( x x' : X ) ( e : paths ( w x ) ( w x' )) : paths (maponpaths w (invmaponpathsweq w x x' e)) e.
Proof. intros. destruct w as [ f is1 ] . set ( w := weqpair f is1 ) . set (g:=invmap w ). set (gf:= fun x:X => (g (f x))). set (ee:= maponpaths g e). set (eee:= maponpathshomidinv gf (homotinvweqweq w ) x x' ee ).
assert (e1: paths (maponpaths f eee) e).
assert (e2: paths (maponpaths g (maponpaths f eee)) (maponpaths g e)).
assert (e3: paths (maponpaths g (maponpaths f eee)) (maponpaths gf eee)). apply maponpathscomp.
assert (e4: paths (maponpaths gf eee) ee). apply maponpathshomid2. apply (pathscomp0 e3 e4).
set (s:= @maponpaths _ _ g (f x) (f x')). set (p:= @pathssec2 _ _ g f (homotweqinvweq w ) (f x) (f x')). set (eps:= @pathssec3 _ _ g f (homotweqinvweq w ) (f x) (f x')). apply (pathssec2 s p eps _ _ e2 ).
assert (e5: paths (maponpaths f (invmaponpathsweq w x x' e)) (maponpaths f (invmaponpathsweq w x x' (maponpaths f eee)))). apply (pathsinv0 (maponpaths (fun e0: paths (f x) (f x') => (maponpaths f (invmaponpathsweq w x x' e0))) e1)).
assert (X0: paths (invmaponpathsweq w x x' (maponpaths f eee)) eee). apply (pathsweq3 w ).
assert (e6: paths (maponpaths f (invmaponpathsweq w x x' (maponpaths f eee))) (maponpaths f eee)). apply (maponpaths (fun eee0: paths x x' => maponpaths f eee0) X0). set (e7:= pathscomp0 e5 e6). set (pathscomp0 e7 e1).
assumption. Defined.

Weak equivalences between contractible types (other implications are proved below)


Lemma iscontrweqb { X Y : UU } ( w : weq X Y ) ( is : iscontr Y ) : iscontr X.
Proof. intros . apply ( iscontrretract (invmap w ) w (homotinvweqweq w ) is ). Defined.

Functions between fibers defined by a path on the base are weak equivalences


Lemma isweqtransportf { X : UU } (P:X -> UU) { x x' : X } (e:paths x x'): isweq (transportf P e).
Proof. intros. destruct e. apply idisweq. Defined.

Lemma isweqtransportb { X : UU } (P:X -> UU) { x x' : X } (e:paths x x'): isweq (transportb P e).
Proof. intros. apply (isweqtransportf _ (pathsinv0 e)). Defined.

unit and contractibility


unit is contractible (recall that tt is the name of the canonical term of the type unit ).

Lemma unitl0: paths tt tt -> coconustot _ tt.
Proof. intros X. apply (coconustotpair _ X). Defined.

Lemma unitl1: coconustot _ tt -> paths tt tt.
Proof. intro X. destruct X as [ x t ]. destruct x. assumption. Defined.

Lemma unitl2: forall e: paths tt tt, paths (unitl1 (unitl0 e)) e.
Proof. intros. unfold unitl0. simpl. apply idpath. Defined.

Lemma unitl3: forall e:paths tt tt, paths e (idpath tt).
Proof. intros.
assert (e0: paths (unitl0 (idpath tt)) (unitl0 e)). eapply connectedcoconustot.
assert (e1:paths (unitl1 (unitl0 (idpath tt))) (unitl1 (unitl0 e))). apply (maponpaths unitl1 e0).
assert (e2: paths (unitl1 (unitl0 e)) e). eapply unitl2.
assert (e3: paths (unitl1 (unitl0 (idpath tt))) (idpath tt)). eapply unitl2.
 destruct e1. clear e0. destruct e2. assumption. Defined.

Theorem iscontrunit: iscontr (unit).
Proof. assert (pp:forall x:unit, paths x tt). intros. destruct x. apply (idpath _).
apply (tpair (fun cntr:unit => forall t:unit, paths t cntr) tt pp). Defined.

paths in unit are contractible.

Theorem iscontrpathsinunit ( x x' : unit ) : iscontr ( paths x x' ) .
Proof. intros . assert (c:paths x x'). destruct x. destruct x'. apply idpath.
assert (X: forall g:paths x x', paths g c). intro. assert (e:paths c c). apply idpath. destruct c. destruct x. apply unitl3. apply (iscontrpair c X). Defined.

A type T : UU is contractible if and only if T -> unit is a weak equivalence.

Lemma ifcontrthenunitl0 ( e1 e2 : paths tt tt ) : paths e1 e2.
Proof. intros. assert (e3: paths e1 (idpath tt) ). apply unitl3.
assert (e4: paths e2 (idpath tt)). apply unitl3. destruct e3. destruct e4. apply idpath. Defined.

Lemma isweqcontrtounit { T : UU } (is : iscontr T) : (isweq (fun t:T => tt)).
Proof. intros T X. unfold isweq. intro y. destruct y.
assert (c: hfiber (fun x:T => tt) tt). destruct X as [ t x0 ]. eapply (hfiberpair _ t (idpath tt)).
assert (e: forall d: (hfiber (fun x:T => tt) tt), paths d c). intros. destruct c as [ t x] . destruct d as [ t0 x0 ].
assert (e': paths x x0). apply ifcontrthenunitl0 .
assert (e'': paths t t0). destruct X as [t1 x1 ].
assert (e''': paths t t1). apply x1.
assert (e'''': paths t0 t1). apply x1.
destruct e''''. assumption.
destruct e''. destruct e'. apply idpath. apply (iscontrpair c e). Defined.

Definition weqcontrtounit { T : UU } ( is : iscontr T ) := weqpair _ ( isweqcontrtounit is ) .

Theorem iscontrifweqtounit { X : UU } ( w : weq X unit ) : iscontr X.
Proof. intros X X0. apply (iscontrweqb X0 ). apply iscontrunit. Defined.

A homotopy equivalence is a weak equivalence


Definition hfibersgftog { X Y Z : UU } (f:X -> Y) (g: Y -> Z) (z:Z) ( xe : hfiber (fun x:X => g(f x)) z ) : hfiber g z := hfiberpair g ( f ( pr21 xe ) ) ( pr22 xe ) .

Lemma constr2 { X Y : UU } (f:X -> Y)(g: Y-> X) (efg: forall y:Y, paths (f(g y)) y) ( x0 : X) ( z0 : hfiber g x0 ) : total2 (fun z': hfiber (fun x:X => g (f x)) x0 => paths z0 (hfibersgftog f g x0 z')).
Proof. intros. destruct z0 as [ y e ].

assert (eint: paths y (f x0 )). assert (e0: paths (f(g y)) y). apply efg. assert (e1: paths (f(g y)) (f x0 )). apply (maponpaths f e). destruct e1. apply pathsinv0. assumption.

set (int1:=constr1 (fun y:Y => paths (g y) x0 ) eint). destruct int1 as [ t x ].
set (int2:=hfiberpair (fun x0 : X => g (f x0)) x0 (t e)). split with int2. apply x. Defined.

Lemma iscontrhfiberl1 { X Y : UU } (f:X -> Y) (g: Y-> X) (efg: forall y:Y, paths (f(g y)) y) (x0 : X): iscontr (hfiber (fun x:X => g (f x)) x0 ) ->iscontr (hfiber g x0).
Proof. intros X Y f g efg x0 X0. set (X1:= hfiber (fun x:X => g(f x)) x0 ). set (Y1:= hfiber g x0 ). set (f1:= hfibersgftog f g x0 ). set (g1:= fun z0:_ => pr21 (constr2 f g efg x0 z0)).
set (efg1:= (fun y1:Y1 => pathsinv0 ( pr22 (constr2 f g efg x0 y1 ) ) ) ) . simpl in efg1. apply ( iscontrretract f1 g1 efg1). assumption. Defined.

Lemma iscontrhfiberl2 { X Y : UU } ( f1 f2 : X-> Y) (h: forall x:X, paths (f2 x) (f1 x)) (y:Y): iscontr (hfiber f2 y) -> iscontr (hfiber f1 y).
Proof. intros X Y f1 f2 h y X0.

set (f:= (fun z:(hfiber f1 y) =>
match z with
(tpair x e) => hfiberpair f2 x (pathscomp0 (h x) e)
end)).

set (g:= (fun z:(hfiber f2 y) =>
match z with
(tpair x e) => hfiberpair f1 x (pathscomp0 (pathsinv0 (h x)) e)
end)).

assert (egf: forall z:(hfiber f1 y), paths (g (f z)) z). intros. destruct z as [ x e ]. simpl . apply ( hfibertriangle2 _ (hfiberpair f1 x (pathscomp0 (pathsinv0 (h x)) (pathscomp0 (h x) e))) ( hfiberpair f1 x e ) ( idpath x ) ) . simpl . destruct e . destruct ( h x ) . apply idpath .

apply ( iscontrretract g f egf X0). Defined.

Corollary isweqhomot { X Y : UU } ( f1 f2 : X-> Y ) (h: forall x:X, paths (f1 x) (f2 x)): isweq f1 -> isweq f2.
Proof. intros X Y f1 f2 h X0. unfold isweq. intro y. set (Y0:= X0 y). apply (iscontrhfiberl2 f2 f1 h). assumption. Defined.

Theorem gradth { X Y : UU } (f:X->Y) (g:Y->X) (egf: forall x:X, paths (g (f x)) x) (efg: forall y:Y, paths (f (g y)) y ): isweq f.
Proof. intros. unfold isweq. intro z.
assert (iscontr (hfiber (fun y:Y => (f (g y))) z)).
assert (efg': forall y:Y, paths y (f (g y))). intros. set (e1:= efg y). apply pathsinv0. assumption.
apply (iscontrhfiberl2 (fun y:Y => (f (g y))) (fun y:Y => y) efg' z (idisweq Y z)).
apply (iscontrhfiberl1 g f egf z). assumption.
Defined.

Definition weqgradth { X Y : UU } (f:X->Y) (g:Y->X) (egf: forall x:X, paths (g (f x)) x) (efg: forall y:Y, paths (f (g y)) y ) : weq X Y := weqpair _ ( gradth _ _ egf efg ) .

Some basic weak equivalences


Corollary isweqinvmap { X Y : UU } ( w : weq X Y ) : isweq (invmap w ).
Proof. intros. set (invf:= invmap w ). assert (efinvf: forall y:Y, paths ( w (invf y)) y). apply homotweqinvweq.
assert (einvff: forall x:X, paths (invf ( w x)) x). apply homotinvweqweq. apply ( weqgradth _ _ efinvf einvff ) . Defined.

Definition invweq { X Y : UU } ( w : weq X Y ) : weq Y X := weqpair (invmap w ) (isweqinvmap w ).

Corollary invinv { X Y :UU } ( w : weq X Y ) ( x : X ) : paths ( invweq ( invweq w ) x) (w x).
Proof. intros. unfold invweq . unfold invmap . simpl . apply idpath . Defined .

Corollary iscontrweqf { X Y : UU } ( w : weq X Y ) : iscontr X -> iscontr Y.
Proof. intros X Y w X0 . apply (iscontrweqb ( invweq w ) ). assumption. Defined.

The standard weak equivalence from unit to a contractible type

Definition wequnittocontr { X : UU } ( is : iscontr X ) : weq unit X .
Proof . intros . set ( f := fun t : unit => pr21 is ) . set ( g := fun x : X => tt ) . split with f .
assert ( egf : forall a : _ , paths ( g ( f a )) a ) . intro . destruct a . apply idpath .
assert ( efg : forall a : _ , paths ( f ( g a ) ) a ) . intro . simpl . apply ( pathsinv0 ( pr22 is a ) ) .
apply ( gradth _ _ egf efg ) . Defined .

A weak equivalence bwteen types defines weak equivalences on the corresponding paths types.

Corollary isweqmaponpaths { X Y : UU } ( w : weq X Y ) ( x x' : X ) : isweq (@maponpaths _ _ w x x').
Proof. intros. apply (gradth (@maponpaths _ _ w x x') (@invmaponpathsweq _ _ w x x') (@pathsweq3 _ _ w x x') (@pathsweq4 _ _ w x x')). Defined.

Definition weqonpaths { X Y : UU } ( w : weq X Y ) ( x x' : X ) := weqpair _ ( isweqmaponpaths w x x' ) .

Corollary isweqpathsinv0 { X : UU } (x x':X): isweq (@pathsinv0 _ x x').
Proof. intros. apply (gradth (@pathsinv0 _ x x') (@pathsinv0 _ x' x) (@pathsinv0inv0 _ _ _ ) (@pathsinv0inv0 _ _ _ )). Defined.

Definition weqpathsinv0 { X : UU } ( x x' : X ) := weqpair _ ( isweqpathsinv0 x x' ) .

Corollary isweqpathscomp0r { X : UU } (x : X ) { x' x'' : X } (e': paths x' x''): isweq (fun e:paths x x' => pathscomp0 e e').
Proof. intros. set (f:= fun e:paths x x' => pathscomp0 e e'). set (g:= fun e'': paths x x'' => pathscomp0 e'' (pathsinv0 e')).
assert (egf: forall e:_ , paths (g (f e)) e). intro. destruct e. simpl. destruct e'. simpl. apply idpath.
assert (efg: forall e'':_, paths (f (g e'')) e''). intro. destruct e''. simpl. destruct e'. simpl. apply idpath.
apply (gradth f g egf efg). Defined.

Corollary isweqtococonusf { X Y : UU } (f:X-> Y): isweq ( tococonusf f) .
Proof . intros. set (ff:= fromcoconusf f). set (gg:= tococonusf f).
assert (egf: forall yxe:_, paths (gg (ff yxe)) yxe). intro. destruct yxe as [t x]. destruct x as [ x e ]. unfold gg. unfold tococonusf. unfold ff. unfold fromcoconusf. simpl. destruct e. apply idpath.
assert (efg: forall x:_, paths (ff (gg x)) x). intro. apply idpath.
apply (gradth _ _ efg egf ). Defined.

Definition weqtococonusf { X Y : UU } ( f : X -> Y ) : weq X ( coconusf f ) := weqpair _ ( isweqtococonusf f ) .

Corollary isweqfromcoconusf { X Y : UU } (f:X-> Y): isweq (fromcoconusf f).
Proof. intros. set (ff:= fromcoconusf f). set (gg:= tococonusf f).
assert (egf: forall yxe:_, paths (gg (ff yxe)) yxe). intro. destruct yxe as [t x]. destruct x as [ x e ]. unfold gg. unfold tococonusf. unfold ff. unfold fromcoconusf. simpl. destruct e. apply idpath.
assert (efg: forall x:_, paths (ff (gg x)) x). intro. apply idpath.
apply (gradth _ _ egf efg). Defined.

Definition weqfromcoconusf { X Y : UU } ( f : X -> Y ) : weq ( coconusf f ) X := weqpair _ ( isweqfromcoconusf f ) .

Corollary isweqdeltap (T:UU) : isweq (deltap T).
Proof. intros. set (ff:=deltap T). set (gg:= fun z:pathsspace T => pr21 z).
assert (egf: forall t:T, paths (gg (ff t)) t). intro. apply idpath.
assert (efg: forall tte: pathsspace T, paths (ff (gg tte)) tte). intro. destruct tte as [ t x ]. destruct x as [ x0 e ]. destruct e. apply idpath.
apply (gradth _ _ egf efg). Defined.

Corollary isweqpr21pr21 (T:UU) : isweq (fun a: pathsspace' T => (pr21 (pr21 a))).
Proof. intros. set (f:= (fun a:_ => (pr21 (pr21 a))): pathsspace' T -> T). set (g:= (fun t:T => tpair _ (dirprodpair t t) (idpath t)): T -> pathsspace' T).
assert (efg: forall t:T, paths (f (g t)) t). intro. apply idpath.
assert (egf: forall a: pathsspace' T, paths (g (f a)) a). intro. destruct a as [ t x ]. destruct t. destruct x. simpl. apply idpath.
apply (gradth _ _ egf efg). Defined.

Lemma hfibershomotftog { X Y : UU } ( f g : X -> Y ) ( h : forall x : X , paths ( f x ) ( g x ) ) ( y : Y ) : hfiber f y -> hfiber g y .
Proof. intros X Y f g h y xe . destruct xe as [ x e ] . split with x . apply ( pathscomp0 ( pathsinv0 ( h x ) ) e ) . Defined .

Lemma hfibershomotgtof { X Y : UU } ( f g : X -> Y ) ( h : forall x : X , paths ( f x ) ( g x ) ) ( y : Y ) : hfiber g y -> hfiber f y .
Proof. intros X Y f g h y xe . destruct xe as [ x e ] . split with x . apply ( pathscomp0 ( h x ) e ) . Defined .

Theorem weqhfibershomot { X Y : UU } ( f g : X -> Y ) ( h : forall x : X , paths ( f x ) ( g x ) ) ( y : Y ) : weq ( hfiber f y ) ( hfiber g y ) .
Proof . intros . set ( ff := hfibershomotftog f g h y ) . set ( gg := hfibershomotgtof f g h y ) . split with ff .
assert ( effgg : forall xe : _ , paths ( ff ( gg xe ) ) xe ) . intro . destruct xe as [ x e ] . simpl .
assert ( eee: paths ( pathscomp0 (pathsinv0 (h x)) (pathscomp0 (h x) e) ) (pathscomp0 (maponpaths g ( idpath x ) ) e ) ) . simpl . destruct e . destruct ( h x ) . simpl . apply idpath .
set ( xe1 := hfiberpair g x ( pathscomp0 (pathsinv0 (h x)) (pathscomp0 (h x) e) ) ) . set ( xe2 := hfiberpair g x e ) . apply ( hfibertriangle2 g xe1 xe2 ( idpath x ) eee ) .
assert ( eggff : forall xe : _ , paths ( gg ( ff xe ) ) xe ) . intro . destruct xe as [ x e ] . simpl .
assert ( eee: paths ( pathscomp0 (h x) (pathscomp0 (pathsinv0 (h x)) e) ) (pathscomp0 (maponpaths f ( idpath x ) ) e ) ) . simpl . destruct e . destruct ( h x ) . simpl . apply idpath .
set ( xe1 := hfiberpair f x ( pathscomp0 (h x) (pathscomp0 (pathsinv0 (h x)) e) ) ) . set ( xe2 := hfiberpair f x e ) . apply ( hfibertriangle2 f xe1 xe2 ( idpath x ) eee ) .
apply ( gradth _ _ eggff effgg ) . Defined .

The 2-out-of-3 property of weak equivalences.



Theorems showing that if any two of three functions f, g, gf are weak equivalences then so is the third - the 2-out-of-3 property.

Theorem twooutof3a { X Y Z : UU } (f:X->Y) (g:Y->Z) (isgf: isweq (fun x:X => g (f x))) (isg: isweq g) : isweq f.
Proof. intros. set ( gw := weqpair g isg ) . set ( gfw := weqpair _ isgf ) . set (invg:= invmap gw ). set (invgf:= invmap gfw ). set (invf := (fun y:Y => invgf (g y))).

assert (efinvf: forall y:Y, paths (f (invf y)) y). intro. assert (int1: paths (g (f (invf y))) (g y)). unfold invf. apply (homotweqinvweq gfw ( g y ) ). apply (invmaponpathsweq gw _ _ int1).

assert (einvff: forall x: X, paths (invf (f x)) x). intro. unfold invf. apply (homotinvweqweq gfw x).

apply (gradth f invf einvff efinvf). Defined.

Corollary isweqcontrcontr { X Y : UU } (f:X -> Y) (isx: iscontr X) (isy: iscontr Y): isweq f.
Proof. intros. set (py:= (fun y:Y => tt)). apply (twooutof3a f py (isweqcontrtounit isx) (isweqcontrtounit isy)). Defined.

Definition weqcontrcontr { X Y : UU } ( isx : iscontr X) (isy: iscontr Y) := weqpair _ ( isweqcontrcontr ( fun x : X => pr21 isy ) isx isy ) .

Theorem twooutof3b { X Y Z : UU } (f:X->Y) (g:Y->Z) (isf: isweq f) (isgf: isweq (fun x:X => g(f x))) : isweq g.
Proof. intros. set ( wf := weqpair f isf ) . set ( wgf := weqpair _ isgf ) . set (invf:= invmap wf ). set (invgf:= invmap wgf ). set (invg := (fun z:Z => f ( invgf z))). set (gf:= fun x:X => (g (f x))).

assert (eginvg: forall z:Z, paths (g (invg z)) z). intro. apply (homotweqinvweq wgf z).

assert (einvgg: forall y:Y, paths (invg (g y)) y). intro. assert (isinvf: isweq invf). apply isweqinvmap. assert (isinvgf: isweq invgf). apply isweqinvmap. assert (int1: paths (g y) (gf (invf y))). apply (maponpaths g (pathsinv0 (homotweqinvweq wf y))). assert (int2: paths (gf (invgf (g y))) (gf (invf y))). assert (int3: paths (gf (invgf (g y))) (g y)). apply (homotweqinvweq wgf ). destruct int1. assumption. assert (int4: paths (invgf (g y)) (invf y)). apply (invmaponpathsweq wgf ). assumption. assert (int5:paths (invf (f (invgf (g y)))) (invgf (g y))). apply (homotinvweqweq wf ). assert (int6: paths (invf (f (invgf (g (y))))) (invf y)). destruct int4. assumption. apply (invmaponpathsweq ( weqpair invf isinvf ) ). assumption. apply (gradth g invg einvgg eginvg). Defined.

Lemma isweql3 { X Y : UU } (f:X-> Y) (g:Y->X) (egf: forall x:X, paths (g (f x)) x): isweq f -> isweq g.
Proof. intros X Y f g egf X0. set (gf:= fun x:X => g (f x)). assert (int1: isweq gf). apply (isweqhomot (fun x:X => x) gf (fun x:X => (pathsinv0 (egf x)))). apply idisweq. apply (twooutof3b f g X0 int1). Defined.

Theorem twooutof3c { X Y Z : UU } (f:X->Y) (g:Y->Z) (isf: isweq f) (isg: isweq g) : isweq (fun x:X => g(f x)).
Proof. intros. set ( wf := weqpair f isf ) . set ( wg := weqpair _ isg ) . set (gf:= fun x:X => g (f x)). set (invf:= invmap wf ). set (invg:= invmap wg ). set (invgf:= fun z:Z => invf (invg z)). assert (egfinvgf: forall x:X, paths (invgf (gf x)) x). unfold gf. unfold invgf. intro x. assert (int1: paths (invf (invg (g (f x)))) (invf (f x))). apply (maponpaths invf (homotinvweqweq wg (f x))). assert (int2: paths (invf (f x)) x). apply homotinvweqweq. destruct int1. assumption.
assert (einvgfgf: forall z:Z, paths (gf (invgf z)) z). unfold gf. unfold invgf. intro z. assert (int1: paths (g (f (invf (invg z)))) (g (invg z))). apply (maponpaths g (homotweqinvweq wf (invg z))). assert (int2: paths (g (invg z)) z). apply (homotweqinvweq wg z). destruct int1. assumption. apply (gradth gf invgf egfinvgf einvgfgf). Defined.

Definition weqcomp { X Y Z : UU } (w1 : weq X Y) (w2 : weq Y Z) : (weq X Z) := weqpair (fun x:X => (pr21 w2 (pr21 w1 x))) (twooutof3c _ _ (pr22 w1) (pr22 w2)).

Associativity of total2


Lemma total2asstor { X : UU } ( P : X -> UU ) ( Q : total2 P -> UU ) : total2 Q -> total2 ( fun x : X => total2 ( fun p : P x => Q ( tpair P x p ) ) ) .
Proof. intros X P Q xpq . destruct xpq as [ xp q ] . destruct xp as [ x p ] . split with x . split with p . assumption . Defined .

Lemma total2asstol { X : UU } ( P : X -> UU ) ( Q : total2 P -> UU ) : total2 ( fun x : X => total2 ( fun p : P x => Q ( tpair P x p ) ) ) -> total2 Q .
Proof. intros X P Q xpq . destruct xpq as [ x pq ] . destruct pq as [ p q ] . split with ( tpair P x p ) . assumption . Defined .

Theorem weqtotal2asstor { X : UU } ( P : X -> UU ) ( Q : total2 P -> UU ) : weq ( total2 Q ) ( total2 ( fun x : X => total2 ( fun p : P x => Q ( tpair P x p ) ) ) ).
Proof. intros . set ( f := total2asstor P Q ) . set ( g:= total2asstol P Q ) . split with f .
assert ( egf : forall xpq : _ , paths ( g ( f xpq ) ) xpq ) . intro . destruct xpq as [ xp q ] . destruct xp as [ x p ] . apply idpath .
assert ( efg : forall xpq : _ , paths ( f ( g xpq ) ) xpq ) . intro . destruct xpq as [ x pq ] . destruct pq as [ p q ] . apply idpath .
apply ( gradth _ _ egf efg ) . Defined.

Definition weqtotal2asstol { X : UU } ( P : X -> UU ) ( Q : total2 P -> UU ) : weq ( total2 ( fun x : X => total2 ( fun p : P x => Q ( tpair P x p ) ) ) ) ( total2 Q ) := invweq ( weqtotal2asstor P Q ) .

Associativity and commutativity of dirprod


Definition weqdirprodasstor ( X Y Z : UU ) : weq ( dirprod ( dirprod X Y ) Z ) ( dirprod X ( dirprod Y Z ) ) .
Proof . intros . apply weqtotal2asstor . Defined .

Definition weqdirprodasstol ( X Y Z : UU ) : weq ( dirprod X ( dirprod Y Z ) ) ( dirprod ( dirprod X Y ) Z ) := invweq ( weqdirprodasstor X Y Z ) .

Definition weqdirprodcomm ( X Y : UU ) : weq ( dirprod X Y ) ( dirprod Y X ) .
Proof. intros . set ( f := fun xy : dirprod X Y => dirprodpair ( pr22 xy ) ( pr21 xy ) ) . set ( g := fun yx : dirprod Y X => dirprodpair ( pr22 yx ) ( pr21 yx ) ) .
assert ( egf : forall xy : _ , paths ( g ( f xy ) ) xy ) . intro . destruct xy . apply idpath .
assert ( efg : forall yx : _ , paths ( f ( g yx ) ) yx ) . intro . destruct yx . apply idpath .
split with f . apply ( gradth _ _ egf efg ) . Defined .

Coproducts and direct products


Definition rdistrtocoprod ( X Y Z : UU ): dirprod X (coprod Y Z) -> coprod (dirprod X Y) (dirprod X Z).
Proof. intros X Y Z X0. destruct X0 as [ t x ]. destruct x as [ y | z ] . apply (ii1 (dirprodpair t y)). apply (ii2 (dirprodpair t z)). Defined.

Definition rdistrtoprod (X Y Z:UU): coprod (dirprod X Y) (dirprod X Z) -> dirprod X (coprod Y Z).
Proof. intros X Y Z X0. destruct X0 as [ d | d ]. destruct d as [ t x ]. apply (dirprodpair t (ii1 x)). destruct d as [ t x ]. apply (dirprodpair t (ii2 x)). Defined.

Theorem isweqrdistrtoprod (X Y Z:UU): isweq (rdistrtoprod X Y Z).
Proof. intros. set (f:= rdistrtoprod X Y Z). set (g:= rdistrtocoprod X Y Z).
assert (egf: forall a:_, paths (g (f a)) a). intro. destruct a as [ d | d ] . destruct d. apply idpath. destruct d. apply idpath.
assert (efg: forall a:_, paths (f (g a)) a). intro. destruct a as [ t x ]. destruct x. apply idpath. apply idpath.
apply (gradth f g egf efg). Defined.

Definition weqrdistrtoprod (X Y Z: UU):= weqpair _ (isweqrdistrtoprod X Y Z).

Corollary isweqrdistrtocoprod (X Y Z:UU): isweq (rdistrtocoprod X Y Z).
Proof. intros. apply (isweqinvmap ( weqrdistrtoprod X Y Z ) ) . Defined.

Definition weqrdistrtocoprod (X Y Z: UU):= weqpair _ (isweqrdistrtocoprod X Y Z).

Total space of a family over a coproduct


Definition fromtotal2overcoprod { X Y : UU } ( P : coprod X Y -> UU ) ( xyp : total2 P ) : coprod ( total2 ( fun x : X => P ( ii1 x ) ) ) ( total2 ( fun y : Y => P ( ii2 y ) ) ) .
Proof. intros . set ( PX := fun x : X => P ( ii1 x ) ) . set ( PY := fun y : Y => P ( ii2 y ) ) . destruct xyp as [ xy p ] . destruct xy as [ x | y ] . apply ( ii1 ( tpair PX x p ) ) . apply ( ii2 ( tpair PY y p ) ) . Defined .

Definition tototal2overcoprod { X Y : UU } ( P : coprod X Y -> UU ) ( xpyp : coprod ( total2 ( fun x : X => P ( ii1 x ) ) ) ( total2 ( fun y : Y => P ( ii2 y ) ) ) ) : total2 P .
Proof . intros . destruct xpyp as [ xp | yp ] . destruct xp as [ x p ] . apply ( tpair P ( ii1 x ) p ) . destruct yp as [ y p ] . apply ( tpair P ( ii2 y ) p ) . Defined .

Theorem weqtotal2overcoprod { X Y : UU } ( P : coprod X Y -> UU ) : weq ( total2 P ) ( coprod ( total2 ( fun x : X => P ( ii1 x ) ) ) ( total2 ( fun y : Y => P ( ii2 y ) ) ) ) .
Proof. intros . set ( f := fromtotal2overcoprod P ) . set ( g := tototal2overcoprod P ) . split with f .
assert ( egf : forall a : _ , paths ( g ( f a ) ) a ) . intro a . destruct a as [ xy p ] . destruct xy as [ x | y ] . simpl . apply idpath . simpl . apply idpath .
assert ( efg : forall a : _ , paths ( f ( g a ) ) a ) . intro a . destruct a as [ xp | yp ] . destruct xp as [ x p ] . simpl . apply idpath . destruct yp as [ y p ] . apply idpath .
apply ( gradth _ _ egf efg ) . Defined .

Weak equivalences and pairwise direct products


Theorem isweqdirprodf { X Y X' Y' : UU } ( w : weq X Y )( w' : weq X' Y' ) : isweq (dirprodf w w' ).
Proof. intros. set ( f := dirprodf w w' ) . set ( g := dirprodf ( invweq w ) ( invweq w' ) ) .
assert ( egf : forall a : _ , paths ( g ( f a ) ) a ) . intro a . destruct a as [ x x' ] . simpl . apply pathsdirprod . apply ( homotinvweqweq w x ) . apply ( homotinvweqweq w' x' ) .
assert ( efg : forall a : _ , paths ( f ( g a ) ) a ) . intro a . destruct a as [ x x' ] . simpl . apply pathsdirprod . apply ( homotweqinvweq w x ) . apply ( homotweqinvweq w' x' ) .
apply ( gradth _ _ egf efg ) . Defined .

Definition weqdirprodf { X Y X' Y' : UU } ( w : weq X Y ) ( w' : weq X' Y' ) := weqpair _ ( isweqdirprodf w w' ) .

Definition weqtodirprodwithunit (X:UU): weq X (dirprod X unit).
Proof. intros. set (f:=fun x:X => dirprodpair x tt). split with f. set (g:= fun xu:dirprod X unit => pr21 xu).
assert (egf: forall x:X, paths (g (f x)) x). intro. apply idpath.
assert (efg: forall xu:_, paths (f (g xu)) xu). intro. destruct xu as [ t x ]. destruct x. apply idpath.
apply (gradth f g egf efg). Defined.

Basics on pairwise coproducts (disjoint unions)


In the current version coprod is a notation, introduced in uuu.v for sum of types which is defined in Coq.Init

Definition sumofmaps {X Y Z:UU}(fx: X -> Z)(fy: Y -> Z): (coprod X Y) -> Z := fun xy:_ => match xy with ii1 x => fx x | ii2 y => fy y end.

Definition boolascoprod: weq (coprod unit unit) bool.
Proof. set (f:= fun xx: coprod unit unit => match xx with ii1 t => true | ii2 t => false end). split with f.
set (g:= fun t:bool => match t with true => ii1 tt | false => ii2 tt end).
assert (egf: forall xx:_, paths (g (f xx)) xx). intro xx . destruct xx as [ u | u ] . destruct u. apply idpath. destruct u. apply idpath.
assert (efg: forall t:_, paths (f (g t)) t). destruct t. apply idpath. apply idpath.
apply (gradth f g egf efg). Defined.

Definition coprodasstor (X Y Z:UU): coprod (coprod X Y) Z -> coprod X (coprod Y Z).
Proof. intros X Y Z X0. destruct X0 as [ c | z ] . destruct c as [ x | y ] . apply (ii1 x). apply (ii2 (ii1 y)). apply (ii2 (ii2 z)). Defined.

Definition coprodasstol (X Y Z: UU): coprod X (coprod Y Z) -> coprod (coprod X Y) Z.
Proof. intros X Y Z X0. destruct X0 as [ x | c ] . apply (ii1 (ii1 x)). destruct c as [ y | z ] . apply (ii1 (ii2 y)). apply (ii2 z). Defined.

Theorem isweqcoprodasstor (X Y Z:UU): isweq (coprodasstor X Y Z).
Proof. intros. set (f:= coprodasstor X Y Z). set (g:= coprodasstol X Y Z).
assert (egf: forall xyz:_, paths (g (f xyz)) xyz). intro xyz. destruct xyz as [ c | z ] . destruct c. apply idpath. apply idpath. apply idpath.
assert (efg: forall xyz:_, paths (f (g xyz)) xyz). intro xyz. destruct xyz as [ x | c ] . apply idpath. destruct c. apply idpath. apply idpath.
apply (gradth f g egf efg). Defined.

Definition weqcoprodasstor ( X Y Z : UU ) := weqpair _ ( isweqcoprodasstor X Y Z ) .

Corollary isweqcoprodasstol (X Y Z:UU): isweq (coprodasstol X Y Z).
Proof. intros. apply (isweqinvmap ( weqcoprodasstor X Y Z) ). Defined.

Definition weqcoprodasstol (X Y Z:UU):= weqpair _ (isweqcoprodasstol X Y Z).

Definition coprodcomm (X Y:UU): coprod X Y -> coprod Y X := fun xy:_ => match xy with ii1 x => ii2 x | ii2 y => ii1 y end.

Theorem isweqcoprodcomm (X Y:UU): isweq (coprodcomm X Y).
Proof. intros. set (f:= coprodcomm X Y). set (g:= coprodcomm Y X).
assert (egf: forall xy:_, paths (g (f xy)) xy). intro. destruct xy. apply idpath. apply idpath.
assert (efg: forall yx:_, paths (f (g yx)) yx). intro. destruct yx. apply idpath. apply idpath.
apply (gradth f g egf efg). Defined.

Definition weqcoprodcomm (X Y:UU):= weqpair _ (isweqcoprodcomm X Y).

Theorem isweqii1withneg (X : UU) { Y : UU } (nf:Y -> empty): isweq (@ii1 X Y).
Proof. intros. set (f:= @ii1 X Y). set (g:= fun xy:coprod X Y => match xy with ii1 x => x | ii2 y => fromempty (nf y) end).
assert (egf: forall x:X, paths (g (f x)) x). intro. apply idpath.
assert (efg: forall xy: coprod X Y, paths (f (g xy)) xy). intro. destruct xy as [ x | y ] . apply idpath. apply (fromempty (nf y)).
apply (gradth f g egf efg). Defined.

Definition weqii1withneg ( X : UU ) { Y : UU } ( nf : neg Y ) := weqpair _ ( isweqii1withneg X nf ) .

Theorem isweqii2withneg { X : UU } ( Y : UU ) (nf : X -> empty): isweq (@ii2 X Y).
Proof. intros. set (f:= @ii2 X Y). set (g:= fun xy:coprod X Y => match xy with ii1 x => fromempty (nf x) | ii2 y => y end).
assert (egf: forall y : Y, paths (g (f y)) y). intro. apply idpath.
assert (efg: forall xy: coprod X Y, paths (f (g xy)) xy). intro. destruct xy as [ x | y ] . apply (fromempty (nf x)). apply idpath.
apply (gradth f g egf efg). Defined.

Definition weqii2withneg { X : UU } ( Y : UU ) ( nf : neg X ) := weqpair _ ( isweqii2withneg Y nf ) .

Definition coprodf { X Y X' Y' : UU } (f: X -> X')(g: Y-> Y'): coprod X Y -> coprod X' Y' := fun xy: coprod X Y =>
match xy with
ii1 x => ii1 (f x)|
ii2 y => ii2 (g y)
end.

Definition homotcoprodfcomp { X X' Y Y' Z Z' : UU } ( f : X -> Y ) ( f' : X' -> Y' ) ( g : Y -> Z ) ( g' : Y' -> Z' ) : homot ( funcomp ( coprodf f f' ) ( coprodf g g' ) ) ( coprodf ( funcomp f g ) ( funcomp f' g' ) ) .
Proof. intros . intro xx' . destruct xx' as [ x | x' ] . apply idpath . apply idpath . Defined .

Definition homotcoprodfhomot { X X' Y Y' } ( f g : X -> Y ) ( f' g' : X' -> Y' ) ( h : homot f g ) ( h' : homot f' g' ) : homot ( coprodf f f') ( coprodf g g') := fun xx' : _ => match xx' with ( ii1 x ) => maponpaths ( @ii1 _ _ ) ( h x ) | ( ii2 x' ) => maponpaths ( @ii2 _ _ ) ( h' x' ) end .

Theorem isweqcoprodf { X Y X' Y' : UU } ( w : weq X X' )( w' : weq Y Y' ) : isweq (coprodf w w' ).
Proof. intros. set (finv:= invmap w ). set (ginv:= invmap w' ). set (ff:=coprodf w w' ). set (gg:=coprodf finv ginv).
assert (egf: forall xy: coprod X Y, paths (gg (ff xy)) xy). intro. destruct xy as [ x | y ] . simpl. apply (maponpaths (@ii1 X Y) (homotinvweqweq w x)). apply (maponpaths (@ii2 X Y) (homotinvweqweq w' y)).
assert (efg: forall xy': coprod X' Y', paths (ff (gg xy')) xy'). intro. destruct xy' as [ x | y ] . simpl. apply (maponpaths (@ii1 X' Y') (homotweqinvweq w x)). apply (maponpaths (@ii2 X' Y') (homotweqinvweq w' y)).
apply (gradth ff gg egf efg). Defined.

Definition weqcoprodf { X Y X' Y' : UU } (w1: weq X Y)(w2: weq X' Y') : weq (coprod X X') (coprod Y Y') := weqpair _ ( isweqcoprodf w1 w2 ) .

Lemma negpathsii1ii2 { X Y : UU } (x:X)(y:Y): neg (paths (ii1 x) (ii2 y)).
Proof. intros. unfold neg. intro X0. set (dist:= fun xy: coprod X Y => match xy with ii1 x => unit | ii2 y => empty end). apply (transportf dist X0 tt). Defined.

Lemma negpathsii2ii1 { X Y : UU } (x:X)(y:Y): neg (paths (ii2 y) (ii1 x)).
Proof. intros. unfold neg. intro X0. set (dist:= fun xy: coprod X Y => match xy with ii1 x => empty | ii2 y => unit end). apply (transportf dist X0 tt). Defined.

Fibrations with only one non-empty fiber.



Theorem saying that if a fibration has only one non-empty fiber then the total space is weakly equivalent to this fiber.

Theorem onefiber { X : UU } (P:X -> UU)(x:X)(c: forall x':X, coprod (paths x x') (P x' -> empty)) : isweq (fun p: P x => tpair P x p).
Proof. intros.

set (f:= fun p: P x => tpair _ x p).

set (cx := c x).
set (cnew:= fun x':X =>
match cx with
ii1 x0 =>
match c x' with
ii1 ee => ii1 (pathscomp0 (pathsinv0 x0) ee)|
ii2 phi => ii2 phi
end |
ii2 phi => c x'
end).

set (g:= fun pp: total2 P =>
match (cnew (pr21 pp)) with
ii1 e => transportb P e (pr22 pp) |
ii2 phi => fromempty (phi (pr22 pp))
end).

assert (efg: forall pp: total2 P, paths (f (g pp)) pp). intro. destruct pp as [ t x0 ]. set (cnewt:= cnew t). unfold g. unfold f. simpl. change (cnew t) with cnewt. destruct cnewt as [ x1 | y ]. apply (pathsinv0 (pr21 (pr22 (constr1 P (pathsinv0 x1))) x0)). destruct (y x0).


set (cnewx:= cnew x).
assert (e1: paths (cnew x) cnewx). apply idpath.
unfold cnew in cnewx. change (c x) with cx in cnewx.
destruct cx as [ x0 | e0 ].
assert (e: paths (cnewx) (ii1 (idpath x))). apply (maponpaths (@ii1 (paths x x) (P x -> empty)) (pathsinv0l x0)).

assert (egf: forall p: P x, paths (g (f p)) p). intro. simpl in g. unfold g. unfold f. simpl.

set (ff:= fun cc:coprod (paths x x) (P x -> empty) =>
match cc with
     | ii1 e0 => transportb P e0 p
     | ii2 phi => fromempty (phi p)
     end).
assert (ee: paths (ff (cnewx)) (ff (@ii1 (paths x x) (P x -> empty) (idpath x)))). apply (maponpaths ff e).
assert (eee: paths (ff (@ii1 (paths x x) (P x -> empty) (idpath x))) p). apply idpath. fold (ff (cnew x)).
assert (e2: paths (ff (cnew x)) (ff cnewx)). apply (maponpaths ff e1).
apply (pathscomp0 (pathscomp0 e2 ee) eee).
apply (gradth f g egf efg).

unfold isweq. intro y0. destruct (e0 (g y0)). Defined.

Pairwise coproducts as dependent sums of families over bool


Fixpoint coprodtobool { X Y : UU } ( xy : coprod X Y ) : bool :=
match xy with
ii1 x => true|
ii2 y => false
end.

Definition boolsumfun (X Y:UU) : bool -> UU := fun t:_ =>
match t with
true => X|
false => Y
end.

Definition coprodtoboolsum ( X Y : UU ) : coprod X Y -> total2 (boolsumfun X Y) := fun xy : _ =>
match xy with
ii1 x => tpair (boolsumfun X Y) true x|
ii2 y => tpair (boolsumfun X Y) false y
end .

Definition boolsumtocoprod (X Y:UU): (total2 (boolsumfun X Y)) -> coprod X Y := (fun xy:_ =>
match xy with
tpair true x => ii1 x|
tpair false y => ii2 y
end).

Theorem isweqcoprodtoboolsum (X Y:UU): isweq (coprodtoboolsum X Y).
Proof. intros. set (f:= coprodtoboolsum X Y). set (g:= boolsumtocoprod X Y).
assert (egf: forall xy: coprod X Y , paths (g (f xy)) xy). destruct xy. apply idpath. apply idpath.
assert (efg: forall xy: total2 (boolsumfun X Y), paths (f (g xy)) xy). intro. destruct xy as [ t x ]. destruct t. apply idpath. apply idpath. apply (gradth f g egf efg). Defined.

Definition weqcoprodtoboolsum ( X Y : UU ) := weqpair _ ( isweqcoprodtoboolsum X Y ) .

Corollary isweqboolsumtocoprod (X Y:UU): isweq (boolsumtocoprod X Y ).
Proof. intros. apply (isweqinvmap ( weqcoprodtoboolsum X Y ) ) . Defined.

Definition weqboolsumtocoprod ( X Y : UU ) := weqpair _ ( isweqboolsumtocoprod X Y ) .

Splitting of X into a coproduct defined by a function X -> coprod Y Z


Definition weqcoprodsplit { X Y Z : UU } ( f : X -> coprod Y Z ) : weq X ( coprod ( total2 ( fun y : Y => hfiber f ( ii1 y ) ) ) ( total2 ( fun z : Z => hfiber f ( ii2 z ) ) ) ) .
Proof . intros . set ( w1 := weqtococonusf f ) . set ( w2 := weqtotal2overcoprod ( fun yz : coprod Y Z => hfiber f yz ) ) . apply ( weqcomp w1 w2 ) . Defined .

Some properties of bool


Definition boolchoice ( x : bool ) : coprod ( paths x true ) ( paths x false ) .
Proof. intro . destruct x . apply ( ii1 ( idpath _ ) ) . apply ( ii2 ( idpath _ ) ) . Defined .

Definition curry : bool -> UU := fun x : bool =>
match x with
false => empty|
true => unit
end.

Theorem nopathstruetofalse: paths true false -> empty.
Proof. intro X. apply (transportf curry X tt). Defined.

Corollary nopathsfalsetotrue: paths false true -> empty.
Proof. intro X. apply (transportb curry X tt). Defined.

Definition truetonegfalse ( x : bool ) : paths x true -> neg ( paths x false ) .
Proof . intros x e . rewrite e . unfold neg . apply nopathstruetofalse . Defined .

Definition falsetonegtrue ( x : bool ) : paths x false -> neg ( paths x true ) .
Proof . intros x e . rewrite e . unfold neg . apply nopathsfalsetotrue . Defined .

Basics about fibration sequences.


Fibrations sequences and their first "left shifts".



The group of constructions related to fibration sequences forms one of the most important computational toolboxes of homotopy theory .

Given a pair of functions ( f : X -> Y ) ( g : Y -> Z ) and a point z : Z , a structure of the complex on such a triple is a homotopy from the composition funcomp f g to the constant function X -> Z corresponding to z i.e. a term ez : forall x:X, paths ( g ( f x ) ) z . Specifing such a structure is essentially equivalent to specifing a structure of the form ezmap : X -> hfiber g z . The mapping in one direction is given in the definition of ezmap below. The mapping in another is given by f := fun x : X => pr21 ( ezmap x ) and ez := fun x : X => pr22 ( ezmap x ) .

A complex is called a fibration sequence if ezmap is a weak equivalence. Correspondingly, the structure of a fibration sequence on f g z is a pair ( ez , is ) where is : isweq ( ezmap f g z ez ) . For a fibration sequence f g z fs where fs : fibseqstr f g z and any y : Y there is defined a function diff1 : paths ( g y ) z -> X and a structure of the fibration sequence fibseqdiff1 on the triple diff1 g y . This new fibration sequence is called the derived fibration sequence of the original one.

The first function of the second derived of f g z fs corresponding to ( y : Y ) ( x : X ) is of the form paths ( f x ) y -> paths ( g y ) z and it is homotopic to the function defined by e => pathscomp0 ( maponpaths g ( pathsinv0 e) ) ( ez x ) . The first function of the third derived of f g z fs corresponding to ( y : Y ) ( x : X ) ( e : paths ( g y ) z ) is of the form paths ( diff1 e ) x -> paths ( f x ) y . Therefore, the third derived of a sequence based on X Y Z is based entirely on paths types of X , Y and Z . When this construction is applied to types of finite h-level (see below) and combined with the fact that the h-level of a path type is strictly lower than the h-level of the ambient type it leads to the possibility of building proofs about types by induction on h-level.

There are three important special cases in which fibration sequences arise:

( pr21 - case ) The fibration sequence fibseqpr21 P z defined by family P : Z -> UU and a term z : Z . It is based on the sequence of functions ( tpair P z : P z -> total2 P ) ( pr21 : total2 P -> Z ) . The corresponding ezmap is defined by an obvious rule and the fact that it is a weak equivalence is proved in isweqfibertohfiber .

( g - case ) The fibration sequence fibseqg g z defined by a function g : Y -> Z and a term z : Z . It is based on the sequence of functions ( hfiberpr21 : hfiber g z -> Y ) ( g : Y -> Z ) and the corresponding ezmap is the function which takes a term ye : hfiber to hfiberpair g ( pr21 ye ) ( pr22 ye ) . If we had eta-concersion for the depndent sums it would be the identiry function. Since we do not have this conversion in Coq this function is only homotopic to the identity function by tppr which is sufficient to ensure that it is a weak equivalence. The first derived of fibseqg g z corresponding to y : Y coincides with fibseqpr21 ( fun y' : Y => paths ( g y' ) z ) y .

( hf -case ) The fibration sequence of homotopy fibers defined for any pair of functions ( f : X -> Y ) ( g : Y -> Z ) and any terms ( z : Z ) ( ye : hfiber g z ) . It is based on functions hfiberftogf : hfiber f ( pr21 ye ) -> hfiber ( funcomp f g ) z and hfibergftog : hfiber ( funcomp f g ) z -> hfiber g z which are defined below.


The structure of a complex structure on a composable pair of functions ( f : X -> Y ) ( g : Y -> Z ) relative to a term z : Z .

Definition complxstr { X Y Z : UU } (f:X -> Y) (g:Y->Z) ( z : Z ) := forall x:X, paths (g (f x)) z .


The structure of a fibration sequence on a complex.

Definition ezmap { X Y Z : UU } (f:X -> Y) (g:Y->Z) ( z : Z ) (ez : complxstr f g z ) : X -> hfiber g z := fun x:X => hfiberpair g (f x) (ez x).

Definition isfibseq { X Y Z : UU } (f:X -> Y) (g:Y->Z) ( z : Z ) (ez : complxstr f g z ) := isweq (ezmap f g z ez).

Definition fibseqstr { X Y Z : UU } (f:X -> Y) (g:Y->Z) ( z : Z ) := total2 ( fun ez : complxstr f g z => isfibseq f g z ez ) .
Definition fibseqstrpair { X Y Z : UU } (f:X -> Y) (g:Y->Z) ( z : Z ) := tpair ( fun ez : complxstr f g z => isfibseq f g z ez ) .
Definition fibseqstrtocomplxstr { X Y Z : UU } (f:X -> Y) (g:Y->Z) ( z : Z ) : fibseqstr f g z -> complxstr f g z := @pr21 _ ( fun ez : complxstr f g z => isfibseq f g z ez ) .
Coercion fibseqstrtocomplxstr : fibseqstr >-> complxstr .

Definition ezweq { X Y Z : UU } (f:X -> Y) (g:Y->Z) ( z : Z ) ( fs : fibseqstr f g z ) : weq X ( hfiber g z ) := weqpair _ ( pr22 fs ) .

Construction of the derived fibration sequence.

Definition d1 { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( fs : fibseqstr f g z ) ( y : Y ) : paths ( g y ) z -> X := fun e : _ => invmap ( ezweq f g z fs ) ( hfiberpair g y e ) .

Definition ezmap1 { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( fs : fibseqstr f g z ) ( y : Y ) ( e : paths ( g y ) z ) : hfiber f y .
Proof . intros . split with ( d1 f g z fs y e ) . unfold d1 . change ( f ( invmap (ezweq f g z fs) (hfiberpair g y e) ) ) with ( hfiberpr21 _ _ ( ezweq f g z fs ( invmap (ezweq f g z fs) (hfiberpair g y e) ) ) ) . apply ( maponpaths ( hfiberpr21 g z ) ( homotweqinvweq ( ezweq f g z fs ) (hfiberpair g y e) ) ) . Defined .

Definition invezmap1 { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( ez : complxstr f g z ) ( y : Y ) : hfiber f y -> paths (g y) z :=
fun xe: hfiber f y =>
match xe with
tpair x e => pathscomp0 (maponpaths g ( pathsinv0 e ) ) ( ez x )
end.

Theorem isweqezmap1 { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( fs : fibseqstr f g z ) ( y : Y ) : isweq ( ezmap1 f g z fs y ) .
Proof . intros . set ( ff := ezmap1 f g z fs y ) . set ( gg := invezmap1 f g z ( pr21 fs ) y ) .
assert ( egf : forall e : _ , paths ( gg ( ff e ) ) e ) . intro . simpl . apply ( hfibertriangle1inv0 g (homotweqinvweq (ezweq f g z fs) (hfiberpair g y e)) ) .
assert ( efg : forall xe : _ , paths ( ff ( gg xe ) ) xe ) . intro . destruct xe as [ x e ] . destruct e . simpl . unfold ff . unfold ezmap1 . unfold d1 . change (hfiberpair g (f x) ( pr21 fs x) ) with ( ezmap f g z fs x ) . apply ( hfibertriangle2 f ( hfiberpair f ( invmap (ezweq f g z fs) (ezmap f g z fs x) ) _ ) ( hfiberpair f x ( idpath _ ) ) ( homotinvweqweq ( ezweq f g z fs ) x ) ) . simpl . set ( e1 := pathsinv0 ( pathscomp0rid (maponpaths f (homotinvweqweq (ezweq f g z fs) x) ) ) ) . assert ( e2 : paths (maponpaths (hfiberpr21 g z) (homotweqinvweq (ezweq f g z fs) ( ( ezmap f g z fs ) x))) (maponpaths f (homotinvweqweq (ezweq f g z fs) x)) ) . set ( e3 := maponpaths ( fun e : _ => maponpaths ( hfiberpr21 g z ) e ) ( pathsinv0 ( homotweqinvweqweq ( ezweq f g z fs ) x ) ) ) . simpl in e3 . set ( e4 := maponpathscomp (ezmap f g z (pr21 fs)) (hfiberpr21 g z) (homotinvweqweq (ezweq f g z fs) x) ) . simpl in e4 . apply ( pathscomp0 e3 e4 ) . apply ( pathscomp0 e2 e1 ) .
apply ( gradth _ _ egf efg ) . Defined .

Definition ezweq1 { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( fs : fibseqstr f g z ) ( y : Y ) := weqpair _ ( isweqezmap1 f g z fs y ) .
Definition fibseq1 { X Y Z : UU } (f:X -> Y) (g:Y->Z) (z:Z) ( fs : fibseqstr f g z )(y:Y) : fibseqstr ( d1 f g z fs y) f y := fibseqstrpair _ _ _ _ ( isweqezmap1 f g z fs y ) .

Explitcit description of the first map in the second derived sequence.

Definition d2 { X Y Z : UU } (f:X -> Y) (g:Y->Z) (z:Z) ( fs : fibseqstr f g z ) (y:Y) (x:X) ( e : paths (f x) y ) : paths (g y) z := pathscomp0 ( maponpaths g ( pathsinv0 e ) ) ( ( pr21 fs ) x ) .
Definition ezweq2 { X Y Z : UU } (f:X -> Y) (g:Y->Z) (z:Z) ( fs : fibseqstr f g z ) (y:Y) (x:X) : weq ( paths (f x) y ) ( hfiber (d1 f g z fs y) x ) := ezweq1 (d1 f g z fs y) f y ( fibseq1 f g z fs y ) x.
Definition fibseq2 { X Y Z : UU } (f:X -> Y) (g:Y->Z) (z:Z) ( fs : fibseqstr f g z ) (y:Y) (x:X) : fibseqstr ( d2 f g z fs y x ) ( d1 f g z fs y ) x := fibseqstrpair _ _ _ _ ( isweqezmap1 (d1 f g z fs y) f y ( fibseq1 f g z fs y ) x ) .

Fibration sequences based on ( tpair P z : P z -> total2 P ) ( pr21 : total2 P -> Z ) ( the "pr21-case" )


Construction of the fibration sequence.

Definition ezmappr21 { Z : UU } ( P : Z -> UU ) ( z : Z ) : P z -> hfiber ( @pr21 Z P ) z := fun p : P z => tpair _ ( tpair _ z p ) ( idpath z ).

Definition invezmappr21 { Z : UU } ( P : Z -> UU) ( z : Z ) : hfiber ( @pr21 Z P ) z -> P z := fun te : hfiber ( @pr21 Z P ) z =>
match te with
tpair t e => transportf P e ( pr22 t )
end.

Definition isweqezmappr21 { Z : UU } ( P : Z -> UU ) ( z : Z ) : isweq ( ezmappr21 P z ).
Proof. intros.
assert ( egf : forall x: P z , paths (invezmappr21 _ z ((ezmappr21 P z ) x)) x). intro. unfold ezmappr21. unfold invezmappr21. simpl. apply idpath.
assert ( efg : forall x: hfiber (@pr21 Z P) z , paths (ezmappr21 _ z (invezmappr21 P z x)) x). intros. destruct x as [ x t0 ]. destruct t0. simpl in x. simpl. destruct x. simpl. unfold transportf. unfold ezmappr21. apply idpath.
apply (gradth _ _ egf efg ). Defined.

Definition ezweqpr21 { Z : UU } ( P : Z -> UU ) ( z : Z ) := weqpair _ ( isweqezmappr21 P z ) .

Lemma isfibseqpr21 { Z : UU } ( P : Z -> UU ) ( z : Z ) : isfibseq (fun p : P z => tpair _ z p) ( @pr21 Z P ) z (fun p: P z => idpath z ).
Proof. intros. unfold isfibseq. unfold ezmap. apply isweqezmappr21. Defined.

Definition fibseqpr21 { Z : UU } ( P : Z -> UU ) ( z : Z ) : fibseqstr (fun p : P z => tpair _ z p) ( @pr21 Z P ) z := fibseqstrpair _ _ _ _ ( isfibseqpr21 P z ) .

The main weak equivalence defined by the first derived of fibseqpr21 .

Definition ezweq1pr21 { Z : UU } ( P : Z -> UU ) ( z : Z ) ( zp : total2 P ) : weq ( paths ( pr21 zp) z ) ( hfiber ( tpair P z ) zp ) := ezweq1 _ _ z ( fibseqpr21 P z ) zp .

Fibration sequences based on ( hfiberpr21 : hfiber g z -> Y ) ( g : Y -> Z ) (the "g-case")


Theorem isfibseqg { Y Z : UU } (g:Y -> Z) (z:Z) : isfibseq (hfiberpr21 g z) g z (fun ye: _ => pr22 ye).
Proof. intros. assert (Y0:forall ye': hfiber g z, paths ye' (ezmap (hfiberpr21 g z) g z (fun ye: _ => pr22 ye) ye')). intro. apply tppr. apply (isweqhomot _ _ Y0 (idisweq _ )). Defined.

Definition ezweqg { Y Z : UU } (g:Y -> Z) (z:Z) := weqpair _ ( isfibseqg g z ) .
Definition fibseqg { Y Z : UU } (g:Y -> Z) (z:Z) : fibseqstr (hfiberpr21 g z) g z := fibseqstrpair _ _ _ _ ( isfibseqg g z ) .

The first derived of fibseqg .

Definition d1g { Y Z : UU} ( g : Y -> Z ) ( z : Z ) ( y : Y ) : paths ( g y ) z -> hfiber g z := hfiberpair g y .

note that d1g coincides with d1 _ _ _ ( fibseqg g z ) which makes the following two definitions possible.

Definition ezweq1g { Y Z : UU } (g:Y -> Z) (z:Z) (y:Y) : weq (paths (g y) z) (hfiber (hfiberpr21 g z) y) := weqpair _ (isweqezmap1 (hfiberpr21 g z) g z ( fibseqg g z ) y) .
Definition fibseq1g { Y Z : UU } (g:Y -> Z) (z:Z) ( y : Y) : fibseqstr (d1g g z y ) ( hfiberpr21 g z ) y := fibseqstrpair _ _ _ _ (isweqezmap1 (hfiberpr21 g z) g z ( fibseqg g z ) y) .

The second derived of fibseqg .

Definition d2g { Y Z : UU } (g:Y -> Z) { z : Z } ( y : Y ) ( ye' : hfiber g z ) ( e: paths (pr21 ye') y ) : paths (g y) z := pathscomp0 ( maponpaths g ( pathsinv0 e ) ) ( pr22 ye' ) .

note that d2g coincides with d2 _ _ _ ( fibseqg g z ) which makes the following two definitions possible.

Definition ezweq2g { Y Z : UU } (g:Y -> Z) { z : Z } ( y : Y ) ( ye' : hfiber g z ) : weq (paths (pr21 ye') y) (hfiber ( hfiberpair g y ) ye') := ezweq2 _ _ _ ( fibseqg g z ) _ _ .
Definition fibseq2g { Y Z : UU } (g:Y -> Z) { z : Z } ( y : Y ) ( ye' : hfiber g z ) : fibseqstr ( d2g g y ye' ) ( hfiberpair g y ) ye' := fibseq2 _ _ _ ( fibseqg g z ) _ _ .

The third derived of fibseqg and an explicit description of the corresponding first map.

Definition d3g { Y Z : UU } (g:Y -> Z) { z : Z } ( y : Y ) ( ye' : hfiber g z ) ( e : paths ( g y ) z ) : paths ( hfiberpair g y e ) ye' -> paths ( pr21 ye' ) y := d2 (d1g g z y) (hfiberpr21 g z) y ( fibseq1g g z y ) ye' e .

Lemma homotd3g { Y Z : UU } ( g : Y -> Z ) { z : Z } ( y : Y ) ( ye' : hfiber g z ) ( e : paths ( g y ) z ) ( ee : paths ( hfiberpair g y e) ye' ) : paths (d3g g y ye' e ee) ( maponpaths ( @pr21 _ _ ) ( pathsinv0 ee ) ) .
Proof. intros. unfold d3g . unfold d2 . simpl . apply pathscomp0rid. Defined .

Definition ezweq3g { Y Z : UU } (g:Y -> Z) { z : Z } ( y : Y ) ( ye' : hfiber g z ) ( e : paths ( g y ) z ) := ezweq2 (d1g g z y) (hfiberpr21 g z) y ( fibseq1g g z y ) ye' e .
Definition fibseq3g { Y Z : UU } (g:Y -> Z) { z : Z } ( y : Y ) ( ye' : hfiber g z ) ( e : paths ( g y ) z ) := fibseq2 (d1g g z y) (hfiberpr21 g z) y ( fibseq1g g z y ) ye' e .

Fibration sequence of h-fibers defined by a composable pair of functions (the "hf-case")



We construct a fibration sequence based on ( hfibersftogf f g z ye : hfiber f ( pr21 ye ) -> hfiber gf z ) ( hfibersgftog f g z : hfiber gf z -> hfiber g z ) .

Definition hfibersftogf { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( ye : hfiber g z ) ( xe : hfiber f ( pr21 ye ) ) : hfiber ( funcomp f g ) z .
Proof . intros . split with ( pr21 xe ) . apply ( pathscomp0 ( maponpaths g ( pr22 xe ) ) ( pr22 ye ) ) . Defined .

Definition ezmaphf { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( ye : hfiber g z ) ( xe : hfiber f ( pr21 ye ) ) : hfiber ( hfibersgftog f g z ) ye .
Proof . intros . split with ( hfibersftogf f g z ye xe ) . simpl . apply ( hfibertriangle2 g (hfiberpair g (f (pr21 xe)) (pathscomp0 (maponpaths g (pr22 xe)) ( pr22 ye ) )) ye ( pr22 xe ) ) . simpl . apply idpath . Defined .

Definition invezmaphf { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( ye : hfiber g z ) ( xee' : hfiber ( hfibersgftog f g z ) ye ) : hfiber f ( pr21 ye ) .
Proof . intros . split with ( pr21 ( pr21 xee' ) ) . apply ( maponpaths ( hfiberpr21 _ _ ) ( pr22 xee' ) ) . Defined .

Definition ffgg { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( ye : hfiber g z ) ( xee' : hfiber ( hfibersgftog f g z ) ye ) : hfiber ( hfibersgftog f g z ) ye .
Proof . intros . destruct ye as [ y e ] . destruct e . unfold hfibersgftog . unfold hfibersgftog in xee' . destruct xee' as [ xe e' ] . destruct xe as [ x e ] . simpl in e' . split with ( hfiberpair ( funcomp f g ) x ( pathscomp0 ( maponpaths g (maponpaths (hfiberpr21 g (g y)) e') ) ( idpath (g y ))) ) . simpl . apply ( hfibertriangle2 _ (hfiberpair g (f x) (( pathscomp0 ( maponpaths g (maponpaths (hfiberpr21 g (g y)) e') ) ( idpath (g y ))))) ( hfiberpair g y ( idpath _ ) ) ( maponpaths ( hfiberpr21 _ _ ) e' ) ( idpath _ ) ) . Defined .

Definition homotffggid { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( ye : hfiber g z ) ( xee' : hfiber ( hfibersgftog f g z ) ye ) : paths ( ffgg f g z ye xee' ) xee' .
Proof . intros . destruct ye as [ y e ] . destruct e . destruct xee' as [ xe e' ] . destruct e' . destruct xe as [ x e ] . destruct e . simpl . apply idpath . Defined .

Theorem isweqezmaphf { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( ye : hfiber g z ) : isweq ( ezmaphf f g z ye ) .
Proof . intros . set ( ff := ezmaphf f g z ye ) . set ( gg := invezmaphf f g z ye ) .
assert ( egf : forall xe : _ , paths ( gg ( ff xe ) ) xe ) . destruct ye as [ y e ] . destruct e . intro xe . apply ( hfibertriangle2 f ( gg ( ff xe ) ) xe ( idpath ( pr21 xe ) ) ) . destruct xe as [ x ex ] . simpl in ex . destruct ( ex ) . simpl . apply idpath .
assert ( efg : forall xee' : _ , paths ( ff ( gg xee' ) ) xee' ) . destruct ye as [ y e ] . destruct e . intro xee' .
assert ( hint : paths ( ff ( gg xee' ) ) ( ffgg f g ( g y ) ( hfiberpair g y ( idpath _ ) ) xee' ) ) . destruct xee' as [ xe e' ] . destruct xe as [ x e ] . apply idpath .
apply ( pathscomp0 hint ( homotffggid _ _ _ _ xee' ) ) .
apply ( gradth _ _ egf efg ) . Defined .

Definition ezweqhf { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( ye : hfiber g z ) : weq ( hfiber f ( pr21 ye ) ) ( hfiber ( hfibersgftog f g z ) ye ) := weqpair _ ( isweqezmaphf f g z ye ) .
Definition fibseqhf { X Y Z : UU } (f:X -> Y)(g: Y -> Z)(z:Z)(ye: hfiber g z) : fibseqstr (hfibersftogf f g z ye) (hfibersgftog f g z) ye := fibseqstrpair _ _ _ _ ( isweqezmaphf f g z ye ) .

Definition isweqinvezmaphf { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( ye : hfiber g z ) : isweq ( invezmaphf f g z ye ) := pr22 ( invweq ( ezweqhf f g z ye ) ) .

Corollary weqhfibersgwtog { X Y Z : UU } ( w : weq X Y ) ( g : Y -> Z ) ( z : Z ) : weq ( hfiber ( funcomp w g ) z ) ( hfiber g z ) .
Proof. intros . split with ( hfibersgftog w g z ) . intro ye . apply ( iscontrweqf ( ezweqhf w g z ye ) ( ( pr22 w ) ( pr21 ye ) ) ) . Defined .

Fiber-wise weak equivalences.



Theorems saying that a fiber-wise morphism between total spaces is a weak equivalence if and only if all the morphisms between the fibers are weak equivalences.

Definition totalfun { X : UU } ( P Q : X -> UU ) (f: forall x:X, P x -> Q x) := (fun z: total2 P => tpair Q (pr21 z) (f (pr21 z) (pr22 z))).

Theorem isweqtotaltofib { X : UU } ( P Q : X -> UU) (f: forall x:X, P x -> Q x):
isweq (totalfun _ _ f) -> forall x:X, isweq (f x).
Proof. intros X P Q f X0 x. set (totp:= total2 P). set (totq := total2 Q). set (totf:= (totalfun _ _ f)). set (pip:= fun z: totp => pr21 z). set (piq:= fun z: totq => pr21 z).

set (hfx:= hfibersgftog totf piq x). simpl in hfx.
assert (H: isweq hfx). unfold isweq. intro y.
set (int:= invezmaphf totf piq x y).
assert (X1:isweq int). apply (isweqinvezmaphf totf piq x y). destruct y as [ t e ].
assert (is1: iscontr (hfiber totf t)). apply (X0 t). apply (iscontrweqb ( weqpair int X1 ) is1).
set (ip:= ezmappr21 P x). set (iq:= ezmappr21 Q x). set (h:= fun p: P x => hfx (ip p)).
assert (is2: isweq h). apply (twooutof3c ip hfx (isweqezmappr21 P x) H). set (h':= fun p: P x => iq ((f x) p)).
assert (ee: forall p:P x, paths (h p) (h' p)). intro. apply idpath.
assert (X2:isweq h'). apply (isweqhomot h h' ee is2).
apply (twooutof3a (f x) iq X2).
apply (isweqezmappr21 Q x). Defined.

Definition weqtotaltofib { X : UU } ( P Q : X -> UU ) ( f : forall x : X , P x -> Q x ) ( is : isweq ( totalfun _ _ f ) ) ( x : X ) : weq ( P x ) ( Q x ) := weqpair _ ( isweqtotaltofib P Q f is x ) .

Theorem isweqfibtototal { X : UU } ( P Q : X -> UU) (f: forall x:X, weq ( P x ) ( Q x ) ) : isweq (totalfun _ _ f).
Proof. intros X P Q f . set (fpq:= totalfun P Q f). set (pr21p:= fun z: total2 P => pr21 z). set (pr21q:= fun z: total2 Q => pr21 z). unfold isweq. intro xq. set (x:= pr21q xq). set (xqe:= hfiberpair pr21q xq (idpath _)). set (hfpqx:= hfibersgftog fpq pr21q x).

assert (isint: iscontr (hfiber hfpqx xqe)).
assert (isint1: isweq hfpqx). set (ipx:= ezmappr21 P x). set (iqx:= ezmappr21 Q x). set (diag:= fun p:P x => (iqx ((f x) p))).
assert (is2: isweq diag). apply (twooutof3c (f x) iqx (pr22 ( f x) ) (isweqezmappr21 Q x)). apply (twooutof3b ipx hfpqx (isweqezmappr21 P x) is2). unfold isweq in isint1. apply (isint1 xqe).
set (intmap:= invezmaphf fpq pr21q x xqe). apply (iscontrweqf ( weqpair intmap (isweqinvezmaphf fpq pr21q x xqe) ) isint).
Defined.

Definition weqfibtototal { X : UU } ( P Q : X -> UU) (f: forall x:X, weq ( P x ) ( Q x ) ) := weqpair _ ( isweqfibtototal P Q f ) .

Homotopy fibers of the function fpmap: total2 X (P f) -> total2 Y P.



Given X Y in UU , P:Y -> UU and f: X -> Y we get a function fpmap: total2 X (P f) -> total2 Y P . The main theorem of this section asserts that the homotopy fiber of fpmap over yp:total Y P is naturally weakly equivalent to the homotopy fiber of f over pr21 yp . In particular, if f is a weak equivalence then so is fpmap .

Definition fpmap { X Y : UU } (f: X -> Y) ( P:Y-> UU) : total2 ( funcomp f P ) -> total2 P :=
(fun z:total2 (fun x:X => P (f x)) => tpair P (f (pr21 z)) (pr22 z)).

Definition hffpmap2 { X Y : UU } (f: X -> Y) (P:Y-> UU): total2 ( funcomp f P ) -> total2 (fun u:total2 P => hfiber f (pr21 u)).
Proof. intros X Y f P X0. set (u:= fpmap f P X0). split with u. set (x:= pr21 X0). split with x. simpl. apply idpath. Defined.

Definition hfiberfpmap { X Y : UU } (f:X -> Y)(P:Y-> UU)(yp: total2 P): hfiber (fpmap f P) yp -> hfiber f (pr21 yp).
Proof. intros X Y f P yp X0. set (int1:= hfibersgftog (hffpmap2 f P) (fun u: (total2 (fun u:total2 P => hfiber f (pr21 u))) => (pr21 u)) yp). set (phi:= invezmappr21 (fun u:total2 P => hfiber f (pr21 u)) yp). apply (phi (int1 X0)). Defined.

Lemma centralfiber { X : UU } (P:X -> UU)(x:X): isweq (fun p: P x => tpair (fun u: coconusfromt X x => P ( pr21 u)) (coconusfromtpair X (idpath x)) p).
Proof. intros. set (f:= fun p: P x => tpair (fun u: coconusfromt X x => P(pr21 u)) (coconusfromtpair X (idpath x)) p). set (g:= fun z: total2 (fun u: coconusfromt X x => P ( pr21 u)) => transportf P (pathsinv0 (pr22 (pr21 z))) (pr22 z)).

assert (efg: forall z: total2 (fun u: coconusfromt X x => P ( pr21 u)), paths (f (g z)) z). intro. destruct z as [ t x0 ]. destruct t as [t x1 ]. simpl. destruct x1. simpl. apply idpath.

assert (egf: forall p: P x , paths (g (f p)) p). intro. apply idpath.

apply (gradth f g egf efg). Defined.

Lemma isweqhff { X Y : UU } (f: X -> Y)(P:Y-> UU): isweq (hffpmap2 f P).
Proof. intros. set (int:= total2 (fun x:X => total2 (fun u: coconusfromt Y (f x) => P (pr21 u)))). set (intpair:= tpair (fun x:X => total2 (fun u: coconusfromt Y (f x) => P (pr21 u)))). set (toint:= fun z: (total2 (fun u : total2 P => hfiber f (pr21 u))) => intpair (pr21 (pr22 z)) (tpair (fun u: coconusfromt Y (f (pr21 (pr22 z))) => P (pr21 u)) (coconusfromtpair _ (pr22 (pr22 z))) (pr22 (pr21 z)))). set (fromint:= fun z: int => tpair (fun u:total2 P => hfiber f (pr21 u)) (tpair P (pr21 (pr21 (pr22 z))) (pr22 (pr22 z))) (hfiberpair f (pr21 z) (pr22 (pr21 (pr22 z))))). assert (fromto: forall u:(total2 (fun u : total2 P => hfiber f (pr21 u))), paths (fromint (toint u)) u). simpl in toint. simpl in fromint. simpl. intro u. destruct u as [ t x ]. destruct x. destruct t as [ p0 p1 ] . simpl. unfold toint. unfold fromint. simpl. apply idpath. assert (tofrom: forall u:int, paths (toint (fromint u)) u). intro. destruct u as [ t x ]. destruct x as [ t0 x ]. destruct t0. simpl in x. simpl. unfold fromint. unfold toint. simpl. apply idpath. assert (is: isweq toint). apply (gradth toint fromint fromto tofrom). clear tofrom. clear fromto. clear fromint.

set (h:= fun u: total2 (fun x:X => P (f x)) => toint ((hffpmap2 f P) u)). simpl in h.

assert (l1: forall x:X, isweq (fun p: P (f x) => tpair (fun u: coconusfromt _ (f x) => P (pr21 u)) (coconusfromtpair _ (idpath (f x))) p)). intro. apply (centralfiber P (f x)).

assert (X0:isweq h). apply (isweqfibtototal (fun x:X => P (f x)) (fun x:X => total2 (fun u: coconusfromt _ (f x) => P (pr21 u))) (fun x:X => weqpair _ ( l1 x ) ) ).

apply (twooutof3a (hffpmap2 f P) toint X0 is). Defined.

Theorem isweqhfiberfp { X Y : UU } (f:X -> Y)(P:Y-> UU)(yp: total2 P): isweq (hfiberfpmap f P yp).
Proof. intros. set (int1:= hfibersgftog (hffpmap2 f P) (fun u: (total2 (fun u:total2 P => hfiber f (pr21 u))) => (pr21 u)) yp). assert (is1: isweq int1). simpl in int1 . apply ( pr22 ( weqhfibersgwtog ( weqpair _ ( isweqhff f P ) ) (fun u : total2 (fun u : total2 P => hfiber f (pr21 u)) => pr21 u) yp ) ) . set (phi:= invezmappr21 (fun u:total2 P => hfiber f (pr21 u)) yp). assert (is2: isweq phi). apply ( pr22 ( invweq ( ezweqpr21 (fun u:total2 P => hfiber f (pr21 u)) yp ) ) ) . apply (twooutof3c int1 phi is1 is2). Defined.

Corollary isweqfpmap { X Y : UU } ( w : weq X Y )(P:Y-> UU) : isweq (fpmap w P).
Proof. intros. unfold isweq. intro y. set (h:=hfiberfpmap w P y).
assert (X1:isweq h). apply isweqhfiberfp.
assert (is: iscontr (hfiber w (pr21 y))). apply ( pr22 w ). apply (iscontrweqb ( weqpair h X1 ) is). Defined.

Definition weqfp { X Y : UU } ( w : weq X Y )(P:Y-> UU) := weqpair _ ( isweqfpmap w P ) .

Total spaces of families over a contractible base


Definition fromtotal2overunit ( P : unit -> UU ) ( tp : total2 P ) : P tt .
Proof . intros . destruct tp as [ t p ] . destruct t . apply p . Defined .

Definition tototal2overunit ( P : unit -> UU ) ( p : P tt ) : total2 P := tpair P tt p .

Theorem weqtotal2overunit ( P : unit -> UU ) : weq ( total2 P ) ( P tt ) .
Proof. intro . set ( f := fromtotal2overunit P ) . set ( g := tototal2overunit P ) . split with f .
assert ( egf : forall a : _ , paths ( g ( f a ) ) a ) . intro a . destruct a as [ t p ] . destruct t . apply idpath .
assert ( efg : forall a : _ , paths ( f ( g a ) ) a ) . intro a . apply idpath .
apply ( gradth _ _ egf efg ) . Defined .

The maps between total spaces of families given by a map between the bases of the families and maps between the corresponding members of the families


Definition bandfmap { X Y : UU }(f: X -> Y) ( P : X -> UU)(Q: Y -> UU)(fm: forall x:X, P x -> (Q (f x))): total2 P -> total2 Q:= fun xp:_ =>
match xp with
tpair x p => tpair Q (f x) (fm x p)
end.

Theorem isweqbandfmap { X Y : UU } (w : weq X Y ) (P:X -> UU)(Q: Y -> UU)( fw : forall x:X, weq ( P x) (Q (w x))) : isweq (bandfmap _ P Q fw).
Proof. intros. set (f1:= totalfun P _ fw). set (is1:= isweqfibtototal P (fun x:X => Q (w x)) fw ). set (f2:= fpmap w Q). set (is2:= isweqfpmap w Q ).
assert (h: forall xp: total2 P, paths (f2 (f1 xp)) (bandfmap w P Q fw xp)). intro. destruct xp. apply idpath. apply (isweqhomot _ _ h (twooutof3c f1 f2 is1 is2)). Defined.

Definition weqbandf { X Y : UU } (w : weq X Y ) (P:X -> UU)(Q: Y -> UU)( fw : forall x:X, weq ( P x) (Q (w x))) := weqpair _ ( isweqbandfmap w P Q fw ) .

Homotopy fiber squares


Homotopy commutative squares


Definition commsqstr { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) := forall ( z : Z ) , paths ( f' ( g' z ) ) ( f ( g z ) ) .

Definition hfibersgtof' { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( h : commsqstr f f' g g' ) ( x : X ) ( ze : hfiber g x ) : hfiber f' ( f x ) .
Proof. intros . destruct ze as [ z e ] . split with ( g' z ) . apply ( pathscomp0 ( h z ) ( maponpaths f e ) ) . Defined .

Definition hfibersg'tof { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( h : commsqstr f f' g g' ) ( x' : X' ) ( ze : hfiber g' x' ) : hfiber f ( f' x' ) .
Proof. intros . destruct ze as [ z e ] . split with ( g z ) . apply ( pathscomp0 ( pathsinv0 ( h z ) ) ( maponpaths f' e ) ) . Defined .

Definition transposcommsqstr { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) : commsqstr f f' g g' -> commsqstr f' f g' g := fun h : _ => fun z : Z => ( pathsinv0 ( h z ) ) .

Short complexes and homotopy commutative squares


Lemma complxstrtocommsqstr { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( h : complxstr f g z ) : commsqstr ( fun t : unit => z ) g ( fun x : X => tt ) f .
Proof. intros . assumption . Defined .

Lemma commsqstrtocomplxstr { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( h : commsqstr ( fun t : unit => z ) g ( fun x : X => tt ) f ) : complxstr f g z .
Proof. intros . assumption . Defined .

Homotopy fiber products


Definition hfp {X X' Y:UU} (f:X -> Y) (f':X' -> Y):= total2 (fun xx' : dirprod X X' => paths ( f' ( pr22 xx' ) ) ( f ( pr21 xx' ) ) ) .
Definition hfpg {X X' Y:UU} (f:X -> Y) (f':X' -> Y) : hfp f f' -> X := fun xx'e => ( pr21 ( pr21 xx'e ) ) .
Definition hfpg' {X X' Y:UU} (f:X -> Y) (f':X' -> Y) : hfp f f' -> X' := fun xx'e => ( pr22 ( pr21 xx'e ) ) .

Definition commsqZtohfp { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( h : commsqstr f f' g g' ) : Z -> hfp f f' := fun z : _ => tpair _ ( dirprodpair ( g z ) ( g' z ) ) ( h z ) .

Definition commsqZtohfphomot { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( h : commsqstr f f' g g' ) : forall z : Z , paths ( hfpg _ _ ( commsqZtohfp _ _ _ _ h z ) ) ( g z ) := fun z : _ => idpath _ .

Definition commsqZtohfphomot' { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( h : commsqstr f f' g g' ) : forall z : Z , paths ( hfpg' _ _ ( commsqZtohfp _ _ _ _ h z ) ) ( g' z ) := fun z : _ => idpath _ .

Definition hfpoverX {X X' Y:UU} (f:X -> Y) (f':X' -> Y) := total2 (fun x : X => hfiber f' ( f x ) ) .
Definition hfpoverX' {X X' Y:UU} (f:X -> Y) (f':X' -> Y) := total2 (fun x' : X' => hfiber f (f' x' ) ) .

Definition weqhfptohfpoverX {X X' Y:UU} (f:X -> Y) (f':X' -> Y) : weq ( hfp f f' ) ( hfpoverX f f' ) .
Proof. intros . apply ( weqtotal2asstor ( fun x : X => X' ) ( fun xx' : dirprod X X' => paths ( f' ( pr22 xx' ) ) ( f ( pr21 xx' ) ) ) ) . Defined .

Definition weqhfptohfpoverX' {X X' Y:UU} (f:X -> Y) (f':X' -> Y) : weq ( hfp f f' ) ( hfpoverX' f f' ) .
Proof. intros . set ( w1 := weqfp ( weqdirprodcomm X X' ) ( fun xx' : dirprod X' X => paths ( f' ( pr21 xx' ) ) ( f ( pr22 xx' ) ) ) ) . simpl in w1 .
set ( w2 := weqfibtototal ( fun x'x : dirprod X' X => paths ( f' ( pr21 x'x ) ) ( f ( pr22 x'x ) ) ) ( fun x'x : dirprod X' X => paths ( f ( pr22 x'x ) ) ( f' ( pr21 x'x ) ) ) ( fun x'x : _ => weqpathsinv0 ( f' ( pr21 x'x ) ) ( f ( pr22 x'x ) ) ) ) . set ( w3 := weqtotal2asstor ( fun x' : X' => X ) ( fun x'x : dirprod X' X => paths ( f ( pr22 x'x ) ) ( f' ( pr21 x'x ) ) ) ) . simpl in w3 . apply ( weqcomp ( weqcomp w1 w2 ) w3 ) . Defined .

Lemma weqhfpcomm { X X' Y : UU } ( f : X -> Y ) ( f' : X' -> Y ) : weq ( hfp f f' ) ( hfp f' f ) .
Proof . intros . set ( w1 := weqfp ( weqdirprodcomm X X' ) ( fun xx' : dirprod X' X => paths ( f' ( pr21 xx' ) ) ( f ( pr22 xx' ) ) ) ) . simpl in w1 . set ( w2 := weqfibtototal ( fun x'x : dirprod X' X => paths ( f' ( pr21 x'x ) ) ( f ( pr22 x'x ) ) ) ( fun x'x : dirprod X' X => paths ( f ( pr22 x'x ) ) ( f' ( pr21 x'x ) ) ) ( fun x'x : _ => weqpathsinv0 ( f' ( pr21 x'x ) ) ( f ( pr22 x'x ) ) ) ) . apply ( weqcomp w1 w2 ) . Defined .

Definition commhfp {X X' Y:UU} (f:X -> Y) (f':X' -> Y) : commsqstr f f' ( hfpg f f' ) ( hfpg' f f' ) := fun xx'e : hfp f f' => pr22 xx'e .

Homotopy fiber products and homotopy fibers


Definition hfibertohfp { X Y : UU } ( f : X -> Y ) ( y : Y ) ( xe : hfiber f y ) : hfp ( fun t : unit => y ) f := tpair ( fun tx : dirprod unit X => paths ( f ( pr22 tx ) ) y ) ( dirprodpair tt ( pr21 xe ) ) ( pr22 xe ) .

Definition hfptohfiber { X Y : UU } ( f : X -> Y ) ( y : Y ) ( hf : hfp ( fun t : unit => y ) f ) : hfiber f y := hfiberpair f ( pr22 ( pr21 hf ) ) ( pr22 hf ) .

Lemma weqhfibertohfp { X Y : UU } ( f : X -> Y ) ( y : Y ) : weq ( hfiber f y ) ( hfp ( fun t : unit => y ) f ) .
Proof . intros . set ( ff := hfibertohfp f y ) . set ( gg := hfptohfiber f y ) . split with ff .
assert ( egf : forall xe : _ , paths ( gg ( ff xe ) ) xe ) . intro . destruct xe . apply idpath .
assert ( efg : forall hf : _ , paths ( ff ( gg hf ) ) hf ) . intro . destruct hf as [ tx e ] . destruct tx as [ t x ] . destruct t . apply idpath .
apply ( gradth _ _ egf efg ) . Defined .

Homotopy fiber squares


Definition ishfsq { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( h : commsqstr f f' g g' ) := isweq ( commsqZtohfp f f' g g' h ) .

Definition hfsqstr { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) := total2 ( fun h : commsqstr f f' g g' => isweq ( commsqZtohfp f f' g g' h ) ) .
Definition hfsqstrpair { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) := tpair ( fun h : commsqstr f f' g g' => isweq ( commsqZtohfp f f' g g' h ) ) .
Definition hfsqstrtocommsqstr { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) : hfsqstr f f' g g' -> commsqstr f f' g g' := @pr21 _ ( fun h : commsqstr f f' g g' => isweq ( commsqZtohfp f f' g g' h ) ) .
Coercion hfsqstrtocommsqstr : hfsqstr >-> commsqstr .

Definition weqZtohfp { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( hf : hfsqstr f f' g g' ) : weq Z ( hfp f f' ) := weqpair _ ( pr22 hf ) .

Lemma isweqhfibersgtof' { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( hf : hfsqstr f f' g g' ) ( x : X ) : isweq ( hfibersgtof' f f' g g' hf x ) .
Proof. intros . set ( is := pr22 hf ) . set ( h := pr21 hf ) .
set ( a := weqtococonusf g ) . set ( c := weqpair _ is ) . set ( d := weqhfptohfpoverX f f' ) . set ( b0 := totalfun _ _ ( hfibersgtof' f f' g g' h ) ) .
assert ( h1 : forall z : Z , paths ( d ( c z ) ) ( b0 ( a z ) ) ) . intro . simpl . unfold b0 . unfold a . unfold weqtococonusf . unfold tococonusf . simpl . unfold totalfun . simpl . assert ( e : paths ( h z ) ( pathscomp0 (h z) (idpath (f (g z))) ) ) . apply ( pathsinv0 ( pathscomp0rid _ ) ) . destruct e . apply idpath .
assert ( is1 : isweq ( fun z : _ => b0 ( a z ) ) ) . apply ( isweqhomot _ _ h1 ) . apply ( twooutof3c _ _ ( pr22 c ) ( pr22 d ) ) .
assert ( is2 : isweq b0 ) . apply ( twooutof3b _ _ ( pr22 a ) is1 ) . apply ( isweqtotaltofib _ _ _ is2 x ) . Defined .

Definition weqhfibersgtof' { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( hf : hfsqstr f f' g g' ) ( x : X ) := weqpair _ ( isweqhfibersgtof' _ _ _ _ hf x ) .

Lemma ishfsqweqhfibersgtof' { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( h : commsqstr f f' g g' ) ( is : forall x : X , isweq ( hfibersgtof' f f' g g' h x ) ) : hfsqstr f f' g g' .
Proof . intros . split with h .
set ( a := weqtococonusf g ) . set ( c0 := commsqZtohfp f f' g g' h ) . set ( d := weqhfptohfpoverX f f' ) . set ( b := weqfibtototal _ _ ( fun x : X => weqpair _ ( is x ) ) ) .
assert ( h1 : forall z : Z , paths ( d ( c0 z ) ) ( b ( a z ) ) ) . intro . simpl . unfold b . unfold a . unfold weqtococonusf . unfold tococonusf . simpl . unfold totalfun . simpl . assert ( e : paths ( h z ) ( pathscomp0 (h z) (idpath (f (g z))) ) ) . apply ( pathsinv0 ( pathscomp0rid _ ) ) . destruct e . apply idpath .
assert ( is1 : isweq ( fun z : _ => d ( c0 z ) ) ) . apply ( isweqhomot _ _ ( fun z : Z => ( pathsinv0 ( h1 z ) ) ) ) . apply ( twooutof3c _ _ ( pr22 a ) ( pr22 b ) ) .
 apply ( twooutof3a _ _ is1 ( pr22 d ) ) . Defined .

Lemma isweqhfibersg'tof { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( hf : hfsqstr f f' g g' ) ( x' : X' ) : isweq ( hfibersg'tof f f' g g' hf x' ) .
Proof. intros . set ( is := pr22 hf ) . set ( h := pr21 hf ) .
set ( a' := weqtococonusf g' ) . set ( c' := weqpair _ is ) . set ( d' := weqhfptohfpoverX' f f' ) . set ( b0' := totalfun _ _ ( hfibersg'tof f f' g g' h ) ) .
assert ( h1 : forall z : Z , paths ( d' ( c' z ) ) ( b0' ( a' z ) ) ) . intro . unfold b0' . unfold a' . unfold weqtococonusf . unfold tococonusf . unfold totalfun . simpl . assert ( e : paths ( pathsinv0 ( h z ) ) ( pathscomp0 ( pathsinv0 (h z) ) (idpath (f' (g' z))) ) ) . apply ( pathsinv0 ( pathscomp0rid _ ) ) . destruct e . apply idpath .
assert ( is1 : isweq ( fun z : _ => b0' ( a' z ) ) ) . apply ( isweqhomot _ _ h1 ) . apply ( twooutof3c _ _ ( pr22 c' ) ( pr22 d' ) ) .
assert ( is2 : isweq b0' ) . apply ( twooutof3b _ _ ( pr22 a' ) is1 ) . apply ( isweqtotaltofib _ _ _ is2 x' ) . Defined .

Definition weqhfibersg'tof { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( hf : hfsqstr f f' g g' ) ( x' : X' ) := weqpair _ ( isweqhfibersg'tof _ _ _ _ hf x' ) .

Lemma ishfsqweqhfibersg'tof { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( h : commsqstr f f' g g' ) ( is : forall x' : X' , isweq ( hfibersg'tof f f' g g' h x' ) ) : hfsqstr f f' g g' .
Proof . intros . split with h .
set ( a' := weqtococonusf g' ) . set ( c0' := commsqZtohfp f f' g g' h ) . set ( d' := weqhfptohfpoverX' f f' ) . set ( b' := weqfibtototal _ _ ( fun x' : X' => weqpair _ ( is x' ) ) ) .
assert ( h1 : forall z : Z , paths ( d' ( c0' z ) ) ( b' ( a' z ) ) ) . intro . simpl . unfold b' . unfold a' . unfold weqtococonusf . unfold tococonusf . unfold totalfun . simpl . assert ( e : paths ( pathsinv0 ( h z ) ) ( pathscomp0 ( pathsinv0 (h z) ) (idpath (f' (g' z))) ) ) . apply ( pathsinv0 ( pathscomp0rid _ ) ) . destruct e . apply idpath .
assert ( is1 : isweq ( fun z : _ => d' ( c0' z ) ) ) . apply ( isweqhomot _ _ ( fun z : Z => ( pathsinv0 ( h1 z ) ) ) ) . apply ( twooutof3c _ _ ( pr22 a' ) ( pr22 b' ) ) .
 apply ( twooutof3a _ _ is1 ( pr22 d' ) ) . Defined .

Theorem transposhfpsqstr { X X' Y Z : UU } ( f : X -> Y ) ( f' : X' -> Y ) ( g : Z -> X ) ( g' : Z -> X' ) ( hf : hfsqstr f f' g g' ) : hfsqstr f' f g' g .
Proof . intros . set ( is := pr22 hf ) . set ( h := pr21 hf ) . set ( th := transposcommsqstr f f' g g' h ) . split with th .
set ( w1 := weqhfpcomm f f' ) . assert ( h1 : forall z : Z , paths ( w1 ( commsqZtohfp f f' g g' h z ) ) ( commsqZtohfp f' f g' g th z ) ) . intro . unfold commsqZtohfp . simpl . unfold fpmap . unfold totalfun . simpl . apply idpath . apply ( isweqhomot _ _ h1 ) . apply ( twooutof3c _ _ is ( pr22 w1 ) ) . Defined .


Fiber sequences and homotopy fiber squares


Theorem fibseqstrtohfsqstr { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( hf : fibseqstr f g z ) : hfsqstr ( fun t : unit => z ) g ( fun x : X => tt ) f .
Proof . intros . split with ( pr21 hf ) . set ( ff := ezweq f g z hf ) . set ( ggff := commsqZtohfp ( fun t : unit => z ) g ( fun x : X => tt ) f ( pr21 hf ) ) . set ( gg := weqhfibertohfp g z ) .
apply ( weqcomp ff gg ) . Defined .

Theorem hfsqstrtofibseqstr { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( hf : hfsqstr ( fun t : unit => z ) g ( fun x : X => tt ) f ) : fibseqstr f g z .
Proof . intros . split with ( pr21 hf ) . set ( ff := ezmap f g z ( pr21 hf ) ) . set ( ggff := weqZtohfp ( fun t : unit => z ) g ( fun x : X => tt ) f hf ) . set ( gg := weqhfibertohfp g z ) .
apply ( twooutof3a ff gg ( pr22 ggff ) ( pr22 gg ) ) . Defined .

Basics about h-levels


h-levels of types


Fixpoint isofhlevel (n:nat) (X:UU): UU:=
match n with
O => iscontr X |
S m => forall x:X, forall x':X, (isofhlevel m (paths x x'))
end.

Theorem hlevelretract (n:nat) { X Y : UU } ( p : X -> Y ) ( s : Y -> X ) ( eps : forall y : Y , paths ( p ( s y ) ) y ) : isofhlevel n X -> isofhlevel n Y .
Proof. intro. 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'))). 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). Defined.

Corollary isofhlevelweqf (n:nat) { X Y : UU } ( f : weq X Y ) : isofhlevel n X -> isofhlevel n Y .
Proof. intros n X Y f X0. apply (hlevelretract n f (invmap f ) (homotweqinvweq f )). assumption. Defined.

Corollary isofhlevelweqb (n:nat) { X Y : UU } ( f : weq X Y ) : isofhlevel n Y -> isofhlevel n X .
Proof. intros n X Y f X0 . apply (hlevelretract n (invmap f ) f (homotinvweqweq f )). assumption. Defined.

Lemma isofhlevelsn ( n : nat ) { X : UU } ( f : X -> isofhlevel ( S n ) X ) : isofhlevel ( S n ) X.
Proof. intros . simpl . intros x x' . apply ( f x x x'). Defined.

Lemma isofhlevelssn (n:nat) { X : UU } ( is : forall x:X, isofhlevel (S n) (paths x x)) : isofhlevel (S (S n)) X.
Proof. intros . simpl. intros x x'. change ( forall ( x0 x'0 : paths x x' ), isofhlevel n ( paths x0 x'0 ) ) with ( isofhlevel (S n) (paths x x') ).
assert ( X1 : paths x x' -> isofhlevel (S n) (paths x x') ) . intro X2. destruct X2. apply ( is x ). apply ( isofhlevelsn n X1 ). Defined.

h-levels of functions


Definition isofhlevelf ( n : nat ) { X Y : UU } ( f : X -> Y ) : UU := forall y:Y, isofhlevel n (hfiber f y).

Theorem isofhlevelfhomot ( n : nat ) { X Y : UU }(f f':X -> Y)(h: forall x:X, paths (f x) (f' x)): isofhlevelf n f -> isofhlevelf n f'.
Proof. intros n X Y f f' h X0. unfold isofhlevelf. intro y . apply ( isofhlevelweqf n ( weqhfibershomot f f' h y ) ( X0 y )) . Defined .

Theorem isofhlevelfpmap ( n : nat ) { X Y : UU } ( f : X -> Y ) ( Q : Y -> UU ) : isofhlevelf n f -> isofhlevelf n ( fpmap f Q ) .
Proof. intros n X Y f Q X0. unfold isofhlevelf. unfold isofhlevelf in X0. intro y . set (yy:= pr21 y). set ( g := hfiberfpmap f Q y). set (is:= isweqhfiberfp f Q y). set (isy:= X0 yy). apply (isofhlevelweqb n ( weqpair g is ) isy). Defined.

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 .
Proof. intros . intro y . assert ( w : weq ( hfiber f y ) ( paths ( g y ) z ) ) . apply ( invweq ( ezweq1 f g z fs y ) ) . apply ( isofhlevelweqb n w ( isz (g y ) z ) ) . Defined.

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 .
Proof. intros n X Y Z f g z fs isf . assert ( w : weq X ( hfiber g z ) ) . apply ( weqpair _ ( pr22 fs ) ) . apply ( isofhlevelweqb n w ( isf z ) ) . Defined .

Theorem isofhlevelffromXY ( n : nat ) { X Y : UU } ( f : X -> Y ) : isofhlevel n X -> isofhlevel (S n) Y -> isofhlevelf n f.
Proof. intro. induction n as [ | n IHn ] . intros X Y f X0 X1.
assert (is1: isofhlevel O Y). split with ( f ( pr21 X0 ) ) . intro t . unfold isofhlevel in X1 . set ( is := X1 t ( f ( pr21 X0 ) ) ) . apply ( pr21 is ).
apply (isweqcontrcontr f X0 is1).

intros X Y f X0 X1. unfold isofhlevelf. simpl.
assert (is1: forall x' x:X, isofhlevel n (paths x' x)). simpl in X0. assumption.
assert (is2: forall y' y:Y, isofhlevel (S n) (paths y' y)). simpl in X1. simpl. assumption.
assert (is3: forall (y:Y)(x:X)(xe': hfiber f y), isofhlevelf n (d2g f x xe')). intros. apply (IHn _ _ (d2g f x xe') (is1 (pr21 xe') x) (is2 (f x) y)).
assert (is4: forall (y:Y)(x:X)(xe': hfiber f y)(e: paths (f x) y), isofhlevel n (paths (hfiberpair f x e) xe')). intros.
apply (isofhlevelweqb n ( ezweq3g f x xe' e) (is3 y x xe' e)).
intros y xe xe' . destruct xe as [ t x ]. apply (is4 y t xe' x). Defined.

Theorem isofhlevelXfromfY ( n : nat ) { X Y : UU } ( f : X -> Y ) : isofhlevelf n f -> isofhlevel n Y -> isofhlevel n X.
Proof. intro. induction n as [ | n IHn ] . intros X Y f X0 X1. apply (iscontrweqb ( weqpair f X0 ) X1). intros X Y f X0 X1. simpl.
assert (is1: forall (y:Y)(xe xe': hfiber f y), isofhlevel n (paths xe xe')). intros. apply (X0 y).
assert (is2: forall (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 (hfiberpair f x y0) xe')).
assert (is3: forall (y' y : Y), isofhlevel n (paths y' y)). simpl in X1. assumption.
intros x' x .
set (y:= f x'). set (e':= idpath y). set (xe':= hfiberpair f x' e').
apply (IHn _ _ (d2g f x xe') (is2 y x xe') (is3 (f x) y)). Defined.

Theorem isofhlevelffib ( n : nat ) { X : UU } ( P : X -> UU ) ( x : X ) ( is : forall x':X, isofhlevel n (paths x' x) ) : isofhlevelf n ( tpair P x ) .
Proof . intros . unfold isofhlevelf . intro xp . apply (isofhlevelweqf n ( ezweq1pr21 P x xp) ( is ( pr21 xp ) ) ) . Defined .

Theorem isofhlevelfhfiberpr21y ( n : nat ) { X Y : UU } ( f : X -> Y ) ( y : Y ) ( is : forall y':Y, isofhlevel n (paths y' y) ) : isofhlevelf n ( hfiberpr21 f y).
Proof. intros . unfold isofhlevelf. intro x. apply (isofhlevelweqf n ( ezweq1g f y x ) ( is ( f x ) ) ) . Defined.

Theorem isofhlevelfsnfib (n:nat) { X : UU } (P:X -> UU)(x:X) ( is : isofhlevel (S n) (paths x x) ) : isofhlevelf (S n) ( tpair P x ).
Proof. intros . unfold isofhlevelf. intro xp. apply (isofhlevelweqf (S n) ( ezweq1pr21 P x xp ) ). apply isofhlevelsn . intro X1 . destruct X1 . assumption . Defined .

Theorem isofhlevelfsnhfiberpr21 ( n : nat ) { X Y : UU } (f : X -> Y ) ( y : Y ) ( is : isofhlevel (S n) (paths y y) ) : isofhlevelf (S n) (hfiberpr21 f y).
Proof. intros . unfold isofhlevelf. intro x. apply (isofhlevelweqf (S n) ( ezweq1g f y x ) ). apply isofhlevelsn. intro X1. destruct X1. assumption. Defined .

Corollary isofhlevelfhfiberpr21 ( n : nat ) { X Y : UU } ( f : X -> Y ) ( y : Y ) ( is : isofhlevel (S n) Y ) : isofhlevelf n ( hfiberpr21 f y ) .
Proof. intros. apply isofhlevelfhfiberpr21y. intro y' . apply (is y' y). Defined.

Theorem isofhlevelff ( n : nat ) { X Y Z : UU } (f : X -> Y ) ( g : Y -> Z ) : isofhlevelf n (fun x : X => g ( f x) ) -> isofhlevelf (S n) g -> isofhlevelf n f.
Proof. intros n X Y Z f g X0 X1. unfold isofhlevelf. intro y . set (ye:= hfiberpair g y (idpath (g y))).
apply (isofhlevelweqb n ( ezweqhf f g (g y) ye ) (isofhlevelffromXY n _ (X0 (g y)) (X1 (g y)) ye)). Defined.

Theorem isofhlevelfgf ( n : nat ) { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) : isofhlevelf n f -> isofhlevelf n g -> isofhlevelf n (fun x:X => g(f x)).
Proof. intros n X Y Z f g 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 (pr21 ye))).
assert (is2: isofhlevel n (hfiber g z)). apply (X1 z).
apply (isofhlevelXfromfY n _ is1 is2). Defined.

Theorem isofhlevelfgwtog (n:nat ) { X Y Z : UU } ( w : weq X Y ) ( g : Y -> Z ) ( is : isofhlevelf n (fun x : X => g ( w x ) ) ) : isofhlevelf n g .
Proof. intros . intro z . assert ( is' : isweq ( hfibersgftog w g z ) ) . intro ye . apply ( iscontrweqf ( ezweqhf w g z ye ) ( pr22 w ( pr21 ye ) ) ) . apply ( isofhlevelweqf _ ( weqpair _ is' ) ( is _ ) ) . Defined .

Theorem isofhlevelfgtogw (n:nat ) { X Y Z : UU } ( w : weq X Y ) ( g : Y -> Z ) ( is : isofhlevelf n g ) : isofhlevelf n (fun x : X => g ( w x ) ) .
Proof. intros . intro z . assert ( is' : isweq ( hfibersgftog w g z ) ) . intro ye . apply ( iscontrweqf ( ezweqhf w g z ye ) ( pr22 w ( pr21 ye ) ) ) . apply ( isofhlevelweqb _ ( weqpair _ is' ) ( is _ ) ) . Defined .

Corollary isofhlevelfhomot2 (n:nat) { X X' Y : UU } (f:X -> Y)(f':X' -> Y)(w : weq X X' )(h:forall x:X, paths (f x) (f' (w x))) : isofhlevelf n f -> isofhlevelf n f'.
Proof. intros n X X' Y f f' w h X0. assert (X1: isofhlevelf n (fun x:X => f' (w x))). apply (isofhlevelfhomot n _ _ h X0).
apply (isofhlevelfgwtog n w f' X1). Defined.

Theorem isofhlevelfonpaths (n:nat) { X Y : UU }(f:X -> Y)(x x':X): isofhlevelf (S n) f -> isofhlevelf n (@maponpaths _ _ f x x').
Proof. intros n X Y f x x' X0.
set (y:= f x'). set (xe':= hfiberpair 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 (hfiberpair f x y0) xe')).
assert (h: forall ee:paths 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)) ). destruct ee. simpl. apply idpath. apply (e0). apply (isofhlevelfhomot2 n _ _ ( weqpair (@pathsinv0 _ x' x ) (isweqpathsinv0 _ _ ) ) h is1) . Defined.

Theorem isofhlevelfsn (n:nat) { X Y : UU } (f:X -> Y): (forall x x':X, isofhlevelf n (@maponpaths _ _ f x x')) -> isofhlevelf (S n) f.
Proof. intros n X Y f X0. unfold isofhlevelf. intro y . simpl. intros x x' . destruct x as [ x e ]. destruct x' as [ x' e' ]. destruct e' . set (xe':= hfiberpair f x' ( idpath _ ) ). set (xe:= hfiberpair f x e). set (d3:= d2g f x xe'). simpl in d3.
assert (is1: isofhlevelf n (d2g f x xe')).
assert (h: forall ee: paths x' x, paths (maponpaths f (pathsinv0 ee)) (d2g f x xe' ee)). intro. unfold d2g. simpl . apply ( pathsinv0 ( pathscomp0rid _ ) ) .
assert (is2: isofhlevelf n (fun ee: paths x' x => maponpaths f (pathsinv0 ee))). apply (isofhlevelfgtogw n ( weqpair _ (isweqpathsinv0 _ _ ) ) (@maponpaths _ _ f x x') (X0 x x')).
apply (isofhlevelfhomot n _ _ h is2).
apply (isofhlevelweqb n ( ezweq3g f x xe' e ) (is1 e)). Defined.

Theorem isofhlevelfssn (n:nat) { X Y : UU } (f:X -> Y): (forall x:X, isofhlevelf (S n) (@maponpaths _ _ f x x)) -> isofhlevelf (S (S n)) f.
Proof. intros n X Y f X0. unfold isofhlevelf. intro y .
assert (forall xe0: hfiber f y, isofhlevel (S n) (paths xe0 xe0)). intro. destruct xe0 as [ x e ]. destruct e . set (e':= idpath ( f x ) ). set (xe':= hfiberpair f x e'). set (xe:= hfiberpair f x e' ). set (d3:= d2g f x xe'). simpl in d3.
assert (is1: isofhlevelf (S n) (d2g f x xe')).
assert (h: forall ee: paths 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: paths x x => maponpaths f (pathsinv0 ee))). apply (isofhlevelfgtogw ( S n ) ( weqpair _ (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. Defined.

h -levels of pr21 , fiber inclusions, fibers, total spaces and bases of fibrations


h-levelf of pr21


Theorem isofhlevelfpr21 (n:nat) { X : UU } (P:X -> UU)(is: forall x:X, isofhlevel n (P x)) : isofhlevelf n (@pr21 X P).
Proof. intros. unfold isofhlevelf. intro x . apply (isofhlevelweqf n ( ezweqpr21 _ x) (is x)). Defined.

Lemma isweqpr21 { Z : UU } ( P : Z -> UU ) ( is1 : forall z : Z, iscontr ( P z ) ) : isweq ( @pr21 Z P ) .
Proof. intros. unfold isweq. intro y. set (isy:= is1 y). apply (iscontrweqf ( ezweqpr21 P y)) . assumption. Defined.

Definition weqpr21 { Z : UU } ( P : Z -> UU ) ( is : forall z : Z , iscontr ( P z ) ) : weq ( total2 P ) Z := weqpair _ ( isweqpr21 P is ) .

h-level of the total space total2


Theorem isofhleveltotal2 ( n : nat ) { X : UU } ( P : X -> UU ) ( is1 : isofhlevel n X )( is2 : forall x:X, isofhlevel n (P x) ) : isofhlevel n (total2 P).
Proof. intros. apply (isofhlevelXfromfY n (@pr21 _ _ )). apply isofhlevelfpr21. assumption. assumption. Defined.

Corollary isofhleveldirprod ( n : nat ) ( X Y : UU ) ( is1 : isofhlevel n X ) ( is2 : isofhlevel n Y ) : isofhlevel n (dirprod X Y).
Proof. intros. apply isofhleveltotal2. assumption. intro. assumption. Defined.

Propositions, inclusions and sets


Basics about types of h-level 1 - "propositions"


Definition isaprop := isofhlevel (S O) .

Notation isapropunit := iscontrpathsinunit .

Lemma isapropifcontr { X : UU } ( is : iscontr X ) : isaprop X .
Proof. intros . set (f:= fun x:X => tt). assert (isw : isweq f). apply isweqcontrtounit. assumption. apply (isofhlevelweqb (S O) ( weqpair f isw ) ). intros x x' . apply iscontrpathsinunit. Defined.
Coercion isapropifcontr : iscontr >-> isaprop .

Theorem hlevelntosn ( n : nat ) ( T : UU ) ( is : isofhlevel n T ) : isofhlevel (S n) T.
Proof. intro. induction n as [ | n IHn ] . intro. apply isapropifcontr. intro. intro X. change (forall t1 t2:T, isofhlevel (S n) (paths t1 t2)). intros t1 t2 . change (forall t1 t2 : T, isofhlevel n (paths t1 t2)) in X. set (XX := X t1 t2). apply (IHn _ XX). Defined.

Corollary isofhlevelcontr (n:nat) { X : UU } ( is : iscontr X ) : isofhlevel n X.
Proof. intro. induction n as [ | n IHn ] . intros X X0 . assumption.
intros X X0. simpl. intros x x' . assert (is: iscontr (paths x x')). apply (isapropifcontr X0 x x'). apply (IHn _ is). Defined.

Lemma isofhlevelfweq ( n : nat ) { X Y : UU } ( f : weq X Y ) : isofhlevelf n f .
Proof. intros n X Y f . unfold isofhlevelf. intro y . apply ( isofhlevelcontr n ). apply ( pr22 f ). Defined.

Corollary isweqfinfibseq { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( fs : fibseqstr f g z ) ( isz : iscontr Z ) : isweq f .
Proof. intros . apply ( isofhlevelfffromZ 0 f g z fs ( isapropifcontr isz ) ) . Defined .

Corollary weqhfibertocontr { X Y : UU } ( f : X -> Y ) ( y : Y ) ( is : iscontr Y ) : weq ( hfiber f y ) X .
Proof. intros . split with ( hfiberpr21 f y ) . apply ( isofhlevelfhfiberpr21 0 f y ( hlevelntosn 0 _ is ) ) . Defined.

Corollary weqhfibertounit ( X : UU ) : weq ( hfiber ( fun x : X => tt ) tt ) X .
Proof. intro . apply ( weqhfibertocontr _ tt iscontrunit ) . Defined.

Corollary isofhleveltofun ( n : nat ) ( X : UU ) : isofhlevel n X -> isofhlevelf n ( fun x : X => tt ) .
Proof. intros n X is . intro t . destruct t . apply ( isofhlevelweqb n ( weqhfibertounit X ) is ) . Defined .

Corollary isofhlevelfromfun ( n : nat ) ( X : UU ) : isofhlevelf n ( fun x : X => tt ) -> isofhlevel n X .
Proof. intros n X is . apply ( isofhlevelweqf n ( weqhfibertounit X ) ( is tt ) ) . Defined .

Lemma isofhlevelsnprop (n:nat) { X : UU } ( is : isaprop X ) : isofhlevel (S n) X.
Proof. intros n X X0. simpl. unfold isaprop in X0. simpl in X0. intros x x' . apply isofhlevelcontr. apply (X0 x x'). Defined.

Lemma iscontraprop1 { X : UU } ( is : isaprop X ) ( x : X ) : iscontr X .
Proof. intros . unfold iscontr. split with x . intro t . unfold isofhlevel in is . set (is' := is t x ). apply ( pr21 is' ).
Defined.

Lemma iscontraprop1inv { X : UU } ( f : X -> iscontr X ) : isaprop X .
Proof. intros X X0. assert ( H : X -> isofhlevel (S O) X). intro X1. apply (hlevelntosn O _ ( X0 X1 ) ) . apply ( isofhlevelsn O H ) . Defined.

Lemma proofirrelevance ( X : UU ) ( is : isaprop X ) : forall x x' : X , paths x x' .
Proof. intros . unfold isaprop in is . unfold isofhlevel in is . apply ( pr21 ( is x x' ) ). Defined.

Lemma invproofirrelevance ( X : UU ) ( ee : forall x x' : X , paths x x' ) : isaprop X.
Proof. intros . unfold isaprop. unfold isofhlevel . intro x .
assert ( is1 : iscontr X ). split with x. intro t . apply ( ee t x). assert ( is2 : isaprop X). apply isapropifcontr. assumption.
unfold isaprop in is2. unfold isofhlevel in is2. apply (is2 x). Defined.

Lemma isweqimplimpl { X Y : UU } ( f : X -> Y ) ( g : Y -> X ) ( isx : isaprop X ) ( isy : isaprop Y ) : isweq f.
Proof. intros.
assert (isx0: forall x:X, paths (g (f x)) x). intro. apply proofirrelevance . apply isx .
assert (isy0 : forall y : Y, paths (f (g y)) y). intro. apply proofirrelevance . apply isy .
apply (gradth f g isx0 isy0). Defined.

Definition weqimplimpl { X Y : UU } ( f : X -> Y ) ( g : Y -> X ) ( isx : isaprop X ) ( isy : isaprop Y ) := weqpair _ ( isweqimplimpl f g isx isy ) .

Theorem isapropempty: isaprop empty.
Proof. unfold isaprop. unfold isofhlevel. intros x x' . destruct x. Defined.

Theorem isapropempty2 { X : UU } ( a : X -> empty ) : isaprop X .
Proof . intros . set ( w := weqpair _ ( isweqtoempty a ) ) . apply ( isofhlevelweqb 1 w isapropempty ) . Defined .

Lemma isapropifnegtrue { X : UU } ( X0 : neg X ) : isaprop X.
Proof. intros X X0. assert (is:isweq X0). intro. apply (fromempty y). apply (isofhlevelweqb (S O) ( weqpair _ is ) isapropempty). Defined.

Functional extensionality for functions to the empty type


Axiom funextempty : forall ( X : UU ) ( f g : X -> empty ) , paths f g .

More results on propositions


Theorem isapropneg (X:UU): isaprop (X -> empty).
Proof. intro. apply invproofirrelevance . intros x x' . apply ( funextempty X x x' ) . Defined .

See also isapropneg2

Corollary isapropdneg (X:UU): isaprop (dneg X).
Proof. intro. apply (isapropneg (neg X)). Defined.

Definition isaninvprop (X:UU) := isweq (todneg X).

Definition invimpl (X:UU) (is: isaninvprop X) : (dneg X) -> X:= invmap ( weqpair (todneg X) is ) .

Lemma isapropaninvprop (X:UU): isaninvprop X -> isaprop X.
Proof. intros X X0.
apply (isofhlevelweqb (S O) ( weqpair (todneg X) X0 ) (isapropdneg X)). Defined.

Theorem isaninvpropneg (X:UU): isaninvprop (neg X).
Proof. intros.
set (f:= todneg (neg X)). set (g:= negf (todneg X)). set (is1:= isapropneg X). set (is2:= isapropneg (dneg X)). apply (isweqimplimpl f g is1 is2). Defined.

Theorem isapropdec (X:UU): (isaprop X) -> (isaprop (coprod X (X-> empty))).
Proof. intros X X0.
assert (X1: forall (x x': X), paths x x'). apply (proofirrelevance _ X0).
assert (X2: forall (x x': coprod X (X -> empty)), paths x x'). intros.
destruct x as [ x0 | y0 ]. destruct x' as [ x | y ]. apply (maponpaths (fun x:X => ii1 x) (X1 x0 x)).
apply (fromempty (y x0)).
destruct x' as [ x | y ]. apply (fromempty (y0 x)).
assert (e: paths y0 y). apply (proofirrelevance _ (isapropneg X) y0 y). apply (maponpaths (fun f: X -> empty => ii2 f) e).
apply (invproofirrelevance _ X2). Defined.

Inclusions - functions of h-level 1


Definition isincl { X Y : UU } (f : X -> Y ) := isofhlevelf 1 f .

Definition incl ( X Y : UU ) := total2 ( fun f : X -> Y => isincl f ) .
Definition inclpair { X Y : UU } ( f : X -> Y ) ( is : isincl f ) : incl X Y := tpair _ f is .
Definition pr21incl ( X Y : UU ) : incl X Y -> ( X -> Y ) := @pr21 _ _ .
Coercion pr21incl : incl >-> Funclass .

Lemma isinclweq ( X Y : UU ) ( f : X -> Y ) : isweq f -> isincl f .
Proof . intros X Y f is . apply ( isofhlevelfweq 1 ( weqpair _ is ) ) . Defined .
Coercion isinclweq : isweq >-> isincl .

Lemma isofhlevelfsnincl (n:nat) { X Y : UU } (f:X -> Y)(is: isincl f): isofhlevelf (S n) f.
Proof. intros. unfold isofhlevelf. intro y . apply isofhlevelsnprop. apply (is y). Defined.

Definition weqtoincl ( X Y : UU ) : weq X Y -> incl X Y := fun w => inclpair ( pr21 w ) ( pr22 w ) .
Coercion weqtoincl : weq >-> incl .

Lemma isinclcomp { X Y Z : UU } ( f : incl X Y ) ( g : incl Y Z ) : isincl ( funcomp ( pr21 f ) ( pr21 g ) ) .
Proof . intros . apply ( isofhlevelfgf 1 f g ( pr22 f ) ( pr22 g ) ) . Defined .

Definition inclcomp { X Y Z : UU } ( f : incl X Y ) ( g : incl Y Z ) : incl X Z := inclpair ( funcomp ( pr21 f ) ( pr21 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 .
Proof . intros . apply ( isofhlevelff 1 f g isgf ) . apply ( isofhlevelfsnincl 1 g isg ) . Defined .

Lemma isinclgwtog { X Y Z : UU } ( w : weq X Y ) ( g : Y -> Z ) ( is : isincl ( funcomp w g ) ) : isincl g .
Proof . intros . apply ( isofhlevelfgwtog 1 w g is ) . Defined .

Lemma isinclgtogw { X Y Z : UU } ( w : weq X Y ) ( g : Y -> Z ) ( is : isincl g ) : isincl ( funcomp w g ) .
Proof . intros . apply ( isofhlevelfgtogw 1 w g is ) . Defined .

Lemma isinclhomot { X Y : UU } ( f g : X -> Y ) ( h : homot f g ) ( isf : isincl f ) : isincl g .
Proof . intros . apply ( isofhlevelfhomot ( S O ) f g h isf ) . Defined .

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 -> (forall x:X, iscontr (hfiber f (f x))).
Proof. intros X Y f X0 x. unfold isofhlevelf in X0. set (isy:= X0 (f x)). apply (iscontraprop1 isy (hfiberpair f _ (idpath (f x)))). Defined.

Lemma isweqonpathsincl { X Y : UU } (f:X -> Y) (is: isincl f)(x x':X): isweq (@maponpaths _ _ f x x').
Proof. intros. apply (isofhlevelfonpaths O f x x' is). Defined.

Definition weqonpathsincl { X Y : UU } (f:X -> Y) (is: isincl f)(x x':X) := weqpair _ ( isweqonpathsincl f is x x' ) .

Definition invmaponpathsincl { X Y : UU } (f:X -> Y) (is: isincl f)(x x':X): paths (f x) (f x') -> paths x x':= invmap ( weqonpathsincl f is x x') .

Lemma isinclweqonpaths { X Y : UU } (f:X -> Y): (forall x x':X, isweq (@maponpaths _ _ f x x')) -> isincl f.
Proof. intros X Y f X0. apply (isofhlevelfsn O f X0). Defined.

Definition isinclpr21 { X : UU } (P:X -> UU)(is: forall x:X, isaprop (P x)): isincl (@pr21 X P):= isofhlevelfpr21 (S O) P is.

Theorem samehfibers { X Y Z : UU } (f: X -> Y) (g: Y -> Z) (is1: isincl g) ( y: Y): weq ( hfiber f y ) ( hfiber ( fun x => g ( f x ) ) ( g y ) ) .
Proof. intros. split with (@hfibersftogf _ _ _ f g (g y) (hfiberpair g y (idpath _ ))) .

set (z:= g y). set (ye:= hfiberpair g y (idpath _ )). unfold isweq. intro xe.
set (is3:= isweqezmap1 _ _ _ ( fibseqhf f g z ye ) xe).
assert (w1: weq (paths (hfibersgftog f g z xe) ye) (hfiber (hfibersftogf f g z ye) xe)). split with (ezmap (d1 (hfibersftogf f g z ye) (hfibersgftog f g z) ye ( fibseqhf f g z ye ) xe) (hfibersftogf f g z ye) xe ( fibseq1 (hfibersftogf f g z ye) (hfibersgftog f g z) ye ( fibseqhf f g z ye ) xe) ). apply is3. apply (iscontrweqf w1 ).
assert (is4: iscontr (hfiber g z)). apply iscontrhfiberofincl. assumption.
apply ( isapropifcontr is4 ). Defined.

Basics about types of h-level 2 - "sets"


Definition isaset ( X : UU ) : UU := forall x x' : X , isaprop ( paths x x' ) .

Lemma isasetunit : isaset unit .
Proof . apply ( isofhlevelcontr 2 iscontrunit ) . Defined .

Lemma isasetempty : isaset empty .
Proof. apply ( isofhlevelsnprop 1 isapropempty ) . Defined .

The following lemma assert "uniqueness of identity proofs" (uip) for sets.

Lemma uip { X : UU } ( is : isaset X ) { x x' : X } ( e e' : paths x x' ) : paths e e' .
Proof. intros . apply ( proofirrelevance _ ( is x x' ) e e' ) . Defined .

For the theorem about the coproduct of two sets see isasetcoprod below.

Lemma isasetdirprod ( X Y : UU ) ( isx : isaset X ) ( isy : isaset Y ) : isaset ( dirprod X Y ) .
Proof. intros . apply ( isofhleveldirprod 2 _ _ isx isy ) . Defined .

Lemma isofhlevelssnset (n:nat) ( X : UU ) ( is : isaset X ) : isofhlevel ( S (S n) ) X.
Proof. intros n X X0. simpl. unfold isaset in X0. intros x x' . apply isofhlevelsnprop. set ( int := X0 x x'). assumption . Defined.

Lemma isasetifiscontrloops (X:UU): (forall x:X, iscontr (paths x x)) -> isaset X.
Proof. intros X X0. unfold isaset. unfold isofhlevel. intros x x' x0 x0' . destruct x0. set (is:= X0 x). apply isapropifcontr. assumption. Defined.

Lemma iscontrloopsifisaset (X:UU): (isaset X) -> (forall x:X, iscontr (paths x x)).
Proof. intros X X0 x. unfold isaset in X0. unfold isofhlevel in X0. change (forall (x x' : X) (x0 x'0 : paths x x'), iscontr (paths x0 x'0)) with (forall (x x':X), isaprop (paths x x')) in X0. apply (iscontraprop1 (X0 x x) (idpath x)). Defined.

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.
Proof. intros. apply (isofhlevelsninclb (S O) f is2). apply is1. Defined.

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 ( @pr21 _ _ ).
Proof. intros. apply isofhlevelfhfiberpr21. assumption. Defined.

Criterion for a function between sets being an inclusion.

Theorem isinclbetweensets { X Y : UU } ( f : X -> Y ) ( isx : isaset X ) ( isy : isaset Y ) ( inj : forall x x' : X , ( paths ( f x ) ( f x' ) -> paths x x' ) ) : isincl f .
Proof. intros . apply isinclweqonpaths . intros x x' . apply ( isweqimplimpl ( @maponpaths _ _ f x x' ) ( inj x x' ) ( isx x x' ) ( isy ( f x ) ( f x' ) ) ) . Defined .

A map from unit to a set is an inclusion.

Theorem isinclfromunit { X : UU } ( f : unit -> X ) ( is : isaset X ) : isincl f .
Proof. intros . apply ( isinclbetweensets f ( isofhlevelcontr 2 ( iscontrunit ) ) is ) . intros . destruct x . destruct x' . apply idpath . Defined .

Isolated points and types with decidable equality.


Basic results on complements to a point


Definition compl ( X : UU ) ( x : X ):= total2 (fun x':X => neg (paths x x' ) ) .
Definition complpair ( X : UU ) ( x : X ) := tpair (fun x':X => neg (paths x x' ) ) .
Definition pr21compl ( X : UU ) ( x : X ) := @pr21 _ (fun x':X => neg (paths x x' ) ) .

Lemma isinclpr21compl ( X : UU ) ( x : X ) : isincl ( pr21compl X x ) .
Proof. intros . apply ( isinclpr21 _ ( fun x' : X => isapropneg _ ) ) . Defined.

Definition recompl ( X : UU ) (x:X): coprod (compl X x) unit -> X := fun u:_ =>
match u with
ii1 x0 => pr21 x0|
ii2 t => x
end.

Definition maponcomplincl { X Y : UU } (f:X -> Y)(is: isincl f)(x:X): compl X x -> compl Y (f x):= fun x0':_ =>
match x0' with
tpair x' neqx => tpair _ (f x') (negf (invmaponpathsincl _ is x x' ) neqx)
end.

Definition maponcomplweq { X Y : UU } (f : weq X Y ) (x:X):= maponcomplincl f (isofhlevelfweq (S O) f ) x.

Theorem isweqmaponcompl { X Y : UU } ( f : weq X Y ) (x:X): isweq (maponcomplweq f x).
Proof. intros. set (is1:= isofhlevelfweq (S O) f). set (map1:= totalfun (fun x':X => neg (paths x x' )) (fun x':X => neg (paths (f x) (f x'))) (fun x':X => negf (invmaponpathsincl _ is1 x x' ))). set (map2:= fpmap f (fun y:Y => neg (paths (f x) y ))).
assert (is2: forall x':X, isweq (negf (invmaponpathsincl _ is1 x x'))). intro.
set (invimpll:= (negf (@maponpaths _ _ f x x'))). apply (isweqimplimpl (negf (invmaponpathsincl _ is1 x x')) (negf (@maponpaths _ _ f x x')) (isapropneg _) (isapropneg _)).
assert (is3: isweq map1). unfold map1 . apply ( isweqfibtototal _ _ (fun x':X => weqpair _ ( is2 x' )) ) .
assert (is4: isweq map2). apply (isweqfpmap f (fun y:Y => neg (paths (f x) y )) ).
assert (h: forall x0':_, paths (map2 (map1 x0')) (maponcomplweq f x x0')). intro. simpl. destruct x0'. simpl. apply idpath.
apply (isweqhomot _ _ h (twooutof3c _ _ is3 is4)).
Defined.

Definition weqoncompl { X Y : UU } (w: weq X Y) ( x : X ) : weq (compl X x) (compl Y (pr21 w x)):= weqpair _ (isweqmaponcompl w x).

Definition homotweqoncomplcomp { X Y Z : UU } ( f : weq X Y ) ( g : weq Y Z ) ( x : X ) : homot ( weqcomp ( weqoncompl f x ) ( weqoncompl g ( f x ) ) ) ( weqoncompl ( weqcomp f g ) x ) .
Proof . intros . intro x' . destruct x' as [ x' nexx' ] . apply ( invmaponpathsincl _ ( isinclpr21compl Z _ ) _ _ ) . simpl . apply idpath . Defined .

Basic results on types with an isolated point.


Definition isisolated (X:UU)(x:X):= forall x':X, coprod (paths x x' ) (paths x x' -> empty).

Definition isolated ( T : UU ) := total2 ( fun t : T => isisolated T t ) .
Definition isolatedpair ( T : UU ) := tpair ( fun t : T => isisolated T t ) .
Definition pr21isolated ( T : UU ) := fun x : isolated T => pr21 x .

Theorem isaproppathsfromisolated ( X : UU ) ( x : X ) ( is : isisolated X x ) : forall x' : X, isaprop ( paths x x' ) .
Proof. intros . apply iscontraprop1inv . intro e . destruct e .
set (f:= fun e: paths x x => coconusfromtpair _ e).
assert (is' : isweq f). apply (onefiber (fun x':X => paths x x' ) x (fun x':X => is x' )).
assert (is2: iscontr (coconusfromt _ x)). apply iscontrcoconusfromt.
apply (iscontrweqb ( weqpair f is' ) ). assumption. Defined.

Theorem isaproppathstoisolated ( X : UU ) ( x : X ) ( is : isisolated X x ) : forall x' : X, isaprop ( paths x' x ) .
Proof . intros . apply ( isofhlevelweqf 1 ( weqpathsinv0 x x' ) ( isaproppathsfromisolated X x is x' ) ) . Defined .

Lemma isisolatedweqf { X Y : UU } ( f : weq X Y ) (x:X) (is2: isisolated _ x) : isisolated _ (f x).
Proof. intros. unfold isisolated. intro y. set (g:=invmap f ). set (x':= g y). destruct (is2 x') as [ x0 | y0 ]. apply (ii1 (pathsweq1' f x y x0) ).
assert (phi: paths y (f x) -> empty).
assert (psi: (paths (g y) x -> empty) -> (paths y (f x) -> empty)). intros X0 X1. apply (X0 (pathsinv0 (pathsweq1 f x y (pathsinv0 X1)))). apply (psi ( ( negf ( @pathsinv0 _ _ _ ) ) y0) ) . apply (ii2 ( negf ( @pathsinv0 _ _ _ ) phi ) ). Defined.

Theorem isisolatedinclb { X Y : UU } ( f : X -> Y ) ( is : isincl f ) ( x : X ) ( is0 : isisolated _ ( f x ) ) : isisolated _