[Agda] eta expansion

[Peter LeFanu Lumsdaine]

On Tue, Mar 19, 2013 at 3:56 PM, Peter Hancock <hancock at spamcop.net> wrote:

> May I ask a naive question that puzzles me?  In type theory, there is no
> constructor making types A = B from types A and B.  There is only
> the type a =_A b between objects of type A.  So how to express the
> univalence axiom
> in type theory?


The univalence axiom is usually taken to refer to a specific universe; i.e.
for a universe (U, El : U -> Type), it states that for each A,B:U, the
canonical map (A =_U B) -> (Equiv (El A) (El B)) is itself an equivalence.

(Indeed, it doesn’t really care about U being a universe — one can look at
the same statement for any family of types (X, P : X -> Type).)

So it does use a universe, as you say, but it doesn’t require any sort of
normal form theorem.

(One can also write down univalence-like axioms which don’t refer to a
universe, though.  One form, for instance would be to take the higher
inductive interval — the type I generated by points 0, 1 : I and an
equality between them — and posit a “large elim” for it, stating that given
any two types A, B, and an equivalence e, there is a dependent type G_e : I
-> Type such that G_e(0) = A, G_e(1) = B, and transport in G_e along the
path from 0 to 1 recovers e.  But this is a non-standard approach and
hasn’t been studied much.)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130319/e6b64b0c/attachment.html