                           premise.demon.co.uk
         peter 2346 Mar 1 22:37
    /home/peter/half/standard.half

March 6, 1998

Time-stamp:  "98/03/01 22:37:15 peter"

An attempt at a standard prelude .

Contents

1 General utilities 1

2 Useful inductively defined sets. 3

1 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,

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