[Agda] Universe construction

[Nils Anders Danielsson]

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. A very simple example is the universe (Bool, T):

   T : Bool → Set
   T true  = ⊤
   T false = ⊥

Another example is (ℕ, Vec A). Did you have something more specific in
mind?

-- 
/NAD