From 1c93d2844192eb22fba714b5a09677dfeb19c6fa Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 28 Nov 2021 19:34:57 -0800 Subject: [PATCH] Remove undercore from refl constructor to avoid KaTeX errors --- content/blog/coq_dawn_eval.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/blog/coq_dawn_eval.md b/content/blog/coq_dawn_eval.md index 6153692..8a7d780 100644 --- a/content/blog/coq_dawn_eval.md +++ b/content/blog/coq_dawn_eval.md @@ -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 {{< sidenote "right" "hott-note" "not provable" >}} 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 homotopic interpretation of type theory, this corresponds to the fact that two paths from \(a\) to \(b\) need not be homotopic (continuously deformable) to each other.