michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
csci8980-f21/versions/20.07/Connectives/index.html

991 lines
152 KiB
HTML
Raw Permalink Blame History

This file contains invisible Unicode characters

This file contains invisible Unicode characters that are indistinguishable to humans but may be processed differently by a computer. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!DOCTYPE html>
<html lang="en"><head>
<meta charset="utf-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>Connectives: Conjunction, disjunction, and implication | Programming Language Foundations in Agda
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
<meta name="generator" content="Jekyll v3.9.0" />
<meta property="og:title" content="Connectives: Conjunction, disjunction, and implication" />
<meta property="og:locale" content="en_US" />
<meta name="description" content="Programming Language Foundations in Agda" />
<meta property="og:description" content="Programming Language Foundations in Agda" />
<link rel="canonical" href="https://plfa.github.io/20.07/Connectives/" />
<meta property="og:url" content="https://plfa.github.io/20.07/Connectives/" />
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
<script type="application/ld+json">
{"url":"https://plfa.github.io/20.07/Connectives/","headline":"Connectives: Conjunction, disjunction, and implication","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
<!-- End Jekyll SEO tag -->
<link rel="stylesheet" href="/20.07/assets/main.css"></head>
<body><header class="site-header" role="banner">
<div class="wrapper">
<a class="site-title" href="/20.07/">Programming Language Foundations in Agda
</a>
<nav class="site-nav">
<span class="menu-icon">
<svg viewBox="0 0 18 15" width="18px" height="15px">
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
</svg>
</span>
<div class="trigger">
<a class="page-link" href="/20.07/">The Book</a>
<a class="page-link" href="/20.07/Announcements/">Announcements</a>
<a class="page-link" href="/20.07/GettingStarted/">Getting Started</a>
<a class="page-link" href="/20.07/Citing/">Citing</a>
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
</div>
</nav>
</div>
</header>
<main class="page-content" aria-label="Content">
<div class="wrapper">
<article class="post">
<header class="post-header">
<h1 class="post-title">Connectives: Conjunction, disjunction, and implication</h1>
</header>
<p style="text-align:center;">
<a alt="Previous chapter" href="/20.07/Isomorphism/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part1/Connectives.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/20.07/Negation/">Next</a>
</p>
<div class="post-content">
<pre class="Agda"><a id="175" class="Keyword">module</a> <a id="182" href="/20.07/Connectives/" class="Module">plfa.part1.Connectives</a> <a id="205" class="Keyword">where</a>
</pre>
<!-- The ⊥ ⊎ A ≅ A exercise requires a (inj₁ ()) pattern,
which the reader will not have seen. Restore this
exercise, and possibly also associativity? Take the
exercises from the final sections on distributivity
and exponentials? -->
<p>This chapter introduces the basic logical connectives, by observing a
correspondence between connectives of logic and data types, a
principle known as <em>Propositions as Types</em>:</p>
<ul>
<li><em>conjunction</em> is <em>product</em>,</li>
<li><em>disjunction</em> is <em>sum</em>,</li>
<li><em>true</em> is <em>unit type</em>,</li>
<li><em>false</em> is <em>empty type</em>,</li>
<li><em>implication</em> is <em>function space</em>.</li>
</ul>
<h2 id="imports">Imports</h2>
<pre class="Agda"><a id="821" class="Keyword">import</a> <a id="828" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="866" class="Symbol">as</a> <a id="869" class="Module">Eq</a>
<a id="872" class="Keyword">open</a> <a id="877" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Eq</a> <a id="880" class="Keyword">using</a> <a id="886" class="Symbol">(</a><a id="887" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="890" class="Symbol">;</a> <a id="892" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="896" class="Symbol">)</a>
<a id="898" class="Keyword">open</a> <a id="903" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2499" class="Module">Eq.≡-Reasoning</a>
<a id="918" class="Keyword">open</a> <a id="923" class="Keyword">import</a> <a id="930" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="939" class="Keyword">using</a> <a id="945" class="Symbol">(</a><a id="946" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="947" class="Symbol">)</a>
<a id="949" class="Keyword">open</a> <a id="954" class="Keyword">import</a> <a id="961" href="https://agda.github.io/agda-stdlib/v1.1/Function.html" class="Module">Function</a> <a id="970" class="Keyword">using</a> <a id="976" class="Symbol">(</a><a id="977" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">_∘_</a><a id="980" class="Symbol">)</a>
<a id="982" class="Keyword">open</a> <a id="987" class="Keyword">import</a> <a id="994" href="/20.07/Isomorphism/" class="Module">plfa.part1.Isomorphism</a> <a id="1017" class="Keyword">using</a> <a id="1023" class="Symbol">(</a><a id="1024" href="/20.07/Isomorphism/#4365" class="Record Operator">_≃_</a><a id="1027" class="Symbol">;</a> <a id="1029" href="/20.07/Isomorphism/#9281" class="Record Operator">_≲_</a><a id="1032" class="Symbol">;</a> <a id="1034" href="/20.07/Isomorphism/#2684" class="Postulate">extensionality</a><a id="1048" class="Symbol">)</a>
<a id="1050" class="Keyword">open</a> <a id="1055" href="/20.07/Isomorphism/#8516" class="Module">plfa.part1.Isomorphism.≃-Reasoning</a>
</pre>
<h2 id="conjunction-is-product">Conjunction is product</h2>
<p>Given two propositions <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>, the conjunction <code class="language-plaintext highlighter-rouge">A × B</code> holds
if both <code class="language-plaintext highlighter-rouge">A</code> holds and <code class="language-plaintext highlighter-rouge">B</code> holds. We formalise this idea by
declaring a suitable record type:</p>
<pre class="Agda"><a id="1287" class="Keyword">data</a> <a id="_×_"></a><a id="1292" href="/20.07/Connectives/#1292" class="Datatype Operator">_×_</a> <a id="1296" class="Symbol">(</a><a id="1297" href="/20.07/Connectives/#1297" class="Bound">A</a> <a id="1299" href="/20.07/Connectives/#1299" class="Bound">B</a> <a id="1301" class="Symbol">:</a> <a id="1303" class="PrimitiveType">Set</a><a id="1306" class="Symbol">)</a> <a id="1308" class="Symbol">:</a> <a id="1310" class="PrimitiveType">Set</a> <a id="1314" class="Keyword">where</a>
<a id="_×_.⟨_,_⟩"></a><a id="1323" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨_,_⟩</a> <a id="1329" class="Symbol">:</a>
<a id="1337" href="/20.07/Connectives/#1297" class="Bound">A</a>
<a id="1343" class="Symbol">→</a> <a id="1345" href="/20.07/Connectives/#1299" class="Bound">B</a>
<a id="1353" class="Comment">-----</a>
<a id="1363" class="Symbol">→</a> <a id="1365" href="/20.07/Connectives/#1297" class="Bound">A</a> <a id="1367" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="1369" href="/20.07/Connectives/#1299" class="Bound">B</a>
</pre>
<p>Evidence that <code class="language-plaintext highlighter-rouge">A × B</code> holds is of the form <code class="language-plaintext highlighter-rouge">⟨ M , N ⟩</code>, where <code class="language-plaintext highlighter-rouge">M</code>
provides evidence that <code class="language-plaintext highlighter-rouge">A</code> holds and <code class="language-plaintext highlighter-rouge">N</code> provides evidence that <code class="language-plaintext highlighter-rouge">B</code>
holds.</p>
<p>Given evidence that <code class="language-plaintext highlighter-rouge">A × B</code> holds, we can conclude that either
<code class="language-plaintext highlighter-rouge">A</code> holds or <code class="language-plaintext highlighter-rouge">B</code> holds:</p>
<pre class="Agda"><a id="proj₁"></a><a id="1608" href="/20.07/Connectives/#1608" class="Function">proj₁</a> <a id="1614" class="Symbol">:</a> <a id="1616" class="Symbol">∀</a> <a id="1618" class="Symbol">{</a><a id="1619" href="/20.07/Connectives/#1619" class="Bound">A</a> <a id="1621" href="/20.07/Connectives/#1621" class="Bound">B</a> <a id="1623" class="Symbol">:</a> <a id="1625" class="PrimitiveType">Set</a><a id="1628" class="Symbol">}</a>
<a id="1632" class="Symbol">→</a> <a id="1634" href="/20.07/Connectives/#1619" class="Bound">A</a> <a id="1636" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="1638" href="/20.07/Connectives/#1621" class="Bound">B</a>
<a id="1644" class="Comment">-----</a>
<a id="1652" class="Symbol">→</a> <a id="1654" href="/20.07/Connectives/#1619" class="Bound">A</a>
<a id="1656" href="/20.07/Connectives/#1608" class="Function">proj₁</a> <a id="1662" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="1664" href="/20.07/Connectives/#1664" class="Bound">x</a> <a id="1666" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="1668" href="/20.07/Connectives/#1668" class="Bound">y</a> <a id="1670" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="1672" class="Symbol">=</a> <a id="1674" href="/20.07/Connectives/#1664" class="Bound">x</a>
<a id="proj₂"></a><a id="1677" href="/20.07/Connectives/#1677" class="Function">proj₂</a> <a id="1683" class="Symbol">:</a> <a id="1685" class="Symbol">∀</a> <a id="1687" class="Symbol">{</a><a id="1688" href="/20.07/Connectives/#1688" class="Bound">A</a> <a id="1690" href="/20.07/Connectives/#1690" class="Bound">B</a> <a id="1692" class="Symbol">:</a> <a id="1694" class="PrimitiveType">Set</a><a id="1697" class="Symbol">}</a>
<a id="1701" class="Symbol">→</a> <a id="1703" href="/20.07/Connectives/#1688" class="Bound">A</a> <a id="1705" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="1707" href="/20.07/Connectives/#1690" class="Bound">B</a>
<a id="1713" class="Comment">-----</a>
<a id="1721" class="Symbol">→</a> <a id="1723" href="/20.07/Connectives/#1690" class="Bound">B</a>
<a id="1725" href="/20.07/Connectives/#1677" class="Function">proj₂</a> <a id="1731" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="1733" href="/20.07/Connectives/#1733" class="Bound">x</a> <a id="1735" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="1737" href="/20.07/Connectives/#1737" class="Bound">y</a> <a id="1739" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="1741" class="Symbol">=</a> <a id="1743" href="/20.07/Connectives/#1737" class="Bound">y</a>
</pre>
<p>If <code class="language-plaintext highlighter-rouge">L</code> provides evidence that <code class="language-plaintext highlighter-rouge">A × B</code> holds, then <code class="language-plaintext highlighter-rouge">proj₁ L</code> provides evidence
that <code class="language-plaintext highlighter-rouge">A</code> holds, and <code class="language-plaintext highlighter-rouge">proj₂ L</code> provides evidence that <code class="language-plaintext highlighter-rouge">B</code> holds.</p>
<p>When <code class="language-plaintext highlighter-rouge">⟨_,_⟩</code> appears in a term on the right-hand side of an equation
we refer to it as a <em>constructor</em>, and when it appears in a pattern on
the left-hand side of an equation we refer to it as a <em>destructor</em>.
We may also refer to <code class="language-plaintext highlighter-rouge">proj₁</code> and <code class="language-plaintext highlighter-rouge">proj₂</code> as destructors, since they
play a similar role.</p>
<p>Other terminology refers to <code class="language-plaintext highlighter-rouge">⟨_,_⟩</code> as <em>introducing</em> a conjunction, and
to <code class="language-plaintext highlighter-rouge">proj₁</code> and <code class="language-plaintext highlighter-rouge">proj₂</code> as <em>eliminating</em> a conjunction; indeed, the
former is sometimes given the name <code class="language-plaintext highlighter-rouge">×-I</code> and the latter two the names
<code class="language-plaintext highlighter-rouge">×-E₁</code> and <code class="language-plaintext highlighter-rouge">×-E₂</code>. As we read the rules from top to bottom,
introduction and elimination do what they say on the tin: the first
<em>introduces</em> a formula for the connective, which appears in the
conclusion but not in the hypotheses; the second <em>eliminates</em> 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 <em>define</em> the connective. An
elimination rule describes what we may conclude when the connective
holds—how to <em>use</em> the connective.<sup id="fnref:from-wadler-2015" role="doc-noteref"><a href="#fn:from-wadler-2015" class="footnote">1</a></sup></p>
<p>In this case, applying each destructor and reassembling the results with the
constructor is the identity over products:</p>
<pre class="Agda"><a id="η-×"></a><a id="3108" href="/20.07/Connectives/#3108" class="Function">η-×</a> <a id="3112" class="Symbol">:</a> <a id="3114" class="Symbol">∀</a> <a id="3116" class="Symbol">{</a><a id="3117" href="/20.07/Connectives/#3117" class="Bound">A</a> <a id="3119" href="/20.07/Connectives/#3119" class="Bound">B</a> <a id="3121" class="Symbol">:</a> <a id="3123" class="PrimitiveType">Set</a><a id="3126" class="Symbol">}</a> <a id="3128" class="Symbol">(</a><a id="3129" href="/20.07/Connectives/#3129" class="Bound">w</a> <a id="3131" class="Symbol">:</a> <a id="3133" href="/20.07/Connectives/#3117" class="Bound">A</a> <a id="3135" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="3137" href="/20.07/Connectives/#3119" class="Bound">B</a><a id="3138" class="Symbol">)</a> <a id="3140" class="Symbol">→</a> <a id="3142" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="3144" href="/20.07/Connectives/#1608" class="Function">proj₁</a> <a id="3150" href="/20.07/Connectives/#3129" class="Bound">w</a> <a id="3152" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="3154" href="/20.07/Connectives/#1677" class="Function">proj₂</a> <a id="3160" href="/20.07/Connectives/#3129" class="Bound">w</a> <a id="3162" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="3164" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="3166" href="/20.07/Connectives/#3129" class="Bound">w</a>
<a id="3168" href="/20.07/Connectives/#3108" class="Function">η-×</a> <a id="3172" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="3174" href="/20.07/Connectives/#3174" class="Bound">x</a> <a id="3176" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="3178" href="/20.07/Connectives/#3178" class="Bound">y</a> <a id="3180" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="3182" class="Symbol">=</a> <a id="3184" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre>
<p>The pattern matching on the left-hand side is essential, since
replacing <code class="language-plaintext highlighter-rouge">w</code> by <code class="language-plaintext highlighter-rouge">⟨ x , y ⟩</code> allows both sides of the
propositional equality to simplify to the same term.</p>
<p>We set the precedence of conjunction so that it binds less
tightly than anything save disjunction:</p>
<pre class="Agda"><a id="3467" class="Keyword">infixr</a> <a id="3474" class="Number">2</a> <a id="3476" href="/20.07/Connectives/#1292" class="Datatype Operator">_×_</a>
</pre>
<p>Thus, <code class="language-plaintext highlighter-rouge">m ≤ n × n ≤ p</code> parses as <code class="language-plaintext highlighter-rouge">(m ≤ n) × (n ≤ p)</code>.</p>
<p>Alternatively, we can declare conjunction as a record type:</p>
<pre class="Agda"><a id="3602" class="Keyword">record</a> <a id="_×′_"></a><a id="3609" href="/20.07/Connectives/#3609" class="Record Operator">_×′_</a> <a id="3614" class="Symbol">(</a><a id="3615" href="/20.07/Connectives/#3615" class="Bound">A</a> <a id="3617" href="/20.07/Connectives/#3617" class="Bound">B</a> <a id="3619" class="Symbol">:</a> <a id="3621" class="PrimitiveType">Set</a><a id="3624" class="Symbol">)</a> <a id="3626" class="Symbol">:</a> <a id="3628" class="PrimitiveType">Set</a> <a id="3632" class="Keyword">where</a>
<a id="3640" class="Keyword">constructor</a> <a id="_×′_.⟨_,_⟩′"></a><a id="3652" href="/20.07/Connectives/#3652" class="InductiveConstructor Operator">⟨_,_⟩′</a>
<a id="3661" class="Keyword">field</a>
<a id="_×′_.proj₁′"></a><a id="3671" href="/20.07/Connectives/#3671" class="Field">proj₁′</a> <a id="3678" class="Symbol">:</a> <a id="3680" href="/20.07/Connectives/#3615" class="Bound">A</a>
<a id="_×′_.proj₂′"></a><a id="3686" href="/20.07/Connectives/#3686" class="Field">proj₂′</a> <a id="3693" class="Symbol">:</a> <a id="3695" href="/20.07/Connectives/#3617" class="Bound">B</a>
<a id="3697" class="Keyword">open</a> <a id="3702" href="/20.07/Connectives/#3609" class="Module Operator">_×′_</a>
</pre>
<p>The record construction <code class="language-plaintext highlighter-rouge">record { proj₁′ = M ; proj₂′ = N }</code> corresponds to the
term <code class="language-plaintext highlighter-rouge">⟨ M , N ⟩</code> where <code class="language-plaintext highlighter-rouge">M</code> is a term of type <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">N</code> is a term of type <code class="language-plaintext highlighter-rouge">B</code>.
The constructor declaration allows us to write <code class="language-plaintext highlighter-rouge">⟨ M , N ⟩′</code> in place of the
record construction.</p>
<p>The data type <code class="language-plaintext highlighter-rouge">_x_</code> and the record type <code class="language-plaintext highlighter-rouge">_×′_</code> behave similarly. One
difference is that for data types we have to prove η-equality, but for record
types, η-equality holds <em>by definition</em>. While proving <code class="language-plaintext highlighter-rouge">η-×′</code>, we do not have to
pattern match on <code class="language-plaintext highlighter-rouge">w</code> to know that η-equality holds:</p>
<pre class="Agda"><a id="η-×′"></a><a id="4253" href="/20.07/Connectives/#4253" class="Function">η-×′</a> <a id="4258" class="Symbol">:</a> <a id="4260" class="Symbol">∀</a> <a id="4262" class="Symbol">{</a><a id="4263" href="/20.07/Connectives/#4263" class="Bound">A</a> <a id="4265" href="/20.07/Connectives/#4265" class="Bound">B</a> <a id="4267" class="Symbol">:</a> <a id="4269" class="PrimitiveType">Set</a><a id="4272" class="Symbol">}</a> <a id="4274" class="Symbol">(</a><a id="4275" href="/20.07/Connectives/#4275" class="Bound">w</a> <a id="4277" class="Symbol">:</a> <a id="4279" href="/20.07/Connectives/#4263" class="Bound">A</a> <a id="4281" href="/20.07/Connectives/#3609" class="Record Operator">×′</a> <a id="4284" href="/20.07/Connectives/#4265" class="Bound">B</a><a id="4285" class="Symbol">)</a> <a id="4287" class="Symbol">→</a> <a id="4289" href="/20.07/Connectives/#3652" class="InductiveConstructor Operator">⟨</a> <a id="4291" href="/20.07/Connectives/#3671" class="Field">proj₁′</a> <a id="4298" href="/20.07/Connectives/#4275" class="Bound">w</a> <a id="4300" href="/20.07/Connectives/#3652" class="InductiveConstructor Operator">,</a> <a id="4302" href="/20.07/Connectives/#3686" class="Field">proj₂′</a> <a id="4309" href="/20.07/Connectives/#4275" class="Bound">w</a> <a id="4311" href="/20.07/Connectives/#3652" class="InductiveConstructor Operator">⟩′</a> <a id="4314" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4316" href="/20.07/Connectives/#4275" class="Bound">w</a>
<a id="4318" href="/20.07/Connectives/#4253" class="Function">η-×′</a> <a id="4323" href="/20.07/Connectives/#4323" class="Bound">w</a> <a id="4325" class="Symbol">=</a> <a id="4327" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre>
<p>It can be very convenient to have η-equality <em>definitionally</em>, and so the
standard library defines <code class="language-plaintext highlighter-rouge">_×_</code> as a record type. We use the definition from the
standard library in later chapters.</p>
<p>Given two types <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>, we refer to <code class="language-plaintext highlighter-rouge">A × B</code> as the
<em>product</em> of <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>. In set theory, it is also sometimes
called the <em>Cartesian product</em>, and in computing it corresponds
to a <em>record</em> type. Among other reasons for
calling it the product, note that if type <code class="language-plaintext highlighter-rouge">A</code> has <code class="language-plaintext highlighter-rouge">m</code>
distinct members, and type <code class="language-plaintext highlighter-rouge">B</code> has <code class="language-plaintext highlighter-rouge">n</code> distinct members,
then the type <code class="language-plaintext highlighter-rouge">A × B</code> has <code class="language-plaintext highlighter-rouge">m * n</code> distinct members.
For instance, consider a type <code class="language-plaintext highlighter-rouge">Bool</code> with two members, and
a type <code class="language-plaintext highlighter-rouge">Tri</code> with three members:</p>
<pre class="Agda"><a id="5014" class="Keyword">data</a> <a id="Bool"></a><a id="5019" href="/20.07/Connectives/#5019" class="Datatype">Bool</a> <a id="5024" class="Symbol">:</a> <a id="5026" class="PrimitiveType">Set</a> <a id="5030" class="Keyword">where</a>
<a id="Bool.true"></a><a id="5038" href="/20.07/Connectives/#5038" class="InductiveConstructor">true</a> <a id="5044" class="Symbol">:</a> <a id="5046" href="/20.07/Connectives/#5019" class="Datatype">Bool</a>
<a id="Bool.false"></a><a id="5053" href="/20.07/Connectives/#5053" class="InductiveConstructor">false</a> <a id="5059" class="Symbol">:</a> <a id="5061" href="/20.07/Connectives/#5019" class="Datatype">Bool</a>
<a id="5067" class="Keyword">data</a> <a id="Tri"></a><a id="5072" href="/20.07/Connectives/#5072" class="Datatype">Tri</a> <a id="5076" class="Symbol">:</a> <a id="5078" class="PrimitiveType">Set</a> <a id="5082" class="Keyword">where</a>
<a id="Tri.aa"></a><a id="5090" href="/20.07/Connectives/#5090" class="InductiveConstructor">aa</a> <a id="5093" class="Symbol">:</a> <a id="5095" href="/20.07/Connectives/#5072" class="Datatype">Tri</a>
<a id="Tri.bb"></a><a id="5101" href="/20.07/Connectives/#5101" class="InductiveConstructor">bb</a> <a id="5104" class="Symbol">:</a> <a id="5106" href="/20.07/Connectives/#5072" class="Datatype">Tri</a>
<a id="Tri.cc"></a><a id="5112" href="/20.07/Connectives/#5112" class="InductiveConstructor">cc</a> <a id="5115" class="Symbol">:</a> <a id="5117" href="/20.07/Connectives/#5072" class="Datatype">Tri</a>
</pre>
<p>Then the type <code class="language-plaintext highlighter-rouge">Bool × Tri</code> has six members:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>⟨ true , aa ⟩ ⟨ true , bb ⟩ ⟨ true , cc ⟩
⟨ false , aa ⟩ ⟨ false , bb ⟩ ⟨ false , cc ⟩
</code></pre></div></div>
<p>For example, the following function enumerates all
possible arguments of type <code class="language-plaintext highlighter-rouge">Bool × Tri</code>:</p>
<pre class="Agda"><a id="×-count"></a><a id="5377" href="/20.07/Connectives/#5377" class="Function">×-count</a> <a id="5385" class="Symbol">:</a> <a id="5387" href="/20.07/Connectives/#5019" class="Datatype">Bool</a> <a id="5392" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="5394" href="/20.07/Connectives/#5072" class="Datatype">Tri</a> <a id="5398" class="Symbol">→</a> <a id="5400" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="5402" href="/20.07/Connectives/#5377" class="Function">×-count</a> <a id="5410" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="5412" href="/20.07/Connectives/#5038" class="InductiveConstructor">true</a> <a id="5418" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="5420" href="/20.07/Connectives/#5090" class="InductiveConstructor">aa</a> <a id="5423" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="5426" class="Symbol">=</a> <a id="5429" class="Number">1</a>
<a id="5431" href="/20.07/Connectives/#5377" class="Function">×-count</a> <a id="5439" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="5441" href="/20.07/Connectives/#5038" class="InductiveConstructor">true</a> <a id="5447" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="5449" href="/20.07/Connectives/#5101" class="InductiveConstructor">bb</a> <a id="5452" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="5455" class="Symbol">=</a> <a id="5458" class="Number">2</a>
<a id="5460" href="/20.07/Connectives/#5377" class="Function">×-count</a> <a id="5468" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="5470" href="/20.07/Connectives/#5038" class="InductiveConstructor">true</a> <a id="5476" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="5478" href="/20.07/Connectives/#5112" class="InductiveConstructor">cc</a> <a id="5481" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="5484" class="Symbol">=</a> <a id="5487" class="Number">3</a>
<a id="5489" href="/20.07/Connectives/#5377" class="Function">×-count</a> <a id="5497" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="5499" href="/20.07/Connectives/#5053" class="InductiveConstructor">false</a> <a id="5505" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="5507" href="/20.07/Connectives/#5090" class="InductiveConstructor">aa</a> <a id="5510" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="5513" class="Symbol">=</a> <a id="5516" class="Number">4</a>
<a id="5518" href="/20.07/Connectives/#5377" class="Function">×-count</a> <a id="5526" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="5528" href="/20.07/Connectives/#5053" class="InductiveConstructor">false</a> <a id="5534" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="5536" href="/20.07/Connectives/#5101" class="InductiveConstructor">bb</a> <a id="5539" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="5542" class="Symbol">=</a> <a id="5545" class="Number">5</a>
<a id="5547" href="/20.07/Connectives/#5377" class="Function">×-count</a> <a id="5555" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="5557" href="/20.07/Connectives/#5053" class="InductiveConstructor">false</a> <a id="5563" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="5565" href="/20.07/Connectives/#5112" class="InductiveConstructor">cc</a> <a id="5568" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="5571" class="Symbol">=</a> <a id="5574" class="Number">6</a>
</pre>
<p>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 <em>up to
isomorphism</em>.</p>
<p>For commutativity, the <code class="language-plaintext highlighter-rouge">to</code> function swaps a pair, taking <code class="language-plaintext highlighter-rouge">⟨ x , y ⟩</code> to
<code class="language-plaintext highlighter-rouge">⟨ y , x ⟩</code>, and the <code class="language-plaintext highlighter-rouge">from</code> function does the same (up to renaming).
Instantiating the patterns correctly in <code class="language-plaintext highlighter-rouge">from∘to</code> and <code class="language-plaintext highlighter-rouge">to∘from</code> is essential.
Replacing the definition of <code class="language-plaintext highlighter-rouge">from∘to</code> by <code class="language-plaintext highlighter-rouge">λ w → refl</code> will not work;
and similarly for <code class="language-plaintext highlighter-rouge">to∘from</code>:</p>
<pre class="Agda"><a id="×-comm"></a><a id="6113" href="/20.07/Connectives/#6113" class="Function">×-comm</a> <a id="6120" class="Symbol">:</a> <a id="6122" class="Symbol">∀</a> <a id="6124" class="Symbol">{</a><a id="6125" href="/20.07/Connectives/#6125" class="Bound">A</a> <a id="6127" href="/20.07/Connectives/#6127" class="Bound">B</a> <a id="6129" class="Symbol">:</a> <a id="6131" class="PrimitiveType">Set</a><a id="6134" class="Symbol">}</a> <a id="6136" class="Symbol">→</a> <a id="6138" href="/20.07/Connectives/#6125" class="Bound">A</a> <a id="6140" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="6142" href="/20.07/Connectives/#6127" class="Bound">B</a> <a id="6144" href="/20.07/Isomorphism/#4365" class="Record Operator">≃</a> <a id="6146" href="/20.07/Connectives/#6127" class="Bound">B</a> <a id="6148" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="6150" href="/20.07/Connectives/#6125" class="Bound">A</a>
<a id="6152" href="/20.07/Connectives/#6113" class="Function">×-comm</a> <a id="6159" class="Symbol">=</a>
<a id="6163" class="Keyword">record</a>
<a id="6174" class="Symbol">{</a> <a id="6176" href="/20.07/Isomorphism/#4405" class="Field">to</a> <a id="6185" class="Symbol">=</a> <a id="6188" class="Symbol">λ{</a> <a id="6191" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="6193" href="/20.07/Connectives/#6193" class="Bound">x</a> <a id="6195" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="6197" href="/20.07/Connectives/#6197" class="Bound">y</a> <a id="6199" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="6201" class="Symbol">→</a> <a id="6203" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="6205" href="/20.07/Connectives/#6197" class="Bound">y</a> <a id="6207" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="6209" href="/20.07/Connectives/#6193" class="Bound">x</a> <a id="6211" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="6213" class="Symbol">}</a>
<a id="6219" class="Symbol">;</a> <a id="6221" href="/20.07/Isomorphism/#4422" class="Field">from</a> <a id="6230" class="Symbol">=</a> <a id="6233" class="Symbol">λ{</a> <a id="6236" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="6238" href="/20.07/Connectives/#6238" class="Bound">y</a> <a id="6240" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="6242" href="/20.07/Connectives/#6242" class="Bound">x</a> <a id="6244" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="6246" class="Symbol">→</a> <a id="6248" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="6250" href="/20.07/Connectives/#6242" class="Bound">x</a> <a id="6252" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="6254" href="/20.07/Connectives/#6238" class="Bound">y</a> <a id="6256" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="6258" class="Symbol">}</a>
<a id="6264" class="Symbol">;</a> <a id="6266" href="/20.07/Isomorphism/#4439" class="Field">from∘to</a> <a id="6275" class="Symbol">=</a> <a id="6278" class="Symbol">λ{</a> <a id="6281" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="6283" href="/20.07/Connectives/#6283" class="Bound">x</a> <a id="6285" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="6287" href="/20.07/Connectives/#6287" class="Bound">y</a> <a id="6289" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="6291" class="Symbol">→</a> <a id="6293" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="6298" class="Symbol">}</a>
<a id="6304" class="Symbol">;</a> <a id="6306" href="/20.07/Isomorphism/#4481" class="Field">to∘from</a> <a id="6315" class="Symbol">=</a> <a id="6318" class="Symbol">λ{</a> <a id="6321" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="6323" href="/20.07/Connectives/#6323" class="Bound">y</a> <a id="6325" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="6327" href="/20.07/Connectives/#6327" class="Bound">x</a> <a id="6329" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="6331" class="Symbol">→</a> <a id="6333" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="6338" class="Symbol">}</a>
<a id="6344" class="Symbol">}</a>
</pre>
<p>Being <em>commutative</em> is different from being <em>commutative up to
isomorphism</em>. Compare the two statements:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m * n ≡ n * m
A × B ≃ B × A
</code></pre></div></div>
<p>In the first case, we might have that <code class="language-plaintext highlighter-rouge">m</code> is <code class="language-plaintext highlighter-rouge">2</code> and <code class="language-plaintext highlighter-rouge">n</code> is <code class="language-plaintext highlighter-rouge">3</code>, and
both <code class="language-plaintext highlighter-rouge">m * n</code> and <code class="language-plaintext highlighter-rouge">n * m</code> are equal to <code class="language-plaintext highlighter-rouge">6</code>. In the second case, we
might have that <code class="language-plaintext highlighter-rouge">A</code> is <code class="language-plaintext highlighter-rouge">Bool</code> and <code class="language-plaintext highlighter-rouge">B</code> is <code class="language-plaintext highlighter-rouge">Tri</code>, and <code class="language-plaintext highlighter-rouge">Bool × Tri</code> is
<em>not</em> the same as <code class="language-plaintext highlighter-rouge">Tri × Bool</code>. But there is an isomorphism between
the two types. For instance, <code class="language-plaintext highlighter-rouge">⟨ true , aa ⟩</code>, which is a member of the
former, corresponds to <code class="language-plaintext highlighter-rouge">⟨ aa , true ⟩</code>, which is a member of the latter.</p>
<p>For associativity, the <code class="language-plaintext highlighter-rouge">to</code> function reassociates two uses of pairing,
taking <code class="language-plaintext highlighter-rouge">⟨ ⟨ x , y ⟩ , z ⟩</code> to <code class="language-plaintext highlighter-rouge">⟨ x , ⟨ y , z ⟩ ⟩</code>, and the <code class="language-plaintext highlighter-rouge">from</code> function does
the inverse. Again, the evidence of left and right inverse requires
matching against a suitable pattern to enable simplification:</p>
<pre class="Agda"><a id="×-assoc"></a><a id="7200" href="/20.07/Connectives/#7200" class="Function">×-assoc</a> <a id="7208" class="Symbol">:</a> <a id="7210" class="Symbol">∀</a> <a id="7212" class="Symbol">{</a><a id="7213" href="/20.07/Connectives/#7213" class="Bound">A</a> <a id="7215" href="/20.07/Connectives/#7215" class="Bound">B</a> <a id="7217" href="/20.07/Connectives/#7217" class="Bound">C</a> <a id="7219" class="Symbol">:</a> <a id="7221" class="PrimitiveType">Set</a><a id="7224" class="Symbol">}</a> <a id="7226" class="Symbol">→</a> <a id="7228" class="Symbol">(</a><a id="7229" href="/20.07/Connectives/#7213" class="Bound">A</a> <a id="7231" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="7233" href="/20.07/Connectives/#7215" class="Bound">B</a><a id="7234" class="Symbol">)</a> <a id="7236" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="7238" href="/20.07/Connectives/#7217" class="Bound">C</a> <a id="7240" href="/20.07/Isomorphism/#4365" class="Record Operator">≃</a> <a id="7242" href="/20.07/Connectives/#7213" class="Bound">A</a> <a id="7244" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="7246" class="Symbol">(</a><a id="7247" href="/20.07/Connectives/#7215" class="Bound">B</a> <a id="7249" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="7251" href="/20.07/Connectives/#7217" class="Bound">C</a><a id="7252" class="Symbol">)</a>
<a id="7254" href="/20.07/Connectives/#7200" class="Function">×-assoc</a> <a id="7262" class="Symbol">=</a>
<a id="7266" class="Keyword">record</a>
<a id="7277" class="Symbol">{</a> <a id="7279" href="/20.07/Isomorphism/#4405" class="Field">to</a> <a id="7287" class="Symbol">=</a> <a id="7289" class="Symbol">λ{</a> <a id="7292" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7294" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7296" href="/20.07/Connectives/#7296" class="Bound">x</a> <a id="7298" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7300" href="/20.07/Connectives/#7300" class="Bound">y</a> <a id="7302" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7304" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7306" href="/20.07/Connectives/#7306" class="Bound">z</a> <a id="7308" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7310" class="Symbol">→</a> <a id="7312" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7314" href="/20.07/Connectives/#7296" class="Bound">x</a> <a id="7316" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7318" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7320" href="/20.07/Connectives/#7300" class="Bound">y</a> <a id="7322" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7324" href="/20.07/Connectives/#7306" class="Bound">z</a> <a id="7326" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7328" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7330" class="Symbol">}</a>
<a id="7336" class="Symbol">;</a> <a id="7338" href="/20.07/Isomorphism/#4422" class="Field">from</a> <a id="7346" class="Symbol">=</a> <a id="7348" class="Symbol">λ{</a> <a id="7351" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7353" href="/20.07/Connectives/#7353" class="Bound">x</a> <a id="7355" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7357" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7359" href="/20.07/Connectives/#7359" class="Bound">y</a> <a id="7361" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7363" href="/20.07/Connectives/#7363" class="Bound">z</a> <a id="7365" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7367" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7369" class="Symbol">→</a> <a id="7371" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7373" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7375" href="/20.07/Connectives/#7353" class="Bound">x</a> <a id="7377" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7379" href="/20.07/Connectives/#7359" class="Bound">y</a> <a id="7381" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7383" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7385" href="/20.07/Connectives/#7363" class="Bound">z</a> <a id="7387" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7389" class="Symbol">}</a>
<a id="7395" class="Symbol">;</a> <a id="7397" href="/20.07/Isomorphism/#4439" class="Field">from∘to</a> <a id="7405" class="Symbol">=</a> <a id="7407" class="Symbol">λ{</a> <a id="7410" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7412" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7414" href="/20.07/Connectives/#7414" class="Bound">x</a> <a id="7416" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7418" href="/20.07/Connectives/#7418" class="Bound">y</a> <a id="7420" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7422" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7424" href="/20.07/Connectives/#7424" class="Bound">z</a> <a id="7426" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7428" class="Symbol">→</a> <a id="7430" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="7435" class="Symbol">}</a>
<a id="7441" class="Symbol">;</a> <a id="7443" href="/20.07/Isomorphism/#4481" class="Field">to∘from</a> <a id="7451" class="Symbol">=</a> <a id="7453" class="Symbol">λ{</a> <a id="7456" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7458" href="/20.07/Connectives/#7458" class="Bound">x</a> <a id="7460" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7462" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="7464" href="/20.07/Connectives/#7464" class="Bound">y</a> <a id="7466" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="7468" href="/20.07/Connectives/#7468" class="Bound">z</a> <a id="7470" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7472" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="7474" class="Symbol">→</a> <a id="7476" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="7481" class="Symbol">}</a>
<a id="7487" class="Symbol">}</a>
</pre>
<p>Being <em>associative</em> is not the same as being <em>associative
up to isomorphism</em>. Compare the two statements:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(m * n) * p ≡ m * (n * p)
(A × B) × C ≃ A × (B × C)
</code></pre></div></div>
<p>For example, the type <code class="language-plaintext highlighter-rouge">(ℕ × Bool) × Tri</code> is <em>not</em> the same as <code class="language-plaintext highlighter-rouge">ℕ ×
(Bool × Tri)</code>. But there is an isomorphism between the two types. For
instance <code class="language-plaintext highlighter-rouge">⟨ ⟨ 1 , true ⟩ , aa ⟩</code>, which is a member of the former,
corresponds to <code class="language-plaintext highlighter-rouge">⟨ 1 , ⟨ true , aa ⟩ ⟩</code>, which is a member of the latter.</p>
<h4 id="exercise--recommended">Exercise <code class="language-plaintext highlighter-rouge">⇔≃×</code> (recommended)</h4>
<p>Show that <code class="language-plaintext highlighter-rouge">A ⇔ B</code> as defined <a href="/20.07/Isomorphism/#iff">earlier</a>
is isomorphic to <code class="language-plaintext highlighter-rouge">(A → B) × (B → A)</code>.</p>
<pre class="Agda"><a id="8095" class="Comment">-- Your code goes here</a>
</pre>
<h2 id="truth-is-unit">Truth is unit</h2>
<p>Truth <code class="language-plaintext highlighter-rouge">⊤</code> always holds. We formalise this idea by
declaring a suitable record type:</p>
<pre class="Agda"><a id="8230" class="Keyword">data</a> <a id="⊤"></a><a id="8235" href="/20.07/Connectives/#8235" class="Datatype">⊤</a> <a id="8237" class="Symbol">:</a> <a id="8239" class="PrimitiveType">Set</a> <a id="8243" class="Keyword">where</a>
<a id="⊤.tt"></a><a id="8252" href="/20.07/Connectives/#8252" class="InductiveConstructor">tt</a> <a id="8255" class="Symbol">:</a>
<a id="8261" class="Comment">--</a>
<a id="8268" href="/20.07/Connectives/#8235" class="Datatype">⊤</a>
</pre>
<p>Evidence that <code class="language-plaintext highlighter-rouge">⊤</code> holds is of the form <code class="language-plaintext highlighter-rouge">tt</code>.</p>
<p>There is an introduction rule, but no elimination rule.
Given evidence that <code class="language-plaintext highlighter-rouge">⊤</code> holds, there is nothing more of interest we
can conclude. Since truth always holds, knowing that it holds tells
us nothing new.</p>
<p>The nullary case of <code class="language-plaintext highlighter-rouge">η-×</code> is <code class="language-plaintext highlighter-rouge">η-⊤</code>, which asserts that any
value of type <code class="language-plaintext highlighter-rouge">⊤</code> must be equal to <code class="language-plaintext highlighter-rouge">tt</code>:</p>
<pre class="Agda"><a id="η-⊤"></a><a id="8634" href="/20.07/Connectives/#8634" class="Function">η-⊤</a> <a id="8638" class="Symbol">:</a> <a id="8640" class="Symbol">∀</a> <a id="8642" class="Symbol">(</a><a id="8643" href="/20.07/Connectives/#8643" class="Bound">w</a> <a id="8645" class="Symbol">:</a> <a id="8647" href="/20.07/Connectives/#8235" class="Datatype">⊤</a><a id="8648" class="Symbol">)</a> <a id="8650" class="Symbol">→</a> <a id="8652" href="/20.07/Connectives/#8252" class="InductiveConstructor">tt</a> <a id="8655" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="8657" href="/20.07/Connectives/#8643" class="Bound">w</a>
<a id="8659" href="/20.07/Connectives/#8634" class="Function">η-⊤</a> <a id="8663" href="/20.07/Connectives/#8252" class="InductiveConstructor">tt</a> <a id="8666" class="Symbol">=</a> <a id="8668" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre>
<p>The pattern matching on the left-hand side is essential. Replacing
<code class="language-plaintext highlighter-rouge">w</code> by <code class="language-plaintext highlighter-rouge">tt</code> allows both sides of the propositional equality to
simplify to the same term.</p>
<p>Alternatively, we can declare truth as an empty record:</p>
<pre class="Agda"><a id="8895" class="Keyword">record</a> <a id="⊤′"></a><a id="8902" href="/20.07/Connectives/#8902" class="Record">⊤′</a> <a id="8905" class="Symbol">:</a> <a id="8907" class="PrimitiveType">Set</a> <a id="8911" class="Keyword">where</a>
<a id="8919" class="Keyword">constructor</a> <a id="⊤′.tt′"></a><a id="8931" href="/20.07/Connectives/#8931" class="InductiveConstructor">tt′</a>
</pre>
<p>The record construction <code class="language-plaintext highlighter-rouge">record {}</code> corresponds to the term <code class="language-plaintext highlighter-rouge">tt</code>. The
constructor declaration allows us to write <code class="language-plaintext highlighter-rouge">tt′</code>.</p>
<p>As with the product, the data type <code class="language-plaintext highlighter-rouge">⊤</code> and the record type <code class="language-plaintext highlighter-rouge">⊤′</code> behave
similarly, but η-equality holds <em>by definition</em> for the record type. While
proving <code class="language-plaintext highlighter-rouge">η-⊤′</code>, we do not have to pattern match on <code class="language-plaintext highlighter-rouge">w</code>—Agda <em>knows</em> it is
equal to <code class="language-plaintext highlighter-rouge">tt′</code>:</p>
<pre class="Agda"><a id="η-⊤′"></a><a id="9302" href="/20.07/Connectives/#9302" class="Function">η-⊤′</a> <a id="9307" class="Symbol">:</a> <a id="9309" class="Symbol">∀</a> <a id="9311" class="Symbol">(</a><a id="9312" href="/20.07/Connectives/#9312" class="Bound">w</a> <a id="9314" class="Symbol">:</a> <a id="9316" href="/20.07/Connectives/#8902" class="Record">⊤′</a><a id="9318" class="Symbol">)</a> <a id="9320" class="Symbol">→</a> <a id="9322" href="/20.07/Connectives/#8931" class="InductiveConstructor">tt′</a> <a id="9326" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="9328" href="/20.07/Connectives/#9312" class="Bound">w</a>
<a id="9330" href="/20.07/Connectives/#9302" class="Function">η-⊤′</a> <a id="9335" href="/20.07/Connectives/#9335" class="Bound">w</a> <a id="9337" class="Symbol">=</a> <a id="9339" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre>
<p>Agda knows that <em>any</em> value of type <code class="language-plaintext highlighter-rouge">⊤′</code> must be <code class="language-plaintext highlighter-rouge">tt′</code>, so any time we need a
value of type <code class="language-plaintext highlighter-rouge">⊤′</code>, we can tell Agda to figure it out:</p>
<pre class="Agda"><a id="truth′"></a><a id="9485" href="/20.07/Connectives/#9485" class="Function">truth′</a> <a id="9492" class="Symbol">:</a> <a id="9494" href="/20.07/Connectives/#8902" class="Record">⊤′</a>
<a id="9497" href="/20.07/Connectives/#9485" class="Function">truth′</a> <a id="9504" class="Symbol">=</a> <a id="9506" class="Symbol">_</a>
</pre>
<p>We refer to <code class="language-plaintext highlighter-rouge">⊤</code> as the <em>unit</em> type. And, indeed,
type <code class="language-plaintext highlighter-rouge">⊤</code> has exactly one member, <code class="language-plaintext highlighter-rouge">tt</code>. For example, the following
function enumerates all possible arguments of type <code class="language-plaintext highlighter-rouge">⊤</code>:</p>
<pre class="Agda"><a id="⊤-count"></a><a id="9689" href="/20.07/Connectives/#9689" class="Function">⊤-count</a> <a id="9697" class="Symbol">:</a> <a id="9699" href="/20.07/Connectives/#8235" class="Datatype">⊤</a> <a id="9701" class="Symbol">→</a> <a id="9703" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="9705" href="/20.07/Connectives/#9689" class="Function">⊤-count</a> <a id="9713" href="/20.07/Connectives/#8252" class="InductiveConstructor">tt</a> <a id="9716" class="Symbol">=</a> <a id="9718" class="Number">1</a>
</pre>
<p>For numbers, one is the identity of multiplication. Correspondingly,
unit is the identity of product <em>up to isomorphism</em>. For left
identity, the <code class="language-plaintext highlighter-rouge">to</code> function takes <code class="language-plaintext highlighter-rouge">⟨ tt , x ⟩</code> to <code class="language-plaintext highlighter-rouge">x</code>, and the <code class="language-plaintext highlighter-rouge">from</code>
function does the inverse. The evidence of left inverse requires
matching against a suitable pattern to enable simplification:</p>
<pre class="Agda"><a id="⊤-identityˡ"></a><a id="10059" href="/20.07/Connectives/#10059" class="Function">⊤-identityˡ</a> <a id="10071" class="Symbol">:</a> <a id="10073" class="Symbol">∀</a> <a id="10075" class="Symbol">{</a><a id="10076" href="/20.07/Connectives/#10076" class="Bound">A</a> <a id="10078" class="Symbol">:</a> <a id="10080" class="PrimitiveType">Set</a><a id="10083" class="Symbol">}</a> <a id="10085" class="Symbol">→</a> <a id="10087" href="/20.07/Connectives/#8235" class="Datatype">⊤</a> <a id="10089" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="10091" href="/20.07/Connectives/#10076" class="Bound">A</a> <a id="10093" href="/20.07/Isomorphism/#4365" class="Record Operator">≃</a> <a id="10095" href="/20.07/Connectives/#10076" class="Bound">A</a>
<a id="10097" href="/20.07/Connectives/#10059" class="Function">⊤-identityˡ</a> <a id="10109" class="Symbol">=</a>
<a id="10113" class="Keyword">record</a>
<a id="10124" class="Symbol">{</a> <a id="10126" href="/20.07/Isomorphism/#4405" class="Field">to</a> <a id="10134" class="Symbol">=</a> <a id="10136" class="Symbol">λ{</a> <a id="10139" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="10141" href="/20.07/Connectives/#8252" class="InductiveConstructor">tt</a> <a id="10144" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="10146" href="/20.07/Connectives/#10146" class="Bound">x</a> <a id="10148" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="10150" class="Symbol">→</a> <a id="10152" href="/20.07/Connectives/#10146" class="Bound">x</a> <a id="10154" class="Symbol">}</a>
<a id="10160" class="Symbol">;</a> <a id="10162" href="/20.07/Isomorphism/#4422" class="Field">from</a> <a id="10170" class="Symbol">=</a> <a id="10172" class="Symbol">λ{</a> <a id="10175" href="/20.07/Connectives/#10175" class="Bound">x</a> <a id="10177" class="Symbol">→</a> <a id="10179" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="10181" href="/20.07/Connectives/#8252" class="InductiveConstructor">tt</a> <a id="10184" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="10186" href="/20.07/Connectives/#10175" class="Bound">x</a> <a id="10188" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="10190" class="Symbol">}</a>
<a id="10196" class="Symbol">;</a> <a id="10198" href="/20.07/Isomorphism/#4439" class="Field">from∘to</a> <a id="10206" class="Symbol">=</a> <a id="10208" class="Symbol">λ{</a> <a id="10211" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="10213" href="/20.07/Connectives/#8252" class="InductiveConstructor">tt</a> <a id="10216" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="10218" href="/20.07/Connectives/#10218" class="Bound">x</a> <a id="10220" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="10222" class="Symbol">→</a> <a id="10224" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="10229" class="Symbol">}</a>
<a id="10235" class="Symbol">;</a> <a id="10237" href="/20.07/Isomorphism/#4481" class="Field">to∘from</a> <a id="10245" class="Symbol">=</a> <a id="10247" class="Symbol">λ{</a> <a id="10250" href="/20.07/Connectives/#10250" class="Bound">x</a> <a id="10252" class="Symbol">→</a> <a id="10254" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="10259" class="Symbol">}</a>
<a id="10265" class="Symbol">}</a>
</pre>
<p>Having an <em>identity</em> is different from having an identity
<em>up to isomorphism</em>. Compare the two statements:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>1 * m ≡ m
⊤ × A ≃ A
</code></pre></div></div>
<p>In the first case, we might have that <code class="language-plaintext highlighter-rouge">m</code> is <code class="language-plaintext highlighter-rouge">2</code>, and both
<code class="language-plaintext highlighter-rouge">1 * m</code> and <code class="language-plaintext highlighter-rouge">m</code> are equal to <code class="language-plaintext highlighter-rouge">2</code>. In the second
case, we might have that <code class="language-plaintext highlighter-rouge">A</code> is <code class="language-plaintext highlighter-rouge">Bool</code>, and <code class="language-plaintext highlighter-rouge">⊤ × Bool</code> is <em>not</em> the
same as <code class="language-plaintext highlighter-rouge">Bool</code>. But there is an isomorphism between the two types.
For instance, <code class="language-plaintext highlighter-rouge">⟨ tt , true ⟩</code>, which is a member of the former,
corresponds to <code class="language-plaintext highlighter-rouge">true</code>, which is a member of the latter.</p>
<p>Right identity follows from commutativity of product and left identity:</p>
<pre class="Agda"><a id="⊤-identityʳ"></a><a id="10851" href="/20.07/Connectives/#10851" class="Function">⊤-identityʳ</a> <a id="10863" class="Symbol">:</a> <a id="10865" class="Symbol">∀</a> <a id="10867" class="Symbol">{</a><a id="10868" href="/20.07/Connectives/#10868" class="Bound">A</a> <a id="10870" class="Symbol">:</a> <a id="10872" class="PrimitiveType">Set</a><a id="10875" class="Symbol">}</a> <a id="10877" class="Symbol">→</a> <a id="10879" class="Symbol">(</a><a id="10880" href="/20.07/Connectives/#10868" class="Bound">A</a> <a id="10882" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="10884" href="/20.07/Connectives/#8235" class="Datatype">⊤</a><a id="10885" class="Symbol">)</a> <a id="10887" href="/20.07/Isomorphism/#4365" class="Record Operator">≃</a> <a id="10889" href="/20.07/Connectives/#10868" class="Bound">A</a>
<a id="10891" href="/20.07/Connectives/#10851" class="Function">⊤-identityʳ</a> <a id="10903" class="Symbol">{</a><a id="10904" href="/20.07/Connectives/#10904" class="Bound">A</a><a id="10905" class="Symbol">}</a> <a id="10907" class="Symbol">=</a>
<a id="10911" href="/20.07/Isomorphism/#8592" class="Function Operator">≃-begin</a>
<a id="10923" class="Symbol">(</a><a id="10924" href="/20.07/Connectives/#10904" class="Bound">A</a> <a id="10926" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="10928" href="/20.07/Connectives/#8235" class="Datatype">⊤</a><a id="10929" class="Symbol">)</a>
<a id="10933" href="/20.07/Isomorphism/#8676" class="Function Operator">≃⟨</a> <a id="10936" href="/20.07/Connectives/#6113" class="Function">×-comm</a> <a id="10943" href="/20.07/Isomorphism/#8676" class="Function Operator">⟩</a>
<a id="10949" class="Symbol">(</a><a id="10950" href="/20.07/Connectives/#8235" class="Datatype">⊤</a> <a id="10952" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="10954" href="/20.07/Connectives/#10904" class="Bound">A</a><a id="10955" class="Symbol">)</a>
<a id="10959" href="/20.07/Isomorphism/#8676" class="Function Operator">≃⟨</a> <a id="10962" href="/20.07/Connectives/#10059" class="Function">⊤-identityˡ</a> <a id="10974" href="/20.07/Isomorphism/#8676" class="Function Operator">⟩</a>
<a id="10980" href="/20.07/Connectives/#10904" class="Bound">A</a>
<a id="10984" href="/20.07/Isomorphism/#8795" class="Function Operator">≃-∎</a>
</pre>
<p>Here we have used a chain of isomorphisms, analogous to that used for
equality.</p>
<h2 id="disjunction-is-sum">Disjunction is sum</h2>
<p>Given two propositions <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>, the disjunction <code class="language-plaintext highlighter-rouge">A ⊎ B</code> holds
if either <code class="language-plaintext highlighter-rouge">A</code> holds or <code class="language-plaintext highlighter-rouge">B</code> holds. We formalise this idea by
declaring a suitable inductive type:</p>
<pre class="Agda"><a id="11265" class="Keyword">data</a> <a id="_⊎_"></a><a id="11270" href="/20.07/Connectives/#11270" class="Datatype Operator">_⊎_</a> <a id="11274" class="Symbol">(</a><a id="11275" href="/20.07/Connectives/#11275" class="Bound">A</a> <a id="11277" href="/20.07/Connectives/#11277" class="Bound">B</a> <a id="11279" class="Symbol">:</a> <a id="11281" class="PrimitiveType">Set</a><a id="11284" class="Symbol">)</a> <a id="11286" class="Symbol">:</a> <a id="11288" class="PrimitiveType">Set</a> <a id="11292" class="Keyword">where</a>
<a id="_⊎_.inj₁"></a><a id="11301" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="11306" class="Symbol">:</a>
<a id="11314" href="/20.07/Connectives/#11275" class="Bound">A</a>
<a id="11322" class="Comment">-----</a>
<a id="11332" class="Symbol">→</a> <a id="11334" href="/20.07/Connectives/#11275" class="Bound">A</a> <a id="11336" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="11338" href="/20.07/Connectives/#11277" class="Bound">B</a>
<a id="_⊎_.inj₂"></a><a id="11343" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="11348" class="Symbol">:</a>
<a id="11356" href="/20.07/Connectives/#11277" class="Bound">B</a>
<a id="11364" class="Comment">-----</a>
<a id="11374" class="Symbol">→</a> <a id="11376" href="/20.07/Connectives/#11275" class="Bound">A</a> <a id="11378" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="11380" href="/20.07/Connectives/#11277" class="Bound">B</a>
</pre>
<p>Evidence that <code class="language-plaintext highlighter-rouge">A ⊎ B</code> holds is either of the form <code class="language-plaintext highlighter-rouge">inj₁ M</code>, where <code class="language-plaintext highlighter-rouge">M</code>
provides evidence that <code class="language-plaintext highlighter-rouge">A</code> holds, or <code class="language-plaintext highlighter-rouge">inj₂ N</code>, where <code class="language-plaintext highlighter-rouge">N</code> provides
evidence that <code class="language-plaintext highlighter-rouge">B</code> holds.</p>
<p>Given evidence that <code class="language-plaintext highlighter-rouge">A → C</code> and <code class="language-plaintext highlighter-rouge">B → C</code> both hold, then given
evidence that <code class="language-plaintext highlighter-rouge">A ⊎ B</code> holds we can conclude that <code class="language-plaintext highlighter-rouge">C</code> holds:</p>
<pre class="Agda"><a id="case-⊎"></a><a id="11674" href="/20.07/Connectives/#11674" class="Function">case-⊎</a> <a id="11681" class="Symbol">:</a> <a id="11683" class="Symbol">∀</a> <a id="11685" class="Symbol">{</a><a id="11686" href="/20.07/Connectives/#11686" class="Bound">A</a> <a id="11688" href="/20.07/Connectives/#11688" class="Bound">B</a> <a id="11690" href="/20.07/Connectives/#11690" class="Bound">C</a> <a id="11692" class="Symbol">:</a> <a id="11694" class="PrimitiveType">Set</a><a id="11697" class="Symbol">}</a>
<a id="11701" class="Symbol">→</a> <a id="11703" class="Symbol">(</a><a id="11704" href="/20.07/Connectives/#11686" class="Bound">A</a> <a id="11706" class="Symbol">→</a> <a id="11708" href="/20.07/Connectives/#11690" class="Bound">C</a><a id="11709" class="Symbol">)</a>
<a id="11713" class="Symbol">→</a> <a id="11715" class="Symbol">(</a><a id="11716" href="/20.07/Connectives/#11688" class="Bound">B</a> <a id="11718" class="Symbol">→</a> <a id="11720" href="/20.07/Connectives/#11690" class="Bound">C</a><a id="11721" class="Symbol">)</a>
<a id="11725" class="Symbol">→</a> <a id="11727" href="/20.07/Connectives/#11686" class="Bound">A</a> <a id="11729" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="11731" href="/20.07/Connectives/#11688" class="Bound">B</a>
<a id="11737" class="Comment">-----------</a>
<a id="11751" class="Symbol">→</a> <a id="11753" href="/20.07/Connectives/#11690" class="Bound">C</a>
<a id="11755" href="/20.07/Connectives/#11674" class="Function">case-⊎</a> <a id="11762" href="/20.07/Connectives/#11762" class="Bound">f</a> <a id="11764" href="/20.07/Connectives/#11764" class="Bound">g</a> <a id="11766" class="Symbol">(</a><a id="11767" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="11772" href="/20.07/Connectives/#11772" class="Bound">x</a><a id="11773" class="Symbol">)</a> <a id="11775" class="Symbol">=</a> <a id="11777" href="/20.07/Connectives/#11762" class="Bound">f</a> <a id="11779" href="/20.07/Connectives/#11772" class="Bound">x</a>
<a id="11781" href="/20.07/Connectives/#11674" class="Function">case-⊎</a> <a id="11788" href="/20.07/Connectives/#11788" class="Bound">f</a> <a id="11790" href="/20.07/Connectives/#11790" class="Bound">g</a> <a id="11792" class="Symbol">(</a><a id="11793" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="11798" href="/20.07/Connectives/#11798" class="Bound">y</a><a id="11799" class="Symbol">)</a> <a id="11801" class="Symbol">=</a> <a id="11803" href="/20.07/Connectives/#11790" class="Bound">g</a> <a id="11805" href="/20.07/Connectives/#11798" class="Bound">y</a>
</pre>
<p>Pattern matching against <code class="language-plaintext highlighter-rouge">inj₁</code> and <code class="language-plaintext highlighter-rouge">inj₂</code> is typical of how we exploit
evidence that a disjunction holds.</p>
<p>When <code class="language-plaintext highlighter-rouge">inj₁</code> and <code class="language-plaintext highlighter-rouge">inj₂</code> appear on the right-hand side of an equation we
refer to them as <em>constructors</em>, and when they appear on the
left-hand side we refer to them as <em>destructors</em>. We also refer to
<code class="language-plaintext highlighter-rouge">case-⊎</code> as a destructor, since it plays a similar role. Other
terminology refers to <code class="language-plaintext highlighter-rouge">inj₁</code> and <code class="language-plaintext highlighter-rouge">inj₂</code> as <em>introducing</em> a
disjunction, and to <code class="language-plaintext highlighter-rouge">case-⊎</code> as <em>eliminating</em> a disjunction; indeed
the former are sometimes given the names <code class="language-plaintext highlighter-rouge">⊎-I₁</code> and <code class="language-plaintext highlighter-rouge">⊎-I₂</code> and the
latter the name <code class="language-plaintext highlighter-rouge">⊎-E</code>.</p>
<p>Applying the destructor to each of the constructors is the identity:</p>
<pre class="Agda"><a id="η-⊎"></a><a id="12474" href="/20.07/Connectives/#12474" class="Function">η-⊎</a> <a id="12478" class="Symbol">:</a> <a id="12480" class="Symbol">∀</a> <a id="12482" class="Symbol">{</a><a id="12483" href="/20.07/Connectives/#12483" class="Bound">A</a> <a id="12485" href="/20.07/Connectives/#12485" class="Bound">B</a> <a id="12487" class="Symbol">:</a> <a id="12489" class="PrimitiveType">Set</a><a id="12492" class="Symbol">}</a> <a id="12494" class="Symbol">(</a><a id="12495" href="/20.07/Connectives/#12495" class="Bound">w</a> <a id="12497" class="Symbol">:</a> <a id="12499" href="/20.07/Connectives/#12483" class="Bound">A</a> <a id="12501" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="12503" href="/20.07/Connectives/#12485" class="Bound">B</a><a id="12504" class="Symbol">)</a> <a id="12506" class="Symbol">→</a> <a id="12508" href="/20.07/Connectives/#11674" class="Function">case-⊎</a> <a id="12515" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="12520" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="12525" href="/20.07/Connectives/#12495" class="Bound">w</a> <a id="12527" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="12529" href="/20.07/Connectives/#12495" class="Bound">w</a>
<a id="12531" href="/20.07/Connectives/#12474" class="Function">η-⊎</a> <a id="12535" class="Symbol">(</a><a id="12536" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="12541" href="/20.07/Connectives/#12541" class="Bound">x</a><a id="12542" class="Symbol">)</a> <a id="12544" class="Symbol">=</a> <a id="12546" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="12551" href="/20.07/Connectives/#12474" class="Function">η-⊎</a> <a id="12555" class="Symbol">(</a><a id="12556" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="12561" href="/20.07/Connectives/#12561" class="Bound">y</a><a id="12562" class="Symbol">)</a> <a id="12564" class="Symbol">=</a> <a id="12566" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre>
<p>More generally, we can also throw in an arbitrary function from a disjunction:</p>
<pre class="Agda"><a id="uniq-⊎"></a><a id="12658" href="/20.07/Connectives/#12658" class="Function">uniq-⊎</a> <a id="12665" class="Symbol">:</a> <a id="12667" class="Symbol">∀</a> <a id="12669" class="Symbol">{</a><a id="12670" href="/20.07/Connectives/#12670" class="Bound">A</a> <a id="12672" href="/20.07/Connectives/#12672" class="Bound">B</a> <a id="12674" href="/20.07/Connectives/#12674" class="Bound">C</a> <a id="12676" class="Symbol">:</a> <a id="12678" class="PrimitiveType">Set</a><a id="12681" class="Symbol">}</a> <a id="12683" class="Symbol">(</a><a id="12684" href="/20.07/Connectives/#12684" class="Bound">h</a> <a id="12686" class="Symbol">:</a> <a id="12688" href="/20.07/Connectives/#12670" class="Bound">A</a> <a id="12690" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="12692" href="/20.07/Connectives/#12672" class="Bound">B</a> <a id="12694" class="Symbol">→</a> <a id="12696" href="/20.07/Connectives/#12674" class="Bound">C</a><a id="12697" class="Symbol">)</a> <a id="12699" class="Symbol">(</a><a id="12700" href="/20.07/Connectives/#12700" class="Bound">w</a> <a id="12702" class="Symbol">:</a> <a id="12704" href="/20.07/Connectives/#12670" class="Bound">A</a> <a id="12706" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="12708" href="/20.07/Connectives/#12672" class="Bound">B</a><a id="12709" class="Symbol">)</a> <a id="12711" class="Symbol">→</a>
<a id="12715" href="/20.07/Connectives/#11674" class="Function">case-⊎</a> <a id="12722" class="Symbol">(</a><a id="12723" href="/20.07/Connectives/#12684" class="Bound">h</a> <a id="12725" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">∘</a> <a id="12727" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a><a id="12731" class="Symbol">)</a> <a id="12733" class="Symbol">(</a><a id="12734" href="/20.07/Connectives/#12684" class="Bound">h</a> <a id="12736" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">∘</a> <a id="12738" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a><a id="12742" class="Symbol">)</a> <a id="12744" href="/20.07/Connectives/#12700" class="Bound">w</a> <a id="12746" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="12748" href="/20.07/Connectives/#12684" class="Bound">h</a> <a id="12750" href="/20.07/Connectives/#12700" class="Bound">w</a>
<a id="12752" href="/20.07/Connectives/#12658" class="Function">uniq-⊎</a> <a id="12759" href="/20.07/Connectives/#12759" class="Bound">h</a> <a id="12761" class="Symbol">(</a><a id="12762" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="12767" href="/20.07/Connectives/#12767" class="Bound">x</a><a id="12768" class="Symbol">)</a> <a id="12770" class="Symbol">=</a> <a id="12772" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="12777" href="/20.07/Connectives/#12658" class="Function">uniq-⊎</a> <a id="12784" href="/20.07/Connectives/#12784" class="Bound">h</a> <a id="12786" class="Symbol">(</a><a id="12787" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="12792" href="/20.07/Connectives/#12792" class="Bound">y</a><a id="12793" class="Symbol">)</a> <a id="12795" class="Symbol">=</a> <a id="12797" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre>
<p>The pattern matching on the left-hand side is essential. Replacing
<code class="language-plaintext highlighter-rouge">w</code> by <code class="language-plaintext highlighter-rouge">inj₁ x</code> allows both sides of the propositional equality to
simplify to the same term, and similarly for <code class="language-plaintext highlighter-rouge">inj₂ y</code>.</p>
<p>We set the precedence of disjunction so that it binds less tightly
than any other declared operator:</p>
<pre class="Agda"><a id="13102" class="Keyword">infixr</a> <a id="13109" class="Number">1</a> <a id="13111" href="/20.07/Connectives/#11270" class="Datatype Operator">_⊎_</a>
</pre>
<p>Thus, <code class="language-plaintext highlighter-rouge">A × C ⊎ B × C</code> parses as <code class="language-plaintext highlighter-rouge">(A × C) ⊎ (B × C)</code>.</p>
<p>Given two types <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>, we refer to <code class="language-plaintext highlighter-rouge">A ⊎ B</code> as the
<em>sum</em> of <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>. In set theory, it is also sometimes
called the <em>disjoint union</em>, and in computing it corresponds
to a <em>variant record</em> type. Among other reasons for
calling it the sum, note that if type <code class="language-plaintext highlighter-rouge">A</code> has <code class="language-plaintext highlighter-rouge">m</code>
distinct members, and type <code class="language-plaintext highlighter-rouge">B</code> has <code class="language-plaintext highlighter-rouge">n</code> distinct members,
then the type <code class="language-plaintext highlighter-rouge">A ⊎ B</code> has <code class="language-plaintext highlighter-rouge">m + n</code> distinct members.
For instance, consider a type <code class="language-plaintext highlighter-rouge">Bool</code> with two members, and
a type <code class="language-plaintext highlighter-rouge">Tri</code> with three members, as defined earlier.
Then the type <code class="language-plaintext highlighter-rouge">Bool ⊎ Tri</code> has five
members:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>inj₁ true inj₂ aa
inj₁ false inj₂ bb
inj₂ cc
</code></pre></div></div>
<p>For example, the following function enumerates all
possible arguments of type <code class="language-plaintext highlighter-rouge">Bool ⊎ Tri</code>:</p>
<pre class="Agda"><a id="⊎-count"></a><a id="13893" href="/20.07/Connectives/#13893" class="Function">⊎-count</a> <a id="13901" class="Symbol">:</a> <a id="13903" href="/20.07/Connectives/#5019" class="Datatype">Bool</a> <a id="13908" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="13910" href="/20.07/Connectives/#5072" class="Datatype">Tri</a> <a id="13914" class="Symbol">→</a> <a id="13916" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="13918" href="/20.07/Connectives/#13893" class="Function">⊎-count</a> <a id="13926" class="Symbol">(</a><a id="13927" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="13932" href="/20.07/Connectives/#5038" class="InductiveConstructor">true</a><a id="13936" class="Symbol">)</a> <a id="13940" class="Symbol">=</a> <a id="13943" class="Number">1</a>
<a id="13945" href="/20.07/Connectives/#13893" class="Function">⊎-count</a> <a id="13953" class="Symbol">(</a><a id="13954" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="13959" href="/20.07/Connectives/#5053" class="InductiveConstructor">false</a><a id="13964" class="Symbol">)</a> <a id="13967" class="Symbol">=</a> <a id="13970" class="Number">2</a>
<a id="13972" href="/20.07/Connectives/#13893" class="Function">⊎-count</a> <a id="13980" class="Symbol">(</a><a id="13981" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="13986" href="/20.07/Connectives/#5090" class="InductiveConstructor">aa</a><a id="13988" class="Symbol">)</a> <a id="13994" class="Symbol">=</a> <a id="13997" class="Number">3</a>
<a id="13999" href="/20.07/Connectives/#13893" class="Function">⊎-count</a> <a id="14007" class="Symbol">(</a><a id="14008" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="14013" href="/20.07/Connectives/#5101" class="InductiveConstructor">bb</a><a id="14015" class="Symbol">)</a> <a id="14021" class="Symbol">=</a> <a id="14024" class="Number">4</a>
<a id="14026" href="/20.07/Connectives/#13893" class="Function">⊎-count</a> <a id="14034" class="Symbol">(</a><a id="14035" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="14040" href="/20.07/Connectives/#5112" class="InductiveConstructor">cc</a><a id="14042" class="Symbol">)</a> <a id="14048" class="Symbol">=</a> <a id="14051" class="Number">5</a>
</pre>
<p>Sum on types also shares a property with sum on numbers in that it is
commutative and associative <em>up to isomorphism</em>.</p>
<h4 id="exercise--comm-recommended">Exercise <code class="language-plaintext highlighter-rouge">⊎-comm</code> (recommended)</h4>
<p>Show sum is commutative up to isomorphism.</p>
<pre class="Agda"><a id="14264" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise--assoc-practice">Exercise <code class="language-plaintext highlighter-rouge">⊎-assoc</code> (practice)</h4>
<p>Show sum is associative up to isomorphism.</p>
<pre class="Agda"><a id="14376" class="Comment">-- Your code goes here</a>
</pre>
<h2 id="false-is-empty">False is empty</h2>
<p>False <code class="language-plaintext highlighter-rouge">⊥</code> never holds. We formalise this idea by declaring
a suitable inductive type:</p>
<pre class="Agda"><a id="14514" class="Keyword">data</a> <a id="⊥"></a><a id="14519" href="/20.07/Connectives/#14519" class="Datatype">⊥</a> <a id="14521" class="Symbol">:</a> <a id="14523" class="PrimitiveType">Set</a> <a id="14527" class="Keyword">where</a>
<a id="14535" class="Comment">-- no clauses!</a>
</pre>
<p>There is no possible evidence that <code class="language-plaintext highlighter-rouge">⊥</code> holds.</p>
<p>Dual to <code class="language-plaintext highlighter-rouge">⊤</code>, for <code class="language-plaintext highlighter-rouge">⊥</code> 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 <code class="language-plaintext highlighter-rouge">⊥</code> holds, we might
conclude anything! This is a basic principle of logic, known in
medieval times by the Latin phrase <em>ex falso</em>, 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:</p>
<pre class="Agda"><a id="⊥-elim"></a><a id="15053" href="/20.07/Connectives/#15053" class="Function">⊥-elim</a> <a id="15060" class="Symbol">:</a> <a id="15062" class="Symbol">∀</a> <a id="15064" class="Symbol">{</a><a id="15065" href="/20.07/Connectives/#15065" class="Bound">A</a> <a id="15067" class="Symbol">:</a> <a id="15069" class="PrimitiveType">Set</a><a id="15072" class="Symbol">}</a>
<a id="15076" class="Symbol">→</a> <a id="15078" href="/20.07/Connectives/#14519" class="Datatype">⊥</a>
<a id="15084" class="Comment">--</a>
<a id="15089" class="Symbol">→</a> <a id="15091" href="/20.07/Connectives/#15065" class="Bound">A</a>
<a id="15093" href="/20.07/Connectives/#15053" class="Function">⊥-elim</a> <a id="15100" class="Symbol">()</a>
</pre>
<p>This is our first use of the <em>absurd pattern</em> <code class="language-plaintext highlighter-rouge">()</code>.
Here since <code class="language-plaintext highlighter-rouge">⊥</code> is a type with no members, we indicate that it is
<em>never</em> possible to match against a value of this type by using
the pattern <code class="language-plaintext highlighter-rouge">()</code>.</p>
<p>The nullary case of <code class="language-plaintext highlighter-rouge">case-⊎</code> is <code class="language-plaintext highlighter-rouge">⊥-elim</code>. By analogy,
we might have called it <code class="language-plaintext highlighter-rouge">case-⊥</code>, but chose to stick with the name
in the standard library.</p>
<p>The nullary case of <code class="language-plaintext highlighter-rouge">uniq-⊎</code> is <code class="language-plaintext highlighter-rouge">uniq-⊥</code>, which asserts that <code class="language-plaintext highlighter-rouge">⊥-elim</code>
is equal to any arbitrary function from <code class="language-plaintext highlighter-rouge">⊥</code>:</p>
<pre class="Agda"><a id="uniq-⊥"></a><a id="15574" href="/20.07/Connectives/#15574" class="Function">uniq-⊥</a> <a id="15581" class="Symbol">:</a> <a id="15583" class="Symbol">∀</a> <a id="15585" class="Symbol">{</a><a id="15586" href="/20.07/Connectives/#15586" class="Bound">C</a> <a id="15588" class="Symbol">:</a> <a id="15590" class="PrimitiveType">Set</a><a id="15593" class="Symbol">}</a> <a id="15595" class="Symbol">(</a><a id="15596" href="/20.07/Connectives/#15596" class="Bound">h</a> <a id="15598" class="Symbol">:</a> <a id="15600" href="/20.07/Connectives/#14519" class="Datatype">⊥</a> <a id="15602" class="Symbol">→</a> <a id="15604" href="/20.07/Connectives/#15586" class="Bound">C</a><a id="15605" class="Symbol">)</a> <a id="15607" class="Symbol">(</a><a id="15608" href="/20.07/Connectives/#15608" class="Bound">w</a> <a id="15610" class="Symbol">:</a> <a id="15612" href="/20.07/Connectives/#14519" class="Datatype">⊥</a><a id="15613" class="Symbol">)</a> <a id="15615" class="Symbol">→</a> <a id="15617" href="/20.07/Connectives/#15053" class="Function">⊥-elim</a> <a id="15624" href="/20.07/Connectives/#15608" class="Bound">w</a> <a id="15626" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="15628" href="/20.07/Connectives/#15596" class="Bound">h</a> <a id="15630" href="/20.07/Connectives/#15608" class="Bound">w</a>
<a id="15632" href="/20.07/Connectives/#15574" class="Function">uniq-⊥</a> <a id="15639" href="/20.07/Connectives/#15639" class="Bound">h</a> <a id="15641" class="Symbol">()</a>
</pre>
<p>Using the absurd pattern asserts there are no possible values for <code class="language-plaintext highlighter-rouge">w</code>,
so the equation holds trivially.</p>
<p>We refer to <code class="language-plaintext highlighter-rouge">⊥</code> as the <em>empty</em> type. And, indeed,
type <code class="language-plaintext highlighter-rouge">⊥</code> has no members. For example, the following function
enumerates all possible arguments of type <code class="language-plaintext highlighter-rouge">⊥</code>:</p>
<pre class="Agda"><a id="⊥-count"></a><a id="15915" href="/20.07/Connectives/#15915" class="Function">⊥-count</a> <a id="15923" class="Symbol">:</a> <a id="15925" href="/20.07/Connectives/#14519" class="Datatype">⊥</a> <a id="15927" class="Symbol">→</a> <a id="15929" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="15931" href="/20.07/Connectives/#15915" class="Function">⊥-count</a> <a id="15939" class="Symbol">()</a>
</pre>
<p>Here again the absurd pattern <code class="language-plaintext highlighter-rouge">()</code> indicates that no value can match
type <code class="language-plaintext highlighter-rouge">⊥</code>.</p>
<p>For numbers, zero is the identity of addition. Correspondingly, empty
is the identity of sums <em>up to isomorphism</em>.</p>
<h4 id="exercise--identityˡ-recommended">Exercise <code class="language-plaintext highlighter-rouge">⊥-identityˡ</code> (recommended)</h4>
<p>Show empty is the left identity of sums up to isomorphism.</p>
<pre class="Agda"><a id="16249" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise--identityʳ-practice">Exercise <code class="language-plaintext highlighter-rouge">⊥-identityʳ</code> (practice)</h4>
<p>Show empty is the right identity of sums up to isomorphism.</p>
<pre class="Agda"><a id="16382" class="Comment">-- Your code goes here</a>
</pre>
<h2 id="implication">Implication is function</h2>
<p>Given two propositions <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>, the implication <code class="language-plaintext highlighter-rouge">A → B</code> holds if
whenever <code class="language-plaintext highlighter-rouge">A</code> holds then <code class="language-plaintext highlighter-rouge">B</code> must also hold. We formalise implication using
the function type, which has appeared throughout this book.</p>
<p>Evidence that <code class="language-plaintext highlighter-rouge">A → B</code> holds is of the form</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>λ (x : A) → N
</code></pre></div></div>
<p>where <code class="language-plaintext highlighter-rouge">N</code> is a term of type <code class="language-plaintext highlighter-rouge">B</code> containing as a free variable <code class="language-plaintext highlighter-rouge">x</code> of type <code class="language-plaintext highlighter-rouge">A</code>.
Given a term <code class="language-plaintext highlighter-rouge">L</code> providing evidence that <code class="language-plaintext highlighter-rouge">A → B</code> holds, and a term <code class="language-plaintext highlighter-rouge">M</code>
providing evidence that <code class="language-plaintext highlighter-rouge">A</code> holds, the term <code class="language-plaintext highlighter-rouge">L M</code> provides evidence that
<code class="language-plaintext highlighter-rouge">B</code> holds. In other words, evidence that <code class="language-plaintext highlighter-rouge">A → B</code> holds is a function that
converts evidence that <code class="language-plaintext highlighter-rouge">A</code> holds into evidence that <code class="language-plaintext highlighter-rouge">B</code> holds.</p>
<p>Put another way, if we know that <code class="language-plaintext highlighter-rouge">A → B</code> and <code class="language-plaintext highlighter-rouge">A</code> both hold,
then we may conclude that <code class="language-plaintext highlighter-rouge">B</code> holds:</p>
<pre class="Agda"><a id="→-elim"></a><a id="17185" href="/20.07/Connectives/#17185" class="Function">→-elim</a> <a id="17192" class="Symbol">:</a> <a id="17194" class="Symbol">∀</a> <a id="17196" class="Symbol">{</a><a id="17197" href="/20.07/Connectives/#17197" class="Bound">A</a> <a id="17199" href="/20.07/Connectives/#17199" class="Bound">B</a> <a id="17201" class="Symbol">:</a> <a id="17203" class="PrimitiveType">Set</a><a id="17206" class="Symbol">}</a>
<a id="17210" class="Symbol">→</a> <a id="17212" class="Symbol">(</a><a id="17213" href="/20.07/Connectives/#17197" class="Bound">A</a> <a id="17215" class="Symbol">→</a> <a id="17217" href="/20.07/Connectives/#17199" class="Bound">B</a><a id="17218" class="Symbol">)</a>
<a id="17222" class="Symbol">→</a> <a id="17224" href="/20.07/Connectives/#17197" class="Bound">A</a>
<a id="17230" class="Comment">-------</a>
<a id="17240" class="Symbol">→</a> <a id="17242" href="/20.07/Connectives/#17199" class="Bound">B</a>
<a id="17244" href="/20.07/Connectives/#17185" class="Function">→-elim</a> <a id="17251" href="/20.07/Connectives/#17251" class="Bound">L</a> <a id="17253" href="/20.07/Connectives/#17253" class="Bound">M</a> <a id="17255" class="Symbol">=</a> <a id="17257" href="/20.07/Connectives/#17251" class="Bound">L</a> <a id="17259" href="/20.07/Connectives/#17253" class="Bound">M</a>
</pre>
<p>In medieval times, this rule was known by the name <em>modus ponens</em>.
It corresponds to function application.</p>
<p>Defining a function, with a named definition or a lambda abstraction,
is referred to as <em>introducing</em> a function,
while applying a function is referred to as <em>eliminating</em> the function.</p>
<p>Elimination followed by introduction is the identity:</p>
<pre class="Agda"><a id="η-→"></a><a id="17618" href="/20.07/Connectives/#17618" class="Function">η-→</a> <a id="17622" class="Symbol">:</a> <a id="17624" class="Symbol">∀</a> <a id="17626" class="Symbol">{</a><a id="17627" href="/20.07/Connectives/#17627" class="Bound">A</a> <a id="17629" href="/20.07/Connectives/#17629" class="Bound">B</a> <a id="17631" class="Symbol">:</a> <a id="17633" class="PrimitiveType">Set</a><a id="17636" class="Symbol">}</a> <a id="17638" class="Symbol">(</a><a id="17639" href="/20.07/Connectives/#17639" class="Bound">f</a> <a id="17641" class="Symbol">:</a> <a id="17643" href="/20.07/Connectives/#17627" class="Bound">A</a> <a id="17645" class="Symbol">→</a> <a id="17647" href="/20.07/Connectives/#17629" class="Bound">B</a><a id="17648" class="Symbol">)</a> <a id="17650" class="Symbol">→</a> <a id="17652" class="Symbol">(λ</a> <a id="17655" class="Symbol">(</a><a id="17656" href="/20.07/Connectives/#17656" class="Bound">x</a> <a id="17658" class="Symbol">:</a> <a id="17660" href="/20.07/Connectives/#17627" class="Bound">A</a><a id="17661" class="Symbol">)</a> <a id="17663" class="Symbol">→</a> <a id="17665" href="/20.07/Connectives/#17639" class="Bound">f</a> <a id="17667" href="/20.07/Connectives/#17656" class="Bound">x</a><a id="17668" class="Symbol">)</a> <a id="17670" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="17672" href="/20.07/Connectives/#17639" class="Bound">f</a>
<a id="17674" href="/20.07/Connectives/#17618" class="Function">η-→</a> <a id="17678" href="/20.07/Connectives/#17678" class="Bound">f</a> <a id="17680" class="Symbol">=</a> <a id="17682" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre>
<p>Implication binds less tightly than any other operator. Thus, <code class="language-plaintext highlighter-rouge">A ⊎ B →
B ⊎ A</code> parses as <code class="language-plaintext highlighter-rouge">(A ⊎ B) → (B ⊎ A)</code>.</p>
<p>Given two types <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code>, we refer to <code class="language-plaintext highlighter-rouge">A → B</code> as the <em>function</em>
space from <code class="language-plaintext highlighter-rouge">A</code> to <code class="language-plaintext highlighter-rouge">B</code>. It is also sometimes called the <em>exponential</em>,
with <code class="language-plaintext highlighter-rouge">B</code> raised to the <code class="language-plaintext highlighter-rouge">A</code> power. Among other reasons for calling
it the exponential, note that if type <code class="language-plaintext highlighter-rouge">A</code> has <code class="language-plaintext highlighter-rouge">m</code> distinct
members, and type <code class="language-plaintext highlighter-rouge">B</code> has <code class="language-plaintext highlighter-rouge">n</code> distinct members, then the type
<code class="language-plaintext highlighter-rouge">A → B</code> has <code class="language-plaintext highlighter-rouge">nᵐ</code> distinct members. For instance, consider a
type <code class="language-plaintext highlighter-rouge">Bool</code> with two members and a type <code class="language-plaintext highlighter-rouge">Tri</code> with three members,
as defined earlier. Then the type <code class="language-plaintext highlighter-rouge">Bool → Tri</code> has nine (that is,
three squared) members:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>λ{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}
</code></pre></div></div>
<p>For example, the following function enumerates all possible
arguments of the type <code class="language-plaintext highlighter-rouge">Bool → Tri</code>:</p>
<pre class="Agda"><a id="→-count"></a><a id="18690" href="/20.07/Connectives/#18690" class="Function">→-count</a> <a id="18698" class="Symbol">:</a> <a id="18700" class="Symbol">(</a><a id="18701" href="/20.07/Connectives/#5019" class="Datatype">Bool</a> <a id="18706" class="Symbol">→</a> <a id="18708" href="/20.07/Connectives/#5072" class="Datatype">Tri</a><a id="18711" class="Symbol">)</a> <a id="18713" class="Symbol">→</a> <a id="18715" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="18717" href="/20.07/Connectives/#18690" class="Function">→-count</a> <a id="18725" href="/20.07/Connectives/#18725" class="Bound">f</a> <a id="18727" class="Keyword">with</a> <a id="18732" href="/20.07/Connectives/#18725" class="Bound">f</a> <a id="18734" href="/20.07/Connectives/#5038" class="InductiveConstructor">true</a> <a id="18739" class="Symbol">|</a> <a id="18741" href="/20.07/Connectives/#18725" class="Bound">f</a> <a id="18743" href="/20.07/Connectives/#5053" class="InductiveConstructor">false</a>
<a id="18749" class="Symbol">...</a> <a id="18762" class="Symbol">|</a> <a id="18764" href="/20.07/Connectives/#5090" class="InductiveConstructor">aa</a> <a id="18771" class="Symbol">|</a> <a id="18773" href="/20.07/Connectives/#5090" class="InductiveConstructor">aa</a> <a id="18781" class="Symbol">=</a> <a id="18785" class="Number">1</a>
<a id="18787" class="Symbol">...</a> <a id="18800" class="Symbol">|</a> <a id="18802" href="/20.07/Connectives/#5090" class="InductiveConstructor">aa</a> <a id="18809" class="Symbol">|</a> <a id="18811" href="/20.07/Connectives/#5101" class="InductiveConstructor">bb</a> <a id="18819" class="Symbol">=</a> <a id="18823" class="Number">2</a>
<a id="18825" class="Symbol">...</a> <a id="18838" class="Symbol">|</a> <a id="18840" href="/20.07/Connectives/#5090" class="InductiveConstructor">aa</a> <a id="18847" class="Symbol">|</a> <a id="18849" href="/20.07/Connectives/#5112" class="InductiveConstructor">cc</a> <a id="18857" class="Symbol">=</a> <a id="18861" class="Number">3</a>
<a id="18863" class="Symbol">...</a> <a id="18876" class="Symbol">|</a> <a id="18878" href="/20.07/Connectives/#5101" class="InductiveConstructor">bb</a> <a id="18885" class="Symbol">|</a> <a id="18887" href="/20.07/Connectives/#5090" class="InductiveConstructor">aa</a> <a id="18895" class="Symbol">=</a> <a id="18899" class="Number">4</a>
<a id="18901" class="Symbol">...</a> <a id="18914" class="Symbol">|</a> <a id="18916" href="/20.07/Connectives/#5101" class="InductiveConstructor">bb</a> <a id="18923" class="Symbol">|</a> <a id="18925" href="/20.07/Connectives/#5101" class="InductiveConstructor">bb</a> <a id="18933" class="Symbol">=</a> <a id="18937" class="Number">5</a>
<a id="18939" class="Symbol">...</a> <a id="18952" class="Symbol">|</a> <a id="18954" href="/20.07/Connectives/#5101" class="InductiveConstructor">bb</a> <a id="18961" class="Symbol">|</a> <a id="18963" href="/20.07/Connectives/#5112" class="InductiveConstructor">cc</a> <a id="18971" class="Symbol">=</a> <a id="18975" class="Number">6</a>
<a id="18977" class="Symbol">...</a> <a id="18990" class="Symbol">|</a> <a id="18992" href="/20.07/Connectives/#5112" class="InductiveConstructor">cc</a> <a id="18999" class="Symbol">|</a> <a id="19001" href="/20.07/Connectives/#5090" class="InductiveConstructor">aa</a> <a id="19009" class="Symbol">=</a> <a id="19013" class="Number">7</a>
<a id="19015" class="Symbol">...</a> <a id="19028" class="Symbol">|</a> <a id="19030" href="/20.07/Connectives/#5112" class="InductiveConstructor">cc</a> <a id="19037" class="Symbol">|</a> <a id="19039" href="/20.07/Connectives/#5101" class="InductiveConstructor">bb</a> <a id="19047" class="Symbol">=</a> <a id="19051" class="Number">8</a>
<a id="19053" class="Symbol">...</a> <a id="19066" class="Symbol">|</a> <a id="19068" href="/20.07/Connectives/#5112" class="InductiveConstructor">cc</a> <a id="19075" class="Symbol">|</a> <a id="19077" href="/20.07/Connectives/#5112" class="InductiveConstructor">cc</a> <a id="19085" class="Symbol">=</a> <a id="19089" class="Number">9</a>
</pre>
<p>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.</p>
<p>Corresponding to the law</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(p ^ n) ^ m ≡ p ^ (n * m)
</code></pre></div></div>
<p>we have the isomorphism</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>A → (B → C) ≃ (A × B) → C
</code></pre></div></div>
<p>Both types can be viewed as functions that given evidence that <code class="language-plaintext highlighter-rouge">A</code> holds
and evidence that <code class="language-plaintext highlighter-rouge">B</code> holds can return evidence that <code class="language-plaintext highlighter-rouge">C</code> holds.
This isomorphism sometimes goes by the name <em>currying</em>.
The proof of the right inverse requires extensionality:</p>
<pre class="Agda"><a id="currying"></a><a id="19615" href="/20.07/Connectives/#19615" class="Function">currying</a> <a id="19624" class="Symbol">:</a> <a id="19626" class="Symbol">∀</a> <a id="19628" class="Symbol">{</a><a id="19629" href="/20.07/Connectives/#19629" class="Bound">A</a> <a id="19631" href="/20.07/Connectives/#19631" class="Bound">B</a> <a id="19633" href="/20.07/Connectives/#19633" class="Bound">C</a> <a id="19635" class="Symbol">:</a> <a id="19637" class="PrimitiveType">Set</a><a id="19640" class="Symbol">}</a> <a id="19642" class="Symbol">→</a> <a id="19644" class="Symbol">(</a><a id="19645" href="/20.07/Connectives/#19629" class="Bound">A</a> <a id="19647" class="Symbol">→</a> <a id="19649" href="/20.07/Connectives/#19631" class="Bound">B</a> <a id="19651" class="Symbol">→</a> <a id="19653" href="/20.07/Connectives/#19633" class="Bound">C</a><a id="19654" class="Symbol">)</a> <a id="19656" href="/20.07/Isomorphism/#4365" class="Record Operator">≃</a> <a id="19658" class="Symbol">(</a><a id="19659" href="/20.07/Connectives/#19629" class="Bound">A</a> <a id="19661" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="19663" href="/20.07/Connectives/#19631" class="Bound">B</a> <a id="19665" class="Symbol">→</a> <a id="19667" href="/20.07/Connectives/#19633" class="Bound">C</a><a id="19668" class="Symbol">)</a>
<a id="19670" href="/20.07/Connectives/#19615" class="Function">currying</a> <a id="19679" class="Symbol">=</a>
<a id="19683" class="Keyword">record</a>
<a id="19694" class="Symbol">{</a> <a id="19696" href="/20.07/Isomorphism/#4405" class="Field">to</a> <a id="19704" class="Symbol">=</a> <a id="19707" class="Symbol">λ{</a> <a id="19710" href="/20.07/Connectives/#19710" class="Bound">f</a> <a id="19712" class="Symbol">→</a> <a id="19714" class="Symbol">λ{</a> <a id="19717" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="19719" href="/20.07/Connectives/#19719" class="Bound">x</a> <a id="19721" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="19723" href="/20.07/Connectives/#19723" class="Bound">y</a> <a id="19725" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="19727" class="Symbol">→</a> <a id="19729" href="/20.07/Connectives/#19710" class="Bound">f</a> <a id="19731" href="/20.07/Connectives/#19719" class="Bound">x</a> <a id="19733" href="/20.07/Connectives/#19723" class="Bound">y</a> <a id="19735" class="Symbol">}}</a>
<a id="19742" class="Symbol">;</a> <a id="19744" href="/20.07/Isomorphism/#4422" class="Field">from</a> <a id="19752" class="Symbol">=</a> <a id="19755" class="Symbol">λ{</a> <a id="19758" href="/20.07/Connectives/#19758" class="Bound">g</a> <a id="19760" class="Symbol">→</a> <a id="19762" class="Symbol">λ{</a> <a id="19765" href="/20.07/Connectives/#19765" class="Bound">x</a> <a id="19767" class="Symbol">→</a> <a id="19769" class="Symbol">λ{</a> <a id="19772" href="/20.07/Connectives/#19772" class="Bound">y</a> <a id="19774" class="Symbol">→</a> <a id="19776" href="/20.07/Connectives/#19758" class="Bound">g</a> <a id="19778" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="19780" href="/20.07/Connectives/#19765" class="Bound">x</a> <a id="19782" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="19784" href="/20.07/Connectives/#19772" class="Bound">y</a> <a id="19786" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="19788" class="Symbol">}}}</a>
<a id="19796" class="Symbol">;</a> <a id="19798" href="/20.07/Isomorphism/#4439" class="Field">from∘to</a> <a id="19806" class="Symbol">=</a> <a id="19809" class="Symbol">λ{</a> <a id="19812" href="/20.07/Connectives/#19812" class="Bound">f</a> <a id="19814" class="Symbol">→</a> <a id="19816" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="19821" class="Symbol">}</a>
<a id="19827" class="Symbol">;</a> <a id="19829" href="/20.07/Isomorphism/#4481" class="Field">to∘from</a> <a id="19837" class="Symbol">=</a> <a id="19840" class="Symbol">λ{</a> <a id="19843" href="/20.07/Connectives/#19843" class="Bound">g</a> <a id="19845" class="Symbol">→</a> <a id="19847" href="/20.07/Isomorphism/#2684" class="Postulate">extensionality</a> <a id="19862" class="Symbol">λ{</a> <a id="19865" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="19867" href="/20.07/Connectives/#19867" class="Bound">x</a> <a id="19869" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="19871" href="/20.07/Connectives/#19871" class="Bound">y</a> <a id="19873" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="19875" class="Symbol">→</a> <a id="19877" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="19882" class="Symbol">}}</a>
<a id="19889" class="Symbol">}</a>
</pre>
<p>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</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>_+_ : ℕ → ℕ → ℕ
</code></pre></div></div>
<p>is isomorphic to a function that accepts a pair of arguments:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>_+′_ : (ℕ × ℕ) → ℕ
</code></pre></div></div>
<p>Agda is optimised for currying, so <code class="language-plaintext highlighter-rouge">2 + 3</code> abbreviates <code class="language-plaintext highlighter-rouge">_+_ 2 3</code>.
In a language optimised for pairing, we would instead take <code class="language-plaintext highlighter-rouge">2 +′ 3</code> as
an abbreviation for <code class="language-plaintext highlighter-rouge">_+′_ ⟨ 2 , 3 ⟩</code>.</p>
<p>Corresponding to the law</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>p ^ (n + m) = (p ^ n) * (p ^ m)
</code></pre></div></div>
<p>we have the isomorphism:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(A ⊎ B) → C ≃ (A → C) × (B → C)
</code></pre></div></div>
<p>That is, the assertion that if either <code class="language-plaintext highlighter-rouge">A</code> holds or <code class="language-plaintext highlighter-rouge">B</code> holds then <code class="language-plaintext highlighter-rouge">C</code> holds
is the same as the assertion that if <code class="language-plaintext highlighter-rouge">A</code> holds then <code class="language-plaintext highlighter-rouge">C</code> holds and if
<code class="language-plaintext highlighter-rouge">B</code> holds then <code class="language-plaintext highlighter-rouge">C</code> holds. The proof of the left inverse requires extensionality:</p>
<pre class="Agda"><a id="→-distrib-⊎"></a><a id="20776" href="/20.07/Connectives/#20776" class="Function">→-distrib-⊎</a> <a id="20788" class="Symbol">:</a> <a id="20790" class="Symbol">∀</a> <a id="20792" class="Symbol">{</a><a id="20793" href="/20.07/Connectives/#20793" class="Bound">A</a> <a id="20795" href="/20.07/Connectives/#20795" class="Bound">B</a> <a id="20797" href="/20.07/Connectives/#20797" class="Bound">C</a> <a id="20799" class="Symbol">:</a> <a id="20801" class="PrimitiveType">Set</a><a id="20804" class="Symbol">}</a> <a id="20806" class="Symbol">→</a> <a id="20808" class="Symbol">(</a><a id="20809" href="/20.07/Connectives/#20793" class="Bound">A</a> <a id="20811" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="20813" href="/20.07/Connectives/#20795" class="Bound">B</a> <a id="20815" class="Symbol">→</a> <a id="20817" href="/20.07/Connectives/#20797" class="Bound">C</a><a id="20818" class="Symbol">)</a> <a id="20820" href="/20.07/Isomorphism/#4365" class="Record Operator">≃</a> <a id="20822" class="Symbol">((</a><a id="20824" href="/20.07/Connectives/#20793" class="Bound">A</a> <a id="20826" class="Symbol">→</a> <a id="20828" href="/20.07/Connectives/#20797" class="Bound">C</a><a id="20829" class="Symbol">)</a> <a id="20831" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="20833" class="Symbol">(</a><a id="20834" href="/20.07/Connectives/#20795" class="Bound">B</a> <a id="20836" class="Symbol">→</a> <a id="20838" href="/20.07/Connectives/#20797" class="Bound">C</a><a id="20839" class="Symbol">))</a>
<a id="20842" href="/20.07/Connectives/#20776" class="Function">→-distrib-⊎</a> <a id="20854" class="Symbol">=</a>
<a id="20858" class="Keyword">record</a>
<a id="20869" class="Symbol">{</a> <a id="20871" href="/20.07/Isomorphism/#4405" class="Field">to</a> <a id="20879" class="Symbol">=</a> <a id="20881" class="Symbol">λ{</a> <a id="20884" href="/20.07/Connectives/#20884" class="Bound">f</a> <a id="20886" class="Symbol">→</a> <a id="20888" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="20890" href="/20.07/Connectives/#20884" class="Bound">f</a> <a id="20892" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">∘</a> <a id="20894" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="20899" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="20901" href="/20.07/Connectives/#20884" class="Bound">f</a> <a id="20903" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">∘</a> <a id="20905" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="20910" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="20912" class="Symbol">}</a>
<a id="20918" class="Symbol">;</a> <a id="20920" href="/20.07/Isomorphism/#4422" class="Field">from</a> <a id="20928" class="Symbol">=</a> <a id="20930" class="Symbol">λ{</a> <a id="20933" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="20935" href="/20.07/Connectives/#20935" class="Bound">g</a> <a id="20937" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="20939" href="/20.07/Connectives/#20939" class="Bound">h</a> <a id="20941" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="20943" class="Symbol">→</a> <a id="20945" class="Symbol">λ{</a> <a id="20948" class="Symbol">(</a><a id="20949" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="20954" href="/20.07/Connectives/#20954" class="Bound">x</a><a id="20955" class="Symbol">)</a> <a id="20957" class="Symbol">→</a> <a id="20959" href="/20.07/Connectives/#20935" class="Bound">g</a> <a id="20961" href="/20.07/Connectives/#20954" class="Bound">x</a> <a id="20963" class="Symbol">;</a> <a id="20965" class="Symbol">(</a><a id="20966" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="20971" href="/20.07/Connectives/#20971" class="Bound">y</a><a id="20972" class="Symbol">)</a> <a id="20974" class="Symbol">→</a> <a id="20976" href="/20.07/Connectives/#20939" class="Bound">h</a> <a id="20978" href="/20.07/Connectives/#20971" class="Bound">y</a> <a id="20980" class="Symbol">}</a> <a id="20982" class="Symbol">}</a>
<a id="20988" class="Symbol">;</a> <a id="20990" href="/20.07/Isomorphism/#4439" class="Field">from∘to</a> <a id="20998" class="Symbol">=</a> <a id="21000" class="Symbol">λ{</a> <a id="21003" href="/20.07/Connectives/#21003" class="Bound">f</a> <a id="21005" class="Symbol">→</a> <a id="21007" href="/20.07/Isomorphism/#2684" class="Postulate">extensionality</a> <a id="21022" class="Symbol">λ{</a> <a id="21025" class="Symbol">(</a><a id="21026" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="21031" href="/20.07/Connectives/#21031" class="Bound">x</a><a id="21032" class="Symbol">)</a> <a id="21034" class="Symbol">→</a> <a id="21036" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="21041" class="Symbol">;</a> <a id="21043" class="Symbol">(</a><a id="21044" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="21049" href="/20.07/Connectives/#21049" class="Bound">y</a><a id="21050" class="Symbol">)</a> <a id="21052" class="Symbol">→</a> <a id="21054" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="21059" class="Symbol">}</a> <a id="21061" class="Symbol">}</a>
<a id="21067" class="Symbol">;</a> <a id="21069" href="/20.07/Isomorphism/#4481" class="Field">to∘from</a> <a id="21077" class="Symbol">=</a> <a id="21079" class="Symbol">λ{</a> <a id="21082" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="21084" href="/20.07/Connectives/#21084" class="Bound">g</a> <a id="21086" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="21088" href="/20.07/Connectives/#21088" class="Bound">h</a> <a id="21090" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="21092" class="Symbol">→</a> <a id="21094" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="21099" class="Symbol">}</a>
<a id="21105" class="Symbol">}</a>
</pre>
<p>Corresponding to the law</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(p * n) ^ m = (p ^ m) * (n ^ m)
</code></pre></div></div>
<p>we have the isomorphism:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>A → B × C ≃ (A → B) × (A → C)
</code></pre></div></div>
<p>That is, the assertion that if <code class="language-plaintext highlighter-rouge">A</code> holds then <code class="language-plaintext highlighter-rouge">B</code> holds and <code class="language-plaintext highlighter-rouge">C</code> holds
is the same as the assertion that if <code class="language-plaintext highlighter-rouge">A</code> holds then <code class="language-plaintext highlighter-rouge">B</code> holds and if
<code class="language-plaintext highlighter-rouge">A</code> holds then <code class="language-plaintext highlighter-rouge">C</code> holds. The proof of left inverse requires both extensionality
and the rule <code class="language-plaintext highlighter-rouge">η-×</code> for products:</p>
<pre class="Agda"><a id="→-distrib-×"></a><a id="21496" href="/20.07/Connectives/#21496" class="Function">→-distrib-×</a> <a id="21508" class="Symbol">:</a> <a id="21510" class="Symbol">∀</a> <a id="21512" class="Symbol">{</a><a id="21513" href="/20.07/Connectives/#21513" class="Bound">A</a> <a id="21515" href="/20.07/Connectives/#21515" class="Bound">B</a> <a id="21517" href="/20.07/Connectives/#21517" class="Bound">C</a> <a id="21519" class="Symbol">:</a> <a id="21521" class="PrimitiveType">Set</a><a id="21524" class="Symbol">}</a> <a id="21526" class="Symbol">→</a> <a id="21528" class="Symbol">(</a><a id="21529" href="/20.07/Connectives/#21513" class="Bound">A</a> <a id="21531" class="Symbol">→</a> <a id="21533" href="/20.07/Connectives/#21515" class="Bound">B</a> <a id="21535" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="21537" href="/20.07/Connectives/#21517" class="Bound">C</a><a id="21538" class="Symbol">)</a> <a id="21540" href="/20.07/Isomorphism/#4365" class="Record Operator">≃</a> <a id="21542" class="Symbol">(</a><a id="21543" href="/20.07/Connectives/#21513" class="Bound">A</a> <a id="21545" class="Symbol">→</a> <a id="21547" href="/20.07/Connectives/#21515" class="Bound">B</a><a id="21548" class="Symbol">)</a> <a id="21550" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="21552" class="Symbol">(</a><a id="21553" href="/20.07/Connectives/#21513" class="Bound">A</a> <a id="21555" class="Symbol">→</a> <a id="21557" href="/20.07/Connectives/#21517" class="Bound">C</a><a id="21558" class="Symbol">)</a>
<a id="21560" href="/20.07/Connectives/#21496" class="Function">→-distrib-×</a> <a id="21572" class="Symbol">=</a>
<a id="21576" class="Keyword">record</a>
<a id="21587" class="Symbol">{</a> <a id="21589" href="/20.07/Isomorphism/#4405" class="Field">to</a> <a id="21597" class="Symbol">=</a> <a id="21599" class="Symbol">λ{</a> <a id="21602" href="/20.07/Connectives/#21602" class="Bound">f</a> <a id="21604" class="Symbol">→</a> <a id="21606" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="21608" href="/20.07/Connectives/#1608" class="Function">proj₁</a> <a id="21614" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">∘</a> <a id="21616" href="/20.07/Connectives/#21602" class="Bound">f</a> <a id="21618" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="21620" href="/20.07/Connectives/#1677" class="Function">proj₂</a> <a id="21626" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">∘</a> <a id="21628" href="/20.07/Connectives/#21602" class="Bound">f</a> <a id="21630" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="21632" class="Symbol">}</a>
<a id="21638" class="Symbol">;</a> <a id="21640" href="/20.07/Isomorphism/#4422" class="Field">from</a> <a id="21648" class="Symbol">=</a> <a id="21650" class="Symbol">λ{</a> <a id="21653" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="21655" href="/20.07/Connectives/#21655" class="Bound">g</a> <a id="21657" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="21659" href="/20.07/Connectives/#21659" class="Bound">h</a> <a id="21661" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="21663" class="Symbol">→</a> <a id="21665" class="Symbol">λ</a> <a id="21667" href="/20.07/Connectives/#21667" class="Bound">x</a> <a id="21669" class="Symbol">→</a> <a id="21671" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="21673" href="/20.07/Connectives/#21655" class="Bound">g</a> <a id="21675" href="/20.07/Connectives/#21667" class="Bound">x</a> <a id="21677" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="21679" href="/20.07/Connectives/#21659" class="Bound">h</a> <a id="21681" href="/20.07/Connectives/#21667" class="Bound">x</a> <a id="21683" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="21685" class="Symbol">}</a>
<a id="21691" class="Symbol">;</a> <a id="21693" href="/20.07/Isomorphism/#4439" class="Field">from∘to</a> <a id="21701" class="Symbol">=</a> <a id="21703" class="Symbol">λ{</a> <a id="21706" href="/20.07/Connectives/#21706" class="Bound">f</a> <a id="21708" class="Symbol">→</a> <a id="21710" href="/20.07/Isomorphism/#2684" class="Postulate">extensionality</a> <a id="21725" class="Symbol">λ{</a> <a id="21728" href="/20.07/Connectives/#21728" class="Bound">x</a> <a id="21730" class="Symbol">→</a> <a id="21732" href="/20.07/Connectives/#3108" class="Function">η-×</a> <a id="21736" class="Symbol">(</a><a id="21737" href="/20.07/Connectives/#21706" class="Bound">f</a> <a id="21739" href="/20.07/Connectives/#21728" class="Bound">x</a><a id="21740" class="Symbol">)</a> <a id="21742" class="Symbol">}</a> <a id="21744" class="Symbol">}</a>
<a id="21750" class="Symbol">;</a> <a id="21752" href="/20.07/Isomorphism/#4481" class="Field">to∘from</a> <a id="21760" class="Symbol">=</a> <a id="21762" class="Symbol">λ{</a> <a id="21765" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="21767" href="/20.07/Connectives/#21767" class="Bound">g</a> <a id="21769" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="21771" href="/20.07/Connectives/#21771" class="Bound">h</a> <a id="21773" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="21775" class="Symbol">→</a> <a id="21777" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="21782" class="Symbol">}</a>
<a id="21788" class="Symbol">}</a>
</pre>
<h2 id="distribution">Distribution</h2>
<p>Products distribute over sum, up to isomorphism. The code to validate
this fact is similar in structure to our previous results:</p>
<pre class="Agda"><a id="×-distrib-⊎"></a><a id="21947" href="/20.07/Connectives/#21947" class="Function">×-distrib-⊎</a> <a id="21959" class="Symbol">:</a> <a id="21961" class="Symbol">∀</a> <a id="21963" class="Symbol">{</a><a id="21964" href="/20.07/Connectives/#21964" class="Bound">A</a> <a id="21966" href="/20.07/Connectives/#21966" class="Bound">B</a> <a id="21968" href="/20.07/Connectives/#21968" class="Bound">C</a> <a id="21970" class="Symbol">:</a> <a id="21972" class="PrimitiveType">Set</a><a id="21975" class="Symbol">}</a> <a id="21977" class="Symbol">→</a> <a id="21979" class="Symbol">(</a><a id="21980" href="/20.07/Connectives/#21964" class="Bound">A</a> <a id="21982" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="21984" href="/20.07/Connectives/#21966" class="Bound">B</a><a id="21985" class="Symbol">)</a> <a id="21987" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="21989" href="/20.07/Connectives/#21968" class="Bound">C</a> <a id="21991" href="/20.07/Isomorphism/#4365" class="Record Operator">≃</a> <a id="21993" class="Symbol">(</a><a id="21994" href="/20.07/Connectives/#21964" class="Bound">A</a> <a id="21996" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="21998" href="/20.07/Connectives/#21968" class="Bound">C</a><a id="21999" class="Symbol">)</a> <a id="22001" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="22003" class="Symbol">(</a><a id="22004" href="/20.07/Connectives/#21966" class="Bound">B</a> <a id="22006" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="22008" href="/20.07/Connectives/#21968" class="Bound">C</a><a id="22009" class="Symbol">)</a>
<a id="22011" href="/20.07/Connectives/#21947" class="Function">×-distrib-⊎</a> <a id="22023" class="Symbol">=</a>
<a id="22027" class="Keyword">record</a>
<a id="22038" class="Symbol">{</a> <a id="22040" href="/20.07/Isomorphism/#4405" class="Field">to</a> <a id="22048" class="Symbol">=</a> <a id="22050" class="Symbol">λ{</a> <a id="22053" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22055" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22060" href="/20.07/Connectives/#22060" class="Bound">x</a> <a id="22062" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22064" href="/20.07/Connectives/#22064" class="Bound">z</a> <a id="22066" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="22068" class="Symbol">→</a> <a id="22070" class="Symbol">(</a><a id="22071" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22076" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22078" href="/20.07/Connectives/#22060" class="Bound">x</a> <a id="22080" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22082" href="/20.07/Connectives/#22064" class="Bound">z</a> <a id="22084" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a><a id="22085" class="Symbol">)</a>
<a id="22104" class="Symbol">;</a> <a id="22106" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22108" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22113" href="/20.07/Connectives/#22113" class="Bound">y</a> <a id="22115" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22117" href="/20.07/Connectives/#22117" class="Bound">z</a> <a id="22119" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="22121" class="Symbol">→</a> <a id="22123" class="Symbol">(</a><a id="22124" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22129" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22131" href="/20.07/Connectives/#22113" class="Bound">y</a> <a id="22133" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22135" href="/20.07/Connectives/#22117" class="Bound">z</a> <a id="22137" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a><a id="22138" class="Symbol">)</a>
<a id="22157" class="Symbol">}</a>
<a id="22163" class="Symbol">;</a> <a id="22165" href="/20.07/Isomorphism/#4422" class="Field">from</a> <a id="22173" class="Symbol">=</a> <a id="22175" class="Symbol">λ{</a> <a id="22178" class="Symbol">(</a><a id="22179" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22184" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22186" href="/20.07/Connectives/#22186" class="Bound">x</a> <a id="22188" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22190" href="/20.07/Connectives/#22190" class="Bound">z</a> <a id="22192" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a><a id="22193" class="Symbol">)</a> <a id="22195" class="Symbol">→</a> <a id="22197" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22199" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22204" href="/20.07/Connectives/#22186" class="Bound">x</a> <a id="22206" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22208" href="/20.07/Connectives/#22190" class="Bound">z</a> <a id="22210" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a>
<a id="22229" class="Symbol">;</a> <a id="22231" class="Symbol">(</a><a id="22232" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22237" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22239" href="/20.07/Connectives/#22239" class="Bound">y</a> <a id="22241" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22243" href="/20.07/Connectives/#22243" class="Bound">z</a> <a id="22245" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a><a id="22246" class="Symbol">)</a> <a id="22248" class="Symbol">→</a> <a id="22250" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22252" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22257" href="/20.07/Connectives/#22239" class="Bound">y</a> <a id="22259" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22261" href="/20.07/Connectives/#22243" class="Bound">z</a> <a id="22263" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a>
<a id="22282" class="Symbol">}</a>
<a id="22288" class="Symbol">;</a> <a id="22290" href="/20.07/Isomorphism/#4439" class="Field">from∘to</a> <a id="22298" class="Symbol">=</a> <a id="22300" class="Symbol">λ{</a> <a id="22303" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22305" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22310" href="/20.07/Connectives/#22310" class="Bound">x</a> <a id="22312" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22314" href="/20.07/Connectives/#22314" class="Bound">z</a> <a id="22316" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="22318" class="Symbol">→</a> <a id="22320" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="22342" class="Symbol">;</a> <a id="22344" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22346" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22351" href="/20.07/Connectives/#22351" class="Bound">y</a> <a id="22353" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22355" href="/20.07/Connectives/#22355" class="Bound">z</a> <a id="22357" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="22359" class="Symbol">→</a> <a id="22361" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="22383" class="Symbol">}</a>
<a id="22389" class="Symbol">;</a> <a id="22391" href="/20.07/Isomorphism/#4481" class="Field">to∘from</a> <a id="22399" class="Symbol">=</a> <a id="22401" class="Symbol">λ{</a> <a id="22404" class="Symbol">(</a><a id="22405" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22410" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22412" href="/20.07/Connectives/#22412" class="Bound">x</a> <a id="22414" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22416" href="/20.07/Connectives/#22416" class="Bound">z</a> <a id="22418" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a><a id="22419" class="Symbol">)</a> <a id="22421" class="Symbol">→</a> <a id="22423" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="22445" class="Symbol">;</a> <a id="22447" class="Symbol">(</a><a id="22448" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22453" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22455" href="/20.07/Connectives/#22455" class="Bound">y</a> <a id="22457" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22459" href="/20.07/Connectives/#22459" class="Bound">z</a> <a id="22461" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a><a id="22462" class="Symbol">)</a> <a id="22464" class="Symbol">→</a> <a id="22466" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="22488" class="Symbol">}</a>
<a id="22494" class="Symbol">}</a>
</pre>
<p>Sums do not distribute over products up to isomorphism, but it is an embedding:</p>
<pre class="Agda"><a id="⊎-distrib-×"></a><a id="22585" href="/20.07/Connectives/#22585" class="Function">⊎-distrib-×</a> <a id="22597" class="Symbol">:</a> <a id="22599" class="Symbol">∀</a> <a id="22601" class="Symbol">{</a><a id="22602" href="/20.07/Connectives/#22602" class="Bound">A</a> <a id="22604" href="/20.07/Connectives/#22604" class="Bound">B</a> <a id="22606" href="/20.07/Connectives/#22606" class="Bound">C</a> <a id="22608" class="Symbol">:</a> <a id="22610" class="PrimitiveType">Set</a><a id="22613" class="Symbol">}</a> <a id="22615" class="Symbol">→</a> <a id="22617" class="Symbol">(</a><a id="22618" href="/20.07/Connectives/#22602" class="Bound">A</a> <a id="22620" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="22622" href="/20.07/Connectives/#22604" class="Bound">B</a><a id="22623" class="Symbol">)</a> <a id="22625" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="22627" href="/20.07/Connectives/#22606" class="Bound">C</a> <a id="22629" href="/20.07/Isomorphism/#9281" class="Record Operator">≲</a> <a id="22631" class="Symbol">(</a><a id="22632" href="/20.07/Connectives/#22602" class="Bound">A</a> <a id="22634" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="22636" href="/20.07/Connectives/#22606" class="Bound">C</a><a id="22637" class="Symbol">)</a> <a id="22639" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="22641" class="Symbol">(</a><a id="22642" href="/20.07/Connectives/#22604" class="Bound">B</a> <a id="22644" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="22646" href="/20.07/Connectives/#22606" class="Bound">C</a><a id="22647" class="Symbol">)</a>
<a id="22649" href="/20.07/Connectives/#22585" class="Function">⊎-distrib-×</a> <a id="22661" class="Symbol">=</a>
<a id="22665" class="Keyword">record</a>
<a id="22676" class="Symbol">{</a> <a id="22678" href="/20.07/Isomorphism/#9321" class="Field">to</a> <a id="22686" class="Symbol">=</a> <a id="22688" class="Symbol">λ{</a> <a id="22691" class="Symbol">(</a><a id="22692" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22697" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22699" href="/20.07/Connectives/#22699" class="Bound">x</a> <a id="22701" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22703" href="/20.07/Connectives/#22703" class="Bound">y</a> <a id="22705" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a><a id="22706" class="Symbol">)</a> <a id="22708" class="Symbol">→</a> <a id="22710" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22712" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22717" href="/20.07/Connectives/#22699" class="Bound">x</a> <a id="22719" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22721" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22726" href="/20.07/Connectives/#22703" class="Bound">y</a> <a id="22728" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a>
<a id="22747" class="Symbol">;</a> <a id="22749" class="Symbol">(</a><a id="22750" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22755" href="/20.07/Connectives/#22755" class="Bound">z</a><a id="22756" class="Symbol">)</a> <a id="22766" class="Symbol">→</a> <a id="22768" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22770" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22775" href="/20.07/Connectives/#22755" class="Bound">z</a> <a id="22777" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22779" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22784" href="/20.07/Connectives/#22755" class="Bound">z</a> <a id="22786" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a>
<a id="22805" class="Symbol">}</a>
<a id="22811" class="Symbol">;</a> <a id="22813" href="/20.07/Isomorphism/#9341" class="Field">from</a> <a id="22821" class="Symbol">=</a> <a id="22823" class="Symbol">λ{</a> <a id="22826" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22828" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22833" href="/20.07/Connectives/#22833" class="Bound">x</a> <a id="22835" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22837" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22842" href="/20.07/Connectives/#22842" class="Bound">y</a> <a id="22844" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="22846" class="Symbol">→</a> <a id="22848" class="Symbol">(</a><a id="22849" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22854" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22856" href="/20.07/Connectives/#22833" class="Bound">x</a> <a id="22858" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22860" href="/20.07/Connectives/#22842" class="Bound">y</a> <a id="22862" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a><a id="22863" class="Symbol">)</a>
<a id="22882" class="Symbol">;</a> <a id="22884" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22886" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="22891" href="/20.07/Connectives/#22891" class="Bound">x</a> <a id="22893" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22895" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22900" href="/20.07/Connectives/#22900" class="Bound">z</a> <a id="22902" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="22904" class="Symbol">→</a> <a id="22906" class="Symbol">(</a><a id="22907" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22912" href="/20.07/Connectives/#22900" class="Bound">z</a><a id="22913" class="Symbol">)</a>
<a id="22932" class="Symbol">;</a> <a id="22934" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="22936" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22941" href="/20.07/Connectives/#22941" class="Bound">z</a> <a id="22943" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="22945" class="Symbol">_</a> <a id="22952" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a> <a id="22954" class="Symbol">→</a> <a id="22956" class="Symbol">(</a><a id="22957" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="22962" href="/20.07/Connectives/#22941" class="Bound">z</a><a id="22963" class="Symbol">)</a>
<a id="22982" class="Symbol">}</a>
<a id="22988" class="Symbol">;</a> <a id="22990" href="/20.07/Isomorphism/#9361" class="Field">from∘to</a> <a id="22998" class="Symbol">=</a> <a id="23000" class="Symbol">λ{</a> <a id="23003" class="Symbol">(</a><a id="23004" href="/20.07/Connectives/#11301" class="InductiveConstructor">inj₁</a> <a id="23009" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟨</a> <a id="23011" href="/20.07/Connectives/#23011" class="Bound">x</a> <a id="23013" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">,</a> <a id="23015" href="/20.07/Connectives/#23015" class="Bound">y</a> <a id="23017" href="/20.07/Connectives/#1323" class="InductiveConstructor Operator">⟩</a><a id="23018" class="Symbol">)</a> <a id="23020" class="Symbol">→</a> <a id="23022" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="23044" class="Symbol">;</a> <a id="23046" class="Symbol">(</a><a id="23047" href="/20.07/Connectives/#11343" class="InductiveConstructor">inj₂</a> <a id="23052" href="/20.07/Connectives/#23052" class="Bound">z</a><a id="23053" class="Symbol">)</a> <a id="23063" class="Symbol">→</a> <a id="23065" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="23087" class="Symbol">}</a>
<a id="23093" class="Symbol">}</a>
</pre>
<p>Note that there is a choice in how we write the <code class="language-plaintext highlighter-rouge">from</code> function.
As given, it takes <code class="language-plaintext highlighter-rouge">⟨ inj₂ z , inj₂ z′ ⟩</code> to <code class="language-plaintext highlighter-rouge">inj₂ z</code>, but it is
easy to write a variant that instead returns <code class="language-plaintext highlighter-rouge">inj₂ z′</code>. We have
an embedding rather than an isomorphism because the
<code class="language-plaintext highlighter-rouge">from</code> function must discard either <code class="language-plaintext highlighter-rouge">z</code> or <code class="language-plaintext highlighter-rouge">z′</code> in this case.</p>
<p>In the usual approach to logic, both of the distribution laws
are given as equivalences, where each side implies the other:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>A × (B ⊎ C) ⇔ (A × B) ⊎ (A × C)
A ⊎ (B × C) ⇔ (A ⊎ B) × (A ⊎ C)
</code></pre></div></div>
<p>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.</p>
<h4 id="exercise--weak--recommended">Exercise <code class="language-plaintext highlighter-rouge">⊎-weak-×</code> (recommended)</h4>
<p>Show that the following property holds:</p>
<pre class="Agda"><a id="23946" class="Keyword">postulate</a>
<a id="⊎-weak-×"></a><a id="23958" href="/20.07/Connectives/#23958" class="Postulate">⊎-weak-×</a> <a id="23967" class="Symbol">:</a> <a id="23969" class="Symbol">∀</a> <a id="23971" class="Symbol">{</a><a id="23972" href="/20.07/Connectives/#23972" class="Bound">A</a> <a id="23974" href="/20.07/Connectives/#23974" class="Bound">B</a> <a id="23976" href="/20.07/Connectives/#23976" class="Bound">C</a> <a id="23978" class="Symbol">:</a> <a id="23980" class="PrimitiveType">Set</a><a id="23983" class="Symbol">}</a> <a id="23985" class="Symbol">→</a> <a id="23987" class="Symbol">(</a><a id="23988" href="/20.07/Connectives/#23972" class="Bound">A</a> <a id="23990" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="23992" href="/20.07/Connectives/#23974" class="Bound">B</a><a id="23993" class="Symbol">)</a> <a id="23995" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="23997" href="/20.07/Connectives/#23976" class="Bound">C</a> <a id="23999" class="Symbol">→</a> <a id="24001" href="/20.07/Connectives/#23972" class="Bound">A</a> <a id="24003" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="24005" class="Symbol">(</a><a id="24006" href="/20.07/Connectives/#23974" class="Bound">B</a> <a id="24008" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="24010" href="/20.07/Connectives/#23976" class="Bound">C</a><a id="24011" class="Symbol">)</a>
</pre>
<p>This is called a <em>weak distributive law</em>. Give the corresponding
distributive law, and explain how it relates to the weak version.</p>
<pre class="Agda"><a id="24153" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise--implies--practice">Exercise <code class="language-plaintext highlighter-rouge">⊎×-implies-×⊎</code> (practice)</h4>
<p>Show that a disjunct of conjuncts implies a conjunct of disjuncts:</p>
<pre class="Agda"><a id="24295" class="Keyword">postulate</a>
<a id="⊎×-implies-×⊎"></a><a id="24307" href="/20.07/Connectives/#24307" class="Postulate">⊎×-implies-×⊎</a> <a id="24321" class="Symbol">:</a> <a id="24323" class="Symbol">∀</a> <a id="24325" class="Symbol">{</a><a id="24326" href="/20.07/Connectives/#24326" class="Bound">A</a> <a id="24328" href="/20.07/Connectives/#24328" class="Bound">B</a> <a id="24330" href="/20.07/Connectives/#24330" class="Bound">C</a> <a id="24332" href="/20.07/Connectives/#24332" class="Bound">D</a> <a id="24334" class="Symbol">:</a> <a id="24336" class="PrimitiveType">Set</a><a id="24339" class="Symbol">}</a> <a id="24341" class="Symbol">→</a> <a id="24343" class="Symbol">(</a><a id="24344" href="/20.07/Connectives/#24326" class="Bound">A</a> <a id="24346" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="24348" href="/20.07/Connectives/#24328" class="Bound">B</a><a id="24349" class="Symbol">)</a> <a id="24351" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="24353" class="Symbol">(</a><a id="24354" href="/20.07/Connectives/#24330" class="Bound">C</a> <a id="24356" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="24358" href="/20.07/Connectives/#24332" class="Bound">D</a><a id="24359" class="Symbol">)</a> <a id="24361" class="Symbol">→</a> <a id="24363" class="Symbol">(</a><a id="24364" href="/20.07/Connectives/#24326" class="Bound">A</a> <a id="24366" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="24368" href="/20.07/Connectives/#24330" class="Bound">C</a><a id="24369" class="Symbol">)</a> <a id="24371" href="/20.07/Connectives/#1292" class="Datatype Operator">×</a> <a id="24373" class="Symbol">(</a><a id="24374" href="/20.07/Connectives/#24328" class="Bound">B</a> <a id="24376" href="/20.07/Connectives/#11270" class="Datatype Operator">⊎</a> <a id="24378" href="/20.07/Connectives/#24332" class="Bound">D</a><a id="24379" class="Symbol">)</a>
</pre>
<p>Does the converse hold? If so, prove; if not, give a counterexample.</p>
<pre class="Agda"><a id="24459" class="Comment">-- Your code goes here</a>
</pre>
<h2 id="standard-library">Standard library</h2>
<p>Definitions similar to those in this chapter can be found in the standard library:</p>
<pre class="Agda"><a id="24596" class="Keyword">import</a> <a id="24603" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html" class="Module">Data.Product</a> <a id="24616" class="Keyword">using</a> <a id="24622" class="Symbol">(</a><a id="24623" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">_×_</a><a id="24626" class="Symbol">;</a> <a id="24628" href="Agda.Builtin.Sigma.html#225" class="Field">proj₁</a><a id="24633" class="Symbol">;</a> <a id="24635" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a><a id="24640" class="Symbol">)</a> <a id="24642" class="Keyword">renaming</a> <a id="24651" class="Symbol">(</a><a id="24652" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">_,_</a> <a id="24656" class="Symbol">to</a> <a id="24659" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨_,_⟩</a><a id="24664" class="Symbol">)</a>
<a id="24666" class="Keyword">import</a> <a id="24673" href="https://agda.github.io/agda-stdlib/v1.1/Data.Unit.html" class="Module">Data.Unit</a> <a id="24683" class="Keyword">using</a> <a id="24689" class="Symbol">(</a><a id="24690" href="Agda.Builtin.Unit.html#137" class="Record">⊤</a><a id="24691" class="Symbol">;</a> <a id="24693" href="Agda.Builtin.Unit.html#174" class="InductiveConstructor">tt</a><a id="24695" class="Symbol">)</a>
<a id="24697" class="Keyword">import</a> <a id="24704" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.html" class="Module">Data.Sum</a> <a id="24713" class="Keyword">using</a> <a id="24719" class="Symbol">(</a><a id="24720" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#612" class="Datatype Operator">_⊎_</a><a id="24723" class="Symbol">;</a> <a id="24725" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a><a id="24729" class="Symbol">;</a> <a id="24731" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a><a id="24735" class="Symbol">)</a> <a id="24737" class="Keyword">renaming</a> <a id="24746" class="Symbol">(</a><a id="24747" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#798" class="Function Operator">[_,_]</a> <a id="24753" class="Symbol">to</a> <a id="24756" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#798" class="Function Operator">case-⊎</a><a id="24762" class="Symbol">)</a>
<a id="24764" class="Keyword">import</a> <a id="24771" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html" class="Module">Data.Empty</a> <a id="24782" class="Keyword">using</a> <a id="24788" class="Symbol">(</a><a id="24789" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a><a id="24790" class="Symbol">;</a> <a id="24792" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a><a id="24798" class="Symbol">)</a>
<a id="24800" class="Keyword">import</a> <a id="24807" href="https://agda.github.io/agda-stdlib/v1.1/Function.Equivalence.html" class="Module">Function.Equivalence</a> <a id="24828" class="Keyword">using</a> <a id="24834" class="Symbol">(</a><a id="24835" href="https://agda.github.io/agda-stdlib/v1.1/Function.Equivalence.html#971" class="Function Operator">_⇔_</a><a id="24838" class="Symbol">)</a>
</pre>
<p>The standard library constructs pairs with <code class="language-plaintext highlighter-rouge">_,_</code> whereas we use <code class="language-plaintext highlighter-rouge">⟨_,_⟩</code>.
The former makes it convenient to build triples or larger tuples from pairs,
permitting <code class="language-plaintext highlighter-rouge">a , b , c</code> to stand for <code class="language-plaintext highlighter-rouge">(a , (b , c))</code>. But it conflicts with
other useful notations, such as <code class="language-plaintext highlighter-rouge">[_,_]</code> to construct a list of two elements in
Chapter <a href="/20.07/Lists/">Lists</a>
and <code class="language-plaintext highlighter-rouge">Γ , A</code> to extend environments in
Chapter <a href="/20.07/DeBruijn/">DeBruijn</a>.
The standard library <code class="language-plaintext highlighter-rouge">_⇔_</code> 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.</p>
<h2 id="unicode">Unicode</h2>
<p>This chapter uses the following unicode:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>× 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 (\&lt;=&gt;)
</code></pre></div></div>
<div class="footnotes" role="doc-endnotes">
<ol>
<li id="fn:from-wadler-2015" role="doc-endnote">
<p>This paragraph was adopted from “Propositions as Types”, Philip Wadler, <em>Communications of the ACM</em>, December 2015. <a href="#fnref:from-wadler-2015" class="reversefootnote" role="doc-backlink">&#8617;</a></p>
</li>
</ol>
</div>
</div>
<p style="text-align:center;">
<a alt="Previous chapter" href="/20.07/Isomorphism/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part1/Connectives.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/20.07/Negation/">Next</a>
</p>
</article>
</div>
</main><footer class="site-footer h-card">
<data class="u-url" href="/20.07/"></data>
<div class="wrapper">
<h2 class="footer-heading">Programming Language Foundations in Agda
</h2><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Philip Wadler</li>
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Wen Kokke</li>
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Jeremy G. Siek</li>
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
</div>
</footer>
<!-- Import jQuery -->
<script type="text/javascript" src="/20.07/assets/jquery.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
<script type="text/javascript">
anchors.add();
</script>
<script type="text/javascript">
// Makes sandwhich menu works
$('.menu-icon').click(function(){
$('.trigger').toggle();
});
// Script which allows for foldable code blocks
$('div.foldable pre').each(function(){
var autoHeight = $(this).height();
var lineHeight = parseFloat($(this).css('line-height'));
var plus = $("<div></div>");
var horLine = $("<div></div>");
var verLine = $("<div></div>");
$(this).prepend(plus);
plus.css({
'position' : 'relative',
'float' : 'right',
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'width' : lineHeight,
'height' : lineHeight});
verLine.css({
'position' : 'relative',
'height' : lineHeight,
'width' : '3px',
'background-color' : '#C1E0FF'});
horLine.css({
'position' : 'relative',
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'height' : '3px',
'width' : lineHeight,
'background-color' : '#C1E0FF'});
plus.append(verLine);
plus.append(horLine);
$(this).height(2.0 * lineHeight);
$(this).css('overflow','hidden');
$(this).click(function(){
if ($(this).height() == autoHeight) {
$(this).height(2.0 * lineHeight);
plus.show();
}
else {
$(this).height('auto');
plus.hide();
}
});
});
</script>
<!-- Import KaTeX -->
<script type="text/javascript" src="/20.07/assets/katex.js"></script>
<!-- Script which renders TeX using KaTeX -->
<script type="text/javascript">
$("script[type='math/tex']").replaceWith(
function(){
var tex = $(this).text();
return "<span class=\"inline-equation\">" +
katex.renderToString(tex) +
"</span>";
});
$("script[type='math/tex; mode=display']").replaceWith(
function(){
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
return "<div class=\"equation\">" +
katex.renderToString("\\displaystyle "+tex) +
"</div>";
});
</script>
</body>
</html>
Reference in a new issue View git blame Copy permalink