{-

\begin{verbatim} Time-stamp: "98/03/01 22:37:15 peter" \end{verbatim}

\newcommand{\defocc}[1]{\framebox{\emph{#1}}} % Defining occurrence

An attempt at a standard prelude .

\tableofcontents

-} {-

\section{ General utilities }

-} Pow ( A : Type ) = {-the Type of set-valued functions defined on A-} ( a : A )-> Set : Type, Fam ( A : Type ) = {-the Type of functions into A-} sig { I : Set, g : ( i : I )-> A } : Type, OP ( A : Type ) = {-the Type of unary operators on type A-} ( a : A )-> A : Type, BINOP ( A : Type ) = {-The Type of binary OPerators on a type A-} ( a : A )-> OP A : Type , op = {-the unary OPerator from a set to the set of unary operators on it-} \ A -> ( a : A )-> A : OP Set, binop = {-The unary OPerator from a set to the set of binary operators on it.-} \ A -> ( a : A )-> op A : OP Set, Connective = {-the Type of binary (non-dependent) operators on sets-} BINOP Set : Type, Quantifier ( A : Type ) = {-The Type of quantifiers (second level predicates) over $A$-} Pow (Pow A) : Type, or = {-the Connective for the co-product of two sets-} \ A B -> data { $inl ( a : A ), $inr ( b : B ) } : Connective, Sigma ( A : Set ) = {-the Quantifier on $A$ which holds of inhabited predicates-} \ B -> sig { p : A , q : B p } : Quantifier A, and = {-the Connective for the product of two sets-} \ A B -> Sigma A (\ junk -> B) : Connective, Pi ( A : Set ) = {-the Quantifier on A which holds of predicates true everywhere.-} \ B -> ( a : A )-> B a : Quantifier A, arrow = {-the Connective for the set of functions between two sets-} \ A B -> Pi A (\ junk -> B) : Connective, fun = arrow : Connective, maybe = {-the OPerator on sets which adds in a new element.-} \ A -> data { $fail, $unit ( a : A ) } : OP Set, {-

\section { Useful inductively defined sets. }

-} Nat = {-the set of natural numbers-} data { $0, $S ( pred : Nat ) } : Set, W ( A : Set ) = {-The W quantifier on A-} \ B -> let { W' = data { $sup ( a : A , phi : fun (B a) W' ) } : Set } in W' : Quantifier A , end_of_prelude = [] : []