From 263ed462531df56321da91f97263589527e2420b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 21 Sep 2023 17:40:43 -0500
Subject: [PATCH] time to bury this forever

---
 src/content/posts/2023-09-15-equality.md | 9 +++++++--
 src/styles/_colors.scss                  | 3 ++-
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/content/posts/2023-09-15-equality.md b/src/content/posts/2023-09-15-equality.md
index 40ba312..0cbabb2 100644
--- a/src/content/posts/2023-09-15-equality.md
+++ b/src/content/posts/2023-09-15-equality.md
@@ -23,13 +23,17 @@ to, since they're very different concepts.
   >
   > - Does $2$ equal $2$? Yes. This is the same object, and equality is reflexive.
   > - Does $s(s(z))$ equal $2$? Well, typically this is how natural numbers are
-  >   defined in type systems: $2 \equiv s(s(z))$. _By definition_ they are
-  >   identical.
+  >   defined in type systems: $2 \equiv s(s(z))$. If somewhere before this, you
+  >   said "let $2$ equal $s(s(z))$", then _by definition_ these are identical.
   > - Does $1 + 1$ equal $2$? The operation $+$ is a function, and requires a
   >   &beta;-reduction to evaluate any further. This choice really comes down to the
   >   choice of the type theory designer; if you wanted a more intensional type
   >   theory, you could choose to not allow &beta;-reduction during evaluation of
   >   identities. Most type theories _do_ allow this though.
+  > - Does $x = y$ for any $x$ and $y$?
+  >
+  > As far as I understand, you can choose whatever to _be_ your "definitional"
+  > equality,
 
 - **Propositional** equality. This describes a _value_ that potentially holds
   true or false. This is typically written $=$ in math.
@@ -114,4 +118,5 @@ in your language too. In Agda, it's `Path {A} x y`.
 - https://ncatlab.org/nlab/show/definitional+equality
 - https://ncatlab.org/nlab/show/judgment
 - https://ncatlab.org/nlab/show/judgmental+equality
+- https://ncatlab.org/nlab/show/propositional+equality
 - https://hott.github.io/book/hott-ebook.pdf.html
diff --git a/src/styles/_colors.scss b/src/styles/_colors.scss
index 7eb4af9..94c67e7 100644
--- a/src/styles/_colors.scss
+++ b/src/styles/_colors.scss
@@ -41,6 +41,7 @@
   $backgroundColor: #202030;
   $textColor: #cdcdcd;
   $linkColor: lightskyblue;
+  $linkHoverColor: #202749;
 
   :root {
     --background-color: #{$backgroundColor};
@@ -53,7 +54,7 @@
     --faded: #666;
     --hr-color: gray;
     --link-color: #{$linkColor};
-    --link-hover-color: #{darken($linkColor, 60%)};
+    --link-hover-color: #{$linkHoverColor};
     --code-color: #{lighten(firebrick, 25%)};
     --tag-color: #{darken($linkColor, 55%)};