/usr/share/doc/agda-stdlib-doc/html/Relation.Binary.SymmetricClosure.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 34 35 36 37 38 | <!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Relation.Binary.SymmetricClosure</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">-- Symmetric closures of binary relations</a>
<a id="148" class="Comment">------------------------------------------------------------------------</a>
<a id="222" class="Keyword">module</a> <a id="229" href="Relation.Binary.SymmetricClosure.html" class="Module">Relation.Binary.SymmetricClosure</a> <a id="262" class="Keyword">where</a>
<a id="269" class="Keyword">open</a> <a id="274" class="Keyword">import</a> <a id="281" href="Data.Sum.html" class="Module">Data.Sum</a> <a id="290" class="Symbol">as</a> <a id="293" class="Module">Sum</a> <a id="297" class="Keyword">using</a> <a id="303" class="Symbol">(</a><a id="304" href="Data.Sum.html#_%E2%8A%8E_" class="Datatype Operator">_⊎_</a><a id="307" class="Symbol">)</a>
<a id="309" class="Keyword">open</a> <a id="314" class="Keyword">import</a> <a id="321" href="Function.html" class="Module">Function</a> <a id="330" class="Keyword">using</a> <a id="336" class="Symbol">(</a><a id="337" href="Function.html#id" class="Function">id</a><a id="339" class="Symbol">)</a>
<a id="341" class="Keyword">open</a> <a id="346" class="Keyword">import</a> <a id="353" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="370" class="Keyword">open</a> <a id="375" href="Data.Sum.html" class="Module">Sum</a> <a id="379" class="Keyword">public</a> <a id="386" class="Keyword">using</a> <a id="392" class="Symbol">()</a> <a id="395" class="Keyword">renaming</a> <a id="404" class="Symbol">(</a><a id="405" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%81" class="InductiveConstructor">inj₁</a> <a id="410" class="Symbol">to</a> <a id="413" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%81" class="InductiveConstructor">fwd</a><a id="416" class="Symbol">;</a> <a id="418" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%82" class="InductiveConstructor">inj₂</a> <a id="423" class="Symbol">to</a> <a id="426" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%82" class="InductiveConstructor">bwd</a><a id="429" class="Symbol">)</a>
<a id="432" class="Comment">-- The symmetric closure of a relation.</a>
<a id="SymClosure" href="Relation.Binary.SymmetricClosure.html#SymClosure" class="Function">SymClosure</a> <a id="484" class="Symbol">:</a> <a id="486" class="Symbol">∀</a> <a id="488" class="Symbol">{</a><a id="489" href="Relation.Binary.SymmetricClosure.html#489" class="Bound">a</a> <a id="491" href="Relation.Binary.SymmetricClosure.html#491" class="Bound">ℓ</a><a id="492" class="Symbol">}</a> <a id="494" class="Symbol">{</a><a id="495" href="Relation.Binary.SymmetricClosure.html#495" class="Bound">A</a> <a id="497" class="Symbol">:</a> <a id="499" class="PrimitiveType">Set</a> <a id="503" href="Relation.Binary.SymmetricClosure.html#489" class="Bound">a</a><a id="504" class="Symbol">}</a> <a id="506" class="Symbol">→</a> <a id="508" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="512" href="Relation.Binary.SymmetricClosure.html#495" class="Bound">A</a> <a id="514" href="Relation.Binary.SymmetricClosure.html#491" class="Bound">ℓ</a> <a id="516" class="Symbol">→</a> <a id="518" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="522" href="Relation.Binary.SymmetricClosure.html#495" class="Bound">A</a> <a id="524" href="Relation.Binary.SymmetricClosure.html#491" class="Bound">ℓ</a>
<a id="526" href="Relation.Binary.SymmetricClosure.html#SymClosure" class="Function">SymClosure</a> <a id="537" href="Relation.Binary.SymmetricClosure.html#537" class="Bound Operator">_∼_</a> <a id="541" href="Relation.Binary.SymmetricClosure.html#541" class="Bound">a</a> <a id="543" href="Relation.Binary.SymmetricClosure.html#543" class="Bound">b</a> <a id="545" class="Symbol">=</a> <a id="547" href="Relation.Binary.SymmetricClosure.html#541" class="Bound">a</a> <a id="549" href="Relation.Binary.SymmetricClosure.html#537" class="Bound Operator">∼</a> <a id="551" href="Relation.Binary.SymmetricClosure.html#543" class="Bound">b</a> <a id="553" href="Data.Sum.html#_%E2%8A%8E_" class="Datatype Operator">⊎</a> <a id="555" href="Relation.Binary.SymmetricClosure.html#543" class="Bound">b</a> <a id="557" href="Relation.Binary.SymmetricClosure.html#537" class="Bound Operator">∼</a> <a id="559" href="Relation.Binary.SymmetricClosure.html#541" class="Bound">a</a>
<a id="562" class="Keyword">module</a> <a id="569" href="Relation.Binary.SymmetricClosure.html#569" class="Module">_</a> <a id="571" class="Symbol">{</a><a id="572" href="Relation.Binary.SymmetricClosure.html#572" class="Bound">a</a> <a id="574" href="Relation.Binary.SymmetricClosure.html#574" class="Bound">ℓ</a><a id="575" class="Symbol">}</a> <a id="577" class="Symbol">{</a><a id="578" href="Relation.Binary.SymmetricClosure.html#578" class="Bound">A</a> <a id="580" class="Symbol">:</a> <a id="582" class="PrimitiveType">Set</a> <a id="586" href="Relation.Binary.SymmetricClosure.html#572" class="Bound">a</a><a id="587" class="Symbol">}</a> <a id="589" class="Keyword">where</a>
<a id="598" class="Comment">-- Symmetric closures are symmetric.</a>
<a id="638" href="Relation.Binary.SymmetricClosure.html#638" class="Function">symmetric</a> <a id="648" class="Symbol">:</a> <a id="650" class="Symbol">(</a><a id="651" href="Relation.Binary.SymmetricClosure.html#651" class="Bound Operator">_∼_</a> <a id="655" class="Symbol">:</a> <a id="657" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="661" href="Relation.Binary.SymmetricClosure.html#578" class="Bound">A</a> <a id="663" href="Relation.Binary.SymmetricClosure.html#574" class="Bound">ℓ</a><a id="664" class="Symbol">)</a> <a id="666" class="Symbol">→</a> <a id="668" href="Relation.Binary.Core.html#Symmetric" class="Function">Symmetric</a> <a id="678" class="Symbol">(</a><a id="679" href="Relation.Binary.SymmetricClosure.html#SymClosure" class="Function">SymClosure</a> <a id="690" href="Relation.Binary.SymmetricClosure.html#651" class="Bound Operator">_∼_</a><a id="693" class="Symbol">)</a>
<a id="697" href="Relation.Binary.SymmetricClosure.html#638" class="Function">symmetric</a> <a id="707" class="Symbol">_</a> <a id="709" class="Symbol">(</a><a id="710" href="Data.Sum.html#_%E2%8A%8E_.fwd" class="InductiveConstructor">fwd</a> <a id="714" href="Relation.Binary.SymmetricClosure.html#714" class="Bound">a∼b</a><a id="717" class="Symbol">)</a> <a id="719" class="Symbol">=</a> <a id="721" href="Data.Sum.html#_%E2%8A%8E_.bwd" class="InductiveConstructor">bwd</a> <a id="725" href="Relation.Binary.SymmetricClosure.html#714" class="Bound">a∼b</a>
<a id="731" href="Relation.Binary.SymmetricClosure.html#638" class="Function">symmetric</a> <a id="741" class="Symbol">_</a> <a id="743" class="Symbol">(</a><a id="744" href="Data.Sum.html#_%E2%8A%8E_.bwd" class="InductiveConstructor">bwd</a> <a id="748" href="Relation.Binary.SymmetricClosure.html#748" class="Bound">b∼a</a><a id="751" class="Symbol">)</a> <a id="753" class="Symbol">=</a> <a id="755" href="Data.Sum.html#_%E2%8A%8E_.fwd" class="InductiveConstructor">fwd</a> <a id="759" href="Relation.Binary.SymmetricClosure.html#748" class="Bound">b∼a</a>
<a id="766" class="Comment">-- A generalised variant of map which allows the index type to change.</a>
<a id="840" href="Relation.Binary.SymmetricClosure.html#840" class="Function">gmap</a> <a id="845" class="Symbol">:</a> <a id="847" class="Symbol">∀</a> <a id="849" class="Symbol">{</a><a id="850" href="Relation.Binary.SymmetricClosure.html#850" class="Bound">b</a> <a id="852" href="Relation.Binary.SymmetricClosure.html#852" class="Bound">ℓ₂</a><a id="854" class="Symbol">}</a> <a id="856" class="Symbol">{</a><a id="857" href="Relation.Binary.SymmetricClosure.html#857" class="Bound">B</a> <a id="859" class="Symbol">:</a> <a id="861" class="PrimitiveType">Set</a> <a id="865" href="Relation.Binary.SymmetricClosure.html#850" class="Bound">b</a><a id="866" class="Symbol">}</a> <a id="868" class="Symbol">{</a><a id="869" href="Relation.Binary.SymmetricClosure.html#869" class="Bound">P</a> <a id="871" class="Symbol">:</a> <a id="873" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="877" href="Relation.Binary.SymmetricClosure.html#578" class="Bound">A</a> <a id="879" href="Relation.Binary.SymmetricClosure.html#574" class="Bound">ℓ</a><a id="880" class="Symbol">}</a> <a id="882" class="Symbol">{</a><a id="883" href="Relation.Binary.SymmetricClosure.html#883" class="Bound">Q</a> <a id="885" class="Symbol">:</a> <a id="887" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="891" href="Relation.Binary.SymmetricClosure.html#857" class="Bound">B</a> <a id="893" href="Relation.Binary.SymmetricClosure.html#852" class="Bound">ℓ₂</a><a id="895" class="Symbol">}</a> <a id="897" class="Symbol">→</a>
<a id="908" class="Symbol">(</a><a id="909" href="Relation.Binary.SymmetricClosure.html#909" class="Bound">f</a> <a id="911" class="Symbol">:</a> <a id="913" href="Relation.Binary.SymmetricClosure.html#578" class="Bound">A</a> <a id="915" class="Symbol">→</a> <a id="917" href="Relation.Binary.SymmetricClosure.html#857" class="Bound">B</a><a id="918" class="Symbol">)</a> <a id="920" class="Symbol">→</a> <a id="922" href="Relation.Binary.SymmetricClosure.html#869" class="Bound">P</a> <a id="924" href="Relation.Binary.Core.html#_%3D%5B_%5D%E2%87%92_" class="Function Operator">=[</a> <a id="927" href="Relation.Binary.SymmetricClosure.html#909" class="Bound">f</a> <a id="929" href="Relation.Binary.Core.html#_%3D%5B_%5D%E2%87%92_" class="Function Operator">]⇒</a> <a id="932" href="Relation.Binary.SymmetricClosure.html#883" class="Bound">Q</a> <a id="934" class="Symbol">→</a> <a id="936" href="Relation.Binary.SymmetricClosure.html#SymClosure" class="Function">SymClosure</a> <a id="947" href="Relation.Binary.SymmetricClosure.html#869" class="Bound">P</a> <a id="949" href="Relation.Binary.Core.html#_%3D%5B_%5D%E2%87%92_" class="Function Operator">=[</a> <a id="952" href="Relation.Binary.SymmetricClosure.html#909" class="Bound">f</a> <a id="954" href="Relation.Binary.Core.html#_%3D%5B_%5D%E2%87%92_" class="Function Operator">]⇒</a> <a id="957" href="Relation.Binary.SymmetricClosure.html#SymClosure" class="Function">SymClosure</a> <a id="968" href="Relation.Binary.SymmetricClosure.html#883" class="Bound">Q</a>
<a id="972" href="Relation.Binary.SymmetricClosure.html#840" class="Function">gmap</a> <a id="977" class="Symbol">_</a> <a id="979" href="Relation.Binary.SymmetricClosure.html#979" class="Bound">g</a> <a id="981" class="Symbol">=</a> <a id="983" href="Data.Sum.html#map" class="Function">Sum.map</a> <a id="991" href="Relation.Binary.SymmetricClosure.html#979" class="Bound">g</a> <a id="993" href="Relation.Binary.SymmetricClosure.html#979" class="Bound">g</a>
<a id="998" href="Relation.Binary.SymmetricClosure.html#998" class="Function">map</a> <a id="1002" class="Symbol">:</a> <a id="1004" class="Symbol">∀</a> <a id="1006" class="Symbol">{</a><a id="1007" href="Relation.Binary.SymmetricClosure.html#1007" class="Bound">ℓ₂</a><a id="1009" class="Symbol">}</a> <a id="1011" class="Symbol">{</a><a id="1012" href="Relation.Binary.SymmetricClosure.html#1012" class="Bound">P</a> <a id="1014" class="Symbol">:</a> <a id="1016" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1020" href="Relation.Binary.SymmetricClosure.html#578" class="Bound">A</a> <a id="1022" href="Relation.Binary.SymmetricClosure.html#574" class="Bound">ℓ</a><a id="1023" class="Symbol">}</a> <a id="1025" class="Symbol">{</a><a id="1026" href="Relation.Binary.SymmetricClosure.html#1026" class="Bound">Q</a> <a id="1028" class="Symbol">:</a> <a id="1030" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1034" href="Relation.Binary.SymmetricClosure.html#578" class="Bound">A</a> <a id="1036" href="Relation.Binary.SymmetricClosure.html#1007" class="Bound">ℓ₂</a><a id="1038" class="Symbol">}</a> <a id="1040" class="Symbol">→</a>
<a id="1050" href="Relation.Binary.SymmetricClosure.html#1012" class="Bound">P</a> <a id="1052" href="Relation.Binary.Core.html#_%E2%87%92_" class="Function Operator">⇒</a> <a id="1054" href="Relation.Binary.SymmetricClosure.html#1026" class="Bound">Q</a> <a id="1056" class="Symbol">→</a> <a id="1058" href="Relation.Binary.SymmetricClosure.html#SymClosure" class="Function">SymClosure</a> <a id="1069" href="Relation.Binary.SymmetricClosure.html#1012" class="Bound">P</a> <a id="1071" href="Relation.Binary.Core.html#_%E2%87%92_" class="Function Operator">⇒</a> <a id="1073" href="Relation.Binary.SymmetricClosure.html#SymClosure" class="Function">SymClosure</a> <a id="1084" href="Relation.Binary.SymmetricClosure.html#1026" class="Bound">Q</a>
<a id="1088" href="Relation.Binary.SymmetricClosure.html#998" class="Function">map</a> <a id="1092" class="Symbol">=</a> <a id="1094" href="Relation.Binary.SymmetricClosure.html#840" class="Function">gmap</a> <a id="1099" href="Function.html#id" class="Function">id</a>
</pre></body></html>
|