diff --git a/src/content/posts/2023-09-15-equality.md b/src/content/posts/2023-09-15-equality.md
new file mode 100644
index 0000000..40ba312
--- /dev/null
+++ b/src/content/posts/2023-09-15-equality.md
@@ -0,0 +1,117 @@
+---
+title: Equality
+date: 2023-09-15T05:36:53.757Z
+tags:
+ - type-theory
+draft: true
+---
+
+When learning type theory, it's important to make a distinction between several
+kinds of "same"-ness. Whenever you talk about two things being equal, you'd want
+to qualify it with one of these in order to make it clear which you're referring
+to, since they're very different concepts.
+
+- **Definitional**, or **judgmental** equality. This is usually written with
+ $\equiv$ in math. If you see $x \equiv y$, this says "I've defined $x$ and $y$
+ to be the same, so anytime you see $x$, you can replace it with $y$ and vice
+ versa."
+
+ > [!NOTE]
+ > Technically speaking, definitional and judgmental are two separate concepts
+ > but coincide in many type theories. You could think of multiple levels of
+ > equalities like this:
+ >
+ > - 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.
+ > - Does $1 + 1$ equal $2$? The operation $+$ is a function, and requires a
+ > β-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 β-reduction during evaluation of
+ > identities. Most type theories _do_ allow this though.
+
+- **Propositional** equality. This describes a _value_ that potentially holds
+ true or false. This is typically written $=$ in math.
+
+## Helpful tips
+
+- You can talk about propositional equalities conditionally, like "if $a$ equals
+ $b$, then $c$ is true". This kind of expression doesn't really make sense for
+ judgmental equality, like in the following example:
+
+ Suppose you made the judgment: $x = 2$. It makes no sense to then say "if $x$
+ equals $2$, then $c$ is true." You can just skip right to $c$ is true, because
+ you've defined it to be true, so it's useless even thinking about
+ the case where it's false because that would be a part of a completely
+ different world entirely.
+
+- Here's a concrete example of the difference between judgmental and
+ propositional equality. Consider these 2 expressions:
+
+ - $2 + 3 = 3 + 2$
+ - $\forall x\ y \in \mathbb{N} . (x + y = y + x)$
+
+ In the first case, performing β-reduction on both terms reduces to $5 =
+ 5$, which is definitionally equal by virtue of being the exact same symbol.
+
+ In the second case however, β-reduction is impossible. Without a specific
+ $x$ or $y$, there's actually no way to reduce either side more. You would need
+ some other constructs to prove it, such as induction.
+
+- Suppose you were expressing these concepts in a language like TypeScript. The
+ analog of a judgment would be something like:
+
+ ```ts
+ type Foo = string;
+ ```
+
+ Any time you're using `Foo`, you really don't have to compare it with
+ `string`, because just through a simple substitution you will get the same
+ symbol:
+
+ ```
+ function sayHello(who: string) { console.log(`Hello, ${who}`); }
+ function run(foo: Foo) { sayHello(foo); }
+ ```
+
+ On the other hand, a propositional equality type might look something like
+ this instead:
+
+ ```ts
+ class Equal {
+ private constructor() {}
+ static refl(): Equal {}
+ }
+ ```
+
+ You could have a value of this type, and query on its truthiness:
+
+ ```ts
+ type TwoEqualsTwo = Equal;
+
+ function trans(x: Equal, y: Equal): Equal {
+ // magic...
+ }
+ ```
+
+## Notation gotcha
+
+The syntax we use in most math papers and other literature and the syntax we use
+for equalities in various dependently-typed programming languages are annoyingly
+different:
+
+| | Math | Agda | Coq | Idris |
+| ------------- | ------------ | ------- | -------- | ------- |
+| Judgmental | $x \equiv y$ | `x = y` | `x := y` | `x = y` |
+| Propositional | $x = y$ | `x ≡ y` | `x = y` | `x = y` |
+
+Usually there'll be some other pre-fix way of writing the propositional equals
+in your language too. In Agda, it's `Path {A} x y`.
+
+## More reading
+
+- https://ncatlab.org/nlab/show/definitional+equality
+- https://ncatlab.org/nlab/show/judgment
+- https://ncatlab.org/nlab/show/judgmental+equality
+- https://hott.github.io/book/hott-ebook.pdf.html
diff --git a/src/styles/_colors.scss b/src/styles/_colors.scss
index 77f94b7..7eb4af9 100644
--- a/src/styles/_colors.scss
+++ b/src/styles/_colors.scss
@@ -18,6 +18,10 @@
--code-color: firebrick;
--tag-color: #{lighten($linkColor, 35%)};
+ // Admonition
+ --note-color: #{$linkColor};
+ --note-background-color: var(--link-hover-color);
+
// Syntax Highlighting
--astro-code-color-text: #24292e;
--astro-code-color-background: inherit;
@@ -53,6 +57,10 @@
--code-color: #{lighten(firebrick, 25%)};
--tag-color: #{darken($linkColor, 55%)};
+ // Admonition
+ --note-color: #{$linkColor};
+ --note-background-color: var(--link-hover-color);
+
// Syntax Highlighting
--astro-code-color-text: #e1e4e8;
--astro-code-color-background: inherit;
diff --git a/src/styles/post.scss b/src/styles/post.scss
index 05d9939..d04976f 100644
--- a/src/styles/post.scss
+++ b/src/styles/post.scss
@@ -39,6 +39,11 @@
display: none;
}
+ p,
+ ul {
+ margin-block: 12px;
+ }
+
p > img {
max-width: 100%;
height: auto;
@@ -250,17 +255,27 @@ hr.endline {
.admonition {
// TODO: Figure out how to distinguish admonitions
- --color: var(--link-color);
+ --admonition-color: var(--note-color);
- border-left: 4px solid var(--color);
- padding-left: 8px;
+ background-color: var(--note-background-color);
+ border-left: 4px solid var(--admonition-color);
+ padding: 8px;
font-size: 0.9rem;
+ border-radius: 8px;
.admonition-title {
- color: var(--color);
+ color: var(--admonition-color);
}
p {
margin: 8px auto;
}
+
+ :first-child {
+ margin-top: 0;
+ }
+
+ :last-child {
+ margin-bottom: 0;
+ }
}