---
title : "Connectives: Conjunction, disjunction, and implication"
permalink : /Connectives/
---
```agda
module plfa.part1.Connectives where
```
This chapter introduces the basic logical connectives, by observing a
correspondence between connectives of logic and data types, a
principle known as _Propositions as Types_:
* _conjunction_ is _product_,
* _disjunction_ is _sum_,
* _true_ is _unit type_,
* _false_ is _empty type_,
* _implication_ is _function space_.
## Imports
```agda
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality; _⇔_)
open plfa.part1.Isomorphism.≃-Reasoning
```
## Conjunction is product
Given two propositions `A` and `B`, the conjunction `A × B` holds
if both `A` holds and `B` holds. We formalise this idea by
declaring a suitable datatype:
```agda
record _×_ (A B : Set) : Set where
constructor ⟨_,_⟩
field
proj₁ : A
proj₂ : B
open _×_
```
Evidence that `A × B` holds is of the form `⟨ M , N ⟩`, where `M`
provides evidence that `A` holds and `N` provides evidence that `B`
holds.
The record construction `record { proj₁ = M ; proj₂ = N }` corresponds to the
term `⟨ M , N ⟩` where `M` is a term of type `A` and `N` is a term of type `B`.
The constructor declaration allows us to write `⟨ M , N ⟩` in place of the
record construction.
Given evidence that `A × B` holds, we can conclude that both
`A` holds and `B` holds, using the projections `proj₁` and `proj₂` respectively.
If `L` provides evidence that `A × B` holds, then `proj₁ L` provides evidence
that `A` holds, and `proj₂ L` provides evidence that `B` holds.
When `⟨_,_⟩` appears in a term on the right-hand side of an equation
we refer to it as a _constructor_, and when it appears in a pattern on
the left-hand side of an equation we refer to it as a _destructor_.
We may also refer to `proj₁` and `proj₂` as destructors, since they
play a similar role.
Other terminology refers to `⟨_,_⟩` as _introducing_ a conjunction, and
to `proj₁` and `proj₂` as _eliminating_ a conjunction; indeed, the
former is sometimes given the name `×-I` and the latter two the names
`×-E₁` and `×-E₂`. As we read the rules from top to bottom,
introduction and elimination do what they say on the tin: the first
_introduces_ a formula for the connective, which appears in the
conclusion but not in the hypotheses; the second _eliminates_ a
formula for the connective, which appears in a hypothesis but not in
the conclusion. An introduction rule describes under what conditions
we say the connective holds---how to _define_ the connective. An
elimination rule describes what we may conclude when the connective
holds---how to _use_ the connective.[^from-wadler-2015]
Applying each destructor and reassembling the results with the
constructor is the identity over products:
```agda
η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× w = refl
```
For record types, η-equality holds *by definition*.
While proving `η-×`, we do not have to
pattern match on `w` to know that η-equality holds.
We set the precedence of conjunction so that it binds less
tightly than anything save disjunction:
```agda
infixr 2 _×_
```
Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)`.
Alternatively, we can declare conjunction as a data type,
and the projections as functions using pattern matching.
```agda
data _×′_ (A B : Set) : Set where
⟨_,_⟩′ :
A
→ B
-----
→ A ×′ B
proj₁′ : ∀ {A B : Set}
→ A ×′ B
-----
→ A
proj₁′ ⟨ x , y ⟩′ = x
proj₂′ : ∀ {A B : Set}
→ A ×′ B
-----
→ B
proj₂′ ⟨ x , y ⟩′ = y
```
The record type `_×_` and the data type `_×′_` behave similarly. One
difference is that for for record
types, η-equality holds *by definition*,
but for data types have to
pattern match know that η-equality holds:
```agda
η-×′ : ∀ {A B : Set} (w : A ×′ B) → ⟨ proj₁′ w , proj₂′ w ⟩′ ≡ w
η-×′ ⟨ x , y ⟩′ = refl
```
The pattern matching on the left-hand side is essential, since
replacing `w` by `⟨ x , y ⟩′` allows both sides of the
propositional equality to simplify to the same term.
It is convenient to have η-equality *definitionally*,
so we use records in preference to data types
whenever there is only one constructor.
Given two types `A` and `B`, we refer to `A × B` as the
_product_ of `A` and `B`. In set theory, it is also sometimes
called the _Cartesian product_, and in computing it corresponds
to a _record_ type. Among other reasons for
calling it the product, note that if type `A` has `m`
distinct members, and type `B` has `n` distinct members,
then the type `A × B` has `m * n` distinct members.
For instance, consider a type `Bool` with two members, and
a type `Tri` with three members:
```agda
data Bool : Set where
true : Bool
false : Bool
data Tri : Set where
aa : Tri
bb : Tri
cc : Tri
```
Then the type `Bool × Tri` has six members:
⟨ true , aa ⟩ ⟨ true , bb ⟩ ⟨ true , cc ⟩
⟨ false , aa ⟩ ⟨ false , bb ⟩ ⟨ false , cc ⟩
For example, the following function enumerates all
possible arguments of type `Bool × Tri`:
```agda
×-count : Bool × Tri → ℕ
×-count ⟨ true , aa ⟩ = 1
×-count ⟨ true , bb ⟩ = 2
×-count ⟨ true , cc ⟩ = 3
×-count ⟨ false , aa ⟩ = 4
×-count ⟨ false , bb ⟩ = 5
×-count ⟨ false , cc ⟩ = 6
```
Product on types also shares a property with product on numbers in
that there is a sense in which it is commutative and associative. In
particular, product is commutative and associative _up to
isomorphism_.
For commutativity, the `to` function swaps a pair, taking `⟨ x , y ⟩` to
`⟨ y , x ⟩`, and the `from` function does the same (up to renaming).
```agda
×-comm : ∀ {A B : Set} → A × B ≃ B × A
×-comm =
record
{ to = λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
; from = λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
; from∘to = λ{ w → refl }
; to∘from = λ{ w → refl }
}
```
Being _commutative_ is different from being _commutative up to
isomorphism_. Compare the two statements:
m * n ≡ n * m
A × B ≃ B × A
In the first case, we might have that `m` is `2` and `n` is `3`, and
both `m * n` and `n * m` are equal to `6`. In the second case, we
might have that `A` is `Bool` and `B` is `Tri`, and `Bool × Tri` is
_not_ the same as `Tri × Bool`. But there is an isomorphism between
the two types. For instance, `⟨ true , aa ⟩`, which is a member of the
former, corresponds to `⟨ aa , true ⟩`, which is a member of the latter.
For associativity, the `to` function reassociates two uses of pairing,
taking `⟨ ⟨ x , y ⟩ , z ⟩` to `⟨ x , ⟨ y , z ⟩ ⟩`, and the `from` function does
the inverse.
```agda
×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
×-assoc =
record
{ to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ }
; from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ }
; from∘to = λ{ w → refl }
; to∘from = λ{ w → refl }
}
```
Being _associative_ is not the same as being _associative
up to isomorphism_. Compare the two statements:
(m * n) * p ≡ m * (n * p)
(A × B) × C ≃ A × (B × C)
For example, the type `(ℕ × Bool) × Tri` is _not_ the same as `ℕ ×
(Bool × Tri)`. But there is an isomorphism between the two types. For
instance `⟨ ⟨ 1 , true ⟩ , aa ⟩`, which is a member of the former,
corresponds to `⟨ 1 , ⟨ true , aa ⟩ ⟩`, which is a member of the latter.
#### Exercise `⇔≃×` (practice)
Show that `A ⇔ B` as defined [earlier](/Isomorphism/#iff)
is isomorphic to `(A → B) × (B → A)`.
```agda
-- Your code goes here
open import plfa.part1.Isomorphism using (_⇔_)
⇔≃× : ∀ {A B : Set} → A ⇔ B ≃ (A → B) × (B → A)
⇔≃× = record
{ to = λ a → ⟨ _⇔_.to a , _⇔_.from a ⟩
; from = λ ab → record { to = proj₁ ab ; from = proj₂ ab }
; from∘to = λ _ → refl
; to∘from = λ _ → refl
}
```
## Truth is unit
Truth `⊤` always holds. We formalise this idea by
declaring the empty record type.
```agda
record ⊤ : Set where
constructor tt
```
Evidence that `⊤` holds is of the form `tt`.
The record construction `record {}` corresponds to the term `tt`. The
constructor declaration allows us to write `tt`.
There is an introduction rule, but no elimination rule.
Given evidence that `⊤` holds, there is nothing more of interest we
can conclude. Since truth always holds, knowing that it holds tells
us nothing new.
The nullary case of `η-×` is `η-⊤`.
While proving `η-⊤`, we do not have to pattern match on `w`---Agda *knows* it
is equal to `tt`:
```agda
η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ w = refl
```
Agda knows that *any* value of type `⊤` must be `tt`, so any time we need a
value of type `⊤`, we can tell Agda to figure it out:
```agda
truth : ⊤
truth = _
```
Alternatively, we can declare truth as a data type:
```agda
data ⊤′ : Set where
tt′ :
--
⊤′
```
As with the product, the record type `⊤` and the data type `⊤′` behave
similarly, but while η-equality holds *by definition* for the record type,
it does not for the data type, so we need to pattern match on `w`:
```agda
η-⊤′ : ∀ (w : ⊤′) → tt′ ≡ w
η-⊤′ tt′ = refl
```
The pattern matching on the left-hand side is essential. Replacing
`w` by `tt′` allows both sides of the propositional equality to
simplify to the same term.
As with products, it is convenient to have η-equality *definitionally*,
so we use records in preference to data types
whenever there is only one constructor.
We refer to `⊤` as the _unit_ type. And, indeed,
type `⊤` has exactly one member, `tt`. For example, the following
function enumerates all possible arguments of type `⊤`:
```agda
⊤-count : ⊤ → ℕ
⊤-count tt = 1
```
For numbers, one is the identity of multiplication. Correspondingly,
unit is the identity of product _up to isomorphism_. For left
identity, the `to` function takes `⟨ tt , x ⟩` to `x`, and the `from`
function does the inverse. The evidence of left inverse requires
matching against a suitable pattern to enable simplification:
```agda
⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
⊤-identityˡ =
record
{ to = λ{ ⟨ tt , x ⟩ → x }
; from = λ{ x → ⟨ tt , x ⟩ }
; from∘to = λ{ ⟨ tt , x ⟩ → refl }
; to∘from = λ{ x → refl }
}
```
Having an _identity_ is different from having an identity
_up to isomorphism_. Compare the two statements:
1 * m ≡ m
⊤ × A ≃ A
In the first case, we might have that `m` is `2`, and both
`1 * m` and `m` are equal to `2`. In the second
case, we might have that `A` is `Bool`, and `⊤ × Bool` is _not_ the
same as `Bool`. But there is an isomorphism between the two types.
For instance, `⟨ tt , true ⟩`, which is a member of the former,
corresponds to `true`, which is a member of the latter.
Right identity follows from commutativity of product and left identity:
```agda
⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
⊤-identityʳ {A} =
≃-begin
(A × ⊤)
≃⟨ ×-comm ⟩
(⊤ × A)
≃⟨ ⊤-identityˡ ⟩
A
≃-∎
```
Here we have used a chain of isomorphisms, analogous to that used for
equality.
## Disjunction is sum
Given two propositions `A` and `B`, the disjunction `A ⊎ B` holds
if either `A` holds or `B` holds. We formalise this idea by
declaring a suitable inductive type:
```agda
data _⊎_ (A B : Set) : Set where
inj₁ :
A
-----
→ A ⊎ B
inj₂ :
B
-----
→ A ⊎ B
```
Evidence that `A ⊎ B` holds is either of the form `inj₁ M`, where `M`
provides evidence that `A` holds, or `inj₂ N`, where `N` provides
evidence that `B` holds.
Given evidence that `A → C` and `B → C` both hold, then given
evidence that `A ⊎ B` holds we can conclude that `C` holds:
```agda
case-⊎ : ∀ {A B C : Set}
→ (A → C)
→ (B → C)
→ A ⊎ B
-----------
→ C
case-⊎ f g (inj₁ x) = f x
case-⊎ f g (inj₂ y) = g y
```
Pattern matching against `inj₁` and `inj₂` is typical of how we exploit
evidence that a disjunction holds.
When `inj₁` and `inj₂` appear on the right-hand side of an equation we
refer to them as _constructors_, and when they appear on the
left-hand side we refer to them as _destructors_. We also refer to
`case-⊎` as a destructor, since it plays a similar role. Other
terminology refers to `inj₁` and `inj₂` as _introducing_ a
disjunction, and to `case-⊎` as _eliminating_ a disjunction; indeed
the former are sometimes given the names `⊎-I₁` and `⊎-I₂` and the
latter the name `⊎-E`.
Applying the destructor to each of the constructors is the identity:
```agda
η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w
η-⊎ (inj₁ x) = refl
η-⊎ (inj₂ y) = refl
```
More generally, we can also throw in an arbitrary function from a disjunction:
```agda
uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) →
case-⊎ (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
uniq-⊎ h (inj₁ x) = refl
uniq-⊎ h (inj₂ y) = refl
```
The pattern matching on the left-hand side is essential. Replacing
`w` by `inj₁ x` allows both sides of the propositional equality to
simplify to the same term, and similarly for `inj₂ y`.
We set the precedence of disjunction so that it binds less tightly
than any other declared operator:
```agda
infixr 1 _⊎_
```
Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
Given two types `A` and `B`, we refer to `A ⊎ B` as the
_sum_ of `A` and `B`. In set theory, it is also sometimes
called the _disjoint union_, and in computing it corresponds
to a _variant record_ type. Among other reasons for
calling it the sum, note that if type `A` has `m`
distinct members, and type `B` has `n` distinct members,
then the type `A ⊎ B` has `m + n` distinct members.
For instance, consider a type `Bool` with two members, and
a type `Tri` with three members, as defined earlier.
Then the type `Bool ⊎ Tri` has five
members:
inj₁ true inj₂ aa
inj₁ false inj₂ bb
inj₂ cc
For example, the following function enumerates all
possible arguments of type `Bool ⊎ Tri`:
```agda
⊎-count : Bool ⊎ Tri → ℕ
⊎-count (inj₁ true) = 1
⊎-count (inj₁ false) = 2
⊎-count (inj₂ aa) = 3
⊎-count (inj₂ bb) = 4
⊎-count (inj₂ cc) = 5
```
Sum on types also shares a property with sum on numbers in that it is
commutative and associative _up to isomorphism_.
#### Exercise `⊎-comm` (recommended)
Show sum is commutative up to isomorphism.
```agda
-- Your code goes here
⊎-comm : ∀ {A B : Set} → A ⊎ B ≃ B ⊎ A
⊎-comm = record
{ to = λ a+b → case-⊎ inj₂ inj₁ a+b
; from = λ b+a → case-⊎ inj₂ inj₁ b+a
; from∘to = λ
{ (inj₁ _) → refl
; (inj₂ _) → refl
}
; to∘from = λ
{ (inj₁ _) → refl
; (inj₂ _) → refl
}
}
```
#### Exercise `⊎-assoc` (practice)
Show sum is associative up to isomorphism.
```agda
-- Your code goes here
⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
⊎-assoc = record
{ to = λ
{ (inj₁ (inj₁ x)) → inj₁ x
; (inj₁ (inj₂ x)) → inj₂ (inj₁ x)
; (inj₂ x) → inj₂ (inj₂ x)
}
; from = λ
{ (inj₁ x) → inj₁ (inj₁ x)
; (inj₂ (inj₁ x)) → inj₁ (inj₂ x)
; (inj₂ (inj₂ x)) → inj₂ x
}
; from∘to = λ
{ (inj₁ (inj₁ x)) → refl
; (inj₁ (inj₂ x)) → refl
; (inj₂ x) → refl
}
; to∘from = λ
{ (inj₁ x) → refl
; (inj₂ (inj₁ x)) → refl
; (inj₂ (inj₂ x)) → refl
}
}
```
## False is empty
False `⊥` never holds. We formalise this idea by declaring
a suitable inductive type:
```agda
data ⊥ : Set where
-- no clauses!
```
There is no possible evidence that `⊥` holds.
Dual to `⊤`, for `⊥` there is no introduction rule but an elimination rule.
Since false never holds, knowing that it holds tells us we are in a
paradoxical situation. Given evidence that `⊥` holds, we might
conclude anything! This is a basic principle of logic, known in
medieval times by the Latin phrase _ex falso_, and known to children
through phrases such as "if pigs had wings, then I'd be the Queen of
Sheba". We formalise it as follows:
```agda
⊥-elim : ∀ {A : Set}
→ ⊥
--
→ A
⊥-elim ()
```
This is our first use of the _absurd pattern_ `()`.
Here since `⊥` is a type with no members, we indicate that it is
_never_ possible to match against a value of this type by using
the pattern `()`.
The nullary case of `case-⊎` is `⊥-elim`. By analogy,
we might have called it `case-⊥`, but chose to stick with the name
in the standard library.
The nullary case of `uniq-⊎` is `uniq-⊥`, which asserts that `⊥-elim`
is equal to any arbitrary function from `⊥`:
```agda
uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
uniq-⊥ h ()
```
Using the absurd pattern asserts there are no possible values for `w`,
so the equation holds trivially.
We can also use `()` in nested patterns. For instance,
`⟨ () , tt ⟩` is a pattern of type `⊥ × ⊤`.
We refer to `⊥` as the _empty_ type. And, indeed,
type `⊥` has no members. For example, the following function
enumerates all possible arguments of type `⊥`:
```agda
⊥-count : ⊥ → ℕ
⊥-count ()
```
Here again the absurd pattern `()` indicates that no value can match
type `⊥`.
For numbers, zero is the identity of addition. Correspondingly, empty
is the identity of sums _up to isomorphism_.
#### Exercise `⊥-identityˡ` (recommended)
Show empty is the left identity of sums up to isomorphism.
```agda
-- Your code goes here
⊥-identityˡ : {A : Set} → ⊥ ⊎ A ≃ A
⊥-identityˡ = record
{ to = λ{ (inj₁ ()); (inj₂ a) → a }
; from = inj₂
; from∘to = λ
{ (inj₁ ())
; (inj₂ a) → refl
}
; to∘from = λ _ → refl
}
```
#### Exercise `⊥-identityʳ` (practice)
Show empty is the right identity of sums up to isomorphism.
```agda
-- Your code goes here
⊥-identityʳ : {A : Set} → A ⊎ ⊥ ≃ A
⊥-identityʳ = record
{ to = λ{ (inj₁ a) → a; (inj₂ ()) }
; from = inj₁
; from∘to = λ
{ (inj₁ a) → refl
; (inj₂ ())
}
; to∘from = λ _ → refl
}
```
## Implication is function {#implication}
Given two propositions `A` and `B`, the implication `A → B` holds if
whenever `A` holds then `B` must also hold. We formalise implication using
the function type, which has appeared throughout this book.
Evidence that `A → B` holds is of the form
λ (x : A) → N
where `N` is a term of type `B` containing as a free variable `x` of type `A`.
Given a term `L` providing evidence that `A → B` holds, and a term `M`
providing evidence that `A` holds, the term `L M` provides evidence that
`B` holds. In other words, evidence that `A → B` holds is a function that
converts evidence that `A` holds into evidence that `B` holds.
Put another way, if we know that `A → B` and `A` both hold,
then we may conclude that `B` holds:
```agda
→-elim : ∀ {A B : Set}
→ (A → B)
→ A
-------
→ B
→-elim L M = L M
```
In medieval times, this rule was known by the name _modus ponens_.
It corresponds to function application.
Defining a function, with a named definition or a lambda abstraction,
is referred to as _introducing_ a function,
while applying a function is referred to as _eliminating_ the function.
Elimination followed by introduction is the identity:
```agda
η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
η-→ f = refl
```
Implication binds less tightly than any other operator. Thus, `A ⊎ B →
B ⊎ A` parses as `(A ⊎ B) → (B ⊎ A)`.
Given two types `A` and `B`, we refer to `A → B` as the _function_
space from `A` to `B`. It is also sometimes called the _exponential_,
with `B` raised to the `A` power. Among other reasons for calling
it the exponential, note that if type `A` has `m` distinct
members, and type `B` has `n` distinct members, then the type
`A → B` has `nᵐ` distinct members. For instance, consider a
type `Bool` with two members and a type `Tri` with three members,
as defined earlier. Then the type `Bool → Tri` has nine (that is,
three squared) members:
λ{true → aa; false → aa} λ{true → aa; false → bb} λ{true → aa; false → cc}
λ{true → bb; false → aa} λ{true → bb; false → bb} λ{true → bb; false → cc}
λ{true → cc; false → aa} λ{true → cc; false → bb} λ{true → cc; false → cc}
For example, the following function enumerates all possible
arguments of the type `Bool → Tri`:
```agda
→-count : (Bool → Tri) → ℕ
→-count f with f true | f false
... | aa | aa = 1
... | aa | bb = 2
... | aa | cc = 3
... | bb | aa = 4
... | bb | bb = 5
... | bb | cc = 6
... | cc | aa = 7
... | cc | bb = 8
... | cc | cc = 9
```
Exponential on types also share a property with exponential on
numbers in that many of the standard identities for numbers carry
over to the types.
Corresponding to the law
(p ^ n) ^ m ≡ p ^ (n * m)
we have the isomorphism
A → (B → C) ≃ (A × B) → C
Both types can be viewed as functions that given evidence that `A` holds
and evidence that `B` holds can return evidence that `C` holds.
This isomorphism sometimes goes by the name *currying*.
```agda
currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
currying =
record
{ to = λ{ f → λ{ ⟨ x , y ⟩ → f x y }}
; from = λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}}
; from∘to = λ{ f → refl }
; to∘from = λ{ g → refl }
}
```
Currying tells us that instead of a function that takes a pair of arguments,
we can have a function that takes the first argument and returns a function that
expects the second argument. Thus, for instance, our way of writing addition
_+_ : ℕ → ℕ → ℕ
is isomorphic to a function that accepts a pair of arguments:
_+′_ : (ℕ × ℕ) → ℕ
Agda is optimised for currying, so `2 + 3` abbreviates `_+_ 2 3`.
In a language optimised for pairing, we would instead take `2 +′ 3` as
an abbreviation for `_+′_ ⟨ 2 , 3 ⟩`.
Corresponding to the law
p ^ (n + m) = (p ^ n) * (p ^ m)
we have the isomorphism:
(A ⊎ B) → C ≃ (A → C) × (B → C)
That is, the assertion that if either `A` holds or `B` holds then `C` holds
is the same as the assertion that if `A` holds then `C` holds and if
`B` holds then `C` holds. The proof of the left inverse requires extensionality:
```agda
→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
→-distrib-⊎ =
record
{ to = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ }
; from = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }
; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } }
; to∘from = λ{ _ → refl }
}
```
Corresponding to the law
(p * n) ^ m = (p ^ m) * (n ^ m)
we have the isomorphism:
A → B × C ≃ (A → B) × (A → C)
That is, the assertion that if `A` holds then `B` holds and `C` holds
is the same as the assertion that if `A` holds then `B` holds and if
`A` holds then `C` holds.
```agda
→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× =
record
{ to = λ{ f → ⟨ proj₁ ∘ f , proj₂ ∘ f ⟩ }
; from = λ{ ⟨ g , h ⟩ → λ x → ⟨ g x , h x ⟩ }
; from∘to = λ{ f → refl }
; to∘from = λ{ ⟨ g , h ⟩ → refl }
}
```
## Distribution
Products distribute over sum, up to isomorphism. The code to validate
this fact is similar in structure to our previous results:
```agda
×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
×-distrib-⊎ =
record
{ to = λ{ ⟨ inj₁ x , z ⟩ → (inj₁ ⟨ x , z ⟩)
; ⟨ inj₂ y , z ⟩ → (inj₂ ⟨ y , z ⟩)
}
; from = λ{ (inj₁ ⟨ x , z ⟩) → ⟨ inj₁ x , z ⟩
; (inj₂ ⟨ y , z ⟩) → ⟨ inj₂ y , z ⟩
}
; from∘to = λ{ ⟨ inj₁ x , z ⟩ → refl
; ⟨ inj₂ y , z ⟩ → refl
}
; to∘from = λ{ (inj₁ ⟨ x , z ⟩) → refl
; (inj₂ ⟨ y , z ⟩) → refl
}
}
```
Sums do not distribute over products up to isomorphism, but it is an embedding:
```agda
⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
⊎-distrib-× =
record
{ to = λ{ (inj₁ ⟨ x , y ⟩) → ⟨ inj₁ x , inj₁ y ⟩
; (inj₂ z) → ⟨ inj₂ z , inj₂ z ⟩
}
; from = λ{ ⟨ inj₁ x , inj₁ y ⟩ → (inj₁ ⟨ x , y ⟩)
; ⟨ inj₁ x , inj₂ z ⟩ → (inj₂ z)
; ⟨ inj₂ z , _ ⟩ → (inj₂ z)
}
; from∘to = λ{ (inj₁ ⟨ x , y ⟩) → refl
; (inj₂ z) → refl
}
}
```
Note that there is a choice in how we write the `from` function.
As given, it takes `⟨ inj₂ z , inj₂ w ⟩` to `inj₂ z`, but it is
easy to write a variant that instead returns `inj₂ w`. We have
an embedding rather than an isomorphism because the
`from` function must discard either `z` or `w` in this case.
In the usual approach to logic, both of the distribution laws
are given as equivalences, where each side implies the other:
A × (B ⊎ C) ⇔ (A × B) ⊎ (A × C)
A ⊎ (B × C) ⇔ (A ⊎ B) × (A ⊎ C)
But when we consider the functions that provide evidence for these
implications, then the first corresponds to an isomorphism while the
second only corresponds to an embedding, revealing a sense in which
one of these laws is "more true" than the other.
#### Exercise `⊎-weak-×` (recommended)
Show that the following property holds:
```agda
postulate
⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
```
This is called a _weak distributive law_. Give the corresponding
distributive law, and explain how it relates to the weak version.
```agda
-- Your code goes here
⊎-weak-×' : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
⊎-weak-×' = λ
{ ⟨ inj₁ a , c ⟩ → inj₁ a
; ⟨ inj₂ b , c ⟩ → inj₂ ⟨ b , c ⟩
}
-- This is similar to ×-distrib-⊎, but it throws away the `C` in inj₁ so it cannot be recovered back from it to form isomorphism
```
#### Exercise `⊎×-implies-×⊎` (practice)
Show that a disjunct of conjuncts implies a conjunct of disjuncts:
```agda
postulate
⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
```
Does the converse hold? If so, prove; if not, give a counterexample.
```agda
-- Your code goes here
⊎×-implies-×⊎' : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
⊎×-implies-×⊎' = λ
{ (inj₁ ⟨ a , b ⟩) → ⟨ inj₁ a , inj₁ b ⟩
; (inj₂ ⟨ c , d ⟩) → ⟨ inj₂ c , inj₂ d ⟩
}
-- ×⊎-implies-⊎× : ∀ {A B C D : Set} → (A ⊎ C) × (B ⊎ D) → (A × B) ⊎ (C × D)
-- ×⊎-implies-⊎× = λ
-- { ⟨ inj₁ a , inj₁ b ⟩ → inj₁ ⟨ a , b ⟩
-- ; ⟨ inj₁ a , inj₂ d ⟩ → {!!} -- cannot construct
-- ; ⟨ inj₂ c , inj₁ b ⟩ → {!!} -- cannot construct
-- ; ⟨ inj₂ c , inj₂ d ⟩ → inj₂ ⟨ c , d ⟩
-- }
```
## Standard library
Definitions similar to those in this chapter can be found in the standard library:
```agda
import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
import Data.Unit using (⊤; tt)
import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
import Data.Empty using (⊥; ⊥-elim)
import Function.Bundles using (_⇔_)
```
The standard library constructs pairs with `_,_` whereas we use `⟨_,_⟩`.
The former makes it convenient to build triples or larger tuples from pairs,
permitting `a , b , c` to stand for `(a , (b , c))`. But it conflicts with
other useful notations, such as `[_,_]` to construct a list of two elements in
Chapter [Lists](/Lists/)
and `Γ , A` to extend environments in
Chapter [DeBruijn](/DeBruijn/).
The standard library `_⇔_` is similar to ours, but the one in the
standard library is less convenient, since it is parameterised with
respect to an arbitrary notion of equivalence.
## Unicode
This chapter uses the following unicode:
× U+00D7 MULTIPLICATION SIGN (\x)
⊎ U+228E MULTISET UNION (\u+)
⊤ U+22A4 DOWN TACK (\top)
⊥ U+22A5 UP TACK (\bot)
η U+03B7 GREEK SMALL LETTER ETA (\eta)
₁ U+2081 SUBSCRIPT ONE (\_1)
₂ U+2082 SUBSCRIPT TWO (\_2)
⇔ U+21D4 LEFT RIGHT DOUBLE ARROW (\<=>)
[^from-wadler-2015]: This paragraph was adopted from "Propositions as Types", Philip Wadler, _Communications of the ACM_, December 2015.