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

703 lines
107 KiB
HTML
Raw Permalink Blame History

This file contains ambiguous Unicode characters

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>Isomorphism: Isomorphism and Embedding | 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="Isomorphism: Isomorphism and Embedding" />
<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/19.08/Isomorphism/" />
<meta property="og:url" content="https://plfa.github.io/19.08/Isomorphism/" />
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
<script type="application/ld+json">
{"url":"https://plfa.github.io/19.08/Isomorphism/","headline":"Isomorphism: Isomorphism and Embedding","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
<!-- End Jekyll SEO tag -->
<link rel="stylesheet" href="/19.08/assets/main.css"></head>
<body><header class="site-header" role="banner">
<div class="wrapper">
<a class="site-title" href="/19.08/">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="/19.08/">The Book</a>
<a class="page-link" href="/19.08/Announcements/">Announcements</a>
<a class="page-link" href="/19.08/GettingStarted/">Getting Started</a>
<a class="page-link" href="/19.08/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">Isomorphism: Isomorphism and Embedding</h1>
</header>
<p style="text-align:center;">
<a alt="Previous chapter" href="/19.08/Equality/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part1/Isomorphism.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/19.08/Connectives/">Next</a>
</p>
<div class="post-content">
<pre class="Agda"><a id="159" class="Keyword">module</a> <a id="166" href="/19.08/Isomorphism/" class="Module">plfa.part1.Isomorphism</a> <a id="189" class="Keyword">where</a>
</pre>
<p>This section introduces isomorphism as a way of asserting that two
types are equal, and embedding as a way of asserting that one type is
smaller than another. We apply isomorphisms in the next chapter
to demonstrate that operations on types such as product and sum
satisfy properties akin to associativity, commutativity, and
distributivity.</p>
<h2 id="imports">Imports</h2>
<pre class="Agda"><a id="560" class="Keyword">import</a> <a id="567" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="605" class="Symbol">as</a> <a id="608" class="Module">Eq</a>
<a id="611" class="Keyword">open</a> <a id="616" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Eq</a> <a id="619" class="Keyword">using</a> <a id="625" class="Symbol">(</a><a id="626" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="629" class="Symbol">;</a> <a id="631" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="635" class="Symbol">;</a> <a id="637" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a><a id="641" class="Symbol">;</a> <a id="643" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html#1308" class="Function">cong-app</a><a id="651" class="Symbol">)</a>
<a id="653" class="Keyword">open</a> <a id="658" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2499" class="Module">Eq.≡-Reasoning</a>
<a id="673" class="Keyword">open</a> <a id="678" class="Keyword">import</a> <a id="685" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="694" class="Keyword">using</a> <a id="700" class="Symbol">(</a><a id="701" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="702" class="Symbol">;</a> <a id="704" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="708" class="Symbol">;</a> <a id="710" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a><a id="713" class="Symbol">;</a> <a id="715" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a><a id="718" class="Symbol">)</a>
<a id="720" class="Keyword">open</a> <a id="725" class="Keyword">import</a> <a id="732" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="752" class="Keyword">using</a> <a id="758" class="Symbol">(</a><a id="759" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911" class="Function">+-comm</a><a id="765" class="Symbol">)</a>
</pre>
<h2 id="lambda-expressions">Lambda expressions</h2>
<p>The chapter begins with a few preliminaries that will be useful
here and elsewhere: lambda expressions, function composition, and
extensionality.</p>
<p><em>Lambda expressions</em> provide a compact way to define functions without
naming them. A term of the form</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>λ{ P₁ → N₁; ⋯ ; Pₙ → Nₙ }
</code></pre></div></div>
<p>is equivalent to a function <code class="language-plaintext highlighter-rouge">f</code> defined by the equations</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>f P₁ = N₁
⋯
f Pₙ = Nₙ
</code></pre></div></div>
<p>where the <code class="language-plaintext highlighter-rouge">Pₙ</code> are patterns (left-hand sides of an equation) and the
<code class="language-plaintext highlighter-rouge">Nₙ</code> are expressions (right-hand side of an equation).</p>
<p>In the case that there is one equation and the pattern is a variable,
we may also use the syntax</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>λ x → N
</code></pre></div></div>
<p>or</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>λ (x : A) → N
</code></pre></div></div>
<p>both of which are equivalent to <code class="language-plaintext highlighter-rouge">λ{x → N}</code>. The latter allows one to
specify the domain of the function.</p>
<p>Often using an anonymous lambda expression is more convenient than
using a named function: it avoids a lengthy type declaration; and the
definition appears exactly where the function is used, so there is no
need for the writer to remember to declare it in advance, or for the
reader to search for the definition in the code.</p>
<h2 id="function-composition">Function composition</h2>
<p>In what follows, we will make use of function composition:</p>
<pre class="Agda"><a id="_∘_"></a><a id="1952" href="/19.08/Isomorphism/#1952" class="Function Operator">_∘_</a> <a id="1956" class="Symbol">:</a> <a id="1958" class="Symbol">∀</a> <a id="1960" class="Symbol">{</a><a id="1961" href="plfa.part1.Isomorphism.html#1961" class="Bound">A</a> <a id="1963" href="plfa.part1.Isomorphism.html#1963" class="Bound">B</a> <a id="1965" href="plfa.part1.Isomorphism.html#1965" class="Bound">C</a> <a id="1967" class="Symbol">:</a> <a id="1969" class="PrimitiveType">Set</a><a id="1972" class="Symbol">}</a> <a id="1974" class="Symbol">→</a> <a id="1976" class="Symbol">(</a><a id="1977" href="plfa.part1.Isomorphism.html#1963" class="Bound">B</a> <a id="1979" class="Symbol">→</a> <a id="1981" href="plfa.part1.Isomorphism.html#1965" class="Bound">C</a><a id="1982" class="Symbol">)</a> <a id="1984" class="Symbol">→</a> <a id="1986" class="Symbol">(</a><a id="1987" href="plfa.part1.Isomorphism.html#1961" class="Bound">A</a> <a id="1989" class="Symbol">→</a> <a id="1991" href="plfa.part1.Isomorphism.html#1963" class="Bound">B</a><a id="1992" class="Symbol">)</a> <a id="1994" class="Symbol">→</a> <a id="1996" class="Symbol">(</a><a id="1997" href="plfa.part1.Isomorphism.html#1961" class="Bound">A</a> <a id="1999" class="Symbol">→</a> <a id="2001" href="plfa.part1.Isomorphism.html#1965" class="Bound">C</a><a id="2002" class="Symbol">)</a>
<a id="2004" class="Symbol">(</a><a id="2005" href="/19.08/Isomorphism/#2005" class="Bound">g</a> <a id="2007" href="plfa.part1.Isomorphism.html#1952" class="Function Operator">∘</a> <a id="2009" href="plfa.part1.Isomorphism.html#2009" class="Bound">f</a><a id="2010" class="Symbol">)</a> <a id="2012" href="plfa.part1.Isomorphism.html#2012" class="Bound">x</a> <a id="2015" class="Symbol">=</a> <a id="2017" href="plfa.part1.Isomorphism.html#2005" class="Bound">g</a> <a id="2019" class="Symbol">(</a><a id="2020" href="plfa.part1.Isomorphism.html#2009" class="Bound">f</a> <a id="2022" href="plfa.part1.Isomorphism.html#2012" class="Bound">x</a><a id="2023" class="Symbol">)</a>
</pre>
<p>Thus, <code class="language-plaintext highlighter-rouge">g ∘ f</code> is the function that first applies <code class="language-plaintext highlighter-rouge">f</code> and
then applies <code class="language-plaintext highlighter-rouge">g</code>. An equivalent definition, exploiting lambda
expressions, is as follows:</p>
<pre class="Agda"><a id="_∘′_"></a><a id="2181" href="/19.08/Isomorphism/#2181" class="Function Operator">_∘′_</a> <a id="2186" class="Symbol">:</a> <a id="2188" class="Symbol">∀</a> <a id="2190" class="Symbol">{</a><a id="2191" href="plfa.part1.Isomorphism.html#2191" class="Bound">A</a> <a id="2193" href="plfa.part1.Isomorphism.html#2193" class="Bound">B</a> <a id="2195" href="plfa.part1.Isomorphism.html#2195" class="Bound">C</a> <a id="2197" class="Symbol">:</a> <a id="2199" class="PrimitiveType">Set</a><a id="2202" class="Symbol">}</a> <a id="2204" class="Symbol">→</a> <a id="2206" class="Symbol">(</a><a id="2207" href="plfa.part1.Isomorphism.html#2193" class="Bound">B</a> <a id="2209" class="Symbol">→</a> <a id="2211" href="plfa.part1.Isomorphism.html#2195" class="Bound">C</a><a id="2212" class="Symbol">)</a> <a id="2214" class="Symbol">→</a> <a id="2216" class="Symbol">(</a><a id="2217" href="plfa.part1.Isomorphism.html#2191" class="Bound">A</a> <a id="2219" class="Symbol">→</a> <a id="2221" href="plfa.part1.Isomorphism.html#2193" class="Bound">B</a><a id="2222" class="Symbol">)</a> <a id="2224" class="Symbol">→</a> <a id="2226" class="Symbol">(</a><a id="2227" href="plfa.part1.Isomorphism.html#2191" class="Bound">A</a> <a id="2229" class="Symbol">→</a> <a id="2231" href="plfa.part1.Isomorphism.html#2195" class="Bound">C</a><a id="2232" class="Symbol">)</a>
<a id="2234" href="/19.08/Isomorphism/#2234" class="Bound">g</a> <a id="2236" href="plfa.part1.Isomorphism.html#2181" class="Function Operator">∘′</a> <a id="2239" href="plfa.part1.Isomorphism.html#2239" class="Bound">f</a> <a id="2242" class="Symbol">=</a> <a id="2245" class="Symbol">λ</a> <a id="2247" href="plfa.part1.Isomorphism.html#2247" class="Bound">x</a> <a id="2249" class="Symbol">→</a> <a id="2251" href="plfa.part1.Isomorphism.html#2234" class="Bound">g</a> <a id="2253" class="Symbol">(</a><a id="2254" href="plfa.part1.Isomorphism.html#2239" class="Bound">f</a> <a id="2256" href="plfa.part1.Isomorphism.html#2247" class="Bound">x</a><a id="2257" class="Symbol">)</a>
</pre>
<h2 id="extensionality">Extensionality</h2>
<p>Extensionality asserts that the only way to distinguish functions is
by applying them; if two functions applied to the same argument always
yield the same result, then they are the same function. It is the
converse of <code class="language-plaintext highlighter-rouge">cong-app</code>, as introduced
<a href="/19.08/Equality/#cong">earlier</a>.</p>
<p>Agda does not presume extensionality, but we can postulate that it holds:</p>
<pre class="Agda"><a id="2672" class="Keyword">postulate</a>
<a id="extensionality"></a><a id="2684" href="/19.08/Isomorphism/#2684" class="Postulate">extensionality</a> <a id="2699" class="Symbol">:</a> <a id="2701" class="Symbol">∀</a> <a id="2703" class="Symbol">{</a><a id="2704" href="plfa.part1.Isomorphism.html#2704" class="Bound">A</a> <a id="2706" href="plfa.part1.Isomorphism.html#2706" class="Bound">B</a> <a id="2708" class="Symbol">:</a> <a id="2710" class="PrimitiveType">Set</a><a id="2713" class="Symbol">}</a> <a id="2715" class="Symbol">{</a><a id="2716" href="plfa.part1.Isomorphism.html#2716" class="Bound">f</a> <a id="2718" href="plfa.part1.Isomorphism.html#2718" class="Bound">g</a> <a id="2720" class="Symbol">:</a> <a id="2722" href="plfa.part1.Isomorphism.html#2704" class="Bound">A</a> <a id="2724" class="Symbol">→</a> <a id="2726" href="plfa.part1.Isomorphism.html#2706" class="Bound">B</a><a id="2727" class="Symbol">}</a>
<a id="2733" class="Symbol">→</a> <a id="2735" class="Symbol">(∀</a> <a id="2738" class="Symbol">(</a><a id="2739" href="/19.08/Isomorphism/#2739" class="Bound">x</a> <a id="2741" class="Symbol">:</a> <a id="2743" href="plfa.part1.Isomorphism.html#2704" class="Bound">A</a><a id="2744" class="Symbol">)</a> <a id="2746" class="Symbol">→</a> <a id="2748" href="plfa.part1.Isomorphism.html#2716" class="Bound">f</a> <a id="2750" href="plfa.part1.Isomorphism.html#2739" class="Bound">x</a> <a id="2752" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="2754" href="plfa.part1.Isomorphism.html#2718" class="Bound">g</a> <a id="2756" href="plfa.part1.Isomorphism.html#2739" class="Bound">x</a><a id="2757" class="Symbol">)</a>
<a id="2765" class="Comment">-----------------------</a>
<a id="2793" class="Symbol">→</a> <a id="2795" href="/19.08/Isomorphism/#2716" class="Bound">f</a> <a id="2797" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="2799" href="plfa.part1.Isomorphism.html#2718" class="Bound">g</a>
</pre>
<p>Postulating extensionality does not lead to difficulties, as it is
known to be consistent with the theory that underlies Agda.</p>
<p>As an example, consider that we need results from two libraries,
one where addition is defined, as in
Chapter <a href="/19.08/Naturals/">Naturals</a>,
and one where it is defined the other way around.</p>
<pre class="Agda"><a id="_+′_"></a><a id="3139" href="/19.08/Isomorphism/#3139" class="Function Operator">_+′_</a> <a id="3144" class="Symbol">:</a> <a id="3146" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="3148" class="Symbol">→</a> <a id="3150" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="3152" class="Symbol">→</a> <a id="3154" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="3156" href="/19.08/Isomorphism/#3156" class="Bound">m</a> <a id="3158" href="plfa.part1.Isomorphism.html#3139" class="Function Operator">+′</a> <a id="3161" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="3167" class="Symbol">=</a> <a id="3169" href="plfa.part1.Isomorphism.html#3156" class="Bound">m</a>
<a id="3171" href="/19.08/Isomorphism/#3171" class="Bound">m</a> <a id="3173" href="plfa.part1.Isomorphism.html#3139" class="Function Operator">+′</a> <a id="3176" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="3180" href="plfa.part1.Isomorphism.html#3180" class="Bound">n</a> <a id="3182" class="Symbol">=</a> <a id="3184" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="3188" class="Symbol">(</a><a id="3189" href="plfa.part1.Isomorphism.html#3171" class="Bound">m</a> <a id="3191" href="plfa.part1.Isomorphism.html#3139" class="Function Operator">+′</a> <a id="3194" href="plfa.part1.Isomorphism.html#3180" class="Bound">n</a><a id="3195" class="Symbol">)</a>
</pre>
<p>Applying commutativity, it is easy to show that both operators always
return the same result given the same arguments:</p>
<pre class="Agda"><a id="same-app"></a><a id="3324" href="/19.08/Isomorphism/#3324" class="Function">same-app</a> <a id="3333" class="Symbol">:</a> <a id="3335" class="Symbol">∀</a> <a id="3337" class="Symbol">(</a><a id="3338" href="plfa.part1.Isomorphism.html#3338" class="Bound">m</a> <a id="3340" href="plfa.part1.Isomorphism.html#3340" class="Bound">n</a> <a id="3342" class="Symbol">:</a> <a id="3344" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="3345" class="Symbol">)</a> <a id="3347" class="Symbol">→</a> <a id="3349" href="plfa.part1.Isomorphism.html#3338" class="Bound">m</a> <a id="3351" href="plfa.part1.Isomorphism.html#3139" class="Function Operator">+′</a> <a id="3354" href="plfa.part1.Isomorphism.html#3340" class="Bound">n</a> <a id="3356" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="3358" href="plfa.part1.Isomorphism.html#3338" class="Bound">m</a> <a id="3360" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3362" href="plfa.part1.Isomorphism.html#3340" class="Bound">n</a>
<a id="3364" href="/19.08/Isomorphism/#3324" class="Function">same-app</a> <a id="3373" href="plfa.part1.Isomorphism.html#3373" class="Bound">m</a> <a id="3375" href="plfa.part1.Isomorphism.html#3375" class="Bound">n</a> <a id="3377" class="Keyword">rewrite</a> <a id="3385" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911" class="Function">+-comm</a> <a id="3392" href="plfa.part1.Isomorphism.html#3373" class="Bound">m</a> <a id="3394" href="plfa.part1.Isomorphism.html#3375" class="Bound">n</a> <a id="3396" class="Symbol">=</a> <a id="3398" href="plfa.part1.Isomorphism.html#3419" class="Function">helper</a> <a id="3405" href="plfa.part1.Isomorphism.html#3373" class="Bound">m</a> <a id="3407" href="plfa.part1.Isomorphism.html#3375" class="Bound">n</a>
<a id="3411" class="Keyword">where</a>
<a id="3419" href="/19.08/Isomorphism/#3419" class="Function">helper</a> <a id="3426" class="Symbol">:</a> <a id="3428" class="Symbol">∀</a> <a id="3430" class="Symbol">(</a><a id="3431" href="plfa.part1.Isomorphism.html#3431" class="Bound">m</a> <a id="3433" href="plfa.part1.Isomorphism.html#3433" class="Bound">n</a> <a id="3435" class="Symbol">:</a> <a id="3437" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="3438" class="Symbol">)</a> <a id="3440" class="Symbol">→</a> <a id="3442" href="plfa.part1.Isomorphism.html#3431" class="Bound">m</a> <a id="3444" href="plfa.part1.Isomorphism.html#3139" class="Function Operator">+′</a> <a id="3447" href="plfa.part1.Isomorphism.html#3433" class="Bound">n</a> <a id="3449" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="3451" href="plfa.part1.Isomorphism.html#3433" class="Bound">n</a> <a id="3453" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3455" href="plfa.part1.Isomorphism.html#3431" class="Bound">m</a>
<a id="3459" href="/19.08/Isomorphism/#3419" class="Function">helper</a> <a id="3466" href="plfa.part1.Isomorphism.html#3466" class="Bound">m</a> <a id="3468" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="3476" class="Symbol">=</a> <a id="3478" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="3485" href="/19.08/Isomorphism/#3419" class="Function">helper</a> <a id="3492" href="plfa.part1.Isomorphism.html#3492" class="Bound">m</a> <a id="3494" class="Symbol">(</a><a id="3495" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="3499" href="plfa.part1.Isomorphism.html#3499" class="Bound">n</a><a id="3500" class="Symbol">)</a> <a id="3502" class="Symbol">=</a> <a id="3504" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="3509" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="3513" class="Symbol">(</a><a id="3514" href="plfa.part1.Isomorphism.html#3419" class="Function">helper</a> <a id="3521" href="plfa.part1.Isomorphism.html#3492" class="Bound">m</a> <a id="3523" href="plfa.part1.Isomorphism.html#3499" class="Bound">n</a><a id="3524" class="Symbol">)</a>
</pre>
<p>However, it might be convenient to assert that the two operators are
actually indistinguishable. This we can do via two applications of
extensionality:</p>
<pre class="Agda"><a id="same"></a><a id="3686" href="/19.08/Isomorphism/#3686" class="Function">same</a> <a id="3691" class="Symbol">:</a> <a id="3693" href="plfa.part1.Isomorphism.html#3139" class="Function Operator">_+′_</a> <a id="3698" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="3700" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a>
<a id="3704" href="/19.08/Isomorphism/#3686" class="Function">same</a> <a id="3709" class="Symbol">=</a> <a id="3711" href="plfa.part1.Isomorphism.html#2684" class="Postulate">extensionality</a> <a id="3726" class="Symbol">(λ</a> <a id="3729" href="plfa.part1.Isomorphism.html#3729" class="Bound">m</a> <a id="3731" class="Symbol">→</a> <a id="3733" href="plfa.part1.Isomorphism.html#2684" class="Postulate">extensionality</a> <a id="3748" class="Symbol">(λ</a> <a id="3751" href="plfa.part1.Isomorphism.html#3751" class="Bound">n</a> <a id="3753" class="Symbol">→</a> <a id="3755" href="plfa.part1.Isomorphism.html#3324" class="Function">same-app</a> <a id="3764" href="plfa.part1.Isomorphism.html#3729" class="Bound">m</a> <a id="3766" href="plfa.part1.Isomorphism.html#3751" class="Bound">n</a><a id="3767" class="Symbol">))</a>
</pre>
<p>We occasionally need to postulate extensionality in what follows.</p>
<p>More generally, we may wish to postulate extensionality for
dependent functions.</p>
<pre class="Agda"><a id="3926" class="Keyword">postulate</a>
<a id="∀-extensionality"></a><a id="3938" href="/19.08/Isomorphism/#3938" class="Postulate">∀-extensionality</a> <a id="3955" class="Symbol">:</a> <a id="3957" class="Symbol">∀</a> <a id="3959" class="Symbol">{</a><a id="3960" href="plfa.part1.Isomorphism.html#3960" class="Bound">A</a> <a id="3962" class="Symbol">:</a> <a id="3964" class="PrimitiveType">Set</a><a id="3967" class="Symbol">}</a> <a id="3969" class="Symbol">{</a><a id="3970" href="plfa.part1.Isomorphism.html#3970" class="Bound">B</a> <a id="3972" class="Symbol">:</a> <a id="3974" href="plfa.part1.Isomorphism.html#3960" class="Bound">A</a> <a id="3976" class="Symbol">→</a> <a id="3978" class="PrimitiveType">Set</a><a id="3981" class="Symbol">}</a> <a id="3983" class="Symbol">{</a><a id="3984" href="plfa.part1.Isomorphism.html#3984" class="Bound">f</a> <a id="3986" href="plfa.part1.Isomorphism.html#3986" class="Bound">g</a> <a id="3988" class="Symbol">:</a> <a id="3990" class="Symbol">∀(</a><a id="3992" href="plfa.part1.Isomorphism.html#3992" class="Bound">x</a> <a id="3994" class="Symbol">:</a> <a id="3996" href="plfa.part1.Isomorphism.html#3960" class="Bound">A</a><a id="3997" class="Symbol">)</a> <a id="3999" class="Symbol">→</a> <a id="4001" href="plfa.part1.Isomorphism.html#3970" class="Bound">B</a> <a id="4003" href="plfa.part1.Isomorphism.html#3992" class="Bound">x</a><a id="4004" class="Symbol">}</a>
<a id="4010" class="Symbol">→</a> <a id="4012" class="Symbol">(∀</a> <a id="4015" class="Symbol">(</a><a id="4016" href="/19.08/Isomorphism/#4016" class="Bound">x</a> <a id="4018" class="Symbol">:</a> <a id="4020" href="plfa.part1.Isomorphism.html#3960" class="Bound">A</a><a id="4021" class="Symbol">)</a> <a id="4023" class="Symbol">→</a> <a id="4025" href="plfa.part1.Isomorphism.html#3984" class="Bound">f</a> <a id="4027" href="plfa.part1.Isomorphism.html#4016" class="Bound">x</a> <a id="4029" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4031" href="plfa.part1.Isomorphism.html#3986" class="Bound">g</a> <a id="4033" href="plfa.part1.Isomorphism.html#4016" class="Bound">x</a><a id="4034" class="Symbol">)</a>
<a id="4042" class="Comment">-----------------------</a>
<a id="4070" class="Symbol">→</a> <a id="4072" href="/19.08/Isomorphism/#3984" class="Bound">f</a> <a id="4074" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4076" href="plfa.part1.Isomorphism.html#3986" class="Bound">g</a>
</pre>
<p>Here the type of <code class="language-plaintext highlighter-rouge">f</code> and <code class="language-plaintext highlighter-rouge">g</code> has changed from <code class="language-plaintext highlighter-rouge">A → B</code> to
<code class="language-plaintext highlighter-rouge">∀ (x : A) → B x</code>, generalising ordinary functions to
dependent functions.</p>
<h2 id="isomorphism">Isomorphism</h2>
<p>Two sets are isomorphic if they are in one-to-one correspondence.
Here is a formal definition of isomorphism:</p>
<pre class="Agda"><a id="4346" class="Keyword">infix</a> <a id="4352" class="Number">0</a> <a id="4354" href="/19.08/Isomorphism/#4365" class="Record Operator">_≃_</a>
<a id="4358" class="Keyword">record</a> <a id="_≃_"></a><a id="4365" href="/19.08/Isomorphism/#4365" class="Record Operator">_≃_</a> <a id="4369" class="Symbol">(</a><a id="4370" href="plfa.part1.Isomorphism.html#4370" class="Bound">A</a> <a id="4372" href="plfa.part1.Isomorphism.html#4372" class="Bound">B</a> <a id="4374" class="Symbol">:</a> <a id="4376" class="PrimitiveType">Set</a><a id="4379" class="Symbol">)</a> <a id="4381" class="Symbol">:</a> <a id="4383" class="PrimitiveType">Set</a> <a id="4387" class="Keyword">where</a>
<a id="4395" class="Keyword">field</a>
<a id="_≃_.to"></a><a id="4405" href="/19.08/Isomorphism/#4405" class="Field">to</a> <a id="4410" class="Symbol">:</a> <a id="4412" href="plfa.part1.Isomorphism.html#4370" class="Bound">A</a> <a id="4414" class="Symbol">→</a> <a id="4416" href="plfa.part1.Isomorphism.html#4372" class="Bound">B</a>
<a id="_≃_.from"></a><a id="4422" href="/19.08/Isomorphism/#4422" class="Field">from</a> <a id="4427" class="Symbol">:</a> <a id="4429" href="plfa.part1.Isomorphism.html#4372" class="Bound">B</a> <a id="4431" class="Symbol">→</a> <a id="4433" href="plfa.part1.Isomorphism.html#4370" class="Bound">A</a>
<a id="_≃_.from∘to"></a><a id="4439" href="/19.08/Isomorphism/#4439" class="Field">from∘to</a> <a id="4447" class="Symbol">:</a> <a id="4449" class="Symbol">∀</a> <a id="4451" class="Symbol">(</a><a id="4452" href="plfa.part1.Isomorphism.html#4452" class="Bound">x</a> <a id="4454" class="Symbol">:</a> <a id="4456" href="plfa.part1.Isomorphism.html#4370" class="Bound">A</a><a id="4457" class="Symbol">)</a> <a id="4459" class="Symbol">→</a> <a id="4461" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="4466" class="Symbol">(</a><a id="4467" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="4470" href="plfa.part1.Isomorphism.html#4452" class="Bound">x</a><a id="4471" class="Symbol">)</a> <a id="4473" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4475" href="plfa.part1.Isomorphism.html#4452" class="Bound">x</a>
<a id="_≃_.to∘from"></a><a id="4481" href="/19.08/Isomorphism/#4481" class="Field">to∘from</a> <a id="4489" class="Symbol">:</a> <a id="4491" class="Symbol">∀</a> <a id="4493" class="Symbol">(</a><a id="4494" href="plfa.part1.Isomorphism.html#4494" class="Bound">y</a> <a id="4496" class="Symbol">:</a> <a id="4498" href="plfa.part1.Isomorphism.html#4372" class="Bound">B</a><a id="4499" class="Symbol">)</a> <a id="4501" class="Symbol">→</a> <a id="4503" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="4506" class="Symbol">(</a><a id="4507" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="4512" href="plfa.part1.Isomorphism.html#4494" class="Bound">y</a><a id="4513" class="Symbol">)</a> <a id="4515" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4517" href="plfa.part1.Isomorphism.html#4494" class="Bound">y</a>
<a id="4519" class="Keyword">open</a> <a id="4524" href="/19.08/Isomorphism/#4365" class="Module Operator">_≃_</a>
</pre>
<p>Let’s unpack the definition. An isomorphism between sets <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code> consists
of four things:</p>
<ul>
<li>A function <code class="language-plaintext highlighter-rouge">to</code> from <code class="language-plaintext highlighter-rouge">A</code> to <code class="language-plaintext highlighter-rouge">B</code>,</li>
<li>A function <code class="language-plaintext highlighter-rouge">from</code> from <code class="language-plaintext highlighter-rouge">B</code> back to <code class="language-plaintext highlighter-rouge">A</code>,</li>
<li>Evidence <code class="language-plaintext highlighter-rouge">from∘to</code> asserting that <code class="language-plaintext highlighter-rouge">from</code> is a <em>left-inverse</em> for <code class="language-plaintext highlighter-rouge">to</code>,</li>
<li>Evidence <code class="language-plaintext highlighter-rouge">to∘from</code> asserting that <code class="language-plaintext highlighter-rouge">from</code> is a <em>right-inverse</em> for <code class="language-plaintext highlighter-rouge">to</code>.</li>
</ul>
<p>In particular, the third asserts that <code class="language-plaintext highlighter-rouge">from ∘ to</code> is the identity, and
the fourth that <code class="language-plaintext highlighter-rouge">to ∘ from</code> is the identity, hence the names.
The declaration <code class="language-plaintext highlighter-rouge">open _≃_</code> makes available the names <code class="language-plaintext highlighter-rouge">to</code>, <code class="language-plaintext highlighter-rouge">from</code>,
<code class="language-plaintext highlighter-rouge">from∘to</code>, and <code class="language-plaintext highlighter-rouge">to∘from</code>, otherwise we would need to write <code class="language-plaintext highlighter-rouge">_≃_.to</code> and so on.</p>
<p>The above is our first use of records. A record declaration is equivalent
to a corresponding inductive data declaration:</p>
<pre class="Agda"><a id="5256" class="Keyword">data</a> <a id="_≃′_"></a><a id="5261" href="/19.08/Isomorphism/#5261" class="Datatype Operator">_≃′_</a> <a id="5266" class="Symbol">(</a><a id="5267" href="plfa.part1.Isomorphism.html#5267" class="Bound">A</a> <a id="5269" href="plfa.part1.Isomorphism.html#5269" class="Bound">B</a> <a id="5271" class="Symbol">:</a> <a id="5273" class="PrimitiveType">Set</a><a id="5276" class="Symbol">):</a> <a id="5279" class="PrimitiveType">Set</a> <a id="5283" class="Keyword">where</a>
<a id="_≃′_.mk-≃′"></a><a id="5291" href="/19.08/Isomorphism/#5291" class="InductiveConstructor">mk-≃′</a> <a id="5297" class="Symbol">:</a> <a id="5299" class="Symbol">∀</a> <a id="5301" class="Symbol">(</a><a id="5302" href="plfa.part1.Isomorphism.html#5302" class="Bound">to</a> <a id="5305" class="Symbol">:</a> <a id="5307" href="plfa.part1.Isomorphism.html#5267" class="Bound">A</a> <a id="5309" class="Symbol">→</a> <a id="5311" href="plfa.part1.Isomorphism.html#5269" class="Bound">B</a><a id="5312" class="Symbol">)</a> <a id="5314" class="Symbol">→</a>
<a id="5326" class="Symbol">∀</a> <a id="5328" class="Symbol">(</a><a id="5329" href="/19.08/Isomorphism/#5329" class="Bound">from</a> <a id="5334" class="Symbol">:</a> <a id="5336" href="plfa.part1.Isomorphism.html#5269" class="Bound">B</a> <a id="5338" class="Symbol">→</a> <a id="5340" href="plfa.part1.Isomorphism.html#5267" class="Bound">A</a><a id="5341" class="Symbol">)</a> <a id="5343" class="Symbol">→</a>
<a id="5355" class="Symbol">∀</a> <a id="5357" class="Symbol">(</a><a id="5358" href="/19.08/Isomorphism/#5358" class="Bound">from∘to</a> <a id="5366" class="Symbol">:</a> <a id="5368" class="Symbol">(∀</a> <a id="5371" class="Symbol">(</a><a id="5372" href="plfa.part1.Isomorphism.html#5372" class="Bound">x</a> <a id="5374" class="Symbol">:</a> <a id="5376" href="plfa.part1.Isomorphism.html#5267" class="Bound">A</a><a id="5377" class="Symbol">)</a> <a id="5379" class="Symbol">→</a> <a id="5381" href="plfa.part1.Isomorphism.html#5329" class="Bound">from</a> <a id="5386" class="Symbol">(</a><a id="5387" href="plfa.part1.Isomorphism.html#5302" class="Bound">to</a> <a id="5390" href="plfa.part1.Isomorphism.html#5372" class="Bound">x</a><a id="5391" class="Symbol">)</a> <a id="5393" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="5395" href="plfa.part1.Isomorphism.html#5372" class="Bound">x</a><a id="5396" class="Symbol">))</a> <a id="5399" class="Symbol">→</a>
<a id="5411" class="Symbol">∀</a> <a id="5413" class="Symbol">(</a><a id="5414" href="/19.08/Isomorphism/#5414" class="Bound">to∘from</a> <a id="5422" class="Symbol">:</a> <a id="5424" class="Symbol">(∀</a> <a id="5427" class="Symbol">(</a><a id="5428" href="plfa.part1.Isomorphism.html#5428" class="Bound">y</a> <a id="5430" class="Symbol">:</a> <a id="5432" href="plfa.part1.Isomorphism.html#5269" class="Bound">B</a><a id="5433" class="Symbol">)</a> <a id="5435" class="Symbol">→</a> <a id="5437" href="plfa.part1.Isomorphism.html#5302" class="Bound">to</a> <a id="5440" class="Symbol">(</a><a id="5441" href="plfa.part1.Isomorphism.html#5329" class="Bound">from</a> <a id="5446" href="plfa.part1.Isomorphism.html#5428" class="Bound">y</a><a id="5447" class="Symbol">)</a> <a id="5449" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="5451" href="plfa.part1.Isomorphism.html#5428" class="Bound">y</a><a id="5452" class="Symbol">))</a> <a id="5455" class="Symbol">→</a>
<a id="5467" href="/19.08/Isomorphism/#5267" class="Bound">A</a> <a id="5469" href="plfa.part1.Isomorphism.html#5261" class="Datatype Operator">≃′</a> <a id="5472" href="plfa.part1.Isomorphism.html#5269" class="Bound">B</a>
<a id="to′"></a><a id="5475" href="/19.08/Isomorphism/#5475" class="Function">to′</a> <a id="5479" class="Symbol">:</a> <a id="5481" class="Symbol">∀</a> <a id="5483" class="Symbol">{</a><a id="5484" href="plfa.part1.Isomorphism.html#5484" class="Bound">A</a> <a id="5486" href="plfa.part1.Isomorphism.html#5486" class="Bound">B</a> <a id="5488" class="Symbol">:</a> <a id="5490" class="PrimitiveType">Set</a><a id="5493" class="Symbol">}</a> <a id="5495" class="Symbol">→</a> <a id="5497" class="Symbol">(</a><a id="5498" href="plfa.part1.Isomorphism.html#5484" class="Bound">A</a> <a id="5500" href="plfa.part1.Isomorphism.html#5261" class="Datatype Operator">≃′</a> <a id="5503" href="plfa.part1.Isomorphism.html#5486" class="Bound">B</a><a id="5504" class="Symbol">)</a> <a id="5506" class="Symbol">→</a> <a id="5508" class="Symbol">(</a><a id="5509" href="plfa.part1.Isomorphism.html#5484" class="Bound">A</a> <a id="5511" class="Symbol">→</a> <a id="5513" href="plfa.part1.Isomorphism.html#5486" class="Bound">B</a><a id="5514" class="Symbol">)</a>
<a id="5516" href="/19.08/Isomorphism/#5475" class="Function">to′</a> <a id="5520" class="Symbol">(</a><a id="5521" href="plfa.part1.Isomorphism.html#5291" class="InductiveConstructor">mk-≃′</a> <a id="5527" href="plfa.part1.Isomorphism.html#5527" class="Bound">f</a> <a id="5529" href="plfa.part1.Isomorphism.html#5529" class="Bound">g</a> <a id="5531" href="plfa.part1.Isomorphism.html#5531" class="Bound">g∘f</a> <a id="5535" href="plfa.part1.Isomorphism.html#5535" class="Bound">f∘g</a><a id="5538" class="Symbol">)</a> <a id="5540" class="Symbol">=</a> <a id="5542" href="plfa.part1.Isomorphism.html#5527" class="Bound">f</a>
<a id="from′"></a><a id="5545" href="/19.08/Isomorphism/#5545" class="Function">from′</a> <a id="5551" class="Symbol">:</a> <a id="5553" class="Symbol">∀</a> <a id="5555" class="Symbol">{</a><a id="5556" href="plfa.part1.Isomorphism.html#5556" class="Bound">A</a> <a id="5558" href="plfa.part1.Isomorphism.html#5558" class="Bound">B</a> <a id="5560" class="Symbol">:</a> <a id="5562" class="PrimitiveType">Set</a><a id="5565" class="Symbol">}</a> <a id="5567" class="Symbol">→</a> <a id="5569" class="Symbol">(</a><a id="5570" href="plfa.part1.Isomorphism.html#5556" class="Bound">A</a> <a id="5572" href="plfa.part1.Isomorphism.html#5261" class="Datatype Operator">≃′</a> <a id="5575" href="plfa.part1.Isomorphism.html#5558" class="Bound">B</a><a id="5576" class="Symbol">)</a> <a id="5578" class="Symbol">→</a> <a id="5580" class="Symbol">(</a><a id="5581" href="plfa.part1.Isomorphism.html#5558" class="Bound">B</a> <a id="5583" class="Symbol">→</a> <a id="5585" href="plfa.part1.Isomorphism.html#5556" class="Bound">A</a><a id="5586" class="Symbol">)</a>
<a id="5588" href="/19.08/Isomorphism/#5545" class="Function">from′</a> <a id="5594" class="Symbol">(</a><a id="5595" href="plfa.part1.Isomorphism.html#5291" class="InductiveConstructor">mk-≃′</a> <a id="5601" href="plfa.part1.Isomorphism.html#5601" class="Bound">f</a> <a id="5603" href="plfa.part1.Isomorphism.html#5603" class="Bound">g</a> <a id="5605" href="plfa.part1.Isomorphism.html#5605" class="Bound">g∘f</a> <a id="5609" href="plfa.part1.Isomorphism.html#5609" class="Bound">f∘g</a><a id="5612" class="Symbol">)</a> <a id="5614" class="Symbol">=</a> <a id="5616" href="plfa.part1.Isomorphism.html#5603" class="Bound">g</a>
<a id="from∘to′"></a><a id="5619" href="/19.08/Isomorphism/#5619" class="Function">from∘to′</a> <a id="5628" class="Symbol">:</a> <a id="5630" class="Symbol">∀</a> <a id="5632" class="Symbol">{</a><a id="5633" href="plfa.part1.Isomorphism.html#5633" class="Bound">A</a> <a id="5635" href="plfa.part1.Isomorphism.html#5635" class="Bound">B</a> <a id="5637" class="Symbol">:</a> <a id="5639" class="PrimitiveType">Set</a><a id="5642" class="Symbol">}</a> <a id="5644" class="Symbol">→</a> <a id="5646" class="Symbol">(</a><a id="5647" href="plfa.part1.Isomorphism.html#5647" class="Bound">A≃B</a> <a id="5651" class="Symbol">:</a> <a id="5653" href="plfa.part1.Isomorphism.html#5633" class="Bound">A</a> <a id="5655" href="plfa.part1.Isomorphism.html#5261" class="Datatype Operator">≃′</a> <a id="5658" href="plfa.part1.Isomorphism.html#5635" class="Bound">B</a><a id="5659" class="Symbol">)</a> <a id="5661" class="Symbol">→</a> <a id="5663" class="Symbol">(∀</a> <a id="5666" class="Symbol">(</a><a id="5667" href="plfa.part1.Isomorphism.html#5667" class="Bound">x</a> <a id="5669" class="Symbol">:</a> <a id="5671" href="plfa.part1.Isomorphism.html#5633" class="Bound">A</a><a id="5672" class="Symbol">)</a> <a id="5674" class="Symbol">→</a> <a id="5676" href="plfa.part1.Isomorphism.html#5545" class="Function">from′</a> <a id="5682" href="plfa.part1.Isomorphism.html#5647" class="Bound">A≃B</a> <a id="5686" class="Symbol">(</a><a id="5687" href="plfa.part1.Isomorphism.html#5475" class="Function">to′</a> <a id="5691" href="plfa.part1.Isomorphism.html#5647" class="Bound">A≃B</a> <a id="5695" href="plfa.part1.Isomorphism.html#5667" class="Bound">x</a><a id="5696" class="Symbol">)</a> <a id="5698" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="5700" href="plfa.part1.Isomorphism.html#5667" class="Bound">x</a><a id="5701" class="Symbol">)</a>
<a id="5703" href="/19.08/Isomorphism/#5619" class="Function">from∘to′</a> <a id="5712" class="Symbol">(</a><a id="5713" href="plfa.part1.Isomorphism.html#5291" class="InductiveConstructor">mk-≃′</a> <a id="5719" href="plfa.part1.Isomorphism.html#5719" class="Bound">f</a> <a id="5721" href="plfa.part1.Isomorphism.html#5721" class="Bound">g</a> <a id="5723" href="plfa.part1.Isomorphism.html#5723" class="Bound">g∘f</a> <a id="5727" href="plfa.part1.Isomorphism.html#5727" class="Bound">f∘g</a><a id="5730" class="Symbol">)</a> <a id="5732" class="Symbol">=</a> <a id="5734" href="plfa.part1.Isomorphism.html#5723" class="Bound">g∘f</a>
<a id="to∘from′"></a><a id="5739" href="/19.08/Isomorphism/#5739" class="Function">to∘from′</a> <a id="5748" class="Symbol">:</a> <a id="5750" class="Symbol">∀</a> <a id="5752" class="Symbol">{</a><a id="5753" href="plfa.part1.Isomorphism.html#5753" class="Bound">A</a> <a id="5755" href="plfa.part1.Isomorphism.html#5755" class="Bound">B</a> <a id="5757" class="Symbol">:</a> <a id="5759" class="PrimitiveType">Set</a><a id="5762" class="Symbol">}</a> <a id="5764" class="Symbol">→</a> <a id="5766" class="Symbol">(</a><a id="5767" href="plfa.part1.Isomorphism.html#5767" class="Bound">A≃B</a> <a id="5771" class="Symbol">:</a> <a id="5773" href="plfa.part1.Isomorphism.html#5753" class="Bound">A</a> <a id="5775" href="plfa.part1.Isomorphism.html#5261" class="Datatype Operator">≃′</a> <a id="5778" href="plfa.part1.Isomorphism.html#5755" class="Bound">B</a><a id="5779" class="Symbol">)</a> <a id="5781" class="Symbol">→</a> <a id="5783" class="Symbol">(∀</a> <a id="5786" class="Symbol">(</a><a id="5787" href="plfa.part1.Isomorphism.html#5787" class="Bound">y</a> <a id="5789" class="Symbol">:</a> <a id="5791" href="plfa.part1.Isomorphism.html#5755" class="Bound">B</a><a id="5792" class="Symbol">)</a> <a id="5794" class="Symbol">→</a> <a id="5796" href="plfa.part1.Isomorphism.html#5475" class="Function">to′</a> <a id="5800" href="plfa.part1.Isomorphism.html#5767" class="Bound">A≃B</a> <a id="5804" class="Symbol">(</a><a id="5805" href="plfa.part1.Isomorphism.html#5545" class="Function">from′</a> <a id="5811" href="plfa.part1.Isomorphism.html#5767" class="Bound">A≃B</a> <a id="5815" href="plfa.part1.Isomorphism.html#5787" class="Bound">y</a><a id="5816" class="Symbol">)</a> <a id="5818" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="5820" href="plfa.part1.Isomorphism.html#5787" class="Bound">y</a><a id="5821" class="Symbol">)</a>
<a id="5823" href="/19.08/Isomorphism/#5739" class="Function">to∘from′</a> <a id="5832" class="Symbol">(</a><a id="5833" href="plfa.part1.Isomorphism.html#5291" class="InductiveConstructor">mk-≃′</a> <a id="5839" href="plfa.part1.Isomorphism.html#5839" class="Bound">f</a> <a id="5841" href="plfa.part1.Isomorphism.html#5841" class="Bound">g</a> <a id="5843" href="plfa.part1.Isomorphism.html#5843" class="Bound">g∘f</a> <a id="5847" href="plfa.part1.Isomorphism.html#5847" class="Bound">f∘g</a><a id="5850" class="Symbol">)</a> <a id="5852" class="Symbol">=</a> <a id="5854" href="plfa.part1.Isomorphism.html#5847" class="Bound">f∘g</a>
</pre>
<p>We construct values of the record type with the syntax</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>record
{ to = f
; from = g
; from∘to = g∘f
; to∘from = f∘g
}
</code></pre></div></div>
<p>which corresponds to using the constructor of the corresponding
inductive type</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>mk-≃′ f g g∘f f∘g
</code></pre></div></div>
<p>where <code class="language-plaintext highlighter-rouge">f</code>, <code class="language-plaintext highlighter-rouge">g</code>, <code class="language-plaintext highlighter-rouge">g∘f</code>, and <code class="language-plaintext highlighter-rouge">f∘g</code> are values of suitable types.</p>
<h2 id="isomorphism-is-an-equivalence">Isomorphism is an equivalence</h2>
<p>Isomorphism is an equivalence, meaning that it is reflexive, symmetric,
and transitive. To show isomorphism is reflexive, we take both <code class="language-plaintext highlighter-rouge">to</code>
and <code class="language-plaintext highlighter-rouge">from</code> to be the identity function:</p>
<pre class="Agda"><a id="≃-refl"></a><a id="6406" href="/19.08/Isomorphism/#6406" class="Function">≃-refl</a> <a id="6413" class="Symbol">:</a> <a id="6415" class="Symbol">∀</a> <a id="6417" class="Symbol">{</a><a id="6418" href="plfa.part1.Isomorphism.html#6418" class="Bound">A</a> <a id="6420" class="Symbol">:</a> <a id="6422" class="PrimitiveType">Set</a><a id="6425" class="Symbol">}</a>
<a id="6431" class="Comment">-----</a>
<a id="6439" class="Symbol">→</a> <a id="6441" href="/19.08/Isomorphism/#6418" class="Bound">A</a> <a id="6443" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="6445" href="plfa.part1.Isomorphism.html#6418" class="Bound">A</a>
<a id="6447" href="/19.08/Isomorphism/#6406" class="Function">≃-refl</a> <a id="6454" class="Symbol">=</a>
<a id="6458" class="Keyword">record</a>
<a id="6469" class="Symbol">{</a> <a id="6471" href="/19.08/Isomorphism/#4405" class="Field">to</a> <a id="6479" class="Symbol">=</a> <a id="6481" class="Symbol">λ{</a><a id="6483" href="plfa.part1.Isomorphism.html#6483" class="Bound">x</a> <a id="6485" class="Symbol">→</a> <a id="6487" href="plfa.part1.Isomorphism.html#6483" class="Bound">x</a><a id="6488" class="Symbol">}</a>
<a id="6494" class="Symbol">;</a> <a id="6496" href="/19.08/Isomorphism/#4422" class="Field">from</a> <a id="6504" class="Symbol">=</a> <a id="6506" class="Symbol">λ{</a><a id="6508" href="plfa.part1.Isomorphism.html#6508" class="Bound">y</a> <a id="6510" class="Symbol">→</a> <a id="6512" href="plfa.part1.Isomorphism.html#6508" class="Bound">y</a><a id="6513" class="Symbol">}</a>
<a id="6519" class="Symbol">;</a> <a id="6521" href="/19.08/Isomorphism/#4439" class="Field">from∘to</a> <a id="6529" class="Symbol">=</a> <a id="6531" class="Symbol">λ{</a><a id="6533" href="plfa.part1.Isomorphism.html#6533" class="Bound">x</a> <a id="6535" class="Symbol">→</a> <a id="6537" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="6541" class="Symbol">}</a>
<a id="6547" class="Symbol">;</a> <a id="6549" href="/19.08/Isomorphism/#4481" class="Field">to∘from</a> <a id="6557" class="Symbol">=</a> <a id="6559" class="Symbol">λ{</a><a id="6561" href="plfa.part1.Isomorphism.html#6561" class="Bound">y</a> <a id="6563" class="Symbol">→</a> <a id="6565" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="6569" class="Symbol">}</a>
<a id="6575" class="Symbol">}</a>
</pre>
<p>In the above, <code class="language-plaintext highlighter-rouge">to</code> and <code class="language-plaintext highlighter-rouge">from</code> are both bound to identity functions,
and <code class="language-plaintext highlighter-rouge">from∘to</code> and <code class="language-plaintext highlighter-rouge">to∘from</code> are both bound to functions that discard
their argument and return <code class="language-plaintext highlighter-rouge">refl</code>. In this case, <code class="language-plaintext highlighter-rouge">refl</code> alone is an
adequate proof since for the left inverse, <code class="language-plaintext highlighter-rouge">from (to x)</code>
simplifies to <code class="language-plaintext highlighter-rouge">x</code>, and similarly for the right inverse.</p>
<p>To show isomorphism is symmetric, we simply swap the roles of <code class="language-plaintext highlighter-rouge">to</code>
and <code class="language-plaintext highlighter-rouge">from</code>, and <code class="language-plaintext highlighter-rouge">from∘to</code> and <code class="language-plaintext highlighter-rouge">to∘from</code>:</p>
<pre class="Agda"><a id="≃-sym"></a><a id="7012" href="/19.08/Isomorphism/#7012" class="Function">≃-sym</a> <a id="7018" class="Symbol">:</a> <a id="7020" class="Symbol">∀</a> <a id="7022" class="Symbol">{</a><a id="7023" href="plfa.part1.Isomorphism.html#7023" class="Bound">A</a> <a id="7025" href="plfa.part1.Isomorphism.html#7025" class="Bound">B</a> <a id="7027" class="Symbol">:</a> <a id="7029" class="PrimitiveType">Set</a><a id="7032" class="Symbol">}</a>
<a id="7036" class="Symbol">→</a> <a id="7038" href="/19.08/Isomorphism/#7023" class="Bound">A</a> <a id="7040" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="7042" href="plfa.part1.Isomorphism.html#7025" class="Bound">B</a>
<a id="7048" class="Comment">-----</a>
<a id="7056" class="Symbol">→</a> <a id="7058" href="/19.08/Isomorphism/#7025" class="Bound">B</a> <a id="7060" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="7062" href="plfa.part1.Isomorphism.html#7023" class="Bound">A</a>
<a id="7064" href="/19.08/Isomorphism/#7012" class="Function">≃-sym</a> <a id="7070" href="plfa.part1.Isomorphism.html#7070" class="Bound">A≃B</a> <a id="7074" class="Symbol">=</a>
<a id="7078" class="Keyword">record</a>
<a id="7089" class="Symbol">{</a> <a id="7091" href="/19.08/Isomorphism/#4405" class="Field">to</a> <a id="7099" class="Symbol">=</a> <a id="7101" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="7106" href="plfa.part1.Isomorphism.html#7070" class="Bound">A≃B</a>
<a id="7114" class="Symbol">;</a> <a id="7116" href="/19.08/Isomorphism/#4422" class="Field">from</a> <a id="7124" class="Symbol">=</a> <a id="7126" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7131" href="plfa.part1.Isomorphism.html#7070" class="Bound">A≃B</a>
<a id="7139" class="Symbol">;</a> <a id="7141" href="/19.08/Isomorphism/#4439" class="Field">from∘to</a> <a id="7149" class="Symbol">=</a> <a id="7151" href="plfa.part1.Isomorphism.html#4481" class="Field">to∘from</a> <a id="7159" href="plfa.part1.Isomorphism.html#7070" class="Bound">A≃B</a>
<a id="7167" class="Symbol">;</a> <a id="7169" href="/19.08/Isomorphism/#4481" class="Field">to∘from</a> <a id="7177" class="Symbol">=</a> <a id="7179" href="plfa.part1.Isomorphism.html#4439" class="Field">from∘to</a> <a id="7187" href="plfa.part1.Isomorphism.html#7070" class="Bound">A≃B</a>
<a id="7195" class="Symbol">}</a>
</pre>
<p>To show isomorphism is transitive, we compose the <code class="language-plaintext highlighter-rouge">to</code> and <code class="language-plaintext highlighter-rouge">from</code>
functions, and use equational reasoning to combine the inverses:</p>
<pre class="Agda"><a id="≃-trans"></a><a id="7337" href="/19.08/Isomorphism/#7337" class="Function">≃-trans</a> <a id="7345" class="Symbol">:</a> <a id="7347" class="Symbol">∀</a> <a id="7349" class="Symbol">{</a><a id="7350" href="plfa.part1.Isomorphism.html#7350" class="Bound">A</a> <a id="7352" href="plfa.part1.Isomorphism.html#7352" class="Bound">B</a> <a id="7354" href="plfa.part1.Isomorphism.html#7354" class="Bound">C</a> <a id="7356" class="Symbol">:</a> <a id="7358" class="PrimitiveType">Set</a><a id="7361" class="Symbol">}</a>
<a id="7365" class="Symbol">→</a> <a id="7367" href="/19.08/Isomorphism/#7350" class="Bound">A</a> <a id="7369" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="7371" href="plfa.part1.Isomorphism.html#7352" class="Bound">B</a>
<a id="7375" class="Symbol">→</a> <a id="7377" href="/19.08/Isomorphism/#7352" class="Bound">B</a> <a id="7379" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="7381" href="plfa.part1.Isomorphism.html#7354" class="Bound">C</a>
<a id="7387" class="Comment">-----</a>
<a id="7395" class="Symbol">→</a> <a id="7397" href="/19.08/Isomorphism/#7350" class="Bound">A</a> <a id="7399" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="7401" href="plfa.part1.Isomorphism.html#7354" class="Bound">C</a>
<a id="7403" href="/19.08/Isomorphism/#7337" class="Function">≃-trans</a> <a id="7411" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7415" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="7419" class="Symbol">=</a>
<a id="7423" class="Keyword">record</a>
<a id="7434" class="Symbol">{</a> <a id="7436" href="/19.08/Isomorphism/#4405" class="Field">to</a> <a id="7445" class="Symbol">=</a> <a id="7447" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7452" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="7456" href="plfa.part1.Isomorphism.html#1952" class="Function Operator">∘</a> <a id="7458" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7463" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a>
<a id="7471" class="Symbol">;</a> <a id="7473" href="/19.08/Isomorphism/#4422" class="Field">from</a> <a id="7482" class="Symbol">=</a> <a id="7484" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="7489" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7493" href="plfa.part1.Isomorphism.html#1952" class="Function Operator">∘</a> <a id="7495" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="7500" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a>
<a id="7508" class="Symbol">;</a> <a id="7510" href="/19.08/Isomorphism/#4439" class="Field">from∘to</a> <a id="7519" class="Symbol">=</a> <a id="7521" class="Symbol">λ{</a><a id="7523" href="plfa.part1.Isomorphism.html#7523" class="Bound">x</a> <a id="7525" class="Symbol">→</a>
<a id="7535" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="7551" class="Symbol">(</a><a id="7552" href="/19.08/Isomorphism/#4422" class="Field">from</a> <a id="7557" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7561" href="plfa.part1.Isomorphism.html#1952" class="Function Operator">∘</a> <a id="7563" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="7568" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a><a id="7571" class="Symbol">)</a> <a id="7573" class="Symbol">((</a><a id="7575" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7578" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="7582" href="plfa.part1.Isomorphism.html#1952" class="Function Operator">∘</a> <a id="7584" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7587" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a><a id="7590" class="Symbol">)</a> <a id="7592" href="plfa.part1.Isomorphism.html#7523" class="Bound">x</a><a id="7593" class="Symbol">)</a>
<a id="7603" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="7617" href="/19.08/Isomorphism/#4422" class="Field">from</a> <a id="7622" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7626" class="Symbol">(</a><a id="7627" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="7632" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="7636" class="Symbol">(</a><a id="7637" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7640" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="7644" class="Symbol">(</a><a id="7645" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7648" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7652" href="plfa.part1.Isomorphism.html#7523" class="Bound">x</a><a id="7653" class="Symbol">)))</a>
<a id="7665" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="7668" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="7673" class="Symbol">(</a><a id="7674" href="/19.08/Isomorphism/#4422" class="Field">from</a> <a id="7679" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a><a id="7682" class="Symbol">)</a> <a id="7684" class="Symbol">(</a><a id="7685" href="plfa.part1.Isomorphism.html#4439" class="Field">from∘to</a> <a id="7693" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="7697" class="Symbol">(</a><a id="7698" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7701" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7705" href="plfa.part1.Isomorphism.html#7523" class="Bound">x</a><a id="7706" class="Symbol">))</a> <a id="7709" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="7721" href="/19.08/Isomorphism/#4422" class="Field">from</a> <a id="7726" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7730" class="Symbol">(</a><a id="7731" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7734" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7738" href="plfa.part1.Isomorphism.html#7523" class="Bound">x</a><a id="7739" class="Symbol">)</a>
<a id="7749" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="7752" href="/19.08/Isomorphism/#4439" class="Field">from∘to</a> <a id="7760" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7764" href="plfa.part1.Isomorphism.html#7523" class="Bound">x</a> <a id="7766" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="7778" href="/19.08/Isomorphism/#7523" class="Bound">x</a>
<a id="7788" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a><a id="7789" class="Symbol">}</a>
<a id="7795" class="Symbol">;</a> <a id="7797" href="/19.08/Isomorphism/#4481" class="Field">to∘from</a> <a id="7805" class="Symbol">=</a> <a id="7807" class="Symbol">λ{</a><a id="7809" href="plfa.part1.Isomorphism.html#7809" class="Bound">y</a> <a id="7811" class="Symbol">→</a>
<a id="7821" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="7837" class="Symbol">(</a><a id="7838" href="/19.08/Isomorphism/#4405" class="Field">to</a> <a id="7841" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="7845" href="plfa.part1.Isomorphism.html#1952" class="Function Operator">∘</a> <a id="7847" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7850" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a><a id="7853" class="Symbol">)</a> <a id="7855" class="Symbol">((</a><a id="7857" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="7862" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7866" href="plfa.part1.Isomorphism.html#1952" class="Function Operator">∘</a> <a id="7868" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="7873" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a><a id="7876" class="Symbol">)</a> <a id="7878" href="plfa.part1.Isomorphism.html#7809" class="Bound">y</a><a id="7879" class="Symbol">)</a>
<a id="7889" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="7903" href="/19.08/Isomorphism/#4405" class="Field">to</a> <a id="7906" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="7910" class="Symbol">(</a><a id="7911" href="plfa.part1.Isomorphism.html#4405" class="Field">to</a> <a id="7914" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7918" class="Symbol">(</a><a id="7919" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="7924" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7928" class="Symbol">(</a><a id="7929" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="7934" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="7938" href="plfa.part1.Isomorphism.html#7809" class="Bound">y</a><a id="7939" class="Symbol">)))</a>
<a id="7951" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="7954" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="7959" class="Symbol">(</a><a id="7960" href="/19.08/Isomorphism/#4405" class="Field">to</a> <a id="7963" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a><a id="7966" class="Symbol">)</a> <a id="7968" class="Symbol">(</a><a id="7969" href="plfa.part1.Isomorphism.html#4481" class="Field">to∘from</a> <a id="7977" href="plfa.part1.Isomorphism.html#7411" class="Bound">A≃B</a> <a id="7981" class="Symbol">(</a><a id="7982" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="7987" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="7991" href="plfa.part1.Isomorphism.html#7809" class="Bound">y</a><a id="7992" class="Symbol">))</a> <a id="7995" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="8007" href="/19.08/Isomorphism/#4405" class="Field">to</a> <a id="8010" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="8014" class="Symbol">(</a><a id="8015" href="plfa.part1.Isomorphism.html#4422" class="Field">from</a> <a id="8020" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="8024" href="plfa.part1.Isomorphism.html#7809" class="Bound">y</a><a id="8025" class="Symbol">)</a>
<a id="8035" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="8038" href="/19.08/Isomorphism/#4481" class="Field">to∘from</a> <a id="8046" href="plfa.part1.Isomorphism.html#7415" class="Bound">B≃C</a> <a id="8050" href="plfa.part1.Isomorphism.html#7809" class="Bound">y</a> <a id="8052" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="8064" href="/19.08/Isomorphism/#7809" class="Bound">y</a>
<a id="8074" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a><a id="8075" class="Symbol">}</a>
<a id="8082" class="Symbol">}</a>
</pre>
<h2 id="equational-reasoning-for-isomorphism">Equational reasoning for isomorphism</h2>
<p>It is straightforward to support a variant of equational reasoning for
isomorphism. We essentially copy the previous definition
of equality for isomorphism. We omit the form that corresponds to <code class="language-plaintext highlighter-rouge">_≡⟨⟩_</code>, since
trivial isomorphisms arise far less often than trivial equalities:</p>
<pre class="Agda"><a id="8414" class="Keyword">module</a> <a id="≃-Reasoning"></a><a id="8421" href="/19.08/Isomorphism/#8421" class="Module">≃-Reasoning</a> <a id="8433" class="Keyword">where</a>
<a id="8442" class="Keyword">infix</a> <a id="8449" class="Number">1</a> <a id="8451" href="/19.08/Isomorphism/#8497" class="Function Operator">≃-begin_</a>
<a id="8462" class="Keyword">infixr</a> <a id="8469" class="Number">2</a> <a id="8471" href="/19.08/Isomorphism/#8581" class="Function Operator">_≃⟨_⟩_</a>
<a id="8480" class="Keyword">infix</a> <a id="8487" class="Number">3</a> <a id="8489" href="/19.08/Isomorphism/#8700" class="Function Operator">_≃-∎</a>
<a id="≃-Reasoning.≃-begin_"></a><a id="8497" href="/19.08/Isomorphism/#8497" class="Function Operator">≃-begin_</a> <a id="8506" class="Symbol">:</a> <a id="8508" class="Symbol">∀</a> <a id="8510" class="Symbol">{</a><a id="8511" href="plfa.part1.Isomorphism.html#8511" class="Bound">A</a> <a id="8513" href="plfa.part1.Isomorphism.html#8513" class="Bound">B</a> <a id="8515" class="Symbol">:</a> <a id="8517" class="PrimitiveType">Set</a><a id="8520" class="Symbol">}</a>
<a id="8526" class="Symbol">→</a> <a id="8528" href="/19.08/Isomorphism/#8511" class="Bound">A</a> <a id="8530" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="8532" href="plfa.part1.Isomorphism.html#8513" class="Bound">B</a>
<a id="8540" class="Comment">-----</a>
<a id="8550" class="Symbol">→</a> <a id="8552" href="/19.08/Isomorphism/#8511" class="Bound">A</a> <a id="8554" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="8556" href="plfa.part1.Isomorphism.html#8513" class="Bound">B</a>
<a id="8560" href="/19.08/Isomorphism/#8497" class="Function Operator">≃-begin</a> <a id="8568" href="plfa.part1.Isomorphism.html#8568" class="Bound">A≃B</a> <a id="8572" class="Symbol">=</a> <a id="8574" href="plfa.part1.Isomorphism.html#8568" class="Bound">A≃B</a>
<a id="≃-Reasoning._≃⟨_⟩_"></a><a id="8581" href="/19.08/Isomorphism/#8581" class="Function Operator">_≃⟨_⟩_</a> <a id="8588" class="Symbol">:</a> <a id="8590" class="Symbol">∀</a> <a id="8592" class="Symbol">(</a><a id="8593" href="plfa.part1.Isomorphism.html#8593" class="Bound">A</a> <a id="8595" class="Symbol">:</a> <a id="8597" class="PrimitiveType">Set</a><a id="8600" class="Symbol">)</a> <a id="8602" class="Symbol">{</a><a id="8603" href="plfa.part1.Isomorphism.html#8603" class="Bound">B</a> <a id="8605" href="plfa.part1.Isomorphism.html#8605" class="Bound">C</a> <a id="8607" class="Symbol">:</a> <a id="8609" class="PrimitiveType">Set</a><a id="8612" class="Symbol">}</a>
<a id="8618" class="Symbol">→</a> <a id="8620" href="/19.08/Isomorphism/#8593" class="Bound">A</a> <a id="8622" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="8624" href="plfa.part1.Isomorphism.html#8603" class="Bound">B</a>
<a id="8630" class="Symbol">→</a> <a id="8632" href="/19.08/Isomorphism/#8603" class="Bound">B</a> <a id="8634" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="8636" href="plfa.part1.Isomorphism.html#8605" class="Bound">C</a>
<a id="8644" class="Comment">-----</a>
<a id="8654" class="Symbol">→</a> <a id="8656" href="/19.08/Isomorphism/#8593" class="Bound">A</a> <a id="8658" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="8660" href="plfa.part1.Isomorphism.html#8605" class="Bound">C</a>
<a id="8664" href="/19.08/Isomorphism/#8664" class="Bound">A</a> <a id="8666" href="plfa.part1.Isomorphism.html#8581" class="Function Operator">≃⟨</a> <a id="8669" href="plfa.part1.Isomorphism.html#8669" class="Bound">A≃B</a> <a id="8673" href="plfa.part1.Isomorphism.html#8581" class="Function Operator">⟩</a> <a id="8675" href="plfa.part1.Isomorphism.html#8675" class="Bound">B≃C</a> <a id="8679" class="Symbol">=</a> <a id="8681" href="plfa.part1.Isomorphism.html#7337" class="Function">≃-trans</a> <a id="8689" href="plfa.part1.Isomorphism.html#8669" class="Bound">A≃B</a> <a id="8693" href="plfa.part1.Isomorphism.html#8675" class="Bound">B≃C</a>
<a id="≃-Reasoning._≃-∎"></a><a id="8700" href="/19.08/Isomorphism/#8700" class="Function Operator">_≃-∎</a> <a id="8705" class="Symbol">:</a> <a id="8707" class="Symbol">∀</a> <a id="8709" class="Symbol">(</a><a id="8710" href="plfa.part1.Isomorphism.html#8710" class="Bound">A</a> <a id="8712" class="Symbol">:</a> <a id="8714" class="PrimitiveType">Set</a><a id="8717" class="Symbol">)</a>
<a id="8725" class="Comment">-----</a>
<a id="8735" class="Symbol">→</a> <a id="8737" href="/19.08/Isomorphism/#8710" class="Bound">A</a> <a id="8739" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="8741" href="plfa.part1.Isomorphism.html#8710" class="Bound">A</a>
<a id="8745" href="/19.08/Isomorphism/#8745" class="Bound">A</a> <a id="8747" href="plfa.part1.Isomorphism.html#8700" class="Function Operator">≃-∎</a> <a id="8751" class="Symbol">=</a> <a id="8753" href="plfa.part1.Isomorphism.html#6406" class="Function">≃-refl</a>
<a id="8761" class="Keyword">open</a> <a id="8766" href="/19.08/Isomorphism/#8421" class="Module">≃-Reasoning</a>
</pre>
<h2 id="embedding">Embedding</h2>
<p>We also need the notion of <em>embedding</em>, which is a weakening of
isomorphism. While an isomorphism shows that two types are in
one-to-one correspondence, an embedding shows that the first type is
included in the second; or, equivalently, that there is a many-to-one
correspondence between the second type and the first.</p>
<p>Here is the formal definition of embedding:</p>
<pre class="Agda"><a id="9167" class="Keyword">infix</a> <a id="9173" class="Number">0</a> <a id="9175" href="/19.08/Isomorphism/#9186" class="Record Operator">_≲_</a>
<a id="9179" class="Keyword">record</a> <a id="_≲_"></a><a id="9186" href="/19.08/Isomorphism/#9186" class="Record Operator">_≲_</a> <a id="9190" class="Symbol">(</a><a id="9191" href="plfa.part1.Isomorphism.html#9191" class="Bound">A</a> <a id="9193" href="plfa.part1.Isomorphism.html#9193" class="Bound">B</a> <a id="9195" class="Symbol">:</a> <a id="9197" class="PrimitiveType">Set</a><a id="9200" class="Symbol">)</a> <a id="9202" class="Symbol">:</a> <a id="9204" class="PrimitiveType">Set</a> <a id="9208" class="Keyword">where</a>
<a id="9216" class="Keyword">field</a>
<a id="_≲_.to"></a><a id="9226" href="/19.08/Isomorphism/#9226" class="Field">to</a> <a id="9234" class="Symbol">:</a> <a id="9236" href="plfa.part1.Isomorphism.html#9191" class="Bound">A</a> <a id="9238" class="Symbol">→</a> <a id="9240" href="plfa.part1.Isomorphism.html#9193" class="Bound">B</a>
<a id="_≲_.from"></a><a id="9246" href="/19.08/Isomorphism/#9246" class="Field">from</a> <a id="9254" class="Symbol">:</a> <a id="9256" href="plfa.part1.Isomorphism.html#9193" class="Bound">B</a> <a id="9258" class="Symbol">→</a> <a id="9260" href="plfa.part1.Isomorphism.html#9191" class="Bound">A</a>
<a id="_≲_.from∘to"></a><a id="9266" href="/19.08/Isomorphism/#9266" class="Field">from∘to</a> <a id="9274" class="Symbol">:</a> <a id="9276" class="Symbol">∀</a> <a id="9278" class="Symbol">(</a><a id="9279" href="plfa.part1.Isomorphism.html#9279" class="Bound">x</a> <a id="9281" class="Symbol">:</a> <a id="9283" href="plfa.part1.Isomorphism.html#9191" class="Bound">A</a><a id="9284" class="Symbol">)</a> <a id="9286" class="Symbol">→</a> <a id="9288" class="Field">from</a> <a id="9293" class="Symbol">(</a><a id="9294" class="Field">to</a> <a id="9297" href="plfa.part1.Isomorphism.html#9279" class="Bound">x</a><a id="9298" class="Symbol">)</a> <a id="9300" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="9302" href="plfa.part1.Isomorphism.html#9279" class="Bound">x</a>
<a id="9304" class="Keyword">open</a> <a id="9309" href="/19.08/Isomorphism/#9186" class="Module Operator">_≲_</a>
</pre>
<p>It is the same as an isomorphism, save that it lacks the <code class="language-plaintext highlighter-rouge">to∘from</code> field.
Hence, we know that <code class="language-plaintext highlighter-rouge">from</code> is left-inverse to <code class="language-plaintext highlighter-rouge">to</code>, but not that <code class="language-plaintext highlighter-rouge">from</code>
is right-inverse to <code class="language-plaintext highlighter-rouge">to</code>.</p>
<p>Embedding is reflexive and transitive, but not symmetric. The proofs
are cut down versions of the similar proofs for isomorphism:</p>
<pre class="Agda"><a id="≲-refl"></a><a id="9625" href="/19.08/Isomorphism/#9625" class="Function">≲-refl</a> <a id="9632" class="Symbol">:</a> <a id="9634" class="Symbol">∀</a> <a id="9636" class="Symbol">{</a><a id="9637" href="plfa.part1.Isomorphism.html#9637" class="Bound">A</a> <a id="9639" class="Symbol">:</a> <a id="9641" class="PrimitiveType">Set</a><a id="9644" class="Symbol">}</a> <a id="9646" class="Symbol">→</a> <a id="9648" href="plfa.part1.Isomorphism.html#9637" class="Bound">A</a> <a id="9650" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="9652" href="plfa.part1.Isomorphism.html#9637" class="Bound">A</a>
<a id="9654" href="/19.08/Isomorphism/#9625" class="Function">≲-refl</a> <a id="9661" class="Symbol">=</a>
<a id="9665" class="Keyword">record</a>
<a id="9676" class="Symbol">{</a> <a id="9678" href="/19.08/Isomorphism/#9226" class="Field">to</a> <a id="9686" class="Symbol">=</a> <a id="9688" class="Symbol">λ{</a><a id="9690" href="plfa.part1.Isomorphism.html#9690" class="Bound">x</a> <a id="9692" class="Symbol">→</a> <a id="9694" href="plfa.part1.Isomorphism.html#9690" class="Bound">x</a><a id="9695" class="Symbol">}</a>
<a id="9701" class="Symbol">;</a> <a id="9703" href="/19.08/Isomorphism/#9246" class="Field">from</a> <a id="9711" class="Symbol">=</a> <a id="9713" class="Symbol">λ{</a><a id="9715" href="plfa.part1.Isomorphism.html#9715" class="Bound">y</a> <a id="9717" class="Symbol">→</a> <a id="9719" href="plfa.part1.Isomorphism.html#9715" class="Bound">y</a><a id="9720" class="Symbol">}</a>
<a id="9726" class="Symbol">;</a> <a id="9728" href="/19.08/Isomorphism/#9266" class="Field">from∘to</a> <a id="9736" class="Symbol">=</a> <a id="9738" class="Symbol">λ{</a><a id="9740" href="plfa.part1.Isomorphism.html#9740" class="Bound">x</a> <a id="9742" class="Symbol">→</a> <a id="9744" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="9748" class="Symbol">}</a>
<a id="9754" class="Symbol">}</a>
<a id="≲-trans"></a><a id="9757" href="/19.08/Isomorphism/#9757" class="Function">≲-trans</a> <a id="9765" class="Symbol">:</a> <a id="9767" class="Symbol">∀</a> <a id="9769" class="Symbol">{</a><a id="9770" href="plfa.part1.Isomorphism.html#9770" class="Bound">A</a> <a id="9772" href="plfa.part1.Isomorphism.html#9772" class="Bound">B</a> <a id="9774" href="plfa.part1.Isomorphism.html#9774" class="Bound">C</a> <a id="9776" class="Symbol">:</a> <a id="9778" class="PrimitiveType">Set</a><a id="9781" class="Symbol">}</a> <a id="9783" class="Symbol">→</a> <a id="9785" href="plfa.part1.Isomorphism.html#9770" class="Bound">A</a> <a id="9787" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="9789" href="plfa.part1.Isomorphism.html#9772" class="Bound">B</a> <a id="9791" class="Symbol">→</a> <a id="9793" href="plfa.part1.Isomorphism.html#9772" class="Bound">B</a> <a id="9795" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="9797" href="plfa.part1.Isomorphism.html#9774" class="Bound">C</a> <a id="9799" class="Symbol">→</a> <a id="9801" href="plfa.part1.Isomorphism.html#9770" class="Bound">A</a> <a id="9803" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="9805" href="plfa.part1.Isomorphism.html#9774" class="Bound">C</a>
<a id="9807" href="/19.08/Isomorphism/#9757" class="Function">≲-trans</a> <a id="9815" href="plfa.part1.Isomorphism.html#9815" class="Bound">A≲B</a> <a id="9819" href="plfa.part1.Isomorphism.html#9819" class="Bound">B≲C</a> <a id="9823" class="Symbol">=</a>
<a id="9827" class="Keyword">record</a>
<a id="9838" class="Symbol">{</a> <a id="9840" href="/19.08/Isomorphism/#9226" class="Field">to</a> <a id="9848" class="Symbol">=</a> <a id="9850" class="Symbol">λ{</a><a id="9852" href="plfa.part1.Isomorphism.html#9852" class="Bound">x</a> <a id="9854" class="Symbol">→</a> <a id="9856" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="9861" href="plfa.part1.Isomorphism.html#9819" class="Bound">B≲C</a> <a id="9865" class="Symbol">(</a><a id="9866" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="9871" href="plfa.part1.Isomorphism.html#9815" class="Bound">A≲B</a> <a id="9875" href="plfa.part1.Isomorphism.html#9852" class="Bound">x</a><a id="9876" class="Symbol">)}</a>
<a id="9883" class="Symbol">;</a> <a id="9885" href="/19.08/Isomorphism/#9246" class="Field">from</a> <a id="9893" class="Symbol">=</a> <a id="9895" class="Symbol">λ{</a><a id="9897" href="plfa.part1.Isomorphism.html#9897" class="Bound">y</a> <a id="9899" class="Symbol">→</a> <a id="9901" href="plfa.part1.Isomorphism.html#9246" class="Field">from</a> <a id="9906" href="plfa.part1.Isomorphism.html#9815" class="Bound">A≲B</a> <a id="9910" class="Symbol">(</a><a id="9911" href="plfa.part1.Isomorphism.html#9246" class="Field">from</a> <a id="9916" href="plfa.part1.Isomorphism.html#9819" class="Bound">B≲C</a> <a id="9920" href="plfa.part1.Isomorphism.html#9897" class="Bound">y</a><a id="9921" class="Symbol">)}</a>
<a id="9928" class="Symbol">;</a> <a id="9930" href="/19.08/Isomorphism/#9266" class="Field">from∘to</a> <a id="9938" class="Symbol">=</a> <a id="9940" class="Symbol">λ{</a><a id="9942" href="plfa.part1.Isomorphism.html#9942" class="Bound">x</a> <a id="9944" class="Symbol">→</a>
<a id="9954" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="9970" href="/19.08/Isomorphism/#9246" class="Field">from</a> <a id="9975" href="plfa.part1.Isomorphism.html#9815" class="Bound">A≲B</a> <a id="9979" class="Symbol">(</a><a id="9980" href="plfa.part1.Isomorphism.html#9246" class="Field">from</a> <a id="9985" href="plfa.part1.Isomorphism.html#9819" class="Bound">B≲C</a> <a id="9989" class="Symbol">(</a><a id="9990" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="9993" href="plfa.part1.Isomorphism.html#9819" class="Bound">B≲C</a> <a id="9997" class="Symbol">(</a><a id="9998" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="10001" href="plfa.part1.Isomorphism.html#9815" class="Bound">A≲B</a> <a id="10005" href="plfa.part1.Isomorphism.html#9942" class="Bound">x</a><a id="10006" class="Symbol">)))</a>
<a id="10018" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="10021" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="10026" class="Symbol">(</a><a id="10027" href="/19.08/Isomorphism/#9246" class="Field">from</a> <a id="10032" href="plfa.part1.Isomorphism.html#9815" class="Bound">A≲B</a><a id="10035" class="Symbol">)</a> <a id="10037" class="Symbol">(</a><a id="10038" href="plfa.part1.Isomorphism.html#9266" class="Field">from∘to</a> <a id="10046" href="plfa.part1.Isomorphism.html#9819" class="Bound">B≲C</a> <a id="10050" class="Symbol">(</a><a id="10051" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="10054" href="plfa.part1.Isomorphism.html#9815" class="Bound">A≲B</a> <a id="10058" href="plfa.part1.Isomorphism.html#9942" class="Bound">x</a><a id="10059" class="Symbol">))</a> <a id="10062" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="10074" href="/19.08/Isomorphism/#9246" class="Field">from</a> <a id="10079" href="plfa.part1.Isomorphism.html#9815" class="Bound">A≲B</a> <a id="10083" class="Symbol">(</a><a id="10084" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="10087" href="plfa.part1.Isomorphism.html#9815" class="Bound">A≲B</a> <a id="10091" href="plfa.part1.Isomorphism.html#9942" class="Bound">x</a><a id="10092" class="Symbol">)</a>
<a id="10102" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="10105" href="/19.08/Isomorphism/#9266" class="Field">from∘to</a> <a id="10113" href="plfa.part1.Isomorphism.html#9815" class="Bound">A≲B</a> <a id="10117" href="plfa.part1.Isomorphism.html#9942" class="Bound">x</a> <a id="10119" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="10131" href="/19.08/Isomorphism/#9942" class="Bound">x</a>
<a id="10141" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a><a id="10142" class="Symbol">}</a>
<a id="10149" class="Symbol">}</a>
</pre>
<p>It is also easy to see that if two types embed in each other, and the
embedding functions correspond, then they are isomorphic. This is a
weak form of anti-symmetry:</p>
<pre class="Agda"><a id="≲-antisym"></a><a id="10327" href="/19.08/Isomorphism/#10327" class="Function">≲-antisym</a> <a id="10337" class="Symbol">:</a> <a id="10339" class="Symbol">∀</a> <a id="10341" class="Symbol">{</a><a id="10342" href="plfa.part1.Isomorphism.html#10342" class="Bound">A</a> <a id="10344" href="plfa.part1.Isomorphism.html#10344" class="Bound">B</a> <a id="10346" class="Symbol">:</a> <a id="10348" class="PrimitiveType">Set</a><a id="10351" class="Symbol">}</a>
<a id="10355" class="Symbol">→</a> <a id="10357" class="Symbol">(</a><a id="10358" href="/19.08/Isomorphism/#10358" class="Bound">A≲B</a> <a id="10362" class="Symbol">:</a> <a id="10364" href="plfa.part1.Isomorphism.html#10342" class="Bound">A</a> <a id="10366" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="10368" href="plfa.part1.Isomorphism.html#10344" class="Bound">B</a><a id="10369" class="Symbol">)</a>
<a id="10373" class="Symbol">→</a> <a id="10375" class="Symbol">(</a><a id="10376" href="/19.08/Isomorphism/#10376" class="Bound">B≲A</a> <a id="10380" class="Symbol">:</a> <a id="10382" href="plfa.part1.Isomorphism.html#10344" class="Bound">B</a> <a id="10384" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="10386" href="plfa.part1.Isomorphism.html#10342" class="Bound">A</a><a id="10387" class="Symbol">)</a>
<a id="10391" class="Symbol">→</a> <a id="10393" class="Symbol">(</a><a id="10394" href="/19.08/Isomorphism/#9226" class="Field">to</a> <a id="10397" href="plfa.part1.Isomorphism.html#10358" class="Bound">A≲B</a> <a id="10401" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="10403" href="plfa.part1.Isomorphism.html#9246" class="Field">from</a> <a id="10408" href="plfa.part1.Isomorphism.html#10376" class="Bound">B≲A</a><a id="10411" class="Symbol">)</a>
<a id="10415" class="Symbol">→</a> <a id="10417" class="Symbol">(</a><a id="10418" href="/19.08/Isomorphism/#9246" class="Field">from</a> <a id="10423" href="plfa.part1.Isomorphism.html#10358" class="Bound">A≲B</a> <a id="10427" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="10429" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="10432" href="plfa.part1.Isomorphism.html#10376" class="Bound">B≲A</a><a id="10435" class="Symbol">)</a>
<a id="10441" class="Comment">-------------------</a>
<a id="10463" class="Symbol">→</a> <a id="10465" href="/19.08/Isomorphism/#10342" class="Bound">A</a> <a id="10467" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="10469" href="plfa.part1.Isomorphism.html#10344" class="Bound">B</a>
<a id="10471" href="/19.08/Isomorphism/#10327" class="Function">≲-antisym</a> <a id="10481" href="plfa.part1.Isomorphism.html#10481" class="Bound">A≲B</a> <a id="10485" href="plfa.part1.Isomorphism.html#10485" class="Bound">B≲A</a> <a id="10489" href="plfa.part1.Isomorphism.html#10489" class="Bound">to≡from</a> <a id="10497" href="plfa.part1.Isomorphism.html#10497" class="Bound">from≡to</a> <a id="10505" class="Symbol">=</a>
<a id="10509" class="Keyword">record</a>
<a id="10520" class="Symbol">{</a> <a id="10522" href="/19.08/Isomorphism/#4405" class="Field">to</a> <a id="10530" class="Symbol">=</a> <a id="10532" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="10535" href="plfa.part1.Isomorphism.html#10481" class="Bound">A≲B</a>
<a id="10543" class="Symbol">;</a> <a id="10545" href="/19.08/Isomorphism/#4422" class="Field">from</a> <a id="10553" class="Symbol">=</a> <a id="10555" href="plfa.part1.Isomorphism.html#9246" class="Field">from</a> <a id="10560" href="plfa.part1.Isomorphism.html#10481" class="Bound">A≲B</a>
<a id="10568" class="Symbol">;</a> <a id="10570" href="/19.08/Isomorphism/#4439" class="Field">from∘to</a> <a id="10578" class="Symbol">=</a> <a id="10580" href="plfa.part1.Isomorphism.html#9266" class="Field">from∘to</a> <a id="10588" href="plfa.part1.Isomorphism.html#10481" class="Bound">A≲B</a>
<a id="10596" class="Symbol">;</a> <a id="10598" href="/19.08/Isomorphism/#4481" class="Field">to∘from</a> <a id="10606" class="Symbol">=</a> <a id="10608" class="Symbol">λ{</a><a id="10610" href="plfa.part1.Isomorphism.html#10610" class="Bound">y</a> <a id="10612" class="Symbol">→</a>
<a id="10622" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="10638" href="/19.08/Isomorphism/#9226" class="Field">to</a> <a id="10641" href="plfa.part1.Isomorphism.html#10481" class="Bound">A≲B</a> <a id="10645" class="Symbol">(</a><a id="10646" href="plfa.part1.Isomorphism.html#9246" class="Field">from</a> <a id="10651" href="plfa.part1.Isomorphism.html#10481" class="Bound">A≲B</a> <a id="10655" href="plfa.part1.Isomorphism.html#10610" class="Bound">y</a><a id="10656" class="Symbol">)</a>
<a id="10666" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="10669" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="10674" class="Symbol">(</a><a id="10675" href="/19.08/Isomorphism/#9226" class="Field">to</a> <a id="10678" href="plfa.part1.Isomorphism.html#10481" class="Bound">A≲B</a><a id="10681" class="Symbol">)</a> <a id="10683" class="Symbol">(</a><a id="10684" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html#1308" class="Function">cong-app</a> <a id="10693" href="plfa.part1.Isomorphism.html#10497" class="Bound">from≡to</a> <a id="10701" href="plfa.part1.Isomorphism.html#10610" class="Bound">y</a><a id="10702" class="Symbol">)</a> <a id="10704" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="10716" href="/19.08/Isomorphism/#9226" class="Field">to</a> <a id="10719" href="plfa.part1.Isomorphism.html#10481" class="Bound">A≲B</a> <a id="10723" class="Symbol">(</a><a id="10724" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="10727" href="plfa.part1.Isomorphism.html#10485" class="Bound">B≲A</a> <a id="10731" href="plfa.part1.Isomorphism.html#10610" class="Bound">y</a><a id="10732" class="Symbol">)</a>
<a id="10742" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="10745" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html#1308" class="Function">cong-app</a> <a id="10754" href="/19.08/Isomorphism/#10489" class="Bound">to≡from</a> <a id="10762" class="Symbol">(</a><a id="10763" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="10766" href="plfa.part1.Isomorphism.html#10485" class="Bound">B≲A</a> <a id="10770" href="plfa.part1.Isomorphism.html#10610" class="Bound">y</a><a id="10771" class="Symbol">)</a> <a id="10773" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="10785" href="/19.08/Isomorphism/#9246" class="Field">from</a> <a id="10790" href="plfa.part1.Isomorphism.html#10485" class="Bound">B≲A</a> <a id="10794" class="Symbol">(</a><a id="10795" href="plfa.part1.Isomorphism.html#9226" class="Field">to</a> <a id="10798" href="plfa.part1.Isomorphism.html#10485" class="Bound">B≲A</a> <a id="10802" href="plfa.part1.Isomorphism.html#10610" class="Bound">y</a><a id="10803" class="Symbol">)</a>
<a id="10813" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="10816" href="/19.08/Isomorphism/#9266" class="Field">from∘to</a> <a id="10824" href="plfa.part1.Isomorphism.html#10485" class="Bound">B≲A</a> <a id="10828" href="plfa.part1.Isomorphism.html#10610" class="Bound">y</a> <a id="10830" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="10842" href="/19.08/Isomorphism/#10610" class="Bound">y</a>
<a id="10852" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a><a id="10853" class="Symbol">}</a>
<a id="10859" class="Symbol">}</a>
</pre>
<p>The first three components are copied from the embedding, while the
last combines the left inverse of <code class="language-plaintext highlighter-rouge">B ≲ A</code> with the equivalences of
the <code class="language-plaintext highlighter-rouge">to</code> and <code class="language-plaintext highlighter-rouge">from</code> components from the two embeddings to obtain
the right inverse of the isomorphism.</p>
<h2 id="equational-reasoning-for-embedding">Equational reasoning for embedding</h2>
<p>We can also support tabular reasoning for embedding,
analogous to that used for isomorphism:</p>
<pre class="Agda"><a id="11241" class="Keyword">module</a> <a id="≲-Reasoning"></a><a id="11248" href="/19.08/Isomorphism/#11248" class="Module">≲-Reasoning</a> <a id="11260" class="Keyword">where</a>
<a id="11269" class="Keyword">infix</a> <a id="11276" class="Number">1</a> <a id="11278" href="/19.08/Isomorphism/#11324" class="Function Operator">≲-begin_</a>
<a id="11289" class="Keyword">infixr</a> <a id="11296" class="Number">2</a> <a id="11298" href="/19.08/Isomorphism/#11408" class="Function Operator">_≲⟨_⟩_</a>
<a id="11307" class="Keyword">infix</a> <a id="11314" class="Number">3</a> <a id="11316" href="/19.08/Isomorphism/#11527" class="Function Operator">_≲-∎</a>
<a id="≲-Reasoning.≲-begin_"></a><a id="11324" href="/19.08/Isomorphism/#11324" class="Function Operator">≲-begin_</a> <a id="11333" class="Symbol">:</a> <a id="11335" class="Symbol">∀</a> <a id="11337" class="Symbol">{</a><a id="11338" href="plfa.part1.Isomorphism.html#11338" class="Bound">A</a> <a id="11340" href="plfa.part1.Isomorphism.html#11340" class="Bound">B</a> <a id="11342" class="Symbol">:</a> <a id="11344" class="PrimitiveType">Set</a><a id="11347" class="Symbol">}</a>
<a id="11353" class="Symbol">→</a> <a id="11355" href="/19.08/Isomorphism/#11338" class="Bound">A</a> <a id="11357" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="11359" href="plfa.part1.Isomorphism.html#11340" class="Bound">B</a>
<a id="11367" class="Comment">-----</a>
<a id="11377" class="Symbol">→</a> <a id="11379" href="/19.08/Isomorphism/#11338" class="Bound">A</a> <a id="11381" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="11383" href="plfa.part1.Isomorphism.html#11340" class="Bound">B</a>
<a id="11387" href="/19.08/Isomorphism/#11324" class="Function Operator">≲-begin</a> <a id="11395" href="plfa.part1.Isomorphism.html#11395" class="Bound">A≲B</a> <a id="11399" class="Symbol">=</a> <a id="11401" href="plfa.part1.Isomorphism.html#11395" class="Bound">A≲B</a>
<a id="≲-Reasoning._≲⟨_⟩_"></a><a id="11408" href="/19.08/Isomorphism/#11408" class="Function Operator">_≲⟨_⟩_</a> <a id="11415" class="Symbol">:</a> <a id="11417" class="Symbol">∀</a> <a id="11419" class="Symbol">(</a><a id="11420" href="plfa.part1.Isomorphism.html#11420" class="Bound">A</a> <a id="11422" class="Symbol">:</a> <a id="11424" class="PrimitiveType">Set</a><a id="11427" class="Symbol">)</a> <a id="11429" class="Symbol">{</a><a id="11430" href="plfa.part1.Isomorphism.html#11430" class="Bound">B</a> <a id="11432" href="plfa.part1.Isomorphism.html#11432" class="Bound">C</a> <a id="11434" class="Symbol">:</a> <a id="11436" class="PrimitiveType">Set</a><a id="11439" class="Symbol">}</a>
<a id="11445" class="Symbol">→</a> <a id="11447" href="/19.08/Isomorphism/#11420" class="Bound">A</a> <a id="11449" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="11451" href="plfa.part1.Isomorphism.html#11430" class="Bound">B</a>
<a id="11457" class="Symbol">→</a> <a id="11459" href="/19.08/Isomorphism/#11430" class="Bound">B</a> <a id="11461" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="11463" href="plfa.part1.Isomorphism.html#11432" class="Bound">C</a>
<a id="11471" class="Comment">-----</a>
<a id="11481" class="Symbol">→</a> <a id="11483" href="/19.08/Isomorphism/#11420" class="Bound">A</a> <a id="11485" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="11487" href="plfa.part1.Isomorphism.html#11432" class="Bound">C</a>
<a id="11491" href="/19.08/Isomorphism/#11491" class="Bound">A</a> <a id="11493" href="plfa.part1.Isomorphism.html#11408" class="Function Operator">≲⟨</a> <a id="11496" href="plfa.part1.Isomorphism.html#11496" class="Bound">A≲B</a> <a id="11500" href="plfa.part1.Isomorphism.html#11408" class="Function Operator">⟩</a> <a id="11502" href="plfa.part1.Isomorphism.html#11502" class="Bound">B≲C</a> <a id="11506" class="Symbol">=</a> <a id="11508" href="plfa.part1.Isomorphism.html#9757" class="Function">≲-trans</a> <a id="11516" href="plfa.part1.Isomorphism.html#11496" class="Bound">A≲B</a> <a id="11520" href="plfa.part1.Isomorphism.html#11502" class="Bound">B≲C</a>
<a id="≲-Reasoning._≲-∎"></a><a id="11527" href="/19.08/Isomorphism/#11527" class="Function Operator">_≲-∎</a> <a id="11532" class="Symbol">:</a> <a id="11534" class="Symbol">∀</a> <a id="11536" class="Symbol">(</a><a id="11537" href="plfa.part1.Isomorphism.html#11537" class="Bound">A</a> <a id="11539" class="Symbol">:</a> <a id="11541" class="PrimitiveType">Set</a><a id="11544" class="Symbol">)</a>
<a id="11552" class="Comment">-----</a>
<a id="11562" class="Symbol">→</a> <a id="11564" href="/19.08/Isomorphism/#11537" class="Bound">A</a> <a id="11566" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="11568" href="plfa.part1.Isomorphism.html#11537" class="Bound">A</a>
<a id="11572" href="/19.08/Isomorphism/#11572" class="Bound">A</a> <a id="11574" href="plfa.part1.Isomorphism.html#11527" class="Function Operator">≲-∎</a> <a id="11578" class="Symbol">=</a> <a id="11580" href="plfa.part1.Isomorphism.html#9625" class="Function">≲-refl</a>
<a id="11588" class="Keyword">open</a> <a id="11593" href="/19.08/Isomorphism/#11248" class="Module">≲-Reasoning</a>
</pre>
<h4 id="exercise--implies--practice">Exercise <code class="language-plaintext highlighter-rouge">≃-implies-≲</code> (practice)</h4>
<p>Show that every isomorphism implies an embedding.</p>
<pre class="Agda"><a id="11704" class="Keyword">postulate</a>
<a id="≃-implies-≲"></a><a id="11716" href="/19.08/Isomorphism/#11716" class="Postulate">≃-implies-≲</a> <a id="11728" class="Symbol">:</a> <a id="11730" class="Symbol">∀</a> <a id="11732" class="Symbol">{</a><a id="11733" href="plfa.part1.Isomorphism.html#11733" class="Bound">A</a> <a id="11735" href="plfa.part1.Isomorphism.html#11735" class="Bound">B</a> <a id="11737" class="Symbol">:</a> <a id="11739" class="PrimitiveType">Set</a><a id="11742" class="Symbol">}</a>
<a id="11748" class="Symbol">→</a> <a id="11750" href="/19.08/Isomorphism/#11733" class="Bound">A</a> <a id="11752" href="plfa.part1.Isomorphism.html#4365" class="Record Operator">≃</a> <a id="11754" href="plfa.part1.Isomorphism.html#11735" class="Bound">B</a>
<a id="11762" class="Comment">-----</a>
<a id="11772" class="Symbol">→</a> <a id="11774" href="/19.08/Isomorphism/#11733" class="Bound">A</a> <a id="11776" href="plfa.part1.Isomorphism.html#9186" class="Record Operator">≲</a> <a id="11778" href="plfa.part1.Isomorphism.html#11735" class="Bound">B</a>
</pre>
<pre class="Agda"><a id="11789" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="iff">Exercise <code class="language-plaintext highlighter-rouge">_⇔_</code> (practice)</h4>
<p>Define equivalence of propositions (also known as “if and only if”) as follows:</p>
<pre class="Agda"><a id="11940" class="Keyword">record</a> <a id="_⇔_"></a><a id="11947" href="/19.08/Isomorphism/#11947" class="Record Operator">_⇔_</a> <a id="11951" class="Symbol">(</a><a id="11952" href="plfa.part1.Isomorphism.html#11952" class="Bound">A</a> <a id="11954" href="plfa.part1.Isomorphism.html#11954" class="Bound">B</a> <a id="11956" class="Symbol">:</a> <a id="11958" class="PrimitiveType">Set</a><a id="11961" class="Symbol">)</a> <a id="11963" class="Symbol">:</a> <a id="11965" class="PrimitiveType">Set</a> <a id="11969" class="Keyword">where</a>
<a id="11977" class="Keyword">field</a>
<a id="_⇔_.to"></a><a id="11987" href="/19.08/Isomorphism/#11987" class="Field">to</a> <a id="11992" class="Symbol">:</a> <a id="11994" href="plfa.part1.Isomorphism.html#11952" class="Bound">A</a> <a id="11996" class="Symbol">→</a> <a id="11998" href="plfa.part1.Isomorphism.html#11954" class="Bound">B</a>
<a id="_⇔_.from"></a><a id="12004" href="/19.08/Isomorphism/#12004" class="Field">from</a> <a id="12009" class="Symbol">:</a> <a id="12011" href="plfa.part1.Isomorphism.html#11954" class="Bound">B</a> <a id="12013" class="Symbol">→</a> <a id="12015" href="plfa.part1.Isomorphism.html#11952" class="Bound">A</a>
</pre>
<p>Show that equivalence is reflexive, symmetric, and transitive.</p>
<pre class="Agda"><a id="12089" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="Bin-embedding">Exercise <code class="language-plaintext highlighter-rouge">Bin-embedding</code> (stretch)</h4>
<p>Recall that Exercises
<a href="/19.08/Naturals/#Bin">Bin</a> and
<a href="/19.08/Induction/#Bin-laws">Bin-laws</a>
define a datatype of bitstrings representing natural numbers:</p>
<pre class="Agda"><a id="12358" class="Keyword">data</a> <a id="Bin"></a><a id="12363" href="/19.08/Isomorphism/#12363" class="Datatype">Bin</a> <a id="12367" class="Symbol">:</a> <a id="12369" class="PrimitiveType">Set</a> <a id="12373" class="Keyword">where</a>
<a id="Bin.nil"></a><a id="12381" href="/19.08/Isomorphism/#12381" class="InductiveConstructor">nil</a> <a id="12385" class="Symbol">:</a> <a id="12387" href="plfa.part1.Isomorphism.html#12363" class="Datatype">Bin</a>
<a id="Bin.x0_"></a><a id="12393" href="/19.08/Isomorphism/#12393" class="InductiveConstructor Operator">x0_</a> <a id="12397" class="Symbol">:</a> <a id="12399" href="plfa.part1.Isomorphism.html#12363" class="Datatype">Bin</a> <a id="12403" class="Symbol">→</a> <a id="12405" href="plfa.part1.Isomorphism.html#12363" class="Datatype">Bin</a>
<a id="Bin.x1_"></a><a id="12411" href="/19.08/Isomorphism/#12411" class="InductiveConstructor Operator">x1_</a> <a id="12415" class="Symbol">:</a> <a id="12417" href="plfa.part1.Isomorphism.html#12363" class="Datatype">Bin</a> <a id="12421" class="Symbol">→</a> <a id="12423" href="plfa.part1.Isomorphism.html#12363" class="Datatype">Bin</a>
</pre>
<p>And ask you to define the following functions</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>to : ℕ → Bin
from : Bin → ℕ
</code></pre></div></div>
<p>which satisfy the following property:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>from (to n) ≡ n
</code></pre></div></div>
<p>Using the above, establish that there is an embedding of <code class="language-plaintext highlighter-rouge">ℕ</code> into <code class="language-plaintext highlighter-rouge">Bin</code>.</p>
<pre class="Agda"><a id="12652" class="Comment">-- Your code goes here</a>
</pre>
<p>Why do <code class="language-plaintext highlighter-rouge">to</code> and <code class="language-plaintext highlighter-rouge">from</code> not form an isomorphism?</p>
<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="12837" class="Keyword">import</a> <a id="12844" href="https://agda.github.io/agda-stdlib/v1.1/Function.html" class="Module">Function</a> <a id="12853" class="Keyword">using</a> <a id="12859" class="Symbol">(</a><a id="12860" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">_∘_</a><a id="12863" class="Symbol">)</a>
<a id="12865" class="Keyword">import</a> <a id="12872" href="https://agda.github.io/agda-stdlib/v1.1/Function.Inverse.html" class="Module">Function.Inverse</a> <a id="12889" class="Keyword">using</a> <a id="12895" class="Symbol">(</a><a id="12896" href="https://agda.github.io/agda-stdlib/v1.1/Function.Inverse.html#2229" class="Function Operator">_↔_</a><a id="12899" class="Symbol">)</a>
<a id="12901" class="Keyword">import</a> <a id="12908" href="https://agda.github.io/agda-stdlib/v1.1/Function.LeftInverse.html" class="Module">Function.LeftInverse</a> <a id="12929" class="Keyword">using</a> <a id="12935" class="Symbol">(</a><a id="12936" href="https://agda.github.io/agda-stdlib/v1.1/Function.LeftInverse.html#2682" class="Function Operator">_↞_</a><a id="12939" class="Symbol">)</a>
</pre>
<p>The standard library <code class="language-plaintext highlighter-rouge">_↔_</code> and <code class="language-plaintext highlighter-rouge">_↞_</code> correspond to our <code class="language-plaintext highlighter-rouge">_≃_</code> and
<code class="language-plaintext highlighter-rouge">_≲_</code>, respectively, but those in the standard library are less
convenient, since they depend on a nested record structure and are
parameterised with regard 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+2218 RING OPERATOR (\o, \circ, \comp)
λ U+03BB GREEK SMALL LETTER LAMBDA (\lambda, \Gl)
≃ U+2243 ASYMPTOTICALLY EQUAL TO (\~-)
≲ U+2272 LESS-THAN OR EQUIVALENT TO (\&lt;~)
⇔ U+21D4 LEFT RIGHT DOUBLE ARROW (\&lt;=&gt;)
</code></pre></div></div>
</div>
<p style="text-align:center;">
<a alt="Previous chapter" href="/19.08/Equality/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part1/Isomorphism.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/19.08/Connectives/">Next</a>
</p>
</article>
</div>
</main><footer class="site-footer h-card">
<data class="u-url" href="/19.08/"></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="/19.08/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="/19.08/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="/19.08/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 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="/19.08/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="/19.08/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="/19.08/assets/jquery.js"></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="/19.08/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