Require Export u2 u1. (* The following definitions establish the hierarchy of universes such that Type1=u1.UU Type2=u2.UU Type1:Type2 and Type1 is a subtype of Type2 *) Definition j12:u1.UU -> u2.UU:= fun T:u1.UU => T. Definition j22:u2.UU -> u2.UU:=fun T:u2.UU => T. Definition Type1:=j22 u1.UU. Definition Type2:=u2.UU. (* Note: by the current agreement in Coq the names introduced in u1, as the last module to be imported, "shadow" the manes introduced in u2 so that, for example, paths is the same as u1.paths and UU is the same as u1.UU *) Definition transportb (P:Type1 -> Type1)(X:Type1)(X':Type1)(e:u2.paths _ X X'): P X' -> P X. Proof. intros. induction e. assumption. Defined. Lemma isweqtransportb (P:Type1 -> Type1)(X:Type1)(X':Type1)(e:u2.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:Type1) (T2:Type1) : (u2.paths _ T1 T2) -> (weq T1 T2). Proof. intros. induction X. apply idweq. Defined. Axiom equivalenceaxiom: forall T1:Type1, forall T2:Type1, u2.isweq (u2.paths Type T1 T2) (weq T1 T2) (eqweqmap T1 T2). Definition weqtopaths (T1:Type1)(T2:Type1)(f:T1 -> T2)(is:isweq _ _ f): u2.paths _ T1 T2 := u2.invmap _ _ (eqweqmap T1 T2) (equivalenceaxiom T1 T2) (weqpair _ _ f is). Definition weqpathsweq (T1:Type1)(T2:Type1)(f:T1 -> T2)(is:isweq _ _ f):u2.paths _ (eqweqmap _ _ (weqtopaths _ _ f is)) (weqpair _ _ f is) := u2.weqfg _ _ (eqweqmap T1 T2) (equivalenceaxiom T1 T2) (weqpair _ _ f is). (* Conjecture: equivalenceaxiom is equivalent to two axioms Axiom weqtopaths0 (T1:Type1)(T2:Type1)(f:T1 -> T2)(is:isweq0 _ _ f): paths1 _ T1 T2. Axiom weqpathsweq0 (T1:Type1)(T2:Type1)(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:Type1)(X0':Type1)(ee: u2.paths _ X0 X0')(P:Type1 -> Type1)(pp': P X0')(R: forall X:Type1, forall X':Type1, forall u:X -> X', forall is: isweq X X' u, P X' -> P X)(r: forall X:Type1, 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:Type1 -> Type1)(R: forall X:Type1, forall X':Type1, forall u:X -> X', forall is: isweq X X' u, P X' -> P X)(r: forall X:Type1, forall p:P X, paths _ (R X X (fun x:X => x) (idisweq X) p) p): forall X:Type1, forall X':Type1, 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:u2.paths _ v uis). unfold weqtopaths in uv. apply (u2.weqfg (u2.paths Type1 X X') (weq X X') (eqweqmap X X') (equivalenceaxiom X X') uis). assert (ee:u2.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':u2.paths _ (R' v) (R' uis)). apply (u2.maponpaths (weq X X') (P X) R' _ _ e). assumption. induction ee. apply l1. assumption. Defined. Corollary isweqweqtransportb (P:Type1 -> Type1)(R: forall X:Type1, forall X':Type1, forall u:X -> X', forall is: isweq X X' u, P X' -> P X)(r: forall X:Type1, forall p:P X, paths _ (R X X (fun x:X => x) (idisweq X) p) p): forall X:Type1, forall X':Type1, 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:Type1)(X':Type1)(u:X->X')(is:isweq _ _ u)(Y:Type1): isweq _ _ (fun f:X'->Y => (fun x:X => f (u x))). Proof. intros. set (P:= fun X0:Type1 => (X0 -> Y)). set (R:= fun X0:Type1 => (fun X0':Type1 => (fun u0:X0 -> X0' => (fun is0:isweq _ _ u0 => (fun f:P X0' => (fun x:X0 => f (u0 x))))))). set (r:= fun X0:Type1 => (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:Type1)(X':Type1)(u:X->X')(is:isweq _ _ u)(Y:Type1)(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:Type1) : 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:Type1)(Y:Type1)(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:Type1)(P1:T -> Type1)(P2:T-> Type1)(e: u2.paths _ P1 P2): u2.paths _ (forall t:T, P1 t) (forall t:T, P2 t). Proof. intros. induction e. apply u2.idpath. Defined. Lemma ifcontrthenunit: forall T:Type1, (iscontr T) -> u2.paths _ T unit. Proof. intros. apply ifcontrthenunit1 in X. apply weqtopaths in X. assumption. Defined. Lemma iscontrtounit (T:Type1) :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:Type1, (iscontr T) -> (isaprop T). Proof. intros. apply ifcontrthenunit in X. assert (e:isaprop unit). apply unitisaprop. induction X. assumption. Defined.