Types and Logical Connectives – II

Empty (false)

The Agda declaration for \(\bot\) (pronounced “bot” or “false”) is even stranger than for \(\top\):

data ⊥ : Set where

This simply says that \(\bot\) is a type… and that’s it. It doesn’t even get a constructor! And how could it? There’s no way to construct a term of \(\bot\), because \(\bot\) doesn’t have any. Recall that a term is also a proof, so since \(\bot\) doesn’t have any proof whatsoever, it can never be true. As its name suggests, it’s always false.

Even more oddly, although \(\bot\) doesn’t have a constructor, it does have an eliminator! Recall from last time that a type’s eliminator can be thought of as a function that allows us to use a term of that type to get a term of another type. But how can we use a term of \(\bot\) when it doesn’t have one? Let’s look at how the PLFA defines the eliminator:

⊥-elim : ∀ {A : Set} → ⊥ → A
⊥-elim ()

Oh… there’s no definition… We didn’t give \(\bot\text{-}\!\mathtt{elim}\) anything, except a pair of empty parentheses. According to the PLFA, this is called the absurd pattern, and it means that we can’t pattern-match. And if we can’t pattern match, there’s no equals sign, and if there’s no equals sign, there’s no definition. Let’s use currying to be a bit more explicit:

\[\begin{align*} \bot\text{-}\mathtt{elim}\ &: \forall\ \{ A : \mathtt{Set} \} \to \bot \to A\\ \bot\text{-}\mathtt{elim}\ &: \bot \to A\\ \bot\text{-}\mathtt{elim}\ () &: A\\ \end{align*}\]

I think I see why this rule is called ex falso.¹ Here \(A\) is any type. Therefore, were the eliminator \(\bot\text{-}\!\mathtt{elim}\) to take a term from \(\bot\) (which is impossible by definition), then we would get a term or proof of any type \(A\). In other words, if we were to have a term of an empty type, that’s a logical contradiction, and from a contradiction we can prove anything. To put it yet another way: if we can make the impossible possible, then literally anything’s possible.

Another thing to keep in mind is that, since \(A\) is any type, then we’re saying there’s a function, \(\bot\text{-}\!\mathtt{elim}\), from \(\bot\) to every type. This function is trivial, though, because it can never return a term.

Function (implication)

Say we have two types \(A\) and \(B\). Then we can freely form the type \(A\to B\). The terms of this type will be functions, i.e., mappings that take a term of \(A\) and return a term or proof of \(B\). The term constructor is the lambda operator: \(\lambda (x: A)\to\_\), which takes a term \(N: B\) containing \(x: A\) as a free variable. Thus \(\lambda (x:A) \to N\) is the term or proof of \(A\to B\). Note that this is equivalent to our previous notation of \(\lambda \{x \to N\}\), where we omit the type \(A\) for simplicity.

The function type is usually presented by giving only the eliminator or elimination rule (see this nLab entry):

→-elim : ∀ {A B : Set} → (A → B) → A → B
→-elim L M = L M

With currying:

\[\begin{align*} \to\!\text{-}\mathtt{elim} &: \forall\ \{A\ B : \mathtt{Set}\} \to (A \to B) \to A \to\! B\\ \to\!\text{-}\mathtt{elim} &: (A \to B) \to A \to B\\ \to\!\text{-}\mathtt{elim}\ f &: A \to B\\ \to\!\text{-}\mathtt{elim}\ f\ x &: B\\ \to\!\text{-}\mathtt{elim}\ f\ x &= f(x) \end{align*}\]

It’s kind of redundant, isn’t it? The term \(\to\!\text{-}\mathtt{elim}\ f\ x\) turns out just to be the function application \(f(x)\).

Note that this resembles the logical rule of modus ponens:

That is, if the implication \(A\to B\) holds, and \(A\) holds, then \(B\) must hold. In type-theoretical terms, if we have a term (a function) of type \(A\to B\) that takes proof of type \(A\) and returns proof of type \(B\), and we apply it to a proof of type \(A\), then it must give us a proof of type \(B\)! This means that the function type \(A\to B\) is equivalent to logical implication!

Do we have eta equality? Yes, indeed: elimination followed by introduction gives us back the original term:

η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
η-→ f = refl

Let’s see: we’ve just seen that elimination is just function application, so applying the rule gave us \(f(x)\) of type \(B\). Introduction is done with a lambda operator of the form \(\lambda (x:A) \to N\), where \(N\) (of type \(B\)) is a term containing a variable \(x\) from \(A\). Then substitute \(N\) with \(f(x)\), and we get \(\lambda (x:A)\to f(x)\). But this is just the definition of \(f\)! In other words, \((x:A)\mapsto f(x)\) is the (anonymous) function that maps \(x\) to \(f(x)\), while the (named) function \(f\) takes \(x\) and returns \(f(x)\). We’re just repeating ourselves at this point. So let’s move on.

Implication and exponentials

The type \(A\to B\) can also be viewed as the “space” of functions from \(A\) to \(B\), which is usually denoted \(B^A\), and called the exponential object.

If we adopt this alternative view, then the law of exponentials, \((p^n)^m \equiv p^{(n \ast m)}\), should hold in type theory. That is, \((C^B)^A \equiv C^{(A\times B)}\) should translate to \(A\to (B\to C) \cong (A\times B) \to C\). And indeed it does! We’ve been doing this all along.

Currying (again)

We’ve been currying throughout these notes: instead of saying “a function that returns a function that returns a value”, for the sake of simplicity we just say “a function that takes two arguments and returns a value”. In other words, we take the function \(A \to B \to C\) to mean \(A\times B \to C\). Well, now we can prove that these two are isomorphic! We’ll call our proof (our isomorphism) \(\mathtt{curr}\):

curr : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
curr =
  record
    { fst  =  λ{ f → λ{ ⟨ x , y ⟩ → f x y }}
    ; snd  =  λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}}
    ; thrd =  λ{ f → refl }
    ; frth =  λ{ g → refl }
    }

Since \(\mathtt{curr}\) is an isomorphism, it must consist of a 4 tuple of components, which we can get through the usual projections \(\mathtt{fst}\), \(\mathtt{snd}\), \(\mathtt{thrd}\) and \(\mathtt{frth}\):

curr : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
curr =
  record
    { fst  (curr) =  λ{ f → λ{ ⟨ x , y ⟩ → f x y }}
    ; snd  (curr) =  λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}}
    ; thrd (curr) =  λ{ f → refl }
    ; frth (curr) =  λ{ g → refl }
    }

On the left-hand side of the isomorphism symbol, we have the type of functions \(A \to (B \to C)\), that is to say functions \(f\) from \(A\) to \(B\to C\). Take one of these functions and give it a term \(x:A\). Then it will return a function \(f(x)\) of type \(B\to C\), such that, given a term \(y:B\), returns a term of type \(C\), namely, \(f(x)(y)\) (or, more simply, \(f(x,y)\)). On the right-hand side, we have the type \((A\times B) \to C\) of functions \(g\) that take a term of type \(A\times B\), i.e., a pair \((x,y)\), and return a term \(g(x,y)\) of type \(C\).

It’s easy to see how \(A \to (B\to C)\) and \((A\times B) \to C\) are equivalent. The first component of the isomorphism \(\mathtt{curr}\), obtained by applying the first projection \(\mathtt{fst}\) on it, must be a function from \(A\to (B\to C)\) to \((A\times B) \to C\). That is, \(\mathtt{fst (curr)}\) must be a function that maps functions \(f\) to a function that maps pairs \((x,y)\) to \(f(x,y)\):

\[\begin{align*} \mathtt{fst (curr)} &: (A \to (B \to C)) \to ((A\times B) \to C)\\ \mathtt{fst (curr)} & = \lambda \{ f \to \lambda \{ (x,y) \to f\ x\ y \}\} \\ \mathtt{fst (curr)}\ f & = \lambda \{ (x,y) \to f\ x\ y \} \\ \mathtt{fst (curr)}\ f (x,y) & = f( x, y ) \end{align*}\]

The second component of the isomorphism \(\mathtt{snd (curr)}\) must be a function that maps a function \(g\) of type \((A\times B) \to C\) to a function of type \(A\to (B\to C)\) that maps a term \(x:A\) to a function that maps \(y:B\) to the value \(g(x,y)\):

\[\begin{align*} \mathtt{snd (curr)} &: ((A\times B) \to C) \to (A\to (B\to C))\\ \mathtt{snd (curr)} &= \lambda \{ g \to \lambda \{x \to \lambda \{ y \to g ( x,y) \}\}\} \\ \mathtt{snd (curr)} g &= \lambda \{x \to \lambda \{ y \to g ( x,y) \}\} \\ \mathtt{snd (curr)} g\ x &= \lambda \{ y \to g ( x,y) \} \\ \mathtt{snd (curr)} g (x, y) &= g ( x,y) \end{align*}\]

The third and fourth components of the isomorphism \(\mathtt{curr}\) are dependent functions that map to an equality:

\[\begin{align*} \mathtt{thrd (curr)} &: \prod_{f: A\to (B\to C)} \mathtt{snd (curr)}\ ( \mathtt{fst (curr)}\ f) \equiv f \end{align*}\]

\[\begin{align*} \mathtt{frth (curr)} &: \prod_{g: (A\times B) \to C} \mathtt{fst (curr)}\ ( \mathtt{snd (curr)}\ g) \equiv g \end{align*}\]

That the left-hand side of the equality can be reduced to the right-hand side should be easy to see:

\[ \mathtt{fst(curr)}\ f = \lambda \{ (x,y) \to f\ x\ y \} \]

We apply \(\mathtt{snd(curry)}\) to it:

\[ \big( \lambda \{ g \to \lambda \{x \to \lambda \{ y \to g ( x,y) \}\}\} \big) \big( \mathtt{fst(curr)}\ f \big) \]

This becomes:

\[ \lambda\{x \to \lambda\{y \to \mathtt{fst(curr)}\ f(x,y) \}\} \]

But we know that \(\mathtt{fst(curr)}\ f(x,y)\) is just \(f(x,y)\). So now we have \(\mathtt{snd(curr)} f\) is:

\[ \lambda \{x \to \lambda\{y \to f(x,y) \}\} \]

Evaluating at \(x: A\) and \(y:B\), we have that \(\mathtt{snd(curr)} f(x,y) = f(x,y)\). Therefore, \(\mathtt{snd(curr)} f \equiv f\).

Similar reasoning applies to the fourth component of the isomorphism.

Product rule

There’s also the product rule for exponents: \(p^{(n+m)} \equiv p^n \ast p^m\). Does this hold in our type theory? Yes! We can translate the exponential notation \(C^{(A+B)} \equiv C^A \ast C^B\) to:

\[ (A\uplus B) \to C \cong (A\to C) \times (B\to C) \]

The Agda proof is as follows:

→-dist-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
→-dist-⊎ =
  record
    { fst  = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ }
    ; snd  = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }
    ; thrd = λ{ f → extens λ{ (inj₁ x) → refl ; (inj₂ y) → refl } }
    ; frth = λ{ y → refl }
    }

Again, the isomorphism \(\to\!\text{-}\mathtt{dist}\text{-}\uplus\) is a 4-tuple. The first component, obtained by applying the projection \(\mathtt{fst}\) to \(\to\!\text{-}\mathtt{dist}\text{-}\uplus\), is a function that maps a function \(f: A\uplus B \to C\) to a term of type \((A\to C) \times (B \to C)\). Since the latter is a product, its terms are pairs, the first component of which is a function of type \(A\to C\) and the second component of type \(B\to C\). Now, recall that a term of type \(A\uplus B\) is constructed with either \(inj_1\) applied to terms of \(A\) or \(inj_2\) applied to terms of \(B\). Therefore, the output of \(f: A\uplus B \to C\) is either \(f\circ inj_1: A \to C\) or \(f\circ inj_2: B \to C\). But these are, respectively, the components of the term \((f\circ inj_1, f\circ inj_2): (A\to C) \times (B\to C)\). Therefore, \(\mathtt{fst} (\to\!\text{-}\mathtt{dist}\text{-}\uplus)\) is a function that maps a function \(f\) to \((f\circ inj_1, f\circ inj_2)\).

The second component, \(\mathtt{snd}(\to\!\text{-}\mathtt{dist}\text{-}\uplus)\) is a function that maps a term of \((A\to C) \times (B \to C)\) to a term of \(A\uplus B \to C\). Let’s say a term of the former is \((g,h)\), where \(g: A \to C\) and \(h: B\to C\), whereas a term of the latter is going to be a function that maps a term of \(A\uplus B\) to \(C\). But a term of \(A\uplus B\) is going to depend on the constructor. We can make it so that the function of type \(A\uplus B\) takes \(inj_1(x)\) and sends it to \(g(x)\) or takes \(inj_2(y)\) and sends it to \(h(y)\). Therefore, the component \(\mathtt{snd}(\to\!\text{-}\mathtt{dist}\text{-}\uplus)\) is a function mapping \((g,h)\) to a function with the mapping \(inj_1(x) \mapsto g(x)\) or \(inj_2(y) \mapsto h(y)\). In lambda notation: \(\lambda \{ (inj_1\ x) \to g\ x ; (inj_2\ y) \to h\ y\}\).

Function extensionality

To save myself some typing and make the following a bit more readable, I’m going to abbreviate \(\mathtt{fst}(\to\!\text{-}\mathtt{dist}\text{-}\uplus)\) to \(\mathtt{fst}\), and I’ll do the same for the other components. I think by now I’ve made it perfectly clear that \(\mathtt{fst}\) and the others are actually projections and not components themselves, so there should be no confusion. Anyway, the third component has the following type:

\[ \prod_{f: A\uplus B \to C} \mathtt{snd}\ (\mathtt{fst}\ f) \equiv f \]

That is to say, it’s a function that maps any \(f: A\uplus B \to C\) to proof that the term on the left is equal to the term on the right, or that the composition acts like the identity.

We know that:

\[ \mathtt{fst}\ f = \langle f \circ inj_1, f \circ inj_2 \rangle \]

Now, apply \(\mathtt{snd}\) on it:

\[ \mathtt{snd}(\mathtt{fst}\ f) = \lambda \{inj_1\ x \to (f\circ inj_1)\ x\ ; inj_2\ y\to (f \circ inj_2)\ y\} \]

Applying the composition according to its definition:

\[ \mathtt{snd}(\mathtt{fst}\ f) = \lambda \{inj_1\ x \to f (inj_1\ x)\ ; inj_2\ y\to f (inj_2\ y)\} \]

So \(\mathtt{snd}( \mathtt{fst}\ f)\) is a function that maps either a term \(inj_1\ x: A\uplus B\) to a term \(f(inj_1\ x): C\), or a term \(inj_2\ y: A\uplus B\) to a term \(f(inj_2\ y): C\). But this is none other than \(f: A\uplus B \to C\). Therefore \(\mathtt{snd}( \mathtt{fst}\ f) \equiv f\).

In short, the type of the third component is equivalently:

\[ \prod_{f: A\uplus B \to C} f \equiv f \]

And so it’s a function sending \(f\)’s to \(\mathtt{refl}\).

Note that I followed roughly the same process as for the third component of \(\mathtt{curr}\). I’ve stared at this for a long while, and I think it’s correct. The process is so simple that you’d think Agda would be able to make the reduction of \(\mathtt{snd}(\mathtt{fst}\ f)\) to \(f\) quite easily, such that we could simply say that the third component \(\mathtt{thrd}\) maps \(f\) to \(\mathtt{refl}\). But if you actually try that, you will get a compilation error! See for yourself:

I don’t understand the substitutions that Agda is doing here. In the following, I’ll try to go through what I think it’s doing.

Well start by expanding the components according to their definition. This is going to get a little tricky, so hold on! First, the first component \(\mathtt{fst}\) applied to \(f\):

\[ (\mathtt{fst})\ f = (\lambda \{ f \to \langle f \circ inj_1, f \circ inj_2\rangle \})\ f \]

Here, I would start evaluating the lambda function with \(f\), but Agda doesn’t seem to do that. So we continue like this. We replace the compositions inside the body of the lambda with their definitions:

\[ (\mathtt{fst})\ f = (\lambda \{ f \to \langle \lambda \{ x \to f (inj_1\ x)\}, \lambda \{y \to f (inj_2\ y)\}\rangle )\ f \]

Again, here I’d evaluate… but we won’t. We now apply \(\mathtt{snd}\) to the above:

\[\begin{align*} \mathtt{snd}\ (\mathtt{fst}\ f) = \lambda &\{ (inj_1\ x)\\ &\to (\lambda \{ f \to \langle \lambda \{ x_1 \to f (inj_1\ x_1)\}, \lambda \{x_1 \to f (inj_2\ x_1)\}\rangle\} )\ f \\ &; (inj_2\ y)\\ &\to (\lambda \{ f \to \langle \lambda \{ x \to f (inj_1\ x)\}, \lambda \{x \to f (inj_2\ x)\}\rangle\})\ f\\ &\} \end{align*}\]

Up to here, the notation resembles Agda’s code (the upper part), but you’ll notice a subtle change: whereas before we had \(inj_1\ x\), Agda has put \(inj_1\ x_1\). I believe it has done this variable name change to avoid “variable capture”. But surprisingly it has used that same variable for \(inj_2\)! That does not make sense to me. The injections are supposed to take terms of different types. Why are we giving them the same variable?

Also, recall that, according to its definition, \(\mathtt{snd} \langle g , h \rangle\) is a function sending \(inj_1\ x\) to \(g\ x\), where \(g\) is the first element in the pair \(\langle g, h\rangle\). So, I would have thought that \(\mathtt{snd}\), taking \((\mathtt{fst}\ f)\), which is a pair, would be a function sending \(inj_1\) to the composite \(f(inj_1\ x)\)—the first element of the pair. But that’s not what Agda is doing. Instead, \(\mathtt{snd}(\mathtt{fst}\ f)\) sends \(inj_1\ x\) to \((\lambda \{ f \to \langle \lambda \{ x \to f (inj_1\ x)\}, \lambda \{y \to f (inj_2\ y)\}\rangle )\ f\). And, weirdly, it also throws in a \(\mathtt{proj_1}\ x\) that it seemingly pulls out of nowhere.

So, who knows what’s really going on here. Since I’m learning to use Agda as I write these notes, I’m not proficient enough in its internals to assess why it tries to make the reduction this way, that is, in a way that fails.

The PLFA says that we need function extensionality as a postulate here. But I’m not sure why, since we didn’t need it when tackling the third component of \(\mathtt{curr}\). But, anyway, here goes:

postulate
  extens : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g

Given any two types \(A\) and \(B\), and any two parallel functions \(f\) and \(g\) from \(A\) to \(B\), if we have proof that the values \(f(x)\) and \(g(x)\) are the same, for every \(x:A\), then \(\mathtt{extens}\) takes that proof and returns proof that \(f\) and \(g\) are the same function:

\[ \mathtt{extens} : \big(\prod_{x:A} (f\ x \equiv g\ x)\big) \to (f \equiv g) \]

Let \(h\) be a proof that \(\prod_{x:A} (f\ x\equiv g\ x)\). Then \(\mathtt{extens}(h)\) is proof that \(f\equiv g\). Of course, \(h\) is a named function, but we can also pass an anonymous one, e.g., \(\mathtt{extens}(\lambda x \to \mathtt{refl}): f\equiv g\).

Let’s recap: The third component \(\mathtt{thrd}\) should take \(f\) and map it to a proof of the equality type \(\mathtt{snd}\ (\mathtt{fst}\ f) \equiv f\). Since we cannot use \(\mathtt{refl}\), for whatever reason, then we have to use \(\mathtt{extens}\). But what exactly do we pass to \(\mathtt{extens}\)? We must give it proof that \(\mathtt{snd}\ (\mathtt{fst}\ f)\ w \equiv f\ w\), for every \(w: A\uplus B\).

\[ \mathtt{extens} : \big(\prod_{w:A\uplus B} \mathtt{snd}\ (\mathtt{fst}\ f)\ w\equiv f\ w\big) \to \mathtt{snd}\ (\mathtt{fst}\ f) \equiv f \]

That proof we can pass as an anonymous function \(\lambda \{ w \to \mathtt{refl}\}\). BUT… since \(w\) could be constructed with either \(inj_1\) or \(inj_2\), we should really give it \(\lambda \{ inj_1(x) \to \mathtt{refl} ; inj_2(y) \to \mathtt{refl} \}\). So, at long last, we have:

\[ \mathtt{thrd} = \lambda \{ f \to \mathtt{extens}\ (\lambda\{ inj_1(x) \to \mathtt{refl} ; inj_2(y)\to \mathtt{refl} \}) \} \]

And now Agda accepts this. Again, as to why this works, I’m going to have to leave for another time.

Three down, one more to go…

The fourth component has the type:

\[ \prod_{y: (A\to C) \times (B \to C)} \mathtt{fst}\ ( \mathtt{snd}\ y) \equiv y\]

Note that \(y\) is a pair of functions, but itself is not a function, so we don’t need extensionality here. Let \(y\) be \(\langle g, h\rangle\), a pair of functions of type \(A\to C\) and \(B\to C\).

So here’s \(\mathtt{snd}\ y\):

\[ (\lambda \{\langle g,h\rangle \to \lambda\{ (inj_1\ x) \to g\ x; (inj_2\ y) \to h\ y\}\}) \langle g,h \rangle \]

Which reduces to:

\[ \lambda\{ (inj_1 x) \to g\ x; (inj_2 y) \to h\ y\} = f \]

The only thing left is to apply \(\mathtt{fst}\) to it, but we already know that \(\mathtt{fst}\ f\) is \(\langle f \circ inj_1 ; f\circ inj_2 \rangle\), i.e., \(\langle g , h \rangle\).

So the type of the fourth component is equivalently:

\[ \prod_{y: (A\to C) \times (B \to C)} y \equiv y\]

And this time we can say that it’s a function mappig \(y\)’s to \(\mathtt{refl}\) and Agda doesn’t complain.