Re: [HoTT] Weaker forms of univalence

[Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>]

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