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