/usr/share/doc/agda-stdlib-doc/html/Relation.Nullary.Sum.html is in agda-stdlib-doc 0.14-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 | <!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Relation.Nullary.Sum</title><link rel="stylesheet" href="Agda.css"></head><body><pre><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">-- Sums of nullary relations</a>
<a id="135" class="Comment">------------------------------------------------------------------------</a>
<a id="209" class="Keyword">module</a> <a id="216" href="Relation.Nullary.Sum.html" class="Module">Relation.Nullary.Sum</a> <a id="237" class="Keyword">where</a>
<a id="244" class="Keyword">open</a> <a id="249" class="Keyword">import</a> <a id="256" href="Data.Sum.html" class="Module">Data.Sum</a>
<a id="265" class="Keyword">open</a> <a id="270" class="Keyword">import</a> <a id="277" href="Data.Empty.html" class="Module">Data.Empty</a>
<a id="288" class="Keyword">open</a> <a id="293" class="Keyword">import</a> <a id="300" href="Level.html" class="Module">Level</a>
<a id="306" class="Keyword">open</a> <a id="311" class="Keyword">import</a> <a id="318" href="Relation.Nullary.html" class="Module">Relation.Nullary</a>
<a id="336" class="Comment">-- Some properties which are preserved by _⊎_.</a>
<a id="384" class="Keyword">infixr</a> <a id="391" class="Number">1</a> <a id="393" href="Relation.Nullary.Sum.html#_%C2%AC-%E2%8A%8E_" class="Function Operator">_¬-⊎_</a> <a id="399" href="Relation.Nullary.Sum.html#_%E2%8A%8E-dec_" class="Function Operator">_⊎-dec_</a>
<a id="_¬-⊎_" href="Relation.Nullary.Sum.html#_%C2%AC-%E2%8A%8E_" class="Function Operator">_¬-⊎_</a> <a id="414" class="Symbol">:</a> <a id="416" class="Symbol">∀</a> <a id="418" class="Symbol">{</a><a id="419" href="Relation.Nullary.Sum.html#419" class="Bound">p</a> <a id="421" href="Relation.Nullary.Sum.html#421" class="Bound">q</a><a id="422" class="Symbol">}</a> <a id="424" class="Symbol">{</a><a id="425" href="Relation.Nullary.Sum.html#425" class="Bound">P</a> <a id="427" class="Symbol">:</a> <a id="429" class="PrimitiveType">Set</a> <a id="433" href="Relation.Nullary.Sum.html#419" class="Bound">p</a><a id="434" class="Symbol">}</a> <a id="436" class="Symbol">{</a><a id="437" href="Relation.Nullary.Sum.html#437" class="Bound">Q</a> <a id="439" class="Symbol">:</a> <a id="441" class="PrimitiveType">Set</a> <a id="445" href="Relation.Nullary.Sum.html#421" class="Bound">q</a><a id="446" class="Symbol">}</a> <a id="448" class="Symbol">→</a>
<a id="458" href="Relation.Nullary.html#%C2%AC_" class="Function Operator">¬</a> <a id="460" href="Relation.Nullary.Sum.html#425" class="Bound">P</a> <a id="462" class="Symbol">→</a> <a id="464" href="Relation.Nullary.html#%C2%AC_" class="Function Operator">¬</a> <a id="466" href="Relation.Nullary.Sum.html#437" class="Bound">Q</a> <a id="468" class="Symbol">→</a> <a id="470" href="Relation.Nullary.html#%C2%AC_" class="Function Operator">¬</a> <a id="472" class="Symbol">(</a><a id="473" href="Relation.Nullary.Sum.html#425" class="Bound">P</a> <a id="475" href="Data.Sum.html#_%E2%8A%8E_" class="Datatype Operator">⊎</a> <a id="477" href="Relation.Nullary.Sum.html#437" class="Bound">Q</a><a id="478" class="Symbol">)</a>
<a id="480" class="Symbol">(</a><a id="481" href="Relation.Nullary.Sum.html#481" class="Bound">¬p</a> <a id="484" href="Relation.Nullary.Sum.html#_%C2%AC-%E2%8A%8E_" class="Function Operator">¬-⊎</a> <a id="488" href="Relation.Nullary.Sum.html#488" class="Bound">¬q</a><a id="490" class="Symbol">)</a> <a id="492" class="Symbol">(</a><a id="493" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%81" class="InductiveConstructor">inj₁</a> <a id="498" href="Relation.Nullary.Sum.html#498" class="Bound">p</a><a id="499" class="Symbol">)</a> <a id="501" class="Symbol">=</a> <a id="503" href="Relation.Nullary.Sum.html#481" class="Bound">¬p</a> <a id="506" href="Relation.Nullary.Sum.html#498" class="Bound">p</a>
<a id="508" class="Symbol">(</a><a id="509" href="Relation.Nullary.Sum.html#509" class="Bound">¬p</a> <a id="512" href="Relation.Nullary.Sum.html#_%C2%AC-%E2%8A%8E_" class="Function Operator">¬-⊎</a> <a id="516" href="Relation.Nullary.Sum.html#516" class="Bound">¬q</a><a id="518" class="Symbol">)</a> <a id="520" class="Symbol">(</a><a id="521" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%82" class="InductiveConstructor">inj₂</a> <a id="526" href="Relation.Nullary.Sum.html#526" class="Bound">q</a><a id="527" class="Symbol">)</a> <a id="529" class="Symbol">=</a> <a id="531" href="Relation.Nullary.Sum.html#516" class="Bound">¬q</a> <a id="534" href="Relation.Nullary.Sum.html#526" class="Bound">q</a>
<a id="_⊎-dec_" href="Relation.Nullary.Sum.html#_%E2%8A%8E-dec_" class="Function Operator">_⊎-dec_</a> <a id="545" class="Symbol">:</a> <a id="547" class="Symbol">∀</a> <a id="549" class="Symbol">{</a><a id="550" href="Relation.Nullary.Sum.html#550" class="Bound">p</a> <a id="552" href="Relation.Nullary.Sum.html#552" class="Bound">q</a><a id="553" class="Symbol">}</a> <a id="555" class="Symbol">{</a><a id="556" href="Relation.Nullary.Sum.html#556" class="Bound">P</a> <a id="558" class="Symbol">:</a> <a id="560" class="PrimitiveType">Set</a> <a id="564" href="Relation.Nullary.Sum.html#550" class="Bound">p</a><a id="565" class="Symbol">}</a> <a id="567" class="Symbol">{</a><a id="568" href="Relation.Nullary.Sum.html#568" class="Bound">Q</a> <a id="570" class="Symbol">:</a> <a id="572" class="PrimitiveType">Set</a> <a id="576" href="Relation.Nullary.Sum.html#552" class="Bound">q</a><a id="577" class="Symbol">}</a> <a id="579" class="Symbol">→</a>
<a id="591" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="595" href="Relation.Nullary.Sum.html#556" class="Bound">P</a> <a id="597" class="Symbol">→</a> <a id="599" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="603" href="Relation.Nullary.Sum.html#568" class="Bound">Q</a> <a id="605" class="Symbol">→</a> <a id="607" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="611" class="Symbol">(</a><a id="612" href="Relation.Nullary.Sum.html#556" class="Bound">P</a> <a id="614" href="Data.Sum.html#_%E2%8A%8E_" class="Datatype Operator">⊎</a> <a id="616" href="Relation.Nullary.Sum.html#568" class="Bound">Q</a><a id="617" class="Symbol">)</a>
<a id="619" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="623" href="Relation.Nullary.Sum.html#623" class="Bound">p</a> <a id="625" href="Relation.Nullary.Sum.html#_%E2%8A%8E-dec_" class="Function Operator">⊎-dec</a> <a id="631" class="Symbol">_</a> <a id="637" class="Symbol">=</a> <a id="639" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="643" class="Symbol">(</a><a id="644" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%81" class="InductiveConstructor">inj₁</a> <a id="649" href="Relation.Nullary.Sum.html#623" class="Bound">p</a><a id="650" class="Symbol">)</a>
<a id="652" class="CatchallClause Symbol">_</a><a id="653" class="CatchallClause"> </a><a id="658" href="Relation.Nullary.Sum.html#_%E2%8A%8E-dec_" class="CatchallClause Function Operator">⊎-dec</a><a id="663" class="CatchallClause"> </a><a id="664" href="Relation.Nullary.html#Dec.yes" class="CatchallClause InductiveConstructor">yes</a><a id="667" class="CatchallClause"> </a><a id="668" href="Relation.Nullary.Sum.html#668" class="CatchallClause Bound">q</a> <a id="670" class="Symbol">=</a> <a id="672" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="676" class="Symbol">(</a><a id="677" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%82" class="InductiveConstructor">inj₂</a> <a id="682" href="Relation.Nullary.Sum.html#668" class="Bound">q</a><a id="683" class="Symbol">)</a>
<a id="685" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="688" href="Relation.Nullary.Sum.html#688" class="Bound">¬p</a> <a id="691" href="Relation.Nullary.Sum.html#_%E2%8A%8E-dec_" class="Function Operator">⊎-dec</a> <a id="697" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="700" href="Relation.Nullary.Sum.html#700" class="Bound">¬q</a> <a id="703" class="Symbol">=</a> <a id="705" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="708" href="Relation.Nullary.Sum.html#725" class="Function">helper</a>
<a id="717" class="Keyword">where</a>
<a id="725" href="Relation.Nullary.Sum.html#725" class="Function">helper</a> <a id="732" class="Symbol">:</a> <a id="734" class="Symbol">_</a> <a id="736" href="Data.Sum.html#_%E2%8A%8E_" class="Datatype Operator">⊎</a> <a id="738" class="Symbol">_</a> <a id="740" class="Symbol">→</a> <a id="742" href="Data.Empty.html#%E2%8A%A5" class="Datatype">⊥</a>
<a id="746" href="Relation.Nullary.Sum.html#725" class="Function">helper</a> <a id="753" class="Symbol">(</a><a id="754" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%81" class="InductiveConstructor">inj₁</a> <a id="759" href="Relation.Nullary.Sum.html#759" class="Bound">p</a><a id="760" class="Symbol">)</a> <a id="762" class="Symbol">=</a> <a id="764" href="Relation.Nullary.Sum.html#688" class="Bound">¬p</a> <a id="767" href="Relation.Nullary.Sum.html#759" class="Bound">p</a>
<a id="771" href="Relation.Nullary.Sum.html#725" class="Function">helper</a> <a id="778" class="Symbol">(</a><a id="779" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%82" class="InductiveConstructor">inj₂</a> <a id="784" href="Relation.Nullary.Sum.html#784" class="Bound">q</a><a id="785" class="Symbol">)</a> <a id="787" class="Symbol">=</a> <a id="789" href="Relation.Nullary.Sum.html#700" class="Bound">¬q</a> <a id="792" href="Relation.Nullary.Sum.html#784" class="Bound">q</a>
</pre></body></html>
|