Re: [HoTT] weak univalence with "beta" implies full univalence

[Martin Escardo <escardo...@googlemail.com>]

Nice, Dan and Anders and Thierry. Martin

On 15/09/16 18:35, Anders wrote:
> Hi,
>
> I've formalized this in cubicaltt now, a self-contained formalization
> can be found here:
>
> https://github.com/mortberg/cubicaltt/blob/master/experiments/univalence_dan.ctt#L123
>
> The proof is a little different from Dan's and follows a sketch that I
> got from Thierry:
>
> We have that
>
>  ua + uabeta
>
> implies that Equiv A B is a retract of Path U A B. Hence
>
>  (X:U) x Equiv A X    is a retract of    (X:U) x Path U A X
>
> But (X:U) x Path U A X is contractible (contractibility of
> singletons). So (X:U) x Equiv A X is contractible as it is a
> retraction of a contractible type. This is an alternative formulation
> of the univalence axiom as noted by Martín:
>
> https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ
>
>
> One difference with Dan's proof is that this is not using the "grad
> lemma" (if f has a quasi-inverse then it is an equivalence (called
> "improve" in Dan's code)). It also shows that not having the
> computation rule for J definitionally doesn't get in the way, however
> having it would have made the proof of uabeta trivial (I now have to
> do some work by hand as two transports don't disappear).
>
> --
> Anders
>
> On Wed, Sep 7, 2016 at 11:10 AM, Dan Licata <d...@cs.cmu.edu> wrote:
>> Hi,
>>
>> What I’m about to say is a trivial consequence of an observation that Egbert/Martin made a couple of years ago (https://github.com/HoTT/book/issues/718), so maybe other people have already realized this, but it was surprising to me.
>>
>> In particular, based on Martin’s observation https://github.com/HoTT/book/issues/718#issuecomment-65378867
>> that any retraction of an identity type is an equivalence:
>>
>>    retract-of-Id-is-Id : ∀ {A : Set} {R : A → A → Set} →
>>                        (r : {x y : A} → x == y -> R x y)
>>                        (s : {x y : A} → R x y → x == y)
>>                        (comp1 : {x y : A} (c : R x y) → r (s c) == c)
>>                        → {x y : A} → IsEquiv {x == y} {R x y} (r {x}{y})
>>
>> it is enough to assert “ua” (equivalence to path) and the “beta” direction of the full univalence axiom, i.e. the fact that transporting along such a path is the equivalence:
>>
>>    ua : ∀ {A B} → Equiv A B → A == B
>>    uaβ : ∀ {A B} (e : Equiv A B) → transport (\ X -> X) (ua e) == fst e
>>
>> The “eta” direction comes for free by Martin’s argument.
>>
>> Here is a self-contained Agda file that checks this:
>> https://github.com/dlicata335/hott-agda/blob/master/misc/UABetaOnly-SelfContained.agda
>> (Almost all of the file is boilerplate, but I wanted to make sure I wasn’t accidentally using anything from my library that relies on univalence.)
>>
>> Unless the absence of definitional beta reduction for J somehow gets in the way, I think this gives another arugment why the Glue type in the Cohen,Coquand,Huber,Mortberg cubical type theory gives full univalence: the only thing specifc to cubical type theory that you need to check is that ua and uaβ can be derived from Glue, and the rest of the argument can happen in book HoTT.  This is a small simplification/rearrangement of the argument in Appendix B of their paper, essentially saying that condition (3) of Lemma 25 can be replaced by the retraction lemma.
>>
>> -Dan
>>
>> --
>> 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.
>