Unifying Cubical Models of Univalent Type Theory

Introduction

A general axiomatisation

Locally cartesian closed categories C P ∨ Q ≡ ||P + Q||, ¬A ≡ A → 0.

The interval and Path types

I : U, 0, 1 : I. (I to be connected) ax₁ : Π_{P : I → U} (Π_{i : I} P(i) + ¬(P(i))) → ((Π_{i : I} P(i)) + (Π_{P : I} ¬(P(i)))), (0, 1 to be distinct) ax₂ : ¬(0 = 1).

(Type of paths in A) A : I → U ⊢ Path(A) ≡ Π_{i : I} → A(i). a : A(0), b : A(1) ⊢ a ∼ b ≡ Σ_{p : Path(A)} (p(0) = a) × (p(1) = b). p : a ∼ b, r : I ⊢ p @ r ≡ app of fst(p) to r, p @ 0 = a, p @ 1 = b.

Cofibrant propositions

cofibrant propositions Φ : U ⊢ (decoding function) [_] : Φ → hProp, (_ ≈ 0) : I → Φ ax₃ : Π_{i : I} [_ ≈ 0] = (i = 0), (_ ≈ 1) : I → Φ ax₄ : Π_{i : I} [_ ≈ 1] = (i = 1), ∨ : Φ → Φ → Φ ax₅ : Π_{φ, ψ : Φ} [φ ∨ ψ] = [φ] ∨ [ψ]. (bottom elements) (0 ≈ 1), (1 ≈ 0), (top elements) (0 ≈ 0), (1 ≈ 1). A : U ⊢ elim₀ : [0 ≈ 1] → A (by ax₂).

Remark 1

(partial element) f : [φ] → A. (extension) f : [φ] → A, x : A ⊢ f ↗ x ≡ Π_{u : [φ]} f(u) = x. f ↗ x is the type of proofs that the partial element f extends to the total element x. (type of all elements of A extending f) A[φ ↦ f] ≡ Σ_{x : A} f ↗ x. f : [φ] → Path(A), r : I ⊢ f · r ≡ u ↦ f(u)(r) : [φ] → A(r).

Fibration structures

Weak composition

r : I, A : I → U, φ : Φ, f : [φ] → Path(A), x₀ : A(r)[φ ↦ f · i] ⊢ wcom : Π_{s : I} A(s)[φ ↦ f · s],wcom : fst(wcom(r)) ∼ fst(x₀), Π_{i : I} f · r ↗ wcom @ i. WComp(r, A, φ, f, x₀) ≡ Σ_{wcom : ...} Σ_{wcom : ...} Π_{i : I} f · r ↗ wcom @ i.

Weak fibrations and fibration structures

A weak fibration (A, α) over Γ : U is a family A : Γ → U equipped with a fibration structure α : isFib(A), where isFib(A) ≡ (r : I)(p : I )(φ : Φ)(f : [φ] → (i : I) → A(p(i)))(x₀ : A(p(r))[φ ↦ f · r]) → WComp(r, (A ◦ p), φ, f, x₀). (type of weak fibrations over Γ) Fib(Γ) ≡ Σ_{A : Γ → U} isFib(A). We obtain a category with families (CwF) [21] where the families over Γ : U are (A, α) : Fib(Γ) and elements of such a family are dependent functions in (x : Γ) → A x. (reindexing of P along σ) P : Fib(Γ), σ : ∆ → Γ ⊢ P[σ] : Fib(∆).

Remark 5

α : isFib(A), s : I, r, p, φ, f, x₀ ⊢ wcom_α^{r → s} p[φ ↦ f] x₀ ≡ fst(fst(α r p φ f x₀) s) : A(p(s)),wcom_α^r p[φ ↦ f] x₀ ≡ fst(snd(α r p φ f x₀)) : wcom_α^{r → r} p[φ ↦ f] x₀ ∼ fst(x₀). φ, ψ : Φ ⊢ [φ ↦ f, ψ ↦ g] : [ φ ∨ ψ ] → A for the union of partial elements f : [φ] → A and g : [ψ] → A that agree where they are both defined, i.e. such that ∀(u : [φ]) (v : [ψ]) ↦ f(u) = g(v). This generalises to [φ1 ↦ f1, ..., φn ↦ fn]. (cofibrant) isCofProp(A : hProp) ≡ Σ_{φ : Φ} A ↔ [φ]. When r, s : I are such that (r = s) is cofibrant, we will be able to 'improve' weak composition r → s to obtain a strict composition that is exactly equal to its cap when r = s.

Strict composition

r : I, A : I → U, φ : Φ, f : [φ] → Path(A), x0 : A(r)[φ ↦ f · i] ⊢ scom : Π_{s : I} isCofProp(r = s) → A(s)[φ ↦ f · s], Π_{c : isCofProp(r = r)} fst(scom r c) = fst(x0).

Strict fibrations

A strict fibration (A, α) over Γ : U is a family A : Γ → U equipped with a strict fibration structure α : isSFib A, where isSFib(A) ≡ (r : I)(p : I → Γ)(φ : Φ)(f : [φ] → (i : I) → A(p(i)))(x0 : A(p(r))[φ ↦ f · r]) → SComp(r, (A ◦ p), φ, f, x0).

Strictification

Γ : U, A : Γ → U ⊢ α : isFib(A), r, p, φ, f, x0 ⊢ w ≡ wcom_α^{r → s} p[φ ↦ f] x₀,w ≡ wcom_α^r p[φ ↦ f] x₀, s : I ⊢ scom(s) ≡ wcom_α^{0 → 1} (_ ↦ p(s))[φ ↦ (u, _) ↦ f u s, (r = s) ↦ (_, i) ↦ w @ i] w, scom : isFib(A) → isSFib(A). As (r = ε) and (ε = r) are always cofibrant for ε = 0, 1, we have strict composition operations ε → r and r → ε in any fibration. Defining 0 ≡ 1 and 1 ≡ 0, we note that the weak compositions ε → ε are already strict, as the cap condition is vacuous.

AFH fibrations

(diagonal cofibrations) (_ ≈ _) : I → I → Φ, ax_Δ : Π_{r, s : I} [r ≈ s] = (r = s).

AFH composition

r : I, A : I → U, φ : Φ, f : [φ] → Path(A), x0 : A(r)[φ ↦ f · i] ⊢ com : Π_{s : I} A(s)[φ ↦ f · s], fst(com(r)) = fst(x0). AFHComp(r, A, φ, f, x0) ≡ ..., isAFHFib(A) ≡ (r : I)(p : I → Γ)(φ : Φ)(f : [φ] → (i : I) → A(p(i))) (x0 : A(p(r))[φ ↦ f · r]) → AFHComp(r, (A ◦ p), φ, f, x0).

Theorem 10

Γ : U, A : Γ → U ⊢ we have isAFHFib(A) iff we have isFib(A).

Remark 11

CCHM fibrations

⊓, ⊔ : I → I → I (from connection algebra), ax_⊓ : Π_{r : I} (0 ⊓ r = 0 = r ⊓ 0) ∧ (1 ⊓ r = r = r ⊓ 1), ax_⊔ : Π_{r : I} (0 ⊔ r = r = r ⊔ 0) ∧ (1 ⊔ r = 1 = r ⊔ 1).

Remark 12

CCHM composition

ε : 1, A : I → U, φ : Φ, f : [φ] → Path(A), x0 : A(ε)[φ ↦ f · i] ⊢ com : A(ε)[φ ↦ f · ε], CCHMComp(ε A φ f x0) ≡ ..., isCCHMFib(A) ≡ (ε : 1)(p : I → Γ)(φ : Φ)(f : [φ] → (i : I) → A(p(i))) (x0 : A(p(ε))[φ ↦ f · r]) → CCHMComp(ε (A ◦ p) φ f x0).

Theorem 14

Fibration structures for basic type formers

Fibrant Σ-types

Glueing

φ : Φ, A : [φ] → U, B : U, f : Π_{x : [φ]} A(x) → B ⊢ Glue(φ, A, B, f) ≡ Σ_{a : Πx : [φ] A(x)} Σ_{b : B} Π_{x : [φ]} f(x)(a(x)) = b.

Fibrant Glue types

Γ : U, φ : Γ → Φ, A : (x : Γ) → [φ(x)] → U, B : Γ → U, f : (x : Γ)(v : [φ(x)]) → A x v → B(x). If f has the structure of an equivalence then there is a function isFib_Glue : isFib(A) → isFib(B) → isFib(Glue(φ, A, B, f)).

Univalence

Γ : U, A, B : Fib(Γ) ⊢ A ∼_U B ≡ Σ_{P : Fib(Γ × I)} P[(id, 0)] = A × P[(id, 1)] = B.

Univalence for ∼_U

(A ∼_U B) ≃ (fst(A) ≃ fst(B)).

Fibrant univalent universes

Crisp type theory. tiny = exponentiation by it has a right adjoint.

Universe construction

Model structures on cubical sets

δ_i : 1 → I for i : 1 for the endpoint inclusions. We use the subscript B when working with objects in a slice category C/B. In particular, we have an interval object I_B defined as the projection I × B → B, with endpoint maps δ_Bi :1_B →I_B.

Cofibrantly generated algebraic weak factorisation systems (AWFSs)

Cofibration and trivial fibration awfs

[−] : Φ → hProp as a monomorphism ⊤ : Φ_true ↣ Φ, where Φ_true ≡ Σ_{φ : Φ} [φ] = ⊤.

Generating cofibrations

Trivial cofibration and fibration AWFS

Weak left lifting property

Mapping cylinder factorisation

The model structure

Lemma 33

Identity types and higher inductive types