diff --git a/assets/sass/_content.scss b/assets/sass/_content.scss
index 2db3e32..e16130a 100644
--- a/assets/sass/_content.scss
+++ b/assets/sass/_content.scss
@@ -1,5 +1,7 @@
@import "footer";
+$breakpoint: 720px;
+
html {
min-height: 100vh;
margin: 0;
@@ -68,7 +70,8 @@ footer {
.side-nav .side-nav-content {
display: flex;
- justify-content: space-evenly;
+ justify-content: center;
+ gap: 20px;
.me {
display: flex;
@@ -91,7 +94,7 @@ footer {
}
}
-@media screen and (max-width: 672px) {
+@media screen and (max-width: $breakpoint) {
.flex-wrapper {
flex-direction: column;
.container {
@@ -116,6 +119,7 @@ footer {
.portrait {
max-height: 80px;
}
+
.bio {
display: none;
}
@@ -123,7 +127,7 @@ footer {
}
}
-@media screen and (min-width: 672px) {
+@media screen and (min-width: $breakpoint) {
.flex-wrapper {
flex-direction: row;
.container {
@@ -137,7 +141,8 @@ footer {
left: 0;
top: 0;
// Capital Min to avoid invoking SCSS min
- max-width: Min(30%, 30em);
+ width: 30%;
+ min-width: 300px;
.side-nav-content {
padding-top: 32px;
diff --git a/blog.agda-lib b/blog.agda-lib
index feecedb..74c74f3 100644
--- a/blog.agda-lib
+++ b/blog.agda-lib
@@ -1,3 +1,3 @@
name: blog
-depend: standard-library
+depend: standard-library cubical
include: content/posts
diff --git a/content/posts/2023-02-04-proving-true-from-false.lagda.md b/content/posts/2023-02-04-proving-true-from-false.lagda.md
new file mode 100644
index 0000000..c08e2b3
--- /dev/null
+++ b/content/posts/2023-02-04-proving-true-from-false.lagda.md
@@ -0,0 +1,75 @@
++++
+title = "Proving true from false"
+slug = "proving-true-from-false"
+date = 2023-02-04
+tags = ["type-theory"]
+math = true
+draft = true
++++
+
+
+Imports
+
+These are some imports that are required for code on this page to work properly.
+
+```agda
+{-# OPTIONS --cubical #-}
+
+open import Cubical.Foundations.Prelude
+open import Data.Bool
+open import Data.Unit
+open import Data.Empty
+
+¬_ : Set → Set
+¬ A = A → ⊥
+
+_≢_ : ∀ {A : Set} → A → A → Set
+x ≢ y = ¬ (x ≡ y)
+```
+
+
+Let's say you wanted to prove that `true` and `false` diverge, a.k.a are not
+equal to each other. In a theorem prover like Agda, you could write this
+statement as something like this:
+
+```
+true≢false : true ≢ false
+```
+
+For many "obvious" statements, it suffices to just write `refl` since the two
+sides are trivially true via rewriting. For example:
+
+```
+open import Data.Nat
+1+2≡3 : 1 + 2 ≡ 3
+1+2≡3 = refl
+```
+
+However, in cubical Agda, this following statement doesn't work. I've commented
+it out so the code on this page can continue to compile.
+
+```
+-- true≢false = refl
+```
+
+It looks like it's not obvious to the interpreter that this statement is
+actually true. Why is this?
+
+Well, in homotopy type theory, TODO
+
+The strategy here is we define some kind of "type-map". Every time we see true,
+we'll map it to some type, and every time we see false, we'll map it to empty.
+
+Because the `≢` type actually means "having `a ≡ b` can produce `⊥`", all we
+need to do is to produce an empty type. To do this, we need to do something
+called _transport_.
+
+In homotopy type theory, is a way of generating functions out of paths.
+
+```
+bool-map : Bool → Type
+bool-map true = ⊤
+bool-map false = ⊥
+
+true≢false p = transport (λ i → bool-map (p i)) tt
+```
diff --git a/layouts/_default/baseof.html b/layouts/_default/baseof.html
index 55409e2..79727e4 100644
--- a/layouts/_default/baseof.html
+++ b/layouts/_default/baseof.html
@@ -10,6 +10,7 @@
{{ if .IsHome }}
+
{{ end }}
{{ $style := resources.Get "sass/main.scss" | resources.ToCSS }}
diff --git a/layouts/partials/left-nav.html b/layouts/partials/left-nav.html
index 6541592..b274879 100644
--- a/layouts/partials/left-nav.html
+++ b/layouts/partials/left-nav.html
@@ -13,6 +13,7 @@
{{ end }}
+