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

[Ian Orton <ri...@cam.ac.uk>]

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