Require Export u1 u0. (* The following definitions establish the hierarchy of universes such that Type0=u0.UU Type1=u1.UU Type0:Type1 and Type0 is a subtype of Type1 *) Definition j01:u0.UU -> u1.UU:= fun T:u0.UU => T. Definition j11:u1.UU -> u1.UU:=fun T:u1.UU => T. Definition Type0:=j11 u0.UU. Definition Type1:=u1.UU. (* Note: by the current agreement in Coq the names introduced in u0, as the last module to be imported, "shadow" the manes introduced in u1 so that, for example, paths is the same as u0.paths and UU is the same as u0.UU *) Definition transportb (P:Type0 -> Type0)(X:Type0)(X':Type0)(e:u1.paths _ X X'): P X' -> P X. Proof. intros. induction e. assumption. Defined. Lemma isweqtransportb (P:Type0 -> Type0)(X:Type0)(X':Type0)(e:u1.paths _ X X'): isweq _ _ (fun p' : P X' => transportb P X X' e p'). Proof. intros. induction e. simpl. apply idisweq. Defined. Definition eqweqmap (T1:Type0) (T2:Type0) : (u1.paths _ T1 T2) -> (weq T1 T2). Proof. intros. induction X. apply idweq. Defined. Axiom equivalenceaxiom: forall T1:Type0, forall T2:Type0, u1.isweq (u1.paths Type T1 T2) (weq T1 T2) (eqweqmap T1 T2). Definition weqtopaths (T1:Type0)(T2:Type0)(f:T1 -> T2)(is:isweq _ _ f): u1.paths _ T1 T2 := u1.invmap _ _ (eqweqmap T1 T2) (equivalenceaxiom T1 T2) (weqpair _ _ f is). Definition weqpathsweq (T1:Type0)(T2:Type0)(f:T1 -> T2)(is:isweq _ _ f):u1.paths _ (eqweqmap _ _ (weqtopaths _ _ f is)) (weqpair _ _ f is) := u1.weqfg _ _ (eqweqmap T1 T2) (equivalenceaxiom T1 T2) (weqpair _ _ f is). (* Conjecture: equivalenceaxiom is equivalent to two axioms Axiom weqtopaths0 (T1:Type0)(T2:Type0)(f:T1 -> T2)(is:isweq0 _ _ f): paths1 _ T1 T2. Axiom weqpathsweq0 (T1:Type0)(T2:Type0)(f:T1 -> T2)(is:isweq0 _ _ f):paths1 _ (eqweqmap0 _ _ (weqtopaths0 _ _ f is)) (weqpair0 _ _ f is). *) (* Theorem saying that any general scheme to "transport" a structure along a weak equivalence which does not change the structure in the case of the identity equivalence is equivalent to the transport along the path which corresponds to a weak equivalence by the equivalenceaxiom. As a corollary we conclude that for any such transport scheme the corresponding maps on spaes of structures are weak equivalences. *) Lemma l1 (X0:Type0)(X0':Type0)(ee: u1.paths _ X0 X0')(P:Type0 -> Type0)(pp': P X0')(R: forall X:Type0, forall X':Type0, forall u:X -> X', forall is: isweq X X' u, P X' -> P X)(r: forall X:Type0, forall p:P X, paths _ (R X X (fun x:X => x) (idisweq X) p) p):paths _ (R X0 X0' (pr21 _ _ (eqweqmap _ _ ee)) (pr22 _ _ (eqweqmap _ _ ee)) pp') (transportb P X0 X0' ee pp'). Proof. intro. intro. intro. intro. intro. induction ee. simpl. intro. intro. apply r. Defined. Theorem weqtransportb (P:Type0 -> Type0)(R: forall X:Type0, forall X':Type0, forall u:X -> X', forall is: isweq X X' u, P X' -> P X)(r: forall X:Type0, forall p:P X, paths _ (R X X (fun x:X => x) (idisweq X) p) p): forall X:Type0, forall X':Type0, forall u:X -> X', forall is: isweq X X' u, forall p':P X', paths _ (R X X' u is p') (transportb P X X' (weqtopaths _ _ u is) p'). Proof. intros. set (uis:=weqpair _ _ u is). set (uv:=weqtopaths _ _ u is). set (v:=eqweqmap _ _ uv). assert (e:u1.paths _ v uis). unfold weqtopaths in uv. apply (u1.weqfg (u1.paths Type0 X X') (weq X X') (eqweqmap X X') (equivalenceaxiom X X') uis). assert (ee:u1.paths _ (R X X' (pr21 _ _ v) (pr22 _ _ v) p') (R X X' u is p')). set (R':= fun vis:weq X X' => R X X' (pr21 _ _ vis) (pr22 _ _ vis) p'). assert (ee':u1.paths _ (R' v) (R' uis)). apply (u1.maponpaths (weq X X') (P X) R' _ _ e). assumption. induction ee. apply l1. assumption. Defined. Corollary isweqweqtransportb (P:Type0 -> Type0)(R: forall X:Type0, forall X':Type0, forall u:X -> X', forall is: isweq X X' u, P X' -> P X)(r: forall X:Type0, forall p:P X, paths _ (R X X (fun x:X => x) (idisweq X) p) p): forall X:Type0, forall X':Type0, forall u:X -> X', forall is: isweq X X' u, isweq _ _ (fun p': P X' => R X X' u is p'). Proof. intros. assert (e:forall p':P X', paths _ (R X X' u is p') (transportb P X X' (weqtopaths _ _ u is) p')). apply weqtransportb. assumption. assert (ee :forall p':P X', paths _ (transportb P X X' (weqtopaths _ _ u is) p') (R X X' u is p')). intro. apply (pathsinv0 _ _ _ (e p')). clear e. assert (is1:isweq _ _ (fun p': P X' => (transportb P X X' (weqtopaths _ _ u is) p'))). apply isweqtransportb. apply (isweqhom _ _ (fun p': P X' => transportb P X X' (weqtopaths X X' u is) p') (fun p' : P X' => R X X' u is p') ee is1). Defined. (* Theorem saying that composition with a weak equivalence is a weak equivalence on function spaces. *) Theorem isweqcompwithweq (X:Type0)(X':Type0)(u:X->X')(is:isweq _ _ u)(Y:Type0): isweq _ _ (fun f:X'->Y => (fun x:X => f (u x))). Proof. intros. set (P:= fun X0:Type0 => (X0 -> Y)). set (R:= fun X0:Type0 => (fun X0':Type0 => (fun u0:X0 -> X0' => (fun is0:isweq _ _ u0 => (fun f:P X0' => (fun x:X0 => f (u0 x))))))). set (r:= fun X0:Type0 => (fun f:X0 -> Y => pathsinv0 _ _ _ (etacor X0 Y f))). apply (isweqweqtransportb P R r X X' u is). Defined. (* Proof of the functional extensionality for functions *) Lemma eqcor0 (X:Type0)(X':Type0)(u:X->X')(is:isweq _ _ u)(Y:Type0)(f1:X'->Y)(f2:X'->Y): (paths _ (fun x:X => f1 (u x)) (fun x:X => f2 (u x))) -> paths _ f1 f2. Proof. intros. apply (isweqpaths1 _ _ (fun f:X'->Y => (fun x:X => f (u x))) (isweqcompwithweq _ _ u is Y) f1 f2). assumption. Defined. Lemma apathpr1topr2 (T:Type0) : paths _ (fun z: pathsspace T => pr21 _ _ z) (fun z: pathsspace T => pr21 _ _ (pr22 _ _ z)). Proof. intro. apply (eqcor0 _ _ (deltap T) (isweqdeltap T) _ (fun z: pathsspace T => pr21 _ _ z) (fun z: pathsspace T => pr21 _ _ (pr22 _ _ z)) (idpath _ (fun t:T => t))). Defined. Theorem funextfun (X:Type0)(Y:Type0)(f1:X->Y)(f2:X->Y)(e: forall x:X, paths _ (f1 x) (f2 x)): paths _ f1 f2. Proof. intros. set (f:= (fun x:X => pathsspacetriple Y (f1 x) (f2 x) (e x))). set (g1:= (fun z:pathsspace Y => pr21 _ _ z)). set (g2:= fun z: pathsspace Y => pr21 _ _ (pr22 _ _ z)). assert (e': paths _ g1 g2). apply (apathpr1topr2 Y). assert (ee:paths _ (fun x:X => f1 x) (fun x:X => f2 x)). apply (maponpaths2b _ _ _ f g1 g2 e'). apply etacoronpaths. assumption. Defined. (* Some elementary corollaries and other constructions. *) Definition funpath1 (T:Type0)(P1:T -> Type0)(P2:T-> Type0)(e: u1.paths _ P1 P2): u1.paths _ (forall t:T, P1 t) (forall t:T, P2 t). Proof. intros. induction e. apply u1.idpath. Defined. Lemma ifcontrthenunit: forall T:Type0, (iscontr T) -> u1.paths _ T unit. Proof. intros. apply ifcontrthenunit1 in X. apply weqtopaths in X. assumption. Defined. Lemma iscontrtounit (T:Type0) :iscontr (T -> unit). Proof. intros. set (cntr:= (fun t:T => tt)). split with cntr. intros. assert (e: forall f1: T -> unit, forall t:T, paths _ (f1 t) tt). intros. induction (f1 t0). apply idpath. apply (funextfun T unit t cntr (e t)). Defined. Theorem ifcontrthenaprop: forall T:Type0, (iscontr T) -> (isaprop T). Proof. intros. apply ifcontrthenunit in X. assert (e:isaprop unit). apply unitisaprop. induction X. assumption. Defined.