diff --git a/.gitignore b/.gitignore
index 51e8812..ac7ca6e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,4 @@
.hugo_build.lock
.direnv
+*.agdai
diff --git a/Justfile b/Justfile
index 2167372..491ab13 100644
--- a/Justfile
+++ b/Justfile
@@ -1,2 +1,5 @@
serve:
hugo serve --bind 0.0.0.0 --buildDrafts
+
+linkcheck:
+ wget --spider -r -nd -nv -H -l 1 http://localhost:1313
diff --git a/assets/sass/_content.scss b/assets/sass/_content.scss
index 168bc83..d2e4d10 100644
--- a/assets/sass/_content.scss
+++ b/assets/sass/_content.scss
@@ -1,4 +1,4 @@
-// @import "home";
+@import "footer";
html {
min-height: 100vh;
diff --git a/assets/sass/_footer.scss b/assets/sass/_footer.scss
new file mode 100644
index 0000000..30f5ebd
--- /dev/null
+++ b/assets/sass/_footer.scss
@@ -0,0 +1,3 @@
+footer {
+ font-size: 0.85rem;
+}
diff --git a/blog.agda-lib b/blog.agda-lib
new file mode 100644
index 0000000..feecedb
--- /dev/null
+++ b/blog.agda-lib
@@ -0,0 +1,3 @@
+name: blog
+depend: standard-library
+include: content/posts
diff --git a/content/about/_index.md b/content/about/_index.md
index 455b973..f602c53 100644
--- a/content/about/_index.md
+++ b/content/about/_index.md
@@ -7,36 +7,62 @@ type = "generic"
layout = "single"
+++
-Hi there! I'm an incoming graduate student at the University of Minnesota. I
-currently work as a Software Developer at [AWS][13] (previously at [SIFT][11]). My
-computing-related interests lie in programming language design and formal
-verification, systems security, cryptography, and distributed systems. Some of the projects I've been working on in my free time include:
+# About Me
-- [**Leanshot**][6], a Linux screen capture tool.
-- [**Garbage**][7], a CLI interface to the trash can API.
+Hi there! I'm a first-year master's student at the University of Minnesota. I
+also currently work as a Software Developer at [AWS] (previously at [SIFT]).
+My computing-related interests lie in programming language design and formal
+verification, systems security, cryptography, and distributed
+systems.
+
+
+
+### Research
+
+Currently, I'm learning about [cubical type theory][cubical]. I'll probably
+write some blog posts as I learn more. My advisor is [Favonia].
+
+### University Involvement
+
+- **[GopherHack]**. I'm an officer at the GopherHack organization, hoping to
+ grow a CTF community at the University.
+- **[PL Seminar]**. A group focused on reading and discussing
+ programming-language-related papers
+
+### Open-source Projects
+
+Some of the projects I've been working on in my free time include:
+
+- **[Leanshot]**. A Linux screen capture tool.
+- **[Garbage]**. A CLI interface to the trash can API.
More can be found on [this page][12] or my public [Gitea][2].
-I've also started making an increased effort at using and supporting [FOSS][8],
+I've also started making an increased effort at using and supporting [FOSS],
and other software that're not predatory towards users. As a part of this
effort, I'm also self-hosting and rewriting some of the services and software
that I use regularly. Find out what I'm using [here][9].
-I'm also an avid rhythm game player and beatmap creator, mostly involved with
-the free-to-play game [osu!][3]. Check out some of my beatmaps on my [osu!
-userpage][4].
+### Hobbies
+
+I'm also an avid rhythm game player and beatmap creator, mostly involved with
+the free-to-play game [osu!]. Check out some of my beatmaps on my osu!
+[userpage].
+
+I also enjoy playing badminton 🏸 at the rec.
-[1]: https://keybase.io/michaelz/pgp_keys.asc?fingerprint=925ecc02890d5cdae26180d4bda47a31a3c8ee6b
[2]: https://git.mzhang.io/explore
-[3]: https://osu.ppy.sh
-[4]: https://osu.ppy.sh/u/2688103
-[5]: https://libera.chat
-[6]: https://git.mzhang.io/michael/leanshot
-[7]: https://git.sr.ht/~iptq/garbage
-[8]: https://en.wikipedia.org/wiki/Free_and_open-source_software
[9]: setup
[10]: pgp.txt
-[11]: https://www.sift.net/
[12]: ../projects
-[13]: https://aws.amazon.com/
+[aws]: https://aws.amazon.com/
+[cubical]: https://ncatlab.org/nlab/show/cubical+type+theory
+[favonia]: https://favonia.org/
+[foss]: https://en.wikipedia.org/wiki/Free_and_open-source_software
+[garbage]: https://git.sr.ht/~mzhang/garbage
+[gopherhack]: https://gopherhack.com
+[leanshot]: https://git.sr.ht/~mzhang/leanshot
+[osu!]: https://osu.ppy.sh
+[pl seminar]: https://umn-plseminar.github.io
+[sift]: https://www.sift.net/
+[userpage]: https://osu.ppy.sh/u/2688103
diff --git a/content/posts/2022-09-20-higher-inductive-types.lagda.md b/content/posts/2022-09-20-higher-inductive-types.lagda.md
new file mode 100644
index 0000000..9539639
--- /dev/null
+++ b/content/posts/2022-09-20-higher-inductive-types.lagda.md
@@ -0,0 +1,189 @@
++++
+title = "Higher Inductive Types"
+slug = "higher-inductive-types"
+date = 2022-09-20
+tags = ["type-theory"]
+toc = true
+math = true
+draft = true
++++
+
+**Higher inductive types (HIT)** are central to developing cubical type theory.
+What this article will try to do is develop an approach to understanding higher
+inductive types based on my struggles to learn the topic.
+
+
+
+Ordinary inductive types
+---
+
+So first off, what is an inductive type? These are a kind of data structure
+that's commonly used in _functional programming_. For example, consider the
+definition of natural numbers (`Nat`):
+
+```agda
+data Nat : Set where
+ zero : Nat
+ suc : Nat → Nat
+```
+
+This defines all `Nat`s as either zero, or one more than another `Nat`. For
+example, here's the first few natural numbers and their corresponding
+representation using this data structure:
+
+```txt
+0 zero
+1 suc zero
+2 suc (suc zero)
+3 suc (suc (suc zero))
+4 suc (suc (suc (suc zero)))
+5 suc (suc (suc (suc (suc zero))))
+```
+
+Why is this representation useful? Well, if you remember **proof by induction**
+from maybe high school geometry, you'll recall that we can prove things about
+all natural numbers by simply proving that it's true for the _base case_ 0, and
+then proving that it's true for any _inductive case_ $n$, given that the
+previous case $n - 1$ is true.
+
+This kind of definition of natural numbers makes this induction structure much
+more clear. For example, look at the definition of a tree:
+
+```agda
+data Tree (A : Set) : Set where
+ leaf : A → Tree A
+ left : Tree A → Tree A
+ right : Tree A → Tree A
+```
+
+We can do induction on trees by simply proving it's true for (1) the base case,
+(2) the left case, and (3) the right case. In fact, all inductive data
+structures have this kind of induction principle. So say you wanted to prove
+that $1 + 2 + 3 + \cdots + n = \frac{n\cdot(n+1)}{2}$ for all $n \in
+\mathbb{N}$, then you could say:
+
+
+(click here for boring requisites)
+
+```agda
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; module ≡-Reasoning)
+open ≡-Reasoning using (begin_; _≡⟨_⟩_; _≡⟨⟩_; step-≡; _∎)
+open import Data.Product using (_×_)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Nat.DivMod using (_/_; 0/n≡0; n/n≡1; m*n/n≡m)
+open import Data.Nat.Properties using (+-assoc; *-identityˡ; *-comm; *-distribʳ-+; +-comm)
+
+sum-to-n : ℕ → ℕ
+sum-to-n zero = zero
+sum-to-n (suc x) = (suc x) + (sum-to-n x)
+
+distrib-/ : ∀ (a b c : ℕ) → a / c + b / c ≡ (a + b) / c
+distrib-/ zero b c =
+ begin
+ zero / c + b / c
+ ≡⟨ cong (_+ b / c) (0/n≡0 c) ⟩
+ b / c
+ ≡⟨ cong (_/ c) refl ⟩
+ (zero + b) / c
+ ∎
+distrib-/ (suc a) b c =
+ begin
+ (1 + a) / c + b / c
+ ≡⟨ cong (_+ b / c) (sym (distrib-/ 1 a c)) ⟩
+ 1 / c + a / c + b / c
+ ≡⟨ +-assoc (1 / c) (a / c) (b / c) ⟩
+ 1 / c + (a / c + b / c)
+ ≡⟨ cong (1 / c +_) (distrib-/ a b c) ⟩
+ 1 / c + (a + b) / c
+ ≡⟨ distrib-/ 1 (a + b) c ⟩
+ (suc a + b) / c
+ ∎
+```
+
+
+
+```agda
+-- Here's the proposition we want to prove:
+our-prop : ∀ (n : ℕ) → sum-to-n n ≡ n * (n + 1) / 2
+
+-- How do we prove this?
+-- Well, we know it's true for zero:
+base-case : sum-to-n 0 ≡ 0 * (0 + 1) / 2
+base-case = refl
+
+-- The next part is proving that it's true for any n + 1, given that it's true
+-- for the previous case n:
+inductive-case : ∀ {n : ℕ}
+ → (inductive-hypothesis : sum-to-n n ≡ n * (n + 1) / 2)
+ → sum-to-n (suc n) ≡ (suc n) * (suc n + 1) / 2
+```
+
+
+Inductive case proof, expand if you're interested
+
+```agda
+inductive-case {n} p =
+ begin
+ sum-to-n (suc n)
+ ≡⟨⟩ -- Expanding definition of sum-to-n
+ suc n + sum-to-n n
+ ≡⟨ cong (suc n +_) p ⟩ -- Substituting the previous case
+ suc n + n * (n + 1) / 2
+ ≡⟨ cong (_+ n * (n + 1) / 2) (sym (m*n/n≡m (suc n) 2)) ⟩
+ (suc n * 2) / 2 + (n * (n + 1)) / 2
+ ≡⟨ distrib-/ (suc n * 2) (n * (n + 1)) 2 ⟩
+ (suc n * 2 + n * (n + 1)) / 2
+ ≡⟨ cong (_/ 2) (cong (_+ n * (n + 1)) (*-comm (suc n) 2)) ⟩
+ (2 * suc n + n * (n + 1)) / 2
+ ≡⟨ cong (_/ 2) (cong (2 * suc n +_) (cong (n *_) (+-comm n 1))) ⟩
+ (2 * suc n + n * suc n) / 2
+ ≡⟨ cong (_/ 2) (sym (*-distribʳ-+ (suc n) 2 n)) ⟩
+ (1 + suc n) * suc n / 2
+ ≡⟨ cong (_/ 2) (cong (_* suc n) (+-comm 1 (suc n))) ⟩
+ (suc n + 1) * suc n / 2
+ ≡⟨ cong (_/ 2) (*-comm (suc n + 1) (suc n)) ⟩
+ (suc n) * (suc n + 1) / 2
+ ∎
+```
+
+
+
+So now that we have both the base and inductive cases, let's combine it using
+this:
+
+```agda
+-- Given any natural number property (p : ℕ → Set), if...
+any-nat-prop : (p : ℕ → Set)
+ -- ...it's true for the base case and...
+ → p 0
+ -- ...it's true for the inductive case...
+ → (∀ {n : ℕ} (a : p n) → p (suc n))
+ -- ...then the property is true for all naturals.
+ → (∀ (n : ℕ) → p n)
+any-nat-prop p base _ zero = base
+any-nat-prop p base ind (suc n) = ind (any-nat-prop p base ind n)
+```
+
+Then:
+
+```
+our-prop = any-nat-prop
+ (λ n → sum-to-n n ≡ n * (n + 1) / 2)
+ base-case inductive-case
+```
+
+Using Agda, we can see that this type-checks correctly.
+
+**TODO:** Ensure totality
+
+Higher inductive types
+---
+
+Moving on, we want to know what _higher_ inductive types brings to the table. To
+illustrate its effect, let's consider the following scenario: suppose you have
+
+#### References
+
+- [nLab](https://ncatlab.org/nlab/show/higher+inductive+type)
+- Section 2.5 of [Favonia's thesis](https://favonia.org/files/thesis.pdf)
+- [Quotient Types for Programmers](https://www.hedonisticlearning.com/posts/quotient-types-for-programmers.html)
diff --git a/layouts/_default/baseof.html b/layouts/_default/baseof.html
index f4c264b..f0c7247 100644
--- a/layouts/_default/baseof.html
+++ b/layouts/_default/baseof.html
@@ -25,7 +25,7 @@