On Fri, Jul 21, 2017 at 2:36 AM, Matt Oliveri 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 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 >> 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 >> 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 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. >