Skip to content

Commit

Permalink
Update REAMDE.md
Browse files Browse the repository at this point in the history
  • Loading branch information
5HT authored Feb 19, 2025
1 parent 6e1e874 commit 96fa436
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions intro/canonicity/REAMDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 96fa436

Please sign in to comment.