Re: [HoTT] univalence without coherent equivalences

[Andrew Pitts <Andrew...@cl.cam.ac.uk>]

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