(* The work on the file started on  Feb. 16, 2010 *)
(* This is a snapshop of work in progress from Sep. 14, 2010. *)

  
(* The files u0.v, u1.v, u2.v, u01.v, u12.v and foundations.v contain the definitions and theorems which form the "basics" of the a foundations and a new approach to the type-theoretic formalization of mathematics. These foundations are inspired by the univalent model of type theory which interprets types as homotopy types (objects of the homotopy category which is defined using the standard set theory), Martin-Lof equality as paths spaces and universes as bases of universal ("univalent") fibrations.

The need to use several files and the distribution of the material among the files are dictated by the current situation with universe management in Coq. As of now there is no intended mechanism for an explicit control over the type universes by the user.  When the identifier "Type" is used the system creates a new universe connected to the previously created ones by a set of constraints which are automatically determined based on the context in which this particular instance of "Type" appears. If the resulting system of constraints becomes incompatible the system produces "Universe Inconsistency" message and does not allow further development. Since a new type universe is introduced essentially every time the identifier "Type" is used it soon becomes very difficult, in the case of a "Universe Inconsistency" situation, to analyze where the problem is and how to resolve it. 

In this version of the "foundations" we use a trick which allows us to avoid the prolifiration of type universes and the corresponding constrains. The current proofs require us in some places (actually in one place only - theorem funcontr) to use the hierarchy which cocnists of three levels of universes Type0, Type1 and Type2 with the condition that Type0:Type1,  Type1:Type2 and Type0 is a subtype of Type1 which is a subtype of Type2.

The files u0, u1, u2 contain the results which require only one universe level. These three files are identical. The universe in each of them is called UU. 

The files u01 and u12 contain the results which require a two-levels universe hierarchy. The file u01 uses universes Type0:=u0.UU and Type1:=u1.UU while u12 uses universes Type1:=u1.UU and Type2:=u2.UU. In all other ways the files u01 and u12 are identical.

The file foundations contains the results which require a three-levels universe hierarchy.   

I tried to keep the notations such that the names of types which are (expected to be) a property in the sense of being of level 1 start with "is" but I have not been very consistent about it. After functional extensionality is proved there follows a series of theorems which assert that different types of the form "is..." (iscontr, isweq etc.) are actuallly properties.

So far none of the developments use Prop. Files u0, u1 and u2 are the largest, followed by u01 and u12 and foundations itself is so far the smallest of the files. 

*)




Require Export u12 u01.



(* Theorem saying that if all members of a family are contractible then the space of sections of the family is contractible. *)

Theorem funcontr (T:Type0) (P: T -> Type0) (is: forall t:T, iscontr (P t)): iscontr (forall t:T, P t).
Proof. intros. assert (e: u1.paths _ P (fun t:T => unit)). apply (u12.funextfun _ _ P (fun t:T => unit) (fun t:T => ifcontrthenunit _ (is t))). assert (e': u1.paths _ (forall t:T, P t) (forall t:T, unit)). apply funpath1. assumption. assert (int: iscontr (forall t:T, unit)). apply iscontrtounit. induction e'. assumption. Defined. 


(* Proof of functional extensionality for sections of general families. *)

Theorem funextsec (T:Type0) (P: T-> Type0) (s1: forall t:T, P t)(s2: forall t:T, P t)(e: forall t:T, paths _ (s1 t) (s2 t)): paths _ s1 s2.
Proof. intros. assert (is1: iscontr (forall t:T, coconustot (P t) (s2 t))). apply funcontr. intro. apply iscontrcoconustot. assert (e': paths _ (fun t:T => coconustotpair _ _  (s1 t) (e t)) (fun t:T => coconustotpair _ _ (s2 t) (idpath _ (s2 t)))). unfold iscontr in is1. destruct is1. assert (int1:= x (fun t0 : T => coconustotpair (P t0) (s2 t0) (s1 t0) (e t0))). assert (int2:= x (fun t0 : T => coconustotpair (P t0) (s2 t0) (s2 t0) (idpath (P t0) (s2 t0)))). induction int2. assumption. 

set (f1:= fun z: (forall x : T, coconustot (P x) (s2 x)) => (fun x: T => pr21 _ _ (z x))). assert (ee: paths _ (fun t:T => s1 t) (fun t:T => s2 t)). apply (maponpaths _ _ f1 _ _ e'). apply etacorrectiononpaths. assumption. Defined. 



(* Proof of the fact that the funextmap from paths _ s1 s2 to forall t:T, paths _ (s1 t) (s2 t) is q weak equivalence. *)


Lemma funextweql1 (T:Type0)(P:T -> Type0)(g: forall t:T, P t): iscontr (total2 _ (fun f:forall t:T, P t => forall t:T, paths _ (f t) (g t))).
Proof. intros. set (X:= forall t:T, coconustot (P t) (g t)). assert (is1: iscontr X). apply (funcontr  _ (fun t:T => coconustot (P t) (g t)) (fun t:T => iscontrcoconustot (P t) (g t))).  set (Y:= total2 _ (fun f:forall t:T, P t => forall t:T, paths _ (f t) (g t))). set (p:= fun z: X => tpair _ (fun f:forall t:T, P t => forall t:T, paths _ (f t) (g t)) (fun t:T => pr21 _ _ (z t)) (fun t:T => pr22 _ _ (z t))).  set (s:= fun u:Y => (fun t:T => coconustotpair (P t) (g t) ((pr21 _ _ u) t) ((pr22 _ _ u) t))).  set (etap:= fun u: Y => tpair _ (fun f:forall t:T, P t => forall t:T, paths _ (f t) (g t)) (fun t:T => ((pr21 _ _ u) t)) (pr22 _ _ u)).

assert (eps: forall u:Y, paths _ (p (s u)) (etap u)).  intro.  destruct u. unfold p. unfold s. unfold etap.   simpl. assert (ex: paths _ x (fun t0:T => x t0)). apply etacorrection.  induction ex. apply idpath. 

assert (eetap: forall u:Y, paths _ (etap u) u). intro. unfold etap. destruct u. simpl.


set (ff:= fun fe: (total2 (forall t0 : T, P t0) (fun f : forall t0 : T, P t0 => forall t0 : T, paths (P t0) (f t0) (g t0))) => tpair _ (fun f : forall t0 : T, P t0 => forall t0 : T, paths (P t0) (f t0) (g t0)) (fun t0:T => (pr21 _ _ fe) t0) (pr22 _ _ fe)). 

assert (isweqff: isweq _ _ ff). apply (isweqfp (forall t:T, P t) (forall t:T, P t) (fun f:forall t:T, P t => (fun t:T => f t)) (fun f: forall t:T, P t => forall t:T, paths (P t) (f t) (g t)) (isweqetacorrection T P)). 

assert (ee: forall fe: (total2 (forall t0 : T, P t0) (fun f : forall t0 : T, P t0 => forall t0 : T, paths (P t0) (f t0) (g t0))), paths _ (ff (ff fe)) (ff fe)). intro. apply idpath.  assert (eee: forall fe: (total2 (forall t0 : T, P t0) (fun f : forall t0 : T, P t0 => forall t0 : T, paths (P t0) (f t0) (g t0))), paths _ (ff  fe) fe). intro. apply (isweqpaths1 _ _ ff isweqff _ _ (ee fe)).  

apply (eee (tpair _ _ t x)). assert (eps0: forall u: Y, paths _ (p (s u)) u). intro. apply (pathscomp0 _ _ _ _ (eps u) (eetap u)). 
 
apply (contrl1' X Y p s eps0). assumption. Defined. 



Definition funextmap (T:Type0) (P:T -> Type0) (f:forall t:T, P t)( g: forall t:T, P t): (paths (forall t:T, P t) f g) -> (forall t:T, paths (P t) (f t) (g t)).
Proof. intros. induction X. apply idpath. Defined. 

Theorem isweqfunextmap(T:Type0)(P:T -> Type0)(f: forall t:T, P t) (g: forall t:T, P t): isweq _ _ (funextmap T P f g). 
Proof. intros. set (tmap:= fun ff: total2 _ (fun f0: forall t:T, P t, paths _ f0 g) => tpair _ (fun f0:forall t:T, P t => forall t:T, paths _ (f0 t) (g t)) (pr21 _ _ ff) (funextmap _ P (pr21 _ _ ff) g (pr22 _ _ ff))). assert (is1: iscontr (total2 _ (fun f0: forall t:T, P t, paths _ f0 g))). apply (iscontrcoconustot _ g).   assert (is2:iscontr (total2 _ (fun f0:forall t:T, P t => forall t:T, paths _ (f0 t) (g t)))). apply funextweql1.  
assert (isweq _ _ tmap).  apply (ifcontrcontrthenweq _ _ tmap is1 is2).  apply (isweqtotaltofib _ (fun f0: forall t:T, P t, paths _ f0 g) (fun f0:forall t:T, P t => forall t:T, paths _ (f0 t) (g t)) (fun f0:forall t:T, P t =>  (funextmap _ P f0 g)) X f).  Defined. 



(* More theorems about levels. *)

(* Theorem saying that if each member of a family is of level n then the space of sections of the family is of level n. *)

Theorem impred (n:nat)(T:Type0)(P:T -> Type0): (forall t:T, isoflevel n (P t)) -> (isoflevel n (forall t:T, P t)).
Proof. intro. induction n. intros.  apply (funcontr T P X). intros. unfold isoflevel in X.  unfold isoflevel. intros. 

assert (is: forall t:T, isoflevel n (paths _ (t1 t) (t2 t))).  intro. apply (X t (t1 t) (t2 t)).  
assert (is2: isoflevel n (forall t:T, paths _ (t1 t) (t2 t))). apply (IHn _ (fun t0:T => paths _ (t1 t0) (t2 t0)) is).
set (u:=funextmap _ P t1 t2).  assert (is3:isweq _ _ u). apply isweqfunextmap.  set (v:= invmap _ _ u is3). assert (is4: isweq _ _ v). apply invisweq. apply (levelweq n _ _ v is4). assumption. Defined.



(* Theorems saying that  (iscontr T) and (isweq f) are of level 1 (i.e. isaprop). *)



Lemma unitl5: iscontr (iscontr unit).
Proof. set (c:=unitiscontr). split with c. intro. induction t. unfold c. unfold unitiscontr. set (y:= (fun x0 : unit => unit_rect (fun x1 : unit => paths unit x1 tt) (idpath unit tt) x0)).  simpl in y. induction t.   assert (e: forall u: unit, paths _ (x u) (y u)). intro.  induction u. simpl. apply unitl3. assert (ee: paths _ x y). apply (funextsec _ (fun u:unit => paths _ u tt) x y e).  induction ee. 

assert (ee: paths _ x (fun x0 : unit =>
         unit_rect (fun x1 : unit => paths unit x1 tt) (idpath unit tt) x0)).  assert (eee: forall t:unit, paths _ (x t) ( (fun x0 : unit =>
         unit_rect (fun x1 : unit => paths unit x1 tt) (idpath unit tt) x0) t)). intro.  induction t. assert (e1:paths (paths unit tt tt) (x tt) (idpath _ tt)). apply unitl3. assert (e2: paths (paths unit tt tt)
     (unit_rect (fun x1 : unit => paths unit x1 tt) (idpath unit tt) tt) (idpath _ tt)).  apply unitl3. induction e1. apply pathsinv0. assumption. apply funextsec. assumption.  induction ee.  apply idpath.  Defined. 


Theorem iscontriscontr: forall T:Type0, iscontr(T)->iscontr(iscontr(T)).
Proof. intros. apply ifcontrthenunit in X. assert (is: iscontr (iscontr unit)). apply unitl5. induction X.  assumption. Defined. 



Theorem iscontrisaprop (T:Type0): isaprop (iscontr T).
Proof. intros.  unfold isaprop.  unfold isoflevel. intros. assert (is: iscontr(iscontr T)). apply iscontriscontr. apply t1. assert (is2: isaprop (iscontr T)). apply (ifcontrthenaprop _ is). apply (is2 t1 t2). Defined.  



Theorem isweqisaprop (X:Type0)(Y:Type0)(f:X-> Y) : isaprop (isweq _ _ f).
Proof. intros. unfold isweq.  apply (impred 1 _ (fun y:Y => iscontr (hfiber X Y f y)) (fun y:Y => iscontrisaprop (hfiber X Y f y))).  Defined. 












(****

Here we start the study of structures. The most fundamental structure is a "pointed type" and we begin with theorems about the space of pointed types. This is closely related to the study of so called "heterogenious equality".

****)


Definition ptype:Type1 := u1.total2 _ (fun T:Type0 => T).

Definition ptypepair:= u1.tpair _ (fun T:Type0 => T).
Definition el (X: ptype):= u1.pr21 _ _ X.
Definition dp (X: ptype):= u1.pr22 _ _ X. 

Definition pfun (X: ptype)(Y: ptype): Type0 := total2 (el X -> el Y) (fun f: el X -> el Y => paths _ (f (dp X)) (dp Y)). 
Definition pfunpair (X: ptype)(Y: ptype):= tpair _ (fun f: el X -> el Y => paths _ (f (dp X)) (dp Y)).

Definition idpfun (X:ptype): pfun X X := pfunpair _ _ (fun x:(el X) => x) (idpath _ (dp X)). 




Definition ispweq (X: ptype)(Y:ptype) (f: pfun X Y):= isweq _ _ (pr21 _ _ f).
Definition pweq (X: ptype)(Y: ptype): Type0 := total2 _ (fun f: pfun X Y => ispweq _ _ f).


Definition pweqpair  (X: ptype)(Y: ptype):= tpair _ (fun f: pfun X Y => ispweq _ _ f).


Definition pidisweq (X: ptype): ispweq _ _ (idpfun X) := idisweq (el X). 

Definition idpweq (X: ptype):pweq X X:= pweqpair _ _ (idpfun X) (pidisweq X).

Definition peqweqmap (X:ptype)(Y:ptype): u1.paths _ X Y -> pweq X Y.
Proof. intros.  induction X0. apply idpweq. Defined. 



(*

Theorem peqth (X:ptype)(Y:ptype): isweq _ _ (peqweqmap X Y).
Proof. intros. unfold isweq. intro.  


Definition ismonic (T1:Type) (T2:Type) (f:T1 -> T2) : Type := forall t1:T1, iscontr(hfiber T1 T2 f (f t1)).

Definition newprop : Type := total2 Type (fun T:Type =>  isaprop T).



(***** Prop is used from this point on ****)



Inductive Isnonempty (T:Type):Prop := wtn:T->(Isnonempty T).

Axiom contractiblechoice: forall T:Type, (iscontr T) -> (isweq T (Isnonempty T) (wtn T)). 

Definition Issurjective (T1:Type) (T2:Type) (f:T1 -> T2) : Prop := forall t2:T2, exists t1, (f t1)= t2.

Definition Isinjective (T1:Type) (T2:Type) (f:T1-> T2): Prop := forall t11:T1, forall t12:T1, ((f t11)=(f t12) -> (t11=t12)).

Definition Isbijective (T1:Type) (T2:Type) (f:T1-> T2) : Prop := (Issurjective T1 T2 f)/\(Isinjective T1 T2 f).





(* CONJECTURES *)



(***)







Conjecture boolisaset: isaset (bool).

Conjecture nataset: isaset (nat).




Definition Rel:= total2 Type (fun T:Type => (T -> T -> Prop)).
Definition relpair (T:Type) (R:T->T->Prop) : Rel := tpair Type (fun T:Type => (T -> T -> Prop)) T R.

Conjecture Releq: forall X:Type, forall Y:Type, forall Rx:X->X->Prop, forall Ry:Y->Y->Prop, forall f:X->Y, forall is1:isweq _ _ f, forall is2: (forall x1:X, forall x2:X, Rx x1 x2 <-> Ry (f x1) (f x2)), paths Rel (relpair X Rx) (relpair Y Ry).

    

Conjecture bijisweq: forall T1:Type, forall T2:Type, forall f:T1 -> T2, forall s1: isaset T1, forall s2: isaset T2,
Isbijective T1 T2 f  -> isweq T1 T2 f.



*)