Type Constructions
(* SOME CONSTRUCTION FOR THE SORT TYPE *)
(* by Venanzio Capretta *)
(* Coq version 6.2.3 *)
Implicit Arguments On.
(* Products of types *)
Section Type_products.
Variables T1, T2 : Type.
(* Product of two types. *)
Inductive
prodT : Type :=
pairT : T1 -> T2 -> prodT.
(* Projection functions. *)
Definition
fstT : prodT -> T1 :=
[z : prodT]
Cases z of
(pairT x y) => x
end.
Definition
sndT : prodT -> T2 :=
[z : prodT]
Cases z of
(pairT x y) => y
end.
End Type_products.
Implicit Arguments Off.
(* Sigma types with first component in Type and secon in Set. *)
Inductive
sigTS [T:Type; P:T->Set] : Type :=
existTS : (A : T)(P A) -> (sigTS T P).
Implicit Arguments On.
Section Sigma_Type_Set.
Variable T : Type.
Variable P : T -> Set.
Definition
projTS1 : (sigTS T P) -> T :=
[p : (sigTS T P)]
Cases p of (existTS A x) => A end.
Definition
projTS2 : (p : (sigTS T P))(P (projTS1 p)) :=
[p : (sigTS T P)]
<[p : (sigTS T P)](P (projTS1 p))>
Cases p of (existTS A x) => x end.
End Sigma_Type_Set.
Implicit Arguments Off.
25/02/99, 14:36