univalence without coherent equivalences

univalence without coherent equivalences

[Michael Shulman]

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

Re: [HoTT] univalence without coherent equivalences

[Nicolai Kraus]

[-- Attachment #1: Type: text/plain, Size: 2388 bytes --]

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

On 10/08/17 21:57, Michael Shulman wrote:
> 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
>


[-- Attachment #2: Type: text/html, Size: 2866 bytes --]

Re: [HoTT] univalence without coherent equivalences

[Michael Shulman]

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".

On Sun, Aug 13, 2017 at 3:05 PM, Nicolai Kraus <nicola...@gmail.com> wrote:
> 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
>
>
> On 10/08/17 21:57, Michael Shulman wrote:
>
> 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
>
>
> --
> 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.

Re: [HoTT] univalence without coherent equivalences

[Andrew 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

Re: [HoTT] univalence without coherent equivalences

[Michael Shulman]

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)?

Re: [HoTT] univalence without coherent equivalences

[Andrew Pitts]

On 14 August 2017 at 10:32, Michael Shulman <shu...@sandiego.edu> wrote:
> 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)?

Oh, yes, quite right (note to self: think before you post!)

Andy