Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Remove undercore from refl constructor to avoid KaTeX errors

Browse Source
This commit is contained in:
Danila Fedorin 2021-11-28 19:34:57 -08:00
parent 2ce351f7ef
commit 1c93d28441
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
content/blog/coq_dawn_eval.md
View File

@ -20,7 +20,7 @@ allows for the case in which the exact same expression is a value for two differ
reasons. Although `IsValue` has only one constructor (`Val_quote`), it's actually reasons. Although `IsValue` has only one constructor (`Val_quote`), it's actually
{{< sidenote "right" "hott-note" "not provable" >}} {{< sidenote "right" "hott-note" "not provable" >}}
Interestingly, it's also not provable that any two proofs of \(a = b\) are equal, Interestingly, it's also not provable that any two proofs of \(a = b\) are equal,
even though equality only has one constructor, \(\text{eq_refl}\ :\ a \rightarrow (a = a) \). even though equality only has one constructor, \(\text{refl}\ :\ a \rightarrow (a = a) \).
Under the <a href="https://homotopytypetheory.org/book/">homotopic interpretation</a> Under the <a href="https://homotopytypetheory.org/book/">homotopic interpretation</a>
of type theory, this corresponds to the fact that two paths from \(a\) to \(b\) need of type theory, this corresponds to the fact that two paths from \(a\) to \(b\) need
not be homotopic (continuously deformable) to each other.<br> not be homotopic (continuously deformable) to each other.<br>