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