Cubical type theory

• Function extensionality
• Identification of isomorphic structures

Introduction

• Nominal extension of λ-calculus
• Refinement of the semantics

It is crucial for the semantics of higher inductive types to have a 'diagonal' operation. Using path types as equality types did not provide a justification of the computation rule of the Martin-Löf identity type as a judgmental equality. This problem has been solved by defining a new type 'equivalent to' but not judgmentally equal to the path type. We add two new operations on contexts: addition of new names representing dimensions and a restriction operation. Using these we can define a notion of extensibility which generalises the notion of being connected by a path, and then a Kan composition operation that expresses that being extensible is preserved along paths. We also define a new operation on types which expresses that this notion of extensibility is preserved by equivalences. The axiom of univalence, and composition for the universe, are then both expressible using this new operation.

Basic type theory

A version of dependent type theory.

• β and η-conversion for dependent functions
• Surjective pairing for dependent pairs

Lemmma 1

Substitution is admissible: Γ ⊢ J ∆ ⊢ σ : Γ --- ∆ ⊢ J σ In particular, weakening is admissible.

Path types

i, j, k, ... (a discrete infinite set of names representing directions). I is a bounded distributive lattice with top element 1 and bottom element 0 with an involution 1 − r satisfying:

• 1 − 0 = 1,
• 1 − 1 = 0,
• 1 − (r ∨ s) = (1 − r) ∧ (1 − s),
• 1 − (r ∧ s) = (1 − r) ∨ (1 − s).

Well-formed contexts, Γ ⊢

--- () ⊢ Γ ⊢ A --- (x ∈/ dom(Γ)) Γ, x : A ⊢

Well-formed types, Γ ⊢ A

Γ, x : A ⊢ B --- Γ ⊢ (x : A) → B Γ, x : A ⊢ B --- Γ ⊢ (x : A) × B Γ ⊢ --- Γ ⊢ ℕ

Well-typed terms, Γ ⊢ t : A

Γ ⊢ t : A Γ ⊢ A = B --- Γ ⊢ t : B Γ, x : A ⊢ t : B --- Γ ⊢ x ↦ t : (x : A) → B Γ ⊢ --- (x : A ∈ Γ) Γ ⊢ x : A Γ ⊢ t : (x : A) → B Γ ⊢ u : A --- Γ ⊢ t(u) : B(u) Γ ⊢ t : (x : A) × B --- Γ ⊢ t.1 : A Γ ⊢ t : (x : A) × B --- Γ ⊢ t.2 : B(t.1) Γ, x : A ⊢ B Γ ⊢ t : A Γ ⊢ u : B(t) --- Γ ⊢ (t, u) : (x : A) × B Γ ⊢ --- Γ ⊢ 0 : ℕ Γ ⊢ n : ℕ --- Γ ⊢ succ(n) : ℕ Γ, n : ℕ ⊢ P Γ ⊢ a : P(0) Γ ⊢ b : (n : ℕ) → P(n) → P(succ(n)) --- Γ ⊢ natrec(a, b) : (n : ℕ) → P(n)

Type equality, Γ ⊢ A = B

(Congruence and equivalence rules which are omitted)

Term equality, Γ ⊢ a = b : A

(Congruence and equivalence rules are omitted) Γ ⊢ t = u : A Γ ⊢ A = B --- Γ ⊢ t = u : B Γ, x : A ⊢ t : B Γ ⊢ u : A --- Γ ⊢ (x : A ↦ t(x))(u) = t(u) : B(u) Γ, x : A ⊢ t(x) = u(x) : B --- Γ ⊢ t = u : (x : A) → B Γ, x : A ⊢ B Γ ⊢ t : A Γ ⊢ u : B(t) --- Γ ⊢ (t, u).1 = t : A Γ, x : A ⊢ B Γ ⊢ t : A Γ ⊢ u : B(t) --- Γ ⊢ (t, u).2 = u : B(t) Γ, x : A ⊢ B Γ ⊢ t.1 = u.1 : A Γ ⊢ t.2 = u.2 : B(t.1) --- Γ ⊢ t = u : (x : A) × B Γ, x : ℕ ⊢ P Γ ⊢ a : P(0) Γ ⊢ b : (n : ℕ) → P(n) → P(succ(n)) --- Γ ⊢ natrec(a, b(0)) = a : P(0) Γ, x : ℕ ⊢ P Γ ⊢ a : P(0) Γ ⊢ b : (n : ℕ) → P(n) → P(succ(n)) Γ ⊢ n : ℕ --- Γ ⊢ natrec(a, b(succ(n))) = b n (natrec(a, b(n))) : P(succ(n))

Syntax and inference rules

Contexts can now be extended with name declarations: Γ, ∆ ::= ... | Γ, i : I together with the context rule: Γ ⊢ --- (i ∈/ dom(Γ)) Γ, i : I ⊢ The extension to the syntax of basic dependent type theory is: t, u, A, B ::= ... | t →_A u | ⟨i⟩ t | t(r) Path types

Inference rules for path types

Γ ⊢ A Γ ⊢ t, u : A --- Γ ⊢ t →_A u Γ ⊢ A Γ, i : I ⊢ t : A --- Γ ⊢ ⟨i⟩ t : t(i/0) →_A t(i/1) Γ ⊢ t : u₀ →_A u₁ Γ ⊢ r : I --- Γ ⊢ t(r) : A Γ ⊢ A Γ, i : I ⊢ t : A Γ ⊢ r : I --- Γ ⊢ (⟨i⟩ t)(r) = t(i/r) : A Γ, i : I ⊢ t(i) = u(i) : A --- Γ ⊢ t = u : u₀ →_A u₁Γ ⊢ t : u₀ →_A u₁--- Γ ⊢ t(0) = u₀ :A Γ ⊢ t : u₀ →_A u₁--- Γ ⊢ t(1) = u₁ : A

1_a : a →_A a 1_a ≡ ⟨i⟩ a, corresponding to a proof of reflexivity. The intuition is that a type in a context with n names corresponds to an n-dimensional cube:

Examples

Γ ⊢ a : A Γ ⊢ b : A Γ ⊢ f : A → B Γ ⊢ p : a →_A b --- Γ ⊢ ⟨i⟩ f(p(i)) : f(a) →_B f(b) Function extensionality for path types: Γ ⊢ f, g : (x : A) → B Γ ⊢ p : (x : A) → f(x) →_B g(x) --- Γ ⊢ ⟨i⟩ x : A ↦ p(x(i)) : f →_{(x : A) → B} g To see that this is correct we check that the term has the correct faces, for instance: (⟨i⟩ x : A ↦ p(x(i)))(0) = x : A ↦ p(x(0)) = x : A ↦ f(x) = f We can also justify the fact that singletons are contractible, that is, that any element in (x : A) × a →_A x is equal to (a, 1_a): Γ ⊢ p : a →_A b --- Γ ⊢ ⟨i⟩ (p(i), ⟨j⟩ p (i ∧ j)) : (a, 1_a) →_{(x : A) × a →A x} (b, p)

Systems, composition, and transport

The face lattice

Face formulas φ, ψ ::= 0_F | 1_F | (i = 0) | (i = 1)| φ ∧ ψ | φ ∨ ψ We have (r = 1) ∧ (r = 0) = 0_F and we define the lattice map F → F, ψ ↦ ψ(i/r) sending (i = 1) to (r = 1) and (i = 0) to (r = 0). Restriction operation Γ, ∆ ::= ... | Γ, φ together with the rule: Γ ⊢ φ : F --- Γ, φ ⊢

Lemma 2

For any element φ of F and any name i we have φ = (∀i.φ) ∨ (φ ∧ (i = 0)) ∨ (φ ∧ (i = 1)) We also have φ ∧ (i = 0) ≤ φ(i/0) and φ ∧ (i = 1) ≤ φ(i/1).

Syntax and inference rules for systems

Sub-polyhedra as compatible unions of cubes. t, u, A, B ::= ... | [] | [φ₁ t₁, ..., φ_n tn ] Systems ∆, (i = 0) ∨ (i = 1) ⊢ (i = 0) ∨ (i = 1) = 1_F.

Inference rules for systems with side condition Γ ⊢ φ₁ ∨ ⋯ ∨ φ_n = 1_F : F

Γ, φ₁ ⊢ A₁ ⋯ Γ, φ_n ⊢ A_n Γ, φ_i ∧ φ_j ⊢ A_i = A_j (1 ≤ i, j ≤ n) --- Γ ⊢ [φ₁ A₁, ⋯, φ_n A_n] Γ ⊢ A Γ, φ₁ ⊢ t₁ : A ⋯ Γ, φ_n ⊢ t_n : A Γ, φ_i ∧ φ_j ⊢ t_i = t_j : A (1 ≤ i, j ≤ n) --- Γ ⊢ [φ₁ t₁, ⋯, φ_n t_n] : A (if Γ ⊢ 0_F = 1_F : F and Γ ⊢ A, then Γ ⊢ [] : A) Γ, φ₁ ⊢ J ⋯ Γ, φ_n ⊢ J --- Γ ⊢ J Γ ⊢ [φ₁ A₁, ⋯, φ_n A_n] Γ ⊢ φ_i = 1_F : F --- Γ ⊢ [φ₁ A₁, ⋯, φ_n A_n] = A_iΓ ⊢ [φ₁ t₁, ⋯, φ_n t_n] : A Γ ⊢ φ_i = 1_F : F --- Γ ⊢ [φ₁ t₁, ⋯, φ_n t_n] = t_i : A We extend the definition of the substitution judgment by ∆ ⊢ σ : Γ, φ if ∆ ⊢ σ : Γ, Γ ⊢ φ : F, and ∆ ⊢ φ σ = 1_F : F. If Γ, φ ⊢ u : A, then Γ ⊢ a : A[φ ↦ u] is an abbreviation for Γ ⊢ a : A and Γ, φ ⊢ a = u : A. In this case, we see this element a as a witness that the partial element u, defined on the 'extent' φ (using the terminology from [10]), is extensible. More generally, we write Γ ⊢ a : A[φ₁ ↦ u₁, ..., φ_k ↦ u_k] for Γ ⊢ a : A and Γ, φ_l ⊢ a = u_l : A for l = 1, ..., k. For instance, if Γ, i : I ⊢ A and Γ, i : I, φ ⊢ u : A where φ = (i = 0) ∨ (i = 1) then the element u is determined by two elements Γ ⊢ a₀ : A(i/0) and Γ ⊢ a₁ : A(i/1) and an element Γ, i : I ⊢ a : A[(i = 0) ↦ a₀, (i = 1) ↦ a₁] gives a path connecting a₀ and a₁.

Lemma 3

Γ ⊢ φ ≤ ψ : F Γ, ψ ⊢ J --- Γ, φ ⊢ J Γ, 1_F ⊢ J --- Γ ⊢ J Γ, φ, ψ ⊢ J === Γ, φ ∧ ψ ⊢ J Furthermore, if φ is independent of i, the following rules are admissible: Γ, i : I, φ ⊢ J === Γ, φ, i : I ⊢ J and it follows that we have in general: Γ, i : I, φ ⊢ J --- Γ, ∀i.φ, i : I ⊢ J

Composition operation

t, u, A, B ::= ... | compⁱ A[φ ↦ u] a₀ Compositions where u is a system on the extent φ. Γ ⊢ φ : F Γ, i : I ⊢ A Γ, φ, i : I ⊢ u : A Γ ⊢ a₀ : A(i/0)[φ ↦ u(i/0)] --- Γ ⊢ compⁱ A[φ ↦ u] a₀ : A(i/1)[φ ↦ u(i/1)] Γ ⊢ compⁱ A [_F ↦ u] a₀ = u(i/1) : A(i/1) If we have a substitution ∆ ⊢ σ : Γ, then (compⁱ A[φ ↦ u] a₀) σ = comp^j A(σ, i/j) [φ σ ↦ u(σ, i/j)] a₀ σ where j is fresh for ∆, which corresponds semantically to the uniformity of the composition operation. We use the abbreviation [φ₁ ↦ u₁, ..., φ_n ↦ u_n] for [∨_l φ_l ↦ [φ₁ u₁, ..., φ_n u_n]] and in particular we write [] for [0_F ↦ []].

Example 4

Transitivity Γ ⊢ p : a →_A b Γ ⊢ q : b →_A c --- Γ ⊢ ⟨i⟩ comp^j A[(i = 0) ↦ a, (i = 1) ↦ q(j)] p(i) : a →_A c

Kan filling operation

Γ, i : I ⊢ fillⁱ A[φ ↦ u] a₀ = comp^j A(i/i ∧ j)[φ ↦ u(i/i ∧ j), (i = 0) ↦ a₀] a₀ : A where j is fresh for Γ. The element Γ, i : I ⊢ v = fillⁱ A [φ ↦ u] a₀ : A satisfies: Γ ⊢ v(i/0) = a₀ : A(i/0) Γ ⊢ v(i/1) = compⁱ A[φ ↦ u] a₀ : A(i/1) Γ, φ, i : I ⊢ v = u : A If φ is the boundary formula on the names declared in Γ, we recover the Kan operation for cubical sets.

Equality judgements for composition

The equality judgments for compⁱ C [φ ↦ u] a₀ are defined by cases on the type C which depends on i, i.e., Γ, i : I ⊢ C. The right hand side of the definitions are all equal to u(i/1) on the extent φ by the typing rule for compositions. There are four cases to consider:Product types, C ≡ (x : A) → B Given Γ, φ, i : I ⊢ μ : C and Γ ⊢ λ0 : C(i/0)[φ ↦ μ(i/0)] the composition will be of type C(i/1). For Γ ⊢ u₁ : A(i/1), we first let: w ≡ fillⁱ A(i/1 − i)[] u₁ (in context Γ, i : I and of type A(i/1 − i)) v ≡ w(i/1 − i) (in context Γ, i : I and of type A) Using this we define the equality judgment: Γ ⊢ (compⁱ C [φ ↦ μ] λ0) u₁ = compⁱ B(x/v) [φ ↦ μ v] (λ₀ v(i/0)) : B(x/v)(i/1)Sum types, C ≡ (x : A) × B Given Γ, φ, i : I ⊢ w : C and Γ ⊢ w0 : C(i/0)[φ ↦ w(i/0)] we let: a ≡ fillⁱ A[φ ↦ w.1] w₀.1 (in context Γ, i : I and of type A) c1 ≡ compⁱ A [φ ↦ w.1] w₀.1 (in context Γ and of type A(i/1)) c2 ≡ compⁱ B(x/a) [φ ↦ w.2] w₀.2 (in context Γ and of type B(x/a)(i/1)) From which we define: Γ ⊢ compⁱ C [φ ↦ w] w₀ = (c1, c2) : C(i/1)Natural numbers, C ≡ ℕ In this we define compⁱ C [φ ↦ n] n₀ by recursion: Γ ⊢ compⁱ C [φ ↦ 0] 0 = 0 : C Γ ⊢ compⁱ C [φ ↦ succ(n)](succ(n₀)) = s(compⁱ C [φ ↦ n] n₀) : CPath types, C ≡ u →_A v Given Γ, φ, i : I ⊢ p : C and Γ ⊢ p₀ : C(i/0)[φ ↦ p(i/0)] we define: Γ ⊢ compⁱ C [φ ↦ p] p₀ = ⟨j⟩ compⁱ A [φ ↦ p j, (j = 0) ↦ u, (j = 1) ↦ v] (p₀ j) : C(i/1)

Transport

Composition for φ = 0_F corresponds to transport: Γ ⊢ transpⁱ(A, a) = compⁱ A [] a : A(i/1)

Derived notions and operations

Contractible types

is_contr(A) ≡ (x : A) × (y : A) → x →_A y. Given Γ ⊢ p : is_contr(A) and Γ, φ ⊢ u : A we define the operation Γ ⊢ contr p [φ ↦ u] ≡ compⁱ A [φ ↦ p.2 u i] p.1 : A[φ ↦ u] This expresses that the restriction map Γ, φ → Γ has the left lifting property w.r.t. any 'trivial fibration', i.e., contractible extensions Γ, x : A → Γ. The restriction maps Γ, φ → Γ thus represent 'cofibrations' while the maps Γ, x : A → Γ represent 'fibrations'.

Lemma 5

Let Γ ⊢ A and assume that we have one operation Γ, φ ⊢ u : A --- Γ ⊢ contr [φ ↦ u] : A[φ ↦ u] then we can find an element of is_contr(A). Proof. We define x ≡ contr [] : A and prove that any element y : A is path equal to x. For this, we introduce a fresh name i : I and define φ = (i = 0) ∨ (i = 1) and u = [(i = 0) ↦ x, (i = 1) ↦ y]. Using this we obtain Γ, i : I ⊢ v = contr [φ ↦ u] : A[φ ↦ u]. In this way, we get a path ⟨i⟩ contr [φ ↦ u] connecting x and y.

The pres operation

Lemma 6

Γ, i : I ⊢ f : T → A Γ ⊢ φ : F Γ, φ, i : I ⊢ t : T Γ ⊢ t₀ : T(i/0)[φ ↦ t(i/0)] --- Γ ⊢ presⁱ f [φ ↦ t] t₀ : (c1 →_A(i/1) c2)[φ ↦ ⟨j⟩ f(t)(i/1)] where c1 ≡ compⁱ A [φ ↦ f(t)] (f(i/0) t₀) and c2 ≡ f(i/1) (compⁱ T [φ ↦ t] t₀). Proof. Let Γ ⊢ a₀ = f(i/0) t₀ : A(i/0) and Γ, i : I ⊢ v = fillⁱ T[φ ↦ t] t₀ : T. We take presⁱ f [φ ↦ t] t₀ = ⟨j⟩ compⁱ A [φ ∨ (j = 1) ↦ f v] a₀. Note that presⁱ binds i in f and t.

The equiv operation

is_equiv(T, A, f) ≡ (y : A) → is_contr((x : T) × y →_A (f(x))) and T ≃ A ≡ Σ_{f : T → A} is_equiv(T, A, f). If f : T ≃ A and t : T , we may write f(t) for f.1 t.

Lemma 7

If Γ ⊢ f : T ≃ A, we have an operation Γ, φ ⊢ t : T Γ ⊢ a : A Γ, φ ⊢ p : a →_A f(t) --- Γ ⊢ equiv f [φ ↦ (t, p)] a : ((x : T) × a →_A (f(x)))[φ ↦ (t, p)] Conversely, if Γ ⊢ f : T → A and we have such an operation, then we can build a proof that f is an equivalence. Proof. We define equiv f [φ ↦ (t, p)] a ≡ contr (f.2 a) [φ ↦ (t, p)] using the contr operation defined above. The second statement follows from Lemma 5.

Glueing

Syntax and inference rules for glueing

t, u, A, B ::= ... | Glue [φ ↦ (T, f)] A Glue type | glue [φ ↦ t] u Glue term | unglue [φ ↦ f] u Unglue term

Inference rules for glueing

Γ ⊢ A Γ, φ ⊢ T Γ, φ ⊢ f : T ≃ A --- Γ ⊢ Glue [φ ↦ (T, f)] A, Γ ⊢ b : Glue [φ ↦ (T, f)] A --- Γ ⊢ unglue b : A[φ ↦ f(b)], Γ, φ ⊢ f : T ≃ A Γ, φ ⊢ t : T Γ ⊢ a : A[φ ↦ f(t)] --- Γ ⊢ glue [φ ↦ t] a : Glue [φ ↦ (T, f)] A, Γ ⊢ T Γ ⊢ f : T ≃ A --- Γ ⊢ Glue [1_F ↦ (T, f)] A = T, Γ ⊢ t : T Γ ⊢ f : T ≃ A --- Γ ⊢ glue [1_F ↦ t] (f t) = t : T, Γ ⊢ b : Glue [φ ↦ (T, f)] A --- Γ ⊢ b = glue [φ ↦ b] (unglue b) : Glue [φ ↦ (T, f)] A, Γ, φ ⊢ f : T ≃ A Γ, φ ⊢ t : T Γ ⊢ a : A[φ ↦ f t] --- Γ ⊢ unglue (glue [φ ↦ t] a) = a : A if Γ ⊢ b : Glue [φ ↦ (T, f)] A, then Γ, φ ⊢ b : T.

Example 8

Using glueing we can construct a path from an equivalence Γ ⊢ f : A ≃ B by defining Γ, i : I ⊢ E ≡ Glue [(i = 0) ↦ (A, f), (i = 1) ↦ (B, id_B)] B so that E(i/0) = A and E(i/1) = B, where id_B : B ≃ B is defined as: id_B ≡ (x : B ↦ x, x : B ↦ ((x, 1_x), u : (y : B) × x →_B y ↦ ⟨i⟩ (u.2 i, ⟨j⟩ u.2 (i ∧ j)))). In Section 7 we introduce a universe of types U and we will be able to define a function of type (A, B : U) → A ≃ B → A →_U B by: (A, B : U) ↦ (f : A ≃ B) ↦ ⟨i⟩ Glue [(i = 0) ↦ (A, f), (i = 1) ↦ (B, id_B)] B

Composition for glueing

We assume Γ, i : I ⊢ B = Glue [φ ↦ (T, f)] A, and define the composition in B. In order to do so, assume Γ, ψ, i : I ⊢ b : B Γ ⊢ b₀ : B(i/0)[ψ ↦ b(i/0)] and define: a ≡ unglue b (in context Γ, ψ, i : I and of type A[φ ↦ f(b)]) a₀ ≡ unglue b₀ (in context Γ and of type A(i/0)[φ(i/0) ↦ f(i/0) b₀, ψ ↦ a(i/0)]) The following provides the algorithm for composition compⁱⁱ B [ψ ↦ b] b₀ = b1 of type B(i/1)[ψ ↦ b(i/1)]. δ = ∀i.φ Γ a′1 = compⁱ A [ψ ↦ a] a₀ Γ t′1 = compⁱ T [ψ ↦ b] b₀ Γ, δ ω = presⁱ f [ψ ↦ b] b₀ Γ, δ (t1, α) = equiv f(i/1) [δ ↦ (t′1, ω), ψ ↦ (b(i/1), ⟨j⟩ a′1)] a′1 Γ, φ(i/1) a₁ = comp^j A(i/1) [φ(i/1) ↦ α j, ψ ↦ a(i/1)] a′1 Γ b1 = glue [φ(i/1) ↦ t1] a′1 Γ We can check that whenever Γ, i : I ⊢ φ = 1_F : F the definition of b₁ coincides with compⁱ T [ψ ↦ b] b₀, which is consistent with the fact that B = T in this case.

Universe and the univalence axiom

Γ ⊢ --- Γ ⊢ U, Γ ⊢ A : U --- Γ ⊢ A. In particular, we have Γ ⊢ Glue [φ ↦ (T, f)] A : U whenever Γ ⊢ A : U, Γ, φ ⊢ T : U, and Γ, φ ⊢ f : T ≃ A.

Composition for the universe

Given Γ ⊢ A, Γ ⊢ B, and Γ, i : I ⊢ E, such that E(i/0) = A and E(i/1) = B, we will construct equivi(E) : A ≃ B. In order to do this we first define f ≡ x : A ↦ transpⁱ(E, x) (in context Γ and of type A → B) g ≡ y : B ↦ (transpⁱ(E(i/1 − i), y))(i/1 − i) (in context Γ and of type B → A) u ≡ x : A ↦ fillⁱ E [] x (in context Γ, i : I and of type A → E) v ≡ y : B ↦ (fillⁱ E(i/1 − i) [] y)(i/1 − i) (incontext Γ, i : I and of type B → E) such that: u(i/0) = x : A ↦ x u(i/1) = f v(i/0) = g v(i/1) = y : B ↦ y. Given y : B we see that (x : A) × y →_B f(x) is inh(A) bited as it contains the element (g y, ⟨j⟩ θ₀(i/1)) where θ₀ ≡ fillⁱ E[(j = 0) ↦ v y, (j = 1) ↦ u (g y)] (g y). Next, given an element (x, β) of (x : A) × y →_B f(x) we will construct a path from (g y, ⟨j⟩ θ₀(i/1)) to (x, β). Let θ₁ ≡ (fillⁱ E(i/1 − i)[(j = 0) ↦ (v y)(i/1 − i), (j = 1) ↦ (u x)(i/1 − i)](β j)) (i/1 − i) and ω = θ₁(i/0) so Γ, i, j : I ⊢ θ₁ : E, ω(j/0) = g y, and ω(j/1) = x. And further with δ = compⁱ E[(k = 0) ↦ θ₀, (k = 1) ↦ θ₁, (j = 0) ↦ v y, (j = 1) ↦ u ω(j/k)] ω(j/j ∧ k) we obtain ⟨k⟩ (ω(j/k), ⟨j⟩ δ) : (g y, ⟨j⟩ θ₀(i/1)) →_{(x : A) × y →B f(x)} (x, β) as desired. This concludes the proof that f is an equivalence and thus also the construction of equivi E : A ≃ B. Using this we can now define the composition for the universe: Γ ⊢ compⁱ U [φ ↦ E] A₀ = Glue [φ ↦ (E(i/1), equivi E(i/1 − i))] A₀ : U Remark. Given Γ, i : I ⊢ E we can also get an equivalence in A ≃ B (where A = E(i/0) and B = E(i/1)) with a less direct description by Γ ⊢ transpⁱ(A ≃ E, id_A) : A ≃ B

The univalence axiom

Given B = Glue [φ ↦ (T, f)] A the map unglue : B → A extends f, in the sense that Γ, φ ⊢ unglue b = f(b) : A if Γ ⊢ b : B.

Theorem 9

The map unglue : B → A is an equivalence. Proof. By Lemma 7 it suffices to construct ̃b : B [ψ ↦ b] α ̃ : u →_A (unglue ̃b ) [ψ ↦ α] given Γ, ψ ⊢ b : B and Γ ⊢ u : A and Γ, ψ ⊢ α : u →_A (unglue b). Since Γ, φ ⊢ f : T → A is an equivalence and Γ, φ, ψ ⊢ b : T Γ, φ, ψ ⊢ α : u →_A f(b) we get, using Lemma 7 Γ, φ ⊢ t : T[ψ ↦ b] Γ, φ ⊢ β : u →_A f t[ψ ↦ α] We then define a ̃ = compⁱ A [φ ↦ β i, ψ ↦ α i] u, and using this we conclude by letting ̃b = glue [φ ↦ t] a ̃ and α ̃ = fillⁱ A[φ ↦ βi, ψ ↦ αi]u.

Corollary 10

For any type A : U the type C ≡ (X : U) × X ≃ A is contractible.4 Proof. It is enough by Lemma 5 to show that any partial element φ ⊢ (T, f) : C is path equal to the restriction of a total element. The map unglue extends f and is an equivalence by the previous theorem. Since any two elements of the type is_equiv X A f.1 are path equal, this shows that any partial element of type C is path equal to the restriction of a total element. We can then conclude by Theorem 9.

Corollary 11 (Univalence axiom)

For any term t : (A, B : U) → (A →_U B) → A ≃ B the map t(A, B) : (A →_U B) → A ≃ B is an equivalence. Proof. Both (X : U) × A →_U X and (X : U) × A ≃ X are contractible. Hence the result follows from Theorem 4.7.7 in [26].

Semantics

Cubical sets, as a presheaf category. Composition structure.

The category of cubes and cubical sets

Extensions: identity types and higher inductive types

Identity types

Identity types(formation) Γ ⊢ A Γ ⊢ a₀ : A Γ ⊢ a₁ : A --- Γ ⊢ a₀ =_A a₁, (introduction) Γ ⊢ ω : a₀ →_A a₁[φ ↦ ⟨i⟩ a₀] --- Γ ⊢ (ω, φ) : a₀ =_A a₁, and we can define r a = (1_a, 1_F) : a =_A a for a : A. (elimination) Given Γ ⊢ a : A, Γ, x : A, α : a =_A x ⊢ C Γ ⊢ d : C(x/a, α/r a) Γ ⊢ b : A Γ ⊢ β : a =_A b --- Γ ⊢ J_{x, α.C} d b β : C(x/b, α/β) together with the following judgmental equality in case β is of the form (ω, φ) J d b β = compⁱ C(x/ω i, α/β^*(i)) [φ ↦ d] d where Γ, i : I ⊢ β^*(i) : a =_A (ω i) is given by β^*(i) ≡ (⟨j⟩ ω (i ∧ j), φ ∨ (i = 0)). Note. J d a (r a) = d. Given Γ, i : I ⊢ a₀ =_A a₁, Γ, φ, i : I ⊢ (ω, ψ) : a₀ =_A a₁, and Γ ⊢ (ω₀, ψ₀) : (a₀ =_A a₁)(i/0)[φ ↦ (ω(i/0), ψ(i/0))] we have the judgmental equality compⁱ (a₀ =_A a₁) [φ ↦ (ω, ψ)] (ω₀, ψ₀) = (compⁱ (a₀ →_A a₁) [φ ↦ ω] ω₀, φ ∧ ψ(i/1)). a =_A b and a →_A b are path-equivalent. A type is path-equivalent iff it is id-contractable. The univalence axiom for the path-type hold as well for the id-type.Cofibration-trivial fibration factorisation'trivial fibration' to be a first projection from a total space of a contractible family of types and a 'cofibration' to be a map that has the left lifting property against any trivial fibration. For this we define, for b : B, the type T_f(b) to be the type of elements [φ ↦ a] with φ ⊢ a : A and φ ⊢ f(a) = b : B.

Theorem 24

The type T_f(b) is contractible and the map A → (b : B) × T_f(b), a ↦ (f(a), [1_F ↦ a]) is a cofibration.

Higher inductive types

Extension to dependent path typesIf i : I ⊢ A and ⊢ a₀ : A(i/0), a₁ : A(i/1), then ⊢ a₀ →ⁱ_A a₁. (introduction) ⊢ ⟨i⟩ t : t(i/0) →ⁱ_A t(i/1) if i : I ⊢ t : A. (elimination) ⊢ p(r) : A(i/r) if ⊢ p : a₀ →ⁱ_A a₁ with equalities p(0) = a₀ : A(i/0) and p(1) = a₁ : A(i/1).SpheresCircle S¹: Γ ⊢ --- Γ ⊢ S¹, Γ ⊢ --- Γ ⊢ base : S¹, Γ ⊢ r : I --- Γ ⊢ loop(r) : S¹, loop(0) = loop(1) = base. Composition as a constructor operation hcompⁱ: Γ, φ, i : I ⊢ u : S¹ Γ ⊢ u₀ : S¹[φ ↦ u(i/0)] --- Γ ⊢ hcompⁱ [φ ↦ u] u₀ : S¹, hcompⁱ [1_F ↦ u] u₀ = u(i/1). Given Π_{x : S¹} A(x), a : A(base) and l : a →ⁱ_A(loop(i)) a, we can define a function g : Π_{x : S¹} A, g(base) ≡ a, g(loop(r)) ≡ l(r), g(hcompⁱ [φ ↦ u] u₀) = compⁱ A(v) [φ ↦ g(u)] (g(u₀)), v ≡ fillⁱ S¹ [φ ↦ u] u₀ = hcomp^j [φ ↦ u(i/i ∧ j), (i = 0) ↦ u₀] u₀. This definition is non ambiguous since l(0) = l(1) = a. For the equation g(loop(r)) = l(r), it may be that l and r are dependent on the same name i, and we could not have followed this definition in the framework of [6]. We have a similar definition for Sn taking as constructors base and loop(r1, ..., rn).propositional truncationΓ ⊢ A --- Γ ⊢ inh(A), Γ ⊢ a : A --- Γ ⊢ inc(a) : inh(A), Γ ⊢ u₀, u₁ : inh(A) Γ ⊢ r : I --- Γ ⊢ squash(u₀, u₁, r) : inh(A), squash(u₀, u₁, 0) ≡ u₀, squash(u₀, u₁, 1) ≡ u₁. Composition as a constructor: Γ, φ, i : I ⊢ u : inh(A) Γ ⊢ u₀ : inh(A[φ ↦ u(i/0)]) --- Γ ⊢ hcompⁱ [φ ↦ u] u₀ : inh(A), hcompⁱ [1_F ↦ u] u₀ ≡ u(i/1). This provides only a definition of compⁱ inh(A) [φ ↦ u] u₀ in the case where A is independent of i, and we have to explain how to define the general case. Γ, i : I ⊢ A Γ ⊢ u₀ : inh(A(i/0)) --- Γ ⊢ transp(u₀) : inh(A(i/1)), Γ, i : I ⊢ A Γ, i : I ⊢ u : inh(A) --- Γ ⊢ squeezeⁱ(u) : transp(u(i/0)) →_inh(A(i/1)) u(i/1), transp(inc(a)) ≡ inc(compⁱ A [] a), transp(squash(u₀, u₁, r)) ≡ squash(transp(u₀), transp(u₁), r), transp(hcomp^j [φ ↦ u] u₀) ≡ hcomp^j [φ ↦ transp(u)] transp(u₀), squeezeⁱ(inc(a)) ≡ ⟨i⟩ inc(comp^j A(i ∨ j) [(i = 1) ↦ a(i/1)] a), squeezeⁱ(squash(u₀, u₁, r)) ≡ ⟨k⟩ squash(squeezeⁱ(u₀(k)), squeezeⁱ(u₁(k)), r(i/k)), squeezeⁱ(hcomp^j [φ ↦ u] v) ≡ ⟨k⟩ hcomp^j S (squeezeⁱ(v(k))), S is the system [δ ↦ squeezeⁱ(u(k)), φ(i/k) ∧ (k = 0) ↦ transp(u(i/0)), φ(i/k) ∧ (k = 1) ↦ u(i/1)], δ = ∀i.φ. General composition: Γ, i : I ⊢ A Γ, φ , i : I ⊢ u : inh(A) Γ ⊢ u₀ : inh(A(i/0)[φ ↦ u(i/0)]) --- Γ ⊢ compⁱ inh(A) [φ ↦ u] u₀ : inh(A(i/1)[φ ↦ u(i/1)]), Γ ⊢ compⁱ inh(A) [φ ↦ u] u₀ ≡ hcomp^j [φ ↦ squeezeⁱ(u(j))] (transp(u₀)) : inh(A)(i/1). Given Γ ⊢ B, Γ ⊢ q : Π_{x, y : B} (x →_B y) and f : A → B we define g : inh(A) → B by the equations g(inc(a)) ≡ f(a), g(squash(u₀, u₁, r)) ≡ q(g(u₀), g(u₁))(r), g(hcomp^j [φ ↦ u] u₀) ≡ comp^j B [φ ↦ g(u)] g(u₀).