Internal Parametricity for Cubical Type Theory

Intro

(smash product, tensor product for U_*) U_* ≡ (X : U) × X, (∧) : U_* → U_* → U_*, α : (X, Y, Z : U∗) → (X ∧ Y) ∧ Z → X ∧ (Y ∧ Z).

Cubical type theory: all constructions act on isomorphisms Internally parametric type theory: all constructions act on relations

dimension variables bridge-discrete types

Cubical type theory

Path dimensions

Rules for Path-types

behavioral specifications path dimensions Γ, i : I ≫ A Γ ≫ a0 : A⟨0/x⟩ Γ ≫ a1 : A⟨1/x⟩ --- Γ ≫ Path i.A (a0, a1), Γ, i : I ≫ a : A Γ ≫ a⟨0/x⟩ =_A⟨0/x⟩ a0 Γ ≫ a⟨1/x⟩ =_A⟨1/x⟩ a1 --- Γ ≫ (i : I ↦ a) : Path i.A (a0, a1), Γ ≫ Q : Path i.A (a0, a1) Γ ≫ j pdim --- Γ ≫ Q @ j : A⟨j/i⟩, Γ, i : I ≫ a : A --- Γ ≫ (i : I ↦ a) @ j =_A⟨j/i⟩ a⟨j/i⟩, Γ ≫ Q : Path i.A (a0, a1) ε : 1--- Γ ≫ Q @ ε =_A⟨ε/i⟩ a_ε, Γ ≫ Q : Path i.A (a0, a1) --- Γ ≫ Q = (i : I ↦ Q) @ i : Path i.A (a0, a1),

--- ·, Γ Γ ≫ A --- Γ, a : A, Γ --- Γ, i : I, Γ Γ ≫ i pdim Γ ≫ j pdim --- Γ, i = j.

A path between a0 : A and a1 : A is a term i : I ≫ a : A such that a⟨0/i⟩ = a0 and a⟨1/i⟩ = a1. (function extensionality) f0, f1 : (a : A) → B, h : (a : A) → Path B (f0(a), f1(a)) ⊢ (i : I) (a : A) ↦ h(a) @ i : f0 →_{(a : A) → B} f1.

Coercion and composition

a : A ⊢ (i : I) ↦ a : a →_A a. The coercion operation turns paths of types into isomorphisms. (isomorphism) A ≃ B ≡ (f : A → B) × (g, h : B → A) × ((a : A) → (g f)(a) →_A a) × ((b : B) → (f h)(b) →_B b). (coercion) Γ, i : I ≫ A Γ ≫ r, s pdim Γ ≫ a : A⟨r/i⟩ --- Γ ≫ coe_i.A^{r ↝ s}(a) : A⟨s/i⟩. All constructions respect paths: B : A → U, a0 : A0, b : B(a0), p : Path A(a0, a1) ⊢ coe_{i.B(p @ i)}^{0 ↝ 1} (b) : B(a1).

Paths in the universe: V-types and univalence

Higher inductive types

Internalising parametricity

Parametricity captures the vague concept of 'uniformity in type variables' by the precise concept of acting on relations.

Bridge dimensions