Isomorphism & Record Types

In set theory, two sets are said to be isomorphic if they are in a one-to-one correspondence, meaning that there is a bijection or, equivalently, the following four conditions are met: 1) a function \(f: A \to B\), 2) a function \(g: B\to A\) in the opposite direction, such that 3) the composition of the functions one way is an identity, \(g(f(x)) = x\), and 4) an identity in the opposite direction as well, \(f(g(y))=y\).

For one thing to be isomorphic to another means that the two are “virtually the same”. For example, the singleton sets \(\{\bullet\}\), \(\{\star\}\), and \(\{\ast\}\), are all isomorphic, though not identical. So isomorphism is not quite equality, but comes very close to it.

Function composition

We haven’t yet defined composition in Agda; let’s do that now:

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) x  = g (f x)

That is:

\[\begin{align*} \_\!\circ\!\_ &: (B \xrightarrow{g} C) \to \big((A\xrightarrow{f} B) \to (A\to C)\big) \\ g \circ\!\_ &: (A\xrightarrow{f} B) \to (A\to C) \\ g \circ f &: A\to C \\ (g \circ f)\ x &: C\\ (g \circ f)\ x &= g(f(x)) \end{align*}\]

We can visualize composition in the following diagram:

First definition

How do we capture the idea of being isomorphic in type theory and, specifically, in Agda? There are two ways, according to the PLFA. The first is the more familiar but more convoluted way, where we declare the new type as a data type along with its constructor:

data _≃′_ (A B : Set): Set where
  mk-≃′ : ∀ (to : A → B) →
          ∀ (from : B → A) →
          ∀ (from∘to : (∀ (x : A) → from (to x) ≡ x)) →
          ∀ (to∘from : (∀ (y : B) → to (from y) ≡ y)) →
          A ≃′ B

to′ : ∀ {A B : Set} → (A ≃′ B) → (A → B)
to′ (mk-≃′ f g g∘f f∘g) = f

from′ : ∀ {A B : Set} → (A ≃′ B) → (B → A)
from′ (mk-≃′ f g g∘f f∘g) = g

from∘to′ : ∀ {A B : Set} → (v : A ≃′ B) → (∀ (x : A) → from′ v (to′ v x) ≡ x)
from∘to′ (mk-≃′ f g g∘f f∘g) = g∘f

to∘from′ : ∀ {A B : Set} → (v : A ≃′ B) → (∀ (y : B) → to′ v (from′ v y) ≡ y)
to∘from′ (mk-≃′ f g g∘f f∘g) = f∘g

For any two types \(A\) and \(B\), we have the type \(A\simeq' B\). We construct terms (isomorphisms) of this new type with the constructor \(mk\text{-}\!\simeq'\). Recall that an isomorphism must fulfill the four conditions stated at the beginning of this entry. For this reason, the constructor is declared so as to take four types of functions: 1) of type \(A\to B\), 2) of type \(B\to A\), 3) of type \(\textstyle\prod_{x:A} \mathtt{from} (\mathtt{to}\ x) \equiv x\), and 4) of type \(\textstyle\prod_{y:B} \mathtt{to} (\mathtt{from}\ y) \equiv y\).¹

In words, the constructor \(mk\text{-}\!\simeq'\) takes functions or morphisms \(A\to B\) and \(B\to A\), as well as evidence that their composition in both directions acts like the identity function, and finally returns an isomorphism of the new type \(A \simeq' B\).

What does the rest of the code mean? The PLFA does not expand on this. So far as I can tell, it declares and defines four eliminators (also called projection functions) for our newly-constructed term, although I’m not entirely sure why we need this. In any case, let’s say our constructed term of \(A\simeq' B\) is \(mk\text{-}\!\simeq' f\ g\ g\!\circ\!f\ f\!\circ\! g\). To recover the original arguments taken by \(mk\text{-}\!\simeq'\), we define new functions (the projections), one for each argument. For example, to get the first argument \(f\) whose type is \(A\to B\), we define \(\mathtt{to}'\), the first projection function. Similarly, to get the second argument \(g\) out of \(mk\text{-}\!\simeq' f\ g\ g\!\circ\!f\ f\!\circ\! g\), we have \(\mathtt{from}'\), the second projection function, etc.

Second definition with a record type

Fortunately, there is an alternative to this convoluted mess. We can use Agda’s record types to shorten the definition of the new type:

record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y

Instead of declaring a constructor, which as we just saw can lead to long code, in a record type we declare the “ingredients” that each term of the new record type must have. Now, buckle up because this is going to get a bit confusing!

Let’s take a familiar example from set theory to make the notion of a record clearer: recall that a Cartesian product \(A\times B\) is a set whose elements are pairs of the form \((a,b)\). Here, \(a\) and \(b\) represent the components or coordinates of the pair-element. Recall also that an ordered pair is a single “thing”, so to project out only one component, we need a projection function, usually denoted \(\pi\). The two projections, \(\pi_1\) and \(\pi_2\), which allow us to recover \(a\) and \(b\) are defined as the mappings \((a,b)\mapsto a\) and \((a,b) \mapsto b\), respectively. (Keep in mind the distinction between a component, say \(a\), and a projection, \(\pi\). This will be important shortly.)

Translating this into type theory, we have that \(A\times B\) is a record type whose terms likewise consist of two things, where the first component \(a:A\) of the term is obtained via the first projection \(\pi_1 : A\times B \to A\), and the second component \(b:B\) via the second projection \(\pi_2: A\times B \to B\). Now, here comes the important question: which of these, the component or the projection, is being referred to by the keyword \(\mathtt{field}\) in the Agda code? Answer: I don’t know!

Getting back to the code, the new type \(A\simeq B\) is introduced as a record type with the keyword \(\mathtt{record}\), and the eliminators or projections by which we get the components of any term \(v: A\simeq B\) are declared following the keyword \(\mathtt{field}\). Since a term \(v: A\simeq B\) is an isomorphism, to recover its components we need four projections: the first projection, \(\mathtt{to}\), applied to \(v\), returns proof of \(A\to B\), and the second one, \(\mathtt{from}\), applied to \(v\), returns proof of \(B\to A\). So far so good.

As for the third and fourth projections, we have to unpack a little bit more. The third projection, \(\mathtt{from\!\circ\! to}\), applied to \(v\), returns a function \(\mathtt{from\!\circ\! to}\ v\) of type \(\textstyle\prod_{x:A} \mathtt{from\ (to}\ x) \equiv_A x\). According to the PLFA, this constitutes proof that the projection \(\mathtt{from}\) is a left-inverse of \(\mathtt{to}\), i.e., that their composition, \(\mathtt{from \circ to}\), is the identity function.²

Similarly for the fourth projection, \(\mathtt{to\!\circ\! from}\) providing proof that \(\mathtt{from}\) is a right-inverse.

Isomorphism is an equivalence

An isomorphism is reflexive, symmetric, and transitive. And no wonder, since it is close to being equality itself. We will now show this. But first, in order to save ourselves from typing a bit of code, we will use lambda expressions to define functions (dependent or not) without using names like \(f\), \(g\), etc.

If you’ve studied the basics of the lambda calculus, you’ll recall that an anonymous function is traditionally denoted something like: \(\lambda x.N\), where \(N\) is the body of the function, and can be read as the mapping \(x \mapsto N\).

In Agda, we’ll use the notation \(\lambda\{x \to N\}\). So, for example, to denote the identity function, that is a function that takes a term and returns that very same term, we could write \(f: A \to A\), s.t. \(f(x) = x\), OR we can simply write \(\lambda\{x \to x\}\), corresponding to the traditional \(\lambda x.x\).

With this in mind, here’s a way to show that an isomorphism is an equivalence.

Reflexivity

≃-refl : ∀ {A : Set} → A ≃ A
≃-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    ; to∘from = λ{y → refl}
    }

\(\simeq\!\text{-}\mathtt{refl}\ \{A\}\) (or \(\simeq\!\text{-}\mathtt{refl}\)) is a term or proof of our new record type \(A\simeq A\). As an isomorphism, the term \(\simeq\!\text{-}\mathtt{refl}\) must be a 4-tuple whose components are obtained via the projections \(\mathtt{to}\), \(\mathtt{from}\), \(\mathtt{from\!\circ\! to}\), and \(\mathtt{to\!\circ\! from}\) applied to \(\simeq\!\text{-}\mathtt{refl}\) itself.³

record
  { to      (≃-refl) = λ{x → x}
  ; from    (≃-refl) = λ{y → y}
  ; from∘to (≃-refl) = λ{x → refl}
  ; to∘from (≃-refl) = λ{y → refl}
  }

The third and fourth projections, \(\mathtt{from\!\circ\! to}\) and \(\mathtt{to\!\circ\! from}\), applied to \(\simeq\!\text{-}\mathtt{refl}\), return functions of the following types:

\[ \prod_{x: A} \mathtt{from} (\mathtt{to}\ x) \equiv_A x \qquad \prod_{y: A} \mathtt{to} (\mathtt{from}\ y) \equiv_A y \] which are equivalent to:

\[ \prod_{x: A} x \equiv_A x \qquad \prod_{y: A} y \equiv_A y \] That is, they are dependent functions that, for any term of \(A\), return a term of the equality type \(x\equiv_A x\) (or \(y \equiv_A y\)), which we can always provide as \(\mathtt{refl}\). Therefore, the values \(\mathtt{from\!\circ\! to}\ (\simeq\!\text{-}\mathtt{refl})\) and \(\mathtt{to\!\circ\! from}\ (\simeq\!\text{-}\mathtt{refl})\) are defined as \(\lambda\) functions that map the argument \(x/y\) to \(\mathtt{refl}\).

Symmetry

≃-sym : ∀ {A B : Set} → A ≃ B → B ≃ A
≃-sym v =
  record
    { to      = from v
    ; from    = to   v
    ; from∘to = to∘from v
    ; to∘from = from∘to v
    }

Here, \(\simeq\!\text{-}\mathtt{sym}\) takes a term \(v\) of \(A\simeq B\) and returns a term \(\simeq\!\text{-}\mathtt{sym}\ v: B\simeq A\). As a term of an isomorphism type, \(\simeq\!\text{-}\mathtt{sym}\ v\) must be a 4-tuple of components obtained from application of the four projections \(\mathtt{to}\), \(\mathtt{from}\), \(\mathtt{from\!\circ\! to}\), and \(\mathtt{to\!\circ\! from}\) to \(\simeq\!\text{-}\mathtt{sym}\ v\).

record
  { to      (≃-sym v) = from v
  ; from    (≃-sym v) = to   v
  ; from∘to (≃-sym v) = to∘from v
  ; to∘from (≃-sym v) = from∘to v
  }

You’ll notice that each function is defined as its inverse. Why? Let’s see: a term \(v\) of \(A\simeq B\) is an isomorphism between terms of \(A\) and terms of \(B\), whereas a term of \(B\simeq A\) is an isomorphism between terms of \(B\) and terms of \(A\). There’s not much of a difference, is there? We are simply inverting the domain and codomain. But this does nothing to an isomorphism: an inverted isomorphism is still an isomorphism.

Therefore, we fix the four functions of \(\simeq\!\text{-}\mathtt{sym}\ v: B\simeq A\) as being their equivalent functions in \(v: A\simeq B\). For example, the function \(\mathtt{to}\ (\simeq\!\text{-}\mathtt{sym}): B \to A\) is defined as the function \(\mathtt{from}\ v: B\to A\). The function \(\mathtt{from}\ (\simeq\!\text{-}\mathtt{sym}): A \to B\) is defined as its equivalent \(\mathtt{to}\ v: A\to B\). Etc.

Transitivity

≃-trans : ∀ {A B C : Set} → A ≃ B → B ≃ C → A ≃ C
≃-trans v w =
  record
    { to       = to   w ∘ to   v
    ; from     = from v ∘ from w
    ; from∘to  = λ{x →
        begin
          (from v ∘ from w) ((to w ∘ to v) x)
        ≡⟨⟩
          from v (from w (to w (to v x)))
        ≡⟨ cong (from v) (from∘to w (to v x)) ⟩
          from v (to v x)
        ≡⟨ from∘to v x ⟩
          x
        ∎}
    ; to∘from = λ{y →
        begin
          (to w ∘ to v) ((from v ∘ from w) y)
        ≡⟨⟩
          to w (to v (from v (from w y)))
        ≡⟨ cong (to w) (to∘from v (from w y)) ⟩
          to w (from w y)
        ≡⟨ to∘from w y ⟩
          y
        ∎}
     }

Sigh.

record
  { to      (≃-trans v w) = to   w ∘ to   v
  ; from    (≃-trans v w) = from v ∘ from w
  ; from∘to (≃-trans v w) = λ{x → ... x∎}
  ; to∘from (≃-trans v w) = λ{y → ... y∎}
  }

Okay, the constructor \(\equiv\text{-}\mathtt{trans}\) takes a term \(v: A\simeq B\), a term \(w: B\simeq C\), and returns the term/isomorphism \(\simeq\text{-}\mathtt{trans}\ v\ w: A\simeq C\).

This term \(\simeq\text{-}\mathtt{trans}\ v\ w\) is a 4-tuple whose components can be recovered from the usual projections, \(\mathtt{to}\), \(\mathtt{from}\), \(\mathtt{from\!\circ\! to}\), and \(\mathtt{to\!\circ\! from}\), all of which will be composites. The types of each component are the following:

\[\begin{gather} A \to C \\ C \to A \\ \prod_{x:A} \mathtt{from}\ v\circ \mathtt{from}\ w\ ((\mathtt{to}\ w \circ \mathtt{to}\ v)\ x) \equiv_A x \\ \prod_{y:C} \mathtt{to}\ w \circ \mathtt{to}\ v\ ((\mathtt{from}\ v \circ \mathtt{from}\ w)\ y) \equiv_C y \end{gather}\]

If this makes your head spin, you’re in good company.

The first component of the term \(\simeq\text{-}\mathtt{trans}\ v\ w: A\simeq C\) is the output of the first projection, \(\mathtt{to}\), defined as the composition of the first component of \(v: A\simeq B\) (i.e., \(\mathtt{to}\ v: A\to B\)) and the first component of \(w: B\simeq C\) (that is, \(\mathtt{to}\ w: B\to C\)), giving us the function \(\mathtt{to}\ w \circ \mathtt{to}\ v\) whose type is \(A\to C\):

Similarly for the second component, which gives us a function of type \(C\to A\) (just invert the arrows in the diagram, and change the names of the functions appropriately).

Before going on to the third and fourth components, looking at the code you might be wondering why we didn’t define them as functions that map to \(\mathtt{refl}\), i.e., \(\lambda \{x \to \mathtt{refl}\}\) and \(\lambda \{y \to \mathtt{refl}\}\). After all, according to their type, they return a proof of an equality type, but the left-hand side of that equality, e.g., \(\mathtt{from}\ v\circ \mathtt{from}\ w\ ((\mathtt{to}\ w \circ \mathtt{to}\ v)\ x)\), reduces to just \(x\), so that the equality type is equivalent to \(x \equiv_A x\), for which we always have \(\mathtt{refl}\). So why the long code? Well, if you define the function as mapping to \(\mathtt{refl}\) and try to compile in Agda, you’ll get an error. It seems Agda can’t see that this should be the case, and needs help. That’s where the equational reasoning comes in.

After opening the equational reasoning environment, we reduce

\[ \mathtt{from}\ v\circ \mathtt{from}\ w\ ((\mathtt{to}\ w \circ \mathtt{to}\ v)\ x) \]

down to

\[ \mathtt{from}\ v\ (\underbrace{\mathtt{from}\ w\ (\mathtt{to}\ w}\ (\mathtt{to}\ v\ x))) \]

with no justification needed in between the angled brackets \(\equiv\!\langle \rangle\), as this follows from the definition of composition.

Now, we want to reduce this term further, and here Agda does need an explicit justification. Note that, for \(w: B\simeq C\), we have \(\mathtt{to}\ w: B\to C\) and \(\mathtt{from}\ w: C \to B\) (which I’ve marked with an underbrace). Therefore, we provide Agda with proof that the composition of these two functions, \(\mathtt{from \circ to}\), is the identity (i.e., \(\mathtt{from}\) is the left inverse of \(\mathtt{to}\)). This proof is the third projection applied to \(w\), i.e., \(\mathtt{from\!\circ\! to}\ w\). This is the justification needed to go from

\[ {\mathtt{from}\ w\ (\mathtt{to}\ w}\ (\mathtt{to}\ v\ x)) \]

to just

\[ (\mathtt{to}\ v\ x) \]

And since these are equivalent, by congruence we can apply \(\mathtt{from}\ v\) to both terms and get equivalent results. Thus we are allowed to go from

\[ \underbrace{\mathtt{from}\ v}\ \mathtt{from}\ w\ (\mathtt{to}\ w\ (\mathtt{to}\ v\ x)) \]

down to

\[ \underbrace{\mathtt{from}\ v}\ (\mathtt{to}\ v\ x) \]

By similar reasoning, we note that, for \(v: A\simeq B\), we have \(\mathtt{to}\ v: A \to B\) and \(\mathtt{from}\ v: B\to A\). We therefore provide proof that the composition \(\mathtt{from \circ to}\) is an identity, namely, the third projection \(\mathtt{from\!\circ\! to}\) applied to \(v\). This allows us to go from

\[ \underbrace{\mathtt{from}\ v\ (\mathtt{to}\ v}\ x) \]

to \(x\). Thus \(\mathtt{from}\ v\circ \mathtt{from}\ w\ ((\mathtt{to}\ w\circ \mathtt{to}\ v)\ x)\) is indeed equivalent to \(x\), and the lambda function defining the third component of \(\simeq\!\text{-}\mathtt{trans}\ v\ w\) is well defined.

By similar reasoning, we can define the fourth component of the term \(\simeq\text{-}\mathtt{trans}\ v\ w\).

We have now correctly defined all components of terms \(\simeq\!\text{-}\mathtt{refl}\), \(\simeq\!\text{-}\mathtt{sym}\ v\), and \(\simeq\!\text{-}\mathtt{trans}\ v\ w\), which provide proof that an isomorphism is reflexive, symmetric, and transitive. \(\blacksquare\)