univalence without coherent equivalences

1 view
Skip to first unread message

Michael Shulman

unread,
Aug 10, 2017, 4:58:15 PM8/10/17
to homotopyt...@googlegroups.com
Thinking about the recently re-mentioned characterization of
univalence in terms of a map
Equiv A B -> (A = B)
that is only assumed to be a section of the canonical map in the other
direction, it occurred to me that this gives a way to state the
univalence axiom without first needing any "coherent" notion of
equivalence. For at least if we have funext to start with, then
equalities in Equiv A B are (for any coherent definition of Equiv A B)
equivalent to equalities in A -> B, so we can state the retraction
property in terms of those.

More precisely, let
coe : (A = B) -> A -> B
be coercion along an equality, and let
QInv A B := Sigma(f:A->B) Sigma(g:B->A) ( (Pi(x:A) g(f(x)) = x)
\times (Pi(y:B) f(g(y))=y) )
be the type of quasi-invertible functions (incoherent equivalences).
We know that it is inconsistent to ask that the map (A = B) -> QInv A
B induced by coe is quasi-invertible. But suppose we instead ask for
just
ua : QInv A B -> (A = B)
and
uabeta : Pi((f,g,a,b) : QInv A B) Pi(a:A), coe (ua (f,g,a,b)) a = f(a)
If full univalence holds, then such functions certainly exist, since
any quasi-inverse can be improved to a coherent equivalence. But
conversely, if we assume funext to start with, then the full
univalence axiom can be proven from this ua and uabeta. (I just
formalized this in Coq to be sure.)

Maybe other people have already observed this, but I don't think I
noticed it before. It means that we don't need to invent or motivate
a coherent notion of equivalence before stating (or, in cubical type
theory or a semantic model, proving) univalence. Instead we can state
univalence in this way, and then (having already motivated funext,
which is much easier, and also has a "weak improves to strong"
theorem) motivate the search for a "good" definition of Equiv A B as
"can we define more explicitly a type that is equivalent to A = B"?

Mike

Nicolai Kraus

unread,
Aug 13, 2017, 6:05:22 PM8/13/17
to HomotopyT...@googlegroups.com
I had not looked at this from this angle so far. If you want to avoid having to come up and justify a notion of equivalence, you could, alternatively to ua + uabeta, take the Orton-Pitts "Axioms for univalence"
www.cl.cam.ac.uk/~amp12/papers/axiu/axiu.pdf
Maybe these are even easier to justify than ua + uabeta!
Nicolai

Michael Shulman

unread,
Aug 14, 2017, 12:16:05 AM8/14/17
to Nicolai Kraus, HomotopyT...@googlegroups.com
Yes, of course their axioms also have the same effect. Their axioms
are special cases of ua + uabeta, so at least at a technical level
they are no harder to check, and in some cases are easier (which was I
believe their point). However, intuitively I think I find it easier
to motivate the more general ua + uabeta: it has the same intuition as
full univalence, but avoids any bother about what we mean by
"equivalence". If I just showed someone the Orton-Pitts axioms I feel
like they would say "that seems like a kinda random collection of
assertions".
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Andrew Pitts

unread,
Aug 14, 2017, 5:30:04 AM8/14/17
to Michael Shulman, HomotopyT...@googlegroups.com, Prof. Andrew M Pitts
On 14 August 2017 at 05:15, Michael Shulman <shu...@sandiego.edu> wrote:
> Yes, of course their axioms also have the same effect. Their axioms
> are special cases of ua + uabeta, so at least at a technical level
> they are no harder to check, and in some cases are easier (which was I
> believe their point). However, intuitively I think I find it easier
> to motivate the more general ua + uabeta: it has the same intuition as
> full univalence, but avoids any bother about what we mean by
> "equivalence". If I just showed someone the Orton-Pitts axioms I feel
> like they would say "that seems like a kinda random collection of
> assertions”.

I wouldn’t disagree with that — I see the axioms Ian and I gave in
that note as something one might use to verify that a model is
univalent, not as the definition univalence one would give initially.
The initial definition I would use is simply that every equivalence in
a universe arises as transport along an identification, having first
defined equivalence the way Voevodsky did (contractible fibres). This
is conceptually appealing to me; and relpacing “every equivalence” by
“every isomorphism” is nice (I had noticed that finesse before),
except for the fact that transport along an identification is in
general an equivalence rather than an iso. But anyway, when you get
down to actually verifying that this holds for a model, the O-P axioms
may be easier to check.

Andy

Michael Shulman

unread,
Aug 14, 2017, 5:33:15 AM8/14/17
to Andrew Pitts, HomotopyT...@googlegroups.com
On Mon, Aug 14, 2017 at 2:29 AM, Andrew Pitts <Andrew...@cl.cam.ac.uk> wrote:
> and replacing “every equivalence” by
> “every isomorphism” is nice (I had noticed that finesse before),
> except for the fact that transport along an identification is in
> general an equivalence rather than an iso.

Transport along an identification is certainly an "isomorphism" too;
isn't that just as easy to prove as that it's an equivalence (for any
notion of coherent equivalence)?

Andrew Pitts

unread,
Aug 14, 2017, 5:37:05 AM8/14/17
to Michael Shulman, HomotopyT...@googlegroups.com
Oh, yes, quite right (note to self: think before you post!)

Andy
Reply all
Reply to author
Forward
0 new messages