Update CANONICITY.md

Author: 5HT

intro/CANONICITY.md

@@ -1,7 +1,7 @@
 Canonicity
 ==========
 
-# Prolog
+## Prolog
 
 I describe this process as the three states of cognitive viscosity—syntactic,
 propositional, and homotopical—each of which manifests across four levels of
@@ -38,9 +38,9 @@ to the idea of a reality whose structure is perfectly captured by these refined,
 mathematical models, unencumbered by the computational and cognitive limitations that
 typically obscure such understanding.
 
-# Definitions
+## Definitions
 
-## 1.1 Syntactic Canonicity
+### 1.1 Syntactic Canonicity
 
 Syntactic canonicity (sometimes referred to as computational canonicity)
 states that every closed term of a certain type reduces to a canonical
@@ -50,7 +50,7 @@ every closed term t : Nat reduces to a numeral n (i.e., `t ⇓ n` where `n ∈ 
 
 Formally: `Π (t: ℕ), Σ (n: ℕ), t ->* n`
 
-## 1.2 Propositional canonicity
+### 1.2 Propositional canonicity
 
 Propositional canonicity weakens syntactic canonicity by allowing
 the equality between a closed term and a numeral to hold only up
@@ -61,7 +61,7 @@ Formally: `Π (t: ℕ), Σ (n: ℕ), t ≡ n`
 This means that, while t may not reduce directly to n, there
 exists a derivable equality proof `p : t ≡ n` in the type theory.
 
-## 1.3 Homotopy Canonicity
+### 1.3 Homotopy Canonicity
 
 Homotopy canonicity is even weaker. Instead of requiring a definitional
 or propositional equality, it only guarantees that every closed term is
@@ -71,31 +71,38 @@ behave coherently up to homotopy.
 
 Formally, in HoTT: `Π (t: ℕ), Σ (n: ℕ), Path ℕ t n`
 
-# Canonicity Across Type Theories
+## Canonicity Across Type Theories
 
 |Type Theory|Syntactical|Propositional|Homotopy                           |
 |-----------|-----------|-------------|-----------------------------------|
 |MLTT       |        Yes| Yes         | Yes                               |
 |HoTT       |         No| Yes         | Yes (Bocquet, Kapulkin, Sattler)  |
 |CCHM       |        Yes| Yes         | Yes (Coquand, Huber, Sattler)     |
 
-# Proof Sketches of Canonicity Results
+## Proof Sketches of Canonicity Results
 
-## Failure of Syntactic Canonicity in HoTT
+Different type-theoretic frameworks impose different levels of canonicity.
+While MLTT has full syntactic, propositional, and homotopy canonicity, HoTT
+lacks syntactic canonicity but retains homotopy canonicity. Cubical HoTT
+restores full canonicity using its explicit cubical structure. Understanding
+these distinctions is crucial for developing computational and proof-theoretic
+applications of type theory.
+
+### Failure of Syntactic Canonicity in HoTT
 
 In Homotopy Type Theory, function extensionality and univalence introduce
 higher-inductive types, making reduction ambiguous for closed terms.
 Specifically, closed terms of Nat may contain elements that do not
 normalize to a numeral but are still provably equal to one in homotopy.
 
-## Proof Idea for Propositional Canonicity in HoTT
+### Proof Idea for Propositional Canonicity in HoTT
 
 Bocquet and Kapulkin-Sattler established that every term of Nat is
 propositionally equal to a numeral. The idea is to use a strict Rezk
 completion of the syntactic model to construct a fibrant replacement
 where each closed term can be shown to be propositionally equal to a numeral.
 
-## Proof Idea for Homotopy Canonicity in Cubical Type Theory
+### Proof Idea for Homotopy Canonicity in Cubical Type Theory
 
 Coquand, Huber, and Sattler proved homotopy canonicity using cubical models,
 where paths (identity types) are explicitly represented as maps over the
@@ -111,16 +118,7 @@ Table 2: Mechanisms Ensuring Canonicity in Different Type Theories
 | HoTT        | Homotopical fibrant replacement (propositional & homotopy canonicity) |
 | CCHM        | Cubical paths + hcomp enforcing structured identity types             |
 
-# Conclusion
-
-Different type-theoretic frameworks impose different levels of canonicity.
-While MLTT has full syntactic, propositional, and homotopy canonicity, HoTT
-lacks syntactic canonicity but retains homotopy canonicity. Cubical HoTT
-restores full canonicity using its explicit cubical structure. Understanding
-these distinctions is crucial for developing computational and proof-theoretic
-applications of type theory.
-
-# Example of Violating Syntactic Canonicity
+## Example of Violating Syntactic Canonicity
 
 `ℕ` defined in CCHM through `W`, `0`, `1`, `2` doesn't compute numerals expressions to same terms,
 however they are propotionally canonical in CCHM though `hcomp`.
@@ -144,7 +142,7 @@ def ℕ-ind (C : ℕ → U) (z : C zero) (s : Π (n : ℕ), C n → C (succ n))
           (λ (f : 𝟏 → ℕ) (g : Π (x : 𝟏), C (f x)), 𝟏⟶ℕ C f (s (f ★) (g ★))))
 ```
 
-## The Code
+### The Code
 
 * `ℕ-ctor` is defined as a two-point inductive type,
   which is essentially the structure of natural numbers,
@@ -160,7 +158,7 @@ def ℕ-ind (C : ℕ → U) (z : C zero) (s : Π (n : ℕ), C n → C (succ n))
 * The terms `𝟎⟶ℕ` and `𝟏⟶ℕ` define the transport functions for zero and successor cases,
   respectively, using transposition (transp).
 
-## Syntactic Canonicity
+### Syntactic Canonicity
 
 In the case of natural numbers through `W`, `0`, `1`, `2`, this would mean that terms involving
 natural numbers reduce to either 0 or succ n for some n. In this case,
@@ -178,7 +176,7 @@ they involve higher inductive types and path spaces.
   terms due to the nature of the recursion and the transport between
   different levels of the inductive structure.
 
-## Failures in Canonicity
+### Failures in Canonicity
 
 * Non-normalizing terms: Because of the presence of path-dependent
   types `PathP` and recursive definitions involving higher inductive
@@ -190,7 +188,7 @@ they involve higher inductive types and path spaces.
   to their normal form, especially if the path spaces themselves
   are complicated or not trivially reducible.
 
-## Reformulating Canonicity for Natural Numbers
+### Reformulating Canonicity for Natural Numbers
 
 To reformulate canonicity for natural numbers built using this approach, consider the following: