diff --git a/posts/type-algebra/1/index.qmd b/posts/type-algebra/1/index.qmd
index dc5afdb..a5bd40e 100644
--- a/posts/type-algebra/1/index.qmd
+++ b/posts/type-algebra/1/index.qmd
@@ -1,159 +1,285 @@
 ---
+title: "Type Algebra and You, Part 1: Basics"
+description: |
+  ...
 format:
   html:
     html-math-method: katex
-jupyter: python3
+# TODO
+date: "2023-11-01"
+date-modified: "2025-08-06"
+categories:
+  - haskell
+  - hyperoperations
+  - type theory
 ---
 
+```{haskell}
+--| echo: false
 
-Type Algebra and You, Part 1: Basics
-====================================
-
-When learning a new programming language, its type system can be a point of contention. Dynamic systems are fairly common in scripting languages like Python and JavaScript, which makes them great for beginners. However, it appears to be a general principle that imposing type-strictness (staticness, strength, ...) will generally allow errors to be caught before someone discovers them.
-
-To the computer, types are illusory, but they are not to the human. Beyond their use in programming languages, mathematicians also work with types in a purely abstract way (putting aside the fact that "type" is already an abstract concept). Types bear some resemblance to sets, yet in other ways resemble numbers and can be manipulated via algebra. In the following couple of posts, I would like to investigate these resemblances. This post will primarily focus on making the numerical resemblance clear, since it is more fundamental and everyone tends to agree on [how to define arithmetic](https://en.wikipedia.org/wiki/Peano_axioms).
-
-Since it can be difficult to appreciate relatively simple expressions without retreating back to programming language, I will use Haskell to demonstrate some interesting consequences of this topsy-turvy world.
+:set -XAllowAmbiguousTypes
+```
 
 
-### Starting from Square Zero
+When learning a new programming language, its type system can be a point of contention.
+Dynamic systems are fairly common in scripting languages like Python and JavaScript,
+  which makes them great for beginners.
+However, it appears to be a general principle that imposing type-strictness (staticness, strength, ...)
+  will generally allow errors to be caught before someone discovers them.
+To the computer, types are illusory, but they are not to the human.
 
-If we can treat types as numbers, then we best start with 0. We interpret this as the number of possible values which populate the type. There are exactly zero possible values of type **0**, i.e., there is no way to construct a value with this type. In Haskell, this type is referred to as `Void`. Here is a paraphrased  definition from (an earlier version of) [`Data.Void`](https://hackage.haskell.org/package/void-0.7/docs/src/Data-Void.html):
+Beyond their use in programming languages, mathematicians also work with types in a purely abstract way
+  (putting aside the fact that "type" is already an abstract concept).
+Types bear some resemblance to sets, yet in other ways resemble numbers and can be manipulated via algebra.
+In the following couple of posts, I would like to investigate these resemblances.
+
+This post will primarily focus on making the numerical resemblance clear,
+  since it is more fundamental and everyone tends to agree on
+  [how to define arithmetic](https://en.wikipedia.org/wiki/Peano_axioms).
+Since it can be difficult to appreciate relatively simple expressions without retreating
+  back to a programming language, I will use Haskell to demonstrate some interesting consequences
+  of this higher-kinded world.
 
 
-```{.haskell}
+Starting from Square Zero
+-------------------------
+
+If we can treat types as numbers, then we best start with 0.
+We interpret this as the number of possible values which populate the type.
+There are exactly zero possible values of type **0**, i.e., there is no way to construct
+  a value with this type.
+
+In Haskell, this type is referred to as `Void`.
+Here is a paraphrased definition from (an earlier version of)
+  [`Data.Void`](https://hackage.haskell.org/package/void-0.7/docs/src/Data-Void.html):
+
+
+```{haskell}
 newtype Void = V Void
 ```
 
-In other words, `V`, the only constructor of `Void`, requires already having a `Void`. This requires infinite regress, so it is logically impossible.
+In other words, `V`, the only constructor of `Void`, requires already having a `Void`.
+This requires infinite regress, so it is logically impossible.
 
 
-### Wait a minute, "only"?
+### Wait a minute, "only constructor"?
 
-Notice that `Void` has a constructor, `V`. It has type `Void -> Void`, which means that this type is definitely populated. It resembles the [empty function](https://en.wikipedia.org/wiki/Function_%28mathematics%29#empty_function) from set theory, of which there is only one for the empty set. This means that by constructing an empty type, we've also constructed a singleton.
+Notice that `Void`'s constructor, `V`, has type `Void -> Void`.
+This type, unlike `Void`, is definitely populated.
+It resembles the [empty function](https://en.wikipedia.org/wiki/Function_%28mathematics%29#empty_function)
+  from set theory, of which there is only one for the empty set.
+This means that by constructing an empty type, we've also constructed a singleton.
 
-Haskell already has a type with only one possible value: `()` (pronounced "unit", its only value is written identically). Can we prove that this is somehow the "same" type as `Void -> Void`? Of course! Remember, Haskell is a functional language. Therefore, we should focus on writing functions between the two types.
+Haskell already has a type with only one possible value: `()`[^1],
+  with its only value written identically.
+Can we prove that this is somehow the "same" type as `Void -> Void`?
+Of course!
+Remember, Haskell is a functional language.
+Therefore, we should focus on writing functions between the two types.
 
-```{.haskell}
+[^1]: Pronounced as "unit"
+
+```{haskell}
+-- Haskell actually complains that you're trying to pattern-match
+--   based on the constructor if you specify `V` on the LHS.
 toUnit :: (Void -> Void) -> ()
+toUnit _ = ()
+
 fromUnit :: () -> (Void -> Void)
-```
-
-The "to" and "from" in the names suggests that if we do one followed by the other, we should end up where we started. Or, in the language of functions, the composition of the functions is the identity.
-
-```{.haskell}
--- fromUnit . toUnit = id :: (Void -> Void) -> (Void -> Void)
--- toUnit . fromUnit = id :: () -> ()
-```
-
-In other words, we can reversibly map values from one type to the other (and vice versa). If such functions (also known as bijections) exist, then the types are *isomorphic*. I haven't actually defined the bijection yet; it is simple, if exhaustive:
-
-```{.haskell}
-toUnit   V  = ()
 fromUnit () = V
 ```
 
-In future examples showing isomorphic types, I will define only of the bijections to save a bit of vertical space. For the other, I'll show only the type annotation.
+The "to" and "from" in the names suggests that if we do one followed by the other,
+  we should end up where we started.
+Or, in the language of functions, the composition of the functions is the identity.
+
+```haskell
+fromUnit . toUnit == (id :: (Void -> Void) -> (Void -> Void))
+toUnit . fromUnit == (id :: () -> ())
+```
+
+In other words, we can reversibly map values from one type to the other (and vice versa).
+If such functions (also known as bijections) exist, then the types are *isomorphic*.
+
+
+### Poly-iso-morphisms
+
+We can assemble pairs of functions resembling this structure into a *typeclass* in Haskell:
+
+```{haskell}
+class Isomorphism a b where
+  -- Isomorphisms must define these two polymorphic functions
+  toA :: (b -> a)
+  toB :: (a -> b)
+
+  -- And these functions, which *could* be derived automatically
+  --   from the prior two, if the compiler didn't complain about ambiguity
+  identityA :: (a -> a)
+  -- aIdentity = toA . toB
+  identityB :: (b -> b)
+  -- bIdentity = toB . toA
+```
+
+Specifically, the isomorphism between `Void -> Void` and `()` looks like:
+
+```{haskell}
+instance Isomorphism (Void -> Void) () where
+  toA = fromUnit
+  toB = toUnit
+
+  identityA = fromUnit . toUnit
+  identityB = toUnit . fromUnit
+```
+
+In future examples, I'll use this typeclass to demonstrate isomorphisms between types.
 
 
 Hyperoperative (Multi)functors
 ------------------------------
 
-Another way to go from 0 to 1 is to just add one, an operation also called the [successor function](https://en.wikipedia.org/wiki/Successor_function). "Function" is vague here, since it is evocative of a mapping between values, rather than a mapping between types. [Kinds](https://wiki.haskell.org/Kind) live one step up from types, and we can conjecture the kind a successor "function" on types would have.
+Another way to go from 0 to 1 is to just add one,
+  an operation also called the [successor function](https://en.wikipedia.org/wiki/Successor_function).
 
-```{.haskell}
-succ :: Int -> Int -- the successor function constructs an integer from an integer
-Succ :: * -> *     -- so we need to be able to construct a "bigger" type from a type
+[Kinds](https://wiki.haskell.org/Kind) live one step up from types,
+  and we can conjecture the kind a successor "function" on types would have.
+
+```haskell
+-- The successor function constructs an integer from an integer
+succ :: Int -> Int
+-- So we need to be able to construct a "bigger" type from a type
+Succ :: * -> *
 ```
 
-The word with the closest meaning is [*functor*](https://wiki.haskell.org/Functor), which Haskell already uses to refer to types with a manipulable "inside" that can be mapped over. Fortunately, the kind of `Succ` matches what Haskell expects `Functor`s to look like (and in fact, since GHC 6.12.1, the compiler is smart enough to derive the definition on its own).
+"Function" is the wrong word for this, since it is evocative of a mapping between values,
+  rather than a mapping between types.
+The word with the closest meaning is [*functor*](https://wiki.haskell.org/Functor),
+  which Haskell already uses to refer to types with a manipulable "inside" that can be mapped over.
+Fortunately, the kind of `Succ` matches what Haskell expects `Functor`s to look like[^2].
 
-The functor in Haskell which most closely resembles the successor is `Maybe`.
+[^2]: In fact, since GHC 6.12.1, the compiler is smart enough to derive definitions in many cases.
 
-```{.haskell}
+The functor in Haskell which most closely resembles the successor function is `Maybe`.
+
+```haskell
 data Maybe a = Nothing | Just a
 type One = Maybe Void
 ```
 
+<!-- Evaluate the above cell -->
+```{haskell}
+--| echo: false
+
+type One = Maybe Void
+```
+
 $$
 \begin{matrix}
-\scriptsize \text{A Maybe of $X$ is either} &
-\scriptsize \text{Nothing} &
-\scriptsize \text{or} &
-\scriptsize \text{a value of $X$} &
-\\
-S(X) := & 1 & + & X \\
-\scriptsize \text{The 1-valued type is} &
-\scriptsize \text{Nothing} &
-\scriptsize \text{or} &
-\scriptsize \text{logically impossible} & \\
-\bold{1}  =& 1 &+& 0
+  \scriptsize \text{A Maybe $X$ is either}
+  & \scriptsize \text{Nothing}
+  & \scriptsize \text{or}
+  & \scriptsize \text{a value of $X$}
+  \\
+  S(X) := & 1 & + & X
+  \\
+  \scriptsize \text{The 1-valued type is}
+  & \scriptsize \text{Nothing}
+  & \scriptsize \text{or}
+  & \scriptsize \text{logically impossible}
+  \\
+  \bold{1}  =& 1 & + & 0
 \end{matrix}
 $$
 
-Since `Void` is has zero possible values, we should expect `Maybe Void` to have exactly one possible value. Constructing a `Just Void` would require that we already had a Void value, which is impossible. Therefore, `Nothing` is the only possible value of `Maybe Void`.
+Since `Void` is has zero possible values, we should expect `Maybe Void` to have exactly one possible value.
+Constructing a `Just Void` would require that we already had a Void value, which is impossible.
+Therefore, `Nothing` is the only possible value of `Maybe Void`.
 
-```{.haskell}
-toUnitM :: Maybe Void -> ()
-toUnitM Nothing = ()
--- toUnitM (Just Void) is fictitious
+```{haskell}
+toUnit :: Maybe Void -> ()
+toUnit Nothing = ()
 
--- fromUnitM :: () -> Maybe Void
--- fromUnitM . toUnitM = id :: Maybe Void -> Maybe Void
--- toUnitM . fromUnitM = id :: () -> ()
+fromUnit :: () -> Maybe Void
+fromUnit () = Nothing
+
+instance Isomorphism (Maybe Void) () where
+  toA = fromUnit
+  toB = toUnit
+
+  identityA = fromUnit . toUnit
+  identityB = toUnit . fromUnit
 ```
 
 
 ### Sums and Products
 
-If there's a functor which resembles the successor, then are there ones which also resemble addition and multiplication? Not exactly. Functors are strictly a single-argument kind, and luckily the successor is a unary function. Addition and multiplication are binary, so they require a slightly more complicated kind:
+If there's a functor which resembles the successor, then are there ones which also resemble addition and multiplication?
+Not exactly.
+Functors are strictly a single-argument kind, and luckily the successor is a unary function.
+Addition and multiplication are binary, so they require a slightly more complicated kind:
 
-```{.haskell}
+```haskell
 (+)      :: Int -> Int -> Int   -- we can add two things together
 Plus a b :: * -> * -> *         -- so we want to be able to add two types together
+
 (*)      :: Int -> Int -> Int   -- likewise, we can multiply two things
 Mult a b :: * -> * -> *         -- and we want to be able to multiply two types
 ```
 
-These kinds match what Haskell expects `Bifunctor`s to look like. Types get complicated when more than one parameter is involved, so GHC cannot derive `Bifunctor`. Alternatively, we can just consider bifunctors as they appear here: a functor with an arity of 2.
+These kinds match what Haskell expects `Bifunctor`s to look like.
+Types get complicated when more than one parameter is involved, so GHC cannot derive `Bifunctor`.
+Alternatively, we can just consider bifunctors as they appear here: a functor with an arity of 2.
 
-Putting aside semantics, Haskell indeed has two types resembling type addition and type multiplication. Respectively, they are `Either` and `(,)` (i.e., a 2-tuple):
+Putting aside semantics, Haskell indeed has two types resembling type addition and type multiplication.
+Respectively, they are `Either` and `(,)` (i.e., a 2-tuple):
 
-```{.haskell}
+```haskell
 data Either a b = Left a | Right b
 data (,) a b = (,) a b
 ```
 
 $$
 \begin{matrix}
-\scriptsize \text{Either $X$ or $Y$ is} &
-\scriptsize \text{a value of $X$} &
-\scriptsize \text{or} &
-\scriptsize \text{a value of $Y$} &
-\\
-E(X,Y) := & X & + & Y
-\\
-\scriptsize \text{A tuple of $X$ and $Y$ is} &
-\scriptsize \text{a value of $X$} &
-\scriptsize \text{and} &
-\scriptsize \text{a value of $Y$} &
-\\
-P(X,Y) := & X & \times & Y
+  \scriptsize \text{Either $X$ or $Y$ is}
+  & \scriptsize \text{a value of $X$}
+  & \scriptsize \text{or}
+  & \scriptsize \text{a value of $Y$}
+  \\
+  E(X,Y) := & X & + & Y
+  \\
+  \scriptsize \text{A tuple of $X$ and $Y$ is}
+  & \scriptsize \text{a value of $X$}
+  & \scriptsize \text{and}
+  & \scriptsize \text{a value of $Y$}
+  \\
+  P(X,Y) := & X & \times & Y
 \end{matrix}
 $$
 
-Product types are common (consider any `struct` or tuple in a more common language, but sum types are less so. `union`s in C get close, but they are bound too memory for our purposes. Using addition, we can actually reconstruct the successor from **1**:
+Product types are common (consider any `struct` or tuple in a more common language,
+  but sum types are less so.
+`union`s in C get close, but they are bound too memory for our purposes.
+Using addition, we can actually reconstruct the successor from **1**:
 
-```{.haskell}
-type Maybe' a = Either () a
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `Maybe a` and `((), a)`
 
-toMaybe' :: Maybe a -> Maybe' a
-toMaybe' Nothing  = Left ()
-toMaybe' (Just x) = Right x
+type MaybeEither a = Either () a
 
--- fromMaybe' :: Maybe' a -> Maybe a
--- fromMaybe' . toMaybe' = id :: Maybe a -> Maybe a
--- toMaybe' . fromMaybe' = id :: Maybe' a -> Maybe' a
+toMaybeEither :: Maybe a -> MaybeEither a
+toMaybeEither Nothing  = Left ()
+toMaybeEither (Just x) = Right x
+
+fromMaybeEither :: MaybeEither a -> Maybe a
+fromMaybeEither (Left ()) = Nothing
+fromMaybeEither (Right x) = Just x
+
+instance Isomorphism (Maybe a) (MaybeEither a) where
+  toA = fromMaybeEither
+  toB = toMaybeEither
+
+  identityA = fromMaybeEither . toMaybeEither
+  identityB = toMaybeEither . fromMaybeEither
 ```
 
 `Left ()` now takes on the role of `Nothing`, while all the `Right`s come from the type parameter `a`.
@@ -161,65 +287,139 @@ toMaybe' (Just x) = Right x
 
 ### Rearranging and Rebracketing
 
-Within the world of numbers, addition and multiplication are commutative and associative. Is the same true for types?
+Within the world of numbers, addition and multiplication are commutative and associative.
+Is the same true for types?
 
-Commutativity is obvious, since we can construct functions which switch *X* and *Y* around. Haskell already provides these functions, whose definitions I have copied here
+Commutativity is obvious, since we can construct functions which switch *X* and *Y* around.
+Haskell already provides these functions, whose definitions I have copied here
 
-```{.haskell}
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `Either a b` and `Either b a`
+
+-- From https://hackage.haskell.org/package/either-5.0.2/docs/Data-Either-Combinators.html#v:swapEither
 swapEither :: Either a b -> Either b a
 swapEither (Left x)  = Right x
 swapEither (Right x) = Left x
 
+instance Isomorphism (Either x y) (Either y x) where
+  toA = swapEither
+  toB = swapEither
+
+  identityA = swapEither . swapEither
+  identityB = swapEither . swapEither
+```
+
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `(a,b)` and `(b,a)`
+
+-- From https://hackage.haskell.org/package/base-4.16.1.0/docs/Data-Tuple.html#v:swap
 swap :: (a, b) -> (b, a)
 swap (x, y) = (y, x)
 
--- swapEither . swapEither = id :: Either a b -> Either a b
--- swap . swap = id :: (a, b) -> (a, b)
+instance Isomorphism (x, y) (y, x) where
+  toA = swap
+  toB = swap
+
+  identityA = swap . swap
+  identityB = swap . swap
 ```
-[swapEither](https://hackage.haskell.org/package/either-5.0.2/docs/Data-Either-Combinators.html#v:swapEither) <br>
-[swap](https://hackage.haskell.org/package/base-4.16.1.0/docs/Data-Tuple.html#v:swap)
 
 Associativity is a bit trickier, since it deals with triples rather than pairs.
 
-```{.haskell}
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `Either a (Either b c)` and `Either (Either a b) c`
+
 assocRightSum :: Either a (Either b c) -> Either (Either a b) c
 assocRightSum (Left x)          = Left (Left x)
 assocRightSum (Right (Left y))  = Left (Right y)
 assocRightSum (Right (Right z)) = Right z
 
--- assocLeftSum :: Either (Either a b) c -> Either a (Either b c)
--- assocLeftSum . assocRightSum = id :: Either a (Either b c) -> Either a (Either b c)
--- assocRightSum . assocLeftSum = id :: Either (Either a b) c -> Either (Either a b) c
+assocLeftSum :: Either (Either a b) c -> Either a (Either b c)
+assocLeftSum (Left (Left x))  = Left x
+assocLeftSum (Left (Right y)) = Right (Left y)
+assocLeftSum (Right z)        = Right (Right z)
+
+instance Isomorphism (Either a (Either b c)) (Either (Either a b) c) where
+  toA = assocLeftSum
+  toB = assocRightSum
+
+  identityA = assocLeftSum . assocRightSum
+  identityB = assocRightSum . assocLeftSum
+```
+
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `(a,(b,c))` and `((a,b),c)`
 
 assocRightProd :: (a, (b, c)) -> ((a, b), c)
 assocRightProd (x, (y, z)) = ((x, y), z)
 
--- assocLeftProd :: ((a, b), c) -> (a, (b, c))
--- assocLeftProd . assocRightProd = id :: (a, (b, c)) -> (a, (b, c))
--- assocRightProd . assocLeftProd = id :: ((a, b), c) -> ((a, b), c)
+assocLeftProd :: ((a, b), c) -> (a, (b, c))
+assocLeftProd ((x, y), z) = (x, (y, z))
+
+instance Isomorphism (a, (b, c)) ((a, b), c) where
+  toA = assocLeftProd
+  toB = assocRightProd
+
+  identityA = assocLeftProd . assocRightProd
+  identityB = assocRightProd . assocLeftProd
 ```
 
-In fact, since we don't care about order or grouping, we can forget both entirely and map them instead into 3-tuples and a triple-sum type:
+In fact, since we don't care about order or grouping, we can forget both entirely
+  and map them instead into 3-tuples and a triple-sum type:
 
-```{.haskell}
+```haskell
 data Either3 a b c = Left3 a | Center3 b | Right3 c
 data (,,) a b c = (,,) a b c
+```
+
+```{haskell}
+--| echo: false
+
+data Either3 a b c = Left3 a | Center3 b | Right3 c
+```
+
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `Either3 a b c` and `Either (Either a b) c`
 
 toLeftSum :: Either3 a b c -> Either (Either a b) c -- x+y+z = (x+y)+z
 toLeftSum (Left3 x)   = Left (Left x)
 toLeftSum (Center3 y) = Left (Right y)
 toLeftSum (Right3 z)  = Right z
 
--- fromLeftSum :: Either (Either a b) c -> Either3 a b c
--- fromLeftSum . toLeftSum = id :: Either3 a b c -> Either3 a b c
--- toLeftSum . fromLeftSum = id :: Either (Either a b) c -> Either (Either a b) c
+fromLeftSum :: Either (Either a b) c -> Either3 a b c
+fromLeftSum (Left (Left x))  = Left3 x
+fromLeftSum (Left (Right y)) = Center3 y
+fromLeftSum (Right z)        = Right3 z
+
+instance Isomorphism (Either3 a b c) (Either (Either a b) c) where
+  toA = fromLeftSum
+  toB = toLeftSum
+
+  identityA = fromLeftSum . toLeftSum
+  identityB = toLeftSum . fromLeftSum
+```
+
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `(a,b,c)` and `((a,b),c)`
 
 toLeftProd :: (a,b,c) -> ((a,b),c)
 toLeftProd (x,y,z) = ((x,y),z)
 
--- fromLeftProd :: ((a,b),c) -> (a,b,c)
--- fromLeftProd . toLeftProd = id :: (a,b,c) -> (a,b,c)
--- toLeftProd . fromLeftProd = id :: ((a,b),c) -> ((a,b),c)
+fromLeftProd :: ((a,b),c) -> (a,b,c)
+fromLeftProd ((x,y),z) = (x,y,z)
+
+instance Isomorphism (a, b, c) ((a,b), c) where
+  toA = fromLeftProd
+  toB = toLeftProd
+
+  identityA = fromLeftProd . toLeftProd
+  identityB = toLeftProd . fromLeftProd
 ```
 
 There's still a bit of work to prove associativity *in general* from these local rules, but we're still primarily concerned with the equivalent functors `Either` and `(,)`, which are local anyway.
@@ -229,143 +429,256 @@ There's still a bit of work to prove associativity *in general* from these local
 
 Naturally, **0** and **1** satisfy their typical properties. There are additional interpretations, however:
 
-| Property                   | Arithmetic          | Haskell | Reasoning
-|----------------------------|---------------------|---------|-----------
-| Additive Identity          | $0 + X \cong X$     | `Either Void a` is equivalent to `a` | Since **0** is unoccupied, its sum with any other type can only ever contain values from that other type (i.e., only `Right` values).
-| Multiplicative Identity    | $1 \cdot X \cong X$ | `((), a)` is equivalent to `a`       | Since **1** has exactly one possible value, its product with any other type is this value and any value from the other type (i.e., tuples of the form `((), x)`).
-| Multiplicative Annihilator | $0 \cdot X \cong 0$ | `(Void, a)` is equivalent to `Void`  | Since **0** is unoccupied, we cannot construct a type which requires a value from it (i.e., writing a tuple of the form `(Void, x)` requires having a `Void` value).
+
+#### Additive identity
+
+::: {layout="[[1,5,6]]" layout-valign="center"}
+$$
+0 + X \cong X
+$$
+
+`Isomorphism (Either Void a) a`
+
+Since **0** is unoccupied, its sum with any other type can only ever contain values from that other type
+  (i.e., only `Right` values).
+:::
+
+
+#### Multiplicative Identity
+
+::: {layout="[[1,5,6]]" layout-valign="center"}
+$$
+1 \cdot X \cong X
+$$
+
+`Isomorphism ((), a) a`
+
+Since **1** has exactly one possible value, its product with any other type is this value
+  and any value from the other type (i.e., tuples of the form `((), x)`).
+:::
+
+
+#### Multiplicative Annihilator
+
+::: {layout="[[1,5,6]]" layout-valign="center"}
+$$
+0 \cdot X \cong 0
+$$
+
+`Isomorphism (Void, a) Void`
+
+Since **0** is unoccupied, we cannot construct a type which requires a value from it
+  (i.e., writing a tuple of the form `(Void, x)` requires having a `Void` value).
+:::
 
 
 ### Distributivity
 
-Finally, to hammer home the resemblance to normal arithmetic, we should consider the distribution of multiplication over addition. We can first see that multiplication does distribute over the successor:
+Finally, to hammer home the resemblance to normal arithmetic, we should consider the
+  distribution of multiplication over addition.
+First, notice that type multiplication does distribute over the successor:
 
-```{.haskell}
-type SuccDist a b = ((Maybe a), (Maybe b))
+```{haskell}
+type SuccDist a b = (Maybe a, Maybe b)
 data SumProd a b = Nada | LProd a | RProd b | BothProd a b
 ```
 
 $$
 \begin{matrix}
-\scriptsize \text{Maybe $X$ and Maybe $Y$} & \scriptsize \text{is equivalent to} \\
-(1 + X) \cdot (1 + Y) \cong \\
-1
-& \scriptsize \text{Both Nothing}\\
-+ X \phantom{\cdot Y}
-& \scriptsize \text{or Just $x$, Nothing} \\
-+ \phantom{X \cdot} Y & \scriptsize \text{or Nothing, Just $y$} \\
-+ X \cdot Y & \scriptsize \text{or Just $x$, Just $y$} \\
+  \scriptsize \text{Maybe $X$ and Maybe $Y$} & \scriptsize \text{is equivalent to}
+  \\
+  (1 + X) \cdot (1 + Y) \cong
+  \\
+  1 & \scriptsize \text{Both Nothing}
+  \\
+    + X \phantom{\cdot Y}
+  & \scriptsize \text{or Just $x$, Nothing}
+  \\
+    + \phantom{X \cdot} Y & \scriptsize \text{or Nothing, Just $y$}
+  \\
+    + X \cdot Y & \scriptsize \text{or Just $x$, Just $y$}
 \end{matrix}
 $$
 
-If we forbade the first and last cases (in other words, if we "subtract" them out), then the type would be equivalent to the sum of *X* and *Y*.
+If we forbade the first and last cases (in other words, if we "subtract" them out),
+  then the type would be equivalent to the sum of *X* and *Y*.
 
-```{.haskell}
-toSuccDist :: Either a b -> SuccDist a b
-toSuccDist (Left x) = (Just x, Nothing)
-toSuccDist (Right y) = (Nothing, Just y)
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `SuccDist a b` and `SumProd a b`
 
-fromSuccDist :: SuccDist a b -> Either a b
-fromSuccDist (Just x, Nothing) = Left x
-fromSuccDist (Nothing, Just y) = Right y
-fromSuccDist _                 = undefined -- non-exhaustive!
+eitherToSuccDist :: Either a b -> SuccDist a b
+eitherToSuccDist (Left x) = (Just x, Nothing)
+eitherToSuccDist (Right y) = (Nothing, Just y)
 
--- fromSuccDist . toSuccDist = id :: Either a b -> Either a b
--- toSuccDist . fromSuccDist /= id -- because of extra values
+succDistToEither :: SuccDist a b -> Either a b
+succDistToEither (Just x, Nothing) = Left x
+succDistToEither (Nothing, Just y) = Right y
+succDistToEither _                 = undefined -- non-exhaustive!
+
+-- succDistToEither . eitherToSuccDist == (id :: Either a b -> Either a b)
+-- eitherToSuccDist . succDistToEither /= id (because of extra values)
+
+toSumProd :: SuccDist a b -> SumProd a b
+toSumProd (Nothing, Nothing) = Nada
+toSumProd (Just x, Nothing)  = LProd x
+toSumProd (Nothing, Just y)  = RProd y
+toSumProd (Just x, Just y)   = BothProd x y
+
+toSuccDist :: SumProd a b -> SuccDist a b
+toSuccDist Nada           = (Nothing, Nothing)
+toSuccDist (LProd x)      = (Just x, Nothing)
+toSuccDist (RProd y)      = (Nothing, Just y)
+toSuccDist (BothProd x y) = (Just x, Just y)
+
+instance Isomorphism (SuccDist a b) (SumProd a b) where
+  toA = toSuccDist
+  toB = toSumProd
+
+  identityA = toSuccDist . toSumProd
+  identityB = toSumProd . toSuccDist
 ```
 
-Fortunately, general distributivity is also relatively simple. We do as grade schoolers do and FOIL out the results...
+Fortunately, general distributivity is also relatively simple.
+We do as grade schoolers do and FOIL out the results.
 
-```{.haskell}
-type PreDist a b c d
-  = (Either a b, Either c d)
-data PostDist a b c d
-  = F a c | O a d | I b c | L b d
-  -- first, outer, inner, last
+```{haskell}
+type PreDist a b c d  = (Either a b, Either c d)
+-- first, outer, inner, last
+data PostDist a b c d = F a c | O a d | I b c | L b d
 ```
 
 $$
 \begin{matrix}
-\scriptsize \text{Either $X$ $Y$ and Either $Z$ $W$} & \scriptsize \text{is equivalent to} \\
-(X + Y) \cdot (Z + W) \cong \\
- \phantom{+} X \cdot Z
-& \scriptsize \text{Firsts,}\\
-\vphantom{} + X \cdot W
-& \scriptsize \text{Outers,} \\
-\vphantom{}+ Y \cdot Z
-& \scriptsize \text{Inners,} \\
-\vphantom{}+ Y \cdot W
-& \scriptsize \text{or Lasts} \\
+  \scriptsize \text{Either $X$ $Y$ and Either $Z$ $W$} & \scriptsize \text{is equivalent to} \\
+  (X + Y) \cdot (Z + W) \cong
+  \\
+   \phantom{+} X \cdot Z
+  & \scriptsize \text{Firsts,}
+  \\
+  \vphantom{} + X \cdot W
+  & \scriptsize \text{Outers,}
+  \\
+  \vphantom{} + Y \cdot Z
+  & \scriptsize \text{Inners,}
+  \\
+  \vphantom{} + Y \cdot W
+  & \scriptsize \text{or Lasts}
 \end{matrix}
 $$
 
 ...then construct our bijections:
 
-```{.haskell}
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `PreDist a b` and `PostDist a b`
+
 distribute :: PreDist a b c d -> PostDist a b c d
 distribute (Left x, Left z)   = F x z
 distribute (Left x, Right w)  = O x w
 distribute (Right y, Left z)  = I y z
 distribute (Right y, Right w) = L y w
 
--- undistribute :: PostDist a b c d -> PreDist a b c d
--- undistribute . distribute = id :: PreDist a b c d -> PreDist a b c d
--- distribute . undistribute = id :: PostDist a b c d -> PostDist a b c d
+undistribute :: PostDist a b c d -> PreDist a b c d
+undistribute (F x z) = (Left x, Left z)
+undistribute (O x w) = (Left x, Right w)
+undistribute (I y z) = (Right y, Left z)
+undistribute (L y w) = (Right y, Right w)
+
+instance Isomorphism (PreDist a b c d) (PostDist a b c d) where
+  toA = undistribute
+  toB = distribute
+
+  identityA = undistribute . distribute
+  identityB = distribute . undistribute
 ```
 
-This works primarily because without further information about any of the types `a`, `b`, `c`, `d`, we can only rearrange them. It may be the case that `a ~ (b -> d)` (a function from `b` to `d`), meaning that we could lose the distinction between the instances `O` and `L` (and be unable to `undistribute`). But we don't have enough information to define `distribute` in any other way than the above. A similar argument holds for our other bijections.
+This works primarily because without further information about any of the types `a`, `b`, `c`, `d`,
+  we can only rearrange values of them.
 
 
 Bools, Bools, and more Bools
 ----------------------------
 
-While it's all well and good that these operations appear to mirror familiar arithmetic, we haven't counted farther than **0** and **1**. Everyone past the age of four recognizes that **2** comes next. Fortunately, this corresponds to a much better-known type: booleans. Rather than defining them as numbers like in lower-level languages (as a computer would understand), we can construct them directly as abstract values in Haskell
+While it's all well and good that these operations appear to mirror familiar arithmetic,
+  we haven't counted farther than **0** and **1**.
+Everyone past the age of two recognizes that **2** comes next.
 
-```{.haskell}
+Fortunately, this corresponds to a much better-known type: booleans.
+Rather than defining them as numbers like in lower-level languages (as a computer would understand),
+  we can construct them directly as abstract values in Haskell
+
+```haskell
 data Bool = True | False
 ```
 
 $$
 \begin{matrix}
-\scriptsize \text{A bool is either} &
-\scriptsize \text{True} &
-\scriptsize \text{or} &
-\scriptsize \text{False} &
-\\
-\text{Bool} := & 1 & + & 1 &= \bold{2}
+  \scriptsize \text{A bool is either}
+  & \scriptsize \text{True}
+  & \scriptsize \text{or}
+  & \scriptsize \text{False}
+  \\
+  \text{Bool} := & 1 & + & 1 &= \bold{2}
 \end{matrix}
 $$
 
 Bools may also be defined using the above functors, either by two successors or by addition:
 
-```{.haskell}
+```{haskell}
 type BoolSucc = Maybe (Maybe Void) -- succ (succ 0)
+type BoolEither = Either () () -- 1 + 1
+```
+
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `Bool` and `BoolSucc`
 
 toBoolSucc :: Bool -> BoolSucc
 toBoolSucc False = Nothing
 toBoolSucc True  = Just Nothing
 
--- fromBoolSucc :: BoolSucc -> Bool
--- fromBoolSucc . toBoolSucc = id :: Bool -> Bool
--- toBoolSucc . fromBoolSucc = id :: BoolSucc -> BoolSucc
+fromBoolSucc :: BoolSucc -> Bool
+fromBoolSucc Nothing        = False
+fromBoolSucc (Just Nothing) = True
 
-type BoolEither = Either () () -- 1 + 1
+instance Isomorphism Bool BoolSucc where
+  toA = fromBoolSucc
+  toB = toBoolSucc
+
+  identityA = fromBoolSucc . toBoolSucc
+  identityB = toBoolSucc . fromBoolSucc
+```
+
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `Bool` and `BoolEither`
 
 toBoolEither :: Bool -> BoolEither
 toBoolEither False = Left ()
-toBoolEither True = Right ()
+toBoolEither True  = Right ()
 
--- fromBoolEither :: BoolEither -> Bool
--- fromBoolEither . toBoolEither = id :: Bool -> Bool
--- toBoolEither . fromBoolEither = id :: BoolEither -> BoolEither
+fromBoolEither :: BoolEither -> Bool
+fromBoolEither (Left ())  = False
+fromBoolEither (Right ()) = True
+
+instance Isomorphism Bool BoolEither where
+  toA = fromBoolEither
+  toB = toBoolEither
+
+  identityA = fromBoolEither . toBoolEither
+  identityB = toBoolEither . fromBoolEither
 ```
 
 
 ### Four Great Justice
 
-Rather than progressing to **3**, let's jump to **4**. The number 2 has an interesting property: its sum with itself is its product with itself (is its exponent with itself...) is 4. Thus, the following types all encode a four-valued type:
+Rather than progressing to **3**, let's jump to **4**.
+The number 2 has an interesting property: its sum with itself is its product with itself
+  (is its exponent with itself...) is 4.
+Thus, the following types all encode a four-valued type:
 
-```{.haskell}
+```{haskell}
 data Four     = Zero | One | Two | Three
 type FourSucc = Maybe (Maybe Bool)
 type FourSum  = Either Bool Bool
@@ -374,25 +687,45 @@ type FourProd = (Bool, Bool)
 
 $$
 \begin{align*}
-4 &:= 1+1+1+1 \\
-&\phantom{:}\cong  S(S(2)) \\
-&\phantom{:}\cong  E(2,2) = 2 + 2 \\
-&\phantom{:}\cong  P(2,2) = 2 \cdot 2 \\
+  4 &:= 1+1+1+1
+  \\
+  & \phantom{:}\cong  S(S(2))
+  \\
+  & \phantom{:}\cong  E(2,2) = 2 + 2
+  \\
+  & \phantom{:}\cong  P(2,2) = 2 \cdot 2 \\
 \end{align*}
 $$
 
 Showing isomorphism here can get a bit tricky, but there are natural bijections for `FourSum` and `FourProd` obtained by examining the binary expansions of 0, 1, 2, and 3.
 
-```{.haskell}
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `Four` and `FourSucc`
+
 toFourSucc :: Four -> FourSucc
 toFourSucc Zero  = Nothing
 toFourSucc One   = Just Nothing
 toFourSucc Two   = Just (Just False)
 toFourSucc Three = Just (Just True)
 
--- fromFourSucc :: FourSucc -> Four
--- fromFourSucc . toFourSucc = id :: Four -> Four
--- toFourSucc . fromFourSucc = id :: FourSucc -> FourSucc
+fromFourSucc :: FourSucc -> Four
+fromFourSucc Nothing             = Zero
+fromFourSucc (Just Nothing)      = One
+fromFourSucc (Just (Just False)) = Two
+fromFourSucc (Just (Just True))  = Three
+
+instance Isomorphism Four FourSucc where
+  toA = fromFourSucc
+  toB = toFourSucc
+
+  identityA = fromFourSucc . toFourSucc
+  identityB = toFourSucc . fromFourSucc
+```
+
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `Four` and `FourSum`
 
 toFourSum :: Four -> FourSum
 toFourSum Zero  = Left False   -- 00
@@ -400,9 +733,23 @@ toFourSum One   = Left True    -- 01
 toFourSum Two   = Right False  -- 10
 toFourSum Three = Right True   -- 11
 
--- fromFourSum :: FourSum -> Four
--- fromFourSum . toFourSum = id :: Four -> Four
--- toFourSum . fromFourSum = id :: FourSum -> FourSum
+fromFourSum :: FourSum -> Four
+fromFourSum (Left False)  = Zero
+fromFourSum (Left True)   = One
+fromFourSum (Right False) = Two
+fromFourSum (Right True)  = Three
+
+instance Isomorphism Four FourSum where
+  toA = fromFourSum
+  toB = toFourSum
+
+  identityA = fromFourSum . toFourSum
+  identityB = toFourSum . fromFourSum
+```
+
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `Four` and `FourProd`
 
 toFourProd :: Four -> FourProd
 toFourProd Zero  = (False, False)  -- 00
@@ -410,46 +757,77 @@ toFourProd One   = (False, True)   -- 01
 toFourProd Two   = (True, False)   -- 10
 toFourProd Three = (True, True)    -- 11
 
--- fromFourProd :: FourProd -> Four
--- fromFourProd . toFourProd = id :: Four -> Four
--- toFourProd . fromFourProd = id :: FourProd -> FourProd
+fromFourProd :: FourProd -> Four
+fromFourProd (False, False) = Zero
+fromFourProd (False, True)  = One
+fromFourProd (True, False)  = Two
+fromFourProd (True, True)   = Three
+
+instance Isomorphism Four FourProd where
+  toA = fromFourProd
+  toB = toFourProd
+
+  identityA = fromFourProd . toFourProd
+  identityB = toFourProd . fromFourProd
 ```
 
 
 ### Hiding in the Clouds
 
-Though I mentioned exponentiation earlier, I did not show the equivalent for types. Set theorists sometimes write [the set of functions from one set *A* to another set *B*](https://en.wikipedia.org/wiki/Function_type) as $B^A$ because the number of possible functions comes from the cardinalities of the sets: $|B|^{|A|}$. We previously examined how the constructor for Void is a singleton, which satisfies the equation $0^0 = 1$. At least in the finite world, sets and types are not so different, and indeed, we can write
+Though I mentioned exponentiation earlier, I did not show the equivalent for types.
+Set theorists sometimes write
+  [the set of functions from one set *A* to another set *B*](https://en.wikipedia.org/wiki/Function_type)
+  as $B^A$ because the number of possible functions comes from the cardinalities of the sets:
+  $|B|^{|A|}$.
+We previously examined how the constructor for Void is a singleton, which satisfies the equation $0^0 = 1$.
+At least in the finite world, sets and types are not so different, and indeed, we can write:
 
-```{.haskell}
+```{haskell}
 type FourFunc = Bool -> Bool
--- there are exactly four functions:
+
+-- There are exactly four functions:
 taut x = True   -- tautology
 cont x = False  -- contradiction
 id'  x = x      -- identity
-not' x = not x  -- negation
+not'   = not    -- negation
 ```
 
 $$
-2 \rightarrow 2 = 2^2 \cong \bold 4
+\textcolor{red}{2} \rightarrow \textcolor{blue}{2}
+  = \textcolor{blue}{2}^{\textcolor{red}{2}} \cong \bold 4
 $$
 
-If we want to map these functions onto our `Four` type, we can again examine the binary expansion of the numbers 0-3. This time, the first place value encodes the value of the function on `False`, and the second value the same on `True`.
+If we want to map these functions onto our `Four` type, we can again examine
+  the binary expansion of the numbers 0-3.
+This time, the rightmost place value encodes the value of the function on `False`,
+  and the leftmost value the same on `True`.
+
+```{haskell}
+--| code-fold: true
+--| code-summary: Isomorphism instance for `Four` and `FourFunc`
 
-```{.haskell}
 toFourFunc :: Four -> FourFunc
--- easiest to consider binary place values as input
---                          10
-toFourFunc Zero  = cont  -- 00
-toFourFunc One   = not'  -- 01
-toFourFunc Two   = id'   -- 10
-toFourFunc Three = taut  -- 11
+--                       -- f(1) f(0)
+toFourFunc Zero  = cont  --   0    0
+toFourFunc One   = not'  --   0    1
+toFourFunc Two   = id'   --   1    0
+toFourFunc Three = taut  --   1    1
 
--- fromFourFunc :: FourFunc -> Four
--- fromFourFunc . toFourFunc = id :: Four -> Four
--- toFourFunc . fromFourFunc = id :: FourFunc -> FourFunc
+fromFourFunc :: FourFunc -> Four
+fromFourFunc cont = Zero
+fromFourFunc not' = One
+fromFourFunc id'  = Two
+fromFourFunc taut = Three
+
+instance Isomorphism Four FourFunc where
+  toA = fromFourFunc
+  toB = toFourFunc
+
+  identityA = fromFourFunc . toFourFunc
+  identityB = toFourFunc . fromFourFunc
 ```
 
-For larger functions, we can see a more generalizable mapping from the truth table, shown here for AND
+For larger functions, we can see a more generalizable mapping from looking at a truth table, shown here for AND:
 
 | Column Number | Binary | Input (x) | Input (y) | x AND y |
 |---------------|--------|-----------|-----------|---------|
@@ -458,20 +836,37 @@ For larger functions, we can see a more generalizable mapping from the truth tab
 | 2             | 10     | True      | False     | False   |
 | 3             | 11     | True      | True      | True    |
 
-Going up the final column and converting to binary digits, we can read "1000", which is the binary expansion of 8. The other numbers from 0 to $(2^2)^2 - 1$ can similarly be associated to boolean functions `Bool -> (Bool -> Bool)`. Note that function arrows are assumed to be right-associative, but this is opposite the right-associativity of typical exponentiation. I'll dive deeper into why this needs to be the case later.
+Going up the final column and converting to binary digits, we can read "1000",
+  which is the binary expansion of 8.
+The other numbers from 0 to $(2^2)^2 - 1$ can similarly be associated to
+  boolean functions `Bool -> (Bool -> Bool)`[^3].
+
+[^3]: Note that function arrows are assumed to be right-associative, but this is opposite
+      the typical application order of exponentiation.
+    I'll dive deeper into why this needs to be the case later.
 
 
 Closing
 -------
 
-If you know your Haskell, especially the difference between `data` and `newtype`, then you know about the slight stretching of the truth I have performed. Yes, it is true that types defined with `data` implicitly add a possible `undefined` value which can tell the runtime to error out. Everyone who knows Haskell better than me says [not to worry about it in most cases](https://wiki.haskell.org/Newtype). At worst, it would make some of the pretty arithmetic above go away.
+If you know your Haskell, especially the difference between `data` and `newtype`,
+  then you know about the way I have slightly stretched the truth.
+It is true that types defined with `data` implicitly add a possible
+  `undefined` value which can tell the runtime to error out.
+Everyone who knows Haskell better than me says
+  [not to worry about it in most cases](https://wiki.haskell.org/Newtype).
+At worst, using `data` would make some of the pretty arithmetic above be less pretty.
 
-Other fascinating concepts live in this world, such as the [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence). Rather than discussing them, in the next post I would like to press onward with the algebra. I have spent this post laying the groundwork for arithmetic on types, so it will focus more upon recursion and fixed points.
-
-A Haskell file containing all of the code on this page can be found [here]().
+Other fascinating concepts live in this world, such as the
+  [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence).
+Rather than discussing them, in [the next post](../2/) I would like to press onward with the algebra.
+I have spent this post laying the groundwork for arithmetic on types,
+  so it will focus more upon recursion and fixed points.
 
 
 ### Additional Links
 
-- [Algebraic Data Types](https://en.wikipedia.org/wiki/Algebraic_data_type) (Wikipedia)
-- [Generically Deriving Bifunctor](https://blog.csongor.co.uk/generic-deriving-bifunctor/) (Blogpost by Csongor Kiss)
+- [Algebraic Data Types](https://en.wikipedia.org/wiki/Algebraic_data_type)
+  (Wikipedia)
+- [Generically Deriving Bifunctor](https://blog.csongor.co.uk/generic-deriving-bifunctor/)
+  (Blogpost by Csongor Kiss)