Normalization for Cubical Type Theory

Syntactic open

(subterminal object) syn : E, j_!1 = (1, 0 → α^*1), Pr(T_□) ≃ E_/syn, syn^* : E → E_/syn, syn_* : E_/syn → E

Syntactic T_□-model

T_□-Mod(U_○)

Family of term variables

var : Pr(A_□)_/α^*tm, tm : Pr(T_□)

Glued interval

I ≡ j_*y_T□(I), I : E, j^*I = y_T□(I). j_*I = y_A□(·.I).

Lemma 32

Y → U, j : U ↪_○ X, i : U ↪_● X,

Normalisation for Cubical Type Theory

Remark 35

α : A_□ → T_□, α_! ⊣ α^*, i : A ↪_● G , E : Pr(A_□), (α_!E, E → α^*α_!E)

Construction 36

Γ : A_□, ⦇Γ⦈

Construction 37

M' : T_□ → E, α : A_□ → T_□, ⟦−⟧ : A_□ → E, M'(α(Γ)), j^*⟦Γ⟧ = y_T□(α(Γ)) = α_!y_A□(Γ).

Construction 38

X : E, [⟦−⟧, X] → α^*j^*X : Pr(A_□), M'(α(Γ)) → X : E,

Construction 39

⦇−⦈ → ⟦−⟧ : Hom(A□, E)

Normalisation function

M' : T□ → E, M.tp → (M'.tp)_M'. atom_M'.tp^*, nftp.

Correctness of normalisation

Completeness, Soundness

Injectivity of type constructors

E = Sh(G□), ∀A, A', B, B'. M.Π(A, B) = M.Π(A', B') ⇒ ●((A, B) = (A', B'))

Idempotence of normalisation

nbe(A) = A, nbe(a) = a

Uniqueness of normalisation

Normalisation algorithm

Decidability of equality