146 lines
69 KiB
HTML
146 lines
69 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Binary.PropositionalEquality.Properties</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">-- Propositional equality</a>
|
||
<a id="132" class="Comment">--</a>
|
||
<a id="135" class="Comment">-- This file contains some core properies of propositional equality which</a>
|
||
<a id="209" class="Comment">-- are re-exported by Relation.Binary.PropositionalEquality. They are</a>
|
||
<a id="279" class="Comment">-- ``equality rearrangement'' lemmas.</a>
|
||
<a id="317" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="391" class="Symbol">{-#</a> <a id="395" class="Keyword">OPTIONS</a> <a id="403" class="Pragma">--without-K</a> <a id="415" class="Pragma">--safe</a> <a id="422" class="Symbol">#-}</a>
|
||
|
||
<a id="427" class="Keyword">module</a> <a id="434" href="Relation.Binary.PropositionalEquality.Properties.html" class="Module">Relation.Binary.PropositionalEquality.Properties</a> <a id="483" class="Keyword">where</a>
|
||
|
||
<a id="490" class="Keyword">open</a> <a id="495" class="Keyword">import</a> <a id="502" href="Function.Base.html" class="Module">Function.Base</a> <a id="516" class="Keyword">using</a> <a id="522" class="Symbol">(</a><a id="523" href="Function.Base.html#615" class="Function">id</a><a id="525" class="Symbol">;</a> <a id="527" href="Function.Base.html#1031" class="Function Operator">_∘_</a><a id="530" class="Symbol">)</a>
|
||
<a id="532" class="Keyword">open</a> <a id="537" class="Keyword">import</a> <a id="544" href="Level.html" class="Module">Level</a>
|
||
<a id="550" class="Keyword">open</a> <a id="555" class="Keyword">import</a> <a id="562" href="Relation.Binary.html" class="Module">Relation.Binary</a>
|
||
<a id="578" class="Keyword">open</a> <a id="583" class="Keyword">import</a> <a id="590" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a>
|
||
<a id="633" class="Keyword">open</a> <a id="638" class="Keyword">import</a> <a id="645" href="Relation.Unary.html" class="Module">Relation.Unary</a> <a id="660" class="Keyword">using</a> <a id="666" class="Symbol">(</a><a id="667" href="Relation.Unary.html#1101" class="Function">Pred</a><a id="671" class="Symbol">)</a>
|
||
|
||
<a id="674" class="Keyword">private</a>
|
||
<a id="684" class="Keyword">variable</a>
|
||
<a id="697" href="Relation.Binary.PropositionalEquality.Properties.html#697" class="Generalizable">a</a> <a id="699" href="Relation.Binary.PropositionalEquality.Properties.html#699" class="Generalizable">p</a> <a id="701" class="Symbol">:</a> <a id="703" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="713" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a> <a id="715" href="Relation.Binary.PropositionalEquality.Properties.html#715" class="Generalizable">B</a> <a id="717" href="Relation.Binary.PropositionalEquality.Properties.html#717" class="Generalizable">C</a> <a id="719" class="Symbol">:</a> <a id="721" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="725" href="Relation.Binary.PropositionalEquality.Properties.html#697" class="Generalizable">a</a>
|
||
|
||
<a id="728" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="801" class="Comment">-- Various equality rearrangement lemmas</a>
|
||
|
||
<a id="trans-reflʳ"></a><a id="843" href="Relation.Binary.PropositionalEquality.Properties.html#843" class="Function">trans-reflʳ</a> <a id="855" class="Symbol">:</a> <a id="857" class="Symbol">∀</a> <a id="859" class="Symbol">{</a><a id="860" href="Relation.Binary.PropositionalEquality.Properties.html#860" class="Bound">x</a> <a id="862" href="Relation.Binary.PropositionalEquality.Properties.html#862" class="Bound">y</a> <a id="864" class="Symbol">:</a> <a id="866" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="867" class="Symbol">}</a> <a id="869" class="Symbol">(</a><a id="870" href="Relation.Binary.PropositionalEquality.Properties.html#870" class="Bound">p</a> <a id="872" class="Symbol">:</a> <a id="874" href="Relation.Binary.PropositionalEquality.Properties.html#860" class="Bound">x</a> <a id="876" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="878" href="Relation.Binary.PropositionalEquality.Properties.html#862" class="Bound">y</a><a id="879" class="Symbol">)</a> <a id="881" class="Symbol">→</a> <a id="883" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="889" href="Relation.Binary.PropositionalEquality.Properties.html#870" class="Bound">p</a> <a id="891" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="896" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="898" href="Relation.Binary.PropositionalEquality.Properties.html#870" class="Bound">p</a>
|
||
<a id="900" href="Relation.Binary.PropositionalEquality.Properties.html#843" class="Function">trans-reflʳ</a> <a id="912" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="917" class="Symbol">=</a> <a id="919" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="trans-assoc"></a><a id="925" href="Relation.Binary.PropositionalEquality.Properties.html#925" class="Function">trans-assoc</a> <a id="937" class="Symbol">:</a> <a id="939" class="Symbol">∀</a> <a id="941" class="Symbol">{</a><a id="942" href="Relation.Binary.PropositionalEquality.Properties.html#942" class="Bound">x</a> <a id="944" href="Relation.Binary.PropositionalEquality.Properties.html#944" class="Bound">y</a> <a id="946" href="Relation.Binary.PropositionalEquality.Properties.html#946" class="Bound">z</a> <a id="948" href="Relation.Binary.PropositionalEquality.Properties.html#948" class="Bound">u</a> <a id="950" class="Symbol">:</a> <a id="952" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="953" class="Symbol">}</a> <a id="955" class="Symbol">(</a><a id="956" href="Relation.Binary.PropositionalEquality.Properties.html#956" class="Bound">p</a> <a id="958" class="Symbol">:</a> <a id="960" href="Relation.Binary.PropositionalEquality.Properties.html#942" class="Bound">x</a> <a id="962" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="964" href="Relation.Binary.PropositionalEquality.Properties.html#944" class="Bound">y</a><a id="965" class="Symbol">)</a> <a id="967" class="Symbol">{</a><a id="968" href="Relation.Binary.PropositionalEquality.Properties.html#968" class="Bound">q</a> <a id="970" class="Symbol">:</a> <a id="972" href="Relation.Binary.PropositionalEquality.Properties.html#944" class="Bound">y</a> <a id="974" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="976" href="Relation.Binary.PropositionalEquality.Properties.html#946" class="Bound">z</a><a id="977" class="Symbol">}</a> <a id="979" class="Symbol">{</a><a id="980" href="Relation.Binary.PropositionalEquality.Properties.html#980" class="Bound">r</a> <a id="982" class="Symbol">:</a> <a id="984" href="Relation.Binary.PropositionalEquality.Properties.html#946" class="Bound">z</a> <a id="986" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="988" href="Relation.Binary.PropositionalEquality.Properties.html#948" class="Bound">u</a><a id="989" class="Symbol">}</a> <a id="991" class="Symbol">→</a>
|
||
<a id="995" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1001" class="Symbol">(</a><a id="1002" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1008" href="Relation.Binary.PropositionalEquality.Properties.html#956" class="Bound">p</a> <a id="1010" href="Relation.Binary.PropositionalEquality.Properties.html#968" class="Bound">q</a><a id="1011" class="Symbol">)</a> <a id="1013" href="Relation.Binary.PropositionalEquality.Properties.html#980" class="Bound">r</a> <a id="1015" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1017" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1023" href="Relation.Binary.PropositionalEquality.Properties.html#956" class="Bound">p</a> <a id="1025" class="Symbol">(</a><a id="1026" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1032" href="Relation.Binary.PropositionalEquality.Properties.html#968" class="Bound">q</a> <a id="1034" href="Relation.Binary.PropositionalEquality.Properties.html#980" class="Bound">r</a><a id="1035" class="Symbol">)</a>
|
||
<a id="1037" href="Relation.Binary.PropositionalEquality.Properties.html#925" class="Function">trans-assoc</a> <a id="1049" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1054" class="Symbol">=</a> <a id="1056" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="trans-symˡ"></a><a id="1062" href="Relation.Binary.PropositionalEquality.Properties.html#1062" class="Function">trans-symˡ</a> <a id="1073" class="Symbol">:</a> <a id="1075" class="Symbol">∀</a> <a id="1077" class="Symbol">{</a><a id="1078" href="Relation.Binary.PropositionalEquality.Properties.html#1078" class="Bound">x</a> <a id="1080" href="Relation.Binary.PropositionalEquality.Properties.html#1080" class="Bound">y</a> <a id="1082" class="Symbol">:</a> <a id="1084" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="1085" class="Symbol">}</a> <a id="1087" class="Symbol">(</a><a id="1088" href="Relation.Binary.PropositionalEquality.Properties.html#1088" class="Bound">p</a> <a id="1090" class="Symbol">:</a> <a id="1092" href="Relation.Binary.PropositionalEquality.Properties.html#1078" class="Bound">x</a> <a id="1094" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1096" href="Relation.Binary.PropositionalEquality.Properties.html#1080" class="Bound">y</a><a id="1097" class="Symbol">)</a> <a id="1099" class="Symbol">→</a> <a id="1101" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1107" class="Symbol">(</a><a id="1108" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="1112" href="Relation.Binary.PropositionalEquality.Properties.html#1088" class="Bound">p</a><a id="1113" class="Symbol">)</a> <a id="1115" href="Relation.Binary.PropositionalEquality.Properties.html#1088" class="Bound">p</a> <a id="1117" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1119" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
<a id="1124" href="Relation.Binary.PropositionalEquality.Properties.html#1062" class="Function">trans-symˡ</a> <a id="1135" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1140" class="Symbol">=</a> <a id="1142" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="trans-symʳ"></a><a id="1148" href="Relation.Binary.PropositionalEquality.Properties.html#1148" class="Function">trans-symʳ</a> <a id="1159" class="Symbol">:</a> <a id="1161" class="Symbol">∀</a> <a id="1163" class="Symbol">{</a><a id="1164" href="Relation.Binary.PropositionalEquality.Properties.html#1164" class="Bound">x</a> <a id="1166" href="Relation.Binary.PropositionalEquality.Properties.html#1166" class="Bound">y</a> <a id="1168" class="Symbol">:</a> <a id="1170" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="1171" class="Symbol">}</a> <a id="1173" class="Symbol">(</a><a id="1174" href="Relation.Binary.PropositionalEquality.Properties.html#1174" class="Bound">p</a> <a id="1176" class="Symbol">:</a> <a id="1178" href="Relation.Binary.PropositionalEquality.Properties.html#1164" class="Bound">x</a> <a id="1180" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1182" href="Relation.Binary.PropositionalEquality.Properties.html#1166" class="Bound">y</a><a id="1183" class="Symbol">)</a> <a id="1185" class="Symbol">→</a> <a id="1187" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1193" href="Relation.Binary.PropositionalEquality.Properties.html#1174" class="Bound">p</a> <a id="1195" class="Symbol">(</a><a id="1196" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="1200" href="Relation.Binary.PropositionalEquality.Properties.html#1174" class="Bound">p</a><a id="1201" class="Symbol">)</a> <a id="1203" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1205" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
<a id="1210" href="Relation.Binary.PropositionalEquality.Properties.html#1148" class="Function">trans-symʳ</a> <a id="1221" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1226" class="Symbol">=</a> <a id="1228" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="trans-injectiveˡ"></a><a id="1234" href="Relation.Binary.PropositionalEquality.Properties.html#1234" class="Function">trans-injectiveˡ</a> <a id="1251" class="Symbol">:</a> <a id="1253" class="Symbol">∀</a> <a id="1255" class="Symbol">{</a><a id="1256" href="Relation.Binary.PropositionalEquality.Properties.html#1256" class="Bound">x</a> <a id="1258" href="Relation.Binary.PropositionalEquality.Properties.html#1258" class="Bound">y</a> <a id="1260" href="Relation.Binary.PropositionalEquality.Properties.html#1260" class="Bound">z</a> <a id="1262" class="Symbol">:</a> <a id="1264" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="1265" class="Symbol">}</a> <a id="1267" class="Symbol">{</a><a id="1268" href="Relation.Binary.PropositionalEquality.Properties.html#1268" class="Bound">p₁</a> <a id="1271" href="Relation.Binary.PropositionalEquality.Properties.html#1271" class="Bound">p₂</a> <a id="1274" class="Symbol">:</a> <a id="1276" href="Relation.Binary.PropositionalEquality.Properties.html#1256" class="Bound">x</a> <a id="1278" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1280" href="Relation.Binary.PropositionalEquality.Properties.html#1258" class="Bound">y</a><a id="1281" class="Symbol">}</a> <a id="1283" class="Symbol">(</a><a id="1284" href="Relation.Binary.PropositionalEquality.Properties.html#1284" class="Bound">q</a> <a id="1286" class="Symbol">:</a> <a id="1288" href="Relation.Binary.PropositionalEquality.Properties.html#1258" class="Bound">y</a> <a id="1290" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1292" href="Relation.Binary.PropositionalEquality.Properties.html#1260" class="Bound">z</a><a id="1293" class="Symbol">)</a> <a id="1295" class="Symbol">→</a>
|
||
<a id="1316" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1322" href="Relation.Binary.PropositionalEquality.Properties.html#1268" class="Bound">p₁</a> <a id="1325" href="Relation.Binary.PropositionalEquality.Properties.html#1284" class="Bound">q</a> <a id="1327" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1329" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1335" href="Relation.Binary.PropositionalEquality.Properties.html#1271" class="Bound">p₂</a> <a id="1338" href="Relation.Binary.PropositionalEquality.Properties.html#1284" class="Bound">q</a> <a id="1340" class="Symbol">→</a> <a id="1342" href="Relation.Binary.PropositionalEquality.Properties.html#1268" class="Bound">p₁</a> <a id="1345" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1347" href="Relation.Binary.PropositionalEquality.Properties.html#1271" class="Bound">p₂</a>
|
||
<a id="1350" href="Relation.Binary.PropositionalEquality.Properties.html#1234" class="Function">trans-injectiveˡ</a> <a id="1367" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1372" class="Symbol">=</a> <a id="1374" href="Relation.Binary.PropositionalEquality.Core.html#1835" class="Function">subst₂</a> <a id="1381" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="1385" class="Symbol">(</a><a id="1386" href="Relation.Binary.PropositionalEquality.Properties.html#843" class="Function">trans-reflʳ</a> <a id="1398" class="Symbol">_)</a> <a id="1401" class="Symbol">(</a><a id="1402" href="Relation.Binary.PropositionalEquality.Properties.html#843" class="Function">trans-reflʳ</a> <a id="1414" class="Symbol">_)</a>
|
||
|
||
<a id="trans-injectiveʳ"></a><a id="1418" href="Relation.Binary.PropositionalEquality.Properties.html#1418" class="Function">trans-injectiveʳ</a> <a id="1435" class="Symbol">:</a> <a id="1437" class="Symbol">∀</a> <a id="1439" class="Symbol">{</a><a id="1440" href="Relation.Binary.PropositionalEquality.Properties.html#1440" class="Bound">x</a> <a id="1442" href="Relation.Binary.PropositionalEquality.Properties.html#1442" class="Bound">y</a> <a id="1444" href="Relation.Binary.PropositionalEquality.Properties.html#1444" class="Bound">z</a> <a id="1446" class="Symbol">:</a> <a id="1448" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="1449" class="Symbol">}</a> <a id="1451" class="Symbol">(</a><a id="1452" href="Relation.Binary.PropositionalEquality.Properties.html#1452" class="Bound">p</a> <a id="1454" class="Symbol">:</a> <a id="1456" href="Relation.Binary.PropositionalEquality.Properties.html#1440" class="Bound">x</a> <a id="1458" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1460" href="Relation.Binary.PropositionalEquality.Properties.html#1442" class="Bound">y</a><a id="1461" class="Symbol">)</a> <a id="1463" class="Symbol">{</a><a id="1464" href="Relation.Binary.PropositionalEquality.Properties.html#1464" class="Bound">q₁</a> <a id="1467" href="Relation.Binary.PropositionalEquality.Properties.html#1467" class="Bound">q₂</a> <a id="1470" class="Symbol">:</a> <a id="1472" href="Relation.Binary.PropositionalEquality.Properties.html#1442" class="Bound">y</a> <a id="1474" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1476" href="Relation.Binary.PropositionalEquality.Properties.html#1444" class="Bound">z</a><a id="1477" class="Symbol">}</a> <a id="1479" class="Symbol">→</a>
|
||
<a id="1500" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1506" href="Relation.Binary.PropositionalEquality.Properties.html#1452" class="Bound">p</a> <a id="1508" href="Relation.Binary.PropositionalEquality.Properties.html#1464" class="Bound">q₁</a> <a id="1511" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1513" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1519" href="Relation.Binary.PropositionalEquality.Properties.html#1452" class="Bound">p</a> <a id="1521" href="Relation.Binary.PropositionalEquality.Properties.html#1467" class="Bound">q₂</a> <a id="1524" class="Symbol">→</a> <a id="1526" href="Relation.Binary.PropositionalEquality.Properties.html#1464" class="Bound">q₁</a> <a id="1529" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1531" href="Relation.Binary.PropositionalEquality.Properties.html#1467" class="Bound">q₂</a>
|
||
<a id="1534" href="Relation.Binary.PropositionalEquality.Properties.html#1418" class="Function">trans-injectiveʳ</a> <a id="1551" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1556" href="Relation.Binary.PropositionalEquality.Properties.html#1556" class="Bound">eq</a> <a id="1559" class="Symbol">=</a> <a id="1561" href="Relation.Binary.PropositionalEquality.Properties.html#1556" class="Bound">eq</a>
|
||
|
||
<a id="cong-id"></a><a id="1565" href="Relation.Binary.PropositionalEquality.Properties.html#1565" class="Function">cong-id</a> <a id="1573" class="Symbol">:</a> <a id="1575" class="Symbol">∀</a> <a id="1577" class="Symbol">{</a><a id="1578" href="Relation.Binary.PropositionalEquality.Properties.html#1578" class="Bound">x</a> <a id="1580" href="Relation.Binary.PropositionalEquality.Properties.html#1580" class="Bound">y</a> <a id="1582" class="Symbol">:</a> <a id="1584" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="1585" class="Symbol">}</a> <a id="1587" class="Symbol">(</a><a id="1588" href="Relation.Binary.PropositionalEquality.Properties.html#1588" class="Bound">p</a> <a id="1590" class="Symbol">:</a> <a id="1592" href="Relation.Binary.PropositionalEquality.Properties.html#1578" class="Bound">x</a> <a id="1594" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1596" href="Relation.Binary.PropositionalEquality.Properties.html#1580" class="Bound">y</a><a id="1597" class="Symbol">)</a> <a id="1599" class="Symbol">→</a> <a id="1601" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1606" href="Function.Base.html#615" class="Function">id</a> <a id="1609" href="Relation.Binary.PropositionalEquality.Properties.html#1588" class="Bound">p</a> <a id="1611" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1613" href="Relation.Binary.PropositionalEquality.Properties.html#1588" class="Bound">p</a>
|
||
<a id="1615" href="Relation.Binary.PropositionalEquality.Properties.html#1565" class="Function">cong-id</a> <a id="1623" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1628" class="Symbol">=</a> <a id="1630" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="cong-∘"></a><a id="1636" href="Relation.Binary.PropositionalEquality.Properties.html#1636" class="Function">cong-∘</a> <a id="1643" class="Symbol">:</a> <a id="1645" class="Symbol">∀</a> <a id="1647" class="Symbol">{</a><a id="1648" href="Relation.Binary.PropositionalEquality.Properties.html#1648" class="Bound">x</a> <a id="1650" href="Relation.Binary.PropositionalEquality.Properties.html#1650" class="Bound">y</a> <a id="1652" class="Symbol">:</a> <a id="1654" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="1655" class="Symbol">}</a> <a id="1657" class="Symbol">{</a><a id="1658" href="Relation.Binary.PropositionalEquality.Properties.html#1658" class="Bound">f</a> <a id="1660" class="Symbol">:</a> <a id="1662" href="Relation.Binary.PropositionalEquality.Properties.html#715" class="Generalizable">B</a> <a id="1664" class="Symbol">→</a> <a id="1666" href="Relation.Binary.PropositionalEquality.Properties.html#717" class="Generalizable">C</a><a id="1667" class="Symbol">}</a> <a id="1669" class="Symbol">{</a><a id="1670" href="Relation.Binary.PropositionalEquality.Properties.html#1670" class="Bound">g</a> <a id="1672" class="Symbol">:</a> <a id="1674" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a> <a id="1676" class="Symbol">→</a> <a id="1678" href="Relation.Binary.PropositionalEquality.Properties.html#715" class="Generalizable">B</a><a id="1679" class="Symbol">}</a> <a id="1681" class="Symbol">(</a><a id="1682" href="Relation.Binary.PropositionalEquality.Properties.html#1682" class="Bound">p</a> <a id="1684" class="Symbol">:</a> <a id="1686" href="Relation.Binary.PropositionalEquality.Properties.html#1648" class="Bound">x</a> <a id="1688" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1690" href="Relation.Binary.PropositionalEquality.Properties.html#1650" class="Bound">y</a><a id="1691" class="Symbol">)</a> <a id="1693" class="Symbol">→</a>
|
||
<a id="1704" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1709" class="Symbol">(</a><a id="1710" href="Relation.Binary.PropositionalEquality.Properties.html#1658" class="Bound">f</a> <a id="1712" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1714" href="Relation.Binary.PropositionalEquality.Properties.html#1670" class="Bound">g</a><a id="1715" class="Symbol">)</a> <a id="1717" href="Relation.Binary.PropositionalEquality.Properties.html#1682" class="Bound">p</a> <a id="1719" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1721" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1726" href="Relation.Binary.PropositionalEquality.Properties.html#1658" class="Bound">f</a> <a id="1728" class="Symbol">(</a><a id="1729" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1734" href="Relation.Binary.PropositionalEquality.Properties.html#1670" class="Bound">g</a> <a id="1736" href="Relation.Binary.PropositionalEquality.Properties.html#1682" class="Bound">p</a><a id="1737" class="Symbol">)</a>
|
||
<a id="1739" href="Relation.Binary.PropositionalEquality.Properties.html#1636" class="Function">cong-∘</a> <a id="1746" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1751" class="Symbol">=</a> <a id="1753" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="trans-cong"></a><a id="1759" href="Relation.Binary.PropositionalEquality.Properties.html#1759" class="Function">trans-cong</a> <a id="1770" class="Symbol">:</a> <a id="1772" class="Symbol">∀</a> <a id="1774" class="Symbol">{</a><a id="1775" href="Relation.Binary.PropositionalEquality.Properties.html#1775" class="Bound">x</a> <a id="1777" href="Relation.Binary.PropositionalEquality.Properties.html#1777" class="Bound">y</a> <a id="1779" href="Relation.Binary.PropositionalEquality.Properties.html#1779" class="Bound">z</a> <a id="1781" class="Symbol">:</a> <a id="1783" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="1784" class="Symbol">}</a> <a id="1786" class="Symbol">{</a><a id="1787" href="Relation.Binary.PropositionalEquality.Properties.html#1787" class="Bound">f</a> <a id="1789" class="Symbol">:</a> <a id="1791" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a> <a id="1793" class="Symbol">→</a> <a id="1795" href="Relation.Binary.PropositionalEquality.Properties.html#715" class="Generalizable">B</a><a id="1796" class="Symbol">}</a> <a id="1798" class="Symbol">(</a><a id="1799" href="Relation.Binary.PropositionalEquality.Properties.html#1799" class="Bound">p</a> <a id="1801" class="Symbol">:</a> <a id="1803" href="Relation.Binary.PropositionalEquality.Properties.html#1775" class="Bound">x</a> <a id="1805" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1807" href="Relation.Binary.PropositionalEquality.Properties.html#1777" class="Bound">y</a><a id="1808" class="Symbol">)</a> <a id="1810" class="Symbol">{</a><a id="1811" href="Relation.Binary.PropositionalEquality.Properties.html#1811" class="Bound">q</a> <a id="1813" class="Symbol">:</a> <a id="1815" href="Relation.Binary.PropositionalEquality.Properties.html#1777" class="Bound">y</a> <a id="1817" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1819" href="Relation.Binary.PropositionalEquality.Properties.html#1779" class="Bound">z</a><a id="1820" class="Symbol">}</a> <a id="1822" class="Symbol">→</a>
|
||
<a id="1837" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1843" class="Symbol">(</a><a id="1844" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1849" href="Relation.Binary.PropositionalEquality.Properties.html#1787" class="Bound">f</a> <a id="1851" href="Relation.Binary.PropositionalEquality.Properties.html#1799" class="Bound">p</a><a id="1852" class="Symbol">)</a> <a id="1854" class="Symbol">(</a><a id="1855" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1860" href="Relation.Binary.PropositionalEquality.Properties.html#1787" class="Bound">f</a> <a id="1862" href="Relation.Binary.PropositionalEquality.Properties.html#1811" class="Bound">q</a><a id="1863" class="Symbol">)</a> <a id="1865" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1867" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1872" href="Relation.Binary.PropositionalEquality.Properties.html#1787" class="Bound">f</a> <a id="1874" class="Symbol">(</a><a id="1875" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1881" href="Relation.Binary.PropositionalEquality.Properties.html#1799" class="Bound">p</a> <a id="1883" href="Relation.Binary.PropositionalEquality.Properties.html#1811" class="Bound">q</a><a id="1884" class="Symbol">)</a>
|
||
<a id="1886" href="Relation.Binary.PropositionalEquality.Properties.html#1759" class="Function">trans-cong</a> <a id="1897" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1902" class="Symbol">=</a> <a id="1904" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="cong₂-reflˡ"></a><a id="1910" href="Relation.Binary.PropositionalEquality.Properties.html#1910" class="Function">cong₂-reflˡ</a> <a id="1922" class="Symbol">:</a> <a id="1924" class="Symbol">∀</a> <a id="1926" class="Symbol">{</a><a id="1927" href="Relation.Binary.PropositionalEquality.Properties.html#1927" class="Bound Operator">_∙_</a> <a id="1931" class="Symbol">:</a> <a id="1933" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a> <a id="1935" class="Symbol">→</a> <a id="1937" href="Relation.Binary.PropositionalEquality.Properties.html#715" class="Generalizable">B</a> <a id="1939" class="Symbol">→</a> <a id="1941" href="Relation.Binary.PropositionalEquality.Properties.html#717" class="Generalizable">C</a><a id="1942" class="Symbol">}</a> <a id="1944" class="Symbol">{</a><a id="1945" href="Relation.Binary.PropositionalEquality.Properties.html#1945" class="Bound">x</a> <a id="1947" href="Relation.Binary.PropositionalEquality.Properties.html#1947" class="Bound">u</a> <a id="1949" href="Relation.Binary.PropositionalEquality.Properties.html#1949" class="Bound">v</a><a id="1950" class="Symbol">}</a> <a id="1952" class="Symbol">→</a> <a id="1954" class="Symbol">(</a><a id="1955" href="Relation.Binary.PropositionalEquality.Properties.html#1955" class="Bound">p</a> <a id="1957" class="Symbol">:</a> <a id="1959" href="Relation.Binary.PropositionalEquality.Properties.html#1947" class="Bound">u</a> <a id="1961" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1963" href="Relation.Binary.PropositionalEquality.Properties.html#1949" class="Bound">v</a><a id="1964" class="Symbol">)</a> <a id="1966" class="Symbol">→</a>
|
||
<a id="1982" href="Relation.Binary.PropositionalEquality.Core.html#1367" class="Function">cong₂</a> <a id="1988" href="Relation.Binary.PropositionalEquality.Properties.html#1927" class="Bound Operator">_∙_</a> <a id="1992" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1997" href="Relation.Binary.PropositionalEquality.Properties.html#1955" class="Bound">p</a> <a id="1999" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2001" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="2006" class="Symbol">(</a><a id="2007" href="Relation.Binary.PropositionalEquality.Properties.html#1945" class="Bound">x</a> <a id="2009" href="Relation.Binary.PropositionalEquality.Properties.html#1927" class="Bound Operator">∙_</a><a id="2011" class="Symbol">)</a> <a id="2013" href="Relation.Binary.PropositionalEquality.Properties.html#1955" class="Bound">p</a>
|
||
<a id="2015" href="Relation.Binary.PropositionalEquality.Properties.html#1910" class="Function">cong₂-reflˡ</a> <a id="2027" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2032" class="Symbol">=</a> <a id="2034" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="cong₂-reflʳ"></a><a id="2040" href="Relation.Binary.PropositionalEquality.Properties.html#2040" class="Function">cong₂-reflʳ</a> <a id="2052" class="Symbol">:</a> <a id="2054" class="Symbol">∀</a> <a id="2056" class="Symbol">{</a><a id="2057" href="Relation.Binary.PropositionalEquality.Properties.html#2057" class="Bound Operator">_∙_</a> <a id="2061" class="Symbol">:</a> <a id="2063" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a> <a id="2065" class="Symbol">→</a> <a id="2067" href="Relation.Binary.PropositionalEquality.Properties.html#715" class="Generalizable">B</a> <a id="2069" class="Symbol">→</a> <a id="2071" href="Relation.Binary.PropositionalEquality.Properties.html#717" class="Generalizable">C</a><a id="2072" class="Symbol">}</a> <a id="2074" class="Symbol">{</a><a id="2075" href="Relation.Binary.PropositionalEquality.Properties.html#2075" class="Bound">x</a> <a id="2077" href="Relation.Binary.PropositionalEquality.Properties.html#2077" class="Bound">y</a> <a id="2079" href="Relation.Binary.PropositionalEquality.Properties.html#2079" class="Bound">u</a><a id="2080" class="Symbol">}</a> <a id="2082" class="Symbol">→</a> <a id="2084" class="Symbol">(</a><a id="2085" href="Relation.Binary.PropositionalEquality.Properties.html#2085" class="Bound">p</a> <a id="2087" class="Symbol">:</a> <a id="2089" href="Relation.Binary.PropositionalEquality.Properties.html#2075" class="Bound">x</a> <a id="2091" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2093" href="Relation.Binary.PropositionalEquality.Properties.html#2077" class="Bound">y</a><a id="2094" class="Symbol">)</a> <a id="2096" class="Symbol">→</a>
|
||
<a id="2112" href="Relation.Binary.PropositionalEquality.Core.html#1367" class="Function">cong₂</a> <a id="2118" href="Relation.Binary.PropositionalEquality.Properties.html#2057" class="Bound Operator">_∙_</a> <a id="2122" href="Relation.Binary.PropositionalEquality.Properties.html#2085" class="Bound">p</a> <a id="2124" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2129" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2131" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="2136" class="Symbol">(</a><a id="2137" href="Relation.Binary.PropositionalEquality.Properties.html#2057" class="Bound Operator">_∙</a> <a id="2140" href="Relation.Binary.PropositionalEquality.Properties.html#2079" class="Bound">u</a><a id="2141" class="Symbol">)</a> <a id="2143" href="Relation.Binary.PropositionalEquality.Properties.html#2085" class="Bound">p</a>
|
||
<a id="2145" href="Relation.Binary.PropositionalEquality.Properties.html#2040" class="Function">cong₂-reflʳ</a> <a id="2157" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2162" class="Symbol">=</a> <a id="2164" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="2170" class="Keyword">module</a> <a id="2177" href="Relation.Binary.PropositionalEquality.Properties.html#2177" class="Module">_</a> <a id="2179" class="Symbol">{</a><a id="2180" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2182" class="Symbol">:</a> <a id="2184" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2189" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a> <a id="2191" href="Relation.Binary.PropositionalEquality.Properties.html#699" class="Generalizable">p</a><a id="2192" class="Symbol">}</a> <a id="2194" class="Symbol">{</a><a id="2195" href="Relation.Binary.PropositionalEquality.Properties.html#2195" class="Bound">x</a> <a id="2197" href="Relation.Binary.PropositionalEquality.Properties.html#2197" class="Bound">y</a> <a id="2199" class="Symbol">:</a> <a id="2201" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="2202" class="Symbol">}</a> <a id="2204" class="Keyword">where</a>
|
||
|
||
<a id="2213" href="Relation.Binary.PropositionalEquality.Properties.html#2213" class="Function">subst-injective</a> <a id="2229" class="Symbol">:</a> <a id="2231" class="Symbol">∀</a> <a id="2233" class="Symbol">(</a><a id="2234" href="Relation.Binary.PropositionalEquality.Properties.html#2234" class="Bound">x≡y</a> <a id="2238" class="Symbol">:</a> <a id="2240" href="Relation.Binary.PropositionalEquality.Properties.html#2195" class="Bound">x</a> <a id="2242" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2244" href="Relation.Binary.PropositionalEquality.Properties.html#2197" class="Bound">y</a><a id="2245" class="Symbol">)</a> <a id="2247" class="Symbol">{</a><a id="2248" href="Relation.Binary.PropositionalEquality.Properties.html#2248" class="Bound">p</a> <a id="2250" href="Relation.Binary.PropositionalEquality.Properties.html#2250" class="Bound">q</a> <a id="2252" class="Symbol">:</a> <a id="2254" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2256" href="Relation.Binary.PropositionalEquality.Properties.html#2195" class="Bound">x</a><a id="2257" class="Symbol">}</a> <a id="2259" class="Symbol">→</a>
|
||
<a id="2281" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2287" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2289" href="Relation.Binary.PropositionalEquality.Properties.html#2234" class="Bound">x≡y</a> <a id="2293" href="Relation.Binary.PropositionalEquality.Properties.html#2248" class="Bound">p</a> <a id="2295" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2297" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2303" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2305" href="Relation.Binary.PropositionalEquality.Properties.html#2234" class="Bound">x≡y</a> <a id="2309" href="Relation.Binary.PropositionalEquality.Properties.html#2250" class="Bound">q</a> <a id="2311" class="Symbol">→</a> <a id="2313" href="Relation.Binary.PropositionalEquality.Properties.html#2248" class="Bound">p</a> <a id="2315" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2317" href="Relation.Binary.PropositionalEquality.Properties.html#2250" class="Bound">q</a>
|
||
<a id="2321" href="Relation.Binary.PropositionalEquality.Properties.html#2213" class="Function">subst-injective</a> <a id="2337" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2342" href="Relation.Binary.PropositionalEquality.Properties.html#2342" class="Bound">p≡q</a> <a id="2346" class="Symbol">=</a> <a id="2348" href="Relation.Binary.PropositionalEquality.Properties.html#2342" class="Bound">p≡q</a>
|
||
|
||
<a id="2355" href="Relation.Binary.PropositionalEquality.Properties.html#2355" class="Function">subst-subst</a> <a id="2367" class="Symbol">:</a> <a id="2369" class="Symbol">∀</a> <a id="2371" class="Symbol">{</a><a id="2372" href="Relation.Binary.PropositionalEquality.Properties.html#2372" class="Bound">z</a><a id="2373" class="Symbol">}</a> <a id="2375" class="Symbol">(</a><a id="2376" href="Relation.Binary.PropositionalEquality.Properties.html#2376" class="Bound">x≡y</a> <a id="2380" class="Symbol">:</a> <a id="2382" href="Relation.Binary.PropositionalEquality.Properties.html#2195" class="Bound">x</a> <a id="2384" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2386" href="Relation.Binary.PropositionalEquality.Properties.html#2197" class="Bound">y</a><a id="2387" class="Symbol">)</a> <a id="2389" class="Symbol">{</a><a id="2390" href="Relation.Binary.PropositionalEquality.Properties.html#2390" class="Bound">y≡z</a> <a id="2394" class="Symbol">:</a> <a id="2396" href="Relation.Binary.PropositionalEquality.Properties.html#2197" class="Bound">y</a> <a id="2398" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2400" href="Relation.Binary.PropositionalEquality.Properties.html#2372" class="Bound">z</a><a id="2401" class="Symbol">}</a> <a id="2403" class="Symbol">{</a><a id="2404" href="Relation.Binary.PropositionalEquality.Properties.html#2404" class="Bound">p</a> <a id="2406" class="Symbol">:</a> <a id="2408" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2410" href="Relation.Binary.PropositionalEquality.Properties.html#2195" class="Bound">x</a><a id="2411" class="Symbol">}</a> <a id="2413" class="Symbol">→</a>
|
||
<a id="2431" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2437" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2439" href="Relation.Binary.PropositionalEquality.Properties.html#2390" class="Bound">y≡z</a> <a id="2443" class="Symbol">(</a><a id="2444" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2450" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2452" href="Relation.Binary.PropositionalEquality.Properties.html#2376" class="Bound">x≡y</a> <a id="2456" href="Relation.Binary.PropositionalEquality.Properties.html#2404" class="Bound">p</a><a id="2457" class="Symbol">)</a> <a id="2459" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2461" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2467" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2469" class="Symbol">(</a><a id="2470" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="2476" href="Relation.Binary.PropositionalEquality.Properties.html#2376" class="Bound">x≡y</a> <a id="2480" href="Relation.Binary.PropositionalEquality.Properties.html#2390" class="Bound">y≡z</a><a id="2483" class="Symbol">)</a> <a id="2485" href="Relation.Binary.PropositionalEquality.Properties.html#2404" class="Bound">p</a>
|
||
<a id="2489" href="Relation.Binary.PropositionalEquality.Properties.html#2355" class="Function">subst-subst</a> <a id="2501" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2506" class="Symbol">=</a> <a id="2508" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="2516" href="Relation.Binary.PropositionalEquality.Properties.html#2516" class="Function">subst-subst-sym</a> <a id="2532" class="Symbol">:</a> <a id="2534" class="Symbol">(</a><a id="2535" href="Relation.Binary.PropositionalEquality.Properties.html#2535" class="Bound">x≡y</a> <a id="2539" class="Symbol">:</a> <a id="2541" href="Relation.Binary.PropositionalEquality.Properties.html#2195" class="Bound">x</a> <a id="2543" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2545" href="Relation.Binary.PropositionalEquality.Properties.html#2197" class="Bound">y</a><a id="2546" class="Symbol">)</a> <a id="2548" class="Symbol">{</a><a id="2549" href="Relation.Binary.PropositionalEquality.Properties.html#2549" class="Bound">p</a> <a id="2551" class="Symbol">:</a> <a id="2553" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2555" href="Relation.Binary.PropositionalEquality.Properties.html#2197" class="Bound">y</a><a id="2556" class="Symbol">}</a> <a id="2558" class="Symbol">→</a>
|
||
<a id="2580" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2586" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2588" href="Relation.Binary.PropositionalEquality.Properties.html#2535" class="Bound">x≡y</a> <a id="2592" class="Symbol">(</a><a id="2593" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2599" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2601" class="Symbol">(</a><a id="2602" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="2606" href="Relation.Binary.PropositionalEquality.Properties.html#2535" class="Bound">x≡y</a><a id="2609" class="Symbol">)</a> <a id="2611" href="Relation.Binary.PropositionalEquality.Properties.html#2549" class="Bound">p</a><a id="2612" class="Symbol">)</a> <a id="2614" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2616" href="Relation.Binary.PropositionalEquality.Properties.html#2549" class="Bound">p</a>
|
||
<a id="2620" href="Relation.Binary.PropositionalEquality.Properties.html#2516" class="Function">subst-subst-sym</a> <a id="2636" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2641" class="Symbol">=</a> <a id="2643" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="2651" href="Relation.Binary.PropositionalEquality.Properties.html#2651" class="Function">subst-sym-subst</a> <a id="2667" class="Symbol">:</a> <a id="2669" class="Symbol">(</a><a id="2670" href="Relation.Binary.PropositionalEquality.Properties.html#2670" class="Bound">x≡y</a> <a id="2674" class="Symbol">:</a> <a id="2676" href="Relation.Binary.PropositionalEquality.Properties.html#2195" class="Bound">x</a> <a id="2678" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2680" href="Relation.Binary.PropositionalEquality.Properties.html#2197" class="Bound">y</a><a id="2681" class="Symbol">)</a> <a id="2683" class="Symbol">{</a><a id="2684" href="Relation.Binary.PropositionalEquality.Properties.html#2684" class="Bound">p</a> <a id="2686" class="Symbol">:</a> <a id="2688" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2690" href="Relation.Binary.PropositionalEquality.Properties.html#2195" class="Bound">x</a><a id="2691" class="Symbol">}</a> <a id="2693" class="Symbol">→</a>
|
||
<a id="2715" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2721" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2723" class="Symbol">(</a><a id="2724" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="2728" href="Relation.Binary.PropositionalEquality.Properties.html#2670" class="Bound">x≡y</a><a id="2731" class="Symbol">)</a> <a id="2733" class="Symbol">(</a><a id="2734" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2740" href="Relation.Binary.PropositionalEquality.Properties.html#2180" class="Bound">P</a> <a id="2742" href="Relation.Binary.PropositionalEquality.Properties.html#2670" class="Bound">x≡y</a> <a id="2746" href="Relation.Binary.PropositionalEquality.Properties.html#2684" class="Bound">p</a><a id="2747" class="Symbol">)</a> <a id="2749" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2751" href="Relation.Binary.PropositionalEquality.Properties.html#2684" class="Bound">p</a>
|
||
<a id="2755" href="Relation.Binary.PropositionalEquality.Properties.html#2651" class="Function">subst-sym-subst</a> <a id="2771" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2776" class="Symbol">=</a> <a id="2778" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="subst-∘"></a><a id="2784" href="Relation.Binary.PropositionalEquality.Properties.html#2784" class="Function">subst-∘</a> <a id="2792" class="Symbol">:</a> <a id="2794" class="Symbol">∀</a> <a id="2796" class="Symbol">{</a><a id="2797" href="Relation.Binary.PropositionalEquality.Properties.html#2797" class="Bound">x</a> <a id="2799" href="Relation.Binary.PropositionalEquality.Properties.html#2799" class="Bound">y</a> <a id="2801" class="Symbol">:</a> <a id="2803" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="2804" class="Symbol">}</a> <a id="2806" class="Symbol">{</a><a id="2807" href="Relation.Binary.PropositionalEquality.Properties.html#2807" class="Bound">P</a> <a id="2809" class="Symbol">:</a> <a id="2811" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2816" href="Relation.Binary.PropositionalEquality.Properties.html#715" class="Generalizable">B</a> <a id="2818" href="Relation.Binary.PropositionalEquality.Properties.html#699" class="Generalizable">p</a><a id="2819" class="Symbol">}</a> <a id="2821" class="Symbol">{</a><a id="2822" href="Relation.Binary.PropositionalEquality.Properties.html#2822" class="Bound">f</a> <a id="2824" class="Symbol">:</a> <a id="2826" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a> <a id="2828" class="Symbol">→</a> <a id="2830" href="Relation.Binary.PropositionalEquality.Properties.html#715" class="Generalizable">B</a><a id="2831" class="Symbol">}</a>
|
||
<a id="2843" class="Symbol">(</a><a id="2844" href="Relation.Binary.PropositionalEquality.Properties.html#2844" class="Bound">x≡y</a> <a id="2848" class="Symbol">:</a> <a id="2850" href="Relation.Binary.PropositionalEquality.Properties.html#2797" class="Bound">x</a> <a id="2852" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2854" href="Relation.Binary.PropositionalEquality.Properties.html#2799" class="Bound">y</a><a id="2855" class="Symbol">)</a> <a id="2857" class="Symbol">{</a><a id="2858" href="Relation.Binary.PropositionalEquality.Properties.html#2858" class="Bound">p</a> <a id="2860" class="Symbol">:</a> <a id="2862" href="Relation.Binary.PropositionalEquality.Properties.html#2807" class="Bound">P</a> <a id="2864" class="Symbol">(</a><a id="2865" href="Relation.Binary.PropositionalEquality.Properties.html#2822" class="Bound">f</a> <a id="2867" href="Relation.Binary.PropositionalEquality.Properties.html#2797" class="Bound">x</a><a id="2868" class="Symbol">)}</a> <a id="2871" class="Symbol">→</a>
|
||
<a id="2883" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2889" class="Symbol">(</a><a id="2890" href="Relation.Binary.PropositionalEquality.Properties.html#2807" class="Bound">P</a> <a id="2892" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="2894" href="Relation.Binary.PropositionalEquality.Properties.html#2822" class="Bound">f</a><a id="2895" class="Symbol">)</a> <a id="2897" href="Relation.Binary.PropositionalEquality.Properties.html#2844" class="Bound">x≡y</a> <a id="2901" href="Relation.Binary.PropositionalEquality.Properties.html#2858" class="Bound">p</a> <a id="2903" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2905" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="2911" href="Relation.Binary.PropositionalEquality.Properties.html#2807" class="Bound">P</a> <a id="2913" class="Symbol">(</a><a id="2914" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="2919" href="Relation.Binary.PropositionalEquality.Properties.html#2822" class="Bound">f</a> <a id="2921" href="Relation.Binary.PropositionalEquality.Properties.html#2844" class="Bound">x≡y</a><a id="2924" class="Symbol">)</a> <a id="2926" href="Relation.Binary.PropositionalEquality.Properties.html#2858" class="Bound">p</a>
|
||
<a id="2928" href="Relation.Binary.PropositionalEquality.Properties.html#2784" class="Function">subst-∘</a> <a id="2936" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2941" class="Symbol">=</a> <a id="2943" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="subst-application"></a><a id="2949" href="Relation.Binary.PropositionalEquality.Properties.html#2949" class="Function">subst-application</a> <a id="2967" class="Symbol">:</a> <a id="2969" class="Symbol">∀</a> <a id="2971" class="Symbol">{</a><a id="2972" href="Relation.Binary.PropositionalEquality.Properties.html#2972" class="Bound">a₁</a> <a id="2975" href="Relation.Binary.PropositionalEquality.Properties.html#2975" class="Bound">a₂</a> <a id="2978" href="Relation.Binary.PropositionalEquality.Properties.html#2978" class="Bound">b₁</a> <a id="2981" href="Relation.Binary.PropositionalEquality.Properties.html#2981" class="Bound">b₂</a><a id="2983" class="Symbol">}</a> <a id="2985" class="Symbol">{</a><a id="2986" href="Relation.Binary.PropositionalEquality.Properties.html#2986" class="Bound">A₁</a> <a id="2989" class="Symbol">:</a> <a id="2991" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2995" href="Relation.Binary.PropositionalEquality.Properties.html#2972" class="Bound">a₁</a><a id="2997" class="Symbol">}</a> <a id="2999" class="Symbol">{</a><a id="3000" href="Relation.Binary.PropositionalEquality.Properties.html#3000" class="Bound">A₂</a> <a id="3003" class="Symbol">:</a> <a id="3005" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3009" href="Relation.Binary.PropositionalEquality.Properties.html#2975" class="Bound">a₂</a><a id="3011" class="Symbol">}</a>
|
||
<a id="3033" class="Symbol">(</a><a id="3034" href="Relation.Binary.PropositionalEquality.Properties.html#3034" class="Bound">B₁</a> <a id="3037" class="Symbol">:</a> <a id="3039" href="Relation.Binary.PropositionalEquality.Properties.html#2986" class="Bound">A₁</a> <a id="3042" class="Symbol">→</a> <a id="3044" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3048" href="Relation.Binary.PropositionalEquality.Properties.html#2978" class="Bound">b₁</a><a id="3050" class="Symbol">)</a> <a id="3052" class="Symbol">{</a><a id="3053" href="Relation.Binary.PropositionalEquality.Properties.html#3053" class="Bound">B₂</a> <a id="3056" class="Symbol">:</a> <a id="3058" href="Relation.Binary.PropositionalEquality.Properties.html#3000" class="Bound">A₂</a> <a id="3061" class="Symbol">→</a> <a id="3063" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3067" href="Relation.Binary.PropositionalEquality.Properties.html#2981" class="Bound">b₂</a><a id="3069" class="Symbol">}</a>
|
||
<a id="3091" class="Symbol">{</a><a id="3092" href="Relation.Binary.PropositionalEquality.Properties.html#3092" class="Bound">f</a> <a id="3094" class="Symbol">:</a> <a id="3096" href="Relation.Binary.PropositionalEquality.Properties.html#3000" class="Bound">A₂</a> <a id="3099" class="Symbol">→</a> <a id="3101" href="Relation.Binary.PropositionalEquality.Properties.html#2986" class="Bound">A₁</a><a id="3103" class="Symbol">}</a> <a id="3105" class="Symbol">{</a><a id="3106" href="Relation.Binary.PropositionalEquality.Properties.html#3106" class="Bound">x₁</a> <a id="3109" href="Relation.Binary.PropositionalEquality.Properties.html#3109" class="Bound">x₂</a> <a id="3112" class="Symbol">:</a> <a id="3114" href="Relation.Binary.PropositionalEquality.Properties.html#3000" class="Bound">A₂</a><a id="3116" class="Symbol">}</a> <a id="3118" class="Symbol">{</a><a id="3119" href="Relation.Binary.PropositionalEquality.Properties.html#3119" class="Bound">y</a> <a id="3121" class="Symbol">:</a> <a id="3123" href="Relation.Binary.PropositionalEquality.Properties.html#3034" class="Bound">B₁</a> <a id="3126" class="Symbol">(</a><a id="3127" href="Relation.Binary.PropositionalEquality.Properties.html#3092" class="Bound">f</a> <a id="3129" href="Relation.Binary.PropositionalEquality.Properties.html#3106" class="Bound">x₁</a><a id="3131" class="Symbol">)}</a>
|
||
<a id="3154" class="Symbol">(</a><a id="3155" href="Relation.Binary.PropositionalEquality.Properties.html#3155" class="Bound">g</a> <a id="3157" class="Symbol">:</a> <a id="3159" class="Symbol">∀</a> <a id="3161" href="Relation.Binary.PropositionalEquality.Properties.html#3161" class="Bound">x</a> <a id="3163" class="Symbol">→</a> <a id="3165" href="Relation.Binary.PropositionalEquality.Properties.html#3034" class="Bound">B₁</a> <a id="3168" class="Symbol">(</a><a id="3169" href="Relation.Binary.PropositionalEquality.Properties.html#3092" class="Bound">f</a> <a id="3171" href="Relation.Binary.PropositionalEquality.Properties.html#3161" class="Bound">x</a><a id="3172" class="Symbol">)</a> <a id="3174" class="Symbol">→</a> <a id="3176" href="Relation.Binary.PropositionalEquality.Properties.html#3053" class="Bound">B₂</a> <a id="3179" href="Relation.Binary.PropositionalEquality.Properties.html#3161" class="Bound">x</a><a id="3180" class="Symbol">)</a> <a id="3182" class="Symbol">(</a><a id="3183" href="Relation.Binary.PropositionalEquality.Properties.html#3183" class="Bound">eq</a> <a id="3186" class="Symbol">:</a> <a id="3188" href="Relation.Binary.PropositionalEquality.Properties.html#3106" class="Bound">x₁</a> <a id="3191" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3193" href="Relation.Binary.PropositionalEquality.Properties.html#3109" class="Bound">x₂</a><a id="3195" class="Symbol">)</a> <a id="3197" class="Symbol">→</a>
|
||
<a id="3219" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="3225" href="Relation.Binary.PropositionalEquality.Properties.html#3053" class="Bound">B₂</a> <a id="3228" href="Relation.Binary.PropositionalEquality.Properties.html#3183" class="Bound">eq</a> <a id="3231" class="Symbol">(</a><a id="3232" href="Relation.Binary.PropositionalEquality.Properties.html#3155" class="Bound">g</a> <a id="3234" href="Relation.Binary.PropositionalEquality.Properties.html#3106" class="Bound">x₁</a> <a id="3237" href="Relation.Binary.PropositionalEquality.Properties.html#3119" class="Bound">y</a><a id="3238" class="Symbol">)</a> <a id="3240" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3242" href="Relation.Binary.PropositionalEquality.Properties.html#3155" class="Bound">g</a> <a id="3244" href="Relation.Binary.PropositionalEquality.Properties.html#3109" class="Bound">x₂</a> <a id="3247" class="Symbol">(</a><a id="3248" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="3254" href="Relation.Binary.PropositionalEquality.Properties.html#3034" class="Bound">B₁</a> <a id="3257" class="Symbol">(</a><a id="3258" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3263" href="Relation.Binary.PropositionalEquality.Properties.html#3092" class="Bound">f</a> <a id="3265" href="Relation.Binary.PropositionalEquality.Properties.html#3183" class="Bound">eq</a><a id="3267" class="Symbol">)</a> <a id="3269" href="Relation.Binary.PropositionalEquality.Properties.html#3119" class="Bound">y</a><a id="3270" class="Symbol">)</a>
|
||
<a id="3272" href="Relation.Binary.PropositionalEquality.Properties.html#2949" class="Function">subst-application</a> <a id="3290" class="Symbol">_</a> <a id="3292" class="Symbol">_</a> <a id="3294" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="3299" class="Symbol">=</a> <a id="3301" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="3307" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="3380" class="Comment">-- Structure of equality as a binary relation</a>
|
||
|
||
<a id="isEquivalence"></a><a id="3427" href="Relation.Binary.PropositionalEquality.Properties.html#3427" class="Function">isEquivalence</a> <a id="3441" class="Symbol">:</a> <a id="3443" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a> <a id="3457" class="Symbol">{</a><a id="3458" class="Argument">A</a> <a id="3460" class="Symbol">=</a> <a id="3462" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="3463" class="Symbol">}</a> <a id="3465" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="3469" href="Relation.Binary.PropositionalEquality.Properties.html#3427" class="Function">isEquivalence</a> <a id="3483" class="Symbol">=</a> <a id="3485" class="Keyword">record</a>
|
||
<a id="3494" class="Symbol">{</a> <a id="3496" href="Relation.Binary.Structures.html#1568" class="Field">refl</a> <a id="3502" class="Symbol">=</a> <a id="3504" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
<a id="3511" class="Symbol">;</a> <a id="3513" href="Relation.Binary.Structures.html#1594" class="Field">sym</a> <a id="3519" class="Symbol">=</a> <a id="3521" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a>
|
||
<a id="3527" class="Symbol">;</a> <a id="3529" href="Relation.Binary.Structures.html#1620" class="Field">trans</a> <a id="3535" class="Symbol">=</a> <a id="3537" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a>
|
||
<a id="3545" class="Symbol">}</a>
|
||
|
||
<a id="isDecEquivalence"></a><a id="3548" href="Relation.Binary.PropositionalEquality.Properties.html#3548" class="Function">isDecEquivalence</a> <a id="3565" class="Symbol">:</a> <a id="3567" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="3577" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="3581" class="Symbol">→</a> <a id="3583" href="Relation.Binary.Structures.html#1824" class="Record">IsDecEquivalence</a> <a id="3600" class="Symbol">{</a><a id="3601" class="Argument">A</a> <a id="3603" class="Symbol">=</a> <a id="3605" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="3606" class="Symbol">}</a> <a id="3608" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="3612" href="Relation.Binary.PropositionalEquality.Properties.html#3548" class="Function">isDecEquivalence</a> <a id="3629" href="Relation.Binary.PropositionalEquality.Properties.html#3629" class="Bound Operator">_≟_</a> <a id="3633" class="Symbol">=</a> <a id="3635" class="Keyword">record</a>
|
||
<a id="3644" class="Symbol">{</a> <a id="3646" href="Relation.Binary.Structures.html#1887" class="Field">isEquivalence</a> <a id="3660" class="Symbol">=</a> <a id="3662" href="Relation.Binary.PropositionalEquality.Properties.html#3427" class="Function">isEquivalence</a>
|
||
<a id="3678" class="Symbol">;</a> <a id="3680" href="Relation.Binary.Structures.html#1921" class="Field Operator">_≟_</a> <a id="3694" class="Symbol">=</a> <a id="3696" href="Relation.Binary.PropositionalEquality.Properties.html#3629" class="Bound Operator">_≟_</a>
|
||
<a id="3702" class="Symbol">}</a>
|
||
|
||
<a id="isPreorder"></a><a id="3705" href="Relation.Binary.PropositionalEquality.Properties.html#3705" class="Function">isPreorder</a> <a id="3716" class="Symbol">:</a> <a id="3718" href="Relation.Binary.Structures.html#2163" class="Record">IsPreorder</a> <a id="3729" class="Symbol">{</a><a id="3730" class="Argument">A</a> <a id="3732" class="Symbol">=</a> <a id="3734" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="3735" class="Symbol">}</a> <a id="3737" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="3741" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="3745" href="Relation.Binary.PropositionalEquality.Properties.html#3705" class="Function">isPreorder</a> <a id="3756" class="Symbol">=</a> <a id="3758" class="Keyword">record</a>
|
||
<a id="3767" class="Symbol">{</a> <a id="3769" href="Relation.Binary.Structures.html#2228" class="Field">isEquivalence</a> <a id="3783" class="Symbol">=</a> <a id="3785" href="Relation.Binary.PropositionalEquality.Properties.html#3427" class="Function">isEquivalence</a>
|
||
<a id="3801" class="Symbol">;</a> <a id="3803" href="Relation.Binary.Structures.html#2331" class="Field">reflexive</a> <a id="3817" class="Symbol">=</a> <a id="3819" href="Function.Base.html#615" class="Function">id</a>
|
||
<a id="3824" class="Symbol">;</a> <a id="3826" href="Relation.Binary.Structures.html#2361" class="Field">trans</a> <a id="3840" class="Symbol">=</a> <a id="3842" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a>
|
||
<a id="3850" class="Symbol">}</a>
|
||
|
||
<a id="3853" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="3926" class="Comment">-- Bundles for equality as a binary relation</a>
|
||
|
||
<a id="setoid"></a><a id="3972" href="Relation.Binary.PropositionalEquality.Properties.html#3972" class="Function">setoid</a> <a id="3979" class="Symbol">:</a> <a id="3981" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3985" href="Relation.Binary.PropositionalEquality.Properties.html#697" class="Generalizable">a</a> <a id="3987" class="Symbol">→</a> <a id="3989" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="3996" class="Symbol">_</a> <a id="3998" class="Symbol">_</a>
|
||
<a id="4000" href="Relation.Binary.PropositionalEquality.Properties.html#3972" class="Function">setoid</a> <a id="4007" href="Relation.Binary.PropositionalEquality.Properties.html#4007" class="Bound">A</a> <a id="4009" class="Symbol">=</a> <a id="4011" class="Keyword">record</a>
|
||
<a id="4020" class="Symbol">{</a> <a id="4022" href="Relation.Binary.Bundles.html#1072" class="Field">Carrier</a> <a id="4036" class="Symbol">=</a> <a id="4038" href="Relation.Binary.PropositionalEquality.Properties.html#4007" class="Bound">A</a>
|
||
<a id="4042" class="Symbol">;</a> <a id="4044" href="Relation.Binary.Bundles.html#1098" class="Field Operator">_≈_</a> <a id="4058" class="Symbol">=</a> <a id="4060" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="4066" class="Symbol">;</a> <a id="4068" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="4082" class="Symbol">=</a> <a id="4084" href="Relation.Binary.PropositionalEquality.Properties.html#3427" class="Function">isEquivalence</a>
|
||
<a id="4100" class="Symbol">}</a>
|
||
|
||
<a id="decSetoid"></a><a id="4103" href="Relation.Binary.PropositionalEquality.Properties.html#4103" class="Function">decSetoid</a> <a id="4113" class="Symbol">:</a> <a id="4115" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="4125" class="Symbol">{</a><a id="4126" class="Argument">A</a> <a id="4128" class="Symbol">=</a> <a id="4130" href="Relation.Binary.PropositionalEquality.Properties.html#713" class="Generalizable">A</a><a id="4131" class="Symbol">}</a> <a id="4133" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="4137" class="Symbol">→</a> <a id="4139" href="Relation.Binary.Bundles.html#1391" class="Record">DecSetoid</a> <a id="4149" class="Symbol">_</a> <a id="4151" class="Symbol">_</a>
|
||
<a id="4153" href="Relation.Binary.PropositionalEquality.Properties.html#4103" class="Function">decSetoid</a> <a id="4163" href="Relation.Binary.PropositionalEquality.Properties.html#4163" class="Bound Operator">_≟_</a> <a id="4167" class="Symbol">=</a> <a id="4169" class="Keyword">record</a>
|
||
<a id="4178" class="Symbol">{</a> <a id="4180" href="Relation.Binary.Bundles.html#1486" class="Field Operator">_≈_</a> <a id="4197" class="Symbol">=</a> <a id="4199" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="4205" class="Symbol">;</a> <a id="4207" href="Relation.Binary.Bundles.html#1523" class="Field">isDecEquivalence</a> <a id="4224" class="Symbol">=</a> <a id="4226" href="Relation.Binary.PropositionalEquality.Properties.html#3548" class="Function">isDecEquivalence</a> <a id="4243" href="Relation.Binary.PropositionalEquality.Properties.html#4163" class="Bound Operator">_≟_</a>
|
||
<a id="4249" class="Symbol">}</a>
|
||
|
||
<a id="preorder"></a><a id="4252" href="Relation.Binary.PropositionalEquality.Properties.html#4252" class="Function">preorder</a> <a id="4261" class="Symbol">:</a> <a id="4263" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4267" href="Relation.Binary.PropositionalEquality.Properties.html#697" class="Generalizable">a</a> <a id="4269" class="Symbol">→</a> <a id="4271" href="Relation.Binary.Bundles.html#1920" class="Record">Preorder</a> <a id="4280" class="Symbol">_</a> <a id="4282" class="Symbol">_</a> <a id="4284" class="Symbol">_</a>
|
||
<a id="4286" href="Relation.Binary.PropositionalEquality.Properties.html#4252" class="Function">preorder</a> <a id="4295" href="Relation.Binary.PropositionalEquality.Properties.html#4295" class="Bound">A</a> <a id="4297" class="Symbol">=</a> <a id="4299" class="Keyword">record</a>
|
||
<a id="4308" class="Symbol">{</a> <a id="4310" href="Relation.Binary.Bundles.html#1999" class="Field">Carrier</a> <a id="4321" class="Symbol">=</a> <a id="4323" href="Relation.Binary.PropositionalEquality.Properties.html#4295" class="Bound">A</a>
|
||
<a id="4327" class="Symbol">;</a> <a id="4329" href="Relation.Binary.Bundles.html#2022" class="Field Operator">_≈_</a> <a id="4340" class="Symbol">=</a> <a id="4342" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="4348" class="Symbol">;</a> <a id="4350" href="Relation.Binary.Bundles.html#2083" class="Field Operator">_∼_</a> <a id="4361" class="Symbol">=</a> <a id="4363" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="4369" class="Symbol">;</a> <a id="4371" href="Relation.Binary.Bundles.html#2133" class="Field">isPreorder</a> <a id="4382" class="Symbol">=</a> <a id="4384" href="Relation.Binary.PropositionalEquality.Properties.html#3705" class="Function">isPreorder</a>
|
||
<a id="4397" class="Symbol">}</a>
|
||
</pre></body></html> |