(* 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: ***
*)