Library uu0c
Univalent Basics. Vladimir Voevodsky. Feb. 2010 - Sep. 2011. Port to coq trunk (8.4-8.5) in
March 2014. The third part of the original uu0 file, created on Dec. 3, 2014.Preambule
Unset Automatic Introduction.
Imports
Require Export Foundations.Generalities.uu0b.
Axiom funextempty : forall ( X : UU ) ( f g : X -> empty ) , paths f g .
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.
induction x as [ x0 | y0 ]. induction x' as [ x | y ]. apply (maponpaths (fun x:X => ii1 x) (X1 x0 x)).
apply (fromempty (y x0)).
induction 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.
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 pr1compl ( X : UU ) ( x : X ) := @pr1 _ (fun x':X => neg (paths x x' ) ) .
Lemma isinclpr1compl ( X : UU ) ( x : X ) : isincl ( pr1compl X x ) .
Proof. intros . apply ( isinclpr1 _ ( fun x' : X => isapropneg _ ) ) . Defined.
Definition recompl ( X : UU ) (x:X): coprod (compl X x) unit -> X := fun u:_ =>
match u with
ii1 x0 => pr1 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. induction 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 (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' . induction x' as [ x' nexx' ] . apply ( invmaponpathsincl _ ( isinclpr1compl Z _ ) _ _ ) . simpl . apply idpath . Defined .
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 pr1isolated ( T : UU ) := fun x : isolated T => pr1 x .
Theorem isaproppathsfromisolated ( X : UU ) ( x : X ) ( is : isisolated X x ) : forall x' : X, isaprop ( paths x x' ) .
Proof. intros . apply iscontraprop1inv . intro e . induction 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). induction (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 _ x .
Proof. intros . unfold isisolated . intro x' . set ( a := is0 ( f x' ) ) . induction a as [ a1 | a2 ] . apply ( ii1 ( invmaponpathsincl f is _ _ a1 ) ) . apply ( ii2 ( ( negf ( @maponpaths _ _ f _ _ ) ) a2 ) ) . Defined.
Lemma disjointl1 (X:UU): isisolated (coprod X unit) (ii2 tt).
Proof. intros. unfold isisolated. intros x' . induction x' as [ x | u ] . apply (ii2 (negpathsii2ii1 x tt )). induction u. apply (ii1 (idpath _ )). Defined.
Weak equivalence weqrecompl from the coproduct of the complement to an isolated point with unit and the original type
Definition invrecompl (X:UU)(x:X)(is: isisolated X x): X -> coprod (compl X x) unit:=
fun x':X => match (is x') with
ii1 e => ii2 tt|
ii2 phi => ii1 (complpair _ _ x' phi)
end.
Theorem isweqrecompl (X:UU)(x:X)(is:isisolated X x): isweq (recompl _ x).
Proof. intros. set (f:= recompl _ x). set (g:= invrecompl X x is). unfold invrecompl in g. simpl in g.
assert (efg: forall x':X, paths (f (g x')) x'). intro. induction (is x') as [ x0 | e ]. induction x0. unfold f. unfold g. simpl. unfold recompl. simpl. induction (is x) as [ x0 | e ] . simpl. apply idpath. induction (e (idpath x)). unfold f. unfold g. simpl. unfold recompl. simpl. induction (is x') as [ x0 | e0 ]. induction (e x0). simpl. apply idpath.
assert (egf: forall u: coprod (compl X x) unit, paths (g (f u)) u). unfold isisolated in is. intro. induction (is (f u)) as [ p | e ] . induction u as [ c | u]. simpl. induction c as [ t x0 ]. simpl in p. induction (x0 p).
induction u.
assert (e1: paths (g (f (ii2 tt))) (g x)). apply (maponpaths g p).
assert (e2: paths (g x) (ii2 tt)). unfold g. induction (is x) as [ i | e ]. apply idpath. induction (e (idpath x)). apply (pathscomp0 e1 e2). induction u as [ c | u ] . simpl. induction c as [ t x0 ]. simpl. unfold isisolated in is. unfold g. induction (is t) as [ p | e0 ] . induction (x0 p). simpl in g.
unfold f. unfold recompl. simpl in e.
assert (ee: paths e0 x0). apply (proofirrelevance _ (isapropneg (paths x t))). induction ee. apply idpath.
unfold f. unfold g. simpl. induction u. induction (is x). apply idpath. induction (e (idpath x)).
apply (gradth f g egf efg). Defined.
Definition weqrecompl ( X : UU ) ( x : X ) ( is : isisolated _ x ) : weq ( coprod ( compl X x ) unit ) X := weqpair _ ( isweqrecompl X x is ) .
Theorem homotrecomplnat { X Y : UU } ( w : weq X Y ) ( x : X ) : forall a : coprod ( compl X x ) unit , paths ( recompl Y ( w x ) ( coprodf ( maponcomplweq w x ) ( fun x: unit => x ) a ) ) ( w ( recompl X x a ) ) .
Proof . intros . induction a as [ ane | t ] . induction ane as [ a ne ] . simpl . apply idpath . induction t . simpl . apply idpath . Defined .
Definition recomplf { X Y : UU } ( x : X ) ( y : Y ) ( isx : isisolated X x ) ( f : compl X x -> compl Y y ) := funcomp ( funcomp ( invmap ( weqrecompl X x isx ) ) ( coprodf f ( idfun unit ) ) ) ( recompl Y y ) .
Definition weqrecomplf { X Y : UU } ( x : X ) ( y : Y ) ( isx : isisolated X x ) ( isy : isisolated Y y ) ( w : weq ( compl X x ) ( compl Y y ) ) := weqcomp ( weqcomp ( invweq ( weqrecompl X x isx ) ) ( weqcoprodf w ( idweq unit ) ) ) ( weqrecompl Y y isy ) .
Definition homotrecomplfhomot { X Y : UU } ( x : X ) ( y : Y ) ( isx : isisolated X x ) ( f f' : compl X x -> compl Y y ) ( h : homot f f' ) : homot ( recomplf x y isx f ) ( recomplf x y isx f') .
Proof . intros. intro a . unfold recomplf . apply ( maponpaths ( recompl Y y ) ( homotcoprodfhomot _ _ _ _ h ( fun t : unit => idpath t ) (invmap (weqrecompl X x isx) a) ) ) . Defined .
Lemma pathsrecomplfxtoy { X Y : UU } ( x : X ) ( y : Y ) ( isx : isisolated X x ) ( f : compl X x -> compl Y y ) : paths ( recomplf x y isx f x ) y .
Proof . intros . unfold recomplf . unfold weqrecompl . unfold invmap . simpl . unfold invrecompl . unfold funcomp . induction ( isx x ) as [ i1 | i2 ] . simpl . apply idpath . induction ( i2 ( idpath _ ) ) . Defined .
Definition homotrecomplfcomp { X Y Z : UU } ( x : X ) ( y : Y ) ( z : Z ) ( isx : isisolated X x ) ( isy : isisolated Y y ) ( f : compl X x -> compl Y y ) ( g : compl Y y -> compl Z z ) : homot ( funcomp ( recomplf x y isx f ) ( recomplf y z isy g ) ) ( recomplf x z isx ( funcomp f g ) ) .
Proof . intros. intro x' . unfold recomplf . set ( e := homotinvweqweq ( weqrecompl Y y isy ) (coprodf f ( idfun unit) (invmap ( weqrecompl X x isx ) x')) ) . unfold funcomp . simpl in e . simpl . rewrite e . set ( e' := homotcoprodfcomp f ( idfun unit ) g ( idfun unit ) (invmap (weqrecompl X x isx) x') ) . unfold funcomp in e' . rewrite e' . apply idpath . Defined .
Definition homotrecomplfidfun { X : UU } ( x : X ) ( isx : isisolated X x ) : homot ( recomplf x x isx ( idfun ( compl X x ) ) ) ( idfun _ ) .
Proof . intros . intro x' . unfold recomplf . unfold weqrecompl . unfold invmap . simpl . unfold invrecompl . unfold funcomp. induction ( isx x' ) as [ e | ne ] . simpl . apply e . simpl . apply idpath . Defined .
Lemma ishomotinclrecomplf { X Y : UU } ( x : X ) ( y : Y ) ( isx : isisolated X x ) ( f : compl X x -> compl Y y ) ( x'n : compl X x ) ( y'n : compl Y y ) ( e : paths ( recomplf x y isx f ( pr1 x'n ) ) ( pr1 y'n ) ) : paths ( f x'n ) y'n .
Proof . intros . induction x'n as [ x' nexx' ] . induction y'n as [ y' neyy' ] . simpl in e . apply ( invmaponpathsincl _ ( isinclpr1compl _ _ ) ) . simpl . rewrite ( pathsinv0 e ) . unfold recomplf. unfold invmap . unfold coprodf . simpl . unfold funcomp . unfold invrecompl . induction ( isx x' ) as [ exx' | nexx'' ] . induction ( nexx' exx' ) . simpl . assert ( ee : paths nexx' nexx'' ) . apply ( proofirrelevance _ ( isapropneg _ ) ) . rewrite ee . apply idpath . Defined .
Definition funtranspos0 { T : UU } ( t1 t2 : T ) ( is2 : isisolated T t2 ) ( x :compl T t1 ) : compl T t2 := match ( is2 ( pr1 x ) ) with
ii1 e => match ( is2 t1 ) with ii1 e' => fromempty ( pr2 x ( pathscomp0 ( pathsinv0 e' ) e ) ) | ii2 ne' => complpair T t2 t1 ne' end |
ii2 ne => complpair T t2 ( pr1 x ) ne end .
Definition homottranspos0t2t1t1t2 { T : UU } ( t1 t2 : T ) ( is1 : isisolated T t1 ) ( is2 : isisolated T t2 ) : homot ( funcomp ( funtranspos0 t1 t2 is2 ) ( funtranspos0 t2 t1 is1 ) ) ( idfun _ ) .
Proof. intros. intro x . unfold funtranspos0 . unfold funcomp . induction x as [ t net1 ] . simpl . induction ( is2 t ) as [ et2 | net2 ] . induction ( is2 t1 ) as [ et2t1 | net2t1 ] . induction (net1 (pathscomp0 (pathsinv0 et2t1) et2)) . simpl . induction ( is1 t1 ) as [ e | ne ] . induction ( is1 t2 ) as [ et1t2 | net1t2 ] . induction (net2t1 (pathscomp0 (pathsinv0 et1t2) e)) . apply ( invmaponpathsincl _ ( isinclpr1compl _ _ ) _ _ ) . simpl . apply et2 . induction ( ne ( idpath _ ) ) . simpl . induction ( is1 t ) as [ et1t | net1t ] . induction ( net1 et1t ) . apply ( invmaponpathsincl _ ( isinclpr1compl _ _ ) _ _ ) . simpl . apply idpath . Defined .
Definition weqtranspos0 { T : UU } ( t1 t2 : T ) ( is1 : isisolated T t1 ) ( is2 : isisolated T t2 ) : weq ( compl T t1 ) ( compl T t2 ) .
Proof . intros . set ( f := funtranspos0 t1 t2 is2 ) . set ( g := funtranspos0 t2 t1 is1 ) . split with f .
assert ( egf : forall x : _ , paths ( g ( f x ) ) x ) . intro x . apply ( homottranspos0t2t1t1t2 t1 t2 is1 is2 ) .
assert ( efg : forall x : _ , paths ( f ( g x ) ) x ) . intro x . apply ( homottranspos0t2t1t1t2 t2 t1 is2 is1 ) .
apply ( gradth _ _ egf efg ) . Defined .
Definition funtranspos { T : UU } ( t1 t2 : isolated T ) : T -> T := recomplf ( pr1 t1 ) ( pr1 t2 ) ( pr2 t1 ) ( funtranspos0 ( pr1 t1 ) ( pr1 t2 ) ( pr2 t2 ) ) .
Definition homottranspost2t1t1t2 { T : UU } ( t1 t2 : T ) ( is1 : isisolated T t1 ) ( is2 : isisolated T t2 ) : homot ( funcomp ( funtranspos ( tpair _ t1 is1 ) ( tpair _ t2 is2 ) ) ( funtranspos ( tpair _ t2 is2 ) ( tpair _ t1 is1 ) ) ) ( idfun _ ) .
Proof. intros. intro t . unfold funtranspos . rewrite ( homotrecomplfcomp t1 t2 t1 is1 is2 _ _ t ) . set ( e:= homotrecomplfhomot t1 t1 is1 _ ( idfun _ ) ( homottranspos0t2t1t1t2 t1 t2 is1 is2 ) t ) . set ( e' := homotrecomplfidfun t1 is1 t ) . apply ( pathscomp0 e e' ) . Defined .
Theorem weqtranspos { T : UU } ( t1 t2 : T ) ( is1 : isisolated T t1 ) ( is2 : isisolated T t2 ) : weq T T .
Proof . intros . set ( f := funtranspos ( tpair _ t1 is1) ( tpair _ t2 is2 ) ) . set ( g := funtranspos ( tpair _ t2 is2 ) ( tpair _ t1 is1 ) ) . split with f .
assert ( egf : forall t : T , paths ( g ( f t ) ) t ) . intro . apply homottranspost2t1t1t2 .
assert ( efg : forall t : T , paths ( f ( g t ) ) t ) . intro . apply homottranspost2t1t1t2 .
apply ( gradth _ _ egf efg ) . Defined .
Lemma pathsfuntransposoft1 { T : UU } ( t1 t2 : T ) ( is1 : isisolated T t1 ) ( is2 : isisolated T t2 ) : paths ( funtranspos ( tpair _ t1 is1 ) ( tpair _ t2 is2 ) t1 ) t2 .
Proof . intros . unfold funtranspos . rewrite ( pathsrecomplfxtoy t1 t2 is1 _ ) . apply idpath . Defined .
Lemma pathsfuntransposoft2 { T : UU } ( t1 t2 : T ) ( is1 : isisolated T t1 ) ( is2 : isisolated T t2 ) : paths ( funtranspos ( tpair _ t1 is1 ) ( tpair _ t2 is2 ) t2 ) t1 .
Proof . intros . unfold funtranspos . simpl . unfold funtranspos0 . unfold recomplf . unfold funcomp . unfold coprodf . unfold invmap . unfold weqrecompl . unfold recompl . simpl . unfold invrecompl . induction ( is1 t2 ) as [ et1t2 | net1t2 ] . apply ( pathsinv0 et1t2 ) . simpl . induction ( is2 t2 ) as [ et2t2 | net2t2 ] . induction ( is2 t1 ) as [ et2t1 | net2t1 ] . induction (net1t2 (pathscomp0 (pathsinv0 et2t1) et2t2) ). simpl . apply idpath . induction ( net2t2 ( idpath _ ) ) . Defined .
Lemma pathsfuntransposofnet1t2 { T : UU } ( t1 t2 : T ) ( is1 : isisolated T t1 ) ( is2 : isisolated T t2 ) ( t : T ) ( net1t : neg ( paths t1 t ) ) ( net2t : neg ( paths t2 t ) ) : paths ( funtranspos ( tpair _ t1 is1 ) ( tpair _ t2 is2 ) t ) t .
Proof . intros . unfold funtranspos . simpl . unfold funtranspos0 . unfold recomplf . unfold funcomp . unfold coprodf . unfold invmap . unfold weqrecompl . unfold recompl . simpl . unfold invrecompl . induction ( is1 t ) as [ et1t | net1t' ] . induction ( net1t et1t ) . simpl . induction ( is2 t ) as [ et2t | net2t' ] . induction ( net2t et2t ) . simpl . apply idpath . Defined .
Lemma homotfuntranspos2 { T : UU } ( t1 t2 : T ) ( is1 : isisolated T t1 ) ( is2 : isisolated T t2 ) : homot ( funcomp ( funtranspos ( tpair _ t1 is1 ) ( tpair _ t2 is2 ) ) ( funtranspos ( tpair _ t1 is1 ) ( tpair _ t2 is2 ) ) ) ( idfun _ ) .
Proof . intros . intro t . unfold funcomp . unfold idfun .
induction ( is1 t ) as [ et1t | net1t ] . rewrite ( pathsinv0 et1t ) . rewrite ( pathsfuntransposoft1 _ _ ) . rewrite ( pathsfuntransposoft2 _ _ ) . apply idpath .
induction ( is2 t ) as [ et2t | net2t ] . rewrite ( pathsinv0 et2t ) . rewrite ( pathsfuntransposoft2 _ _ ) . rewrite ( pathsfuntransposoft1 _ _ ) . apply idpath .
rewrite ( pathsfuntransposofnet1t2 _ _ _ _ _ net1t net2t ) . rewrite ( pathsfuntransposofnet1t2 _ _ _ _ _ net1t net2t ) . apply idpath . Defined .
Definition isdeceq (X:UU) : UU := forall (x x':X), coprod (paths x x' ) (paths x x' -> empty).
Lemma isdeceqweqf { X Y : UU } ( w : weq X Y ) ( is : isdeceq X ) : isdeceq Y .
Proof. intros . intros y y' . set ( w' := weqonpaths ( invweq w ) y y' ) . set ( int := is ( ( invweq w ) y ) ( ( invweq w ) y' ) ) . induction int as [ i | ni ] . apply ( ii1 ( ( invweq w' ) i ) ) . apply ( ii2 ( ( negf w' ) ni ) ) . Defined .
Lemma isdeceqweqb { X Y : UU } ( w : weq X Y ) ( is : isdeceq Y ) : isdeceq X .
Proof . intros . apply ( isdeceqweqf ( invweq w ) is ) . Defined .
Theorem isdeceqinclb { X Y : UU } ( f : X -> Y ) ( is : isdeceq Y ) ( is' : isincl f ) : isdeceq X .
Proof. intros . intros x x' . set ( w := weqonpathsincl f is' x x' ) . set ( int := is ( f x ) ( f x' ) ) . induction int as [ i | ni ] . apply ( ii1 ( ( invweq w ) i ) ) . apply ( ii2 ( ( negf w ) ni ) ) . Defined .
Lemma isdeceqifisaprop ( X : UU ) : isaprop X -> isdeceq X .
Proof. intros X is . intros x x' . apply ( ii1 ( proofirrelevance _ is x x' ) ) . Defined .
Theorem isasetifdeceq (X:UU): isdeceq X -> isaset X.
Proof. intro X . intro is. intros x x' . apply ( isaproppathsfromisolated X x ( is x ) ) . Defined .
Definition booleq { X : UU } ( is : isdeceq X ) ( x x' : X ) : bool .
Proof . intros . induction ( is x x' ) . apply true . apply false . Defined .
Lemma eqfromdnegeq (X:UU)(is: isdeceq X)(x x':X): dneg ( paths x x' ) -> paths x x'.
Proof. intros X is x x' X0. induction ( is x x' ) as [ y | n ] . assumption . induction ( X0 n ) . Defined .
Theorem isdeceqbool: isdeceq bool.
Proof. unfold isdeceq. intros x' x . induction x. induction x'. apply (ii1 (idpath true)). apply (ii2 nopathsfalsetotrue). induction x'. apply (ii2 nopathstruetofalse). apply (ii1 (idpath false)). Defined.
Theorem isasetbool: isaset bool.
Proof. apply (isasetifdeceq _ isdeceqbool). Defined.
Definition subsetsplit { X : UU } ( f : X -> bool ) ( x : X ) : coprod ( hfiber f true ) ( hfiber f false ) .
Proof . intros . induction ( boolchoice ( f x ) ) as [ a | b ] . apply ( ii1 ( hfiberpair f x a ) ) . apply ( ii2 ( hfiberpair f x b ) ) . Defined .
Definition subsetsplitinv { X : UU } ( f : X -> bool ) ( ab : coprod (hfiber f true) (hfiber f false) ) : X := match ab with ii1 xt => pr1 xt | ii2 xf => pr1 xf end.
Theorem weqsubsetsplit { X : UU } ( f : X -> bool ) : weq X (coprod ( hfiber f true) ( hfiber f false) ) .
Proof . intros . set ( ff := subsetsplit f ) . set ( gg := subsetsplitinv f ) . split with ff .
assert ( egf : forall a : _ , paths ( gg ( ff a ) ) a ) . intros . unfold ff . unfold subsetsplit . induction ( boolchoice ( f a ) ) as [ et | ef ] . simpl . apply idpath . simpl . apply idpath .
assert ( efg : forall a : _ , paths ( ff ( gg a ) ) a ) . intros . induction a as [ et | ef ] . induction et as [ x et' ] . simpl . unfold ff . unfold subsetsplit . induction ( boolchoice ( f x ) ) as [ e1 | e2 ] . apply ( maponpaths ( @ii1 _ _ ) ) . apply ( maponpaths ( hfiberpair f x ) ) . apply uip . apply isasetbool . induction ( nopathstruetofalse ( pathscomp0 ( pathsinv0 et' ) e2 ) ) . induction ef as [ x et' ] . simpl . unfold ff . unfold subsetsplit . induction ( boolchoice ( f x ) ) as [ e1 | e2 ] . induction ( nopathsfalsetotrue ( pathscomp0 ( pathsinv0 et' ) e1 ) ) . apply ( maponpaths ( @ii2 _ _ ) ) . apply ( maponpaths ( hfiberpair f x ) ) . apply uip . apply isasetbool .
apply ( gradth _ _ egf efg ) . Defined .
Definition eqbx ( X : UU ) ( x : X ) ( is : isisolated X x ) : X -> bool .
Proof. intros X x is x' . induction ( is x' ) . apply true . apply false . Defined .
Lemma iscontrhfibereqbx ( X : UU ) ( x : X ) ( is : isisolated X x ) : iscontr ( hfiber ( eqbx X x is ) true ) .
Proof. intros . assert ( b : paths ( eqbx X x is x ) true ) . unfold eqbx . induction ( is x ) as [ e | ne ] . apply idpath . induction ( ne ( idpath _ ) ) . set ( i := hfiberpair ( eqbx X x is ) x b ) . split with i .
unfold eqbx . induction ( boolchoice ( eqbx X x is x ) ) as [ b' | nb' ] . intro t . induction t as [ x' e ] . assert ( e' : paths x' x ) . induction ( is x' ) as [ ee | nee ] . apply ( pathsinv0 ee ) . induction ( nopathsfalsetotrue e ) . apply ( invmaponpathsincl _ ( isinclfromhfiber ( eqbx X x is ) isasetbool true ) ( hfiberpair _ x' e ) i e' ) . induction ( nopathstruetofalse ( pathscomp0 ( pathsinv0 b ) nb' ) ) . Defined .
Definition bhfiber { X Y : UU } ( f : X -> Y ) ( y : Y ) ( is : isisolated Y y ) := hfiber ( fun x : X => eqbx Y y is ( f x ) ) true .
Lemma weqhfibertobhfiber { X Y : UU } ( f : X -> Y ) ( y : Y ) ( is : isisolated Y y ) : weq ( hfiber f y ) ( bhfiber f y is ) .
Proof . intros . set ( g := eqbx Y y is ) . set ( ye := pr1 ( iscontrhfibereqbx Y y is ) ) . split with ( hfibersftogf f g true ye ) . apply ( isofhlevelfffromZ 0 _ _ ye ( fibseqhf f g true ye ) ) . apply ( isapropifcontr ) . apply ( iscontrhfibereqbx _ y is ) . Defined .
Theorem isinclii1 (X Y:UU): isincl (@ii1 X Y).
Proof. intros. set (f:= @ii1 X Y). set (g:= coprodtoboolsum X Y). set (gf:= fun x:X => (g (f x))). set (gf':= fun x:X => tpair (boolsumfun X Y) true x).
assert (h: forall x:X , paths (gf' x) (gf x)). intro. apply idpath.
assert (is1: isofhlevelf (S O) gf'). apply (isofhlevelfsnfib O (boolsumfun X Y) true (isasetbool true true)).
assert (is2: isofhlevelf (S O) gf). apply (isofhlevelfhomot (S O) gf' gf h is1).
apply (isofhlevelff (S O) _ _ is2 (isofhlevelfweq (S (S O) ) (weqcoprodtoboolsum X Y))). Defined.
Corollary iscontrhfiberii1x ( X Y : UU ) ( x : X ) : iscontr ( hfiber ( @ii1 X Y ) ( ii1 x ) ) .
Proof. intros . set ( xe1 := hfiberpair ( @ii1 _ _ ) x ( idpath ( @ii1 X Y x ) ) ) . apply ( iscontraprop1 ( isinclii1 X Y ( ii1 x ) ) xe1 ) . Defined .
Corollary neghfiberii1y ( X Y : UU ) ( y : Y ) : neg ( hfiber ( @ii1 X Y ) ( ii2 y ) ) .
Proof. intros . intro xe . induction xe as [ x e ] . apply ( negpathsii1ii2 _ _ e ) . Defined.
Theorem isinclii2 (X Y:UU): isincl (@ii2 X Y).
Proof. intros. set (f:= @ii2 X Y). set (g:= coprodtoboolsum X Y). set (gf:= fun y:Y => (g (f y))). set (gf':= fun y:Y => tpair (boolsumfun X Y) false y).
assert (h: forall y:Y , paths (gf' y) (gf y)). intro. apply idpath.
assert (is1: isofhlevelf (S O) gf'). apply (isofhlevelfsnfib O (boolsumfun X Y) false (isasetbool false false)).
assert (is2: isofhlevelf (S O) gf). apply (isofhlevelfhomot (S O) gf' gf h is1).
apply (isofhlevelff (S O) _ _ is2 (isofhlevelfweq (S (S O)) ( weqcoprodtoboolsum X Y))). Defined.
Corollary iscontrhfiberii2y ( X Y : UU ) ( y : Y ) : iscontr ( hfiber ( @ii2 X Y ) ( ii2 y ) ) .
Proof. intros . set ( xe1 := hfiberpair ( @ii2 _ _ ) y ( idpath ( @ii2 X Y y ) ) ) . apply ( iscontraprop1 ( isinclii2 X Y ( ii2 y ) ) xe1 ) . Defined .
Corollary neghfiberii2x ( X Y : UU ) ( x : X ) : neg ( hfiber ( @ii2 X Y ) ( ii1 x ) ) .
Proof. intros . intro ye . induction ye as [ y e ] . apply ( negpathsii2ii1 _ _ e ) . Defined.
Lemma negintersectii1ii2 { X Y : UU } (z: coprod X Y): hfiber (@ii1 X Y) z -> hfiber (@ii2 _ _) z -> empty.
Proof. intros X Y z X0 X1. induction X0 as [ t x ]. induction X1 as [ t0 x0 ].
set (e:= pathscomp0 x (pathsinv0 x0)). apply (negpathsii1ii2 _ _ e). Defined.
Lemma isolatedtoisolatedii1 (X Y:UU)(x:X)(is:isisolated _ x): isisolated ( coprod X Y ) (ii1 x).
Proof. intros. unfold isisolated . intro x' . induction x' as [ x0 | y ] . induction (is x0) as [ p | e ] . apply (ii1 (maponpaths (@ii1 X Y) p)). apply (ii2 (negf (invmaponpathsincl (@ii1 X Y) (isinclii1 X Y) _ _ ) e)). apply (ii2 (negpathsii1ii2 x y)). Defined.
Lemma isolatedtoisolatedii2 (X Y:UU)(y:Y)(is:isisolated _ y): isisolated ( coprod X Y ) (ii2 y).
Proof. intros. intro x' . induction x' as [ x | y0 ] . apply (ii2 (negpathsii2ii1 x y)). induction (is y0) as [ p | e ] . apply (ii1 (maponpaths (@ii2 X Y) p)). apply (ii2 (negf (invmaponpathsincl (@ii2 X Y) (isinclii2 X Y) _ _ ) e)). Defined.
Theorem weqhfibercoprodf1 { X Y X' Y' : UU } (f: X -> X')(g:Y -> Y')(x':X'): weq (hfiber f x') (hfiber (coprodf f g) (ii1 x')).
Proof. intros. set ( ix := @ii1 X Y ) . set ( ix' := @ii1 X' Y' ) . set ( fpg := coprodf f g ) . set ( fpgix := fun x : X => ( fpg ( ix x ) ) ) .
assert ( w1 : weq ( hfiber f x' ) ( hfiber fpgix ( ix' x' ) ) ) . apply ( samehfibers f ix' ( isinclii1 _ _ ) x' ) .
assert ( w2 : weq ( hfiber fpgix ( ix' x' ) ) ( hfiber fpg ( ix' x' ) ) ) . split with (hfibersgftog ix fpg ( ix' x' ) ) . unfold isweq. intro y .
set (u:= invezmaphf ix fpg ( ix' x' ) y).
assert (is: isweq u). apply isweqinvezmaphf.
apply (iscontrweqb ( weqpair u is ) ) . induction y as [ xy e ] . induction xy as [ x0 | y0 ] . simpl . apply iscontrhfiberofincl . apply ( isinclii1 X Y ) . apply ( fromempty ( ( negpathsii2ii1 x' ( g y0 ) ) e ) ) .
apply ( weqcomp w1 w2 ) .
Defined.
Theorem weqhfibercoprodf2 { X Y X' Y' : UU } (f: X -> X')(g:Y -> Y')(y':Y'): weq (hfiber g y') (hfiber (coprodf f g) (ii2 y')).
Proof. intros. set ( iy := @ii2 X Y ) . set ( iy' := @ii2 X' Y' ) . set ( fpg := coprodf f g ) . set ( fpgiy := fun y : Y => ( fpg ( iy y ) ) ) .
assert ( w1 : weq ( hfiber g y' ) ( hfiber fpgiy ( iy' y' ) ) ) . apply ( samehfibers g iy' ( isinclii2 _ _ ) y' ) .
assert ( w2 : weq ( hfiber fpgiy ( iy' y' ) ) ( hfiber fpg ( iy' y' ) ) ) . split with (hfibersgftog iy fpg ( iy' y' ) ) . unfold isweq. intro y .
set (u:= invezmaphf iy fpg ( iy' y' ) y).
assert (is: isweq u). apply isweqinvezmaphf.
apply (iscontrweqb ( weqpair u is ) ) . induction y as [ xy e ] . induction xy as [ x0 | y0 ] . simpl . apply ( fromempty ( ( negpathsii1ii2 ( f x0 ) y' ) e ) ) . simpl. apply iscontrhfiberofincl . apply ( isinclii2 X Y ) .
apply ( weqcomp w1 w2 ) .
Defined.
Theorem isofhlevelfcoprodf (n:nat) { X Y Z T : UU } (f : X -> Z ) ( g : Y -> T )( is1 : isofhlevelf n f ) ( is2 : isofhlevelf n g ) : isofhlevelf n (coprodf f g).
Proof. intros. unfold isofhlevelf . intro y . induction y as [ z | t ] . apply (isofhlevelweqf n (weqhfibercoprodf1 f g z) ). apply ( is1 z ) . apply (isofhlevelweqf n (weqhfibercoprodf2 f g t )). apply ( is2 t ) . Defined.
Theorem isofhlevelsnsummand1 ( n : nat ) ( X Y : UU ) : isofhlevel ( S n ) ( coprod X Y ) -> isofhlevel ( S n ) X .
Proof. intros n X Y is . apply ( isofhlevelXfromfY ( S n ) ( @ii1 X Y ) ( isofhlevelfsnincl n _ ( isinclii1 _ _ ) ) is ) . Defined.
Theorem isofhlevelsnsummand2 ( n : nat ) ( X Y : UU ) : isofhlevel ( S n ) ( coprod X Y ) -> isofhlevel ( S n ) Y .
Proof. intros n X Y is . apply ( isofhlevelXfromfY ( S n ) ( @ii2 X Y ) ( isofhlevelfsnincl n _ ( isinclii2 _ _ ) ) is ) . Defined.
Theorem isofhlevelssncoprod ( n : nat ) ( X Y : UU ) ( isx : isofhlevel ( S ( S n ) ) X ) ( isy : isofhlevel ( S ( S n ) ) Y ) : isofhlevel ( S ( S n ) ) ( coprod X Y ) .
Proof. intros . apply isofhlevelfromfun . set ( f := coprodf ( fun x : X => tt ) ( fun y : Y => tt ) ) . assert ( is1 : isofhlevelf ( S ( S n ) ) f ) . apply ( isofhlevelfcoprodf ( S ( S n ) ) _ _ ( isofhleveltofun _ X isx ) ( isofhleveltofun _ Y isy ) ) . assert ( is2 : isofhlevel ( S ( S n ) ) ( coprod unit unit ) ) . apply ( isofhlevelweqb ( S ( S n ) ) boolascoprod ( isofhlevelssnset n _ ( isasetbool ) ) ) . apply ( isofhlevelfgf ( S ( S n ) ) _ _ is1 ( isofhleveltofun _ _ is2 ) ) . Defined .
Lemma isasetcoprod ( X Y : UU ) ( isx : isaset X ) ( isy : isaset Y ) : isaset ( coprod X Y ) .
Proof. intros . apply ( isofhlevelssncoprod 0 _ _ isx isy ) . Defined .
Lemma coprodofhfiberstohfiber { X Y Z : UU } ( f : X -> Z ) ( g : Y -> Z ) ( z : Z ) : coprod ( hfiber f z ) ( hfiber g z ) -> hfiber ( sumofmaps f g ) z .
Proof. intros X Y Z f g z hfg . induction hfg as [ hf | hg ] . induction hf as [ x fe ] . split with ( ii1 x ) . simpl . assumption . induction hg as [ y ge ] . split with ( ii2 y ) . simpl . assumption .
Defined.
Lemma hfibertocoprodofhfibers { X Y Z : UU } ( f : X -> Z ) ( g : Y -> Z ) ( z : Z ) : hfiber ( sumofmaps f g ) z -> coprod ( hfiber f z ) ( hfiber g z ) .
Proof. intros X Y Z f g z hsfg . induction hsfg as [ xy e ] . induction xy as [ x | y ] . simpl in e . apply ( ii1 ( hfiberpair _ x e ) ) . simpl in e . apply ( ii2 ( hfiberpair _ y e ) ) . Defined .
Theorem weqhfibersofsumofmaps { X Y Z : UU } ( f : X -> Z ) ( g : Y -> Z ) ( z : Z ) : weq ( coprod ( hfiber f z ) ( hfiber g z ) ) ( hfiber ( sumofmaps f g ) z ) .
Proof. intros . set ( ff := coprodofhfiberstohfiber f g z ) . set ( gg := hfibertocoprodofhfibers f g z ) . split with ff .
assert ( effgg : forall hsfg : _ , paths ( ff ( gg hsfg ) ) hsfg ) . intro . induction hsfg as [ xy e ] . induction xy as [ x | y ] . simpl . apply idpath . simpl . apply idpath .
assert ( eggff : forall hfg : _ , paths ( gg ( ff hfg ) ) hfg ) . intro . induction hfg as [ hf | hg ] . induction hf as [ x fe ] . simpl . apply idpath . induction hg as [ y ge ] . simpl . apply idpath .
apply ( gradth _ _ eggff effgg ) . Defined .
Theorem isofhlevelfssnsumofmaps ( n : nat ) { X Y Z : UU } ( f : X -> Z ) ( g : Y -> Z ) ( isf : isofhlevelf ( S ( S n ) ) f ) ( isg : isofhlevelf ( S ( S n ) ) g ) : isofhlevelf ( S ( S n ) ) ( sumofmaps f g ) .
Proof . intros . intro z . set ( w := weqhfibersofsumofmaps f g z ) . set ( is := isofhlevelssncoprod n _ _ ( isf z ) ( isg z ) ) . apply ( isofhlevelweqf _ w is ) . Defined .
Theorem saying that the sum of two functions of h-level n with non-intersecting images is of h-level n
Lemma noil1 { X Y Z : UU } ( f : X -> Z ) ( g : Y -> Z ) ( noi : forall ( x : X ) ( y : Y ) , neg ( paths ( f x ) ( g y ) ) ) ( z : Z ) : hfiber f z -> hfiber g z -> empty .
Proof. intros X Y Z f g noi z hfz hgz . induction hfz as [ x fe ] . induction hgz as [ y ge ] . apply ( noi x y ( pathscomp0 fe ( pathsinv0 ge ) ) ) . Defined .
Lemma weqhfibernoi1 { X Y Z : UU } ( f : X -> Z ) ( g : Y -> Z ) ( noi : forall ( x : X ) ( y : Y ) , neg ( paths ( f x ) ( g y ) ) ) ( z : Z ) ( xe : hfiber f z ) : weq ( hfiber ( sumofmaps f g ) z ) ( hfiber f z ) .
Proof. intros . set ( w1 := invweq ( weqhfibersofsumofmaps f g z ) ) . assert ( a : neg ( hfiber g z ) ) . intro ye . apply ( noil1 f g noi z xe ye ) . set ( w2 := invweq ( weqii1withneg ( hfiber f z ) a ) ) . apply ( weqcomp w1 w2 ) . Defined .
Lemma weqhfibernoi2 { X Y Z : UU } ( f : X -> Z ) ( g : Y -> Z ) ( noi : forall ( x : X ) ( y : Y ) , neg ( paths ( f x ) ( g y ) ) ) ( z : Z ) ( ye : hfiber g z ) : weq ( hfiber ( sumofmaps f g ) z ) ( hfiber g z ) .
Proof. intros . set ( w1 := invweq ( weqhfibersofsumofmaps f g z ) ) . assert ( a : neg ( hfiber f z ) ) . intro xe . apply ( noil1 f g noi z xe ye ) . set ( w2 := invweq ( weqii2withneg ( hfiber g z ) a ) ) . apply ( weqcomp w1 w2 ) . Defined .
Theorem isofhlevelfsumofmapsnoi ( n : nat ) { X Y Z : UU } ( f : X -> Z ) ( g : Y -> Z ) ( isf : isofhlevelf n f ) ( isg : isofhlevelf n g ) ( noi : forall ( x : X ) ( y : Y ) , neg ( paths ( f x ) ( g y ) ) ) : isofhlevelf n ( sumofmaps f g ) .
Proof. intros . intro z . induction n as [ | n ] . set ( zinx := invweq ( weqpair _ isf ) z ) . set ( ziny := invweq ( weqpair _ isg ) z ) . assert ( ex : paths ( f zinx ) z ) . apply ( homotweqinvweq ( weqpair _ isf ) z ) . assert ( ey : paths ( g ziny ) z ) . apply ( homotweqinvweq ( weqpair _ isg ) z ) . induction ( ( noi zinx ziny ) ( pathscomp0 ex ( pathsinv0 ey ) ) ) .
apply isofhlevelsn . intro hfgz . induction ( ( invweq ( weqhfibersofsumofmaps f g z ) hfgz ) ) as [ xe | ye ] . apply ( isofhlevelweqb _ ( weqhfibernoi1 f g noi z xe ) ( isf z ) ) . apply ( isofhlevelweqb _ ( weqhfibernoi2 f g noi z ye ) ( isg z ) ) . Defined .
Definition tocompltoii1x (X Y:UU)(x:X): coprod (compl X x) Y -> compl (coprod X Y) (ii1 x).
Proof. intros X Y x X0. induction X0 as [ c | y ] . split with (ii1 (pr1 c)).
assert (e: neg(paths x (pr1 c) )). apply (pr2 c). apply (negf (invmaponpathsincl ( @ii1 _ _ ) (isinclii1 X Y) _ _) e).
split with (ii2 y). apply (negf (pathsinv0 ) (negpathsii2ii1 x y)). Defined.
Definition fromcompltoii1x (X Y:UU)(x:X): compl (coprod X Y) (ii1 x) -> coprod (compl X x) Y.
Proof. intros X Y x X0. induction X0 as [ t x0 ]. induction t as [ x1 | y ].
assert (ne: neg (paths x x1 )). apply (negf (maponpaths ( @ii1 _ _ ) ) x0). apply (ii1 (complpair _ _ x1 ne )). apply (ii2 y). Defined.
Theorem isweqtocompltoii1x (X Y:UU)(x:X): isweq (tocompltoii1x X Y x).
Proof. intros. set (f:= tocompltoii1x X Y x). set (g:= fromcompltoii1x X Y x).
assert (egf:forall nexy:_ , paths (g (f nexy)) nexy). intro. induction nexy as [ c | y ]. induction c as [ t x0 ]. simpl.
assert (e: paths (negf (maponpaths (@ii1 X Y)) (negf (invmaponpathsincl (@ii1 X Y) (isinclii1 X Y) x t) x0)) x0). apply (isapropneg (paths x t) ).
apply (maponpaths (fun ee: neg (paths x t ) => ii1 (complpair X x t ee)) e). apply idpath.
assert (efg: forall neii1x:_, paths (f (g neii1x)) neii1x). intro. induction neii1x as [ t x0 ]. induction t as [ x1 | y ]. simpl.
assert (e: paths (negf (invmaponpathsincl (@ii1 X Y) (isinclii1 X Y) x x1 ) (negf (maponpaths (@ii1 X Y) ) x0)) x0). apply (isapropneg (paths _ _ ) ).
apply (maponpaths (fun ee: (neg (paths (ii1 x) (ii1 x1))) => (complpair _ _ (ii1 x1) ee)) e). simpl.
assert (e: paths (negf pathsinv0 (negpathsii2ii1 x y)) x0). apply (isapropneg (paths _ _ ) ).
apply (maponpaths (fun ee: (neg (paths (ii1 x) (ii2 y) )) => (complpair _ _ (ii2 y) ee)) e).
apply (gradth f g egf efg). Defined.
Definition tocompltoii2y (X Y:UU)(y:Y): coprod X (compl Y y) -> compl (coprod X Y) (ii2 y).
Proof. intros X Y y X0. induction X0 as [ x | c ]. split with (ii1 x). apply (negpathsii2ii1 x y ).
split with (ii2 (pr1 c)). assert (e: neg(paths y (pr1 c) )). apply (pr2 c). apply (negf (invmaponpathsincl ( @ii2 _ _ ) (isinclii2 X Y) _ _ ) e).
Defined.
Definition fromcompltoii2y (X Y:UU)(y:Y): compl (coprod X Y) (ii2 y) -> coprod X (compl Y y).
Proof. intros X Y y X0. induction X0 as [ t x ]. induction t as [ x0 | y0 ]. apply (ii1 x0).
assert (ne: neg (paths y y0 )). apply (negf (maponpaths ( @ii2 _ _ ) ) x). apply (ii2 (complpair _ _ y0 ne)). Defined.
Theorem isweqtocompltoii2y (X Y:UU)(y:Y): isweq (tocompltoii2y X Y y).
Proof. intros. set (f:= tocompltoii2y X Y y). set (g:= fromcompltoii2y X Y y).
assert (egf:forall nexy:_ , paths (g (f nexy)) nexy). intro. induction nexy as [ x | c ].
apply idpath. induction c as [ t x ]. simpl.
assert (e: paths (negf (maponpaths (@ii2 X Y) ) (negf (invmaponpathsincl (@ii2 X Y) (isinclii2 X Y) y t) x)) x). apply (isapropneg (paths y t ) ).
apply (maponpaths (fun ee: neg ( paths y t ) => ii2 (complpair _ y t ee)) e).
assert (efg: forall neii2x:_, paths (f (g neii2x)) neii2x). intro. induction neii2x as [ t x ]. induction t as [ x0 | y0 ]. simpl.
assert (e: paths (negpathsii2ii1 x0 y) x). apply (isapropneg (paths _ _ ) ).
apply (maponpaths (fun ee: (neg (paths (ii2 y) (ii1 x0) )) => (complpair _ _ (ii1 x0) ee)) e). simpl.
assert (e: paths (negf (invmaponpathsincl _ (isinclii2 X Y) y y0 ) (negf (maponpaths (@ii2 X Y) ) x)) x). apply (isapropneg (paths _ _ ) ).
apply (maponpaths (fun ee: (neg (paths (ii2 y) (ii2 y0) )) => (complpair _ _ (ii2 y0) ee)) e).
apply (gradth f g egf efg). Defined.
Definition tocompltodisjoint (X:UU): X -> compl (coprod X unit) (ii2 tt) := fun x:_ => complpair _ _ (ii1 x) (negpathsii2ii1 x tt).
Definition fromcompltodisjoint (X:UU): compl (coprod X unit) (ii2 tt) -> X.
Proof. intros X X0. induction X0 as [ t x ]. induction t as [ x0 | u ] . assumption. induction u. apply (fromempty (x (idpath (ii2 tt)))). Defined.
Lemma isweqtocompltodisjoint (X:UU): isweq (tocompltodisjoint X).
Proof. intros. set (ff:= tocompltodisjoint X). set (gg:= fromcompltodisjoint X).
assert (egf: forall x:X, paths (gg (ff x)) x). intro. apply idpath.
assert (efg: forall xx:_, paths (ff (gg xx)) xx). intro. induction xx as [ t x ]. induction t as [ x0 | u ] . simpl. unfold ff. unfold tocompltodisjoint. simpl. assert (ee: paths (negpathsii2ii1 x0 tt) x). apply (proofirrelevance _ (isapropneg _) ). induction ee. apply idpath. induction u. simpl. apply (fromempty (x (idpath _))). apply (gradth ff gg egf efg). Defined.
Definition weqtocompltodisjoint ( X : UU ) := weqpair _ ( isweqtocompltodisjoint X ) .
Corollary isweqfromcompltodisjoint (X:UU): isweq (fromcompltodisjoint X).
Proof. intros. apply (isweqinvmap ( weqtocompltodisjoint X ) ). Defined.
Definition isdecprop ( X : UU ) := iscontr ( coprod X ( neg X ) ) .
Lemma isdecproptoisaprop ( X : UU ) ( is : isdecprop X ) : isaprop X .
Proof. intros X is . apply ( isofhlevelsnsummand1 0 _ _ ( isapropifcontr is ) ) . Defined .
Coercion isdecproptoisaprop : isdecprop >-> isaprop .
Lemma isdecpropif ( X : UU ) : isaprop X -> ( coprod X ( neg X ) ) -> isdecprop X .
Proof. intros X is a . assert ( is1 : isaprop ( coprod X ( neg X ) ) ) . apply isapropdec . assumption . apply ( iscontraprop1 is1 a ) . Defined.
Lemma isdecpropfromiscontr { X : UU } ( is : iscontr X ) : isdecprop X .
Proof. intros . apply ( isdecpropif _ ( is ) ( ii1 ( pr1 is ) ) ) . Defined.
Lemma isdecpropempty : isdecprop empty .
Proof. apply ( isdecpropif _ isapropempty ( ii2 ( fun a : empty => a ) ) ) . Defined.
Lemma isdecpropweqf { X Y : UU } ( w : weq X Y ) ( is : isdecprop X ) : isdecprop Y .
Proof. intros . apply isdecpropif . apply ( isofhlevelweqf 1 w ( isdecproptoisaprop _ is ) ) . induction ( pr1 is ) as [ x | nx ] . apply ( ii1 ( w x ) ) . apply ( ii2 ( negf ( invweq w ) nx ) ) . Defined .
Lemma isdecpropweqb { X Y : UU } ( w : weq X Y ) ( is : isdecprop Y ) : isdecprop X .
Proof. intros . apply isdecpropif . apply ( isofhlevelweqb 1 w ( isdecproptoisaprop _ is ) ) . induction ( pr1 is ) as [ y | ny ] . apply ( ii1 ( invweq w y ) ) . apply ( ii2 ( ( negf w ) ny ) ) . Defined .
Lemma isdecproplogeqf { X Y : UU } ( isx : isdecprop X ) ( isy : isaprop Y ) ( lg : X <-> Y ) : isdecprop Y .
Proof . intros. set ( w := weqimplimpl ( pr1 lg ) ( pr2 lg ) isx isy ) . apply ( isdecpropweqf w isx ) . Defined .
Lemma isdecproplogeqb { X Y : UU } ( isx : isaprop X ) ( isy : isdecprop Y ) ( lg : X <-> Y ) : isdecprop X .
Proof . intros. set ( w := weqimplimpl ( pr1 lg ) ( pr2 lg ) isx isy ) . apply ( isdecpropweqb w isy ) . Defined .
Lemma isdecpropfromneg { X : UU } ( ne : neg X ) : isdecprop X .
Proof. intros . apply ( isdecpropweqb ( weqtoempty ne ) isdecpropempty ) . Defined .
Lemma isdecproppaths { X : UU } ( is : isdeceq X ) ( x x' : X ) : isdecprop ( paths x x' ) .
Proof. intros . apply ( isdecpropif _ ( isasetifdeceq _ is x x' ) ( is x x' ) ) . Defined .
Lemma isdeceqif { X : UU } ( is : forall x x' : X , isdecprop ( paths x x' ) ) : isdeceq X .
Proof . intros . intros x x' . apply ( pr1 ( is x x' ) ) . Defined .
Lemma isaninv1 (X:UU): isdecprop X -> isaninvprop X.
Proof. intros X is1. unfold isaninvprop. set (is2:= pr1 is1). simpl in is2.
assert (adjevinv: dneg X -> X). intro X0. induction is2 as [ a | b ]. assumption. induction (X0 b).
assert (is3: isaprop (dneg X)). apply (isapropneg (X -> empty)). apply (isweqimplimpl (todneg X) adjevinv is1 is3). Defined.
Theorem isdecpropfibseq1 { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( fs : fibseqstr f g z ) : isdecprop X -> isaprop Z -> isdecprop Y .
Proof . intros X Y Z f g z fs isx isz . assert ( isc : iscontr Z ) . apply ( iscontraprop1 isz z ) . assert ( isweq f ) . apply ( isweqfinfibseq f g z fs isc ) . apply ( isdecpropweqf ( weqpair _ X0 ) isx ) . Defined .
Theorem isdecpropfibseq0 { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( z : Z ) ( fs : fibseqstr f g z ) : isdecprop Y -> isdeceq Z -> isdecprop X .
Proof . intros X Y Z f g z fs isy isz . assert ( isg : isofhlevelf 1 g ) . apply ( isofhlevelffromXY 1 g ( isdecproptoisaprop _ isy ) ( isasetifdeceq _ isz ) ) .
assert ( isp : isaprop X ) . apply ( isofhlevelXfromg 1 f g z fs isg ) .
induction ( pr1 isy ) as [ y | ny ] . apply ( isdecpropfibseq1 _ _ y ( fibseq1 f g z fs y ) ( isdecproppaths isz ( g y ) z ) ( isdecproptoisaprop _ isy ) ) .
apply ( isdecpropif _ isp ( ii2 ( negf f ny ) ) ) . Defined.
Theorem isdecpropdirprod { X Y : UU } ( isx : isdecprop X ) ( isy : isdecprop Y ) : isdecprop ( dirprod X Y ) .
Proof. intros . assert ( isp : isaprop ( dirprod X Y ) ) . apply ( isofhleveldirprod 1 _ _ ( isdecproptoisaprop _ isx ) ( isdecproptoisaprop _ isy ) ) . induction ( pr1 isx ) as [ x | nx ] . induction ( pr1 isy ) as [ y | ny ] . apply ( isdecpropif _ isp ( ii1 ( dirprodpair x y ) ) ) . assert ( nxy : neg ( dirprod X Y ) ) . intro xy . induction xy as [ x0 y0 ] . apply ( ny y0 ) . apply ( isdecpropif _ isp ( ii2 nxy ) ) . assert ( nxy : neg ( dirprod X Y ) ) . intro xy . induction xy as [ x0 y0 ] . apply ( nx x0 ) . apply ( isdecpropif _ isp ( ii2 nxy ) ) . Defined.
Lemma fromneganddecx { X Y : UU } ( isx : isdecprop X ) ( nf : neg ( dirprod X Y ) ) : coprod ( neg X ) ( neg Y ) .
Proof . intros . induction ( pr1 isx ) as [ x | nx ] . set ( ny := negf ( fun y : Y => dirprodpair x y ) nf ) . apply ( ii2 ny ) . apply ( ii1 nx ) . Defined .
Lemma fromneganddecy { X Y : UU } ( isy : isdecprop Y ) ( nf : neg ( dirprod X Y ) ) : coprod ( neg X ) ( neg Y ) .
Proof . intros . induction ( pr1 isy ) as [ y | ny ] . set ( nx := negf ( fun x : X => dirprodpair x y ) nf ) . apply ( ii1 nx ) . apply ( ii2 ny ) . Defined .
Lemma isdecproppathsfromisolated ( X : UU ) ( x : X ) ( is : isisolated X x ) ( x' : X ) : isdecprop ( paths x x' ) .
Proof. intros . apply isdecpropif . apply isaproppathsfromisolated . assumption . apply ( is x' ) . Defined .
Lemma isdecproppathstoisolated ( X : UU ) ( x : X ) ( is : isisolated X x ) ( x' : X ) : isdecprop ( paths x' x ) .
Proof . intros . apply ( isdecpropweqf ( weqpathsinv0 x x' ) ( isdecproppathsfromisolated X x is x' ) ) . Defined .
Definition isdecincl {X Y:UU} (f :X -> Y) := forall y:Y, isdecprop ( hfiber f y ).
Lemma isdecincltoisincl { X Y : UU } ( f : X -> Y ) : isdecincl f -> isincl f .
Proof. intros X Y f is . intro y . apply ( isdecproptoisaprop _ ( is y ) ) . Defined.
Coercion isdecincltoisincl : isdecincl >-> isincl .
Lemma isdecinclfromisweq { X Y : UU } ( f : X -> Y ) : isweq f -> isdecincl f .
Proof. intros X Y f iswf . intro y . apply ( isdecpropfromiscontr ( iswf y ) ) . Defined .
Lemma isdecpropfromdecincl { X Y : UU } ( f : X -> Y ) : isdecincl f -> isdecprop Y -> isdecprop X .
Proof. intros X Y f isf isy . induction ( pr1 isy ) as [ y | n ] . assert ( w : weq ( hfiber f y ) X ) . apply ( weqhfibertocontr f y ( iscontraprop1 ( isdecproptoisaprop _ isy ) y ) ) . apply ( isdecpropweqf w ( isf y ) ) . apply isdecpropif . apply ( isapropinclb _ isf isy ) . apply ( ii2 ( negf f n ) ) . Defined .
Lemma isdecinclii1 (X Y: UU): isdecincl ( @ii1 X Y ) .
Proof. intros. intro y . induction y as [ x | y ] . apply ( isdecpropif _ ( isinclii1 X Y ( ii1 x ) ) ( ii1 (hfiberpair (@ii1 _ _ ) x (idpath _ )) ) ) .
apply ( isdecpropif _ ( isinclii1 X Y ( ii2 y ) ) ( ii2 ( neghfiberii1y X Y y ) ) ) . Defined.
Lemma isdecinclii2 (X Y: UU): isdecincl ( @ii2 X Y ) .
Proof. intros. intro y . induction y as [ x | y ] . apply ( isdecpropif _ ( isinclii2 X Y ( ii1 x ) ) ( ii2 ( neghfiberii2x X Y x ) ) ) .
apply ( isdecpropif _ ( isinclii2 X Y ( ii2 y ) ) ( ii1 (hfiberpair (@ii2 _ _ ) y (idpath _ )) ) ) . Defined.
Lemma isdecinclpr1 { X : UU } ( P : X -> UU ) ( is : forall x : X , isdecprop ( P x ) ) : isdecincl ( @pr1 _ P ) .
Proof . intros . intro x . assert ( w : weq ( P x ) ( hfiber (@pr1 _ P ) x ) ) . apply ezweqpr1 . apply ( isdecpropweqf w ( is x ) ) . Defined .
Theorem isdecinclhomot { X Y : UU } ( f g : X -> Y ) ( h : forall x : X , paths ( f x ) ( g x ) ) ( is : isdecincl f ) : isdecincl g .
Proof. intros . intro y . apply ( isdecpropweqf ( weqhfibershomot f g h y ) ( is y ) ) . Defined .
Theorem isdecinclcomp { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( isf : isdecincl f ) ( isg : isdecincl g ) : isdecincl ( fun x : X => g ( f x ) ) .
Proof. intros. intro z . set ( gf := fun x : X => g ( f x ) ) . assert ( wy : forall ye : hfiber g z , weq ( hfiber f ( pr1 ye ) ) ( hfiber ( hfibersgftog f g z ) ye ) ) . apply ezweqhf .
assert ( ww : forall y : Y , weq ( hfiber f y ) ( hfiber gf ( g y ) ) ) . intro . apply ( samehfibers f g ) . apply ( isdecincltoisincl _ isg ) .
induction ( pr1 ( isg z ) ) as [ ye | nye ] . induction ye as [ y e ] . induction e . apply ( isdecpropweqf ( ww y ) ( isf y ) ) . assert ( wz : weq ( hfiber gf z ) ( hfiber g z ) ) . split with ( hfibersgftog f g z ) . intro ye . induction ( nye ye ) . apply ( isdecpropweqb wz ( isg z ) ) . Defined .
The conditions of the following theorem can be weakened by assuming only that the h-fibers of g satisfy isdeceq i.e. are "sets with decidable equality".
Theorem isdecinclf { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( isg : isincl g ) ( isgf : isdecincl ( fun x : X => g ( f x ) ) ) : isdecincl f .
Proof. intros . intro y . set ( gf := fun x : _ => g ( f x ) ) . assert ( ww : weq ( hfiber f y ) ( hfiber gf ( g y ) ) ) . apply ( samehfibers f g ) . assumption . apply ( isdecpropweqb ww ( isgf ( g y ) ) ) . Defined .
Theorem isdecinclg { X Y Z : UU } ( f : X -> Y ) ( g : Y -> Z ) ( isf : isweq f ) ( isgf : isdecincl ( fun x : X => g ( f x ) ) ) : isdecincl g .
Proof. intros . intro z . set ( gf := fun x : X => g ( f x ) ) . assert ( w : weq ( hfiber gf z ) ( hfiber g z ) ) . split with ( hfibersgftog f g z ) . intro ye . assert ( ww : weq ( hfiber f ( pr1 ye ) ) ( hfiber ( hfibersgftog f g z ) ye ) ) . apply ezweqhf . apply ( iscontrweqf ww ( isf ( pr1 ye ) ) ) . apply ( isdecpropweqf w ( isgf z ) ) . Defined .
Theorem isisolateddecinclf { X Y : UU } ( f : X -> Y ) ( x : X ) : isdecincl f -> isisolated X x -> isisolated Y ( f x ) .
Proof . intros X Y f x isf isx . assert ( is' : forall y : Y , isdecincl ( d1g f y x ) ) . intro y . intro xe . set ( w := ezweq2g f x xe ) . apply ( isdecpropweqf w ( isdecproppathstoisolated X x isx _ ) ) . assert ( is'' : forall y : Y , isdecprop ( paths ( f x ) y ) ) . intro . apply ( isdecpropfromdecincl _ ( is' y ) ( isf y ) ) . intro y' . apply ( pr1 ( is'' y' ) ) . Defined .
Definition negimage { X Y : UU } ( f : X -> Y ) := total2 ( fun y : Y => neg ( hfiber f y ) ) .
Definition negimagepair { X Y : UU } ( f : X -> Y ) := tpair ( fun y : Y => neg ( hfiber f y ) ) .
Lemma isinclfromcoprodwithnegimage { X Y : UU } ( f : X -> Y ) ( is : isincl f ) : isincl ( sumofmaps f ( @pr1 _ ( fun y : Y => neg ( hfiber f y ) ) ) ) .
Proof . intros . assert ( noi : forall ( x : X ) ( nx : negimage f ) , neg ( paths ( f x ) ( pr1 nx ) ) ) . intros x nx e . induction nx as [ y nhf ] . simpl in e . apply ( nhf ( hfiberpair _ x e ) ) . assert ( is' : isincl ( @pr1 _ ( fun y : Y => neg ( hfiber f y ) ) ) ) . apply isinclpr1 . intro y . apply isapropneg . apply ( isofhlevelfsumofmapsnoi 1 f _ is is' noi ) . Defined .
Definition iscoproj { X Y : UU } ( f : X -> Y ) := isweq ( sumofmaps f ( @pr1 _ ( fun y : Y => neg ( hfiber f y ) ) ) ) .
Definition weqcoproj { X Y : UU } ( f : X -> Y ) ( is : iscoproj f ) : weq ( coprod X ( negimage f ) ) Y := weqpair _ is .
Theorem iscoprojfromisdecincl { X Y : UU } ( f : X -> Y ) ( is : isdecincl f ) : iscoproj f .
Proof. intros . set ( p := sumofmaps f ( @pr1 _ ( fun y : Y => neg ( hfiber f y ) ) ) ) . assert ( is' : isincl p ) . apply isinclfromcoprodwithnegimage . apply ( isdecincltoisincl _ is ) . unfold iscoproj . intro y . induction ( pr1 ( is y ) ) as [ h | nh ] . induction h as [ x e ] . induction e . change ( f x ) with ( p ( ii1 x ) ) . apply iscontrhfiberofincl . assumption . change y with ( p ( ii2 ( negimagepair _ y nh ) ) ) . apply iscontrhfiberofincl . assumption . Defined .
Theorem isdecinclfromiscoproj { X Y : UU } ( f : X -> Y ) ( is : iscoproj f ) : isdecincl f .
Proof . intros . set ( g := ( sumofmaps f ( @pr1 _ ( fun y : Y => neg ( hfiber f y ) ) ) ) ) . set ( f' := fun x : X => g ( ii1 x ) ) . assert ( is' : isdecincl f' ) . apply ( isdecinclcomp _ _ ( isdecinclii1 _ _ ) ( isdecinclfromisweq _ is ) ) . assumption . Defined .
Results using full form of the functional extentionality axioms.
Axioms and their basic corollaries
Definition etacorrection: forall T:UU, forall P:T -> UU, forall f: (forall t:T, P t), paths f (fun t:T => f t).
Proof. reflexivity. Defined.
Lemma isweqetacorrection { T : UU } (P:T -> UU): isweq (fun f: forall t:T, P t => (fun t:T => f t)).
Proof. intros. apply (isweqhomot (fun f: forall t:T, P t => f) (fun f: forall t:T, P t => (fun t:T => f t)) (fun f: forall t:T, P t => etacorrection _ P f) (idisweq _)). Defined.
Definition weqeta { T : UU } (P:T -> UU) := weqpair _ ( isweqetacorrection P ) .
Lemma etacorrectiononpaths { T : UU } (P:T->UU)(s1 s2 :forall t:T, P t) : paths (fun t:T => s1 t) (fun t:T => s2 t)-> paths s1 s2.
Proof. intros T P s1 s2 X. set (ew := weqeta P). apply (invmaponpathsweq ew s1 s2 X). Defined.
Definition etacor { X Y : UU } (f:X -> Y) : paths f (fun x:X => f x) := etacorrection _ (fun T:X => Y) f.
Lemma etacoronpaths { X Y : UU } (f1 f2 : X->Y) : paths (fun x:X => f1 x) (fun x:X => f2 x) -> paths f1 f2.
Proof. intros X Y f1 f2 X0. set (ec:= weqeta (fun x:X => Y) ). apply (invmaponpathsweq ec f1 f2 X0). Defined.
Dependent functions and sections up to homotopy I
Definition toforallpaths { T : UU } (P:T -> UU) (f g :forall t:T, P t) : (paths f g) -> (forall t:T, paths (f t) (g t)).
Proof. intros T P f g X t. induction X. apply (idpath (f t)). Defined.
Definition sectohfiber { X : UU } (P:X -> UU): (forall x:X, P x) -> (hfiber (fun f:_ => fun x:_ => pr1 (f x)) (fun x:X => x)) := (fun a : forall x:X, P x => tpair _ (fun x:_ => tpair _ x (a x)) (idpath (fun x:X => x))).
Definition hfibertosec { X : UU } (P:X -> UU): (hfiber (fun f:_ => fun x:_ => pr1 (f x)) (fun x:X => x)) -> (forall x:X, P x):= fun se:_ => fun x:X => match se as se' return P x with tpair _ s e => (transportf P (toforallpaths (fun x:X => X) (fun x:X => pr1 (s x)) (fun x:X => x) e x) (pr2 (s x))) end.
Definition sectohfibertosec { X : UU } (P:X -> UU): forall a: forall x:X, P x, paths (hfibertosec _ (sectohfiber _ a)) a := fun a:_ => (pathsinv0 (etacorrection _ _ a)).