Skip to content

Commit 316c251

Browse files
5HT5HT
committed
canonicity
1 parent d7b36b6 commit 316c251

File tree

4 files changed

+291
-31
lines changed

4 files changed

+291
-31
lines changed

‎intro/canonicity/REAMDE.md‎

Lines changed: 253 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,253 @@
1+
Canonicity
2+
==========
3+
4+
# Definitions
5+
6+
## 1.1 Syntactic Canonicity
7+
8+
Syntactic canonicity (sometimes referred to as computational canonicity)
9+
states that every closed term of a certain type reduces to a canonical
10+
form using the internal reduction rules of the type theory. Specifically,
11+
for the type of natural numbers (Nat), syntactic canonicity means that
12+
every closed term t : Nat reduces to a numeral n (i.e., t ⇓ n where n ∈ ℕ).
13+
14+
Formally: `Π (t: ℕ), Σ (n: ℕ), t ->* n`
15+
16+
## 1.2 Propositional canonicity
17+
18+
Propositional canonicity weakens syntactic canonicity by allowing
19+
the equality between a closed term and a numeral to hold only up
20+
to propositional equality (≡), rather than requiring direct computational reduction.
21+
22+
Formally: `Π (t: ℕ), Σ (n: ℕ), t ≡ n`
23+
24+
This means that, while t may not reduce directly to n, there
25+
exists a derivable equality proof p : t ≡ n in the type theory.
26+
27+
## 1.3 Homotopy Canonicity
28+
29+
Homotopy canonicity is even weaker. Instead of requiring a definitional
30+
or propositional equality, it only guarantees that every closed term is
31+
homotopically equivalent to a numeral. This is relevant in frameworks
32+
like HoTT, where identity types may not be strictly computable but still
33+
behave coherently up to homotopy.
34+
35+
Formally, in HoTT: `Π (t: ℕ), Σ (n: ℕ), Path ℕ t n`
36+
37+
# Canonicity Across Type Theories
38+
39+
|Type Theory|Syntactical|Propositional|Homotopy |
40+
|-----------|-----------|-------------|-----------------------------------|
41+
|MLTT | Yes| Yes | Yes |
42+
|HoTT | No| Yes | Yes (Bocquet, Kapulkin, Sattler) |
43+
|CCHM | Yes| Yes | Yes (Coquand, Huber, Sattler) |
44+
45+
3. Proof Sketches of Canonicity Results
46+
47+
3.1 Failure of Syntactic Canonicity in HoTT
48+
49+
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.
50+
51+
3.2 Proof Idea for Propositional Canonicity in HoTT
52+
53+
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.
54+
55+
3.3 Proof Idea for Homotopy Canonicity in Cubical Type Theory
56+
57+
Coquand, Huber, and Sattler proved homotopy canonicity using cubical models, where paths (identity types) are explicitly represented as maps over the interval type I. The crucial tool here is homogeneous composition (hcomp), which ensures that any term in Nat is homotopically equivalent to a numeral, enforcing canonicity in a structured manner.
58+
59+
Table 2: Mechanisms Ensuring Canonicity in Different Type Theories
60+
61+
| Type Theory | Mechanism for Canonicity |
62+
|-------------|-----------------------------------------------------------------------|
63+
| MLTT | Normalization via term reduction (syntactic canonicity) |
64+
| HoTT | Homotopical fibrant replacement (propositional & homotopy canonicity) |
65+
| CCHM | Cubical paths + hcomp enforcing structured identity types |
66+
67+
# Conclusion
68+
69+
Different type-theoretic frameworks impose different levels of canonicity.
70+
While MLTT has full syntactic, propositional, and homotopy canonicity, HoTT
71+
lacks syntactic canonicity but retains homotopy canonicity. Cubical HoTT
72+
restores full canonicity using its explicit cubical structure. Understanding
73+
these distinctions is crucial for developing computational and proof-theoretic
74+
applications of type theory.
75+
76+
# Example of Violating Syntactic Canonicity
77+
78+
`ℕ` defined in CCHM through W, 0, 1, 2 doesn't compute numerals expressions to same terms,
79+
however they are propotionally canonical in CCHM though `hcomp`.
80+
81+
```
82+
def ℕ-ctor := ind_2 (λ (f : 𝟐), U) 𝟎 𝟏
83+
def ℕ := W (x : 𝟐), ℕ-ctor x
84+
def zero : ℕ := sup 𝟐 ℕ-ctor 0₂ (ind₀ ℕ)
85+
def succ (n : ℕ) : ℕ := sup 𝟐 ℕ-ctor 1₂ (λ (x : 𝟏), n)
86+
87+
def 𝟎⟶ℕ (C : ℕ → U) (f : 𝟎 → ℕ) : C zero → C (sup 𝟐 ℕ-ctor 0₂ f)
88+
:= transp (<i> C (sup 𝟐 ℕ-ctor 0₂ (λ (x : 𝟎), ind₀ (PathP (<_> ℕ) (ind₀ ℕ x) (f x)) x @ i))) 0
89+
90+
def 𝟏⟶ℕ (C : ℕ → U) (f : 𝟏 → ℕ) : C (succ (f ★)) → C (sup 𝟐 ℕ-ctor 1₂ f)
91+
:= transp (<i> C (sup 𝟐 ℕ-ctor 1₂ (λ (x : 𝟏), ind₁ (λ (y : 𝟏), PathP (<_> ℕ) (f ★) (f y)) (<_> f ★) x @ i))) 0
92+
93+
def ℕ-ind (C : ℕ → U) (z : C zero) (s : Π (n : ℕ), C n → C (succ n)) : Π (n : ℕ), C n
94+
:= indᵂ 𝟐 ℕ-ctor C
95+
(ind₂ (λ (x : 𝟐), Π (f : ℕ-ctor x → ℕ), (Π (b : ℕ-ctor x), C (f b)) → C (sup 𝟐 ℕ-ctor x f))
96+
(λ (f : 𝟎 → ℕ) (g : Π (x : 𝟎), C (f x)), 𝟎⟶ℕ C f z)
97+
(λ (f : 𝟏 → ℕ) (g : Π (x : 𝟏), C (f x)), 𝟏⟶ℕ C f (s (f ★) (g ★))))
98+
```
99+
100+
## The Code
101+
102+
* `ℕ-ctor` is defined as a two-point inductive type,
103+
which is essentially the structure of natural numbers,
104+
with two constructors 0 (zero) and 1 (successor).
105+
106+
* The function `ℕ` defines the type of natural numbers
107+
by recursively applying the inductive constructor
108+
`ℕ-ctor` to `W` (a parameter that will allow for recursion).
109+
110+
* `zero` defines the natural number 0, and `succ` defines the successor function,
111+
producing the next natural number.
112+
113+
* The terms `𝟎⟶ℕ` and `𝟏⟶ℕ` define the transport functions for zero and successor cases,
114+
respectively, using transposition (transp).
115+
116+
## Syntactic Canonicity
117+
118+
In the case of natural numbers through W, 0, 1, 2, this would mean that terms involving
119+
natural numbers reduce to either 0 or succ n for some n. In this case,
120+
however, the terms seem to fail syntactic canonicity because of the way
121+
they involve higher inductive types and path spaces.
122+
123+
* PathP: There is use of path types, which introduces potential non-canonical forms.
124+
For example, the ind₀ (PathP (<_> ℕ) ...) terms are path-dependent terms,
125+
where the result depends on the path between natural numbers. This creates
126+
a situation where the terms cannot necessarily be reduced directly to 0 or
127+
succ n since the path spaces themselves may involve complex terms.
128+
129+
* W: The definition of ℕ using W introduces a recursive structure.
130+
This is a higher inductive type, meaning that ℕ will involve non-canonical
131+
terms due to the nature of the recursion and the transport between
132+
different levels of the inductive structure.
133+
134+
## Failures in Canonicity
135+
136+
* Non-normalizing terms: Because of the presence of path-dependent
137+
types (PathP) and recursive definitions involving higher inductive
138+
types (like W), the terms may not always reduce to a simple form
139+
like 0 or succ n.
140+
141+
* Complexity in path spaces: The presence of path spaces (PathP)
142+
introduces a level of complexity where terms can fail to simplify
143+
to their normal form, especially if the path spaces themselves
144+
are complicated or not trivially reducible.
145+
146+
## Reformulating Canonicity for Natural Numbers
147+
148+
To reformulate canonicity for natural numbers built using this approach, consider the following:
149+
150+
1) Explicit normal forms: Instead of using higher inductive types and path
151+
spaces directly in the constructors of ℕ, you could attempt to define
152+
explicit normal forms for each level of recursion. For example, if `ℕ`
153+
is constructed inductively, the recursion should be designed to
154+
ensure that each term reduces to a canonical form (either 0 or succ n).
155+
156+
2) Defining a simplification rule: You could introduce simplification rules
157+
for the terms involving PathP and ind₂. For example, if the term involves
158+
a path between two elements of the same type, it could simplify based on
159+
the structure of that path.
160+
161+
3) Weakening of transport functions: The use of transport
162+
functions (`𝟎⟶ℕ` and `𝟏⟶ℕ`) could be streamlined or simplified,
163+
possibly by ensuring that the terms they produce are more
164+
straightforward, avoiding the creation of complex path-dependent terms.
165+
166+
4) Avoiding path dependencies in constructors: If path dependencies
167+
are introduced in terms like `ℕ-ctor` x, ensuring they do not lead
168+
to terms that require higher reductions may help maintain
169+
syntactic canonicity. This might involve constructing the natural
170+
number terms without relying on path-dependent constructs, focusing
171+
on simpler inductive rules.
172+
173+
## Conclusion
174+
175+
In summary, the failure of syntactic canonicity in the given example arises
176+
due to the complexity introduced by path types, homotopy composition, and
177+
the recursive definition via W. To reformulate it for canonicity, consider
178+
reducing the reliance on path-dependent constructions and focusing on
179+
explicit normal forms and simpler recursive definitions. Alternatively,
180+
you could introduce simplification mechanisms for the terms involving
181+
path spaces to ensure they normalize to canonical forms.
182+
183+
In the context of Constructive Cubical Higher Modalities (CCHM) and the
184+
question of preserving syntactical canonicity when expressing natural
185+
numbers (ℕ) using the type constructors W, 0, 1, and 2 (which are
186+
typically used in higher inductive type theory), there are significant
187+
challenges. However, understanding these challenges in detail can help
188+
identify potential paths to express natural numbers while preserving syntactical canonicity.
189+
190+
### Understanding the Problem with Syntactical Canonicity
191+
192+
In type theory, syntactical canonicity refers to the property that
193+
every term of a given type has a unique, reduced form (also called "normal form").
194+
This is important because it ensures that terms can be reduced deterministically
195+
and without ambiguity, which is often a crucial feature of constructive type theories.
196+
197+
When natural numbers are expressed using higher inductive
198+
types (like W in your example), path-dependent types and
199+
the recursive constructions involving homotopy (e.g., W,
200+
PathP, and ind₂) can introduce significant complexity. This
201+
complexity can lead to the failure of syntactical canonicity, because:
202+
203+
Inductive structures involving path spaces (e.g., PathP) may not reduce
204+
directly to canonical forms (like 0 or succ n) due to the presence of
205+
higher-dimensional structures.
206+
207+
Recursion using W introduces non-trivial paths and depends on how the
208+
recursion unfolds, which can result in terms that do not have simple normal forms.
209+
210+
Homotopy-theoretic aspects (like `hcomp`, `ind₂`) typically introduce more
211+
flexibility in the way terms are constructed and reduced, which makes
212+
maintaining syntactic canonicity more difficult.
213+
214+
### Can Nat in W, 0, 1, 2 Preserve Syntactical Canonicity in CCHM?
215+
216+
Expressing natural numbers (ℕ) using the approach you’ve described (via W, 0, 1,
217+
and 2 constructors) does not preserve syntactical canonicity in the standard
218+
sense within CCHM. The introduction of higher inductive types, especially
219+
the use of path-dependent terms, creates structures that do not always
220+
reduce directly to canonical forms.
221+
222+
More specifically, the failure of canonicity is often a consequence of the following:
223+
224+
Path spaces and homotopies: When W and path-dependent types are used,
225+
it introduces an extra layer of complexity, meaning terms in ℕ might
226+
reduce to non-normal forms, and paths between elements in ℕ can be non-trivial.
227+
228+
Higher inductive types: The construction of ℕ via W leads to a
229+
structure that does not admit a simple reduction to 0 or succ n.
230+
The recursion over W induces terms that involve complex higher-dimensional
231+
paths, making it hard to guarantee that each term will have a canonical form.
232+
233+
### Is This a Dead End, or Can It Be Fixed?
234+
235+
There are established results in type theory, particularly in homotopy
236+
type theory and constructive type theories, which show that the use of
237+
higher inductive types can break syntactical canonicity. In fact, this
238+
has been the subject of study, and there are theorems stating that higher
239+
inductive types generally do not preserve syntactical canonicity.
240+
241+
However, this does not mean that expressing natural numbers via W and
242+
path-dependent constructions is entirely unworkable. Instead, it means that:
243+
244+
* You may need to reconsider how you define your natural numbers
245+
and possibly avoid certain path-dependent constructions if you
246+
want to maintain syntactic canonicity.
247+
248+
* It might be possible to use simple inductive types or other definitions
249+
of ℕ that avoid the pitfalls of higher inductive types while still
250+
respecting constructive and homotopical principles.
251+
252+
* Direct inductive definition of ℕ: One way to preserve canonicity is to define
253+

‎lib/foundations/mltt/bool.anders‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
module bool where
2+
import lib/foundations/univalent/path
23
import lib/foundations/mltt/either
34
import lib/foundations/mltt/proto
45

@@ -20,3 +21,26 @@ def bool′ := Π (α : U), α → α → α
2021
def true′ : bool′ := λ (α : U) (t f : α), t
2122
def false′ : bool′ := λ (α : U) (t f : α), f
2223
def ite (α : U) (a b : α) (f : bool′) : α := f α a b
24+
25+
def th722 (A: U) (R: A -> A -> U) (r: Π(x: A), R x x) (h: Π(x y: A), isProp (R x y)) (f: Π (x y: A), R x y -> Path A x y) : isSet A
26+
:= λ (a b: A), λ (p q: Path A a b),
27+
<i j> hcomp A (∂ i ∨ ∂ j) (λ (l : I), [(i = 0) -> p @ l /\ j,
28+
(i = 1) -> q @ l /\ j,
29+
(j = 0) -> f (p @ j) (q @ j) (h (p @ j) (q @ j) (r a) (r (p @ i /\ j)) @ j) @ -l \/ -j,
30+
(j = 1) -> f a b (transp (<i> R a (q @ i)) 0 (r a)) @ l]) a
31+
32+
def cor723 (A: U) (h: Π (x y: A), ((Path A x y -> 𝟎) -> 𝟎) -> Path A x y) : isSet A
33+
:= th722 A (λ (x y: A), (Path A x y -> 𝟎) -> 𝟎) (λ (x: A) (g: Path A x x -> 𝟎), g (<i0> x))
34+
(λ(x y: A) (a b: (Path A x y -> 𝟎) -> 𝟎), <j> λ (p: Path A x y -> 𝟎), ind₀ (Path 𝟎 (a p) (b p)) (a p) @ j) h
35+
36+
def ffineqtt (h: Path 𝟐 0₂ 1₂) : 𝟎
37+
:= transp (<i> ind₂ (λ(_: 𝟐), U) 𝟎 𝟏 (h @ -i)) 0 ★
38+
39+
def boolset : isSet 𝟐
40+
:= cor723 𝟐 (ind₂ (λ (x: 𝟐), Π (y: 𝟐), ((Path 𝟐 x y -> 𝟎) ->𝟎) -> Path 𝟐 x y)
41+
(ind₂ (λ (y: 𝟐), ((Path 𝟐 0₂ y -> 𝟎) -> 𝟎) -> Path 𝟐 0₂ y)
42+
(λ (h00: ((Path 𝟐 0₂ 0₂ -> 𝟎) -> 𝟎)), <i1> 0₂)
43+
(λ (h01: ((Path 𝟐 0₂ 1₂ -> 𝟎) -> 𝟎)), ind₀ (Path 𝟐 0₂ 1₂) (h01 ffineqtt)))
44+
(ind₂ (λ (y: 𝟐), ((Path 𝟐 1₂ y -> 𝟎) ->𝟎) -> Path 𝟐 1₂ y)
45+
(λ (h10: ((Path 𝟐 1₂ 0₂ -> 𝟎) -> 𝟎)), ind₀ (Path 𝟐 1₂ 0₂) (h10 (λ (g: Path 𝟐 1₂ 0₂), ffineqtt (<l> g @ -l))))
46+
(λ (h11: ((Path 𝟐 1₂ 1₂ -> 𝟎) -> 𝟎)), <j> 1₂)))

‎lib/foundations/mltt/sigma.anders‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ def Σ-ind (A : U) (B : A -> U) (C : Π (s: Σ (x: A), B x), U)
2525
def ac (A B: U) (R: A -> B -> U) (g: Π (x: A), Σ (y: B), R x y)
2626
: Σ (f: A -> B), Π (x: A), R x (f x) := (\(i:A),(g i).1,\(j:A),(g j).2)
2727

28-
def total (A:U) (B C : A -> U) (f : Π (x:A), B x -> C x) (w: Σ(x: A), B x)
28+
def total-space (A:U) (B C : A -> U) (f : Π (x:A), B x -> C x) (w: Σ(x: A), B x)
2929
: Σ (x: A), C x := (w.1,f (w.1) (w.2))
3030

3131
def funDepTr (A: U) (P: A -> U) (a0 a1: A) (p: PathP (<_>A) a0 a1) (u0: P a0) (u1: P a1)

‎lib/foundations/univalent/path.anders‎

Lines changed: 13 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -357,44 +357,27 @@ def hcomp-Path-is-correct (A : U) (v w : A) (r : I) (u : I → Partial (Path A v
357357
: Path (Path A v w) (hcomp-Path A v w r u u₀) (hcomp-Path′ A v w r u u₀)
358358
:= <_> hcomp-Path A v w r u u₀
359359

360-
--- Id functions
360+
--- Id functions and Propositional Canonicity
361+
362+
def idfun (A : U) : A → A := λ (a : A), a
363+
def idfun′ (A : U) : A → A := λ (a : A), transp (<i> A) 0 a
364+
def idfun″ (A : U) : A → A := λ (a : A), hcomp A 0 (λ (i : I), []) a
361365

362366
def transp′ (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I), A]]) := λ (x: A), x
363367
def transp′′ (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I), A]]) := transp (<i> (ouc p) i) j
364368
def transp′′′ (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I), A]]) := transp (<i> (λ (_ : I), A) i) j
365369

366-
def idfun (A : U) : A → A := λ (a : A), a
367-
def idfun′ (A : U) : A → A := λ (a : A), transp (<i> A) 0 a
368-
def idfun″ (A : U) : A → A := λ (a : A), hcomp A 0 (λ (i : I), []) a
370+
def idfun=idfun′ (A : U) : Path (A → A) (idfun A) (idfun′ A)
371+
:= <i> transp (<_> A) -i
372+
373+
def idfun=idfun″ (A : U) : Path (A → A) (idfun A) (idfun″ A)
374+
:= <i> λ (a : A), hcomp A -i (λ (j : I), [(i = 0) → a]) a
369375

370-
def idfun=idfun′ (A : U) : Path (A → A) (idfun A) (idfun′ A) := <i> transp (<_> A) -i
371-
def idfun=idfun″ (A : U) : Path (A → A) (idfun A) (idfun″ A) := <i> λ (a : A), hcomp A -i (λ (j : I), [(i = 0) → a]) a
372376
def idfun′=idfun″ (A : U) : Path (A → A) (idfun′ A) (idfun″ A)
373377
:= comp-Path (A → A) (idfun′ A) (idfun A) (idfun″ A) (<i> idfun=idfun′ A @ -i) (idfun=idfun″ A)
374378

375-
def 𝟏-contr : Π (x : 𝟏), Path 𝟏 x ★ := ind₁ (λ (x : 𝟏), Path 𝟏 x ★) (<_> ★)
379+
def 𝟏-contr : Π (x : 𝟏), Path 𝟏 x ★
380+
:= ind₁ (λ (x : 𝟏), Path 𝟏 x ★) (<_> ★)
381+
376382
def contr-impl-prop (A : U) (H : isContr A) : isProp A
377383
:= λ (a b : A), <i> hcomp A (∂ i) (λ (j : I), [(i = 0) → H.2 a @ j, (i = 1) → H.2 b @ j]) H.1
378-
379-
def th722 (A: U) (R: A -> A -> U) (r: Π(x: A), R x x) (h: Π(x y: A), isProp (R x y)) (f: Π (x y: A), R x y -> Path A x y) : isSet A
380-
:= λ (a b: A), λ (p q: Path A a b),
381-
<i j> hcomp A (∂ i ∨ ∂ j) (λ (l : I), [(i = 0) -> p @ l /\ j,
382-
(i = 1) -> q @ l /\ j,
383-
(j = 0) -> f (p @ j) (q @ j) (h (p @ j) (q @ j) (r a) (r (p @ i /\ j)) @ j) @ -l \/ -j,
384-
(j = 1) -> f a b (transp (<i> R a (q @ i)) 0 (r a)) @ l]) a
385-
386-
def cor723 (A: U) (h: Π (x y: A), ((Path A x y -> 𝟎) -> 𝟎) -> Path A x y) : isSet A
387-
:= th722 A (λ (x y: A), (Path A x y -> 𝟎) -> 𝟎) (λ (x: A) (g: Path A x x -> 𝟎), g (<i0> x))
388-
(λ(x y: A) (a b: (Path A x y -> 𝟎) -> 𝟎), <j> λ (p: Path A x y -> 𝟎), ind₀ (Path 𝟎 (a p) (b p)) (a p) @ j) h
389-
390-
def ffineqtt (h: Path 𝟐 0₂ 1₂) : 𝟎
391-
:= transp (<i> ind₂ (λ(_: 𝟐), U) 𝟎 𝟏 (h @ -i)) 0 ★
392-
393-
def boolset : isSet 𝟐
394-
:= cor723 𝟐 (ind₂ (λ (x: 𝟐), Π (y: 𝟐), ((Path 𝟐 x y -> 𝟎) ->𝟎) -> Path 𝟐 x y)
395-
(ind₂ (λ (y: 𝟐), ((Path 𝟐 0₂ y -> 𝟎) -> 𝟎) -> Path 𝟐 0₂ y)
396-
(λ (h00: ((Path 𝟐 0₂ 0₂ -> 𝟎) -> 𝟎)), <i1> 0₂)
397-
(λ (h01: ((Path 𝟐 0₂ 1₂ -> 𝟎) -> 𝟎)), ind₀ (Path 𝟐 0₂ 1₂) (h01 ffineqtt)))
398-
(ind₂ (λ (y: 𝟐), ((Path 𝟐 1₂ y -> 𝟎) ->𝟎) -> Path 𝟐 1₂ y)
399-
(λ (h10: ((Path 𝟐 1₂ 0₂ -> 𝟎) -> 𝟎)), ind₀ (Path 𝟐 1₂ 0₂) (h10 (λ (g: Path 𝟐 1₂ 0₂), ffineqtt (<l> g @ -l))))
400-
(λ (h11: ((Path 𝟐 1₂ 1₂ -> 𝟎) -> 𝟎)), <j> 1₂)))

0 commit comments

Comments
 (0)