42 lines
13 KiB
HTML
42 lines
13 KiB
HTML
|
<!DOCTYPE HTML>
|
|||
|
|
<html><head><meta charset="utf-8"><title>Relation.Binary.Indexed.Heterogeneous.Core</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.Core.html" class="Module">Relation.Binary.Indexed.Heterogeneous.Core</a> <a id="393" class="Keyword">where</a>
|
|||
|
|
|
|||
|
|
<a id="400" class="Keyword">open</a> <a id="405" class="Keyword">import</a> <a id="412" href="Level.html" class="Module">Level</a>
|
|||
|
|
<a id="418" class="Keyword">import</a> <a id="425" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a> <a id="446" class="Symbol">as</a> <a id="449" class="Module">B</a>
|
|||
|
|
<a id="451" class="Keyword">import</a> <a id="458" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="486" class="Symbol">as</a> <a id="489" class="Module">B</a>
|
|||
|
|
<a id="491" class="Keyword">import</a> <a id="498" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a> <a id="541" class="Symbol">as</a> <a id="544" class="Module">P</a>
|
|||
|
|
|
|||
|
|
<a id="547" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
<a id="620" class="Comment">-- Indexed binary relations</a>
|
|||
|
|
|
|||
|
|
<a id="649" class="Comment">-- Heterogeneous types</a>
|
|||
|
|
|
|||
|
|
<a id="IREL"></a><a id="673" href="Relation.Binary.Indexed.Heterogeneous.Core.html#673" class="Function">IREL</a> <a id="678" class="Symbol">:</a> <a id="680" class="Symbol">∀</a> <a id="682" class="Symbol">{</a><a id="683" href="Relation.Binary.Indexed.Heterogeneous.Core.html#683" class="Bound">i₁</a> <a id="686" href="Relation.Binary.Indexed.Heterogeneous.Core.html#686" class="Bound">i₂</a> <a id="689" href="Relation.Binary.Indexed.Heterogeneous.Core.html#689" class="Bound">a₁</a> <a id="692" href="Relation.Binary.Indexed.Heterogeneous.Core.html#692" class="Bound">a₂</a><a id="694" class="Symbol">}</a> <a id="696" class="Symbol">{</a><a id="697" href="Relation.Binary.Indexed.Heterogeneous.Core.html#697" class="Bound">I₁</a> <a id="700" class="Symbol">:</a> <a id="702" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="706" href="Relation.Binary.Indexed.Heterogeneous.Core.html#683" class="Bound">i₁</a><a id="708" class="Symbol">}</a> <a id="710" class="Symbol">{</a><a id="711" href="Relation.Binary.Indexed.Heterogeneous.Core.html#711" class="Bound">I₂</a> <a id="714" class="Symbol">:</a> <a id="716" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="720" href="Relation.Binary.Indexed.Heterogeneous.Core.html#686" class="Bound">i₂</a><a id="722" class="Symbol">}</a> <a id="724" class="Symbol">→</a>
|
|||
|
|
<a id="732" class="Symbol">(</a><a id="733" href="Relation.Binary.Indexed.Heterogeneous.Core.html#697" class="Bound">I₁</a> <a id="736" class="Symbol">→</a> <a id="738" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="742" href="Relation.Binary.Indexed.Heterogeneous.Core.html#689" class="Bound">a₁</a><a id="744" class="Symbol">)</a> <a id="746" class="Symbol">→</a> <a id="748" class="Symbol">(</a><a id="749" href="Relation.Binary.Indexed.Heterogeneous.Core.html#711" class="Bound">I₂</a> <a id="752" class="Symbol">→</a> <a id="754" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="758" href="Relation.Binary.Indexed.Heterogeneous.Core.html#692" class="Bound">a₂</a><a id="760" class="Symbol">)</a> <a id="762" class="Symbol">→</a> <a id="764" class="Symbol">(</a><a id="765" href="Relation.Binary.Indexed.Heterogeneous.Core.html#765" class="Bound">ℓ</a> <a id="767" class="Symbol">:</a> <a id="769" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="774" class="Symbol">)</a> <a id="776" class="Symbol">→</a> <a id="778" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="782" class="Symbol">_</a>
|
|||
|
|
<a id="784" href="Relation.Binary.Indexed.Heterogeneous.Core.html#673" class="Function">IREL</a> <a id="789" href="Relation.Binary.Indexed.Heterogeneous.Core.html#789" class="Bound">A₁</a> <a id="792" href="Relation.Binary.Indexed.Heterogeneous.Core.html#792" class="Bound">A₂</a> <a id="795" href="Relation.Binary.Indexed.Heterogeneous.Core.html#795" class="Bound">ℓ</a> <a id="797" class="Symbol">=</a> <a id="799" class="Symbol">∀</a> <a id="801" class="Symbol">{</a><a id="802" href="Relation.Binary.Indexed.Heterogeneous.Core.html#802" class="Bound">i₁</a> <a id="805" href="Relation.Binary.Indexed.Heterogeneous.Core.html#805" class="Bound">i₂</a><a id="807" class="Symbol">}</a> <a id="809" class="Symbol">→</a> <a id="811" href="Relation.Binary.Indexed.Heterogeneous.Core.html#789" class="Bound">A₁</a> <a id="814" href="Relation.Binary.Indexed.Heterogeneous.Core.html#802" class="Bound">i₁</a> <a id="817" class="Symbol">→</a> <a id="819" href="Relation.Binary.Indexed.Heterogeneous.Core.html#792" class="Bound">A₂</a> <a id="822" href="Relation.Binary.Indexed.Heterogeneous.Core.html#805" class="Bound">i₂</a> <a id="825" class="Symbol">→</a> <a id="827" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="831" href="Relation.Binary.Indexed.Heterogeneous.Core.html#795" class="Bound">ℓ</a>
|
|||
|
|
|
|||
|
|
<a id="834" class="Comment">-- Homogeneous types</a>
|
|||
|
|
|
|||
|
|
<a id="IRel"></a><a id="856" href="Relation.Binary.Indexed.Heterogeneous.Core.html#856" class="Function">IRel</a> <a id="861" class="Symbol">:</a> <a id="863" class="Symbol">∀</a> <a id="865" class="Symbol">{</a><a id="866" href="Relation.Binary.Indexed.Heterogeneous.Core.html#866" class="Bound">i</a> <a id="868" href="Relation.Binary.Indexed.Heterogeneous.Core.html#868" class="Bound">a</a><a id="869" class="Symbol">}</a> <a id="871" class="Symbol">{</a><a id="872" href="Relation.Binary.Indexed.Heterogeneous.Core.html#872" class="Bound">I</a> <a id="874" class="Symbol">:</a> <a id="876" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="880" href="Relation.Binary.Indexed.Heterogeneous.Core.html#866" class="Bound">i</a><a id="881" class="Symbol">}</a> <a id="883" class="Symbol">→</a> <a id="885" class="Symbol">(</a><a id="886" href="Relation.Binary.Indexed.Heterogeneous.Core.html#872" class="Bound">I</a> <a id="888" class="Symbol">→</a> <a id="890" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="894" href="Relation.Binary.Indexed.Heterogeneous.Core.html#868" class="Bound">a</a><a id="895" class="Symbol">)</a> <a id="897" class="Symbol">→</a> <a id="899" class="Symbol">(</a><a id="900" href="Relation.Binary.Indexed.Heterogeneous.Core.html#900" class="Bound">ℓ</a> <a id="902" class="Symbol">:</a> <a id="904" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="909" class="Symbol">)</a> <a id="911" class="Symbol">→</a> <a id="913" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="917" class="Symbol">_</a>
|
|||
|
|
<a id="919" href="Relation.Binary.Indexed.Heterogeneous.Core.html#856" class="Function">IRel</a> <a id="924" href="Relation.Binary.Indexed.Heterogeneous.Core.html#924" class="Bound">A</a> <a id="926" href="Relation.Binary.Indexed.Heterogeneous.Core.html#926" class="Bound">ℓ</a> <a id="928" class="Symbol">=</a> <a id="930" href="Relation.Binary.Indexed.Heterogeneous.Core.html#673" class="Function">IREL</a> <a id="935" href="Relation.Binary.Indexed.Heterogeneous.Core.html#924" class="Bound">A</a> <a id="937" href="Relation.Binary.Indexed.Heterogeneous.Core.html#924" class="Bound">A</a> <a id="939" href="Relation.Binary.Indexed.Heterogeneous.Core.html#926" class="Bound">ℓ</a>
|
|||
|
|
|
|||
|
|
<a id="942" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
<a id="1015" class="Comment">-- Generalised implication.</a>
|
|||
|
|
|
|||
|
|
<a id="1044" class="Keyword">infixr</a> <a id="1051" class="Number">4</a> <a id="1053" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1062" class="Function Operator">_=[_]⇒_</a>
|
|||
|
|
|
|||
|
|
<a id="_=[_]⇒_"></a><a id="1062" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1062" class="Function Operator">_=[_]⇒_</a> <a id="1070" class="Symbol">:</a> <a id="1072" class="Symbol">∀</a> <a id="1074" class="Symbol">{</a><a id="1075" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1075" class="Bound">a</a> <a id="1077" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1077" class="Bound">b</a> <a id="1079" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1079" class="Bound">ℓ₁</a> <a id="1082" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1082" class="Bound">ℓ₂</a><a id="1084" class="Symbol">}</a> <a id="1086" class="Symbol">{</a><a id="1087" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1087" class="Bound">A</a> <a id="1089" class="Symbol">:</a> <a id="1091" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1095" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1075" class="Bound">a</a><a id="1096" class="Symbol">}</a> <a id="1098" class="Symbol">{</a><a id="1099" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1099" class="Bound">B</a> <a id="1101" class="Symbol">:</a> <a id="1103" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1087" class="Bound">A</a> <a id="1105" class="Symbol">→</a> <a id="1107" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1111" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1077" class="Bound">b</a><a id="1112" class="Symbol">}</a> <a id="1114" class="Symbol">→</a>
|
|||
|
|
<a id="1126" href="Relation.Binary.Core.html#882" class="Function">B.Rel</a> <a id="1132" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1087" class="Bound">A</a> <a id="1134" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1079" class="Bound">ℓ₁</a> <a id="1137" class="Symbol">→</a> <a id="1139" class="Symbol">((</a><a id="1141" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1141" class="Bound">x</a> <a id="1143" class="Symbol">:</a> <a id="1145" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1087" class="Bound">A</a><a id="1146" class="Symbol">)</a> <a id="1148" class="Symbol">→</a> <a id="1150" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1099" class="Bound">B</a> <a id="1152" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1141" class="Bound">x</a><a id="1153" class="Symbol">)</a> <a id="1155" class="Symbol">→</a> <a id="1157" href="Relation.Binary.Indexed.Heterogeneous.Core.html#856" class="Function">IRel</a> <a id="1162" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1099" class="Bound">B</a> <a id="1164" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1082" class="Bound">ℓ₂</a> <a id="1167" class="Symbol">→</a> <a id="1169" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1173" class="Symbol">_</a>
|
|||
|
|
<a id="1175" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1175" class="Bound">P</a> <a id="1177" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1062" class="Function Operator">=[</a> <a id="1180" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1180" class="Bound">f</a> <a id="1182" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1062" class="Function Operator">]⇒</a> <a id="1185" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1185" class="Bound">Q</a> <a id="1187" class="Symbol">=</a> <a id="1189" class="Symbol">∀</a> <a id="1191" class="Symbol">{</a><a id="1192" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1192" class="Bound">i</a> <a id="1194" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1194" class="Bound">j</a><a id="1195" class="Symbol">}</a> <a id="1197" class="Symbol">→</a> <a id="1199" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1175" class="Bound">P</a> <a id="1201" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1192" class="Bound">i</a> <a id="1203" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1194" class="Bound">j</a> <a id="1205" class="Symbol">→</a> <a id="1207" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1185" class="Bound">Q</a> <a id="1209" class="Symbol">(</a><a id="1210" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1180" class="Bound">f</a> <a id="1212" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1192" class="Bound">i</a><a id="1213" class="Symbol">)</a> <a id="1215" class="Symbol">(</a><a id="1216" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1180" class="Bound">f</a> <a id="1218" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1194" class="Bound">j</a><a id="1219" class="Symbol">)</a>
|
|||
|
|
</pre></body></html>
|