[Agda] Embedded universe polymorphic programming.

[flicky frans]

Thanks for the answers.


Frédéric Blanqui, yep, that could be useful. I've played a little with
cumulativity, and looks like it's possible to have some cumulativity
almost without explicit intocorporating it in the datatype definitions
[1]. For example this works:

  test : Term (‵Type (suc zero) ⟶ ‵Type (suc (suc (suc (suc zero)))))
  test = ⇧ λ A -> type-↑ (‵Lift (detag A))

  test-test : Term (⟦ test · type-↑ ((‵Type zero ‵Π‵ λ A -> A) ⟶ ‵Level₀) ⟧
                      ⟶ ((‵Type zero ‵Π‵ λ A -> A) ⟶ ‵Level₀))
  test-test = ⇧ λ x -> ↑ (tag (detag x))      -- (tag ∘ detag) reduces
expression

where ‵Lift is not a constructor, but the plain function.

Vladimir Voevodsky, thanks, I'll study your paper.

Andreas Abel, I've mentioned this paper in the first post. It's a
great paper, but I'm not sure, if it's possible with Larry Diehl's
encoding to freely manipulate types like values.

[1] http://lpaste.net/112179