weak univalence with "beta" implies full univalence

weak univalence with "beta" implies full univalence

[Dan Licata]

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

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

[Andrew Pitts]

On 7 September 2016 at 16:10, Dan Licata <d...@cs.cmu.edu> wrote:
> 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.

Very spooky: I recently noticed this for myself (though not via the
observation you mention) and was just about to ask this list whether
it was "well known".

> 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.

You are stating this for the usual inductively defined Martin-Lof
identity type ==, right?  Actually I believe it holds with respect to
any notion of propositional identity type (by which I mean any model
of the Coquand-Danielsson axioms), such as the path types that occur
in the CCHM model. Also I think you need to assume the identity types,
whatever they are, satisfy function extensionality don't you?

> Unless the absence of definitional beta reduction for J somehow gets in the way,

I don't think it does get 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.

Yes indeed. This certainly seems a pleasantly minimal condition to
have to check for univalence and, as you say, applies to the model of
Cohen,Coquand,Huber & Mortberg [CCHM]. (Ian Orton and I are trying to
apply it to a different model we are developing.)

Andy

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

[Dan Licata]

Hi Andy,

Thanks for the interesting comments!  A few replies below.  

>> 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.
> 
> You are stating this for the usual inductively defined Martin-Lof
> identity type ==, right?  

Yes. 

> Also I think you need to assume the identity types,
> whatever they are, satisfy function extensionality don't you?

I didn’t, but I stated uaβ as an equation at function type.  If it were pointwise, then I would have needed it.  For an identity type with definitional J-on-refl reduction, this suffices to get the usual statement of univalence (I updated the file a little to remove a use a funext to make sure).  Maybe this depends on having definitional J-on-refl though.  

-Dan

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

[Andrew Pitts]

On 7 September 2016 at 23:20, Dan Licata <d...@cs.cmu.edu> wrote:
>> Also I think you need to assume the identity types,
>> whatever they are, satisfy function extensionality don't you?
>
> I didn’t, but I stated uaβ as an equation at function type.  If it were pointwise, then I would have needed it.  For an identity type with definitional J-on-refl reduction, this suffices to get the usual statement of univalence (I updated the file a little to remove a use a funext to make sure).  Maybe this depends on having definitional J-on-refl though.

OK, I see. The proof I made up for myself used along the way the fact
that being contractible is a mere proposition; and for that I seemed
to need function extensionality. But in any case, stating uaβ
pointwise seems more useful. Plus the fact that in the models where we
have been using this nice characterisation of univalence, function
extensionality holds for the propositional identity types in question
for other reasons to do with them being given by paths, as you know.

Best wishes,

Andy

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

[Michael Shulman]

I feel like we sort of knew this, but I'm not sure it was written down
exactly.  Essentially the same argument did come up a couple of years
ago in discussing higher inductive-recursive universes:
https://homotopytypetheory.org/2014/06/08/hiru-tdd/

On Wed, Sep 7, 2016 at 8: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.

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

[Anders]

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.

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

[Martin Escardo]

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.
>

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

[Jason Gross]

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

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

[Ian Orton]

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

Hi all,

I wanted to follow up on Dan's previous observations by suggesting a 
different set of axioms which imply those in his email (and hence imply 
univalence). I think these are interesting because they're potentially 
easier to check in a model - I'll argue that this is the case for 
cubical sets/cubical type theory. I've personally found this 
decomposition of univalence particularly useful for understanding what's 
going on in the cubical sets model.

Firstly, assume funext*. Next, assume two special cases of ua (as 
defined in Dan's email), where A B : Set and C : A → B → Set,

    unit : A = (Σ[ a ∈ A ] ⊤)
    flip  : (Σ[ a ∈ A ] Σ[ b ∈ B ] C a b) = (Σ[ b ∈ B ] Σ[ a ∈ A ] C a b)

Finally, assume the following:

    contract : isContr A → A = ⊤

Recall that singletons, sing(x) := Σ[ y ∈ A ] x = y, are contractible 
and a function f : A --> B is an equivalence if, for every b : B, the 
fiber, fib_f(b) := Σ[ a ∈ A ] (f a = b), is contractible.

Now, given an equivalence (f,e) : isEquiv A B, the following calculation 
shows how to construct an equality ua(f,e) : A = B

    A = Σ[ a ∈ A ] ⊤   -- by unit
        = Σ[ a ∈ A ] Σ[ b ∈ B ] (f a = b)   -- by contract on sing(f a)
        = Σ[ b ∈ B ] Σ[ a ∈ A ] (f a = b)   -- by flip
        = Σ[ b ∈ B ] ⊤   -- by contract on fib_f(b)
        = B   -- by unit

Showing uaβ requires the following assumptions (which are in fact 
special cases of uaβ):

    unitβ : (A : Set) → transport (λ X → X) (unit A) = λ a → (a , tt)
    flipβ  : {A B : Set}{C : A → B → Set} →
        transport (λ X → X) flip = λ{(a , b , c) → (b , a , c)}

So given funext + these 5 assumptions we get univalence.

All of this has been formalised in Agda, and can be found at 
http://www.cl.cam.ac.uk/~rio22/agda/axi-univ/UnivArg.html

To understand why this is interesting, consider the cubical sets model. 
Funext is easily validated in cubical sets. The axioms unit and flip 
arise as special cases of a more general construction: types in cubical 
TT are interpreted as presheaves. Given two types Γ ⊢ A B which are 
interpreted as isomorphic presheaves (note that this condition is 
stronger than being equivalent types in the type theory) then define a 
presheaf P(x,i) := A(x) if i =0 or B(x) otherwise. This gives a new type 
Γ, i : I ⊢ P which is A when i=0 and B when i=1. This then gives us a 
path in the universe from A to B.

To validate contract you need to, given a contractible type Γ ⊢ A, 
define a new type Γ, i : I ⊢ C which is A when i=0 and ⊤ when i=1. 
Define C to be the partial elements of A with extent i=0.
When i=0 this is isomorphic to A and when i=1 this is isomorphic to ⊤. 
We strengthen the isomorphisms at each end to equalities using the 
construction in the previous paragraph.

Everything described here is happening in the Glueing construction 
currently used to show univalence.

Cheers,
Ian

* You can make do with weaker assumptions, but things are simpler with 
funext, and it doesn't seem to cause problems for the purpose of finding 
axioms which are easy to check in models. It's very easy to validate 
funext in cubical TT/sets and others models I've been looking at with my 
supervisor (Andy Pitts).

On 07/09/2016 16:10, Dan Licata 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 observationhttps://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
>


[-- Attachment #2: Type: text/html, Size: 6706 bytes --]