[-- Attachment #1: Type: text/plain, Size: 2719 bytes --] Resurrecting this thread from many years ago, because I was thinking about it again recently, it seems to me that although { f & isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) = e judgmentally, it doesn't satisfy the rule that sym id = id judgmentally. (In particular, I am not sure what relational equivalence to use for the identity equivalence which does not change judgmentally when I flip the order of its arguments.) Is there a version of equivalence which simultaneously satisfies that the inverse of the identity is judgmentally the identity, and that inverting an equivalence twice judgmentally gives you what you started with? -Jason On Thu, Nov 13, 2014 at 12:59 PM Vladimir Voevodsky <vladimir@ias.edu> wrote: > In general no. But their model is essentially syntactic and more or less > complete. Or, to be more precise, I would expect it to > be more or less complete. > > V. > > > On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine < > p.l.lumsdaine@gmail.com> wrote: > > On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky <vladimir@ias.edu> > wrote: > >> The question is about how you interpret this operation for the univalent >> universe. If there is an interpretation of such an operation then there is >> a way to define equivalences between types in an involutionary way. >> > > I don’t follow why this should be the case. This shows that there is some > notion of equivalence *in the model* (i.e. constructed in the meta-theory) > which is strictly involutive. But there is no reason that this notion need > be definable in the syntax of the object theory, is there? > > –p. > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCao60%3DRFWY%3DCn0BTV9bWcRCQXRSqOjvCYbS37mHOeJ0Yqg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4424 bytes --] <div dir="ltr">Resurrecting this thread from many years ago, because I was thinking about it again recently, it seems to me that although { f & isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) = e judgmentally, it doesn't satisfy the rule that sym id = id judgmentally. (In particular, I am not sure what relational equivalence to use for the identity equivalence which does not change judgmentally when I flip the order of its arguments.) Is there a version of equivalence which simultaneously satisfies that the inverse of the identity is judgmentally the identity, and that inverting an equivalence twice judgmentally gives you what you started with?<div><br></div><div>-Jason</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Nov 13, 2014 at 12:59 PM Vladimir Voevodsky <<a href="mailto:vladimir@ias.edu">vladimir@ias.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;">In general no. But their model is essentially syntactic and more or less complete. Or, to be more precise, I would expect it to <div>be more or less complete. <br><div><br></div><div>V.</div><div><br></div><div><br><div><blockquote type="cite"><div>On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine <<a href="mailto:p.l.lumsdaine@gmail.com" target="_blank">p.l.lumsdaine@gmail.com</a>> wrote:</div><br class="gmail-m_-7971364555980655673Apple-interchange-newline"><div><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky <span dir="ltr"><<a href="mailto:vladimir@ias.edu" target="_blank">vladimir@ias.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The question is about how you interpret this operation for the univalent universe. If there is an interpretation of such an operation then there is a way to define equivalences between types in an involutionary way.<br><div class="gmail-m_-7971364555980655673HOEnZb"><div class="gmail-m_-7971364555980655673h5"></div></div></blockquote><div><br></div><div>I don’t follow why this should be the case. This shows that there is some notion of equivalence *in the model* (i.e. constructed in the meta-theory) which is strictly involutive. But there is no reason that this notion need be definable in the syntax of the object theory, is there?</div><div><br></div><div>–p. </div></div></div></div><div><br class="gmail-m_-7971364555980655673webkit-block-placeholder"></div> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> For more options, visit <a href="https://groups.google.com/d/optout" target="_blank">https://groups.google.com/d/optout</a>.<br> </div></blockquote></div><br></div></div></div> <p></p> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> For more options, visit <a href="https://groups.google.com/d/optout" target="_blank">https://groups.google.com/d/optout</a>.<br> </blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCao60%3DRFWY%3DCn0BTV9bWcRCQXRSqOjvCYbS37mHOeJ0Yqg%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCao60%3DRFWY%3DCn0BTV9bWcRCQXRSqOjvCYbS37mHOeJ0Yqg%40mail.gmail.com</a>.<br />

[-- Attachment #1.1: Type: text/plain, Size: 6134 bytes --] On 17/08/2019 01:14, Jason Gross wrote: > Resurrecting this thread from many years ago, because I was thinking > about it again recently, it seems to me that although { f & > isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) = e > judgmentally, it doesn't satisfy the rule that sym id = id > judgmentally. (In particular, I am not sure what relational equivalence > to use for the identity equivalence which does not change judgmentally > when I flip the order of its arguments.) Is there a version of > equivalence which simultaneously satisfies that the inverse of the > identity is judgmentally the identity, and that inverting an equivalence > twice judgmentally gives you what you started with? > > -Jason I am not sure this answer will be of the kind you are expecting. First I will consider the identity type and then the equivalence type using the same idea. I will use "=" for definitional equality. (1) If you have some identity type (_≡_, refl , J) with _≡_ : {X : 𝓤} → X → X → 𝓤 refl : {X : 𝓤 } (x : X) → x ≣ x J : (X : 𝓤) (A : (x y : X) → x ≡ y → 𝓤) → ((x : X) → A x x (refl x)) → (x y : X) (p : x ≡ y) → A x y p then you can define another identity type (_≡'_ , refl' , J') by x ≡' y = Σ (z : X), (z ≡ x) × (z ≡ y) (which is equivalent to the diagonal fiber of (x,y) and also to x ≡ y (both in pure MLTT)) refl' x = x , refl x , refl x J' X A f x y (z , p , q) = γ z x p y q where φ : (x y : X) (q : x ≡ y) → A x y (x , refl x , q) φ = J X (λ x y q → A x y (x , refl x , q)) f γ : (z x : X) (p : z ≡ x) (y : X) (q : z ≡ y) → A x y (z , p , q) γ = J X (λ z x p → (y : X) (q : z ≡ y) → A x y (z , p , q)) φ so that J' X A f x x (refl' x) = f x definitionally using the original J's computation rule. For this new identity type, we can define ≡'-sym : {X : 𝓤 ̇ } {x y : X} → x ≡' y → y ≡' x ≡'-sym (a , p , q) = (a , q , p) so that ≡'-sym (refl' x) = refl' x and ≡'-sym (≡'-sym p') = p', both definitionally. (2) Similarly we can define an equivalence type _≃'_ from an equivalence type _≃_ by X ≃' Y = Σ (Z : 𝓤), (Z ≃ X) × (Z ≃ X) with the analogous identity equivalence and symmetrization operation so that the definitional equalities you want hold. This is related to the relational definition of equivalence as follows. The type X × Y → 𝓤 of type-valued relations is in canonical bijection with the "slice type" Σ (Z : 𝓤), Z → X × Y by a well-known construction, and in turn to Σ (Z : 𝓤), (Z → X) × (Z → Y). When you restrict to relations R such that for all x:X and y:Y the types Σ (x : X), R x y and Σ (y : Y), R x y are contractible, the type Σ (Z : 𝓤), (Z → X) × (Z → Y) gets restricted to Σ (Z : 𝓤), (Z ≃ X) × (Z ≃ X) by the canonical equivalence (X × Y → 𝓤) ≃ Σ (Z : 𝓤), (Z → X) × (Z → Y). (3) If you want composition of identifications to be definitionally associative with refl definitionally neutral on both sides, you can consider the alternative identity type defined by x ≡'' y = (z : X) → (z ≡ x) → (z ≡ y) which is again equivalent to the original identity type x ≡ y (which amounts to Yoneda), refl'' x = (z : X) → λ (p : x ≡ z) , p because composition of identifications is given by function composition, which is definitionally associative with the identity function as its definitionally neutral element (assuming the η rule). (Exercise: write down J''.) (4) I don't know how to get the definitional equalities of (1) and (3) together by a suitable modification of the identity type. The constructions (1) and (3) are kind of dual. Martin On Thu, Nov 13, 2014 at 12:59 PM Vladimir Voevodsky <vlad...@ias.edu > <javascript:>> wrote: > >> In general no. But their model is essentially syntactic and more or less >> complete. Or, to be more precise, I would expect it to >> be more or less complete. >> >> V. >> >> >> On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine <p.l.l...@gmail.com >> <javascript:>> wrote: >> >> On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky <vlad...@ias.edu >> <javascript:>> wrote: >> >>> The question is about how you interpret this operation for the univalent >>> universe. If there is an interpretation of such an operation then there is >>> a way to define equivalences between types in an involutionary way. >>> >> >> I don’t follow why this should be the case. This shows that there is >> some notion of equivalence *in the model* (i.e. constructed in the >> meta-theory) which is strictly involutive. But there is no reason that >> this notion need be definable in the syntax of the object theory, is there? >> >> –p. >> >> -- >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com <javascript:>. >> For more options, visit https://groups.google.com/d/optout. >> >> >> -- >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com <javascript:>. >> For more options, visit https://groups.google.com/d/optout. >> > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/142000b0-e2e8-42cb-9201-4d2dcbec3de7%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 10258 bytes --] <div dir="ltr"><br><div>On 17/08/2019 01:14, Jason Gross wrote:</div><div>> Resurrecting this thread from many years ago, because I was thinking</div><div>> about it again recently, it seems to me that although { f &</div><div>> isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) = e</div><div>> judgmentally, it doesn't satisfy the rule that sym id = id</div><div>> judgmentally. (In particular, I am not sure what relational equivalence</div><div>> to use for the identity equivalence which does not change judgmentally</div><div>> when I flip the order of its arguments.) Is there a version of</div><div>> equivalence which simultaneously satisfies that the inverse of the</div><div>> identity is judgmentally the identity, and that inverting an equivalence</div><div>> twice judgmentally gives you what you started with?</div><div>></div><div>> -Jason</div><div><br></div><div><br></div><div>I am not sure this answer will be of the kind you are expecting.</div><div><br></div><div>First I will consider the identity type and then the equivalence type</div><div>using the same idea.</div><div><br></div><div>I will use "=" for definitional equality.</div><div><br></div><div>(1) If you have some identity type (_≡_, refl , J) with</div><div><br></div><div> _≡_ : {X : 𝓤} → X → X → 𝓤</div><div><br></div><div> refl : {X : 𝓤 } (x : X) → x ≣ x</div><div><br></div><div> J : (X : 𝓤) (A : (x y : X) → x ≡ y → 𝓤)</div><div> → ((x : X) → A x x (refl x))</div><div> → (x y : X) (p : x ≡ y) → A x y p</div><div><br></div><div>then you can define another identity type (_≡'_ , refl' , J') by</div><div><br></div><div><br></div><div> x ≡' y = Σ (z : X), (z ≡ x) × (z ≡ y)</div><div><br></div><div>(which is equivalent to the diagonal fiber of (x,y) and also to x ≡ y</div><div>(both in pure MLTT))</div><div><br></div><div><br></div><div> refl' x = x , refl x , refl x</div><div><br></div><div><br></div><div> J' X A f x y (z , p , q) = γ z x p y q</div><div> where</div><div> φ : (x y : X) (q : x ≡ y) → A x y (x , refl x , q)</div><div> φ = J X (λ x y q → A x y (x , refl x , q)) f</div><div><br></div><div> γ : (z x : X) (p : z ≡ x) (y : X) (q : z ≡ y) → A x y (z , p , q)</div><div> γ = J X (λ z x p → (y : X) (q : z ≡ y) → A x y (z , p , q)) φ</div><div><br></div><div>so that</div><div><br></div><div> J' X A f x x (refl' x) = f x</div><div><br></div><div>definitionally using the original J's computation rule.</div><div><br></div><div><br></div><div>For this new identity type, we can define</div><div><br></div><div> ≡'-sym : {X : 𝓤 ̇ } {x y : X} → x ≡' y → y ≡' x</div><div> ≡'-sym (a , p , q) = (a , q , p)</div><div><br></div><div>so that</div><div><br></div><div> ≡'-sym (refl' x) = refl' x</div><div><br></div><div>and</div><div><br></div><div> ≡'-sym (≡'-sym p') = p',</div><div><br></div><div>both definitionally.</div><div><br></div><div>(2) Similarly we can define an equivalence type _≃'_ from an equivalence type _≃_ by</div><div><br></div><div> X ≃' Y = Σ (Z : 𝓤), (Z ≃ X) × (Z ≃ X)</div><div><br></div><div>with the analogous identity equivalence and symmetrization operation</div><div>so that the definitional equalities you want hold.</div><div><br></div><div>This is related to the relational definition of equivalence as</div><div>follows. The type</div><div><br></div><div> X × Y → 𝓤</div><div><br></div><div>of type-valued relations is in canonical bijection with the "slice type"</div><div><br></div><div> Σ (Z : 𝓤), Z → X × Y</div><div><br></div><div>by a well-known construction, and in turn to</div><div><br></div><div> Σ (Z : 𝓤), (Z → X) × (Z → Y).</div><div><br></div><div>When you restrict to relations R such that for all x:X and y:Y the types</div><div><br></div><div> Σ (x : X), R x y</div><div><br></div><div>and</div><div><br></div><div> Σ (y : Y), R x y</div><div><br></div><div>are contractible, the type Σ (Z : 𝓤), (Z → X) × (Z → Y) gets restricted to</div><div><br></div><div> Σ (Z : 𝓤), (Z ≃ X) × (Z ≃ X)</div><div><br></div><div>by the canonical equivalence</div><div><br></div><div> (X × Y → 𝓤) ≃ Σ (Z : 𝓤), (Z → X) × (Z → Y).</div><div><br></div><div>(3) If you want composition of identifications to be definitionally</div><div>associative with refl definitionally neutral on both sides, you can</div><div>consider the alternative identity type defined by</div><div><br></div><div> x ≡'' y = (z : X) → (z ≡ x) → (z ≡ y)</div><div><br></div><div>which is again equivalent to the original identity type x ≡ y (which</div><div>amounts to Yoneda),</div><div><br></div><div> refl'' x = (z : X) → λ (p : x ≡ z) , p</div><div><br></div><div>because composition of identifications is given by function</div><div>composition, which is definitionally associative with the identity</div><div>function as its definitionally neutral element (assuming the η rule).</div><div><br></div><div> (Exercise: write down J''.)</div><div><br></div><div>(4) I don't know how to get the definitional equalities of (1) and (3)</div><div>together by a suitable modification of the identity type. The</div><div>constructions (1) and (3) are kind of dual.</div><div><br></div><div>Martin</div><div><br></div><blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div class="gmail_quote"><div dir="ltr">On Thu, Nov 13, 2014 at 12:59 PM Vladimir Voevodsky <<a href="javascript:" target="_blank" gdf-obfuscated-mailto="1oMZCNpxAQAJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">vlad...@ias.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>In general no. But their model is essentially syntactic and more or less complete. Or, to be more precise, I would expect it to <div>be more or less complete. <br><div><br></div><div>V.</div><div><br></div><div><br><div><blockquote type="cite"><div>On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine <<a href="javascript:" target="_blank" gdf-obfuscated-mailto="1oMZCNpxAQAJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">p.l.l...@gmail.com</a>> wrote:</div><br><div><div dir="ltr"><div><div class="gmail_quote">On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky <span dir="ltr"><<a href="javascript:" target="_blank" gdf-obfuscated-mailto="1oMZCNpxAQAJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">vlad...@ias.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The question is about how you interpret this operation for the univalent universe. If there is an interpretation of such an operation then there is a way to define equivalences between types in an involutionary way.<br><div><div></div></div></blockquote><div><br></div><div>I don’t follow why this should be the case. This shows that there is some notion of equivalence *in the model* (i.e. constructed in the meta-theory) which is strictly involutive. But there is no reason that this notion need be definable in the syntax of the object theory, is there?</div><div><br></div><div>–p. </div></div></div></div><div><br></div> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="javascript:" target="_blank" gdf-obfuscated-mailto="1oMZCNpxAQAJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">HomotopyTypeTheory+<wbr>unsubscribe@googlegroups.com</a>.<br> For more options, visit <a href="https://groups.google.com/d/optout" target="_blank" rel="nofollow" onmousedown="this.href='https://groups.google.com/d/optout';return true;" onclick="this.href='https://groups.google.com/d/optout';return true;">https://groups.google.com/d/<wbr>optout</a>.<br> </div></blockquote></div><br></div></div></div> <p></p> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="javascript:" target="_blank" gdf-obfuscated-mailto="1oMZCNpxAQAJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">HomotopyTypeTheory+<wbr>unsubscribe@googlegroups.com</a>.<br> For more options, visit <a href="https://groups.google.com/d/optout" target="_blank" rel="nofollow" onmousedown="this.href='https://groups.google.com/d/optout';return true;" onclick="this.href='https://groups.google.com/d/optout';return true;">https://groups.google.com/d/<wbr>optout</a>.<br> </blockquote></div> </blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/142000b0-e2e8-42cb-9201-4d2dcbec3de7%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/142000b0-e2e8-42cb-9201-4d2dcbec3de7%40googlegroups.com</a>.<br />