Switch branches/tags
Nothing to show
Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
..
Failed to load latest commit information.
Alg-IIR.agda
Containers.agda
Data.agda
Data1.agda
Desc.agda
Desc.v
DescFix.agda
DescStrat.agda
DescStrat.lhs
DescTT.agda
FMSB.agda
IDesc.agda
IDescTT.agda
ILabel.agda
IMDesc.agda
Prob.agda
README.Descriptions
Records.agda
RevisedHutton.agda
StratSigma.agda

README.Descriptions

****************************************************************
                        Descriptions
****************************************************************


The models of Epigram's universe of descriptions are:
    - DescTT.agda: model of descriptions
      		 (with type-in-type)
    - Desc.agda: model of descriptions
      		 (with universe polymorphism)
    - Desc.v: model of descriptions
      	      (with typical ambiguity)
    - DescStrat.agda: model of descriptions, with no fancy stuff
              (chopped of at Desc42, 
	       see DescStrat.lhs for cutting at any N)
    - IDescTT.agda: model of indexed descriptions
      		    (with type-in-type)
    - IDesc.agda: model of indexed descriptions
      		  (with universe polymorphism)

Each of these file is self-contained: we build our own equipment for
Sigma-type, sums, and equality. This corresponds to the requirements
we have in the paper wrt. the underlying type-theory (excepted for
equality and Pi-types, which we inherit from Agda).


These files follow the plan of the paper:

* Desc.agda implements the universe of inductive types, Desc, the
  examples, and generic constructions of Section 3 and 4.

* DescTT.agda is similar to Desc.agda, excepted that the hierarchy of
  Sets is collapsed by --type-in-type.

* IDescTT.agda implements the universe of inductive families, IDesc,
  the examples, and generic constructions of Section 5. 

* IDesc.agda is the stratified implementation of indexed
  descriptions. We also describe IDesc in itself and prove that it is
  isomorphic to the host one.


As shown by Desc.agda and IDesc.agda, --type-in-type is not necessary
for DescTT.agda and IDescTT.agda. But the *TT version make prototyping
easier, as the universe polymorphic version is cluttered with lifting
operations and implicit levels that requires extreme care.