michael/blog
1
0
Fork 0
Code Issues 2 Pull requests Releases Packages 1 Wiki Activity

time to bury this forever

Browse source
This commit is contained in:
Michael Zhang 2023-09-21 17:40:43 -05:00
parent 328680c54b
commit 263ed46253
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/content/posts/2023-09-15-equality.md
View file

@ -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 $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 > - 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 > defined in type systems: $2 \equiv s(s(z))$. If somewhere before this, you
> identical. > 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 > - 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 > β-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 > choice of the type theory designer; if you wanted a more intensional type
> theory, you could choose to not allow β-reduction during evaluation of > theory, you could choose to not allow β-reduction during evaluation of
> identities. Most type theories _do_ allow this though. > 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 - **Propositional** equality. This describes a _value_ that potentially holds
true or false. This is typically written $=$ in math. 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/definitional+equality
- https://ncatlab.org/nlab/show/judgment - https://ncatlab.org/nlab/show/judgment
- https://ncatlab.org/nlab/show/judgmental+equality - https://ncatlab.org/nlab/show/judgmental+equality
- https://ncatlab.org/nlab/show/propositional+equality
- https://hott.github.io/book/hott-ebook.pdf.html - https://hott.github.io/book/hott-ebook.pdf.html

3
src/styles/_colors.scss
View file

@ -41,6 +41,7 @@
$backgroundColor: #202030; $backgroundColor: #202030;
$textColor: #cdcdcd; $textColor: #cdcdcd;
$linkColor: lightskyblue; $linkColor: lightskyblue;
$linkHoverColor: #202749;
:root { :root {
--background-color: #{$backgroundColor}; --background-color: #{$backgroundColor};
@ -53,7 +54,7 @@
--faded: #666; --faded: #666;
--hr-color: gray; --hr-color: gray;
--link-color: #{$linkColor}; --link-color: #{$linkColor};
--link-hover-color: #{darken($linkColor, 60%)}; --link-hover-color: #{$linkHoverColor};
--code-color: #{lighten(firebrick, 25%)}; --code-color: #{lighten(firebrick, 25%)};
--tag-color: #{darken($linkColor, 55%)}; --tag-color: #{darken($linkColor, 55%)};