<div dir="ltr">On Tue, Mar 19, 2013 at 3:56 PM, Peter Hancock <span dir="ltr"><<a href="mailto:hancock@spamcop.net" target="_blank">hancock@spamcop.net</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div class="im"><span style="color:rgb(34,34,34)">May I ask a naive question that puzzles me? In type theory, there is no</span><br>
</div>
constructor making types A = B from types A and B. There is only<br>
the type a =_A b between objects of type A. So how to express the univalence axiom<br>
in type theory? </blockquote><div><br></div><div style>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.</div>
<div style><br></div><div style><div>(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).)</div><div><br></div></div><div style>So it does use a universe, as you say, but it doesn’t require any sort of normal form theorem.</div>
<div style><br></div><div style>(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.)</div>
</div></div></div>