(* First we fix a universe: *)

Definition UU := Type. 

(* We now re-define the idenity types using the inductive machinery of Coq: *) 

Inductive paths ( X : UU ) ( x : X ) : X -> UU := idpath : paths X x x.

(* ... and dependent sums using the same machinery: *)

Inductive total2 (X : UU ) ( Q : X -> UU ) : UU := tpair: forall x : X, forall y : Q x, total2 X Q. 

(* The first fundamental definition of the univalent approach is the definition of types of h-level 0 or contractible types *)

Definition iscontr ( X : UU ) := total2 X (fun x : X => forall y : X, paths X x y). 

(* To define weak equivalences one proceeds in two steps. Fisrt one defines the notion of the h-fiber of a function over a point: *)

Definition hfiber ( X Y : UU ) ( f : X -> Y ) ( y : Y ) := total2 X (fun pointover : X => paths Y (f pointover) y). 

(* then one defines a function to be a weak equivalence if all of its h-fibers are contractible: *)

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

(* "Propositions" or types of h-level 1 are defined by: *)

Definition isaprop (X:UU) := forall x1:X, forall x2:X, iscontr (paths X x1 x2). 

(* ... and then sets are defined by: *)

Definition isaset (X:UU) := forall x1:X, forall x2:X, isaprop (paths X x1 x2). 


(* The following theorems show that the expressions given above whose name starts with "is" are indeed properties i.e. types of h-level 1. The proofs of these theorems require functional extensionality. *)

Theorem isapropiscontr ( X : UU ) :isaprop ( iscontr X ).
Proof. Admitted.

Theorem isapropisweq ( X Y : UU ) ( f : X -> Y ) : isaprop ( isweq X Y f ).
Proof. Admitted. 

Theorem isapropisaprop ( X : UU ) : isaprop ( isaprop X ).
Proof. Admitted.


Theorem isapropisaset ( X : UU ) : isaprop ( isaset X ).
Proof. Admitted. 


(* The following theorem asserts that natural numbers form a set.  The proof of this theorem is not very simple. See [ isasetnat ] in uu0.v *)

Theorem th1: isaset nat.
Proof.  Admitted. 







(* 
*** Local Variables: ***
*** coq-prog-name: "/opt/local/bin/coqtop" ***
*** coq-prog-args: ("-emacs-U") ***
*** End: ***
 *)