* univalence without coherent equivalences @ 2017-08-10 20:57 Michael Shulman 2017-08-13 22:05 ` [HoTT] " Nicolai Kraus 0 siblings, 1 reply; 6+ messages in thread From: Michael Shulman @ 2017-08-10 20:57 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] univalence without coherent equivalences 2017-08-10 20:57 univalence without coherent equivalences Michael Shulman @ 2017-08-13 22:05 ` Nicolai Kraus 2017-08-14 4:15 ` Michael Shulman 0 siblings, 1 reply; 6+ messages in thread From: Nicolai Kraus @ 2017-08-13 22:05 UTC (permalink / raw) To: HomotopyTypeTheory [-- 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 --] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] univalence without coherent equivalences 2017-08-13 22:05 ` [HoTT] " Nicolai Kraus @ 2017-08-14 4:15 ` Michael Shulman 2017-08-14 9:29 ` Andrew Pitts 0 siblings, 1 reply; 6+ messages in thread From: Michael Shulman @ 2017-08-14 4:15 UTC (permalink / raw) To: Nicolai Kraus; +Cc: 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". 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. ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] univalence without coherent equivalences 2017-08-14 4:15 ` Michael Shulman @ 2017-08-14 9:29 ` Andrew Pitts 2017-08-14 9:32 ` Michael Shulman 0 siblings, 1 reply; 6+ messages in thread From: Andrew Pitts @ 2017-08-14 9:29 UTC (permalink / raw) To: Michael Shulman; +Cc: 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 ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] univalence without coherent equivalences 2017-08-14 9:29 ` Andrew Pitts @ 2017-08-14 9:32 ` Michael Shulman 2017-08-14 9:36 ` Andrew Pitts 0 siblings, 1 reply; 6+ messages in thread From: Michael Shulman @ 2017-08-14 9:32 UTC (permalink / raw) To: Andrew Pitts; +Cc: 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)? ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] univalence without coherent equivalences 2017-08-14 9:32 ` Michael Shulman @ 2017-08-14 9:36 ` Andrew Pitts 0 siblings, 0 replies; 6+ messages in thread From: Andrew Pitts @ 2017-08-14 9:36 UTC (permalink / raw) To: Michael Shulman; +Cc: HomotopyT...@googlegroups.com 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 ^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2017-08-14 9:37 UTC | newest] Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-08-10 20:57 univalence without coherent equivalences Michael Shulman 2017-08-13 22:05 ` [HoTT] " Nicolai Kraus 2017-08-14 4:15 ` Michael Shulman 2017-08-14 9:29 ` Andrew Pitts 2017-08-14 9:32 ` Michael Shulman 2017-08-14 9:36 ` Andrew Pitts
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).