[Agda] Universe construction

[David Haguenauer]

* Nils Anders Danielsson <nad at Cs.Nott.AC.UK>, 2011-01-13 18:53:34 Thu:
> On 2011-01-12 00:27, David Haguenauer wrote:
> >Are there any examples of significant developments making use of
> >universe construction?
> If by "universe" you mean (roughly) a set of codes U and an
> interpretation function El : U -> Set, then yes, universes are used
> quite a lot. [...] Did you have something more specific in mind?

That's what I had in mind. There are cases where I don't know how to
translate examples found in the literature into something that Agda
accepts, but that's probably just because of inexperience on my side.


* Dan Doel <dan.doel at gmail.com>, 2011-01-13 13:59:19 Thu:
> On Tuesday 11 January 2011 6:27:32 pm David Haguenauer wrote:
> > Are there any examples of significant developments making use of
> > universe construction? Or reasons why not?
> Universes go all the way back to Martin-Loef (at least). [...]
>
> while it's interesting to use Agda's support for induction-recursion
> to play with the Martin-Loef sort of setup, it isn't as necessary,
> because Agda includes a lot of the features that these universes
> would otherwise add to the theory as built-ins.
> 
> The utility in Agda thus falls to other things. [...]

Thanks for the great answers, it's exactly the kind of thing I wanted
to know.

-- 
David Haguenauer
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 254 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20110115/337939af/attachment.bin