Re: [HoTT] Weaker forms of univalence

[Matt Oliveri <atm...@gmail.com>]

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