[Agda] eta expansion
Peter LeFanu Lumsdaine
p.l.lumsdaine at gmail.com
Tue Mar 19 21:37:26 CET 2013
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...
More information about the Agda