Embedding

🛑 The names of variables in the code have been changed to save myself a lot of typing. Thus, instead of A≃B, I write \(v\), and instead of B≃C, \(w\). If you are using the PLFA, avoid mixing my code with theirs, otherwise Agda won’t compile.

In the last entry, we saw that an isomorphism requires 4 “ingredients”: a function \(f: A\to B\), a function \(g: B\to A\), proof that \(g\) is \(f\)’s left inverse, i.e., \(g \circ f = id_A\), and proof that \(g\) is also \(f\)’s right inverse, i.e., \(f \circ g = id_B\).

What if we don’t have that last condition? In that case, we have, not an isomorphism, but an embedding. We’ll use set theory again to make this more intuitive.

Picture the subset \(A \subseteq B\). Take \(A\) “outside” of \(B\), and then define a function \(f\) that, for every element of \(A\), picks out an element of \(B\), s.t. \(f\) identifies the whole subset \(A\) inside \(B\) again. In this case, it is easy to define another function \(g\) that simply “undoes” \(f\), i.e,. \(g(f(x)) = x\). This makes \(g\) the left inverse of \(f\).

This embedding allows us to identify \(A\) “inside” of, or “within”, \(B\) (denoted \(A\preccurlyeq B\)) but not vice versa. Now if \(g\) were also a right inverse of \(f\), then \(B\) would be in a one-to-one correspondence with \(A\) and there would be an isomorphism between \(A\) and \(B\). Denying this right-inverse property to \(g\), leaves us with an embedding.

record _≲_ (A B : Set) : Set where
  field
    fst  : A → B
    snd  : B → A
    thrd : ∀ (x : A) → snd (fst x) ≡ x

Here I’ve changed the name of the projections to \(\mathtt{fst}\), \(\mathtt{snd}\), and \(\mathtt{thrd}\), for the reason I’m about to explain.

A little detour…

According to the Agda documentation, the declared type constructor \(\preccurlyeq\) has the type \((A: \mathtt{Set}) \to (B: \mathtt{Set}) \to \mathtt{Set}\). In the code, we “abbreviate” this by setting the types \(A\) and \(B\) as parameters.

After the keyword \(\mathtt{field}\), we are told that each term of the new type has 3 components, each obtained via a projection. The reason I changed the names of the projections from \(\mathtt{to}\) and \(\mathtt{from}\) to \(\mathtt{fst}\) and \(\mathtt{snd}\) is to make clearer the fact that the first component is got from the first projection \(\mathtt{fst}\), the second component from the second projection \(\mathtt{snd}\), etc.

Now the above code is a bit… misleading. Well, not really, but it hides something, which was the source of much confusion on my part in the previous entry on isomorphism. For example, the first projection, \(\mathtt{fst}\), does not have type \(A\to B\), because a projection acts on the term of the new record type, and \(A\) is not that. I had to search the Agda documentation (and elsewhere on the Internet) to find out why the code is written this way. The Agda docs tell us that \(\mathtt{fst}\) has the following internal (hidden) declaration:

\[\begin{align} \preccurlyeq.\mathtt{fst} &: \{A\ B : \mathtt{Set}\} \to (A\preccurlyeq B \to (A\to B))\\ \preccurlyeq.\mathtt{fst} &: A\preccurlyeq B \to (A\to B)\\ \preccurlyeq.\mathtt{fst}\ v &: A\to B \end{align}\]

Here the first projection is prefixed by the name of the type-former \(\preccurlyeq\) and a dot \((.)\). As you can see, the type of \(\preccurlyeq.\mathtt{fst}\) is \(\{A\ B : \mathtt{Set}\} \to (A\preccurlyeq B \to (A\to B))\) or, if we omit the implicit parameters, just \(A\preccurlyeq B \to (A\to B)\), meaning that it takes a term of the new record type, say \(v: A\preccurlyeq B\), and returns the first component of that term, i.e., \(\preccurlyeq.\mathtt{fst}\ v\), whose type is \(A\to B\). Therefore, I was right in assuming that the declared types in the \(\mathtt{field}\) section of the code referred not to the projections, but to their return value.

With this in mind, the way we should read the code is by picturing that the projections \(\mathtt{fst}\), \(\mathtt{snd}\), and \(\mathtt{thrd}\) all have a “hidden” argument of the new type \(A\preccurlyeq B\). Let’s call that term \(v\). Then the above record type declaration would be written in pseudo-code as:

I say psuedo-code because this won’t work in Agda. The way record types were baked into Agda prevent us from putting any arguments there. At the same time, without this, one is liable to get confused as to the types of the projections, which determines what arguments they can take. In the following, I will be including a second version of the code with the missing argument just to emphasize that \(\mathtt{fst}\ (v)\), for example, is the equivalent to the internally-defined \(\preccurlyeq.\mathtt{fst}\ v\) in Agda. Just keep in mind that this second version is pseudo-code.

Also, note that I omitted the third projection because it presents another interesting issue: it makes reference to the previous two projections. According to what I’ve just presented, it should be thought of as:

But note that \(\mathtt{fst}\), on the right side, appears to take \(x: A\). However, we already agreed that \(\mathtt{fst}\) is not a function of type \(A\to B\). What is a function of that type is \(\mathtt{fst}\ (v)\) (or, \(\preccurlyeq.\mathtt{fst}\ v\)). Therefore, we must also picture a hidden \(v\) on the right side as well:

Properties

Reflexivity

An embedding, because it has 3/4 of the ingredients of an isomorphism, also has the property of reflexivity and transitivity. But instead of symmetry, it has the property of anti-symmetry. We prove each of these below.

≲-refl : ∀ {A : Set} → A ≲ A
≲-refl =
  record
    { fst   = λ{x → x}
    ; snd   = λ{y → y}
    ; thrd  = λ{x → refl}
    }

That is, \(\preccurlyeq\!\text{-}\mathtt{refl} \{A\}\), or just \(\preccurlyeq\!\text{-}\mathtt{refl}\), is a term or proof of the new type \(A \preccurlyeq A\). Because this new type is a record, then \(\preccurlyeq\!\text{-}\mathtt{refl}\) must have 3 components, each obtained by a projection. So, after the keyword \(\mathtt{record}\), we define the return value of each projection on the term \(\preccurlyeq\!\text{-}\mathtt{refl}\). Here we used lambda expressions.

It follows the same logic as when we proved reflexivity for isomorphism, except we don’t have the fourth projection.

Transitivity

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

Remark. Note how the lambda expressions now make the projections’ argument, \(v\) or \(w\), explicit. We don’t have to imagine the argument there.

Note also the difference from our previous proof of transitivity for an isomorphism: there we used the notation for function composition, e.g. \(\mathtt{fst}\ w \circ \mathtt{fst}\ v\), whereas here we’re using lambda expressions, e.g. \(\lambda\{x \to \mathtt{fst}\ w\ (\mathtt{fst}\ v\ x)\}\). It works both ways.

The first component of \(\preccurlyeq\!\text{-}\mathtt{trans}\ v\ w : A\preccurlyeq C\) is the result of applying the first projection \(\mathtt{fst}\) on it, and getting the function composition \(\mathtt{fst}\ w \circ \mathtt{fst}\ v\). That is to say, the first component of \(\preccurlyeq\!\text{-}\mathtt{trans}\ v\ w\) is the composition of the first component \(\mathtt{fst}\ v\) of \(v:A\preccurlyeq B\) and the first component \(\mathtt{fst}\ w\) of \(w:B\preccurlyeq C\). Similarly for the second component of \(\preccurlyeq\!\text{-}\mathtt{trans}\ v\ w\).

Now, the third component is, by definition, a dependent function. Suppose the term were \(v: A\preccurlyeq B\), then its third component, \(\mathtt{thrd}\ v\), is a dependent function such that, for any \(x: A\), it returns a proof of the equality type \(\mathtt{snd}\ v\ (\mathtt{fst}\ v\ x) \equiv x\).

In the present case, the third component, \(\mathtt{thrd}\ (\preccurlyeq\!\text{-}\mathtt{trans}\ v\ w)\), is a dependent function, such that, for any \(x: A\), returns proof of the equality type

\[ \mathtt{snd}\ v\ (\mathtt{snd}\ w\ (\mathtt{fst}\ w\ (\mathtt{fst}\ v\ x))) \equiv x \]

The equational chain provides the reasoning for reducing the left-hand term to the right-hand term. It’s similar to the reasoning for transitivity in the entry on isomorphism.

Antisymmetry

We know that an embedding is not symmetric. If \(A\) is embedded in \(B\), we cannot say that \(B\) is embedded in \(A\). However, what if we do have proof that both \(A\preccurlyeq B\) and \(B\preccurlyeq A\)? Does this mean that we can now claim \(A\) and \(B\) are isomorphic since we have an apparent symmetry? Not quite!

\[\begin{align*} \mathtt{fst}\ v &: A \to B\\ \mathtt{snd}\ v&: B \to A\\ \mathtt{thrd}\ v&: \prod_{x:A} \mathtt{snd}\ v\ (\mathtt{fst}\ v\ x) \equiv_A x \end{align*}\]

\[\begin{align*} \mathtt{fst}\ w &: B \to A\\ \mathtt{snd}\ w&: A \to B\\ \mathtt{thrd}\ w&: \prod_{y:B} \mathtt{snd}\ w\ (\mathtt{fst}\ w\ y) \equiv_B y \end{align*}\]

In both cases, the third component gives us proof that \(\mathtt{snd}\ v\) (respectively, \(\mathtt{snd}\ w\)) is a left inverse. To get an isomorphism, we need proof that \(\mathtt{snd}\ v\) (resp. \(\mathtt{snd}\ w\)) is also a right inverse, i.e., that \(\mathtt{fst}\ v\ (\mathtt{snd}\ v\ y) \equiv_B y\) (resp. \(\mathtt{fst}\ w\ (\mathtt{snd}\ w\ x) \equiv_A x\)). We achieve this right-inverse property of \(\mathtt{snd}\ v\) (resp. \(\mathtt{snd}\ w\)) if \(\mathtt{snd}\ v\) is the same as \(\mathtt{fst}\ w\) and \(\mathtt{snd}\ w\) is the same as \(\mathtt{fst}\ v\).

So, if we have proofs of these four types: \(A\preccurlyeq B\), \(B\preccurlyeq A\), \(\mathtt{fst}\ v \equiv \mathtt{snd}\ w\), and \(\mathtt{snd}\ v \equiv \mathtt{fst}\ w\), then we have a way to construct a proof (term) of an isomorphism type. Call the function that allows us such a construction \(\preccurlyeq\!\text{-}\mathtt{antisym}\).

≲-antisym : ∀ {A B : Set} → (v : A ≲ B) → (w : B ≲ A)
  → (fst v ≡ snd w) → (snd v ≡ fst w) → A ≃ B
≲-antisym v w r s =
  record
    { fst  = fst v
    ; snd  = snd v
    ; thrd = thrd v
    ; frth = λ{y →
        begin
          fst v (snd v y)
        ≡⟨ cong (fst v) (cong-app s y) ⟩
          fst v (fst w y)
        ≡⟨ cong-app r (fst w y) ⟩
          snd w (fst w y)
        ≡⟨ thrd w y ⟩
          y
        ∎}
    }

Again, if \(\preccurlyeq\!\text{-}\mathtt{antisym}\ v\ w\ r\ s\) is a term of type \(A\simeq B\), then it’s an isomorphism. As such, it must consist of the 4 components we met in the previous entry: 1) a function of type \(A\to B\), 2) another of type \(B\to A\), as well as proofs 3) of \(\prod_{x: A} \mathtt{snd}\ v\ (\mathtt{fst}\ v\ x) \equiv x\), and 4) of \(\prod_{y: B} \mathtt{fst}\ v\ (\mathtt{snd}\ v\ y) \equiv y\).

But this is easy! Because a term of the embedding \(A\preccurlyeq B\) has three out of the four components of a term of the isomorphism type \(A\simeq B\), we just provide them. For instance the first component of

which is also of type \(A\to B\). And so on for components two and three. But what about the fourth component? Since an embedding only has three out of the four components of an isomorphism, we must provide the reasoning that shows why \(\mathtt{fst}\ v \equiv \mathtt{snd}\ w\) and \(\mathtt{snd}\ v \equiv \mathtt{fst}\ w\) gives us the right-inverse property for \(\mathtt{snd}\ v\). This leads us to define the fourth component, \(\mathtt{frth}\ (\preccurlyeq\!\text{-}\mathtt{antisym}\ v\ w\ r\ s)\), via equational reasoning. The goal is to prove that \(\mathtt{snd}\ v\) in the right position, i.e., \(\mathtt{fst}\ v \circ \mathtt{snd}\ v\), is the identity function for \(B\). In other words, the proof is achieved by reducing the left-hand term to the right-hand term:

with the justification \(\mathtt{cong}\ (\mathtt{fst}\ v)\ (\mathtt{cong\text{-}app}\ s\ y)\). This says that, by congruence, applying the same operation, \(\mathtt{fst}\ v\), to equivalent terms (the bracketed parts) yields equivalent terms. And the proof that the bracketed terms are equivalent is provided by \(\mathtt{cong\text{-}app}\ s\ y\). Recall that \(\mathtt{cong\text{-}app}\) takes a proof that two functions are the same, in this case \(s\) is proof that \(\mathtt{snd}\ v \equiv \mathtt{fst}\ w\), and returns another function, \(\mathtt{cong\text{-}app}\ s\), that, for any \(y: B\), returns proof that the “two” functions applied to \(y\) are the same term, i.e., \(\mathtt{cong\text{-}app}\ s\ y\).

with justification \((\mathtt{cong\text{-}app}\ r\ (\mathtt{fst}\ w\ y))\). The reasoning is the same as before. \(\mathtt{cong\text{-}app}\) takes proof \(r\) that \(\mathtt{fst}\ v\) is the same as \(\mathtt{snd}\ w\). So because these two functions are the same, applied to the same term yields the same result.

Lastly, we can reduce \(\mathtt{snd}\ w\ (\mathtt{fst}\ w\ y)\) down to \(y\) because the composition of \(\mathtt{snd}\ w\) and \(\mathtt{fst}\ w\) is the very definition of \(\mathtt{thrd}\ w\)! Whew! \(\blacksquare\)