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

[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

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

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

[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

[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

[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

[Martin Escardo]

Nice, Dan and Anders and Thierry. Martin

[Jason Gross]

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

[Ian Orton]

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