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

619 lines
154 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>Assignment5: PUC Assignment 5 | 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="Assignment5: PUC Assignment 5" />
<meta property="og:locale" content="en_US" />
<meta name="description" content="Programming Language Foundations in Agda" />
<meta property="og:description" content="Programming Language Foundations in Agda" />
<link rel="canonical" href="https://plfa.github.io/20.07/PUC/2019/Assignment5/" />
<meta property="og:url" content="https://plfa.github.io/20.07/PUC/2019/Assignment5/" />
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
<script type="application/ld+json">
{"url":"https://plfa.github.io/20.07/PUC/2019/Assignment5/","headline":"Assignment5: PUC Assignment 5","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
<!-- End Jekyll SEO tag -->
<link rel="stylesheet" href="/20.07/assets/main.css"></head>
<body><header class="site-header" role="banner">
<div class="wrapper">
<a class="site-title" href="/20.07/">Programming Language Foundations in Agda
</a>
<nav class="site-nav">
<span class="menu-icon">
<svg viewBox="0 0 18 15" width="18px" height="15px">
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
</svg>
</span>
<div class="trigger">
<a class="page-link" href="/20.07/">The Book</a>
<a class="page-link" href="/20.07/Announcements/">Announcements</a>
<a class="page-link" href="/20.07/GettingStarted/">Getting Started</a>
<a class="page-link" href="/20.07/Citing/">Citing</a>
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
</div>
</nav>
</div>
</header>
<main class="page-content" aria-label="Content">
<div class="wrapper">
<article class="post">
<header class="post-header">
<h1 class="post-title">Assignment5: PUC Assignment 5</h1>
</header>
<p style="text-align:center;">
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/courses/puc/2019/Assignment5.lagda.md">Source</a>
</p>
<div class="post-content">
<pre class="Agda"><a id="110" class="Keyword">module</a> <a id="117" href="/20.07/PUC/2019/Assignment5/" class="Module">Assignment5</a> <a id="129" class="Keyword">where</a>
</pre>
<h2 id="your-name-and-email-goes-here">YOUR NAME AND EMAIL GOES HERE</h2>
<h2 id="introduction">Introduction</h2>
<p>You must do <em>all</em> the exercises labelled “(recommended)”.</p>
<p>Exercises labelled “(stretch)” are there to provide an extra challenge.
You don’t need to do all of these, but should attempt at least a few.</p>
<p>Exercises without a label are optional, and may be done if you want
some extra practice.</p>
<p>Please ensure your files execute correctly under Agda!</p>
<p><strong>IMPORTANT</strong> For ease of marking, when modifying the given code please write</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- begin
-- end
</code></pre></div></div>
<p>before and after code you add, to indicate your changes.</p>
<h2 id="imports">Imports</h2>
<pre class="Agda"><a id="719" class="Keyword">import</a> <a id="726" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="764" class="Symbol">as</a> <a id="767" class="Module">Eq</a>
<a id="770" class="Keyword">open</a> <a id="775" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Eq</a> <a id="778" class="Keyword">using</a> <a id="784" class="Symbol">(</a><a id="785" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="788" class="Symbol">;</a> <a id="790" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="794" class="Symbol">;</a> <a id="796" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a><a id="799" class="Symbol">;</a> <a id="801" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#984" class="Function">trans</a><a id="806" class="Symbol">;</a> <a id="808" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a><a id="812" class="Symbol">;</a> <a id="814" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html#1436" class="Function">cong₂</a><a id="819" class="Symbol">;</a> <a id="821" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#799" class="Function Operator">_≢_</a><a id="824" class="Symbol">)</a>
<a id="826" class="Keyword">open</a> <a id="831" class="Keyword">import</a> <a id="838" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html" class="Module">Data.Empty</a> <a id="849" class="Keyword">using</a> <a id="855" class="Symbol">(</a><a id="856" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a><a id="857" class="Symbol">;</a> <a id="859" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a><a id="865" class="Symbol">)</a>
<a id="867" class="Keyword">open</a> <a id="872" class="Keyword">import</a> <a id="879" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="888" class="Keyword">using</a> <a id="894" class="Symbol">(</a><a id="895" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="896" class="Symbol">;</a> <a id="898" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="902" class="Symbol">;</a> <a id="904" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a><a id="907" class="Symbol">;</a> <a id="909" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a><a id="912" class="Symbol">;</a> <a id="914" href="Agda.Builtin.Nat.html#501" class="Primitive Operator">_*_</a><a id="917" class="Symbol">)</a>
<a id="919" class="Keyword">open</a> <a id="924" class="Keyword">import</a> <a id="931" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html" class="Module">Data.Product</a> <a id="944" class="Keyword">using</a> <a id="950" class="Symbol">(</a><a id="951" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">_×_</a><a id="954" class="Symbol">;</a> <a id="956" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1364" class="Function">∃</a><a id="957" class="Symbol">;</a> <a id="959" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃-syntax</a><a id="967" class="Symbol">)</a> <a id="969" class="Keyword">renaming</a> <a id="978" class="Symbol">(</a><a id="979" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">_,_</a> <a id="983" class="Symbol">to</a> <a id="986" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨_,_⟩</a><a id="991" class="Symbol">)</a>
<a id="993" class="Keyword">open</a> <a id="998" class="Keyword">import</a> <a id="1005" href="https://agda.github.io/agda-stdlib/v1.1/Data.String.html" class="Module">Data.String</a> <a id="1017" class="Keyword">using</a> <a id="1023" class="Symbol">(</a><a id="1024" href="Agda.Builtin.String.html#206" class="Postulate">String</a><a id="1030" class="Symbol">;</a> <a id="1032" href="https://agda.github.io/agda-stdlib/v1.1/Data.String.Properties.html#2569" class="Function Operator">_≟_</a><a id="1035" class="Symbol">)</a>
<a id="1037" class="Keyword">open</a> <a id="1042" class="Keyword">import</a> <a id="1049" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="1066" class="Keyword">using</a> <a id="1072" class="Symbol">(</a><a id="1073" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬_</a><a id="1075" class="Symbol">;</a> <a id="1077" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a><a id="1080" class="Symbol">;</a> <a id="1082" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a><a id="1085" class="Symbol">;</a> <a id="1087" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a><a id="1089" class="Symbol">)</a>
</pre>
<h2 id="inference">Inference</h2>
<pre class="Agda"><a id="1115" class="Keyword">module</a> <a id="Inference"></a><a id="1122" href="/20.07/PUC/2019/Assignment5/#1122" class="Module">Inference</a> <a id="1132" class="Keyword">where</a>
</pre>
<p>Remember to indent all code by two spaces.</p>
<h3 id="imports-1">Imports</h3>
<pre class="Agda"> <a id="1206" class="Keyword">import</a> <a id="1213" href="/20.07/More/" class="Module">plfa.part2.More</a> <a id="1229" class="Symbol">as</a> <a id="1232" class="Module">DB</a>
</pre>
<h3 id="syntax">Syntax</h3>
<pre class="Agda"> <a id="1258" class="Keyword">infix</a> <a id="1266" class="Number">4</a> <a id="1269" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">_∋_⦂_</a>
<a id="1277" class="Keyword">infix</a> <a id="1285" class="Number">4</a> <a id="1288" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">_⊢_↑_</a>
<a id="1296" class="Keyword">infix</a> <a id="1304" class="Number">4</a> <a id="1307" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">_⊢_↓_</a>
<a id="1315" class="Keyword">infixl</a> <a id="1323" class="Number">5</a> <a id="1326" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">_,_⦂_</a>
<a id="1335" class="Keyword">infixr</a> <a id="1343" class="Number">7</a> <a id="1346" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">_⇒_</a>
<a id="1353" class="Keyword">infix</a> <a id="1361" class="Number">5</a> <a id="1364" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">ƛ_⇒_</a>
<a id="1371" class="Keyword">infix</a> <a id="1379" class="Number">5</a> <a id="1382" href="/20.07/PUC/2019/Assignment5/#2157" class="InductiveConstructor Operator">μ_⇒_</a>
<a id="1389" class="Keyword">infix</a> <a id="1397" class="Number">6</a> <a id="1400" href="/20.07/PUC/2019/Assignment5/#2207" class="InductiveConstructor Operator">_↑</a>
<a id="1405" class="Keyword">infix</a> <a id="1413" class="Number">6</a> <a id="1416" href="/20.07/PUC/2019/Assignment5/#1886" class="InductiveConstructor Operator">_↓_</a>
<a id="1422" class="Keyword">infixl</a> <a id="1430" class="Number">7</a> <a id="1433" href="/20.07/PUC/2019/Assignment5/#3036" class="InductiveConstructor Operator">_·_</a>
<a id="1439" class="Keyword">infix</a> <a id="1447" class="Number">8</a> <a id="1450" href="/20.07/PUC/2019/Assignment5/#2046" class="InductiveConstructor Operator">`suc_</a>
<a id="1458" class="Keyword">infix</a> <a id="1466" class="Number">9</a> <a id="1469" href="/20.07/PUC/2019/Assignment5/#1789" class="InductiveConstructor Operator">`_</a>
</pre>
<h3 id="identifiers-types-and-contexts">Identifiers, types, and contexts</h3>
<pre class="Agda"> <a id="Inference.Id"></a><a id="1521" href="/20.07/PUC/2019/Assignment5/#1521" class="Function">Id</a> <a id="1524" class="Symbol">:</a> <a id="1526" class="PrimitiveType">Set</a>
<a id="1532" href="/20.07/PUC/2019/Assignment5/#1521" class="Function">Id</a> <a id="1535" class="Symbol">=</a> <a id="1537" href="Agda.Builtin.String.html#206" class="Postulate">String</a>
<a id="1547" class="Keyword">data</a> <a id="Inference.Type"></a><a id="1552" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a> <a id="1557" class="Symbol">:</a> <a id="1559" class="PrimitiveType">Set</a> <a id="1563" class="Keyword">where</a>
<a id="Inference.Type.`ℕ"></a><a id="1573" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="1579" class="Symbol">:</a> <a id="1581" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a>
<a id="Inference.Type._⇒_"></a><a id="1590" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">_⇒_</a> <a id="1596" class="Symbol">:</a> <a id="1598" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a> <a id="1603" class="Symbol">→</a> <a id="1605" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a> <a id="1610" class="Symbol">→</a> <a id="1612" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a>
<a id="1620" class="Keyword">data</a> <a id="Inference.Context"></a><a id="1625" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a> <a id="1633" class="Symbol">:</a> <a id="1635" class="PrimitiveType">Set</a> <a id="1639" class="Keyword">where</a>
<a id="Inference.Context.∅"></a><a id="1649" href="/20.07/PUC/2019/Assignment5/#1649" class="InductiveConstructor">∅</a> <a id="1655" class="Symbol">:</a> <a id="1657" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a>
<a id="Inference.Context._,_⦂_"></a><a id="1669" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">_,_⦂_</a> <a id="1675" class="Symbol">:</a> <a id="1677" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a> <a id="1685" class="Symbol">→</a> <a id="1687" href="/20.07/PUC/2019/Assignment5/#1521" class="Function">Id</a> <a id="1690" class="Symbol">→</a> <a id="1692" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a> <a id="1697" class="Symbol">→</a> <a id="1699" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a>
</pre>
<h3 id="terms">Terms</h3>
<pre class="Agda"> <a id="1729" class="Keyword">data</a> <a id="Inference.Term⁺"></a><a id="1734" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a> <a id="1740" class="Symbol">:</a> <a id="1742" class="PrimitiveType">Set</a>
<a id="1748" class="Keyword">data</a> <a id="Inference.Term⁻"></a><a id="1753" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a> <a id="1759" class="Symbol">:</a> <a id="1761" class="PrimitiveType">Set</a>
<a id="1768" class="Keyword">data</a> <a id="1773" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a> <a id="1779" class="Keyword">where</a>
<a id="Inference.Term⁺.`_"></a><a id="1789" href="/20.07/PUC/2019/Assignment5/#1789" class="InductiveConstructor Operator">`_</a> <a id="1815" class="Symbol">:</a> <a id="1817" href="/20.07/PUC/2019/Assignment5/#1521" class="Function">Id</a> <a id="1820" class="Symbol">→</a> <a id="1822" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a>
<a id="Inference.Term⁺._·_"></a><a id="1832" href="/20.07/PUC/2019/Assignment5/#1832" class="InductiveConstructor Operator">_·_</a> <a id="1858" class="Symbol">:</a> <a id="1860" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a> <a id="1866" class="Symbol">→</a> <a id="1868" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a> <a id="1874" class="Symbol">→</a> <a id="1876" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a>
<a id="Inference.Term⁺._↓_"></a><a id="1886" href="/20.07/PUC/2019/Assignment5/#1886" class="InductiveConstructor Operator">_↓_</a> <a id="1912" class="Symbol">:</a> <a id="1914" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a> <a id="1920" class="Symbol">→</a> <a id="1922" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a> <a id="1927" class="Symbol">→</a> <a id="1929" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a>
<a id="1938" class="Keyword">data</a> <a id="1943" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a> <a id="1949" class="Keyword">where</a>
<a id="Inference.Term⁻.ƛ_⇒_"></a><a id="1959" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">ƛ_⇒_</a> <a id="1984" class="Symbol">:</a> <a id="1986" href="/20.07/PUC/2019/Assignment5/#1521" class="Function">Id</a> <a id="1989" class="Symbol">→</a> <a id="1991" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a> <a id="1997" class="Symbol">→</a> <a id="1999" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a>
<a id="Inference.Term⁻.`zero"></a><a id="2009" href="/20.07/PUC/2019/Assignment5/#2009" class="InductiveConstructor">`zero</a> <a id="2034" class="Symbol">:</a> <a id="2036" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a>
<a id="Inference.Term⁻.`suc_"></a><a id="2046" href="/20.07/PUC/2019/Assignment5/#2046" class="InductiveConstructor Operator">`suc_</a> <a id="2071" class="Symbol">:</a> <a id="2073" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a> <a id="2079" class="Symbol">→</a> <a id="2081" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a>
<a id="Inference.Term⁻.`case_[zero⇒_|suc_⇒_]"></a><a id="2091" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">`case_[zero⇒_|suc_⇒_]</a> <a id="2116" class="Symbol">:</a> <a id="2118" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a> <a id="2124" class="Symbol">→</a> <a id="2126" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a> <a id="2132" class="Symbol">→</a> <a id="2134" href="/20.07/PUC/2019/Assignment5/#1521" class="Function">Id</a> <a id="2137" class="Symbol">→</a> <a id="2139" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a> <a id="2145" class="Symbol">→</a> <a id="2147" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a>
<a id="Inference.Term⁻.μ_⇒_"></a><a id="2157" href="/20.07/PUC/2019/Assignment5/#2157" class="InductiveConstructor Operator">μ_⇒_</a> <a id="2182" class="Symbol">:</a> <a id="2184" href="/20.07/PUC/2019/Assignment5/#1521" class="Function">Id</a> <a id="2187" class="Symbol">→</a> <a id="2189" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a> <a id="2195" class="Symbol">→</a> <a id="2197" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a>
<a id="Inference.Term⁻._↑"></a><a id="2207" href="/20.07/PUC/2019/Assignment5/#2207" class="InductiveConstructor Operator">_↑</a> <a id="2232" class="Symbol">:</a> <a id="2234" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a> <a id="2240" class="Symbol">→</a> <a id="2242" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a>
</pre>
<h3 id="sample-terms">Sample terms</h3>
<pre class="Agda"> <a id="Inference.two"></a><a id="2277" href="/20.07/PUC/2019/Assignment5/#2277" class="Function">two</a> <a id="2281" class="Symbol">:</a> <a id="2283" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a>
<a id="2291" href="/20.07/PUC/2019/Assignment5/#2277" class="Function">two</a> <a id="2295" class="Symbol">=</a> <a id="2297" href="/20.07/PUC/2019/Assignment5/#2046" class="InductiveConstructor Operator">`suc</a> <a id="2302" class="Symbol">(</a><a id="2303" href="/20.07/PUC/2019/Assignment5/#2046" class="InductiveConstructor Operator">`suc</a> <a id="2308" href="/20.07/PUC/2019/Assignment5/#2009" class="InductiveConstructor">`zero</a><a id="2313" class="Symbol">)</a>
<a id="Inference.plus"></a><a id="2318" href="/20.07/PUC/2019/Assignment5/#2318" class="Function">plus</a> <a id="2323" class="Symbol">:</a> <a id="2325" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a>
<a id="2333" href="/20.07/PUC/2019/Assignment5/#2318" class="Function">plus</a> <a id="2338" class="Symbol">=</a> <a id="2340" class="Symbol">(</a><a id="2341" href="/20.07/PUC/2019/Assignment5/#2157" class="InductiveConstructor Operator">μ</a> <a id="2343" class="String">&quot;p&quot;</a> <a id="2347" href="/20.07/PUC/2019/Assignment5/#2157" class="InductiveConstructor Operator">⇒</a> <a id="2349" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">ƛ</a> <a id="2351" class="String">&quot;m&quot;</a> <a id="2355" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">⇒</a> <a id="2357" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">ƛ</a> <a id="2359" class="String">&quot;n&quot;</a> <a id="2363" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">⇒</a>
<a id="2377" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">`case</a> <a id="2383" class="Symbol">(</a><a id="2384" href="/20.07/PUC/2019/Assignment5/#1789" class="InductiveConstructor Operator">`</a> <a id="2386" class="String">&quot;m&quot;</a><a id="2389" class="Symbol">)</a> <a id="2391" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">[zero⇒</a> <a id="2398" href="/20.07/PUC/2019/Assignment5/#1789" class="InductiveConstructor Operator">`</a> <a id="2400" class="String">&quot;n&quot;</a> <a id="2404" href="/20.07/PUC/2019/Assignment5/#2207" class="InductiveConstructor Operator">↑</a>
<a id="2432" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">|suc</a> <a id="2437" class="String">&quot;m&quot;</a> <a id="2441" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">⇒</a> <a id="2443" href="/20.07/PUC/2019/Assignment5/#2046" class="InductiveConstructor Operator">`suc</a> <a id="2448" class="Symbol">(</a><a id="2449" href="/20.07/PUC/2019/Assignment5/#1789" class="InductiveConstructor Operator">`</a> <a id="2451" class="String">&quot;p&quot;</a> <a id="2455" href="/20.07/PUC/2019/Assignment5/#1832" class="InductiveConstructor Operator">·</a> <a id="2457" class="Symbol">(</a><a id="2458" href="/20.07/PUC/2019/Assignment5/#1789" class="InductiveConstructor Operator">`</a> <a id="2460" class="String">&quot;m&quot;</a> <a id="2464" href="/20.07/PUC/2019/Assignment5/#2207" class="InductiveConstructor Operator">↑</a><a id="2465" class="Symbol">)</a> <a id="2467" href="/20.07/PUC/2019/Assignment5/#1832" class="InductiveConstructor Operator">·</a> <a id="2469" class="Symbol">(</a><a id="2470" href="/20.07/PUC/2019/Assignment5/#1789" class="InductiveConstructor Operator">`</a> <a id="2472" class="String">&quot;n&quot;</a> <a id="2476" href="/20.07/PUC/2019/Assignment5/#2207" class="InductiveConstructor Operator">↑</a><a id="2477" class="Symbol">)</a> <a id="2479" href="/20.07/PUC/2019/Assignment5/#2207" class="InductiveConstructor Operator">↑</a><a id="2480" class="Symbol">)</a> <a id="2482" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">]</a><a id="2483" class="Symbol">)</a>
<a id="2499" href="/20.07/PUC/2019/Assignment5/#1886" class="InductiveConstructor Operator">↓</a> <a id="2501" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="2504" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="2506" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="2509" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="2511" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a>
<a id="Inference.2+2"></a><a id="2517" href="/20.07/PUC/2019/Assignment5/#2517" class="Function">2+2</a> <a id="2521" class="Symbol">:</a> <a id="2523" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a>
<a id="2531" href="/20.07/PUC/2019/Assignment5/#2517" class="Function">2+2</a> <a id="2535" class="Symbol">=</a> <a id="2537" href="/20.07/PUC/2019/Assignment5/#2318" class="Function">plus</a> <a id="2542" href="/20.07/PUC/2019/Assignment5/#1832" class="InductiveConstructor Operator">·</a> <a id="2544" href="/20.07/PUC/2019/Assignment5/#2277" class="Function">two</a> <a id="2548" href="/20.07/PUC/2019/Assignment5/#1832" class="InductiveConstructor Operator">·</a> <a id="2550" href="/20.07/PUC/2019/Assignment5/#2277" class="Function">two</a>
</pre>
<h3 id="lookup">Lookup</h3>
<pre class="Agda"> <a id="2577" class="Keyword">data</a> <a id="Inference._∋_⦂_"></a><a id="2582" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">_∋_⦂_</a> <a id="2588" class="Symbol">:</a> <a id="2590" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a> <a id="2598" class="Symbol">→</a> <a id="2600" href="/20.07/PUC/2019/Assignment5/#1521" class="Function">Id</a> <a id="2603" class="Symbol">→</a> <a id="2605" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a> <a id="2610" class="Symbol">→</a> <a id="2612" class="PrimitiveType">Set</a> <a id="2616" class="Keyword">where</a>
<a id="Inference._∋_⦂_.Z"></a><a id="2627" href="/20.07/PUC/2019/Assignment5/#2627" class="InductiveConstructor">Z</a> <a id="2629" class="Symbol">:</a> <a id="2631" class="Symbol">∀</a> <a id="2633" class="Symbol">{</a><a id="2634" href="/20.07/PUC/2019/Assignment5/#2634" class="Bound">Γ</a> <a id="2636" href="/20.07/PUC/2019/Assignment5/#2636" class="Bound">x</a> <a id="2638" href="/20.07/PUC/2019/Assignment5/#2638" class="Bound">A</a><a id="2639" class="Symbol">}</a>
<a id="2649" class="Comment">--------------------</a>
<a id="2676" class="Symbol">→</a> <a id="2678" href="/20.07/PUC/2019/Assignment5/#2634" class="Bound">Γ</a> <a id="2680" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="2682" href="/20.07/PUC/2019/Assignment5/#2636" class="Bound">x</a> <a id="2684" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="2686" href="/20.07/PUC/2019/Assignment5/#2638" class="Bound">A</a> <a id="2688" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">∋</a> <a id="2690" href="/20.07/PUC/2019/Assignment5/#2636" class="Bound">x</a> <a id="2692" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">⦂</a> <a id="2694" href="/20.07/PUC/2019/Assignment5/#2638" class="Bound">A</a>
<a id="Inference._∋_⦂_.S"></a><a id="2701" href="/20.07/PUC/2019/Assignment5/#2701" class="InductiveConstructor">S</a> <a id="2703" class="Symbol">:</a> <a id="2705" class="Symbol">∀</a> <a id="2707" class="Symbol">{</a><a id="2708" href="/20.07/PUC/2019/Assignment5/#2708" class="Bound">Γ</a> <a id="2710" href="/20.07/PUC/2019/Assignment5/#2710" class="Bound">x</a> <a id="2712" href="/20.07/PUC/2019/Assignment5/#2712" class="Bound">y</a> <a id="2714" href="/20.07/PUC/2019/Assignment5/#2714" class="Bound">A</a> <a id="2716" href="/20.07/PUC/2019/Assignment5/#2716" class="Bound">B</a><a id="2717" class="Symbol">}</a>
<a id="2725" class="Symbol">→</a> <a id="2727" href="/20.07/PUC/2019/Assignment5/#2710" class="Bound">x</a> <a id="2729" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#799" class="Function Operator">≢</a> <a id="2731" href="/20.07/PUC/2019/Assignment5/#2712" class="Bound">y</a>
<a id="2739" class="Symbol">→</a> <a id="2741" href="/20.07/PUC/2019/Assignment5/#2708" class="Bound">Γ</a> <a id="2743" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">∋</a> <a id="2745" href="/20.07/PUC/2019/Assignment5/#2710" class="Bound">x</a> <a id="2747" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">⦂</a> <a id="2749" href="/20.07/PUC/2019/Assignment5/#2714" class="Bound">A</a>
<a id="2759" class="Comment">-----------------</a>
<a id="2783" class="Symbol">→</a> <a id="2785" href="/20.07/PUC/2019/Assignment5/#2708" class="Bound">Γ</a> <a id="2787" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="2789" href="/20.07/PUC/2019/Assignment5/#2712" class="Bound">y</a> <a id="2791" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="2793" href="/20.07/PUC/2019/Assignment5/#2716" class="Bound">B</a> <a id="2795" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">∋</a> <a id="2797" href="/20.07/PUC/2019/Assignment5/#2710" class="Bound">x</a> <a id="2799" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">⦂</a> <a id="2801" href="/20.07/PUC/2019/Assignment5/#2714" class="Bound">A</a>
</pre>
<h3 id="bidirectional-type-checking">Bidirectional type checking</h3>
<pre class="Agda"> <a id="2847" class="Keyword">data</a> <a id="Inference._⊢_↑_"></a><a id="2852" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">_⊢_↑_</a> <a id="2858" class="Symbol">:</a> <a id="2860" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a> <a id="2868" class="Symbol">→</a> <a id="2870" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a> <a id="2876" class="Symbol">→</a> <a id="2878" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a> <a id="2883" class="Symbol">→</a> <a id="2885" class="PrimitiveType">Set</a>
<a id="2891" class="Keyword">data</a> <a id="Inference._⊢_↓_"></a><a id="2896" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">_⊢_↓_</a> <a id="2902" class="Symbol">:</a> <a id="2904" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a> <a id="2912" class="Symbol">→</a> <a id="2914" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a> <a id="2920" class="Symbol">→</a> <a id="2922" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a> <a id="2927" class="Symbol">→</a> <a id="2929" class="PrimitiveType">Set</a>
<a id="2936" class="Keyword">data</a> <a id="2941" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">_⊢_↑_</a> <a id="2947" class="Keyword">where</a>
<a id="Inference._⊢_↑_.⊢`"></a><a id="2958" href="/20.07/PUC/2019/Assignment5/#2958" class="InductiveConstructor">⊢`</a> <a id="2961" class="Symbol">:</a> <a id="2963" class="Symbol">∀</a> <a id="2965" class="Symbol">{</a><a id="2966" href="/20.07/PUC/2019/Assignment5/#2966" class="Bound">Γ</a> <a id="2968" href="/20.07/PUC/2019/Assignment5/#2968" class="Bound">A</a> <a id="2970" href="/20.07/PUC/2019/Assignment5/#2970" class="Bound">x</a><a id="2971" class="Symbol">}</a>
<a id="2979" class="Symbol">→</a> <a id="2981" href="/20.07/PUC/2019/Assignment5/#2966" class="Bound">Γ</a> <a id="2983" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">∋</a> <a id="2985" href="/20.07/PUC/2019/Assignment5/#2970" class="Bound">x</a> <a id="2987" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">⦂</a> <a id="2989" href="/20.07/PUC/2019/Assignment5/#2968" class="Bound">A</a>
<a id="2999" class="Comment">-----------</a>
<a id="3017" class="Symbol">→</a> <a id="3019" href="/20.07/PUC/2019/Assignment5/#2966" class="Bound">Γ</a> <a id="3021" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="3023" href="/20.07/PUC/2019/Assignment5/#1789" class="InductiveConstructor Operator">`</a> <a id="3025" href="/20.07/PUC/2019/Assignment5/#2970" class="Bound">x</a> <a id="3027" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="3029" href="/20.07/PUC/2019/Assignment5/#2968" class="Bound">A</a>
<a id="Inference._⊢_↑_._·_"></a><a id="3036" href="/20.07/PUC/2019/Assignment5/#3036" class="InductiveConstructor Operator">_·_</a> <a id="3040" class="Symbol">:</a> <a id="3042" class="Symbol">∀</a> <a id="3044" class="Symbol">{</a><a id="3045" href="/20.07/PUC/2019/Assignment5/#3045" class="Bound">Γ</a> <a id="3047" href="/20.07/PUC/2019/Assignment5/#3047" class="Bound">L</a> <a id="3049" href="/20.07/PUC/2019/Assignment5/#3049" class="Bound">M</a> <a id="3051" href="/20.07/PUC/2019/Assignment5/#3051" class="Bound">A</a> <a id="3053" href="/20.07/PUC/2019/Assignment5/#3053" class="Bound">B</a><a id="3054" class="Symbol">}</a>
<a id="3062" class="Symbol">→</a> <a id="3064" href="/20.07/PUC/2019/Assignment5/#3045" class="Bound">Γ</a> <a id="3066" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="3068" href="/20.07/PUC/2019/Assignment5/#3047" class="Bound">L</a> <a id="3070" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="3072" href="/20.07/PUC/2019/Assignment5/#3051" class="Bound">A</a> <a id="3074" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="3076" href="/20.07/PUC/2019/Assignment5/#3053" class="Bound">B</a>
<a id="3084" class="Symbol">→</a> <a id="3086" href="/20.07/PUC/2019/Assignment5/#3045" class="Bound">Γ</a> <a id="3088" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3090" href="/20.07/PUC/2019/Assignment5/#3049" class="Bound">M</a> <a id="3092" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3094" href="/20.07/PUC/2019/Assignment5/#3051" class="Bound">A</a>
<a id="3104" class="Comment">-------------</a>
<a id="3124" class="Symbol">→</a> <a id="3126" href="/20.07/PUC/2019/Assignment5/#3045" class="Bound">Γ</a> <a id="3128" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="3130" href="/20.07/PUC/2019/Assignment5/#3047" class="Bound">L</a> <a id="3132" href="/20.07/PUC/2019/Assignment5/#1832" class="InductiveConstructor Operator">·</a> <a id="3134" href="/20.07/PUC/2019/Assignment5/#3049" class="Bound">M</a> <a id="3136" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="3138" href="/20.07/PUC/2019/Assignment5/#3053" class="Bound">B</a>
<a id="Inference._⊢_↑_.⊢↓"></a><a id="3145" href="/20.07/PUC/2019/Assignment5/#3145" class="InductiveConstructor">⊢↓</a> <a id="3148" class="Symbol">:</a> <a id="3150" class="Symbol">∀</a> <a id="3152" class="Symbol">{</a><a id="3153" href="/20.07/PUC/2019/Assignment5/#3153" class="Bound">Γ</a> <a id="3155" href="/20.07/PUC/2019/Assignment5/#3155" class="Bound">M</a> <a id="3157" href="/20.07/PUC/2019/Assignment5/#3157" class="Bound">A</a><a id="3158" class="Symbol">}</a>
<a id="3166" class="Symbol">→</a> <a id="3168" href="/20.07/PUC/2019/Assignment5/#3153" class="Bound">Γ</a> <a id="3170" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3172" href="/20.07/PUC/2019/Assignment5/#3155" class="Bound">M</a> <a id="3174" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3176" href="/20.07/PUC/2019/Assignment5/#3157" class="Bound">A</a>
<a id="3186" class="Comment">---------------</a>
<a id="3208" class="Symbol">→</a> <a id="3210" href="/20.07/PUC/2019/Assignment5/#3153" class="Bound">Γ</a> <a id="3212" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="3214" class="Symbol">(</a><a id="3215" href="/20.07/PUC/2019/Assignment5/#3155" class="Bound">M</a> <a id="3217" href="/20.07/PUC/2019/Assignment5/#1886" class="InductiveConstructor Operator">↓</a> <a id="3219" href="/20.07/PUC/2019/Assignment5/#3157" class="Bound">A</a><a id="3220" class="Symbol">)</a> <a id="3222" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="3224" href="/20.07/PUC/2019/Assignment5/#3157" class="Bound">A</a>
<a id="3229" class="Keyword">data</a> <a id="3234" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">_⊢_↓_</a> <a id="3240" class="Keyword">where</a>
<a id="Inference._⊢_↓_.⊢ƛ"></a><a id="3251" href="/20.07/PUC/2019/Assignment5/#3251" class="InductiveConstructor">⊢ƛ</a> <a id="3254" class="Symbol">:</a> <a id="3256" class="Symbol">∀</a> <a id="3258" class="Symbol">{</a><a id="3259" href="/20.07/PUC/2019/Assignment5/#3259" class="Bound">Γ</a> <a id="3261" href="/20.07/PUC/2019/Assignment5/#3261" class="Bound">x</a> <a id="3263" href="/20.07/PUC/2019/Assignment5/#3263" class="Bound">N</a> <a id="3265" href="/20.07/PUC/2019/Assignment5/#3265" class="Bound">A</a> <a id="3267" href="/20.07/PUC/2019/Assignment5/#3267" class="Bound">B</a><a id="3268" class="Symbol">}</a>
<a id="3276" class="Symbol">→</a> <a id="3278" href="/20.07/PUC/2019/Assignment5/#3259" class="Bound">Γ</a> <a id="3280" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="3282" href="/20.07/PUC/2019/Assignment5/#3261" class="Bound">x</a> <a id="3284" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="3286" href="/20.07/PUC/2019/Assignment5/#3265" class="Bound">A</a> <a id="3288" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3290" href="/20.07/PUC/2019/Assignment5/#3263" class="Bound">N</a> <a id="3292" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3294" href="/20.07/PUC/2019/Assignment5/#3267" class="Bound">B</a>
<a id="3304" class="Comment">-------------------</a>
<a id="3330" class="Symbol">→</a> <a id="3332" href="/20.07/PUC/2019/Assignment5/#3259" class="Bound">Γ</a> <a id="3334" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3336" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">ƛ</a> <a id="3338" href="/20.07/PUC/2019/Assignment5/#3261" class="Bound">x</a> <a id="3340" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">⇒</a> <a id="3342" href="/20.07/PUC/2019/Assignment5/#3263" class="Bound">N</a> <a id="3344" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3346" href="/20.07/PUC/2019/Assignment5/#3265" class="Bound">A</a> <a id="3348" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="3350" href="/20.07/PUC/2019/Assignment5/#3267" class="Bound">B</a>
<a id="Inference._⊢_↓_.⊢zero"></a><a id="3357" href="/20.07/PUC/2019/Assignment5/#3357" class="InductiveConstructor">⊢zero</a> <a id="3363" class="Symbol">:</a> <a id="3365" class="Symbol">∀</a> <a id="3367" class="Symbol">{</a><a id="3368" href="/20.07/PUC/2019/Assignment5/#3368" class="Bound">Γ</a><a id="3369" class="Symbol">}</a>
<a id="3379" class="Comment">--------------</a>
<a id="3400" class="Symbol">→</a> <a id="3402" href="/20.07/PUC/2019/Assignment5/#3368" class="Bound">Γ</a> <a id="3404" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3406" href="/20.07/PUC/2019/Assignment5/#2009" class="InductiveConstructor">`zero</a> <a id="3412" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3414" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a>
<a id="Inference._⊢_↓_.⊢suc"></a><a id="3422" href="/20.07/PUC/2019/Assignment5/#3422" class="InductiveConstructor">⊢suc</a> <a id="3427" class="Symbol">:</a> <a id="3429" class="Symbol">∀</a> <a id="3431" class="Symbol">{</a><a id="3432" href="/20.07/PUC/2019/Assignment5/#3432" class="Bound">Γ</a> <a id="3434" href="/20.07/PUC/2019/Assignment5/#3434" class="Bound">M</a><a id="3435" class="Symbol">}</a>
<a id="3443" class="Symbol">→</a> <a id="3445" href="/20.07/PUC/2019/Assignment5/#3432" class="Bound">Γ</a> <a id="3447" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3449" href="/20.07/PUC/2019/Assignment5/#3434" class="Bound">M</a> <a id="3451" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3453" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a>
<a id="3464" class="Comment">---------------</a>
<a id="3486" class="Symbol">→</a> <a id="3488" href="/20.07/PUC/2019/Assignment5/#3432" class="Bound">Γ</a> <a id="3490" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3492" href="/20.07/PUC/2019/Assignment5/#2046" class="InductiveConstructor Operator">`suc</a> <a id="3497" href="/20.07/PUC/2019/Assignment5/#3434" class="Bound">M</a> <a id="3499" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3501" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a>
<a id="Inference._⊢_↓_.⊢case"></a><a id="3509" href="/20.07/PUC/2019/Assignment5/#3509" class="InductiveConstructor">⊢case</a> <a id="3515" class="Symbol">:</a> <a id="3517" class="Symbol">∀</a> <a id="3519" class="Symbol">{</a><a id="3520" href="/20.07/PUC/2019/Assignment5/#3520" class="Bound">Γ</a> <a id="3522" href="/20.07/PUC/2019/Assignment5/#3522" class="Bound">L</a> <a id="3524" href="/20.07/PUC/2019/Assignment5/#3524" class="Bound">M</a> <a id="3526" href="/20.07/PUC/2019/Assignment5/#3526" class="Bound">x</a> <a id="3528" href="/20.07/PUC/2019/Assignment5/#3528" class="Bound">N</a> <a id="3530" href="/20.07/PUC/2019/Assignment5/#3530" class="Bound">A</a><a id="3531" class="Symbol">}</a>
<a id="3539" class="Symbol">→</a> <a id="3541" href="/20.07/PUC/2019/Assignment5/#3520" class="Bound">Γ</a> <a id="3543" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="3545" href="/20.07/PUC/2019/Assignment5/#3522" class="Bound">L</a> <a id="3547" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="3549" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a>
<a id="3558" class="Symbol">→</a> <a id="3560" href="/20.07/PUC/2019/Assignment5/#3520" class="Bound">Γ</a> <a id="3562" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3564" href="/20.07/PUC/2019/Assignment5/#3524" class="Bound">M</a> <a id="3566" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3568" href="/20.07/PUC/2019/Assignment5/#3530" class="Bound">A</a>
<a id="3576" class="Symbol">→</a> <a id="3578" href="/20.07/PUC/2019/Assignment5/#3520" class="Bound">Γ</a> <a id="3580" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="3582" href="/20.07/PUC/2019/Assignment5/#3526" class="Bound">x</a> <a id="3584" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="3586" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="3589" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3591" href="/20.07/PUC/2019/Assignment5/#3528" class="Bound">N</a> <a id="3593" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3595" href="/20.07/PUC/2019/Assignment5/#3530" class="Bound">A</a>
<a id="3605" class="Comment">-------------------------------------</a>
<a id="3649" class="Symbol">→</a> <a id="3651" href="/20.07/PUC/2019/Assignment5/#3520" class="Bound">Γ</a> <a id="3653" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3655" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">`case</a> <a id="3661" href="/20.07/PUC/2019/Assignment5/#3522" class="Bound">L</a> <a id="3663" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">[zero⇒</a> <a id="3670" href="/20.07/PUC/2019/Assignment5/#3524" class="Bound">M</a> <a id="3672" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">|suc</a> <a id="3677" href="/20.07/PUC/2019/Assignment5/#3526" class="Bound">x</a> <a id="3679" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">⇒</a> <a id="3681" href="/20.07/PUC/2019/Assignment5/#3528" class="Bound">N</a> <a id="3683" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">]</a> <a id="3685" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3687" href="/20.07/PUC/2019/Assignment5/#3530" class="Bound">A</a>
<a id="Inference._⊢_↓_.⊢μ"></a><a id="3694" href="/20.07/PUC/2019/Assignment5/#3694" class="InductiveConstructor">⊢μ</a> <a id="3697" class="Symbol">:</a> <a id="3699" class="Symbol">∀</a> <a id="3701" class="Symbol">{</a><a id="3702" href="/20.07/PUC/2019/Assignment5/#3702" class="Bound">Γ</a> <a id="3704" href="/20.07/PUC/2019/Assignment5/#3704" class="Bound">x</a> <a id="3706" href="/20.07/PUC/2019/Assignment5/#3706" class="Bound">N</a> <a id="3708" href="/20.07/PUC/2019/Assignment5/#3708" class="Bound">A</a><a id="3709" class="Symbol">}</a>
<a id="3717" class="Symbol">→</a> <a id="3719" href="/20.07/PUC/2019/Assignment5/#3702" class="Bound">Γ</a> <a id="3721" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="3723" href="/20.07/PUC/2019/Assignment5/#3704" class="Bound">x</a> <a id="3725" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="3727" href="/20.07/PUC/2019/Assignment5/#3708" class="Bound">A</a> <a id="3729" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3731" href="/20.07/PUC/2019/Assignment5/#3706" class="Bound">N</a> <a id="3733" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3735" href="/20.07/PUC/2019/Assignment5/#3708" class="Bound">A</a>
<a id="3745" class="Comment">-----------------</a>
<a id="3769" class="Symbol">→</a> <a id="3771" href="/20.07/PUC/2019/Assignment5/#3702" class="Bound">Γ</a> <a id="3773" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3775" href="/20.07/PUC/2019/Assignment5/#2157" class="InductiveConstructor Operator">μ</a> <a id="3777" href="/20.07/PUC/2019/Assignment5/#3704" class="Bound">x</a> <a id="3779" href="/20.07/PUC/2019/Assignment5/#2157" class="InductiveConstructor Operator">⇒</a> <a id="3781" href="/20.07/PUC/2019/Assignment5/#3706" class="Bound">N</a> <a id="3783" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3785" href="/20.07/PUC/2019/Assignment5/#3708" class="Bound">A</a>
<a id="Inference._⊢_↓_.⊢↑"></a><a id="3792" href="/20.07/PUC/2019/Assignment5/#3792" class="InductiveConstructor">⊢↑</a> <a id="3795" class="Symbol">:</a> <a id="3797" class="Symbol">∀</a> <a id="3799" class="Symbol">{</a><a id="3800" href="/20.07/PUC/2019/Assignment5/#3800" class="Bound">Γ</a> <a id="3802" href="/20.07/PUC/2019/Assignment5/#3802" class="Bound">M</a> <a id="3804" href="/20.07/PUC/2019/Assignment5/#3804" class="Bound">A</a> <a id="3806" href="/20.07/PUC/2019/Assignment5/#3806" class="Bound">B</a><a id="3807" class="Symbol">}</a>
<a id="3815" class="Symbol">→</a> <a id="3817" href="/20.07/PUC/2019/Assignment5/#3800" class="Bound">Γ</a> <a id="3819" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="3821" href="/20.07/PUC/2019/Assignment5/#3802" class="Bound">M</a> <a id="3823" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="3825" href="/20.07/PUC/2019/Assignment5/#3804" class="Bound">A</a>
<a id="3833" class="Symbol">→</a> <a id="3835" href="/20.07/PUC/2019/Assignment5/#3804" class="Bound">A</a> <a id="3837" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="3839" href="/20.07/PUC/2019/Assignment5/#3806" class="Bound">B</a>
<a id="3849" class="Comment">-------------</a>
<a id="3869" class="Symbol">→</a> <a id="3871" href="/20.07/PUC/2019/Assignment5/#3800" class="Bound">Γ</a> <a id="3873" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="3875" class="Symbol">(</a><a id="3876" href="/20.07/PUC/2019/Assignment5/#3802" class="Bound">M</a> <a id="3878" href="/20.07/PUC/2019/Assignment5/#2207" class="InductiveConstructor Operator">↑</a><a id="3879" class="Symbol">)</a> <a id="3881" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="3883" href="/20.07/PUC/2019/Assignment5/#3806" class="Bound">B</a>
</pre>
<h3 id="type-equality">Type equality</h3>
<pre class="Agda"> <a id="Inference._≟Tp_"></a><a id="3916" href="/20.07/PUC/2019/Assignment5/#3916" class="Function Operator">_≟Tp_</a> <a id="3922" class="Symbol">:</a> <a id="3924" class="Symbol">(</a><a id="3925" href="/20.07/PUC/2019/Assignment5/#3925" class="Bound">A</a> <a id="3927" href="/20.07/PUC/2019/Assignment5/#3927" class="Bound">B</a> <a id="3929" class="Symbol">:</a> <a id="3931" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a><a id="3935" class="Symbol">)</a> <a id="3937" class="Symbol">→</a> <a id="3939" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a> <a id="3943" class="Symbol">(</a><a id="3944" href="/20.07/PUC/2019/Assignment5/#3925" class="Bound">A</a> <a id="3946" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="3948" href="/20.07/PUC/2019/Assignment5/#3927" class="Bound">B</a><a id="3949" class="Symbol">)</a>
<a id="3953" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="3961" href="/20.07/PUC/2019/Assignment5/#3916" class="Function Operator">≟Tp</a> <a id="3965" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="3981" class="Symbol">=</a> <a id="3984" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="3988" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="3995" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="4003" href="/20.07/PUC/2019/Assignment5/#3916" class="Function Operator">≟Tp</a> <a id="4007" class="Symbol">(</a><a id="4008" href="/20.07/PUC/2019/Assignment5/#4008" class="Bound">A</a> <a id="4010" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="4012" href="/20.07/PUC/2019/Assignment5/#4012" class="Bound">B</a><a id="4013" class="Symbol">)</a> <a id="4023" class="Symbol">=</a> <a id="4026" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="4029" class="Symbol">λ()</a>
<a id="4035" class="Symbol">(</a><a id="4036" href="/20.07/PUC/2019/Assignment5/#4036" class="Bound">A</a> <a id="4038" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="4040" href="/20.07/PUC/2019/Assignment5/#4040" class="Bound">B</a><a id="4041" class="Symbol">)</a> <a id="4043" href="/20.07/PUC/2019/Assignment5/#3916" class="Function Operator">≟Tp</a> <a id="4047" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="4063" class="Symbol">=</a> <a id="4066" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="4069" class="Symbol">λ()</a>
<a id="4075" class="Symbol">(</a><a id="4076" href="/20.07/PUC/2019/Assignment5/#4076" class="Bound">A</a> <a id="4078" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="4080" href="/20.07/PUC/2019/Assignment5/#4080" class="Bound">B</a><a id="4081" class="Symbol">)</a> <a id="4083" href="/20.07/PUC/2019/Assignment5/#3916" class="Function Operator">≟Tp</a> <a id="4087" class="Symbol">(</a><a id="4088" href="/20.07/PUC/2019/Assignment5/#4088" class="Bound">A′</a> <a id="4091" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="4093" href="/20.07/PUC/2019/Assignment5/#4093" class="Bound">B′</a><a id="4095" class="Symbol">)</a>
<a id="4101" class="Keyword">with</a> <a id="4106" href="/20.07/PUC/2019/Assignment5/#4076" class="Bound">A</a> <a id="4108" href="/20.07/PUC/2019/Assignment5/#3916" class="Function Operator">≟Tp</a> <a id="4112" href="/20.07/PUC/2019/Assignment5/#4088" class="Bound">A′</a> <a id="4115" class="Symbol">|</a> <a id="4117" href="/20.07/PUC/2019/Assignment5/#4080" class="Bound">B</a> <a id="4119" href="/20.07/PUC/2019/Assignment5/#3916" class="Function Operator">≟Tp</a> <a id="4123" href="/20.07/PUC/2019/Assignment5/#4093" class="Bound">B′</a>
<a id="4128" class="Symbol">...</a> <a id="4133" class="Symbol">|</a> <a id="4135" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="4138" href="/20.07/PUC/2019/Assignment5/#4138" class="Bound">A≢</a> <a id="4144" class="Symbol">|</a> <a id="4146" class="Symbol">_</a> <a id="4156" class="Symbol">=</a> <a id="4159" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="4162" class="Symbol">λ{</a><a id="4164" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="4169" class="Symbol">→</a> <a id="4171" href="/20.07/PUC/2019/Assignment5/#4138" class="Bound">A≢</a> <a id="4174" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="4178" class="Symbol">}</a>
<a id="4182" class="Symbol">...</a> <a id="4187" class="Symbol">|</a> <a id="4189" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="4193" class="Symbol">_</a> <a id="4198" class="Symbol">|</a> <a id="4200" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="4203" href="/20.07/PUC/2019/Assignment5/#4203" class="Bound">B≢</a> <a id="4210" class="Symbol">=</a> <a id="4213" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="4216" class="Symbol">λ{</a><a id="4218" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="4223" class="Symbol">→</a> <a id="4225" href="/20.07/PUC/2019/Assignment5/#4203" class="Bound">B≢</a> <a id="4228" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="4232" class="Symbol">}</a>
<a id="4236" class="Symbol">...</a> <a id="4241" class="Symbol">|</a> <a id="4243" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="4247" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="4252" class="Symbol">|</a> <a id="4254" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="4258" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="4264" class="Symbol">=</a> <a id="4267" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="4271" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre>
<h3 id="prerequisites">Prerequisites</h3>
<pre class="Agda"> <a id="Inference.dom≡"></a><a id="4306" href="/20.07/PUC/2019/Assignment5/#4306" class="Function">dom≡</a> <a id="4311" class="Symbol">:</a> <a id="4313" class="Symbol">∀</a> <a id="4315" class="Symbol">{</a><a id="4316" href="/20.07/PUC/2019/Assignment5/#4316" class="Bound">A</a> <a id="4318" href="/20.07/PUC/2019/Assignment5/#4318" class="Bound">A′</a> <a id="4321" href="/20.07/PUC/2019/Assignment5/#4321" class="Bound">B</a> <a id="4323" href="/20.07/PUC/2019/Assignment5/#4323" class="Bound">B′</a><a id="4325" class="Symbol">}</a> <a id="4327" class="Symbol">→</a> <a id="4329" href="/20.07/PUC/2019/Assignment5/#4316" class="Bound">A</a> <a id="4331" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="4333" href="/20.07/PUC/2019/Assignment5/#4321" class="Bound">B</a> <a id="4335" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4337" href="/20.07/PUC/2019/Assignment5/#4318" class="Bound">A′</a> <a id="4340" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="4342" href="/20.07/PUC/2019/Assignment5/#4323" class="Bound">B′</a> <a id="4345" class="Symbol">→</a> <a id="4347" href="/20.07/PUC/2019/Assignment5/#4316" class="Bound">A</a> <a id="4349" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4351" href="/20.07/PUC/2019/Assignment5/#4318" class="Bound">A′</a>
<a id="4356" href="/20.07/PUC/2019/Assignment5/#4306" class="Function">dom≡</a> <a id="4361" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="4366" class="Symbol">=</a> <a id="4368" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="Inference.rng≡"></a><a id="4376" href="/20.07/PUC/2019/Assignment5/#4376" class="Function">rng≡</a> <a id="4381" class="Symbol">:</a> <a id="4383" class="Symbol">∀</a> <a id="4385" class="Symbol">{</a><a id="4386" href="/20.07/PUC/2019/Assignment5/#4386" class="Bound">A</a> <a id="4388" href="/20.07/PUC/2019/Assignment5/#4388" class="Bound">A′</a> <a id="4391" href="/20.07/PUC/2019/Assignment5/#4391" class="Bound">B</a> <a id="4393" href="/20.07/PUC/2019/Assignment5/#4393" class="Bound">B′</a><a id="4395" class="Symbol">}</a> <a id="4397" class="Symbol">→</a> <a id="4399" href="/20.07/PUC/2019/Assignment5/#4386" class="Bound">A</a> <a id="4401" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="4403" href="/20.07/PUC/2019/Assignment5/#4391" class="Bound">B</a> <a id="4405" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4407" href="/20.07/PUC/2019/Assignment5/#4388" class="Bound">A′</a> <a id="4410" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="4412" href="/20.07/PUC/2019/Assignment5/#4393" class="Bound">B′</a> <a id="4415" class="Symbol">→</a> <a id="4417" href="/20.07/PUC/2019/Assignment5/#4391" class="Bound">B</a> <a id="4419" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4421" href="/20.07/PUC/2019/Assignment5/#4393" class="Bound">B′</a>
<a id="4426" href="/20.07/PUC/2019/Assignment5/#4376" class="Function">rng≡</a> <a id="4431" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="4436" class="Symbol">=</a> <a id="4438" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="Inference.ℕ≢⇒"></a><a id="4446" href="/20.07/PUC/2019/Assignment5/#4446" class="Function">ℕ≢⇒</a> <a id="4450" class="Symbol">:</a> <a id="4452" class="Symbol">∀</a> <a id="4454" class="Symbol">{</a><a id="4455" href="/20.07/PUC/2019/Assignment5/#4455" class="Bound">A</a> <a id="4457" href="/20.07/PUC/2019/Assignment5/#4457" class="Bound">B</a><a id="4458" class="Symbol">}</a> <a id="4460" class="Symbol">→</a> <a id="4462" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="4465" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#799" class="Function Operator">≢</a> <a id="4467" href="/20.07/PUC/2019/Assignment5/#4455" class="Bound">A</a> <a id="4469" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="4471" href="/20.07/PUC/2019/Assignment5/#4457" class="Bound">B</a>
<a id="4475" href="/20.07/PUC/2019/Assignment5/#4446" class="Function">ℕ≢⇒</a> <a id="4479" class="Symbol">()</a>
</pre>
<h3 id="unique-lookup">Unique lookup</h3>
<pre class="Agda"> <a id="Inference.uniq-∋"></a><a id="4513" href="/20.07/PUC/2019/Assignment5/#4513" class="Function">uniq-∋</a> <a id="4520" class="Symbol">:</a> <a id="4522" class="Symbol">∀</a> <a id="4524" class="Symbol">{</a><a id="4525" href="/20.07/PUC/2019/Assignment5/#4525" class="Bound">Γ</a> <a id="4527" href="/20.07/PUC/2019/Assignment5/#4527" class="Bound">x</a> <a id="4529" href="/20.07/PUC/2019/Assignment5/#4529" class="Bound">A</a> <a id="4531" href="/20.07/PUC/2019/Assignment5/#4531" class="Bound">B</a><a id="4532" class="Symbol">}</a> <a id="4534" class="Symbol">→</a> <a id="4536" href="/20.07/PUC/2019/Assignment5/#4525" class="Bound">Γ</a> <a id="4538" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">∋</a> <a id="4540" href="/20.07/PUC/2019/Assignment5/#4527" class="Bound">x</a> <a id="4542" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">⦂</a> <a id="4544" href="/20.07/PUC/2019/Assignment5/#4529" class="Bound">A</a> <a id="4546" class="Symbol">→</a> <a id="4548" href="/20.07/PUC/2019/Assignment5/#4525" class="Bound">Γ</a> <a id="4550" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">∋</a> <a id="4552" href="/20.07/PUC/2019/Assignment5/#4527" class="Bound">x</a> <a id="4554" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">⦂</a> <a id="4556" href="/20.07/PUC/2019/Assignment5/#4531" class="Bound">B</a> <a id="4558" class="Symbol">→</a> <a id="4560" href="/20.07/PUC/2019/Assignment5/#4529" class="Bound">A</a> <a id="4562" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4564" href="/20.07/PUC/2019/Assignment5/#4531" class="Bound">B</a>
<a id="4568" href="/20.07/PUC/2019/Assignment5/#4513" class="Function">uniq-∋</a> <a id="4575" href="/20.07/PUC/2019/Assignment5/#2627" class="InductiveConstructor">Z</a> <a id="4577" href="/20.07/PUC/2019/Assignment5/#2627" class="InductiveConstructor">Z</a> <a id="4595" class="Symbol">=</a> <a id="4598" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="4605" href="/20.07/PUC/2019/Assignment5/#4513" class="Function">uniq-∋</a> <a id="4612" href="/20.07/PUC/2019/Assignment5/#2627" class="InductiveConstructor">Z</a> <a id="4614" class="Symbol">(</a><a id="4615" href="/20.07/PUC/2019/Assignment5/#2701" class="InductiveConstructor">S</a> <a id="4617" href="/20.07/PUC/2019/Assignment5/#4617" class="Bound">x≢y</a> <a id="4621" class="Symbol">_)</a> <a id="4632" class="Symbol">=</a> <a id="4635" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="4642" class="Symbol">(</a><a id="4643" href="/20.07/PUC/2019/Assignment5/#4617" class="Bound">x≢y</a> <a id="4647" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="4651" class="Symbol">)</a>
<a id="4655" href="/20.07/PUC/2019/Assignment5/#4513" class="Function">uniq-∋</a> <a id="4662" class="Symbol">(</a><a id="4663" href="/20.07/PUC/2019/Assignment5/#2701" class="InductiveConstructor">S</a> <a id="4665" href="/20.07/PUC/2019/Assignment5/#4665" class="Bound">x≢y</a> <a id="4669" class="Symbol">_)</a> <a id="4672" href="/20.07/PUC/2019/Assignment5/#2627" class="InductiveConstructor">Z</a> <a id="4682" class="Symbol">=</a> <a id="4685" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="4692" class="Symbol">(</a><a id="4693" href="/20.07/PUC/2019/Assignment5/#4665" class="Bound">x≢y</a> <a id="4697" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="4701" class="Symbol">)</a>
<a id="4705" href="/20.07/PUC/2019/Assignment5/#4513" class="Function">uniq-∋</a> <a id="4712" class="Symbol">(</a><a id="4713" href="/20.07/PUC/2019/Assignment5/#2701" class="InductiveConstructor">S</a> <a id="4715" class="Symbol">_</a> <a id="4717" href="/20.07/PUC/2019/Assignment5/#4717" class="Bound">∋x</a><a id="4719" class="Symbol">)</a> <a id="4721" class="Symbol">(</a><a id="4722" href="/20.07/PUC/2019/Assignment5/#2701" class="InductiveConstructor">S</a> <a id="4724" class="Symbol">_</a> <a id="4726" href="/20.07/PUC/2019/Assignment5/#4726" class="Bound">∋x′</a><a id="4729" class="Symbol">)</a> <a id="4732" class="Symbol">=</a> <a id="4735" href="/20.07/PUC/2019/Assignment5/#4513" class="Function">uniq-∋</a> <a id="4742" href="/20.07/PUC/2019/Assignment5/#4717" class="Bound">∋x</a> <a id="4745" href="/20.07/PUC/2019/Assignment5/#4726" class="Bound">∋x′</a>
</pre>
<h3 id="unique-synthesis">Unique synthesis</h3>
<pre class="Agda"> <a id="Inference.uniq-↑"></a><a id="4782" href="/20.07/PUC/2019/Assignment5/#4782" class="Function">uniq-↑</a> <a id="4789" class="Symbol">:</a> <a id="4791" class="Symbol">∀</a> <a id="4793" class="Symbol">{</a><a id="4794" href="/20.07/PUC/2019/Assignment5/#4794" class="Bound">Γ</a> <a id="4796" href="/20.07/PUC/2019/Assignment5/#4796" class="Bound">M</a> <a id="4798" href="/20.07/PUC/2019/Assignment5/#4798" class="Bound">A</a> <a id="4800" href="/20.07/PUC/2019/Assignment5/#4800" class="Bound">B</a><a id="4801" class="Symbol">}</a> <a id="4803" class="Symbol">→</a> <a id="4805" href="/20.07/PUC/2019/Assignment5/#4794" class="Bound">Γ</a> <a id="4807" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="4809" href="/20.07/PUC/2019/Assignment5/#4796" class="Bound">M</a> <a id="4811" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="4813" href="/20.07/PUC/2019/Assignment5/#4798" class="Bound">A</a> <a id="4815" class="Symbol">→</a> <a id="4817" href="/20.07/PUC/2019/Assignment5/#4794" class="Bound">Γ</a> <a id="4819" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="4821" href="/20.07/PUC/2019/Assignment5/#4796" class="Bound">M</a> <a id="4823" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="4825" href="/20.07/PUC/2019/Assignment5/#4800" class="Bound">B</a> <a id="4827" class="Symbol">→</a> <a id="4829" href="/20.07/PUC/2019/Assignment5/#4798" class="Bound">A</a> <a id="4831" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4833" href="/20.07/PUC/2019/Assignment5/#4800" class="Bound">B</a>
<a id="4837" href="/20.07/PUC/2019/Assignment5/#4782" class="Function">uniq-↑</a> <a id="4844" class="Symbol">(</a><a id="4845" href="/20.07/PUC/2019/Assignment5/#2958" class="InductiveConstructor">⊢`</a> <a id="4848" href="/20.07/PUC/2019/Assignment5/#4848" class="Bound">∋x</a><a id="4850" class="Symbol">)</a> <a id="4852" class="Symbol">(</a><a id="4853" href="/20.07/PUC/2019/Assignment5/#2958" class="InductiveConstructor">⊢`</a> <a id="4856" href="/20.07/PUC/2019/Assignment5/#4856" class="Bound">∋x′</a><a id="4859" class="Symbol">)</a> <a id="4867" class="Symbol">=</a> <a id="4870" href="/20.07/PUC/2019/Assignment5/#4513" class="Function">uniq-∋</a> <a id="4877" href="/20.07/PUC/2019/Assignment5/#4848" class="Bound">∋x</a> <a id="4880" href="/20.07/PUC/2019/Assignment5/#4856" class="Bound">∋x′</a>
<a id="4886" href="/20.07/PUC/2019/Assignment5/#4782" class="Function">uniq-↑</a> <a id="4893" class="Symbol">(</a><a id="4894" href="/20.07/PUC/2019/Assignment5/#4894" class="Bound">⊢L</a> <a id="4897" href="/20.07/PUC/2019/Assignment5/#3036" class="InductiveConstructor Operator">·</a> <a id="4899" href="/20.07/PUC/2019/Assignment5/#4899" class="Bound">⊢M</a><a id="4901" class="Symbol">)</a> <a id="4903" class="Symbol">(</a><a id="4904" href="/20.07/PUC/2019/Assignment5/#4904" class="Bound">⊢L′</a> <a id="4908" href="/20.07/PUC/2019/Assignment5/#3036" class="InductiveConstructor Operator">·</a> <a id="4910" href="/20.07/PUC/2019/Assignment5/#4910" class="Bound">⊢M′</a><a id="4913" class="Symbol">)</a> <a id="4916" class="Symbol">=</a> <a id="4919" href="/20.07/PUC/2019/Assignment5/#4376" class="Function">rng≡</a> <a id="4924" class="Symbol">(</a><a id="4925" href="/20.07/PUC/2019/Assignment5/#4782" class="Function">uniq-↑</a> <a id="4932" href="/20.07/PUC/2019/Assignment5/#4894" class="Bound">⊢L</a> <a id="4935" href="/20.07/PUC/2019/Assignment5/#4904" class="Bound">⊢L′</a><a id="4938" class="Symbol">)</a>
<a id="4942" href="/20.07/PUC/2019/Assignment5/#4782" class="Function">uniq-↑</a> <a id="4949" class="Symbol">(</a><a id="4950" href="/20.07/PUC/2019/Assignment5/#3145" class="InductiveConstructor">⊢↓</a> <a id="4953" href="/20.07/PUC/2019/Assignment5/#4953" class="Bound">⊢M</a><a id="4955" class="Symbol">)</a> <a id="4957" class="Symbol">(</a><a id="4958" href="/20.07/PUC/2019/Assignment5/#3145" class="InductiveConstructor">⊢↓</a> <a id="4961" href="/20.07/PUC/2019/Assignment5/#4961" class="Bound">⊢M′</a><a id="4964" class="Symbol">)</a> <a id="4972" class="Symbol">=</a> <a id="4975" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre>
<h2 id="lookup-type-of-a-variable-in-the-context">Lookup type of a variable in the context</h2>
<pre class="Agda"> <a id="Inference.ext∋"></a><a id="5036" href="/20.07/PUC/2019/Assignment5/#5036" class="Function">ext∋</a> <a id="5041" class="Symbol">:</a> <a id="5043" class="Symbol">∀</a> <a id="5045" class="Symbol">{</a><a id="5046" href="/20.07/PUC/2019/Assignment5/#5046" class="Bound">Γ</a> <a id="5048" href="/20.07/PUC/2019/Assignment5/#5048" class="Bound">B</a> <a id="5050" href="/20.07/PUC/2019/Assignment5/#5050" class="Bound">x</a> <a id="5052" href="/20.07/PUC/2019/Assignment5/#5052" class="Bound">y</a><a id="5053" class="Symbol">}</a>
<a id="5059" class="Symbol">→</a> <a id="5061" href="/20.07/PUC/2019/Assignment5/#5050" class="Bound">x</a> <a id="5063" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#799" class="Function Operator">≢</a> <a id="5065" href="/20.07/PUC/2019/Assignment5/#5052" class="Bound">y</a>
<a id="5071" class="Symbol">→</a> <a id="5073" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5075" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃[</a> <a id="5078" href="/20.07/PUC/2019/Assignment5/#5078" class="Bound">A</a> <a id="5080" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">]</a><a id="5081" class="Symbol">(</a> <a id="5083" href="/20.07/PUC/2019/Assignment5/#5046" class="Bound">Γ</a> <a id="5085" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">∋</a> <a id="5087" href="/20.07/PUC/2019/Assignment5/#5050" class="Bound">x</a> <a id="5089" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">⦂</a> <a id="5091" href="/20.07/PUC/2019/Assignment5/#5078" class="Bound">A</a> <a id="5093" class="Symbol">)</a>
<a id="5101" class="Comment">-----------------------------</a>
<a id="5135" class="Symbol">→</a> <a id="5137" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5139" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃[</a> <a id="5142" href="/20.07/PUC/2019/Assignment5/#5142" class="Bound">A</a> <a id="5144" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">]</a><a id="5145" class="Symbol">(</a> <a id="5147" href="/20.07/PUC/2019/Assignment5/#5046" class="Bound">Γ</a> <a id="5149" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="5151" href="/20.07/PUC/2019/Assignment5/#5052" class="Bound">y</a> <a id="5153" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="5155" href="/20.07/PUC/2019/Assignment5/#5048" class="Bound">B</a> <a id="5157" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">∋</a> <a id="5159" href="/20.07/PUC/2019/Assignment5/#5050" class="Bound">x</a> <a id="5161" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">⦂</a> <a id="5163" href="/20.07/PUC/2019/Assignment5/#5142" class="Bound">A</a> <a id="5165" class="Symbol">)</a>
<a id="5169" href="/20.07/PUC/2019/Assignment5/#5036" class="Function">ext∋</a> <a id="5174" href="/20.07/PUC/2019/Assignment5/#5174" class="Bound">x≢y</a> <a id="5178" class="Symbol">_</a> <a id="5181" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5183" href="/20.07/PUC/2019/Assignment5/#5183" class="Bound">A</a> <a id="5185" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5187" href="/20.07/PUC/2019/Assignment5/#2627" class="InductiveConstructor">Z</a> <a id="5189" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5197" class="Symbol">=</a> <a id="5200" href="/20.07/PUC/2019/Assignment5/#5174" class="Bound">x≢y</a> <a id="5204" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="5211" href="/20.07/PUC/2019/Assignment5/#5036" class="Function">ext∋</a> <a id="5216" class="Symbol">_</a> <a id="5220" href="/20.07/PUC/2019/Assignment5/#5220" class="Bound">¬∃</a> <a id="5223" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5225" href="/20.07/PUC/2019/Assignment5/#5225" class="Bound">A</a> <a id="5227" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5229" href="/20.07/PUC/2019/Assignment5/#2701" class="InductiveConstructor">S</a> <a id="5231" class="Symbol">_</a> <a id="5233" href="/20.07/PUC/2019/Assignment5/#5233" class="Bound">⊢x</a> <a id="5236" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5239" class="Symbol">=</a> <a id="5242" href="/20.07/PUC/2019/Assignment5/#5220" class="Bound">¬∃</a> <a id="5245" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5247" href="/20.07/PUC/2019/Assignment5/#5225" class="Bound">A</a> <a id="5249" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5251" href="/20.07/PUC/2019/Assignment5/#5233" class="Bound">⊢x</a> <a id="5254" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="Inference.lookup"></a><a id="5259" href="/20.07/PUC/2019/Assignment5/#5259" class="Function">lookup</a> <a id="5266" class="Symbol">:</a> <a id="5268" class="Symbol">∀</a> <a id="5270" class="Symbol">(</a><a id="5271" href="/20.07/PUC/2019/Assignment5/#5271" class="Bound">Γ</a> <a id="5273" class="Symbol">:</a> <a id="5275" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a><a id="5282" class="Symbol">)</a> <a id="5284" class="Symbol">(</a><a id="5285" href="/20.07/PUC/2019/Assignment5/#5285" class="Bound">x</a> <a id="5287" class="Symbol">:</a> <a id="5289" href="/20.07/PUC/2019/Assignment5/#1521" class="Function">Id</a><a id="5291" class="Symbol">)</a>
<a id="5299" class="Comment">-----------------------</a>
<a id="5327" class="Symbol">→</a> <a id="5329" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a> <a id="5333" class="Symbol">(</a><a id="5334" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃[</a> <a id="5337" href="/20.07/PUC/2019/Assignment5/#5337" class="Bound">A</a> <a id="5339" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">]</a><a id="5340" class="Symbol">(</a><a id="5341" href="/20.07/PUC/2019/Assignment5/#5271" class="Bound">Γ</a> <a id="5343" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">∋</a> <a id="5345" href="/20.07/PUC/2019/Assignment5/#5285" class="Bound">x</a> <a id="5347" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">⦂</a> <a id="5349" href="/20.07/PUC/2019/Assignment5/#5337" class="Bound">A</a><a id="5350" class="Symbol">))</a>
<a id="5355" href="/20.07/PUC/2019/Assignment5/#5259" class="Function">lookup</a> <a id="5362" href="/20.07/PUC/2019/Assignment5/#1649" class="InductiveConstructor">∅</a> <a id="5364" href="/20.07/PUC/2019/Assignment5/#5364" class="Bound">x</a> <a id="5389" class="Symbol">=</a> <a id="5392" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="5396" class="Symbol">(λ</a> <a id="5399" class="Symbol">())</a>
<a id="5405" href="/20.07/PUC/2019/Assignment5/#5259" class="Function">lookup</a> <a id="5412" class="Symbol">(</a><a id="5413" href="/20.07/PUC/2019/Assignment5/#5413" class="Bound">Γ</a> <a id="5415" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="5417" href="/20.07/PUC/2019/Assignment5/#5417" class="Bound">y</a> <a id="5419" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="5421" href="/20.07/PUC/2019/Assignment5/#5421" class="Bound">B</a><a id="5422" class="Symbol">)</a> <a id="5424" href="/20.07/PUC/2019/Assignment5/#5424" class="Bound">x</a> <a id="5426" class="Keyword">with</a> <a id="5431" href="/20.07/PUC/2019/Assignment5/#5424" class="Bound">x</a> <a id="5433" href="https://agda.github.io/agda-stdlib/v1.1/Data.String.Properties.html#2569" class="Function Operator">≟</a> <a id="5435" href="/20.07/PUC/2019/Assignment5/#5417" class="Bound">y</a>
<a id="5439" class="Symbol">...</a> <a id="5443" class="Symbol">|</a> <a id="5445" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="5449" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="5473" class="Symbol">=</a> <a id="5476" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="5480" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5482" class="Bound">B</a> <a id="5484" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5486" href="/20.07/PUC/2019/Assignment5/#2627" class="InductiveConstructor">Z</a> <a id="5488" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="5492" class="Symbol">...</a> <a id="5496" class="Symbol">|</a> <a id="5498" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="5501" href="/20.07/PUC/2019/Assignment5/#5501" class="Bound">x≢y</a> <a id="5505" class="Keyword">with</a> <a id="5510" href="/20.07/PUC/2019/Assignment5/#5259" class="Function">lookup</a> <a id="5517" class="Bound">Γ</a> <a id="5519" class="Bound">x</a>
<a id="5523" class="Symbol">...</a> <a id="5539" class="Symbol">|</a> <a id="5541" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="5545" href="/20.07/PUC/2019/Assignment5/#5545" class="Bound">¬∃</a> <a id="5557" class="Symbol">=</a> <a id="5560" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="5564" class="Symbol">(</a><a id="5565" href="/20.07/PUC/2019/Assignment5/#5036" class="Function">ext∋</a> <a id="5570" class="Bound">x≢y</a> <a id="5574" href="/20.07/PUC/2019/Assignment5/#5545" class="Bound">¬∃</a><a id="5576" class="Symbol">)</a>
<a id="5580" class="Symbol">...</a> <a id="5596" class="Symbol">|</a> <a id="5598" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="5602" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5604" href="/20.07/PUC/2019/Assignment5/#5604" class="Bound">A</a> <a id="5606" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5608" href="/20.07/PUC/2019/Assignment5/#5608" class="Bound">⊢x</a> <a id="5611" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5614" class="Symbol">=</a> <a id="5617" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="5621" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5623" href="/20.07/PUC/2019/Assignment5/#5604" class="Bound">A</a> <a id="5625" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5627" href="/20.07/PUC/2019/Assignment5/#2701" class="InductiveConstructor">S</a> <a id="5629" class="Bound">x≢y</a> <a id="5633" href="/20.07/PUC/2019/Assignment5/#5608" class="Bound">⊢x</a> <a id="5636" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
</pre>
<h3 id="promoting-negations">Promoting negations</h3>
<pre class="Agda"> <a id="Inference.¬arg"></a><a id="5674" href="/20.07/PUC/2019/Assignment5/#5674" class="Function">¬arg</a> <a id="5679" class="Symbol">:</a> <a id="5681" class="Symbol">∀</a> <a id="5683" class="Symbol">{</a><a id="5684" href="/20.07/PUC/2019/Assignment5/#5684" class="Bound">Γ</a> <a id="5686" href="/20.07/PUC/2019/Assignment5/#5686" class="Bound">A</a> <a id="5688" href="/20.07/PUC/2019/Assignment5/#5688" class="Bound">B</a> <a id="5690" href="/20.07/PUC/2019/Assignment5/#5690" class="Bound">L</a> <a id="5692" href="/20.07/PUC/2019/Assignment5/#5692" class="Bound">M</a><a id="5693" class="Symbol">}</a>
<a id="5699" class="Symbol">→</a> <a id="5701" href="/20.07/PUC/2019/Assignment5/#5684" class="Bound">Γ</a> <a id="5703" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="5705" href="/20.07/PUC/2019/Assignment5/#5690" class="Bound">L</a> <a id="5707" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="5709" href="/20.07/PUC/2019/Assignment5/#5686" class="Bound">A</a> <a id="5711" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="5713" href="/20.07/PUC/2019/Assignment5/#5688" class="Bound">B</a>
<a id="5719" class="Symbol">→</a> <a id="5721" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5723" href="/20.07/PUC/2019/Assignment5/#5684" class="Bound">Γ</a> <a id="5725" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="5727" href="/20.07/PUC/2019/Assignment5/#5692" class="Bound">M</a> <a id="5729" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="5731" href="/20.07/PUC/2019/Assignment5/#5686" class="Bound">A</a>
<a id="5739" class="Comment">-------------------------</a>
<a id="5769" class="Symbol">→</a> <a id="5771" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5773" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃[</a> <a id="5776" href="/20.07/PUC/2019/Assignment5/#5776" class="Bound">B′</a> <a id="5779" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">]</a><a id="5780" class="Symbol">(</a><a id="5781" href="/20.07/PUC/2019/Assignment5/#5684" class="Bound">Γ</a> <a id="5783" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="5785" href="/20.07/PUC/2019/Assignment5/#5690" class="Bound">L</a> <a id="5787" href="/20.07/PUC/2019/Assignment5/#1832" class="InductiveConstructor Operator">·</a> <a id="5789" href="/20.07/PUC/2019/Assignment5/#5692" class="Bound">M</a> <a id="5791" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="5793" href="/20.07/PUC/2019/Assignment5/#5776" class="Bound">B′</a><a id="5795" class="Symbol">)</a>
<a id="5799" href="/20.07/PUC/2019/Assignment5/#5674" class="Function">¬arg</a> <a id="5804" href="/20.07/PUC/2019/Assignment5/#5804" class="Bound">⊢L</a> <a id="5807" href="/20.07/PUC/2019/Assignment5/#5807" class="Bound">¬⊢M</a> <a id="5811" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5813" href="/20.07/PUC/2019/Assignment5/#5813" class="Bound">B′</a> <a id="5816" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5818" href="/20.07/PUC/2019/Assignment5/#5818" class="Bound">⊢L′</a> <a id="5822" href="/20.07/PUC/2019/Assignment5/#3036" class="InductiveConstructor Operator">·</a> <a id="5824" href="/20.07/PUC/2019/Assignment5/#5824" class="Bound">⊢M′</a> <a id="5828" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5830" class="Keyword">rewrite</a> <a id="5838" href="/20.07/PUC/2019/Assignment5/#4306" class="Function">dom≡</a> <a id="5843" class="Symbol">(</a><a id="5844" href="/20.07/PUC/2019/Assignment5/#4782" class="Function">uniq-↑</a> <a id="5851" href="/20.07/PUC/2019/Assignment5/#5804" class="Bound">⊢L</a> <a id="5854" href="/20.07/PUC/2019/Assignment5/#5818" class="Bound">⊢L′</a><a id="5857" class="Symbol">)</a> <a id="5859" class="Symbol">=</a> <a id="5861" href="/20.07/PUC/2019/Assignment5/#5807" class="Bound">¬⊢M</a> <a id="5865" href="/20.07/PUC/2019/Assignment5/#5824" class="Bound">⊢M′</a>
<a id="Inference.¬switch"></a><a id="5872" href="/20.07/PUC/2019/Assignment5/#5872" class="Function">¬switch</a> <a id="5880" class="Symbol">:</a> <a id="5882" class="Symbol">∀</a> <a id="5884" class="Symbol">{</a><a id="5885" href="/20.07/PUC/2019/Assignment5/#5885" class="Bound">Γ</a> <a id="5887" href="/20.07/PUC/2019/Assignment5/#5887" class="Bound">M</a> <a id="5889" href="/20.07/PUC/2019/Assignment5/#5889" class="Bound">A</a> <a id="5891" href="/20.07/PUC/2019/Assignment5/#5891" class="Bound">B</a><a id="5892" class="Symbol">}</a>
<a id="5898" class="Symbol">→</a> <a id="5900" href="/20.07/PUC/2019/Assignment5/#5885" class="Bound">Γ</a> <a id="5902" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="5904" href="/20.07/PUC/2019/Assignment5/#5887" class="Bound">M</a> <a id="5906" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="5908" href="/20.07/PUC/2019/Assignment5/#5889" class="Bound">A</a>
<a id="5914" class="Symbol">→</a> <a id="5916" href="/20.07/PUC/2019/Assignment5/#5889" class="Bound">A</a> <a id="5918" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#799" class="Function Operator">≢</a> <a id="5920" href="/20.07/PUC/2019/Assignment5/#5891" class="Bound">B</a>
<a id="5928" class="Comment">---------------</a>
<a id="5948" class="Symbol">→</a> <a id="5950" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5952" href="/20.07/PUC/2019/Assignment5/#5885" class="Bound">Γ</a> <a id="5954" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="5956" class="Symbol">(</a><a id="5957" href="/20.07/PUC/2019/Assignment5/#5887" class="Bound">M</a> <a id="5959" href="/20.07/PUC/2019/Assignment5/#2207" class="InductiveConstructor Operator">↑</a><a id="5960" class="Symbol">)</a> <a id="5962" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="5964" href="/20.07/PUC/2019/Assignment5/#5891" class="Bound">B</a>
<a id="5968" href="/20.07/PUC/2019/Assignment5/#5872" class="Function">¬switch</a> <a id="5976" href="/20.07/PUC/2019/Assignment5/#5976" class="Bound">⊢M</a> <a id="5979" href="/20.07/PUC/2019/Assignment5/#5979" class="Bound">A≢B</a> <a id="5983" class="Symbol">(</a><a id="5984" href="/20.07/PUC/2019/Assignment5/#3792" class="InductiveConstructor">⊢↑</a> <a id="5987" href="/20.07/PUC/2019/Assignment5/#5987" class="Bound">⊢M′</a> <a id="5991" href="/20.07/PUC/2019/Assignment5/#5991" class="Bound">A′≡B</a><a id="5995" class="Symbol">)</a> <a id="5997" class="Keyword">rewrite</a> <a id="6005" href="/20.07/PUC/2019/Assignment5/#4782" class="Function">uniq-↑</a> <a id="6012" href="/20.07/PUC/2019/Assignment5/#5976" class="Bound">⊢M</a> <a id="6015" href="/20.07/PUC/2019/Assignment5/#5987" class="Bound">⊢M′</a> <a id="6019" class="Symbol">=</a> <a id="6021" href="/20.07/PUC/2019/Assignment5/#5979" class="Bound">A≢B</a> <a id="6025" href="/20.07/PUC/2019/Assignment5/#5991" class="Bound">A′≡B</a>
</pre>
<h2 id="synthesize-and-inherit-types">Synthesize and inherit types</h2>
<pre class="Agda"> <a id="Inference.synthesize"></a><a id="6075" href="/20.07/PUC/2019/Assignment5/#6075" class="Function">synthesize</a> <a id="6086" class="Symbol">:</a> <a id="6088" class="Symbol">∀</a> <a id="6090" class="Symbol">(</a><a id="6091" href="/20.07/PUC/2019/Assignment5/#6091" class="Bound">Γ</a> <a id="6093" class="Symbol">:</a> <a id="6095" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a><a id="6102" class="Symbol">)</a> <a id="6104" class="Symbol">(</a><a id="6105" href="/20.07/PUC/2019/Assignment5/#6105" class="Bound">M</a> <a id="6107" class="Symbol">:</a> <a id="6109" href="/20.07/PUC/2019/Assignment5/#1734" class="Datatype">Term⁺</a><a id="6114" class="Symbol">)</a>
<a id="6122" class="Comment">-----------------------</a>
<a id="6150" class="Symbol">→</a> <a id="6152" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a> <a id="6156" class="Symbol">(</a><a id="6157" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃[</a> <a id="6160" href="/20.07/PUC/2019/Assignment5/#6160" class="Bound">A</a> <a id="6162" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">]</a><a id="6163" class="Symbol">(</a><a id="6164" href="/20.07/PUC/2019/Assignment5/#6091" class="Bound">Γ</a> <a id="6166" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="6168" href="/20.07/PUC/2019/Assignment5/#6105" class="Bound">M</a> <a id="6170" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="6172" href="/20.07/PUC/2019/Assignment5/#6160" class="Bound">A</a><a id="6173" class="Symbol">))</a>
<a id="Inference.inherit"></a><a id="6179" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="6187" class="Symbol">:</a> <a id="6189" class="Symbol">∀</a> <a id="6191" class="Symbol">(</a><a id="6192" href="/20.07/PUC/2019/Assignment5/#6192" class="Bound">Γ</a> <a id="6194" class="Symbol">:</a> <a id="6196" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a><a id="6203" class="Symbol">)</a> <a id="6205" class="Symbol">(</a><a id="6206" href="/20.07/PUC/2019/Assignment5/#6206" class="Bound">M</a> <a id="6208" class="Symbol">:</a> <a id="6210" href="/20.07/PUC/2019/Assignment5/#1753" class="Datatype">Term⁻</a><a id="6215" class="Symbol">)</a> <a id="6217" class="Symbol">(</a><a id="6218" href="/20.07/PUC/2019/Assignment5/#6218" class="Bound">A</a> <a id="6220" class="Symbol">:</a> <a id="6222" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a><a id="6226" class="Symbol">)</a>
<a id="6234" class="Comment">---------------</a>
<a id="6254" class="Symbol">→</a> <a id="6256" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a> <a id="6260" class="Symbol">(</a><a id="6261" href="/20.07/PUC/2019/Assignment5/#6192" class="Bound">Γ</a> <a id="6263" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="6265" href="/20.07/PUC/2019/Assignment5/#6206" class="Bound">M</a> <a id="6267" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="6269" href="/20.07/PUC/2019/Assignment5/#6218" class="Bound">A</a><a id="6270" class="Symbol">)</a>
<a id="6275" href="/20.07/PUC/2019/Assignment5/#6075" class="Function">synthesize</a> <a id="6286" href="/20.07/PUC/2019/Assignment5/#6286" class="Bound">Γ</a> <a id="6288" class="Symbol">(</a><a id="6289" href="/20.07/PUC/2019/Assignment5/#1789" class="InductiveConstructor Operator">`</a> <a id="6291" href="/20.07/PUC/2019/Assignment5/#6291" class="Bound">x</a><a id="6292" class="Symbol">)</a> <a id="6294" class="Keyword">with</a> <a id="6299" href="/20.07/PUC/2019/Assignment5/#5259" class="Function">lookup</a> <a id="6306" href="/20.07/PUC/2019/Assignment5/#6286" class="Bound">Γ</a> <a id="6308" href="/20.07/PUC/2019/Assignment5/#6291" class="Bound">x</a>
<a id="6312" class="Symbol">...</a> <a id="6316" class="Symbol">|</a> <a id="6318" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6322" href="/20.07/PUC/2019/Assignment5/#6322" class="Bound">¬∃</a> <a id="6338" class="Symbol">=</a> <a id="6341" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6345" class="Symbol">(λ{</a> <a id="6349" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6351" href="/20.07/PUC/2019/Assignment5/#6351" class="Bound">A</a> <a id="6353" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6355" href="/20.07/PUC/2019/Assignment5/#2958" class="InductiveConstructor">⊢`</a> <a id="6358" href="/20.07/PUC/2019/Assignment5/#6358" class="Bound">∋x</a> <a id="6361" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6363" class="Symbol">→</a> <a id="6365" href="/20.07/PUC/2019/Assignment5/#6322" class="Bound">¬∃</a> <a id="6368" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6370" href="/20.07/PUC/2019/Assignment5/#6351" class="Bound">A</a> <a id="6372" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6374" href="/20.07/PUC/2019/Assignment5/#6358" class="Bound">∋x</a> <a id="6377" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6379" class="Symbol">})</a>
<a id="6384" class="Symbol">...</a> <a id="6388" class="Symbol">|</a> <a id="6390" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6394" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6396" href="/20.07/PUC/2019/Assignment5/#6396" class="Bound">A</a> <a id="6398" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6400" href="/20.07/PUC/2019/Assignment5/#6400" class="Bound">∋x</a> <a id="6403" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6410" class="Symbol">=</a> <a id="6413" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6417" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6419" href="/20.07/PUC/2019/Assignment5/#6396" class="Bound">A</a> <a id="6421" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6423" href="/20.07/PUC/2019/Assignment5/#2958" class="InductiveConstructor">⊢`</a> <a id="6426" href="/20.07/PUC/2019/Assignment5/#6400" class="Bound">∋x</a> <a id="6429" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="6433" href="/20.07/PUC/2019/Assignment5/#6075" class="Function">synthesize</a> <a id="6444" href="/20.07/PUC/2019/Assignment5/#6444" class="Bound">Γ</a> <a id="6446" class="Symbol">(</a><a id="6447" href="/20.07/PUC/2019/Assignment5/#6447" class="Bound">L</a> <a id="6449" href="/20.07/PUC/2019/Assignment5/#1832" class="InductiveConstructor Operator">·</a> <a id="6451" href="/20.07/PUC/2019/Assignment5/#6451" class="Bound">M</a><a id="6452" class="Symbol">)</a> <a id="6454" class="Keyword">with</a> <a id="6459" href="/20.07/PUC/2019/Assignment5/#6075" class="Function">synthesize</a> <a id="6470" href="/20.07/PUC/2019/Assignment5/#6444" class="Bound">Γ</a> <a id="6472" href="/20.07/PUC/2019/Assignment5/#6447" class="Bound">L</a>
<a id="6476" class="Symbol">...</a> <a id="6480" class="Symbol">|</a> <a id="6482" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6486" href="/20.07/PUC/2019/Assignment5/#6486" class="Bound">¬∃</a> <a id="6502" class="Symbol">=</a> <a id="6505" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6509" class="Symbol">(λ{</a> <a id="6513" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6515" class="Symbol">_</a> <a id="6517" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6519" href="/20.07/PUC/2019/Assignment5/#6519" class="Bound">⊢L</a> <a id="6523" href="/20.07/PUC/2019/Assignment5/#3036" class="InductiveConstructor Operator">·</a> <a id="6525" class="Symbol">_</a> <a id="6528" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6531" class="Symbol">→</a> <a id="6534" href="/20.07/PUC/2019/Assignment5/#6486" class="Bound">¬∃</a> <a id="6537" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6539" class="Symbol">_</a> <a id="6541" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6543" href="/20.07/PUC/2019/Assignment5/#6519" class="Bound">⊢L</a> <a id="6546" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6548" class="Symbol">})</a>
<a id="6553" class="Symbol">...</a> <a id="6557" class="Symbol">|</a> <a id="6559" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6563" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6565" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="6568" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6573" href="/20.07/PUC/2019/Assignment5/#6573" class="Bound">⊢L</a> <a id="6576" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6579" class="Symbol">=</a> <a id="6582" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6586" class="Symbol">(λ{</a> <a id="6590" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6592" class="Symbol">_</a> <a id="6594" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6596" href="/20.07/PUC/2019/Assignment5/#6596" class="Bound">⊢L′</a> <a id="6600" href="/20.07/PUC/2019/Assignment5/#3036" class="InductiveConstructor Operator">·</a> <a id="6602" class="Symbol">_</a> <a id="6605" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6608" class="Symbol">→</a> <a id="6611" href="/20.07/PUC/2019/Assignment5/#4446" class="Function">ℕ≢⇒</a> <a id="6615" class="Symbol">(</a><a id="6616" href="/20.07/PUC/2019/Assignment5/#4782" class="Function">uniq-↑</a> <a id="6623" href="/20.07/PUC/2019/Assignment5/#6573" class="Bound">⊢L</a> <a id="6626" href="/20.07/PUC/2019/Assignment5/#6596" class="Bound">⊢L′</a><a id="6629" class="Symbol">)</a> <a id="6631" class="Symbol">})</a>
<a id="6636" class="Symbol">...</a> <a id="6640" class="Symbol">|</a> <a id="6642" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6646" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6648" href="/20.07/PUC/2019/Assignment5/#6648" class="Bound">A</a> <a id="6650" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="6652" href="/20.07/PUC/2019/Assignment5/#6652" class="Bound">B</a> <a id="6654" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6656" href="/20.07/PUC/2019/Assignment5/#6656" class="Bound">⊢L</a> <a id="6659" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6661" class="Keyword">with</a> <a id="6666" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="6674" class="Bound">Γ</a> <a id="6676" class="Bound">M</a> <a id="6678" href="/20.07/PUC/2019/Assignment5/#6648" class="Bound">A</a>
<a id="6682" class="Symbol">...</a> <a id="6689" class="Symbol">|</a> <a id="6691" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6695" href="/20.07/PUC/2019/Assignment5/#6695" class="Bound">¬⊢M</a> <a id="6708" class="Symbol">=</a> <a id="6711" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6715" class="Symbol">(</a><a id="6716" href="/20.07/PUC/2019/Assignment5/#5674" class="Function">¬arg</a> <a id="6721" class="Bound">⊢L</a> <a id="6724" href="/20.07/PUC/2019/Assignment5/#6695" class="Bound">¬⊢M</a><a id="6727" class="Symbol">)</a>
<a id="6731" class="Symbol">...</a> <a id="6738" class="Symbol">|</a> <a id="6740" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6744" href="/20.07/PUC/2019/Assignment5/#6744" class="Bound">⊢M</a> <a id="6757" class="Symbol">=</a> <a id="6760" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6764" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6766" class="Bound">B</a> <a id="6768" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6770" class="Bound">⊢L</a> <a id="6773" href="/20.07/PUC/2019/Assignment5/#3036" class="InductiveConstructor Operator">·</a> <a id="6775" href="/20.07/PUC/2019/Assignment5/#6744" class="Bound">⊢M</a> <a id="6778" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="6782" href="/20.07/PUC/2019/Assignment5/#6075" class="Function">synthesize</a> <a id="6793" href="/20.07/PUC/2019/Assignment5/#6793" class="Bound">Γ</a> <a id="6795" class="Symbol">(</a><a id="6796" href="/20.07/PUC/2019/Assignment5/#6796" class="Bound">M</a> <a id="6798" href="/20.07/PUC/2019/Assignment5/#1886" class="InductiveConstructor Operator">↓</a> <a id="6800" href="/20.07/PUC/2019/Assignment5/#6800" class="Bound">A</a><a id="6801" class="Symbol">)</a> <a id="6803" class="Keyword">with</a> <a id="6808" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="6816" href="/20.07/PUC/2019/Assignment5/#6793" class="Bound">Γ</a> <a id="6818" href="/20.07/PUC/2019/Assignment5/#6796" class="Bound">M</a> <a id="6820" href="/20.07/PUC/2019/Assignment5/#6800" class="Bound">A</a>
<a id="6824" class="Symbol">...</a> <a id="6828" class="Symbol">|</a> <a id="6830" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6834" href="/20.07/PUC/2019/Assignment5/#6834" class="Bound">¬⊢M</a> <a id="6850" class="Symbol">=</a> <a id="6853" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6857" class="Symbol">(λ{</a> <a id="6861" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6863" class="Symbol">_</a> <a id="6865" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6867" href="/20.07/PUC/2019/Assignment5/#3145" class="InductiveConstructor">⊢↓</a> <a id="6870" href="/20.07/PUC/2019/Assignment5/#6870" class="Bound">⊢M</a> <a id="6873" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6876" class="Symbol">→</a> <a id="6879" href="/20.07/PUC/2019/Assignment5/#6834" class="Bound">¬⊢M</a> <a id="6883" href="/20.07/PUC/2019/Assignment5/#6870" class="Bound">⊢M</a> <a id="6886" class="Symbol">})</a>
<a id="6891" class="Symbol">...</a> <a id="6895" class="Symbol">|</a> <a id="6897" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6901" href="/20.07/PUC/2019/Assignment5/#6901" class="Bound">⊢M</a> <a id="6917" class="Symbol">=</a> <a id="6920" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6924" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6926" class="Bound">A</a> <a id="6928" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6930" href="/20.07/PUC/2019/Assignment5/#3145" class="InductiveConstructor">⊢↓</a> <a id="6933" href="/20.07/PUC/2019/Assignment5/#6901" class="Bound">⊢M</a> <a id="6936" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="6941" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="6949" href="/20.07/PUC/2019/Assignment5/#6949" class="Bound">Γ</a> <a id="6951" class="Symbol">(</a><a id="6952" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">ƛ</a> <a id="6954" href="/20.07/PUC/2019/Assignment5/#6954" class="Bound">x</a> <a id="6956" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">⇒</a> <a id="6958" href="/20.07/PUC/2019/Assignment5/#6958" class="Bound">N</a><a id="6959" class="Symbol">)</a> <a id="6961" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="6969" class="Symbol">=</a> <a id="6972" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6976" class="Symbol">(λ())</a>
<a id="6984" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="6992" href="/20.07/PUC/2019/Assignment5/#6992" class="Bound">Γ</a> <a id="6994" class="Symbol">(</a><a id="6995" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">ƛ</a> <a id="6997" href="/20.07/PUC/2019/Assignment5/#6997" class="Bound">x</a> <a id="6999" href="/20.07/PUC/2019/Assignment5/#1959" class="InductiveConstructor Operator">⇒</a> <a id="7001" href="/20.07/PUC/2019/Assignment5/#7001" class="Bound">N</a><a id="7002" class="Symbol">)</a> <a id="7004" class="Symbol">(</a><a id="7005" href="/20.07/PUC/2019/Assignment5/#7005" class="Bound">A</a> <a id="7007" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="7009" href="/20.07/PUC/2019/Assignment5/#7009" class="Bound">B</a><a id="7010" class="Symbol">)</a> <a id="7012" class="Keyword">with</a> <a id="7017" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7025" class="Symbol">(</a><a id="7026" href="/20.07/PUC/2019/Assignment5/#6992" class="Bound">Γ</a> <a id="7028" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="7030" href="/20.07/PUC/2019/Assignment5/#6997" class="Bound">x</a> <a id="7032" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="7034" href="/20.07/PUC/2019/Assignment5/#7005" class="Bound">A</a><a id="7035" class="Symbol">)</a> <a id="7037" href="/20.07/PUC/2019/Assignment5/#7001" class="Bound">N</a> <a id="7039" href="/20.07/PUC/2019/Assignment5/#7009" class="Bound">B</a>
<a id="7043" class="Symbol">...</a> <a id="7047" class="Symbol">|</a> <a id="7049" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7052" href="/20.07/PUC/2019/Assignment5/#7052" class="Bound">¬⊢N</a> <a id="7071" class="Symbol">=</a> <a id="7074" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7078" class="Symbol">(λ{</a> <a id="7082" class="Symbol">(</a><a id="7083" href="/20.07/PUC/2019/Assignment5/#3251" class="InductiveConstructor">⊢ƛ</a> <a id="7086" href="/20.07/PUC/2019/Assignment5/#7086" class="Bound">⊢N</a><a id="7088" class="Symbol">)</a> <a id="7091" class="Symbol">→</a> <a id="7094" href="/20.07/PUC/2019/Assignment5/#7052" class="Bound">¬⊢N</a> <a id="7098" href="/20.07/PUC/2019/Assignment5/#7086" class="Bound">⊢N</a> <a id="7101" class="Symbol">})</a>
<a id="7106" class="Symbol">...</a> <a id="7110" class="Symbol">|</a> <a id="7112" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="7116" href="/20.07/PUC/2019/Assignment5/#7116" class="Bound">⊢N</a> <a id="7134" class="Symbol">=</a> <a id="7137" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="7141" class="Symbol">(</a><a id="7142" href="/20.07/PUC/2019/Assignment5/#3251" class="InductiveConstructor">⊢ƛ</a> <a id="7145" href="/20.07/PUC/2019/Assignment5/#7116" class="Bound">⊢N</a><a id="7147" class="Symbol">)</a>
<a id="7151" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7159" href="/20.07/PUC/2019/Assignment5/#7159" class="Bound">Γ</a> <a id="7161" href="/20.07/PUC/2019/Assignment5/#2009" class="InductiveConstructor">`zero</a> <a id="7167" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="7179" class="Symbol">=</a> <a id="7182" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="7186" href="/20.07/PUC/2019/Assignment5/#3357" class="InductiveConstructor">⊢zero</a>
<a id="7194" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7202" href="/20.07/PUC/2019/Assignment5/#7202" class="Bound">Γ</a> <a id="7204" href="/20.07/PUC/2019/Assignment5/#2009" class="InductiveConstructor">`zero</a> <a id="7210" class="Symbol">(</a><a id="7211" href="/20.07/PUC/2019/Assignment5/#7211" class="Bound">A</a> <a id="7213" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="7215" href="/20.07/PUC/2019/Assignment5/#7215" class="Bound">B</a><a id="7216" class="Symbol">)</a> <a id="7222" class="Symbol">=</a> <a id="7225" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7229" class="Symbol">(λ())</a>
<a id="7237" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7245" href="/20.07/PUC/2019/Assignment5/#7245" class="Bound">Γ</a> <a id="7247" class="Symbol">(</a><a id="7248" href="/20.07/PUC/2019/Assignment5/#2046" class="InductiveConstructor Operator">`suc</a> <a id="7253" href="/20.07/PUC/2019/Assignment5/#7253" class="Bound">M</a><a id="7254" class="Symbol">)</a> <a id="7256" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="7259" class="Keyword">with</a> <a id="7264" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7272" href="/20.07/PUC/2019/Assignment5/#7245" class="Bound">Γ</a> <a id="7274" href="/20.07/PUC/2019/Assignment5/#7253" class="Bound">M</a> <a id="7276" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a>
<a id="7281" class="Symbol">...</a> <a id="7285" class="Symbol">|</a> <a id="7287" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7290" href="/20.07/PUC/2019/Assignment5/#7290" class="Bound">¬⊢M</a> <a id="7309" class="Symbol">=</a> <a id="7312" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7316" class="Symbol">(λ{</a> <a id="7320" class="Symbol">(</a><a id="7321" href="/20.07/PUC/2019/Assignment5/#3422" class="InductiveConstructor">⊢suc</a> <a id="7326" href="/20.07/PUC/2019/Assignment5/#7326" class="Bound">⊢M</a><a id="7328" class="Symbol">)</a> <a id="7331" class="Symbol">→</a> <a id="7334" href="/20.07/PUC/2019/Assignment5/#7290" class="Bound">¬⊢M</a> <a id="7338" href="/20.07/PUC/2019/Assignment5/#7326" class="Bound">⊢M</a> <a id="7341" class="Symbol">})</a>
<a id="7346" class="Symbol">...</a> <a id="7350" class="Symbol">|</a> <a id="7352" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="7356" href="/20.07/PUC/2019/Assignment5/#7356" class="Bound">⊢M</a> <a id="7374" class="Symbol">=</a> <a id="7377" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="7381" class="Symbol">(</a><a id="7382" href="/20.07/PUC/2019/Assignment5/#3422" class="InductiveConstructor">⊢suc</a> <a id="7387" href="/20.07/PUC/2019/Assignment5/#7356" class="Bound">⊢M</a><a id="7389" class="Symbol">)</a>
<a id="7393" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7401" href="/20.07/PUC/2019/Assignment5/#7401" class="Bound">Γ</a> <a id="7403" class="Symbol">(</a><a id="7404" href="/20.07/PUC/2019/Assignment5/#2046" class="InductiveConstructor Operator">`suc</a> <a id="7409" href="/20.07/PUC/2019/Assignment5/#7409" class="Bound">M</a><a id="7410" class="Symbol">)</a> <a id="7412" class="Symbol">(</a><a id="7413" href="/20.07/PUC/2019/Assignment5/#7413" class="Bound">A</a> <a id="7415" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="7417" href="/20.07/PUC/2019/Assignment5/#7417" class="Bound">B</a><a id="7418" class="Symbol">)</a> <a id="7421" class="Symbol">=</a> <a id="7424" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7428" class="Symbol">(λ())</a>
<a id="7436" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7444" href="/20.07/PUC/2019/Assignment5/#7444" class="Bound">Γ</a> <a id="7446" class="Symbol">(</a><a id="7447" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">`case</a> <a id="7453" href="/20.07/PUC/2019/Assignment5/#7453" class="Bound">L</a> <a id="7455" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">[zero⇒</a> <a id="7462" href="/20.07/PUC/2019/Assignment5/#7462" class="Bound">M</a> <a id="7464" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">|suc</a> <a id="7469" href="/20.07/PUC/2019/Assignment5/#7469" class="Bound">x</a> <a id="7471" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">⇒</a> <a id="7473" href="/20.07/PUC/2019/Assignment5/#7473" class="Bound">N</a> <a id="7475" href="/20.07/PUC/2019/Assignment5/#2091" class="InductiveConstructor Operator">]</a><a id="7476" class="Symbol">)</a> <a id="7478" href="/20.07/PUC/2019/Assignment5/#7478" class="Bound">A</a> <a id="7480" class="Keyword">with</a> <a id="7485" href="/20.07/PUC/2019/Assignment5/#6075" class="Function">synthesize</a> <a id="7496" href="/20.07/PUC/2019/Assignment5/#7444" class="Bound">Γ</a> <a id="7498" href="/20.07/PUC/2019/Assignment5/#7453" class="Bound">L</a>
<a id="7502" class="Symbol">...</a> <a id="7506" class="Symbol">|</a> <a id="7508" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7511" href="/20.07/PUC/2019/Assignment5/#7511" class="Bound">¬∃</a> <a id="7530" class="Symbol">=</a> <a id="7533" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7537" class="Symbol">(λ{</a> <a id="7541" class="Symbol">(</a><a id="7542" href="/20.07/PUC/2019/Assignment5/#3509" class="InductiveConstructor">⊢case</a> <a id="7548" href="/20.07/PUC/2019/Assignment5/#7548" class="Bound">⊢L</a> <a id="7552" class="Symbol">_</a> <a id="7554" class="Symbol">_)</a> <a id="7557" class="Symbol">→</a> <a id="7559" href="/20.07/PUC/2019/Assignment5/#7511" class="Bound">¬∃</a> <a id="7562" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7564" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="7567" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7569" href="/20.07/PUC/2019/Assignment5/#7548" class="Bound">⊢L</a> <a id="7572" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a><a id="7573" class="Symbol">})</a>
<a id="7578" class="Symbol">...</a> <a id="7582" class="Symbol">|</a> <a id="7584" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="7588" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7590" class="Symbol">_</a> <a id="7592" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="7594" class="Symbol">_</a> <a id="7596" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7598" href="/20.07/PUC/2019/Assignment5/#7598" class="Bound">⊢L</a> <a id="7601" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7606" class="Symbol">=</a> <a id="7609" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7613" class="Symbol">(λ{</a> <a id="7617" class="Symbol">(</a><a id="7618" href="/20.07/PUC/2019/Assignment5/#3509" class="InductiveConstructor">⊢case</a> <a id="7624" href="/20.07/PUC/2019/Assignment5/#7624" class="Bound">⊢L′</a> <a id="7628" class="Symbol">_</a> <a id="7630" class="Symbol">_)</a> <a id="7633" class="Symbol">→</a> <a id="7635" href="/20.07/PUC/2019/Assignment5/#4446" class="Function">ℕ≢⇒</a> <a id="7639" class="Symbol">(</a><a id="7640" href="/20.07/PUC/2019/Assignment5/#4782" class="Function">uniq-↑</a> <a id="7647" href="/20.07/PUC/2019/Assignment5/#7624" class="Bound">⊢L′</a> <a id="7651" href="/20.07/PUC/2019/Assignment5/#7598" class="Bound">⊢L</a><a id="7653" class="Symbol">)</a> <a id="7655" class="Symbol">})</a>
<a id="7660" class="Symbol">...</a> <a id="7664" class="Symbol">|</a> <a id="7666" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="7670" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="7672" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="7675" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="7680" href="/20.07/PUC/2019/Assignment5/#7680" class="Bound">⊢L</a> <a id="7683" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="7685" class="Keyword">with</a> <a id="7690" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7698" class="Bound">Γ</a> <a id="7700" class="Bound">M</a> <a id="7702" class="Bound">A</a>
<a id="7706" class="Symbol">...</a> <a id="7713" class="Symbol">|</a> <a id="7715" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7718" href="/20.07/PUC/2019/Assignment5/#7718" class="Bound">¬⊢M</a> <a id="7734" class="Symbol">=</a> <a id="7737" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7741" class="Symbol">(λ{</a> <a id="7745" class="Symbol">(</a><a id="7746" href="/20.07/PUC/2019/Assignment5/#3509" class="InductiveConstructor">⊢case</a> <a id="7752" class="Symbol">_</a> <a id="7754" href="/20.07/PUC/2019/Assignment5/#7754" class="Bound">⊢M</a> <a id="7757" class="Symbol">_)</a> <a id="7760" class="Symbol">→</a> <a id="7762" href="/20.07/PUC/2019/Assignment5/#7718" class="Bound">¬⊢M</a> <a id="7766" href="/20.07/PUC/2019/Assignment5/#7754" class="Bound">⊢M</a> <a id="7769" class="Symbol">})</a>
<a id="7774" class="Symbol">...</a> <a id="7781" class="Symbol">|</a> <a id="7783" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="7787" href="/20.07/PUC/2019/Assignment5/#7787" class="Bound">⊢M</a> <a id="7790" class="Keyword">with</a> <a id="7795" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7803" class="Symbol">(</a><a id="7804" class="Bound">Γ</a> <a id="7806" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="7808" class="Bound">x</a> <a id="7810" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="7812" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a><a id="7814" class="Symbol">)</a> <a id="7816" class="Bound">N</a> <a id="7818" class="Bound">A</a>
<a id="7822" class="Symbol">...</a> <a id="7832" class="Symbol">|</a> <a id="7834" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7837" href="/20.07/PUC/2019/Assignment5/#7837" class="Bound">¬⊢N</a> <a id="7850" class="Symbol">=</a> <a id="7853" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="7857" class="Symbol">(λ{</a> <a id="7861" class="Symbol">(</a><a id="7862" href="/20.07/PUC/2019/Assignment5/#3509" class="InductiveConstructor">⊢case</a> <a id="7868" class="Symbol">_</a> <a id="7870" class="Symbol">_</a> <a id="7872" href="/20.07/PUC/2019/Assignment5/#7872" class="Bound">⊢N</a><a id="7874" class="Symbol">)</a> <a id="7876" class="Symbol">→</a> <a id="7878" href="/20.07/PUC/2019/Assignment5/#7837" class="Bound">¬⊢N</a> <a id="7882" href="/20.07/PUC/2019/Assignment5/#7872" class="Bound">⊢N</a> <a id="7885" class="Symbol">})</a>
<a id="7890" class="Symbol">...</a> <a id="7900" class="Symbol">|</a> <a id="7902" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="7906" href="/20.07/PUC/2019/Assignment5/#7906" class="Bound">⊢N</a> <a id="7918" class="Symbol">=</a> <a id="7921" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="7925" class="Symbol">(</a><a id="7926" href="/20.07/PUC/2019/Assignment5/#3509" class="InductiveConstructor">⊢case</a> <a id="7932" class="Bound">⊢L</a> <a id="7935" class="Bound">⊢M</a> <a id="7938" href="/20.07/PUC/2019/Assignment5/#7906" class="Bound">⊢N</a><a id="7940" class="Symbol">)</a>
<a id="7944" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7952" href="/20.07/PUC/2019/Assignment5/#7952" class="Bound">Γ</a> <a id="7954" class="Symbol">(</a><a id="7955" href="/20.07/PUC/2019/Assignment5/#2157" class="InductiveConstructor Operator">μ</a> <a id="7957" href="/20.07/PUC/2019/Assignment5/#7957" class="Bound">x</a> <a id="7959" href="/20.07/PUC/2019/Assignment5/#2157" class="InductiveConstructor Operator">⇒</a> <a id="7961" href="/20.07/PUC/2019/Assignment5/#7961" class="Bound">N</a><a id="7962" class="Symbol">)</a> <a id="7964" href="/20.07/PUC/2019/Assignment5/#7964" class="Bound">A</a> <a id="7966" class="Keyword">with</a> <a id="7971" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="7979" class="Symbol">(</a><a id="7980" href="/20.07/PUC/2019/Assignment5/#7952" class="Bound">Γ</a> <a id="7982" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="7984" href="/20.07/PUC/2019/Assignment5/#7957" class="Bound">x</a> <a id="7986" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="7988" href="/20.07/PUC/2019/Assignment5/#7964" class="Bound">A</a><a id="7989" class="Symbol">)</a> <a id="7991" href="/20.07/PUC/2019/Assignment5/#7961" class="Bound">N</a> <a id="7993" href="/20.07/PUC/2019/Assignment5/#7964" class="Bound">A</a>
<a id="7997" class="Symbol">...</a> <a id="8001" class="Symbol">|</a> <a id="8003" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="8006" href="/20.07/PUC/2019/Assignment5/#8006" class="Bound">¬⊢N</a> <a id="8025" class="Symbol">=</a> <a id="8028" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="8032" class="Symbol">(λ{</a> <a id="8036" class="Symbol">(</a><a id="8037" href="/20.07/PUC/2019/Assignment5/#3694" class="InductiveConstructor">⊢μ</a> <a id="8040" href="/20.07/PUC/2019/Assignment5/#8040" class="Bound">⊢N</a><a id="8042" class="Symbol">)</a> <a id="8044" class="Symbol">→</a> <a id="8046" href="/20.07/PUC/2019/Assignment5/#8006" class="Bound">¬⊢N</a> <a id="8050" href="/20.07/PUC/2019/Assignment5/#8040" class="Bound">⊢N</a> <a id="8053" class="Symbol">})</a>
<a id="8058" class="Symbol">...</a> <a id="8062" class="Symbol">|</a> <a id="8064" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="8068" href="/20.07/PUC/2019/Assignment5/#8068" class="Bound">⊢N</a> <a id="8086" class="Symbol">=</a> <a id="8089" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="8093" class="Symbol">(</a><a id="8094" href="/20.07/PUC/2019/Assignment5/#3694" class="InductiveConstructor">⊢μ</a> <a id="8097" href="/20.07/PUC/2019/Assignment5/#8068" class="Bound">⊢N</a><a id="8099" class="Symbol">)</a>
<a id="8103" href="/20.07/PUC/2019/Assignment5/#6179" class="Function">inherit</a> <a id="8111" href="/20.07/PUC/2019/Assignment5/#8111" class="Bound">Γ</a> <a id="8113" class="Symbol">(</a><a id="8114" href="/20.07/PUC/2019/Assignment5/#8114" class="Bound">M</a> <a id="8116" href="/20.07/PUC/2019/Assignment5/#2207" class="InductiveConstructor Operator">↑</a><a id="8117" class="Symbol">)</a> <a id="8119" href="/20.07/PUC/2019/Assignment5/#8119" class="Bound">B</a> <a id="8121" class="Keyword">with</a> <a id="8126" href="/20.07/PUC/2019/Assignment5/#6075" class="Function">synthesize</a> <a id="8137" href="/20.07/PUC/2019/Assignment5/#8111" class="Bound">Γ</a> <a id="8139" href="/20.07/PUC/2019/Assignment5/#8114" class="Bound">M</a>
<a id="8143" class="Symbol">...</a> <a id="8147" class="Symbol">|</a> <a id="8149" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="8153" href="/20.07/PUC/2019/Assignment5/#8153" class="Bound">¬∃</a> <a id="8171" class="Symbol">=</a> <a id="8174" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="8178" class="Symbol">(λ{</a> <a id="8182" class="Symbol">(</a><a id="8183" href="/20.07/PUC/2019/Assignment5/#3792" class="InductiveConstructor">⊢↑</a> <a id="8186" href="/20.07/PUC/2019/Assignment5/#8186" class="Bound">⊢M</a> <a id="8189" class="Symbol">_)</a> <a id="8192" class="Symbol">→</a> <a id="8194" href="/20.07/PUC/2019/Assignment5/#8153" class="Bound">¬∃</a> <a id="8197" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="8199" class="Symbol">_</a> <a id="8201" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="8203" href="/20.07/PUC/2019/Assignment5/#8186" class="Bound">⊢M</a> <a id="8206" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="8208" class="Symbol">})</a>
<a id="8213" class="Symbol">...</a> <a id="8217" class="Symbol">|</a> <a id="8219" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="8223" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="8225" href="/20.07/PUC/2019/Assignment5/#8225" class="Bound">A</a> <a id="8227" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="8229" href="/20.07/PUC/2019/Assignment5/#8229" class="Bound">⊢M</a> <a id="8232" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="8234" class="Keyword">with</a> <a id="8239" href="/20.07/PUC/2019/Assignment5/#8225" class="Bound">A</a> <a id="8241" href="/20.07/PUC/2019/Assignment5/#3916" class="Function Operator">≟Tp</a> <a id="8245" class="Bound">B</a>
<a id="8249" class="Symbol">...</a> <a id="8255" class="Symbol">|</a> <a id="8257" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="8261" href="/20.07/PUC/2019/Assignment5/#8261" class="Bound">A≢B</a> <a id="8277" class="Symbol">=</a> <a id="8280" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="8284" class="Symbol">(</a><a id="8285" href="/20.07/PUC/2019/Assignment5/#5872" class="Function">¬switch</a> <a id="8293" class="Bound">⊢M</a> <a id="8296" href="/20.07/PUC/2019/Assignment5/#8261" class="Bound">A≢B</a><a id="8299" class="Symbol">)</a>
<a id="8303" class="Symbol">...</a> <a id="8309" class="Symbol">|</a> <a id="8311" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="8315" href="/20.07/PUC/2019/Assignment5/#8315" class="Bound">A≡B</a> <a id="8331" class="Symbol">=</a> <a id="8334" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="8338" class="Symbol">(</a><a id="8339" href="/20.07/PUC/2019/Assignment5/#3792" class="InductiveConstructor">⊢↑</a> <a id="8342" class="Bound">⊢M</a> <a id="8345" href="/20.07/PUC/2019/Assignment5/#8315" class="Bound">A≡B</a><a id="8348" class="Symbol">)</a>
</pre>
<h3 id="erasure">Erasure</h3>
<pre class="Agda"> <a id="Inference.∥_∥Tp"></a><a id="8374" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥_∥Tp</a> <a id="8380" class="Symbol">:</a> <a id="8382" href="/20.07/PUC/2019/Assignment5/#1552" class="Datatype">Type</a> <a id="8387" class="Symbol">→</a> <a id="8389" href="/20.07/More/#14469" class="Datatype">DB.Type</a>
<a id="8399" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥</a> <a id="8401" href="/20.07/PUC/2019/Assignment5/#1573" class="InductiveConstructor">`ℕ</a> <a id="8404" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥Tp</a> <a id="8420" class="Symbol">=</a> <a id="8423" href="/20.07/More/#14488" class="InductiveConstructor">DB.`ℕ</a>
<a id="8431" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥</a> <a id="8433" href="/20.07/PUC/2019/Assignment5/#8433" class="Bound">A</a> <a id="8435" href="/20.07/PUC/2019/Assignment5/#1590" class="InductiveConstructor Operator">⇒</a> <a id="8437" href="/20.07/PUC/2019/Assignment5/#8437" class="Bound">B</a> <a id="8439" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥Tp</a> <a id="8452" class="Symbol">=</a> <a id="8455" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥</a> <a id="8457" href="/20.07/PUC/2019/Assignment5/#8433" class="Bound">A</a> <a id="8459" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥Tp</a> <a id="8463" href="/20.07/More/#14503" class="InductiveConstructor Operator">DB.⇒</a> <a id="8468" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥</a> <a id="8470" href="/20.07/PUC/2019/Assignment5/#8437" class="Bound">B</a> <a id="8472" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥Tp</a>
<a id="Inference.∥_∥Cx"></a><a id="8479" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥_∥Cx</a> <a id="8485" class="Symbol">:</a> <a id="8487" href="/20.07/PUC/2019/Assignment5/#1625" class="Datatype">Context</a> <a id="8495" class="Symbol">→</a> <a id="8497" href="/20.07/More/#14602" class="Datatype">DB.Context</a>
<a id="8510" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥</a> <a id="8512" href="/20.07/PUC/2019/Assignment5/#1649" class="InductiveConstructor">∅</a> <a id="8514" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥Cx</a> <a id="8531" class="Symbol">=</a> <a id="8534" href="/20.07/More/#14624" class="InductiveConstructor">DB.∅</a>
<a id="8541" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥</a> <a id="8543" href="/20.07/PUC/2019/Assignment5/#8543" class="Bound">Γ</a> <a id="8545" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">,</a> <a id="8547" href="/20.07/PUC/2019/Assignment5/#8547" class="Bound">x</a> <a id="8549" href="/20.07/PUC/2019/Assignment5/#1669" class="InductiveConstructor Operator">⦂</a> <a id="8551" href="/20.07/PUC/2019/Assignment5/#8551" class="Bound">A</a> <a id="8553" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥Cx</a> <a id="8562" class="Symbol">=</a> <a id="8565" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥</a> <a id="8567" href="/20.07/PUC/2019/Assignment5/#8543" class="Bound">Γ</a> <a id="8569" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥Cx</a> <a id="8573" href="/20.07/More/#14640" class="InductiveConstructor Operator">DB.,</a> <a id="8578" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥</a> <a id="8580" href="/20.07/PUC/2019/Assignment5/#8551" class="Bound">A</a> <a id="8582" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥Tp</a>
<a id="Inference.∥_∥∋"></a><a id="8589" href="/20.07/PUC/2019/Assignment5/#8589" class="Function Operator">∥_∥∋</a> <a id="8594" class="Symbol">:</a> <a id="8596" class="Symbol">∀</a> <a id="8598" class="Symbol">{</a><a id="8599" href="/20.07/PUC/2019/Assignment5/#8599" class="Bound">Γ</a> <a id="8601" href="/20.07/PUC/2019/Assignment5/#8601" class="Bound">x</a> <a id="8603" href="/20.07/PUC/2019/Assignment5/#8603" class="Bound">A</a><a id="8604" class="Symbol">}</a> <a id="8606" class="Symbol">→</a> <a id="8608" href="/20.07/PUC/2019/Assignment5/#8599" class="Bound">Γ</a> <a id="8610" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">∋</a> <a id="8612" href="/20.07/PUC/2019/Assignment5/#8601" class="Bound">x</a> <a id="8614" href="/20.07/PUC/2019/Assignment5/#2582" class="Datatype Operator">⦂</a> <a id="8616" href="/20.07/PUC/2019/Assignment5/#8603" class="Bound">A</a> <a id="8618" class="Symbol">→</a> <a id="8620" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥</a> <a id="8622" href="/20.07/PUC/2019/Assignment5/#8599" class="Bound">Γ</a> <a id="8624" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥Cx</a> <a id="8628" href="/20.07/More/#14724" class="Datatype Operator">DB.∋</a> <a id="8633" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥</a> <a id="8635" href="/20.07/PUC/2019/Assignment5/#8603" class="Bound">A</a> <a id="8637" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥Tp</a>
<a id="8643" href="/20.07/PUC/2019/Assignment5/#8589" class="Function Operator">∥</a> <a id="8645" href="/20.07/PUC/2019/Assignment5/#2627" class="InductiveConstructor">Z</a> <a id="8647" href="/20.07/PUC/2019/Assignment5/#8589" class="Function Operator">∥∋</a> <a id="8664" class="Symbol">=</a> <a id="8667" href="/20.07/More/#14760" class="InductiveConstructor">DB.Z</a>
<a id="8674" href="/20.07/PUC/2019/Assignment5/#8589" class="Function Operator">∥</a> <a id="8676" href="/20.07/PUC/2019/Assignment5/#2701" class="InductiveConstructor">S</a> <a id="8678" href="/20.07/PUC/2019/Assignment5/#8678" class="Bound">x≢</a> <a id="8681" href="/20.07/PUC/2019/Assignment5/#8681" class="Bound">⊢x</a> <a id="8684" href="/20.07/PUC/2019/Assignment5/#8589" class="Function Operator">∥∋</a> <a id="8695" class="Symbol">=</a> <a id="8698" href="/20.07/More/#14807" class="InductiveConstructor Operator">DB.S</a> <a id="8703" href="/20.07/PUC/2019/Assignment5/#8589" class="Function Operator">∥</a> <a id="8705" href="/20.07/PUC/2019/Assignment5/#8681" class="Bound">⊢x</a> <a id="8708" href="/20.07/PUC/2019/Assignment5/#8589" class="Function Operator">∥∋</a>
<a id="Inference.∥_∥⁺"></a><a id="8714" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥_∥⁺</a> <a id="8719" class="Symbol">:</a> <a id="8721" class="Symbol">∀</a> <a id="8723" class="Symbol">{</a><a id="8724" href="/20.07/PUC/2019/Assignment5/#8724" class="Bound">Γ</a> <a id="8726" href="/20.07/PUC/2019/Assignment5/#8726" class="Bound">M</a> <a id="8728" href="/20.07/PUC/2019/Assignment5/#8728" class="Bound">A</a><a id="8729" class="Symbol">}</a> <a id="8731" class="Symbol">→</a> <a id="8733" href="/20.07/PUC/2019/Assignment5/#8724" class="Bound">Γ</a> <a id="8735" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">⊢</a> <a id="8737" href="/20.07/PUC/2019/Assignment5/#8726" class="Bound">M</a> <a id="8739" href="/20.07/PUC/2019/Assignment5/#2852" class="Datatype Operator">↑</a> <a id="8741" href="/20.07/PUC/2019/Assignment5/#8728" class="Bound">A</a> <a id="8743" class="Symbol">→</a> <a id="8745" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥</a> <a id="8747" href="/20.07/PUC/2019/Assignment5/#8724" class="Bound">Γ</a> <a id="8749" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥Cx</a> <a id="8753" href="/20.07/More/#14915" class="Datatype Operator">DB.⊢</a> <a id="8758" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥</a> <a id="8760" href="/20.07/PUC/2019/Assignment5/#8728" class="Bound">A</a> <a id="8762" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥Tp</a>
<a id="Inference.∥_∥⁻"></a><a id="8768" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥_∥⁻</a> <a id="8773" class="Symbol">:</a> <a id="8775" class="Symbol">∀</a> <a id="8777" class="Symbol">{</a><a id="8778" href="/20.07/PUC/2019/Assignment5/#8778" class="Bound">Γ</a> <a id="8780" href="/20.07/PUC/2019/Assignment5/#8780" class="Bound">M</a> <a id="8782" href="/20.07/PUC/2019/Assignment5/#8782" class="Bound">A</a><a id="8783" class="Symbol">}</a> <a id="8785" class="Symbol">→</a> <a id="8787" href="/20.07/PUC/2019/Assignment5/#8778" class="Bound">Γ</a> <a id="8789" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">⊢</a> <a id="8791" href="/20.07/PUC/2019/Assignment5/#8780" class="Bound">M</a> <a id="8793" href="/20.07/PUC/2019/Assignment5/#2896" class="Datatype Operator">↓</a> <a id="8795" href="/20.07/PUC/2019/Assignment5/#8782" class="Bound">A</a> <a id="8797" class="Symbol">→</a> <a id="8799" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥</a> <a id="8801" href="/20.07/PUC/2019/Assignment5/#8778" class="Bound">Γ</a> <a id="8803" href="/20.07/PUC/2019/Assignment5/#8479" class="Function Operator">∥Cx</a> <a id="8807" href="/20.07/More/#14915" class="Datatype Operator">DB.⊢</a> <a id="8812" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥</a> <a id="8814" href="/20.07/PUC/2019/Assignment5/#8782" class="Bound">A</a> <a id="8816" href="/20.07/PUC/2019/Assignment5/#8374" class="Function Operator">∥Tp</a>
<a id="8823" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥</a> <a id="8825" href="/20.07/PUC/2019/Assignment5/#2958" class="InductiveConstructor">⊢`</a> <a id="8828" href="/20.07/PUC/2019/Assignment5/#8828" class="Bound">⊢x</a> <a id="8831" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥⁺</a> <a id="8844" class="Symbol">=</a> <a id="8847" href="/20.07/More/#14967" class="InductiveConstructor Operator">DB.`</a> <a id="8852" href="/20.07/PUC/2019/Assignment5/#8589" class="Function Operator">∥</a> <a id="8854" href="/20.07/PUC/2019/Assignment5/#8828" class="Bound">⊢x</a> <a id="8857" href="/20.07/PUC/2019/Assignment5/#8589" class="Function Operator">∥∋</a>
<a id="8862" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥</a> <a id="8864" href="/20.07/PUC/2019/Assignment5/#8864" class="Bound">⊢L</a> <a id="8867" href="/20.07/PUC/2019/Assignment5/#3036" class="InductiveConstructor Operator">·</a> <a id="8869" href="/20.07/PUC/2019/Assignment5/#8869" class="Bound">⊢M</a> <a id="8872" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥⁺</a> <a id="8883" class="Symbol">=</a> <a id="8886" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥</a> <a id="8888" href="/20.07/PUC/2019/Assignment5/#8864" class="Bound">⊢L</a> <a id="8891" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥⁺</a> <a id="8894" href="/20.07/More/#15103" class="InductiveConstructor Operator">DB.·</a> <a id="8899" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="8901" href="/20.07/PUC/2019/Assignment5/#8869" class="Bound">⊢M</a> <a id="8904" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a>
<a id="8909" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥</a> <a id="8911" href="/20.07/PUC/2019/Assignment5/#3145" class="InductiveConstructor">⊢↓</a> <a id="8914" href="/20.07/PUC/2019/Assignment5/#8914" class="Bound">⊢M</a> <a id="8917" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥⁺</a> <a id="8930" class="Symbol">=</a> <a id="8933" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="8935" href="/20.07/PUC/2019/Assignment5/#8914" class="Bound">⊢M</a> <a id="8938" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a>
<a id="8944" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="8946" href="/20.07/PUC/2019/Assignment5/#3251" class="InductiveConstructor">⊢ƛ</a> <a id="8949" href="/20.07/PUC/2019/Assignment5/#8949" class="Bound">⊢N</a> <a id="8952" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a> <a id="8965" class="Symbol">=</a> <a id="8968" href="/20.07/More/#15035" class="InductiveConstructor Operator">DB.ƛ</a> <a id="8973" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="8975" href="/20.07/PUC/2019/Assignment5/#8949" class="Bound">⊢N</a> <a id="8978" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a>
<a id="8983" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="8985" href="/20.07/PUC/2019/Assignment5/#3357" class="InductiveConstructor">⊢zero</a> <a id="8991" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a> <a id="9004" class="Symbol">=</a> <a id="9007" href="/20.07/More/#15193" class="InductiveConstructor">DB.`zero</a>
<a id="9018" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="9020" href="/20.07/PUC/2019/Assignment5/#3422" class="InductiveConstructor">⊢suc</a> <a id="9025" href="/20.07/PUC/2019/Assignment5/#9025" class="Bound">⊢M</a> <a id="9028" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a> <a id="9039" class="Symbol">=</a> <a id="9042" href="/20.07/More/#15236" class="InductiveConstructor Operator">DB.`suc</a> <a id="9050" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="9052" href="/20.07/PUC/2019/Assignment5/#9025" class="Bound">⊢M</a> <a id="9055" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a>
<a id="9060" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="9062" href="/20.07/PUC/2019/Assignment5/#3509" class="InductiveConstructor">⊢case</a> <a id="9068" href="/20.07/PUC/2019/Assignment5/#9068" class="Bound">⊢L</a> <a id="9071" href="/20.07/PUC/2019/Assignment5/#9071" class="Bound">⊢M</a> <a id="9074" href="/20.07/PUC/2019/Assignment5/#9074" class="Bound">⊢N</a> <a id="9077" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a> <a id="9081" class="Symbol">=</a> <a id="9084" href="/20.07/More/#15292" class="InductiveConstructor">DB.case</a> <a id="9092" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥</a> <a id="9094" href="/20.07/PUC/2019/Assignment5/#9068" class="Bound">⊢L</a> <a id="9097" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥⁺</a> <a id="9100" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="9102" href="/20.07/PUC/2019/Assignment5/#9071" class="Bound">⊢M</a> <a id="9105" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a> <a id="9108" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="9110" href="/20.07/PUC/2019/Assignment5/#9074" class="Bound">⊢N</a> <a id="9113" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a>
<a id="9118" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="9120" href="/20.07/PUC/2019/Assignment5/#3694" class="InductiveConstructor">⊢μ</a> <a id="9123" href="/20.07/PUC/2019/Assignment5/#9123" class="Bound">⊢M</a> <a id="9126" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a> <a id="9139" class="Symbol">=</a> <a id="9142" href="/20.07/More/#15391" class="InductiveConstructor Operator">DB.μ</a> <a id="9147" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="9149" href="/20.07/PUC/2019/Assignment5/#9123" class="Bound">⊢M</a> <a id="9152" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a>
<a id="9157" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥</a> <a id="9159" href="/20.07/PUC/2019/Assignment5/#3792" class="InductiveConstructor">⊢↑</a> <a id="9162" href="/20.07/PUC/2019/Assignment5/#9162" class="Bound">⊢M</a> <a id="9165" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="9170" href="/20.07/PUC/2019/Assignment5/#8768" class="Function Operator">∥⁻</a> <a id="9178" class="Symbol">=</a> <a id="9181" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥</a> <a id="9183" href="/20.07/PUC/2019/Assignment5/#9162" class="Bound">⊢M</a> <a id="9186" href="/20.07/PUC/2019/Assignment5/#8714" class="Function Operator">∥⁺</a>
</pre>
<h4 id="bidirectional-mul">Exercise <code class="language-plaintext highlighter-rouge">bidirectional-mul</code> (recommended)</h4>
<p>Rewrite your definition of multiplication from
Chapter [Lambda][plfa.Lambda], decorated to support inference.</p>
<h4 id="bidirectional-products">Exercise <code class="language-plaintext highlighter-rouge">bidirectional-products</code> (recommended)</h4>
<p>Extend the bidirectional type rules to include products from
Chapter [More][plfa.More].</p>
<h4 id="exercise-bidirectional-rest-stretch">Exercise <code class="language-plaintext highlighter-rouge">bidirectional-rest</code> (stretch)</h4>
<p>Extend the bidirectional type rules to include the rest of the constructs from
Chapter [More][plfa.More].</p>
<h4 id="exercise-inference-mul-recommended">Exercise <code class="language-plaintext highlighter-rouge">inference-mul</code> (recommended)</h4>
<p>Using the definition from exercise <a href="#bidirectional-mul">bidirectional-mul</a>,
infer the corresponding inherently typed term.
Show that erasure of the inferred typing yields your definition of
multiplication from Chapter [DeBruijn][plfa.DeBruijn].</p>
<h4 id="exercise-inference-products-recommended">Exercise <code class="language-plaintext highlighter-rouge">inference-products</code> (recommended)</h4>
<p>Extend bidirectional inference to include products from
Chapter [More][plfa.More].</p>
<h4 id="exercise-inference-rest-stretch">Exercise <code class="language-plaintext highlighter-rouge">inference-rest</code> (stretch)</h4>
<p>Extend bidirectional inference to include the rest of the constructs from
Chapter [More][plfa.More].</p>
<h2 id="untyped">Untyped</h2>
<h4 id="exercise-type">Exercise (<code class="language-plaintext highlighter-rouge">Type≃⊤</code>)</h4>
<p>Show that <code class="language-plaintext highlighter-rouge">Type</code> is isomorphic to <code class="language-plaintext highlighter-rouge">⊤</code>, the unit type.</p>
<h4 id="exercise-contextℕ">Exercise (<code class="language-plaintext highlighter-rouge">Context≃ℕ</code>)</h4>
<p>Show that <code class="language-plaintext highlighter-rouge">Context</code> is isomorphic to <code class="language-plaintext highlighter-rouge">ℕ</code>.</p>
<h4 id="exercise-variant-1">Exercise (<code class="language-plaintext highlighter-rouge">variant-1</code>)</h4>
<p>How would the rules change if we want call-by-value where terms
normalise completely? Assume that <code class="language-plaintext highlighter-rouge">β</code> should not permit reduction
unless both terms are in normal form.</p>
<h4 id="exercise-variant-2">Exercise (<code class="language-plaintext highlighter-rouge">variant-2</code>)</h4>
<p>How would the rules change if we want call-by-value where terms
do not reduce underneath lambda? Assume that <code class="language-plaintext highlighter-rouge">β</code>
permits reduction when both terms are values (that is, lambda
abstractions). What would <code class="language-plaintext highlighter-rouge">2+2ᶜ</code> reduce to in this case?</p>
<h4 id="exercise-plus-eval">Exercise <code class="language-plaintext highlighter-rouge">plus-eval</code></h4>
<p>Use the evaluator to confirm that <code class="language-plaintext highlighter-rouge">plus · two · two</code> and <code class="language-plaintext highlighter-rouge">four</code>
normalise to the same term.</p>
<h4 id="exercise-multiplication-untyped-recommended">Exercise <code class="language-plaintext highlighter-rouge">multiplication-untyped</code> (recommended)</h4>
<p>Use the encodings above to translate your definition of
multiplication from previous chapters with the Scott
representation and the encoding of the fixpoint operator.
Confirm that two times two is four.</p>
<h4 id="exercise-encode-more-stretch">Exercise <code class="language-plaintext highlighter-rouge">encode-more</code> (stretch)</h4>
<p>Along the lines above, encode all of the constructs of
Chapter [More][plfa.More],
save for primitive numbers, in the untyped lambda calculus.</p>
</div>
<p style="text-align:center;">
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/courses/puc/2019/Assignment5.lagda.md">Source</a>
</p>
</article>
</div>
</main><footer class="site-footer h-card">
<data class="u-url" href="/20.07/"></data>
<div class="wrapper">
<h2 class="footer-heading">Programming Language Foundations in Agda
</h2><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Philip Wadler</li>
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Wen Kokke</li>
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Jeremy G. Siek</li>
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
</div>
</footer>
<!-- Import jQuery -->
<script type="text/javascript" src="/20.07/assets/jquery.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
<script type="text/javascript">
anchors.add();
</script>
<script type="text/javascript">
// Makes sandwhich menu works
$('.menu-icon').click(function(){
$('.trigger').toggle();
});
// Script which allows for foldable code blocks
$('div.foldable pre').each(function(){
var autoHeight = $(this).height();
var lineHeight = parseFloat($(this).css('line-height'));
var plus = $("<div></div>");
var horLine = $("<div></div>");
var verLine = $("<div></div>");
$(this).prepend(plus);
plus.css({
'position' : 'relative',
'float' : 'right',
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'width' : lineHeight,
'height' : lineHeight});
verLine.css({
'position' : 'relative',
'height' : lineHeight,
'width' : '3px',
'background-color' : '#C1E0FF'});
horLine.css({
'position' : 'relative',
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'height' : '3px',
'width' : lineHeight,
'background-color' : '#C1E0FF'});
plus.append(verLine);
plus.append(horLine);
$(this).height(2.0 * lineHeight);
$(this).css('overflow','hidden');
$(this).click(function(){
if ($(this).height() == autoHeight) {
$(this).height(2.0 * lineHeight);
plus.show();
}
else {
$(this).height('auto');
plus.hide();
}
});
});
</script>
<!-- Import KaTeX -->
<script type="text/javascript" src="/20.07/assets/katex.js"></script>
<!-- Script which renders TeX using KaTeX -->
<script type="text/javascript">
$("script[type='math/tex']").replaceWith(
function(){
var tex = $(this).text();
return "<span class=\"inline-equation\">" +
katex.renderToString(tex) +
"</span>";
});
$("script[type='math/tex; mode=display']").replaceWith(
function(){
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
return "<div class=\"equation\">" +
katex.renderToString("\\displaystyle "+tex) +
"</div>";
});
</script>
</body>
</html>
Reference in a new issue View git blame Copy permalink