rachel/rachel.cafe
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
e15f3ac5cb
rachel.cafe/agda/Relation.Nullary.Decidable.Core.html

132 lines
44 KiB
HTML
Raw Normal View History

add some agda stuff
2022-06-23 22:12:24 +02:00
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Relation.Nullary.Decidable.Core</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Operations on and properties of decidable relations</a>
<a id="161" class="Comment">--</a>
<a id="164" class="Comment">-- This file contains some core definitions which are re-exported by</a>
<a id="233" class="Comment">-- Relation.Nullary.Decidable</a>
<a id="263" class="Comment">------------------------------------------------------------------------</a>
<a id="337" class="Symbol">{-#</a> <a id="341" class="Keyword">OPTIONS</a> <a id="349" class="Pragma">--without-K</a> <a id="361" class="Pragma">--safe</a> <a id="368" class="Symbol">#-}</a>
<a id="373" class="Keyword">module</a> <a id="380" href="Relation.Nullary.Decidable.Core.html" class="Module">Relation.Nullary.Decidable.Core</a> <a id="412" class="Keyword">where</a>
<a id="419" class="Keyword">open</a> <a id="424" class="Keyword">import</a> <a id="431" href="Level.html" class="Module">Level</a> <a id="437" class="Keyword">using</a> <a id="443" class="Symbol">(</a><a id="444" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="449" class="Symbol">;</a> <a id="451" href="Level.html#400" class="Record">Lift</a><a id="455" class="Symbol">)</a>
<a id="457" class="Keyword">open</a> <a id="462" class="Keyword">import</a> <a id="469" href="Data.Bool.Base.html" class="Module">Data.Bool.Base</a> <a id="484" class="Keyword">using</a> <a id="490" class="Symbol">(</a><a id="491" href="Agda.Builtin.Bool.html#163" class="Datatype">Bool</a><a id="495" class="Symbol">;</a> <a id="497" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a><a id="502" class="Symbol">;</a> <a id="504" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a><a id="508" class="Symbol">;</a> <a id="510" href="Data.Bool.Base.html#932" class="Function">not</a><a id="513" class="Symbol">;</a> <a id="515" href="Data.Bool.Base.html#1451" class="Function">T</a><a id="516" class="Symbol">)</a>
<a id="518" class="Keyword">open</a> <a id="523" class="Keyword">import</a> <a id="530" href="Data.Unit.Base.html" class="Module">Data.Unit.Base</a> <a id="545" class="Keyword">using</a> <a id="551" class="Symbol">(</a><a id="552" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a><a id="553" class="Symbol">)</a>
<a id="555" class="Keyword">open</a> <a id="560" class="Keyword">import</a> <a id="567" href="Data.Empty.html" class="Module">Data.Empty</a>
<a id="578" class="Keyword">open</a> <a id="583" class="Keyword">import</a> <a id="590" href="Data.Product.html" class="Module">Data.Product</a>
<a id="603" class="Keyword">open</a> <a id="608" class="Keyword">import</a> <a id="615" href="Function.Base.html" class="Module">Function.Base</a>
<a id="630" class="Keyword">open</a> <a id="635" class="Keyword">import</a> <a id="642" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a>
<a id="664" class="Keyword">open</a> <a id="669" class="Keyword">import</a> <a id="676" href="Relation.Nullary.Reflects.html" class="Module">Relation.Nullary.Reflects</a>
<a id="702" class="Keyword">open</a> <a id="707" class="Keyword">import</a> <a id="714" href="Relation.Nullary.html" class="Module">Relation.Nullary</a>
<a id="732" class="Keyword">private</a>
<a id="742" class="Keyword">variable</a>
<a id="755" href="Relation.Nullary.Decidable.Core.html#755" class="Generalizable">p</a> <a id="757" href="Relation.Nullary.Decidable.Core.html#757" class="Generalizable">q</a> <a id="759" class="Symbol">:</a> <a id="761" href="Agda.Primitive.html#597" class="Postulate">Level</a>
<a id="771" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="773" class="Symbol">:</a> <a id="775" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="779" href="Relation.Nullary.Decidable.Core.html#755" class="Generalizable">p</a>
<a id="785" href="Relation.Nullary.Decidable.Core.html#785" class="Generalizable">Q</a> <a id="787" class="Symbol">:</a> <a id="789" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="793" href="Relation.Nullary.Decidable.Core.html#757" class="Generalizable">q</a>
<a id="796" class="Comment">-- `isYes` is a stricter version of `does`. The lack of computation means that</a>
<a id="875" class="Comment">-- we can recover the proposition `P` from `isYes P?` by unification. This is</a>
<a id="953" class="Comment">-- useful when we are using the decision procedure for proof automation.</a>
<a id="isYes"></a><a id="1027" href="Relation.Nullary.Decidable.Core.html#1027" class="Function">isYes</a> <a id="1033" class="Symbol">:</a> <a id="1035" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1039" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="1041" class="Symbol">→</a> <a id="1043" href="Agda.Builtin.Bool.html#163" class="Datatype">Bool</a>
<a id="1048" href="Relation.Nullary.Decidable.Core.html#1027" class="Function">isYes</a> <a id="1054" class="Symbol">(</a> <a id="1056" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="1061" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1069" class="Symbol">_)</a> <a id="1072" class="Symbol">=</a> <a id="1074" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a>
<a id="1079" href="Relation.Nullary.Decidable.Core.html#1027" class="Function">isYes</a> <a id="1085" class="Symbol">(</a><a id="1086" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="1092" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1100" class="Symbol">_)</a> <a id="1103" class="Symbol">=</a> <a id="1105" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a>
<a id="isYes≗does"></a><a id="1112" href="Relation.Nullary.Decidable.Core.html#1112" class="Function">isYes≗does</a> <a id="1123" class="Symbol">:</a> <a id="1125" class="Symbol">(</a><a id="1126" href="Relation.Nullary.Decidable.Core.html#1126" class="Bound">P?</a> <a id="1129" class="Symbol">:</a> <a id="1131" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1135" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="1136" class="Symbol">)</a> <a id="1138" class="Symbol">→</a> <a id="1140" href="Relation.Nullary.Decidable.Core.html#1027" class="Function">isYes</a> <a id="1146" href="Relation.Nullary.Decidable.Core.html#1126" class="Bound">P?</a> <a id="1149" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1151" href="Relation.Nullary.html#1581" class="Field">does</a> <a id="1156" href="Relation.Nullary.Decidable.Core.html#1126" class="Bound">P?</a>
<a id="1159" href="Relation.Nullary.Decidable.Core.html#1112" class="Function">isYes≗does</a> <a id="1170" class="Symbol">(</a> <a id="1172" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="1177" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1185" class="Symbol">_)</a> <a id="1188" class="Symbol">=</a> <a id="1190" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
<a id="1195" href="Relation.Nullary.Decidable.Core.html#1112" class="Function">isYes≗does</a> <a id="1206" class="Symbol">(</a><a id="1207" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="1213" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1221" class="Symbol">_)</a> <a id="1224" class="Symbol">=</a> <a id="1226" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
<a id="1232" class="Comment">-- The traditional name for isYes is ⌊_⌋, indicating the stripping of evidence.</a>
<a id="⌊_⌋"></a><a id="1312" href="Relation.Nullary.Decidable.Core.html#1312" class="Function Operator">⌊_⌋</a> <a id="1316" class="Symbol">=</a> <a id="1318" href="Relation.Nullary.Decidable.Core.html#1027" class="Function">isYes</a>
<a id="isNo"></a><a id="1325" href="Relation.Nullary.Decidable.Core.html#1325" class="Function">isNo</a> <a id="1330" class="Symbol">:</a> <a id="1332" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1336" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="1338" class="Symbol">→</a> <a id="1340" href="Agda.Builtin.Bool.html#163" class="Datatype">Bool</a>
<a id="1345" href="Relation.Nullary.Decidable.Core.html#1325" class="Function">isNo</a> <a id="1350" class="Symbol">=</a> <a id="1352" href="Data.Bool.Base.html#932" class="Function">not</a> <a id="1356" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1358" href="Relation.Nullary.Decidable.Core.html#1027" class="Function">isYes</a>
<a id="True"></a><a id="1365" href="Relation.Nullary.Decidable.Core.html#1365" class="Function">True</a> <a id="1370" class="Symbol">:</a> <a id="1372" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1376" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="1378" class="Symbol">→</a> <a id="1380" href="Agda.Primitive.html#326" class="Primitive">Set</a>
<a id="1384" href="Relation.Nullary.Decidable.Core.html#1365" class="Function">True</a> <a id="1389" href="Relation.Nullary.Decidable.Core.html#1389" class="Bound">Q</a> <a id="1391" class="Symbol">=</a> <a id="1393" href="Data.Bool.Base.html#1451" class="Function">T</a> <a id="1395" class="Symbol">(</a><a id="1396" href="Relation.Nullary.Decidable.Core.html#1027" class="Function">isYes</a> <a id="1402" href="Relation.Nullary.Decidable.Core.html#1389" class="Bound">Q</a><a id="1403" class="Symbol">)</a>
<a id="False"></a><a id="1406" href="Relation.Nullary.Decidable.Core.html#1406" class="Function">False</a> <a id="1412" class="Symbol">:</a> <a id="1414" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1418" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="1420" class="Symbol">→</a> <a id="1422" href="Agda.Primitive.html#326" class="Primitive">Set</a>
<a id="1426" href="Relation.Nullary.Decidable.Core.html#1406" class="Function">False</a> <a id="1432" href="Relation.Nullary.Decidable.Core.html#1432" class="Bound">Q</a> <a id="1434" class="Symbol">=</a> <a id="1436" href="Data.Bool.Base.html#1451" class="Function">T</a> <a id="1438" class="Symbol">(</a><a id="1439" href="Relation.Nullary.Decidable.Core.html#1325" class="Function">isNo</a> <a id="1444" href="Relation.Nullary.Decidable.Core.html#1432" class="Bound">Q</a><a id="1445" class="Symbol">)</a>
<a id="1448" class="Comment">-- Gives a witness to the &quot;truth&quot;.</a>
<a id="toWitness"></a><a id="1484" href="Relation.Nullary.Decidable.Core.html#1484" class="Function">toWitness</a> <a id="1494" class="Symbol">:</a> <a id="1496" class="Symbol">{</a><a id="1497" href="Relation.Nullary.Decidable.Core.html#1497" class="Bound">Q</a> <a id="1499" class="Symbol">:</a> <a id="1501" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1505" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="1506" class="Symbol">}</a> <a id="1508" class="Symbol">→</a> <a id="1510" href="Relation.Nullary.Decidable.Core.html#1365" class="Function">True</a> <a id="1515" href="Relation.Nullary.Decidable.Core.html#1497" class="Bound">Q</a> <a id="1517" class="Symbol">→</a> <a id="1519" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a>
<a id="1521" href="Relation.Nullary.Decidable.Core.html#1484" class="Function">toWitness</a> <a id="1531" class="Symbol">{</a><a id="1532" class="Argument">Q</a> <a id="1534" class="Symbol">=</a> <a id="1536" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="1542" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1550" href="Relation.Nullary.Decidable.Core.html#1550" class="Bound">[p]</a><a id="1553" class="Symbol">}</a> <a id="1555" class="Symbol">_</a> <a id="1558" class="Symbol">=</a> <a id="1560" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="1567" href="Relation.Nullary.Decidable.Core.html#1550" class="Bound">[p]</a>
<a id="1571" href="Relation.Nullary.Decidable.Core.html#1484" class="Function">toWitness</a> <a id="1581" class="Symbol">{</a><a id="1582" class="Argument">Q</a> <a id="1584" class="Symbol">=</a> <a id="1586" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="1592" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1601" class="Symbol">_</a> <a id="1603" class="Symbol">}</a> <a id="1605" class="Symbol">()</a>
<a id="1609" class="Comment">-- Establishes a &quot;truth&quot;, given a witness.</a>
<a id="fromWitness"></a><a id="1653" href="Relation.Nullary.Decidable.Core.html#1653" class="Function">fromWitness</a> <a id="1665" class="Symbol">:</a> <a id="1667" class="Symbol">{</a><a id="1668" href="Relation.Nullary.Decidable.Core.html#1668" class="Bound">Q</a> <a id="1670" class="Symbol">:</a> <a id="1672" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1676" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="1677" class="Symbol">}</a> <a id="1679" class="Symbol">→</a> <a id="1681" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="1683" class="Symbol">→</a> <a id="1685" href="Relation.Nullary.Decidable.Core.html#1365" class="Function">True</a> <a id="1690" href="Relation.Nullary.Decidable.Core.html#1668" class="Bound">Q</a>
<a id="1692" href="Relation.Nullary.Decidable.Core.html#1653" class="Function">fromWitness</a> <a id="1704" class="Symbol">{</a><a id="1705" class="Argument">Q</a> <a id="1707" class="Symbol">=</a> <a id="1709" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="1715" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1725" class="Symbol">_</a> <a id="1727" class="Symbol">}</a> <a id="1729" class="Symbol">=</a> <a id="1731" href="Function.Base.html#636" class="Function">const</a> <a id="1737" class="Symbol">_</a>
<a id="1739" href="Relation.Nullary.Decidable.Core.html#1653" class="Function">fromWitness</a> <a id="1751" class="Symbol">{</a><a id="1752" class="Argument">Q</a> <a id="1754" class="Symbol">=</a> <a id="1756" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="1762" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1770" href="Relation.Nullary.Decidable.Core.html#1770" class="Bound">[¬p]</a><a id="1774" class="Symbol">}</a> <a id="1776" class="Symbol">=</a> <a id="1778" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="1785" href="Relation.Nullary.Decidable.Core.html#1770" class="Bound">[¬p]</a>
<a id="1791" class="Comment">-- Variants for False.</a>
<a id="toWitnessFalse"></a><a id="1815" href="Relation.Nullary.Decidable.Core.html#1815" class="Function">toWitnessFalse</a> <a id="1830" class="Symbol">:</a> <a id="1832" class="Symbol">{</a><a id="1833" href="Relation.Nullary.Decidable.Core.html#1833" class="Bound">Q</a> <a id="1835" class="Symbol">:</a> <a id="1837" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1841" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="1842" class="Symbol">}</a> <a id="1844" class="Symbol">→</a> <a id="1846" href="Relation.Nullary.Decidable.Core.html#1406" class="Function">False</a> <a id="1852" href="Relation.Nullary.Decidable.Core.html#1833" class="Bound">Q</a> <a id="1854" class="Symbol">→</a> <a id="1856" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="1858" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a>
<a id="1860" href="Relation.Nullary.Decidable.Core.html#1815" class="Function">toWitnessFalse</a> <a id="1875" class="Symbol">{</a><a id="1876" class="Argument">Q</a> <a id="1878" class="Symbol">=</a> <a id="1880" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="1886" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1896" class="Symbol">_</a> <a id="1898" class="Symbol">}</a> <a id="1900" class="Symbol">()</a>
<a id="1903" href="Relation.Nullary.Decidable.Core.html#1815" class="Function">toWitnessFalse</a> <a id="1918" class="Symbol">{</a><a id="1919" class="Argument">Q</a> <a id="1921" class="Symbol">=</a> <a id="1923" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="1929" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1937" href="Relation.Nullary.Decidable.Core.html#1937" class="Bound">[¬p]</a><a id="1941" class="Symbol">}</a> <a id="1943" class="Symbol">_</a> <a id="1946" class="Symbol">=</a> <a id="1948" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="1955" href="Relation.Nullary.Decidable.Core.html#1937" class="Bound">[¬p]</a>
<a id="fromWitnessFalse"></a><a id="1961" href="Relation.Nullary.Decidable.Core.html#1961" class="Function">fromWitnessFalse</a> <a id="1978" class="Symbol">:</a> <a id="1980" class="Symbol">{</a><a id="1981" href="Relation.Nullary.Decidable.Core.html#1981" class="Bound">Q</a> <a id="1983" class="Symbol">:</a> <a id="1985" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1989" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="1990" class="Symbol">}</a> <a id="1992" class="Symbol">→</a> <a id="1994" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="1996" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="1998" class="Symbol">→</a> <a id="2000" href="Relation.Nullary.Decidable.Core.html#1406" class="Function">False</a> <a id="2006" href="Relation.Nullary.Decidable.Core.html#1981" class="Bound">Q</a>
<a id="2008" href="Relation.Nullary.Decidable.Core.html#1961" class="Function">fromWitnessFalse</a> <a id="2025" class="Symbol">{</a><a id="2026" class="Argument">Q</a> <a id="2028" class="Symbol">=</a> <a id="2030" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="2036" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2044" href="Relation.Nullary.Decidable.Core.html#2044" class="Bound">[p]</a><a id="2047" class="Symbol">}</a> <a id="2049" class="Symbol">=</a> <a id="2051" href="Function.Base.html#1554" class="Function">flip</a> <a id="2056" href="Function.Base.html#1919" class="Function Operator">_$_</a> <a id="2060" class="Symbol">(</a><a id="2061" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="2068" href="Relation.Nullary.Decidable.Core.html#2044" class="Bound">[p]</a><a id="2071" class="Symbol">)</a>
<a id="2073" href="Relation.Nullary.Decidable.Core.html#1961" class="Function">fromWitnessFalse</a> <a id="2090" class="Symbol">{</a><a id="2091" class="Argument">Q</a> <a id="2093" class="Symbol">=</a> <a id="2095" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="2101" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2110" class="Symbol">_</a> <a id="2112" class="Symbol">}</a> <a id="2114" class="Symbol">=</a> <a id="2116" href="Function.Base.html#636" class="Function">const</a> <a id="2122" class="Symbol">_</a>
<a id="2125" class="Comment">-- If a decision procedure returns &quot;yes&quot;, then we can extract the</a>
<a id="2191" class="Comment">-- proof using from-yes.</a>
<a id="2217" class="Keyword">module</a> <a id="2224" href="Relation.Nullary.Decidable.Core.html#2224" class="Module">_</a> <a id="2226" class="Symbol">{</a><a id="2227" href="Relation.Nullary.Decidable.Core.html#2227" class="Bound">p</a><a id="2228" class="Symbol">}</a> <a id="2230" class="Symbol">{</a><a id="2231" href="Relation.Nullary.Decidable.Core.html#2231" class="Bound">P</a> <a id="2233" class="Symbol">:</a> <a id="2235" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2239" href="Relation.Nullary.Decidable.Core.html#2227" class="Bound">p</a><a id="2240" class="Symbol">}</a> <a id="2242" class="Keyword">where</a>
<a id="2251" href="Relation.Nullary.Decidable.Core.html#2251" class="Function">From-yes</a> <a id="2260" class="Symbol">:</a> <a id="2262" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="2266" href="Relation.Nullary.Decidable.Core.html#2231" class="Bound">P</a> <a id="2268" class="Symbol">→</a> <a id="2270" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2274" href="Relation.Nullary.Decidable.Core.html#2227" class="Bound">p</a>
<a id="2278" href="Relation.Nullary.Decidable.Core.html#2251" class="Function">From-yes</a> <a id="2287" class="Symbol">(</a><a id="2288" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="2294" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2302" class="Symbol">_)</a> <a id="2305" class="Symbol">=</a> <a id="2307" href="Relation.Nullary.Decidable.Core.html#2231" class="Bound">P</a>
<a id="2311" href="Relation.Nullary.Decidable.Core.html#2251" class="Function">From-yes</a> <a id="2320" class="Symbol">(</a><a id="2321" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="2327" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2335" class="Symbol">_)</a> <a id="2338" class="Symbol">=</a> <a id="2340" href="Level.html#400" class="Record">Lift</a> <a id="2345" href="Relation.Nullary.Decidable.Core.html#2227" class="Bound">p</a> <a id="2347" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a>
<a id="2352" href="Relation.Nullary.Decidable.Core.html#2352" class="Function">from-yes</a> <a id="2361" class="Symbol">:</a> <a id="2363" class="Symbol">(</a><a id="2364" href="Relation.Nullary.Decidable.Core.html#2364" class="Bound">p</a> <a id="2366" class="Symbol">:</a> <a id="2368" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="2372" href="Relation.Nullary.Decidable.Core.html#2231" class="Bound">P</a><a id="2373" class="Symbol">)</a> <a id="2375" class="Symbol">→</a> <a id="2377" href="Relation.Nullary.Decidable.Core.html#2251" class="Function">From-yes</a> <a id="2386" href="Relation.Nullary.Decidable.Core.html#2364" class="Bound">p</a>
<a id="2390" href="Relation.Nullary.Decidable.Core.html#2352" class="Function">from-yes</a> <a id="2399" class="Symbol">(</a><a id="2400" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="2406" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2414" href="Relation.Nullary.Decidable.Core.html#2414" class="Bound">[p]</a><a id="2417" class="Symbol">)</a> <a id="2419" class="Symbol">=</a> <a id="2421" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="2428" href="Relation.Nullary.Decidable.Core.html#2414" class="Bound">[p]</a>
<a id="2434" href="Relation.Nullary.Decidable.Core.html#2352" class="Function">from-yes</a> <a id="2443" class="Symbol">(</a><a id="2444" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="2450" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2458" class="Symbol">_</a> <a id="2460" class="Symbol">)</a> <a id="2462" class="Symbol">=</a> <a id="2464" class="Symbol">_</a>
<a id="2467" class="Comment">-- If a decision procedure returns &quot;no&quot;, then we can extract the proof</a>
<a id="2538" class="Comment">-- using from-no.</a>
<a id="2559" href="Relation.Nullary.Decidable.Core.html#2559" class="Function">From-no</a> <a id="2567" class="Symbol">:</a> <a id="2569" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="2573" href="Relation.Nullary.Decidable.Core.html#2231" class="Bound">P</a> <a id="2575" class="Symbol">→</a> <a id="2577" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2581" href="Relation.Nullary.Decidable.Core.html#2227" class="Bound">p</a>
<a id="2585" href="Relation.Nullary.Decidable.Core.html#2559" class="Function">From-no</a> <a id="2593" class="Symbol">(</a><a id="2594" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="2600" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2608" class="Symbol">_)</a> <a id="2611" class="Symbol">=</a> <a id="2613" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2615" href="Relation.Nullary.Decidable.Core.html#2231" class="Bound">P</a>
<a id="2619" href="Relation.Nullary.Decidable.Core.html#2559" class="Function">From-no</a> <a id="2627" class="Symbol">(</a><a id="2628" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="2634" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2642" class="Symbol">_)</a> <a id="2645" class="Symbol">=</a> <a id="2647" href="Level.html#400" class="Record">Lift</a> <a id="2652" href="Relation.Nullary.Decidable.Core.html#2227" class="Bound">p</a> <a id="2654" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a>
<a id="2659" href="Relation.Nullary.Decidable.Core.html#2659" class="Function">from-no</a> <a id="2667" class="Symbol">:</a> <a id="2669" class="Symbol">(</a><a id="2670" href="Relation.Nullary.Decidable.Core.html#2670" class="Bound">p</a> <a id="2672" class="Symbol">:</a> <a id="2674" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="2678" href="Relation.Nullary.Decidable.Core.html#2231" class="Bound">P</a><a id="2679" class="Symbol">)</a> <a id="2681" class="Symbol">→</a> <a id="2683" href="Relation.Nullary.Decidable.Core.html#2559" class="Function">From-no</a> <a id="2691" href="Relation.Nullary.Decidable.Core.html#2670" class="Bound">p</a>
<a id="2695" href="Relation.Nullary.Decidable.Core.html#2659" class="Function">from-no</a> <a id="2703" class="Symbol">(</a><a id="2704" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="2710" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2718" href="Relation.Nullary.Decidable.Core.html#2718" class="Bound">[¬p]</a><a id="2722" class="Symbol">)</a> <a id="2724" class="Symbol">=</a> <a id="2726" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="2733" href="Relation.Nullary.Decidable.Core.html#2718" class="Bound">[¬p]</a>
<a id="2740" href="Relation.Nullary.Decidable.Core.html#2659" class="Function">from-no</a> <a id="2748" class="Symbol">(</a><a id="2749" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="2755" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2765" class="Symbol">_</a> <a id="2767" class="Symbol">)</a> <a id="2769" class="Symbol">=</a> <a id="2771" class="Symbol">_</a>
<a id="2774" class="Comment">------------------------------------------------------------------------</a>
<a id="2847" class="Comment">-- Result of decidability</a>
<a id="dec-true"></a><a id="2874" href="Relation.Nullary.Decidable.Core.html#2874" class="Function">dec-true</a> <a id="2883" class="Symbol">:</a> <a id="2885" class="Symbol">(</a><a id="2886" href="Relation.Nullary.Decidable.Core.html#2886" class="Bound">p?</a> <a id="2889" class="Symbol">:</a> <a id="2891" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="2895" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="2896" class="Symbol">)</a> <a id="2898" class="Symbol">→</a> <a id="2900" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="2902" class="Symbol">→</a> <a id="2904" href="Relation.Nullary.html#1581" class="Field">does</a> <a id="2909" href="Relation.Nullary.Decidable.Core.html#2886" class="Bound">p?</a> <a id="2912" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2914" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a>
<a id="2919" href="Relation.Nullary.Decidable.Core.html#2874" class="Function">dec-true</a> <a id="2928" class="Symbol">(</a><a id="2929" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="2935" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2945" class="Symbol">_</a> <a id="2947" class="Symbol">)</a> <a id="2949" href="Relation.Nullary.Decidable.Core.html#2949" class="Bound">p</a> <a id="2951" class="Symbol">=</a> <a id="2953" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
<a id="2958" href="Relation.Nullary.Decidable.Core.html#2874" class="Function">dec-true</a> <a id="2967" class="Symbol">(</a><a id="2968" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="2974" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="2982" href="Relation.Nullary.Decidable.Core.html#2982" class="Bound">[¬p]</a><a id="2986" class="Symbol">)</a> <a id="2988" href="Relation.Nullary.Decidable.Core.html#2988" class="Bound">p</a> <a id="2990" class="Symbol">=</a> <a id="2992" href="Data.Empty.html#628" class="Function">⊥-elim</a> <a id="2999" class="Symbol">(</a><a id="3000" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="3007" href="Relation.Nullary.Decidable.Core.html#2982" class="Bound">[¬p]</a> <a id="3012" href="Relation.Nullary.Decidable.Core.html#2988" class="Bound">p</a><a id="3013" class="Symbol">)</a>
<a id="dec-false"></a><a id="3016" href="Relation.Nullary.Decidable.Core.html#3016" class="Function">dec-false</a> <a id="3026" class="Symbol">:</a> <a id="3028" class="Symbol">(</a><a id="3029" href="Relation.Nullary.Decidable.Core.html#3029" class="Bound">p?</a> <a id="3032" class="Symbol">:</a> <a id="3034" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="3038" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="3039" class="Symbol">)</a> <a id="3041" class="Symbol">→</a> <a id="3043" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="3045" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="3047" class="Symbol">→</a> <a id="3049" href="Relation.Nullary.html#1581" class="Field">does</a> <a id="3054" href="Relation.Nullary.Decidable.Core.html#3029" class="Bound">p?</a> <a id="3057" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3059" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a>
<a id="3065" href="Relation.Nullary.Decidable.Core.html#3016" class="Function">dec-false</a> <a id="3075" class="Symbol">(</a><a id="3076" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="3082" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="3091" class="Symbol">_</a> <a id="3093" class="Symbol">)</a> <a id="3095" href="Relation.Nullary.Decidable.Core.html#3095" class="Bound">¬p</a> <a id="3098" class="Symbol">=</a> <a id="3100" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
<a id="3105" href="Relation.Nullary.Decidable.Core.html#3016" class="Function">dec-false</a> <a id="3115" class="Symbol">(</a><a id="3116" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="3122" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="3130" href="Relation.Nullary.Decidable.Core.html#3130" class="Bound">[p]</a><a id="3133" class="Symbol">)</a> <a id="3135" href="Relation.Nullary.Decidable.Core.html#3135" class="Bound">¬p</a> <a id="3138" class="Symbol">=</a> <a id="3140" href="Data.Empty.html#628" class="Function">⊥-elim</a> <a id="3147" class="Symbol">(</a><a id="3148" href="Relation.Nullary.Decidable.Core.html#3135" class="Bound">¬p</a> <a id="3151" class="Symbol">(</a><a id="3152" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="3159" href="Relation.Nullary.Decidable.Core.html#3130" class="Bound">[p]</a><a id="3162" class="Symbol">))</a>
<a id="dec-yes"></a><a id="3166" href="Relation.Nullary.Decidable.Core.html#3166" class="Function">dec-yes</a> <a id="3174" class="Symbol">:</a> <a id="3176" class="Symbol">(</a><a id="3177" href="Relation.Nullary.Decidable.Core.html#3177" class="Bound">p?</a> <a id="3180" class="Symbol">:</a> <a id="3182" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="3186" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="3187" class="Symbol">)</a> <a id="3189" class="Symbol">→</a> <a id="3191" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="3193" class="Symbol">→</a> <a id="3195" href="Data.Product.html#1369" class="Function">∃</a> <a id="3197" class="Symbol">λ</a> <a id="3199" href="Relation.Nullary.Decidable.Core.html#3199" class="Bound">p′</a> <a id="3202" class="Symbol">→</a> <a id="3204" href="Relation.Nullary.Decidable.Core.html#3177" class="Bound">p?</a> <a id="3207" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3209" href="Relation.Nullary.html#1648" class="InductiveConstructor">yes</a> <a id="3213" href="Relation.Nullary.Decidable.Core.html#3199" class="Bound">p′</a>
<a id="3216" href="Relation.Nullary.Decidable.Core.html#3166" class="Function">dec-yes</a> <a id="3224" href="Relation.Nullary.Decidable.Core.html#3224" class="Bound">p?</a> <a id="3227" href="Relation.Nullary.Decidable.Core.html#3227" class="Bound">p</a> <a id="3229" class="Keyword">with</a> <a id="3234" href="Relation.Nullary.Decidable.Core.html#2874" class="Function">dec-true</a> <a id="3243" href="Relation.Nullary.Decidable.Core.html#3224" class="Bound">p?</a> <a id="3246" href="Relation.Nullary.Decidable.Core.html#3227" class="Bound">p</a>
<a id="3248" href="Relation.Nullary.Decidable.Core.html#3166" class="Function">dec-yes</a> <a id="3256" class="Symbol">(</a><a id="3257" href="Relation.Nullary.html#1648" class="InductiveConstructor">yes</a> <a id="3261" href="Relation.Nullary.Decidable.Core.html#3261" class="Bound">p′</a><a id="3263" class="Symbol">)</a> <a id="3265" href="Relation.Nullary.Decidable.Core.html#3265" class="Bound">p</a> <a id="3267" class="Symbol">|</a> <a id="3269" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="3274" class="Symbol">=</a> <a id="3276" href="Relation.Nullary.Decidable.Core.html#3261" class="Bound">p′</a> <a id="3279" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3281" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
<a id="dec-no"></a><a id="3287" href="Relation.Nullary.Decidable.Core.html#3287" class="Function">dec-no</a> <a id="3294" class="Symbol">:</a> <a id="3296" class="Symbol">(</a><a id="3297" href="Relation.Nullary.Decidable.Core.html#3297" class="Bound">p?</a> <a id="3300" class="Symbol">:</a> <a id="3302" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="3306" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="3307" class="Symbol">)</a> <a id="3309" class="Symbol">→</a> <a id="3311" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="3313" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="3315" class="Symbol">→</a> <a id="3317" href="Data.Product.html#1369" class="Function">∃</a> <a id="3319" class="Symbol">λ</a> <a id="3321" href="Relation.Nullary.Decidable.Core.html#3321" class="Bound">¬p′</a> <a id="3325" class="Symbol">→</a> <a id="3327" href="Relation.Nullary.Decidable.Core.html#3297" class="Bound">p?</a> <a id="3330" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3332" href="Relation.Nullary.html#1685" class="InductiveConstructor">no</a> <a id="3335" href="Relation.Nullary.Decidable.Core.html#3321" class="Bound">¬p′</a>
<a id="3339" href="Relation.Nullary.Decidable.Core.html#3287" class="Function">dec-no</a> <a id="3346" href="Relation.Nullary.Decidable.Core.html#3346" class="Bound">p?</a> <a id="3349" href="Relation.Nullary.Decidable.Core.html#3349" class="Bound">¬p</a> <a id="3352" class="Keyword">with</a> <a id="3357" href="Relation.Nullary.Decidable.Core.html#3016" class="Function">dec-false</a> <a id="3367" href="Relation.Nullary.Decidable.Core.html#3346" class="Bound">p?</a> <a id="3370" href="Relation.Nullary.Decidable.Core.html#3349" class="Bound">¬p</a>
<a id="3373" href="Relation.Nullary.Decidable.Core.html#3287" class="Function">dec-no</a> <a id="3380" class="Symbol">(</a><a id="3381" href="Relation.Nullary.html#1685" class="InductiveConstructor">no</a> <a id="3384" href="Relation.Nullary.Decidable.Core.html#3384" class="Bound">¬p′</a><a id="3387" class="Symbol">)</a> <a id="3389" href="Relation.Nullary.Decidable.Core.html#3389" class="Bound">¬p</a> <a id="3392" class="Symbol">|</a> <a id="3394" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="3399" class="Symbol">=</a> <a id="3401" href="Relation.Nullary.Decidable.Core.html#3384" class="Bound">¬p′</a> <a id="3405" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3407" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
<a id="dec-yes-irr"></a><a id="3413" href="Relation.Nullary.Decidable.Core.html#3413" class="Function">dec-yes-irr</a> <a id="3425" class="Symbol">:</a> <a id="3427" class="Symbol">(</a><a id="3428" href="Relation.Nullary.Decidable.Core.html#3428" class="Bound">p?</a> <a id="3431" class="Symbol">:</a> <a id="3433" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="3437" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="3438" class="Symbol">)</a> <a id="3440" class="Symbol">→</a> <a id="3442" href="Relation.Nullary.html#2040" class="Function">Irrelevant</a> <a id="3453" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="3455" class="Symbol">→</a> <a id="3457" class="Symbol">(</a><a id="3458" href="Relation.Nullary.Decidable.Core.html#3458" class="Bound">p</a> <a id="3460" class="Symbol">:</a> <a id="3462" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="3463" class="Symbol">)</a> <a id="3465" class="Symbol">→</a> <a id="3467" href="Relation.Nullary.Decidable.Core.html#3428" class="Bound">p?</a> <a id="3470" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3472" href="Relation.Nullary.html#1648" class="InductiveConstructor">yes</a> <a id="3476" href="Relation.Nullary.Decidable.Core.html#3458" class="Bound">p</a>
<a id="3478" href="Relation.Nullary.Decidable.Core.html#3413" class="Function">dec-yes-irr</a> <a id="3490" href="Relation.Nullary.Decidable.Core.html#3490" class="Bound">p?</a> <a id="3493" href="Relation.Nullary.Decidable.Core.html#3493" class="Bound">irr</a> <a id="3497" href="Relation.Nullary.Decidable.Core.html#3497" class="Bound">p</a> <a id="3499" class="Keyword">with</a> <a id="3504" href="Relation.Nullary.Decidable.Core.html#3166" class="Function">dec-yes</a> <a id="3512" href="Relation.Nullary.Decidable.Core.html#3490" class="Bound">p?</a> <a id="3515" href="Relation.Nullary.Decidable.Core.html#3497" class="Bound">p</a>
<a id="3517" class="Symbol">...</a> <a id="3521" class="Symbol">|</a> <a id="3523" href="Relation.Nullary.Decidable.Core.html#3523" class="Bound">p′</a> <a id="3526" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3528" href="Relation.Nullary.Decidable.Core.html#3528" class="Bound">eq</a> <a id="3531" class="Keyword">rewrite</a> <a id="3539" class="Bound">irr</a> <a id="3543" class="Bound">p</a> <a id="3545" href="Relation.Nullary.Decidable.Core.html#3523" class="Bound">p′</a> <a id="3548" class="Symbol">=</a> <a id="3550" href="Relation.Nullary.Decidable.Core.html#3528" class="Bound">eq</a>
<a id="3554" class="Comment">------------------------------------------------------------------------</a>
<a id="3627" class="Comment">-- Maps</a>
<a id="map′"></a><a id="3636" href="Relation.Nullary.Decidable.Core.html#3636" class="Function">map′</a> <a id="3641" class="Symbol">:</a> <a id="3643" class="Symbol">(</a><a id="3644" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="3646" class="Symbol">→</a> <a id="3648" href="Relation.Nullary.Decidable.Core.html#785" class="Generalizable">Q</a><a id="3649" class="Symbol">)</a> <a id="3651" class="Symbol">→</a> <a id="3653" class="Symbol">(</a><a id="3654" href="Relation.Nullary.Decidable.Core.html#785" class="Generalizable">Q</a> <a id="3656" class="Symbol">→</a> <a id="3658" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a><a id="3659" class="Symbol">)</a> <a id="3661" class="Symbol">→</a> <a id="3663" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="3667" href="Relation.Nullary.Decidable.Core.html#771" class="Generalizable">P</a> <a id="3669" class="Symbol">→</a> <a id="3671" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="3675" href="Relation.Nullary.Decidable.Core.html#785" class="Generalizable">Q</a>
<a id="3677" href="Relation.Nullary.html#1581" class="Field">does</a> <a id="3683" class="Symbol">(</a><a id="3684" href="Relation.Nullary.Decidable.Core.html#3636" class="Function">map′</a> <a id="3689" href="Relation.Nullary.Decidable.Core.html#3689" class="Bound">P→Q</a> <a id="3693" href="Relation.Nullary.Decidable.Core.html#3693" class="Bound">Q→P</a> <a id="3697" href="Relation.Nullary.Decidable.Core.html#3697" class="Bound">p?</a><a id="3699" class="Symbol">)</a> <a id="3719" class="Symbol">=</a> <a id="3721" href="Relation.Nullary.html#1581" class="Field">does</a> <a id="3726" href="Relation.Nullary.Decidable.Core.html#3697" class="Bound">p?</a>
<a id="3729" href="Relation.Nullary.html#1598" class="Field">proof</a> <a id="3735" class="Symbol">(</a><a id="3736" href="Relation.Nullary.Decidable.Core.html#3636" class="Function">map′</a> <a id="3741" href="Relation.Nullary.Decidable.Core.html#3741" class="Bound">P→Q</a> <a id="3745" href="Relation.Nullary.Decidable.Core.html#3745" class="Bound">Q→P</a> <a id="3749" class="Symbol">(</a><a id="3750" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="3756" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="3765" href="Relation.Nullary.Decidable.Core.html#3765" class="Bound">[p]</a><a id="3768" class="Symbol">))</a> <a id="3771" class="Symbol">=</a> <a id="3773" href="Relation.Nullary.html#902" class="InductiveConstructor">ofʸ</a> <a id="3777" class="Symbol">(</a><a id="3778" href="Relation.Nullary.Decidable.Core.html#3741" class="Bound">P→Q</a> <a id="3782" class="Symbol">(</a><a id="3783" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="3790" href="Relation.Nullary.Decidable.Core.html#3765" class="Bound">[p]</a><a id="3793" class="Symbol">))</a>
<a id="3796" href="Relation.Nullary.html#1598" class="Field">proof</a> <a id="3802" class="Symbol">(</a><a id="3803" href="Relation.Nullary.Decidable.Core.html#3636" class="Function">map′</a> <a id="3808" href="Relation.Nullary.Decidable.Core.html#3808" class="Bound">P→Q</a> <a id="3812" href="Relation.Nullary.Decidable.Core.html#3812" class="Bound">Q→P</a> <a id="3816" class="Symbol">(</a><a id="3817" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="3823" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="3831" href="Relation.Nullary.Decidable.Core.html#3831" class="Bound">[¬p]</a><a id="3835" class="Symbol">))</a> <a id="3838" class="Symbol">=</a> <a id="3840" href="Relation.Nullary.html#939" class="InductiveConstructor">ofⁿ</a> <a id="3844" class="Symbol">(</a><a id="3845" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="3852" href="Relation.Nullary.Decidable.Core.html#3831" class="Bound">[¬p]</a> <a id="3857" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="3859" href="Relation.Nullary.Decidable.Core.html#3812" class="Bound">Q→P</a><a id="3862" class="Symbol">)</a>
</pre></body></html>
Reference in New Issue Copy Permalink