37 lines
10 KiB
HTML
37 lines
10 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Binary.Indexed.Heterogeneous.Definitions</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">-- Indexed binary relations</a>
|
||
<a id="134" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="208" class="Comment">-- The contents of this module should be accessed via</a>
|
||
<a id="262" class="Comment">-- `Relation.Binary.Indexed.Heterogeneous`.</a>
|
||
|
||
<a id="307" class="Symbol">{-#</a> <a id="311" class="Keyword">OPTIONS</a> <a id="319" class="Pragma">--without-K</a> <a id="331" class="Pragma">--safe</a> <a id="338" class="Symbol">#-}</a>
|
||
|
||
<a id="343" class="Keyword">module</a> <a id="350" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html" class="Module">Relation.Binary.Indexed.Heterogeneous.Definitions</a> <a id="400" class="Keyword">where</a>
|
||
|
||
<a id="407" class="Keyword">open</a> <a id="412" class="Keyword">import</a> <a id="419" href="Level.html" class="Module">Level</a>
|
||
<a id="425" class="Keyword">import</a> <a id="432" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a> <a id="453" class="Symbol">as</a> <a id="456" class="Module">B</a>
|
||
<a id="458" class="Keyword">import</a> <a id="465" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="493" class="Symbol">as</a> <a id="496" class="Module">B</a>
|
||
<a id="498" class="Keyword">import</a> <a id="505" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a> <a id="548" class="Symbol">as</a> <a id="551" class="Module">P</a>
|
||
<a id="553" class="Keyword">open</a> <a id="558" class="Keyword">import</a> <a id="565" href="Relation.Binary.Indexed.Heterogeneous.Core.html" class="Module">Relation.Binary.Indexed.Heterogeneous.Core</a>
|
||
|
||
<a id="609" class="Keyword">private</a>
|
||
<a id="619" class="Keyword">variable</a>
|
||
<a id="632" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#632" class="Generalizable">i</a> <a id="634" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#634" class="Generalizable">a</a> <a id="636" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#636" class="Generalizable">ℓ</a> <a id="638" class="Symbol">:</a> <a id="640" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="650" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#650" class="Generalizable">I</a> <a id="652" class="Symbol">:</a> <a id="654" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="658" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#632" class="Generalizable">i</a>
|
||
|
||
<a id="661" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="734" class="Comment">-- Simple properties of indexed binary relations</a>
|
||
|
||
<a id="Reflexive"></a><a id="784" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#784" class="Function">Reflexive</a> <a id="794" class="Symbol">:</a> <a id="796" class="Symbol">(</a><a id="797" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#797" class="Bound">A</a> <a id="799" class="Symbol">:</a> <a id="801" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#650" class="Generalizable">I</a> <a id="803" class="Symbol">→</a> <a id="805" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="809" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#634" class="Generalizable">a</a><a id="810" class="Symbol">)</a> <a id="812" class="Symbol">→</a> <a id="814" href="Relation.Binary.Indexed.Heterogeneous.Core.html#856" class="Function">IRel</a> <a id="819" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#797" class="Bound">A</a> <a id="821" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#636" class="Generalizable">ℓ</a> <a id="823" class="Symbol">→</a> <a id="825" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="829" class="Symbol">_</a>
|
||
<a id="831" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#784" class="Function">Reflexive</a> <a id="841" class="Symbol">_</a> <a id="843" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#843" class="Bound Operator">_∼_</a> <a id="847" class="Symbol">=</a> <a id="849" class="Symbol">∀</a> <a id="851" class="Symbol">{</a><a id="852" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#852" class="Bound">i</a><a id="853" class="Symbol">}</a> <a id="855" class="Symbol">→</a> <a id="857" href="Relation.Binary.Definitions.html#1339" class="Function">B.Reflexive</a> <a id="869" class="Symbol">(</a><a id="870" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#843" class="Bound Operator">_∼_</a> <a id="874" class="Symbol">{</a><a id="875" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#852" class="Bound">i</a><a id="876" class="Symbol">})</a>
|
||
|
||
<a id="Symmetric"></a><a id="880" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#880" class="Function">Symmetric</a> <a id="890" class="Symbol">:</a> <a id="892" class="Symbol">(</a><a id="893" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#893" class="Bound">A</a> <a id="895" class="Symbol">:</a> <a id="897" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#650" class="Generalizable">I</a> <a id="899" class="Symbol">→</a> <a id="901" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="905" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#634" class="Generalizable">a</a><a id="906" class="Symbol">)</a> <a id="908" class="Symbol">→</a> <a id="910" href="Relation.Binary.Indexed.Heterogeneous.Core.html#856" class="Function">IRel</a> <a id="915" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#893" class="Bound">A</a> <a id="917" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#636" class="Generalizable">ℓ</a> <a id="919" class="Symbol">→</a> <a id="921" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="925" class="Symbol">_</a>
|
||
<a id="927" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#880" class="Function">Symmetric</a> <a id="937" class="Symbol">_</a> <a id="939" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#939" class="Bound Operator">_∼_</a> <a id="943" class="Symbol">=</a> <a id="945" class="Symbol">∀</a> <a id="947" class="Symbol">{</a><a id="948" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#948" class="Bound">i</a> <a id="950" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#950" class="Bound">j</a><a id="951" class="Symbol">}</a> <a id="953" class="Symbol">→</a> <a id="955" href="Relation.Binary.Definitions.html#1424" class="Function">B.Sym</a> <a id="961" class="Symbol">(</a><a id="962" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#939" class="Bound Operator">_∼_</a> <a id="966" class="Symbol">{</a><a id="967" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#948" class="Bound">i</a><a id="968" class="Symbol">}</a> <a id="970" class="Symbol">{</a><a id="971" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#950" class="Bound">j</a><a id="972" class="Symbol">})</a> <a id="975" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#939" class="Bound Operator">_∼_</a>
|
||
|
||
<a id="Transitive"></a><a id="980" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#980" class="Function">Transitive</a> <a id="991" class="Symbol">:</a> <a id="993" class="Symbol">(</a><a id="994" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#994" class="Bound">A</a> <a id="996" class="Symbol">:</a> <a id="998" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#650" class="Generalizable">I</a> <a id="1000" class="Symbol">→</a> <a id="1002" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1006" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#634" class="Generalizable">a</a><a id="1007" class="Symbol">)</a> <a id="1009" class="Symbol">→</a> <a id="1011" href="Relation.Binary.Indexed.Heterogeneous.Core.html#856" class="Function">IRel</a> <a id="1016" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#994" class="Bound">A</a> <a id="1018" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#636" class="Generalizable">ℓ</a> <a id="1020" class="Symbol">→</a> <a id="1022" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1026" class="Symbol">_</a>
|
||
<a id="1028" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#980" class="Function">Transitive</a> <a id="1039" class="Symbol">_</a> <a id="1041" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#1041" class="Bound Operator">_∼_</a> <a id="1045" class="Symbol">=</a> <a id="1047" class="Symbol">∀</a> <a id="1049" class="Symbol">{</a><a id="1050" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#1050" class="Bound">i</a> <a id="1052" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#1052" class="Bound">j</a> <a id="1054" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#1054" class="Bound">k</a><a id="1055" class="Symbol">}</a> <a id="1057" class="Symbol">→</a> <a id="1059" href="Relation.Binary.Definitions.html#1585" class="Function">B.Trans</a> <a id="1067" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#1041" class="Bound Operator">_∼_</a> <a id="1071" class="Symbol">(</a><a id="1072" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#1041" class="Bound Operator">_∼_</a> <a id="1076" class="Symbol">{</a><a id="1077" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#1052" class="Bound">j</a><a id="1078" class="Symbol">})</a> <a id="1081" class="Symbol">(</a><a id="1082" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#1041" class="Bound Operator">_∼_</a> <a id="1086" class="Symbol">{</a><a id="1087" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#1050" class="Bound">i</a><a id="1088" class="Symbol">}</a> <a id="1090" class="Symbol">{</a><a id="1091" href="Relation.Binary.Indexed.Heterogeneous.Definitions.html#1054" class="Bound">k</a><a id="1092" class="Symbol">})</a>
|
||
</pre></body></html> |