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