Contribution  Padova/SUBSETS
                          ============================

This directory contains a formalization in Coq of the content of this paper
describing a theory of subsets on a intuitionistic a predicative foundation:

G.Sambin, S.Valentini: 
Building up a toolbox for Martin-Lof's type theory: subset theory.
In Proc. of Twenty-five years of constructive type theory,
Oxford U.P. (1998) pp. 221-244.

Author & Date: Ferruccio Guidi
               Department of Computer Science, University of Bologna
               March 2005
E-mail : fguidi@cs.unibo.it
WWW    : http://www.cs.unibo.it/~fguidi

Installation procedure:
-----------------------

  To get this contribution compiled, type

    make 

  or

    make opt

  The main modules produced by the compilation are:

     Toolbox   provides the theory of subsets and its prerequisites

     Base      provides just the prerequisites

Description:
------------

Further information on this contribution:
-----------------------------------------

  The latest version of this development is maintained in the CVS repository
  of the HELM project <helm.cs.unibo.it> and can be downloaded at: 
   
  www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/SUBSETS.tgz