/usr/share/doc/agda-stdlib-doc/html/Relation.Binary.EquivalenceClosure.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 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 | <!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Relation.Binary.EquivalenceClosure</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">-- Equivalence closures of binary relations</a>
<a id="150" class="Comment">------------------------------------------------------------------------</a>
<a id="224" class="Keyword">module</a> <a id="231" href="Relation.Binary.EquivalenceClosure.html" class="Module">Relation.Binary.EquivalenceClosure</a> <a id="266" class="Keyword">where</a>
<a id="273" class="Keyword">open</a> <a id="278" class="Keyword">import</a> <a id="285" href="Data.Star.html" class="Module">Data.Star</a> <a id="295" class="Symbol">as</a> <a id="298" class="Module">Star</a> <a id="303" class="Keyword">using</a> <a id="309" class="Symbol">(</a><a id="310" href="Data.Star.html#Star" class="Datatype">Star</a><a id="314" class="Symbol">;</a> <a id="316" href="Data.Star.html#Star.%CE%B5" class="InductiveConstructor">ε</a><a id="317" class="Symbol">;</a> <a id="319" href="Data.Star.html#_%E2%97%85%E2%97%85_" class="Function Operator">_◅◅_</a><a id="323" class="Symbol">;</a> <a id="325" href="Data.Star.html#reverse" class="Function">reverse</a><a id="332" class="Symbol">)</a>
<a id="334" class="Keyword">open</a> <a id="339" class="Keyword">import</a> <a id="346" href="Function.html" class="Module">Function</a> <a id="355" class="Keyword">using</a> <a id="361" class="Symbol">(</a><a id="362" href="Function.html#flip" class="Function">flip</a><a id="366" class="Symbol">;</a> <a id="368" href="Function.html#id" class="Function">id</a><a id="370" class="Symbol">;</a> <a id="372" href="Function.html#_%E2%88%98_" class="Function Operator">_∘_</a><a id="375" class="Symbol">)</a>
<a id="377" class="Keyword">open</a> <a id="382" class="Keyword">import</a> <a id="389" href="Level.html" class="Module">Level</a> <a id="395" class="Keyword">using</a> <a id="401" class="Symbol">(</a><a id="402" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">_⊔_</a><a id="405" class="Symbol">)</a>
<a id="407" class="Keyword">open</a> <a id="412" class="Keyword">import</a> <a id="419" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="435" class="Keyword">open</a> <a id="440" class="Keyword">import</a> <a id="447" href="Relation.Binary.SymmetricClosure.html" class="Module">Relation.Binary.SymmetricClosure</a> <a id="480" class="Symbol">as</a> <a id="483" class="Module">SC</a> <a id="486" class="Keyword">using</a> <a id="492" class="Symbol">(</a><a id="493" href="Relation.Binary.SymmetricClosure.html#SymClosure" class="Function">SymClosure</a><a id="503" class="Symbol">)</a>
<a id="506" class="Comment">-- The reflexive, transitive and symmetric closure of a binary</a>
<a id="569" class="Comment">-- relation (aka the equivalence closure).</a>
<a id="EqClosure" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="623" class="Symbol">:</a> <a id="625" class="Symbol">∀</a> <a id="627" class="Symbol">{</a><a id="628" href="Relation.Binary.EquivalenceClosure.html#628" class="Bound">a</a> <a id="630" href="Relation.Binary.EquivalenceClosure.html#630" class="Bound">ℓ</a><a id="631" class="Symbol">}</a> <a id="633" class="Symbol">{</a><a id="634" href="Relation.Binary.EquivalenceClosure.html#634" class="Bound">A</a> <a id="636" class="Symbol">:</a> <a id="638" class="PrimitiveType">Set</a> <a id="642" href="Relation.Binary.EquivalenceClosure.html#628" class="Bound">a</a><a id="643" class="Symbol">}</a> <a id="645" class="Symbol">→</a> <a id="647" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="651" href="Relation.Binary.EquivalenceClosure.html#634" class="Bound">A</a> <a id="653" href="Relation.Binary.EquivalenceClosure.html#630" class="Bound">ℓ</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.EquivalenceClosure.html#634" class="Bound">A</a> <a id="663" class="Symbol">(</a><a id="664" href="Relation.Binary.EquivalenceClosure.html#628" class="Bound">a</a> <a id="666" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">⊔</a> <a id="668" href="Relation.Binary.EquivalenceClosure.html#630" class="Bound">ℓ</a><a id="669" class="Symbol">)</a>
<a id="671" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="681" href="Relation.Binary.EquivalenceClosure.html#681" class="Bound Operator">_∼_</a> <a id="685" class="Symbol">=</a> <a id="687" href="Data.Star.html#Star" class="Datatype">Star</a> <a id="692" class="Symbol">(</a><a id="693" href="Relation.Binary.SymmetricClosure.html#SymClosure" class="Function">SymClosure</a> <a id="704" href="Relation.Binary.EquivalenceClosure.html#681" class="Bound Operator">_∼_</a><a id="707" class="Symbol">)</a>
<a id="710" class="Keyword">module</a> <a id="717" href="Relation.Binary.EquivalenceClosure.html#717" class="Module">_</a> <a id="719" class="Symbol">{</a><a id="720" href="Relation.Binary.EquivalenceClosure.html#720" class="Bound">a</a> <a id="722" href="Relation.Binary.EquivalenceClosure.html#722" class="Bound">ℓ</a><a id="723" class="Symbol">}</a> <a id="725" class="Symbol">{</a><a id="726" href="Relation.Binary.EquivalenceClosure.html#726" class="Bound">A</a> <a id="728" class="Symbol">:</a> <a id="730" class="PrimitiveType">Set</a> <a id="734" href="Relation.Binary.EquivalenceClosure.html#720" class="Bound">a</a><a id="735" class="Symbol">}</a> <a id="737" class="Keyword">where</a>
<a id="746" class="Comment">-- Equivalence closures are equivalences.</a>
<a id="791" href="Relation.Binary.EquivalenceClosure.html#791" class="Function">reflexive</a> <a id="801" class="Symbol">:</a> <a id="803" class="Symbol">(</a><a id="804" href="Relation.Binary.EquivalenceClosure.html#804" class="Bound Operator">_∼_</a> <a id="808" class="Symbol">:</a> <a id="810" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="814" href="Relation.Binary.EquivalenceClosure.html#726" class="Bound">A</a> <a id="816" href="Relation.Binary.EquivalenceClosure.html#722" class="Bound">ℓ</a><a id="817" class="Symbol">)</a> <a id="819" class="Symbol">→</a> <a id="821" href="Relation.Binary.Core.html#Reflexive" class="Function">Reflexive</a> <a id="831" class="Symbol">(</a><a id="832" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="842" href="Relation.Binary.EquivalenceClosure.html#804" class="Bound Operator">_∼_</a><a id="845" class="Symbol">)</a>
<a id="849" href="Relation.Binary.EquivalenceClosure.html#791" class="Function">reflexive</a> <a id="859" href="Relation.Binary.EquivalenceClosure.html#859" class="Bound Operator">_∼_</a> <a id="863" class="Symbol">=</a> <a id="865" href="Data.Star.html#Star.%CE%B5" class="InductiveConstructor">ε</a>
<a id="870" href="Relation.Binary.EquivalenceClosure.html#870" class="Function">transitive</a> <a id="881" class="Symbol">:</a> <a id="883" class="Symbol">(</a><a id="884" href="Relation.Binary.EquivalenceClosure.html#884" class="Bound Operator">_∼_</a> <a id="888" class="Symbol">:</a> <a id="890" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="894" href="Relation.Binary.EquivalenceClosure.html#726" class="Bound">A</a> <a id="896" href="Relation.Binary.EquivalenceClosure.html#722" class="Bound">ℓ</a><a id="897" class="Symbol">)</a> <a id="899" class="Symbol">→</a> <a id="901" href="Relation.Binary.Core.html#Transitive" class="Function">Transitive</a> <a id="912" class="Symbol">(</a><a id="913" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="923" href="Relation.Binary.EquivalenceClosure.html#884" class="Bound Operator">_∼_</a><a id="926" class="Symbol">)</a>
<a id="930" href="Relation.Binary.EquivalenceClosure.html#870" class="Function">transitive</a> <a id="941" href="Relation.Binary.EquivalenceClosure.html#941" class="Bound Operator">_∼_</a> <a id="945" class="Symbol">=</a> <a id="947" href="Data.Star.html#_%E2%97%85%E2%97%85_" class="Function Operator">_◅◅_</a>
<a id="955" href="Relation.Binary.EquivalenceClosure.html#955" class="Function">symmetric</a> <a id="965" class="Symbol">:</a> <a id="967" class="Symbol">(</a><a id="968" href="Relation.Binary.EquivalenceClosure.html#968" class="Bound Operator">_∼_</a> <a id="972" class="Symbol">:</a> <a id="974" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="978" href="Relation.Binary.EquivalenceClosure.html#726" class="Bound">A</a> <a id="980" href="Relation.Binary.EquivalenceClosure.html#722" class="Bound">ℓ</a><a id="981" class="Symbol">)</a> <a id="983" class="Symbol">→</a> <a id="985" href="Relation.Binary.Core.html#Symmetric" class="Function">Symmetric</a> <a id="995" class="Symbol">(</a><a id="996" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="1006" href="Relation.Binary.EquivalenceClosure.html#968" class="Bound Operator">_∼_</a><a id="1009" class="Symbol">)</a>
<a id="1013" href="Relation.Binary.EquivalenceClosure.html#955" class="Function">symmetric</a> <a id="1023" href="Relation.Binary.EquivalenceClosure.html#1023" class="Bound Operator">_∼_</a> <a id="1027" class="Symbol">=</a> <a id="1029" href="Data.Star.html#reverse" class="Function">reverse</a> <a id="1037" class="Symbol">(</a><a id="1038" href="Relation.Binary.SymmetricClosure.html#638" class="Function">SC.symmetric</a> <a id="1051" href="Relation.Binary.EquivalenceClosure.html#1023" class="Bound Operator">_∼_</a><a id="1054" class="Symbol">)</a>
<a id="1059" href="Relation.Binary.EquivalenceClosure.html#1059" class="Function">isEquivalence</a> <a id="1073" class="Symbol">:</a> <a id="1075" class="Symbol">(</a><a id="1076" href="Relation.Binary.EquivalenceClosure.html#1076" class="Bound Operator">_∼_</a> <a id="1080" class="Symbol">:</a> <a id="1082" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1086" href="Relation.Binary.EquivalenceClosure.html#726" class="Bound">A</a> <a id="1088" href="Relation.Binary.EquivalenceClosure.html#722" class="Bound">ℓ</a><a id="1089" class="Symbol">)</a> <a id="1091" class="Symbol">→</a> <a id="1093" href="Relation.Binary.Core.html#IsEquivalence" class="Record">IsEquivalence</a> <a id="1107" class="Symbol">(</a><a id="1108" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="1118" href="Relation.Binary.EquivalenceClosure.html#1076" class="Bound Operator">_∼_</a><a id="1121" class="Symbol">)</a>
<a id="1125" href="Relation.Binary.EquivalenceClosure.html#1059" class="Function">isEquivalence</a> <a id="1139" href="Relation.Binary.EquivalenceClosure.html#1139" class="Bound Operator">_∼_</a> <a id="1143" class="Symbol">=</a> <a id="1145" class="Keyword">record</a>
<a id="1156" class="Symbol">{</a> <a id="1158" class="Field">refl</a> <a id="1164" class="Symbol">=</a> <a id="1166" href="Relation.Binary.EquivalenceClosure.html#791" class="Function">reflexive</a> <a id="1177" href="Relation.Binary.EquivalenceClosure.html#1139" class="Bound Operator">_∼_</a>
<a id="1185" class="Symbol">;</a> <a id="1187" class="Field">sym</a> <a id="1193" class="Symbol">=</a> <a id="1195" href="Relation.Binary.EquivalenceClosure.html#955" class="Function">symmetric</a> <a id="1206" href="Relation.Binary.EquivalenceClosure.html#1139" class="Bound Operator">_∼_</a>
<a id="1214" class="Symbol">;</a> <a id="1216" class="Field">trans</a> <a id="1222" class="Symbol">=</a> <a id="1224" href="Relation.Binary.EquivalenceClosure.html#870" class="Function">transitive</a> <a id="1235" href="Relation.Binary.EquivalenceClosure.html#1139" class="Bound Operator">_∼_</a>
<a id="1243" class="Symbol">}</a>
<a id="1248" class="Comment">-- The setoid associated with an equivalence closure.</a>
<a id="1305" href="Relation.Binary.EquivalenceClosure.html#1305" class="Function">setoid</a> <a id="1312" class="Symbol">:</a> <a id="1314" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1318" href="Relation.Binary.EquivalenceClosure.html#726" class="Bound">A</a> <a id="1320" href="Relation.Binary.EquivalenceClosure.html#722" class="Bound">ℓ</a> <a id="1322" class="Symbol">→</a> <a id="1324" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="1331" href="Relation.Binary.EquivalenceClosure.html#720" class="Bound">a</a> <a id="1333" class="Symbol">(</a><a id="1334" href="Relation.Binary.EquivalenceClosure.html#720" class="Bound">a</a> <a id="1336" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">⊔</a> <a id="1338" href="Relation.Binary.EquivalenceClosure.html#722" class="Bound">ℓ</a><a id="1339" class="Symbol">)</a>
<a id="1343" href="Relation.Binary.EquivalenceClosure.html#1305" class="Function">setoid</a> <a id="1350" href="Relation.Binary.EquivalenceClosure.html#1350" class="Bound Operator">_∼_</a> <a id="1354" class="Symbol">=</a> <a id="1356" class="Keyword">record</a>
<a id="1367" class="Symbol">{</a> <a id="1369" class="Field Operator">_≈_</a> <a id="1383" class="Symbol">=</a> <a id="1385" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="1395" href="Relation.Binary.EquivalenceClosure.html#1350" class="Bound Operator">_∼_</a>
<a id="1403" class="Symbol">;</a> <a id="1405" class="Field">isEquivalence</a> <a id="1419" class="Symbol">=</a> <a id="1421" href="Relation.Binary.EquivalenceClosure.html#1059" class="Function">isEquivalence</a> <a id="1435" href="Relation.Binary.EquivalenceClosure.html#1350" class="Bound Operator">_∼_</a>
<a id="1443" class="Symbol">}</a>
<a id="1448" class="Comment">-- A generalised variant of map which allows the index type to change.</a>
<a id="1522" href="Relation.Binary.EquivalenceClosure.html#1522" class="Function">gmap</a> <a id="1527" class="Symbol">:</a> <a id="1529" class="Symbol">∀</a> <a id="1531" class="Symbol">{</a><a id="1532" href="Relation.Binary.EquivalenceClosure.html#1532" class="Bound">b</a> <a id="1534" href="Relation.Binary.EquivalenceClosure.html#1534" class="Bound">ℓ₂</a><a id="1536" class="Symbol">}</a> <a id="1538" class="Symbol">{</a><a id="1539" href="Relation.Binary.EquivalenceClosure.html#1539" class="Bound">B</a> <a id="1541" class="Symbol">:</a> <a id="1543" class="PrimitiveType">Set</a> <a id="1547" href="Relation.Binary.EquivalenceClosure.html#1532" class="Bound">b</a><a id="1548" class="Symbol">}</a> <a id="1550" class="Symbol">{</a><a id="1551" href="Relation.Binary.EquivalenceClosure.html#1551" class="Bound">P</a> <a id="1553" class="Symbol">:</a> <a id="1555" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1559" href="Relation.Binary.EquivalenceClosure.html#726" class="Bound">A</a> <a id="1561" href="Relation.Binary.EquivalenceClosure.html#722" class="Bound">ℓ</a><a id="1562" class="Symbol">}</a> <a id="1564" class="Symbol">{</a><a id="1565" href="Relation.Binary.EquivalenceClosure.html#1565" class="Bound">Q</a> <a id="1567" class="Symbol">:</a> <a id="1569" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1573" href="Relation.Binary.EquivalenceClosure.html#1539" class="Bound">B</a> <a id="1575" href="Relation.Binary.EquivalenceClosure.html#1534" class="Bound">ℓ₂</a><a id="1577" class="Symbol">}</a> <a id="1579" class="Symbol">→</a>
<a id="1590" class="Symbol">(</a><a id="1591" href="Relation.Binary.EquivalenceClosure.html#1591" class="Bound">f</a> <a id="1593" class="Symbol">:</a> <a id="1595" href="Relation.Binary.EquivalenceClosure.html#726" class="Bound">A</a> <a id="1597" class="Symbol">→</a> <a id="1599" href="Relation.Binary.EquivalenceClosure.html#1539" class="Bound">B</a><a id="1600" class="Symbol">)</a> <a id="1602" class="Symbol">→</a> <a id="1604" href="Relation.Binary.EquivalenceClosure.html#1551" class="Bound">P</a> <a id="1606" href="Relation.Binary.Core.html#_%3D%5B_%5D%E2%87%92_" class="Function Operator">=[</a> <a id="1609" href="Relation.Binary.EquivalenceClosure.html#1591" class="Bound">f</a> <a id="1611" href="Relation.Binary.Core.html#_%3D%5B_%5D%E2%87%92_" class="Function Operator">]⇒</a> <a id="1614" href="Relation.Binary.EquivalenceClosure.html#1565" class="Bound">Q</a> <a id="1616" class="Symbol">→</a> <a id="1618" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="1628" href="Relation.Binary.EquivalenceClosure.html#1551" class="Bound">P</a> <a id="1630" href="Relation.Binary.Core.html#_%3D%5B_%5D%E2%87%92_" class="Function Operator">=[</a> <a id="1633" href="Relation.Binary.EquivalenceClosure.html#1591" class="Bound">f</a> <a id="1635" href="Relation.Binary.Core.html#_%3D%5B_%5D%E2%87%92_" class="Function Operator">]⇒</a> <a id="1638" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="1648" href="Relation.Binary.EquivalenceClosure.html#1565" class="Bound">Q</a>
<a id="1652" href="Relation.Binary.EquivalenceClosure.html#1522" class="Function">gmap</a> <a id="1657" class="Symbol">{</a><a id="1658" class="Argument">Q</a> <a id="1660" class="Symbol">=</a> <a id="1662" href="Relation.Binary.EquivalenceClosure.html#1662" class="Bound">Q</a><a id="1663" class="Symbol">}</a> <a id="1665" href="Relation.Binary.EquivalenceClosure.html#1665" class="Bound">f</a> <a id="1667" class="Symbol">=</a> <a id="1669" href="Data.Star.html#gmap" class="Function">Star.gmap</a> <a id="1679" href="Relation.Binary.EquivalenceClosure.html#1665" class="Bound">f</a> <a id="1681" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="1683" href="Relation.Binary.SymmetricClosure.html#840" class="Function">SC.gmap</a> <a id="1691" class="Symbol">{</a><a id="1692" class="Argument">Q</a> <a id="1694" class="Symbol">=</a> <a id="1696" href="Relation.Binary.EquivalenceClosure.html#1662" class="Bound">Q</a><a id="1697" class="Symbol">}</a> <a id="1699" href="Relation.Binary.EquivalenceClosure.html#1665" class="Bound">f</a>
<a id="1704" href="Relation.Binary.EquivalenceClosure.html#1704" class="Function">map</a> <a id="1708" class="Symbol">:</a> <a id="1710" class="Symbol">∀</a> <a id="1712" class="Symbol">{</a><a id="1713" href="Relation.Binary.EquivalenceClosure.html#1713" class="Bound">ℓ₂</a><a id="1715" class="Symbol">}</a> <a id="1717" class="Symbol">{</a><a id="1718" href="Relation.Binary.EquivalenceClosure.html#1718" class="Bound">P</a> <a id="1720" class="Symbol">:</a> <a id="1722" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1726" href="Relation.Binary.EquivalenceClosure.html#726" class="Bound">A</a> <a id="1728" href="Relation.Binary.EquivalenceClosure.html#722" class="Bound">ℓ</a><a id="1729" class="Symbol">}</a> <a id="1731" class="Symbol">{</a><a id="1732" href="Relation.Binary.EquivalenceClosure.html#1732" class="Bound">Q</a> <a id="1734" class="Symbol">:</a> <a id="1736" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1740" href="Relation.Binary.EquivalenceClosure.html#726" class="Bound">A</a> <a id="1742" href="Relation.Binary.EquivalenceClosure.html#1713" class="Bound">ℓ₂</a><a id="1744" class="Symbol">}</a> <a id="1746" class="Symbol">→</a>
<a id="1756" href="Relation.Binary.EquivalenceClosure.html#1718" class="Bound">P</a> <a id="1758" href="Relation.Binary.Core.html#_%E2%87%92_" class="Function Operator">⇒</a> <a id="1760" href="Relation.Binary.EquivalenceClosure.html#1732" class="Bound">Q</a> <a id="1762" class="Symbol">→</a> <a id="1764" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="1774" href="Relation.Binary.EquivalenceClosure.html#1718" class="Bound">P</a> <a id="1776" href="Relation.Binary.Core.html#_%E2%87%92_" class="Function Operator">⇒</a> <a id="1778" href="Relation.Binary.EquivalenceClosure.html#EqClosure" class="Function">EqClosure</a> <a id="1788" href="Relation.Binary.EquivalenceClosure.html#1732" class="Bound">Q</a>
<a id="1792" href="Relation.Binary.EquivalenceClosure.html#1704" class="Function">map</a> <a id="1796" class="Symbol">=</a> <a id="1798" href="Relation.Binary.EquivalenceClosure.html#1522" class="Function">gmap</a> <a id="1803" href="Function.html#id" class="Function">id</a>
</pre></body></html>
|