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.