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