* Weaker forms of univalence @ 2017-07-19 16:26 Ian Orton 2017-07-19 17:19 ` [HoTT] " Michael Shulman 2017-07-19 17:21 ` Jason Gross 0 siblings, 2 replies; 11+ messages in thread From: Ian Orton @ 2017-07-19 16:26 UTC (permalink / raw) To: HomotopyTypeTheory Consider the following three statements, for all types A and B: (1) (A ≃ B) -> (A = B) (2) (A ≃ B) ≃ (A = B) (3) isEquiv idtoeqv (3) is the full univalence axiom and we have implications (3) -> (2) -> (1), but can we say anything about the other directions? Do we have (1) -> (2) or (2) -> (3)? Can we construct models separating any/all of these three statements? Thanks, Ian ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: [HoTT] Weaker forms of univalence 2017-07-19 16:26 Weaker forms of univalence Ian Orton @ 2017-07-19 17:19 ` Michael Shulman 2017-07-19 18:04 ` Nicolai Kraus 2017-07-20 6:56 ` Bas Spitters 2017-07-19 17:21 ` Jason Gross 1 sibling, 2 replies; 11+ messages in thread From: Michael Shulman @ 2017-07-19 17:19 UTC (permalink / raw) To: Ian Orton; +Cc: HomotopyT...@googlegroups.com It was observed previously on this list, I think, that full univalence (3) is equivalent to (4) forall A, IsContr( Sigma(B:U) (A ≃ B) ). This follows from the fact that a fiberwise map is a fiberwise equivalence as soon as it induces an equivalence on total spaces, and the fact that based path spaces are contractible. But the contractibility of based path spaces also gives (2) -> (4), and hence (2) -> (3). I am not sure about (1). It might be an open question even in the case when A and B are propositions. On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk> wrote: > Consider the following three statements, for all types A and B: > > (1) (A ≃ B) -> (A = B) > (2) (A ≃ B) ≃ (A = B) > (3) isEquiv idtoeqv > > (3) is the full univalence axiom and we have implications (3) -> (2) -> (1), > but can we say anything about the other directions? Do we have (1) -> (2) or > (2) -> (3)? Can we construct models separating any/all of these three > statements? > > Thanks, > Ian > > -- > 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] 11+ messages in thread
* Re: [HoTT] Weaker forms of univalence 2017-07-19 17:19 ` [HoTT] " Michael Shulman @ 2017-07-19 18:04 ` Nicolai Kraus 2017-07-20 6:56 ` Bas Spitters 1 sibling, 0 replies; 11+ messages in thread From: Nicolai Kraus @ 2017-07-19 18:04 UTC (permalink / raw) To: HomotopyTypeTheory On 19/07/17 18:19, Michael Shulman wrote: > I am not sure about (1). It might be an open question even in the > case when A and B are propositions. If we restrict ourselves to the case that A and B are propositions, then (1) (A ≃ B) -> (A = B) is as strong as (2) / (3), since (1) then says that equality is implied by a reflexive propositional relation and thus a proposition. Of course this needs funext. (Afaik (1) is often called "propositional extensionality", but we could also just call it "univalence for propositions.) We have once discussed on this list whether (1) is consistent with UIP (i.e. it would be different from (2)), but we did not find an answer. Nicolai ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: [HoTT] Weaker forms of univalence 2017-07-19 17:19 ` [HoTT] " Michael Shulman 2017-07-19 18:04 ` Nicolai Kraus @ 2017-07-20 6:56 ` Bas Spitters 2017-07-20 11:59 ` Steve Awodey 1 sibling, 1 reply; 11+ messages in thread From: Bas Spitters @ 2017-07-20 6:56 UTC (permalink / raw) To: Michael Shulman; +Cc: Ian Orton, HomotopyT...@googlegroups.com >It was observed previously on this list, Maybe we should be using our wiki more? https://ncatlab.org/homotopytypetheory/ On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandiego.edu> wrote: > It was observed previously on this list, I think, that full univalence > (3) is equivalent to > > (4) forall A, IsContr( Sigma(B:U) (A ≃ B) ). > > This follows from the fact that a fiberwise map is a fiberwise > equivalence as soon as it induces an equivalence on total spaces, and > the fact that based path spaces are contractible. But the > contractibility of based path spaces also gives (2) -> (4), and hence > (2) -> (3). > > I am not sure about (1). It might be an open question even in the > case when A and B are propositions. > > > On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk> wrote: >> Consider the following three statements, for all types A and B: >> >> (1) (A ≃ B) -> (A = B) >> (2) (A ≃ B) ≃ (A = B) >> (3) isEquiv idtoeqv >> >> (3) is the full univalence axiom and we have implications (3) -> (2) -> (1), >> but can we say anything about the other directions? Do we have (1) -> (2) or >> (2) -> (3)? Can we construct models separating any/all of these three >> statements? >> >> Thanks, >> Ian >> >> -- >> 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. > > -- > 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] 11+ messages in thread
* Re: [HoTT] Weaker forms of univalence 2017-07-20 6:56 ` Bas Spitters @ 2017-07-20 11:59 ` Steve Awodey 2017-07-20 17:57 ` Michael Shulman 0 siblings, 1 reply; 11+ messages in thread From: Steve Awodey @ 2017-07-20 11:59 UTC (permalink / raw) To: Bas Spitters; +Cc: Michael Shulman, Ian Orton, HomotopyT...@googlegroups.com I think we’ve been through this before: (1) (A ≃ B) -> (A = B) is logically equivalent to what may be called “invariance”: if P(X) is any type depending on a type variable X, then given any equivalence e : A ≃ B , we have P(A) ≃ P(B). if we add to this a certain “computation rule”, we get something logically equivalent to UA: assume p : A ≃ B → A = B; then given e : A ≃ B, we have p(e) : A = B is a path in U. Since we can transport along this path in any family of types over U, and transport is always an equivalence, there is a transport p(e)∗ : A ≃ B in the identity family. The required “computation rule” states that p(e)∗ = e. Steve > On Jul 20, 2017, at 8:56 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote: > >> It was observed previously on this list, > Maybe we should be using our wiki more? > https://ncatlab.org/homotopytypetheory/ > > > On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandiego.edu> wrote: >> It was observed previously on this list, I think, that full univalence >> (3) is equivalent to >> >> (4) forall A, IsContr( Sigma(B:U) (A ≃ B) ). >> >> This follows from the fact that a fiberwise map is a fiberwise >> equivalence as soon as it induces an equivalence on total spaces, and >> the fact that based path spaces are contractible. But the >> contractibility of based path spaces also gives (2) -> (4), and hence >> (2) -> (3). >> >> I am not sure about (1). It might be an open question even in the >> case when A and B are propositions. >> >> >> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk> wrote: >>> Consider the following three statements, for all types A and B: >>> >>> (1) (A ≃ B) -> (A = B) >>> (2) (A ≃ B) ≃ (A = B) >>> (3) isEquiv idtoeqv >>> >>> (3) is the full univalence axiom and we have implications (3) -> (2) -> (1), >>> but can we say anything about the other directions? Do we have (1) -> (2) or >>> (2) -> (3)? Can we construct models separating any/all of these three >>> statements? >>> >>> Thanks, >>> Ian >>> >>> -- >>> 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. >> >> -- >> 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. > > -- > 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] 11+ messages in thread
* Re: [HoTT] Weaker forms of univalence 2017-07-20 11:59 ` Steve Awodey @ 2017-07-20 17:57 ` Michael Shulman 2017-07-21 1:36 ` Matt Oliveri 0 siblings, 1 reply; 11+ messages in thread From: Michael Shulman @ 2017-07-20 17:57 UTC (permalink / raw) To: Steve Awodey; +Cc: Bas Spitters, Ian Orton, HomotopyT...@googlegroups.com But is it known that this is definitely weaker? E.g. are there models that satisfy invariance but not the computation rule? On Thu, Jul 20, 2017 at 4:59 AM, Steve Awodey <awo...@cmu.edu> wrote: > I think we’ve been through this before: > > (1) (A ≃ B) -> (A = B) > > is logically equivalent to what may be called “invariance”: > > if P(X) is any type depending on a type variable X, then given any equivalence e : A ≃ B , we have P(A) ≃ P(B). > > if we add to this a certain “computation rule”, we get something logically equivalent to UA: > assume p : A ≃ B → A = B; then given e : A ≃ B, we have p(e) : A = B is a path in U. > Since we can transport along this path in any family of types over U, and transport is always an equivalence, > there is a transport p(e)∗ : A ≃ B in the identity family. > The required “computation rule” states that p(e)∗ = e. > > Steve > > > >> On Jul 20, 2017, at 8:56 AM, Bas Spitters <b.a.w.s...@gmail.com> wrote: >> >>> It was observed previously on this list, >> Maybe we should be using our wiki more? >> https://ncatlab.org/homotopytypetheory/ >> >> >> On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandiego.edu> wrote: >>> It was observed previously on this list, I think, that full univalence >>> (3) is equivalent to >>> >>> (4) forall A, IsContr( Sigma(B:U) (A ≃ B) ). >>> >>> This follows from the fact that a fiberwise map is a fiberwise >>> equivalence as soon as it induces an equivalence on total spaces, and >>> the fact that based path spaces are contractible. But the >>> contractibility of based path spaces also gives (2) -> (4), and hence >>> (2) -> (3). >>> >>> I am not sure about (1). It might be an open question even in the >>> case when A and B are propositions. >>> >>> >>> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk> wrote: >>>> Consider the following three statements, for all types A and B: >>>> >>>> (1) (A ≃ B) -> (A = B) >>>> (2) (A ≃ B) ≃ (A = B) >>>> (3) isEquiv idtoeqv >>>> >>>> (3) is the full univalence axiom and we have implications (3) -> (2) -> (1), >>>> but can we say anything about the other directions? Do we have (1) -> (2) or >>>> (2) -> (3)? Can we construct models separating any/all of these three >>>> statements? >>>> >>>> Thanks, >>>> Ian >>>> >>>> -- >>>> 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. >>> >>> -- >>> 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. >> >> -- >> 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. > > -- > 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] 11+ messages in thread
* Re: [HoTT] Weaker forms of univalence 2017-07-20 17:57 ` Michael Shulman @ 2017-07-21 1:36 ` Matt Oliveri 2017-07-21 7:43 ` Peter LeFanu Lumsdaine 0 siblings, 1 reply; 11+ messages in thread From: Matt Oliveri @ 2017-07-21 1:36 UTC (permalink / raw) To: Homotopy Type Theory; +Cc: awo..., b.a.w.s..., ri... [-- Attachment #1.1: Type: text/plain, Size: 2778 bytes --] Why wouldn't a skeletal LCCC be a model of (1) + UIP? On Thursday, July 20, 2017 at 1:57:37 PM UTC-4, Michael Shulman wrote: > > But is it known that this is definitely weaker? E.g. are there models > that satisfy invariance but not the computation rule? > > On Thu, Jul 20, 2017 at 4:59 AM, Steve Awodey <awo...@cmu.edu > <javascript:>> wrote: > > I think we’ve been through this before: > > > > (1) (A ≃ B) -> (A = B) > > > > is logically equivalent to what may be called “invariance”: > > > > if P(X) is any type depending on a type variable X, then given > any equivalence e : A ≃ B , we have P(A) ≃ P(B). > > > > if we add to this a certain “computation rule”, we get something > logically equivalent to UA: > > assume p : A ≃ B → A = B; then given e : A ≃ B, we have p(e) : A = B is > a path in U. > > Since we can transport along this path in any family of types over U, > and transport is always an equivalence, > > there is a transport p(e)∗ : A ≃ B in the identity family. > > The required “computation rule” states that p(e)∗ = e. > > > > Steve > > > > > > > >> On Jul 20, 2017, at 8:56 AM, Bas Spitters <b.a.w...@gmail.com > <javascript:>> wrote: > >> > >>> It was observed previously on this list, > >> Maybe we should be using our wiki more? > >> https://ncatlab.org/homotopytypetheory/ > >> > >> > >> On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandiego.edu > <javascript:>> wrote: > >>> It was observed previously on this list, I think, that full univalence > >>> (3) is equivalent to > >>> > >>> (4) forall A, IsContr( Sigma(B:U) (A ≃ B) ). > >>> > >>> This follows from the fact that a fiberwise map is a fiberwise > >>> equivalence as soon as it induces an equivalence on total spaces, and > >>> the fact that based path spaces are contractible. But the > >>> contractibility of based path spaces also gives (2) -> (4), and hence > >>> (2) -> (3). > >>> > >>> I am not sure about (1). It might be an open question even in the > >>> case when A and B are propositions. > >>> > >>> > >>> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk > <javascript:>> wrote: > >>>> Consider the following three statements, for all types A and B: > >>>> > >>>> (1) (A ≃ B) -> (A = B) > >>>> (2) (A ≃ B) ≃ (A = B) > >>>> (3) isEquiv idtoeqv > >>>> > >>>> (3) is the full univalence axiom and we have implications (3) -> (2) > -> (1), > >>>> but can we say anything about the other directions? Do we have (1) -> > (2) or > >>>> (2) -> (3)? Can we construct models separating any/all of these three > >>>> statements? > >>>> > >>>> Thanks, > >>>> Ian > [-- Attachment #1.2: Type: text/html, Size: 4675 bytes --] ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: [HoTT] Weaker forms of univalence 2017-07-21 1:36 ` Matt Oliveri @ 2017-07-21 7:43 ` Peter LeFanu Lumsdaine 0 siblings, 0 replies; 11+ messages in thread From: Peter LeFanu Lumsdaine @ 2017-07-21 7:43 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory, Steve Awodey, Bas Spitters, Ian Orton [-- Attachment #1: Type: text/plain, Size: 3680 bytes --] On Fri, Jul 21, 2017 at 2:36 AM, Matt Oliveri <atm...@gmail.com> wrote: > Why wouldn't a skeletal LCCC be a model of (1) + UIP? > Because (1) would require not just the category itself to be skeletal, but also its slices, if “(A ≃ B) -> (A = B)” is taken as a global axiom scheme, and unlike for skeletality of the category itself, one cannot generally replace a category by an equivalent one with suitably skeletal slices. (If it’s taken as a quantified axiom “forall A,B:U, (A ≃ B) -> (A = B)”, as it more usually is, then its validity doesn’t follow directly from any amount of skeletality at all, but is to do with the specific universe chosen.) –p. > > On Thursday, July 20, 2017 at 1:57:37 PM UTC-4, Michael Shulman wrote: >> >> But is it known that this is definitely weaker? E.g. are there models >> that satisfy invariance but not the computation rule? >> >> On Thu, Jul 20, 2017 at 4:59 AM, Steve Awodey <awo...@cmu.edu> wrote: >> > I think we’ve been through this before: >> > >> > (1) (A ≃ B) -> (A = B) >> > >> > is logically equivalent to what may be called “invariance”: >> > >> > if P(X) is any type depending on a type variable X, then given >> any equivalence e : A ≃ B , we have P(A) ≃ P(B). >> > >> > if we add to this a certain “computation rule”, we get something >> logically equivalent to UA: >> > assume p : A ≃ B → A = B; then given e : A ≃ B, we have p(e) : A = B is >> a path in U. >> > Since we can transport along this path in any family of types over U, >> and transport is always an equivalence, >> > there is a transport p(e)∗ : A ≃ B in the identity family. >> > The required “computation rule” states that p(e)∗ = e. >> > >> > Steve >> > >> > >> > >> >> On Jul 20, 2017, at 8:56 AM, Bas Spitters <b.a.w...@gmail.com> >> wrote: >> >> >> >>> It was observed previously on this list, >> >> Maybe we should be using our wiki more? >> >> https://ncatlab.org/homotopytypetheory/ >> >> >> >> >> >> On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandiego.edu> >> wrote: >> >>> It was observed previously on this list, I think, that full >> univalence >> >>> (3) is equivalent to >> >>> >> >>> (4) forall A, IsContr( Sigma(B:U) (A ≃ B) ). >> >>> >> >>> This follows from the fact that a fiberwise map is a fiberwise >> >>> equivalence as soon as it induces an equivalence on total spaces, and >> >>> the fact that based path spaces are contractible. But the >> >>> contractibility of based path spaces also gives (2) -> (4), and hence >> >>> (2) -> (3). >> >>> >> >>> I am not sure about (1). It might be an open question even in the >> >>> case when A and B are propositions. >> >>> >> >>> >> >>> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.uk> wrote: >> >>>> Consider the following three statements, for all types A and B: >> >>>> >> >>>> (1) (A ≃ B) -> (A = B) >> >>>> (2) (A ≃ B) ≃ (A = B) >> >>>> (3) isEquiv idtoeqv >> >>>> >> >>>> (3) is the full univalence axiom and we have implications (3) -> (2) >> -> (1), >> >>>> but can we say anything about the other directions? Do we have (1) >> -> (2) or >> >>>> (2) -> (3)? Can we construct models separating any/all of these >> three >> >>>> statements? >> >>>> >> >>>> Thanks, >> >>>> Ian >> > -- > 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. > [-- Attachment #2: Type: text/html, Size: 5917 bytes --] ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: [HoTT] Weaker forms of univalence 2017-07-19 16:26 Weaker forms of univalence Ian Orton 2017-07-19 17:19 ` [HoTT] " Michael Shulman @ 2017-07-19 17:21 ` Jason Gross 2017-07-19 17:28 ` Michael Shulman 1 sibling, 1 reply; 11+ messages in thread From: Jason Gross @ 2017-07-19 17:21 UTC (permalink / raw) To: Ian Orton, HomotopyT... [-- Attachment #1: Type: text/plain, Size: 1133 bytes --] Certainly (2) => (3), at least if you assume function extensionality; it suffices to show that (\Sigma B, A ≃ B) is contractable, and since contractibility and sigma respect equivalence, we can transfer the proof that (\Sigma B, A = B) is contractable. I think the same is not true of (1), though I'm not sure. On Wed, Jul 19, 2017, 7:26 PM Ian Orton <ri...@cam.ac.uk> wrote: > Consider the following three statements, for all types A and B: > > (1) (A ≃ B) -> (A = B) > (2) (A ≃ B) ≃ (A = B) > (3) isEquiv idtoeqv > > (3) is the full univalence axiom and we have implications (3) -> (2) -> > (1), but can we say anything about the other directions? Do we have (1) > -> (2) or (2) -> (3)? Can we construct models separating any/all of > these three statements? > > Thanks, > Ian > > -- > 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. > [-- Attachment #2: Type: text/html, Size: 1605 bytes --] ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: [HoTT] Weaker forms of univalence 2017-07-19 17:21 ` Jason Gross @ 2017-07-19 17:28 ` Michael Shulman 2017-07-19 18:02 ` Jason Gross 0 siblings, 1 reply; 11+ messages in thread From: Michael Shulman @ 2017-07-19 17:28 UTC (permalink / raw) To: Jason Gross; +Cc: Ian Orton, HomotopyT...@googlegroups.com I don't think you need function extensionality for contractibility and Sigma to respect equivalence. We need funext for Pi to respect equivalence, but there are no Pis here. On Wed, Jul 19, 2017 at 10:21 AM, Jason Gross <jason...@gmail.com> wrote: > Certainly (2) => (3), at least if you assume function extensionality; it > suffices to show that (\Sigma B, A ≃ B) is contractable, and since > contractibility and sigma respect equivalence, we can transfer the proof > that (\Sigma B, A = B) is contractable. I think the same is not true of (1), > though I'm not sure. > > On Wed, Jul 19, 2017, 7:26 PM Ian Orton <ri...@cam.ac.uk> wrote: >> >> Consider the following three statements, for all types A and B: >> >> (1) (A ≃ B) -> (A = B) >> (2) (A ≃ B) ≃ (A = B) >> (3) isEquiv idtoeqv >> >> (3) is the full univalence axiom and we have implications (3) -> (2) -> >> (1), but can we say anything about the other directions? Do we have (1) >> -> (2) or (2) -> (3)? Can we construct models separating any/all of >> these three statements? >> >> Thanks, >> Ian >> >> -- >> 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. > > -- > 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] 11+ messages in thread
* Re: [HoTT] Weaker forms of univalence 2017-07-19 17:28 ` Michael Shulman @ 2017-07-19 18:02 ` Jason Gross 0 siblings, 0 replies; 11+ messages in thread From: Jason Gross @ 2017-07-19 18:02 UTC (permalink / raw) To: Michael Shulman; +Cc: Ian Orton, HomotopyT...@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 2502 bytes --] > I am not sure about (1). It might be an open > question even in the > case when A and B are propositions. If A and B are hProps, then (1) => (3) under function extensionality (not sure if you can do away with out here). The key idea is that there can be only one equivalence between hProps. To prove contractibility, we must show that (A, idequiv) = (B, e) for any equivalence e of A and B. Let us prove A = B by (1); what remains is proving that idequiv = transport (1) e. It now suffices to show that A ≃ A is an hProp for A an hProp. This follows from function extensionality. On Wed, Jul 19, 2017, 8:28 PM Michael Shulman <shu...@sandiego.edu> wrote: > I don't think you need function extensionality for contractibility and > Sigma to respect equivalence. We need funext for Pi to respect > equivalence, but there are no Pis here. > > On Wed, Jul 19, 2017 at 10:21 AM, Jason Gross <jason...@gmail.com> > wrote: > > Certainly (2) => (3), at least if you assume function extensionality; it > > suffices to show that (\Sigma B, A ≃ B) is contractable, and since > > contractibility and sigma respect equivalence, we can transfer the proof > > that (\Sigma B, A = B) is contractable. I think the same is not true of > (1), > > though I'm not sure. > > > > On Wed, Jul 19, 2017, 7:26 PM Ian Orton <ri...@cam.ac.uk> wrote: > >> > >> Consider the following three statements, for all types A and B: > >> > >> (1) (A ≃ B) -> (A = B) > >> (2) (A ≃ B) ≃ (A = B) > >> (3) isEquiv idtoeqv > >> > >> (3) is the full univalence axiom and we have implications (3) -> (2) -> > >> (1), but can we say anything about the other directions? Do we have (1) > >> -> (2) or (2) -> (3)? Can we construct models separating any/all of > >> these three statements? > >> > >> Thanks, > >> Ian > >> > >> -- > >> 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. > > > > -- > > 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. > [-- Attachment #2: Type: text/html, Size: 3490 bytes --] ^ permalink raw reply [flat|nested] 11+ messages in thread
end of thread, other threads:[~2017-07-21 7:43 UTC | newest] Thread overview: 11+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-07-19 16:26 Weaker forms of univalence Ian Orton 2017-07-19 17:19 ` [HoTT] " Michael Shulman 2017-07-19 18:04 ` Nicolai Kraus 2017-07-20 6:56 ` Bas Spitters 2017-07-20 11:59 ` Steve Awodey 2017-07-20 17:57 ` Michael Shulman 2017-07-21 1:36 ` Matt Oliveri 2017-07-21 7:43 ` Peter LeFanu Lumsdaine 2017-07-19 17:21 ` Jason Gross 2017-07-19 17:28 ` Michael Shulman 2017-07-19 18:02 ` Jason Gross
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).