Library uuu
Introduction. Vladimir Voevodsky . Feb. 2010 - Sep. 2011
Unset Automatic Introduction.
This line has to be removed for the file to compile with Coq8.2
Universe structure
Notation UUU := Set .
Empty type. The empty type is introduced in Coq.Init.Datatypes by the line:
Inductive Empty_set : Set := .
Notation empty := Empty_set.
Notation empty_rect := Empty_set_rect.
Identity Types. Idenity types are introduced in Coq.Init.Datatypes by the lines :
Inductive identity ( A : Type ) ( a : A ) : A -> Type := identity_refl : identity _ a a .
Hint Resolve identity_refl : core .
Notation paths := identity .
Notation a = b added by B.A., oct 2014
Notation "a = b" := (paths a b) (at level 70, no associativity) : type_scope.
Notation idpath := identity_refl .
Notation paths_rect := identity_rect .
Notation idpath := identity_refl .
Notation paths_rect := identity_rect .
Coproducts .
The coproduct of two types is introduced in Coq.Init.Datatypes by the lines:
Inductive sum (A B:Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B.
Notation coprod := sum .
Notation ii1fun := inl .
Notation ii2fun := inr .
Notation ii1 := inl .
Notation ii2 := inr .
Implicit Arguments ii1 [ A B ] .
Implicit Arguments ii2 [ A B ] .
Notation coprod_rect := sum_rect.
Dependent sums.
One can not use a new record each time one needs it because the general theorems about this
construction would not apply to new instances of "Record" due to the "generativity" of inductive
definitions in Coq. One could use "Inductive" instead of "Record" here but using "Record" which is
equivalent to "Structure" allows us later to use the mechanism of canonical structures with total2.
Inductive total2 { T: Type } ( P: T -> Type ) := tpair : forall ( t : T ) ( p : P t ) , total2 P .
Arguments tpair {T} _ _ _.
Definition pr1 ( T : Type ) ( P : T -> Type ) ( t : total2 P ) : T .
Proof . intros . induction t as [ t p ] . exact t . Defined.
Arguments pr1 {_ _} _.
Definition pr2 ( T : Type ) ( P : T -> Type ) ( t : total2 P ) : P ( pr1 t ) .
Proof . intros . induction t as [ t p ] . exact p . Defined.
Arguments pr2 {_ _} _.
The following command checks wheather the patch which modifies the universe level assignement for inductive types have been installed. With the patch it returns paths 0 0 : UUU . Without the patch it returns paths 0 0 : Prop .
Check (O = O) .