From 96fa436b29c8a5dff13a741f2b09b851497df7c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=D0=9C=D0=B0=D0=BA=D1=81=D0=B8=D0=BC=20=D0=A1=D0=BE=D1=85?= =?UTF-8?q?=D0=B0=D1=86=D1=8C=D0=BA=D0=B8=D0=B9?= Date: Wed, 19 Feb 2025 21:36:23 +0200 Subject: [PATCH] Update REAMDE.md --- intro/canonicity/REAMDE.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/intro/canonicity/REAMDE.md b/intro/canonicity/REAMDE.md index b67b841..0382681 100644 --- a/intro/canonicity/REAMDE.md +++ b/intro/canonicity/REAMDE.md @@ -242,6 +242,8 @@ paths, making it hard to guarantee that each term will have a canonical form. ### Is This a Dead End, or Can It Be Fixed? +It is a dead and and can be fixed! + There are established results in type theory, particularly in homotopy type theory and constructive type theories, which show that the use of higher inductive types can break syntactical canonicity. In fact, this