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

[Jason Gross <jason...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 5183 bytes --]

To belatedly add a little bit to this discussion:

> so maybe other people have already realized this, but it was surprising
to me

A way that I've found to make this seem more obvious is that too use the
encode-decode method, you provide a proof of "forall x, Contr { y : A &
code x y }" (using Coq notation for sigma types).  With a bit of
rearranging, giving your ua and uaβ is the same as giving the data for
"forall A (p q : { B : Type & A <~> B }), p = q", i.e., giving the hProp
obligation for contractibility.  There's some Coq code that implements this
that I put here:
https://github.com/HoTT/HoTT/issues/757#issuecomment-102128029, and in the
following discussion, Mike and Vladimir and Steve pointed out that this had
been seen before.

-Jason

On Thu, Sep 15, 2016 at 3:39 PM 'Martin Escardo' via Homotopy Type Theory <
HomotopyT...@googlegroups.com> wrote:

> 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.
> >
>
> --
> 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: 8961 bytes --]