{-

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

\newcommand{\defocc}{\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 = [] : []