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 HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.