60 lines
16 KiB
HTML
60 lines
16 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Binary.Indexed.Heterogeneous.Construct.Trivial</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">-- Creates trivially indexed records from their non-indexed counterpart.</a>
|
||
<a id="179" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="253" class="Symbol">{-#</a> <a id="257" class="Keyword">OPTIONS</a> <a id="265" class="Pragma">--without-K</a> <a id="277" class="Pragma">--safe</a> <a id="284" class="Symbol">#-}</a>
|
||
|
||
<a id="289" class="Keyword">module</a> <a id="296" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html" class="Module">Relation.Binary.Indexed.Heterogeneous.Construct.Trivial</a>
|
||
<a id="354" class="Symbol">{</a><a id="355" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#355" class="Bound">i</a><a id="356" class="Symbol">}</a> <a id="358" class="Symbol">{</a><a id="359" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#359" class="Bound">I</a> <a id="361" class="Symbol">:</a> <a id="363" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="367" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#355" class="Bound">i</a><a id="368" class="Symbol">}</a> <a id="370" class="Keyword">where</a>
|
||
|
||
<a id="377" class="Keyword">open</a> <a id="382" class="Keyword">import</a> <a id="389" href="Relation.Binary.html" class="Module">Relation.Binary</a>
|
||
<a id="405" class="Keyword">open</a> <a id="410" class="Keyword">import</a> <a id="417" href="Relation.Binary.Indexed.Heterogeneous.html" class="Module">Relation.Binary.Indexed.Heterogeneous</a> <a id="455" class="Keyword">hiding</a> <a id="462" class="Symbol">(</a><a id="463" href="Relation.Binary.Indexed.Heterogeneous.html#1067" class="Function">Rel</a><a id="466" class="Symbol">)</a>
|
||
<a id="470" class="Keyword">hiding</a> <a id="477" class="Symbol">(</a><a id="478" href="Relation.Binary.Indexed.Heterogeneous.html#1304" class="Function">IsEquivalence</a><a id="491" class="Symbol">;</a> <a id="493" href="Relation.Binary.Indexed.Heterogeneous.html#1172" class="Function">Setoid</a><a id="499" class="Symbol">)</a>
|
||
|
||
<a id="502" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="575" class="Comment">-- Structures</a>
|
||
|
||
<a id="590" class="Keyword">module</a> <a id="597" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#597" class="Module">_</a> <a id="599" class="Symbol">{</a><a id="600" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#600" class="Bound">a</a><a id="601" class="Symbol">}</a> <a id="603" class="Symbol">{</a><a id="604" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#604" class="Bound">A</a> <a id="606" class="Symbol">:</a> <a id="608" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="612" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#600" class="Bound">a</a><a id="613" class="Symbol">}</a> <a id="615" class="Keyword">where</a>
|
||
|
||
<a id="624" class="Keyword">private</a>
|
||
<a id="636" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#636" class="Function">Aᵢ</a> <a id="639" class="Symbol">:</a> <a id="641" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#359" class="Bound">I</a> <a id="643" class="Symbol">→</a> <a id="645" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="649" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#600" class="Bound">a</a>
|
||
<a id="655" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#636" class="Function">Aᵢ</a> <a id="658" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#658" class="Bound">i</a> <a id="660" class="Symbol">=</a> <a id="662" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#604" class="Bound">A</a>
|
||
|
||
<a id="667" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#667" class="Function">isIndexedEquivalence</a> <a id="688" class="Symbol">:</a> <a id="690" class="Symbol">∀</a> <a id="692" class="Symbol">{</a><a id="693" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#693" class="Bound">ℓ</a><a id="694" class="Symbol">}</a> <a id="696" class="Symbol">{</a><a id="697" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#697" class="Bound Operator">_≈_</a> <a id="701" class="Symbol">:</a> <a id="703" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="707" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#604" class="Bound">A</a> <a id="709" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#693" class="Bound">ℓ</a><a id="710" class="Symbol">}</a> <a id="712" class="Symbol">→</a> <a id="714" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a> <a id="728" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#697" class="Bound Operator">_≈_</a> <a id="732" class="Symbol">→</a>
|
||
<a id="759" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#852" class="Record">IsIndexedEquivalence</a> <a id="780" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#636" class="Function">Aᵢ</a> <a id="783" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#697" class="Bound Operator">_≈_</a>
|
||
<a id="789" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#667" class="Function">isIndexedEquivalence</a> <a id="810" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#810" class="Bound">isEq</a> <a id="815" class="Symbol">=</a> <a id="817" class="Keyword">record</a>
|
||
<a id="828" class="Symbol">{</a> <a id="830" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#909" class="Field">refl</a> <a id="836" class="Symbol">=</a> <a id="838" href="Relation.Binary.Structures.html#1568" class="Field">refl</a>
|
||
<a id="847" class="Symbol">;</a> <a id="849" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#938" class="Field">sym</a> <a id="855" class="Symbol">=</a> <a id="857" href="Relation.Binary.Structures.html#1594" class="Field">sym</a>
|
||
<a id="865" class="Symbol">;</a> <a id="867" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#967" class="Field">trans</a> <a id="873" class="Symbol">=</a> <a id="875" href="Relation.Binary.Structures.html#1620" class="Field">trans</a>
|
||
<a id="885" class="Symbol">}</a>
|
||
<a id="891" class="Keyword">where</a> <a id="897" class="Keyword">open</a> <a id="902" href="Relation.Binary.Structures.html#1522" class="Module">IsEquivalence</a> <a id="916" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#810" class="Bound">isEq</a>
|
||
|
||
<a id="924" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#924" class="Function">isIndexedPreorder</a> <a id="942" class="Symbol">:</a> <a id="944" class="Symbol">∀</a> <a id="946" class="Symbol">{</a><a id="947" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#947" class="Bound">ℓ₁</a> <a id="950" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#950" class="Bound">ℓ₂</a><a id="952" class="Symbol">}</a> <a id="954" class="Symbol">{</a><a id="955" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#955" class="Bound Operator">_≈_</a> <a id="959" class="Symbol">:</a> <a id="961" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="965" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#604" class="Bound">A</a> <a id="967" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#947" class="Bound">ℓ₁</a><a id="969" class="Symbol">}</a> <a id="971" class="Symbol">{</a><a id="972" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#972" class="Bound Operator">_∼_</a> <a id="976" class="Symbol">:</a> <a id="978" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="982" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#604" class="Bound">A</a> <a id="984" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#950" class="Bound">ℓ₂</a><a id="986" class="Symbol">}</a> <a id="988" class="Symbol">→</a>
|
||
<a id="1012" href="Relation.Binary.Structures.html#2163" class="Record">IsPreorder</a> <a id="1023" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#955" class="Bound Operator">_≈_</a> <a id="1027" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#972" class="Bound Operator">_∼_</a> <a id="1031" class="Symbol">→</a>
|
||
<a id="1055" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#1070" class="Record">IsIndexedPreorder</a> <a id="1073" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#636" class="Function">Aᵢ</a> <a id="1076" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#955" class="Bound Operator">_≈_</a> <a id="1080" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#972" class="Bound Operator">_∼_</a>
|
||
<a id="1086" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#924" class="Function">isIndexedPreorder</a> <a id="1104" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1104" class="Bound">isPreorder</a> <a id="1115" class="Symbol">=</a> <a id="1117" class="Keyword">record</a>
|
||
<a id="1128" class="Symbol">{</a> <a id="1130" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#1152" class="Field">isEquivalence</a> <a id="1144" class="Symbol">=</a> <a id="1146" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#667" class="Function">isIndexedEquivalence</a> <a id="1167" href="Relation.Binary.Structures.html#2228" class="Field">isEquivalence</a>
|
||
<a id="1185" class="Symbol">;</a> <a id="1187" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#1193" class="Field">reflexive</a> <a id="1201" class="Symbol">=</a> <a id="1203" href="Relation.Binary.Structures.html#2331" class="Field">reflexive</a>
|
||
<a id="1217" class="Symbol">;</a> <a id="1219" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#1249" class="Field">trans</a> <a id="1233" class="Symbol">=</a> <a id="1235" href="Relation.Binary.Structures.html#2361" class="Field">trans</a>
|
||
<a id="1245" class="Symbol">}</a>
|
||
<a id="1251" class="Keyword">where</a> <a id="1257" class="Keyword">open</a> <a id="1262" href="Relation.Binary.Structures.html#2163" class="Module">IsPreorder</a> <a id="1273" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1104" class="Bound">isPreorder</a>
|
||
|
||
<a id="1285" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1358" class="Comment">-- Bundles</a>
|
||
|
||
<a id="indexedSetoid"></a><a id="1370" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1370" class="Function">indexedSetoid</a> <a id="1384" class="Symbol">:</a> <a id="1386" class="Symbol">∀</a> <a id="1388" class="Symbol">{</a><a id="1389" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1389" class="Bound">a</a> <a id="1391" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1391" class="Bound">ℓ</a><a id="1392" class="Symbol">}</a> <a id="1394" class="Symbol">→</a> <a id="1396" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1403" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1389" class="Bound">a</a> <a id="1405" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1391" class="Bound">ℓ</a> <a id="1407" class="Symbol">→</a> <a id="1409" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#789" class="Record">IndexedSetoid</a> <a id="1423" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#359" class="Bound">I</a> <a id="1425" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1389" class="Bound">a</a> <a id="1427" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1391" class="Bound">ℓ</a>
|
||
<a id="1429" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1370" class="Function">indexedSetoid</a> <a id="1443" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1443" class="Bound">S</a> <a id="1445" class="Symbol">=</a> <a id="1447" class="Keyword">record</a>
|
||
<a id="1456" class="Symbol">{</a> <a id="1458" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#944" class="Field">isEquivalence</a> <a id="1472" class="Symbol">=</a> <a id="1474" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#667" class="Function">isIndexedEquivalence</a> <a id="1495" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a>
|
||
<a id="1511" class="Symbol">}</a>
|
||
<a id="1515" class="Keyword">where</a> <a id="1521" class="Keyword">open</a> <a id="1526" href="Relation.Binary.Bundles.html#1009" class="Module">Setoid</a> <a id="1533" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1443" class="Bound">S</a>
|
||
|
||
<a id="indexedPreorder"></a><a id="1536" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1536" class="Function">indexedPreorder</a> <a id="1552" class="Symbol">:</a> <a id="1554" class="Symbol">∀</a> <a id="1556" class="Symbol">{</a><a id="1557" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1557" class="Bound">a</a> <a id="1559" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1559" class="Bound">ℓ₁</a> <a id="1562" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1562" class="Bound">ℓ₂</a><a id="1564" class="Symbol">}</a> <a id="1566" class="Symbol">→</a> <a id="1568" href="Relation.Binary.Bundles.html#1920" class="Record">Preorder</a> <a id="1577" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1557" class="Bound">a</a> <a id="1579" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1559" class="Bound">ℓ₁</a> <a id="1582" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1562" class="Bound">ℓ₂</a> <a id="1585" class="Symbol">→</a>
|
||
<a id="1605" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#1052" class="Record">IndexedPreorder</a> <a id="1621" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#359" class="Bound">I</a> <a id="1623" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1557" class="Bound">a</a> <a id="1625" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1559" class="Bound">ℓ₁</a> <a id="1628" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1562" class="Bound">ℓ₂</a>
|
||
<a id="1631" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1536" class="Function">indexedPreorder</a> <a id="1647" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1647" class="Bound">O</a> <a id="1649" class="Symbol">=</a> <a id="1651" class="Keyword">record</a>
|
||
<a id="1660" class="Symbol">{</a> <a id="1662" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#1321" class="Field">isPreorder</a> <a id="1673" class="Symbol">=</a> <a id="1675" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#924" class="Function">isIndexedPreorder</a> <a id="1693" href="Relation.Binary.Bundles.html#2133" class="Field">isPreorder</a>
|
||
<a id="1706" class="Symbol">}</a>
|
||
<a id="1710" class="Keyword">where</a> <a id="1716" class="Keyword">open</a> <a id="1721" href="Relation.Binary.Bundles.html#1920" class="Module">Preorder</a> <a id="1730" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1647" class="Bound">O</a>
|
||
</pre></body></html> |