127 lines
44 KiB
HTML
127 lines
44 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Binary.PropositionalEquality.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">-- Propositional equality</a>
|
||
<a id="132" class="Comment">--</a>
|
||
<a id="135" class="Comment">-- This file contains some core definitions which are re-exported by</a>
|
||
<a id="204" class="Comment">-- Relation.Binary.PropositionalEquality.</a>
|
||
<a id="246" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="320" class="Symbol">{-#</a> <a id="324" class="Keyword">OPTIONS</a> <a id="332" class="Pragma">--without-K</a> <a id="344" class="Pragma">--safe</a> <a id="351" class="Symbol">#-}</a>
|
||
|
||
<a id="356" class="Keyword">module</a> <a id="363" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a> <a id="406" class="Keyword">where</a>
|
||
|
||
<a id="413" class="Keyword">open</a> <a id="418" class="Keyword">import</a> <a id="425" href="Data.Product.html" class="Module">Data.Product</a> <a id="438" class="Keyword">using</a> <a id="444" class="Symbol">(</a><a id="445" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a><a id="448" class="Symbol">)</a>
|
||
<a id="450" class="Keyword">open</a> <a id="455" class="Keyword">import</a> <a id="462" href="Function.Base.html" class="Module">Function.Base</a> <a id="476" class="Keyword">using</a> <a id="482" class="Symbol">(</a><a id="483" href="Function.Base.html#1031" class="Function Operator">_∘_</a><a id="486" class="Symbol">)</a>
|
||
<a id="488" class="Keyword">open</a> <a id="493" class="Keyword">import</a> <a id="500" href="Level.html" class="Module">Level</a>
|
||
<a id="506" class="Keyword">open</a> <a id="511" class="Keyword">import</a> <a id="518" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a>
|
||
<a id="539" class="Keyword">open</a> <a id="544" class="Keyword">import</a> <a id="551" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a>
|
||
<a id="579" class="Keyword">open</a> <a id="584" class="Keyword">import</a> <a id="591" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="608" class="Keyword">using</a> <a id="614" class="Symbol">(</a><a id="615" href="Relation.Nullary.html#656" class="Function Operator">¬_</a><a id="617" class="Symbol">)</a>
|
||
|
||
<a id="620" class="Keyword">private</a>
|
||
<a id="630" class="Keyword">variable</a>
|
||
<a id="643" href="Relation.Binary.PropositionalEquality.Core.html#643" class="Generalizable">a</a> <a id="645" href="Relation.Binary.PropositionalEquality.Core.html#645" class="Generalizable">b</a> <a id="647" href="Relation.Binary.PropositionalEquality.Core.html#647" class="Generalizable">ℓ</a> <a id="649" class="Symbol">:</a> <a id="651" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="661" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="663" href="Relation.Binary.PropositionalEquality.Core.html#663" class="Generalizable">B</a> <a id="665" href="Relation.Binary.PropositionalEquality.Core.html#665" class="Generalizable">C</a> <a id="667" class="Symbol">:</a> <a id="669" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="673" href="Relation.Binary.PropositionalEquality.Core.html#643" class="Generalizable">a</a>
|
||
|
||
<a id="676" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="749" class="Comment">-- Propositional equality</a>
|
||
|
||
<a id="776" class="Keyword">open</a> <a id="781" class="Keyword">import</a> <a id="788" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a> <a id="810" class="Keyword">public</a>
|
||
|
||
<a id="818" class="Keyword">infix</a> <a id="824" class="Number">4</a> <a id="826" href="Relation.Binary.PropositionalEquality.Core.html#830" class="Function Operator">_≢_</a>
|
||
<a id="_≢_"></a><a id="830" href="Relation.Binary.PropositionalEquality.Core.html#830" class="Function Operator">_≢_</a> <a id="834" class="Symbol">:</a> <a id="836" class="Symbol">{</a><a id="837" href="Relation.Binary.PropositionalEquality.Core.html#837" class="Bound">A</a> <a id="839" class="Symbol">:</a> <a id="841" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="845" href="Relation.Binary.PropositionalEquality.Core.html#643" class="Generalizable">a</a><a id="846" class="Symbol">}</a> <a id="848" class="Symbol">→</a> <a id="850" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="854" href="Relation.Binary.PropositionalEquality.Core.html#837" class="Bound">A</a> <a id="856" href="Relation.Binary.PropositionalEquality.Core.html#643" class="Generalizable">a</a>
|
||
<a id="858" href="Relation.Binary.PropositionalEquality.Core.html#858" class="Bound">x</a> <a id="860" href="Relation.Binary.PropositionalEquality.Core.html#830" class="Function Operator">≢</a> <a id="862" href="Relation.Binary.PropositionalEquality.Core.html#862" class="Bound">y</a> <a id="864" class="Symbol">=</a> <a id="866" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="868" href="Relation.Binary.PropositionalEquality.Core.html#858" class="Bound">x</a> <a id="870" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="872" href="Relation.Binary.PropositionalEquality.Core.html#862" class="Bound">y</a>
|
||
|
||
<a id="875" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="948" class="Comment">-- A variant of `refl` where the argument is explicit</a>
|
||
|
||
<a id="1003" class="Keyword">pattern</a> <a id="erefl"></a><a id="1011" href="Relation.Binary.PropositionalEquality.Core.html#1011" class="InductiveConstructor">erefl</a> <a id="1017" href="Relation.Binary.PropositionalEquality.Core.html#1031" class="Bound">x</a> <a id="1019" class="Symbol">=</a> <a id="1021" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1026" class="Symbol">{</a><a id="1027" class="Argument">x</a> <a id="1029" class="Symbol">=</a> <a id="1031" href="Relation.Binary.PropositionalEquality.Core.html#1031" class="Bound">x</a><a id="1032" class="Symbol">}</a>
|
||
|
||
<a id="1035" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1108" class="Comment">-- Congruence lemmas</a>
|
||
|
||
<a id="cong"></a><a id="1130" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1135" class="Symbol">:</a> <a id="1137" class="Symbol">∀</a> <a id="1139" class="Symbol">(</a><a id="1140" href="Relation.Binary.PropositionalEquality.Core.html#1140" class="Bound">f</a> <a id="1142" class="Symbol">:</a> <a id="1144" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="1146" class="Symbol">→</a> <a id="1148" href="Relation.Binary.PropositionalEquality.Core.html#663" class="Generalizable">B</a><a id="1149" class="Symbol">)</a> <a id="1151" class="Symbol">{</a><a id="1152" href="Relation.Binary.PropositionalEquality.Core.html#1152" class="Bound">x</a> <a id="1154" href="Relation.Binary.PropositionalEquality.Core.html#1154" class="Bound">y</a><a id="1155" class="Symbol">}</a> <a id="1157" class="Symbol">→</a> <a id="1159" href="Relation.Binary.PropositionalEquality.Core.html#1152" class="Bound">x</a> <a id="1161" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1163" href="Relation.Binary.PropositionalEquality.Core.html#1154" class="Bound">y</a> <a id="1165" class="Symbol">→</a> <a id="1167" href="Relation.Binary.PropositionalEquality.Core.html#1140" class="Bound">f</a> <a id="1169" href="Relation.Binary.PropositionalEquality.Core.html#1152" class="Bound">x</a> <a id="1171" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1173" href="Relation.Binary.PropositionalEquality.Core.html#1140" class="Bound">f</a> <a id="1175" href="Relation.Binary.PropositionalEquality.Core.html#1154" class="Bound">y</a>
|
||
<a id="1177" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1182" href="Relation.Binary.PropositionalEquality.Core.html#1182" class="Bound">f</a> <a id="1184" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1189" class="Symbol">=</a> <a id="1191" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="cong′"></a><a id="1197" href="Relation.Binary.PropositionalEquality.Core.html#1197" class="Function">cong′</a> <a id="1203" class="Symbol">:</a> <a id="1205" class="Symbol">∀</a> <a id="1207" class="Symbol">{</a><a id="1208" href="Relation.Binary.PropositionalEquality.Core.html#1208" class="Bound">f</a> <a id="1210" class="Symbol">:</a> <a id="1212" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="1214" class="Symbol">→</a> <a id="1216" href="Relation.Binary.PropositionalEquality.Core.html#663" class="Generalizable">B</a><a id="1217" class="Symbol">}</a> <a id="1219" href="Relation.Binary.PropositionalEquality.Core.html#1219" class="Bound">x</a> <a id="1221" class="Symbol">→</a> <a id="1223" href="Relation.Binary.PropositionalEquality.Core.html#1208" class="Bound">f</a> <a id="1225" href="Relation.Binary.PropositionalEquality.Core.html#1219" class="Bound">x</a> <a id="1227" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1229" href="Relation.Binary.PropositionalEquality.Core.html#1208" class="Bound">f</a> <a id="1231" href="Relation.Binary.PropositionalEquality.Core.html#1219" class="Bound">x</a>
|
||
<a id="1233" href="Relation.Binary.PropositionalEquality.Core.html#1197" class="Function">cong′</a> <a id="1239" class="Symbol">_</a> <a id="1241" class="Symbol">=</a> <a id="1243" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="icong"></a><a id="1249" href="Relation.Binary.PropositionalEquality.Core.html#1249" class="Function">icong</a> <a id="1255" class="Symbol">:</a> <a id="1257" class="Symbol">∀</a> <a id="1259" class="Symbol">{</a><a id="1260" href="Relation.Binary.PropositionalEquality.Core.html#1260" class="Bound">f</a> <a id="1262" class="Symbol">:</a> <a id="1264" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="1266" class="Symbol">→</a> <a id="1268" href="Relation.Binary.PropositionalEquality.Core.html#663" class="Generalizable">B</a><a id="1269" class="Symbol">}</a> <a id="1271" class="Symbol">{</a><a id="1272" href="Relation.Binary.PropositionalEquality.Core.html#1272" class="Bound">x</a> <a id="1274" href="Relation.Binary.PropositionalEquality.Core.html#1274" class="Bound">y</a><a id="1275" class="Symbol">}</a> <a id="1277" class="Symbol">→</a> <a id="1279" href="Relation.Binary.PropositionalEquality.Core.html#1272" class="Bound">x</a> <a id="1281" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1283" href="Relation.Binary.PropositionalEquality.Core.html#1274" class="Bound">y</a> <a id="1285" class="Symbol">→</a> <a id="1287" href="Relation.Binary.PropositionalEquality.Core.html#1260" class="Bound">f</a> <a id="1289" href="Relation.Binary.PropositionalEquality.Core.html#1272" class="Bound">x</a> <a id="1291" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1293" href="Relation.Binary.PropositionalEquality.Core.html#1260" class="Bound">f</a> <a id="1295" href="Relation.Binary.PropositionalEquality.Core.html#1274" class="Bound">y</a>
|
||
<a id="1297" href="Relation.Binary.PropositionalEquality.Core.html#1249" class="Function">icong</a> <a id="1303" class="Symbol">=</a> <a id="1305" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1310" class="Symbol">_</a>
|
||
|
||
<a id="icong′"></a><a id="1313" href="Relation.Binary.PropositionalEquality.Core.html#1313" class="Function">icong′</a> <a id="1320" class="Symbol">:</a> <a id="1322" class="Symbol">∀</a> <a id="1324" class="Symbol">{</a><a id="1325" href="Relation.Binary.PropositionalEquality.Core.html#1325" class="Bound">f</a> <a id="1327" class="Symbol">:</a> <a id="1329" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="1331" class="Symbol">→</a> <a id="1333" href="Relation.Binary.PropositionalEquality.Core.html#663" class="Generalizable">B</a><a id="1334" class="Symbol">}</a> <a id="1336" href="Relation.Binary.PropositionalEquality.Core.html#1336" class="Bound">x</a> <a id="1338" class="Symbol">→</a> <a id="1340" href="Relation.Binary.PropositionalEquality.Core.html#1325" class="Bound">f</a> <a id="1342" href="Relation.Binary.PropositionalEquality.Core.html#1336" class="Bound">x</a> <a id="1344" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1346" href="Relation.Binary.PropositionalEquality.Core.html#1325" class="Bound">f</a> <a id="1348" href="Relation.Binary.PropositionalEquality.Core.html#1336" class="Bound">x</a>
|
||
<a id="1350" href="Relation.Binary.PropositionalEquality.Core.html#1313" class="Function">icong′</a> <a id="1357" class="Symbol">_</a> <a id="1359" class="Symbol">=</a> <a id="1361" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="cong₂"></a><a id="1367" href="Relation.Binary.PropositionalEquality.Core.html#1367" class="Function">cong₂</a> <a id="1373" class="Symbol">:</a> <a id="1375" class="Symbol">∀</a> <a id="1377" class="Symbol">(</a><a id="1378" href="Relation.Binary.PropositionalEquality.Core.html#1378" class="Bound">f</a> <a id="1380" class="Symbol">:</a> <a id="1382" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="1384" class="Symbol">→</a> <a id="1386" href="Relation.Binary.PropositionalEquality.Core.html#663" class="Generalizable">B</a> <a id="1388" class="Symbol">→</a> <a id="1390" href="Relation.Binary.PropositionalEquality.Core.html#665" class="Generalizable">C</a><a id="1391" class="Symbol">)</a> <a id="1393" class="Symbol">{</a><a id="1394" href="Relation.Binary.PropositionalEquality.Core.html#1394" class="Bound">x</a> <a id="1396" href="Relation.Binary.PropositionalEquality.Core.html#1396" class="Bound">y</a> <a id="1398" href="Relation.Binary.PropositionalEquality.Core.html#1398" class="Bound">u</a> <a id="1400" href="Relation.Binary.PropositionalEquality.Core.html#1400" class="Bound">v</a><a id="1401" class="Symbol">}</a> <a id="1403" class="Symbol">→</a> <a id="1405" href="Relation.Binary.PropositionalEquality.Core.html#1394" class="Bound">x</a> <a id="1407" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1409" href="Relation.Binary.PropositionalEquality.Core.html#1396" class="Bound">y</a> <a id="1411" class="Symbol">→</a> <a id="1413" href="Relation.Binary.PropositionalEquality.Core.html#1398" class="Bound">u</a> <a id="1415" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1417" href="Relation.Binary.PropositionalEquality.Core.html#1400" class="Bound">v</a> <a id="1419" class="Symbol">→</a> <a id="1421" href="Relation.Binary.PropositionalEquality.Core.html#1378" class="Bound">f</a> <a id="1423" href="Relation.Binary.PropositionalEquality.Core.html#1394" class="Bound">x</a> <a id="1425" href="Relation.Binary.PropositionalEquality.Core.html#1398" class="Bound">u</a> <a id="1427" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1429" href="Relation.Binary.PropositionalEquality.Core.html#1378" class="Bound">f</a> <a id="1431" href="Relation.Binary.PropositionalEquality.Core.html#1396" class="Bound">y</a> <a id="1433" href="Relation.Binary.PropositionalEquality.Core.html#1400" class="Bound">v</a>
|
||
<a id="1435" href="Relation.Binary.PropositionalEquality.Core.html#1367" class="Function">cong₂</a> <a id="1441" href="Relation.Binary.PropositionalEquality.Core.html#1441" class="Bound">f</a> <a id="1443" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1448" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1453" class="Symbol">=</a> <a id="1455" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="cong-app"></a><a id="1461" href="Relation.Binary.PropositionalEquality.Core.html#1461" class="Function">cong-app</a> <a id="1470" class="Symbol">:</a> <a id="1472" class="Symbol">∀</a> <a id="1474" class="Symbol">{</a><a id="1475" href="Relation.Binary.PropositionalEquality.Core.html#1475" class="Bound">A</a> <a id="1477" class="Symbol">:</a> <a id="1479" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1483" href="Relation.Binary.PropositionalEquality.Core.html#643" class="Generalizable">a</a><a id="1484" class="Symbol">}</a> <a id="1486" class="Symbol">{</a><a id="1487" href="Relation.Binary.PropositionalEquality.Core.html#1487" class="Bound">B</a> <a id="1489" class="Symbol">:</a> <a id="1491" href="Relation.Binary.PropositionalEquality.Core.html#1475" class="Bound">A</a> <a id="1493" class="Symbol">→</a> <a id="1495" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1499" href="Relation.Binary.PropositionalEquality.Core.html#645" class="Generalizable">b</a><a id="1500" class="Symbol">}</a> <a id="1502" class="Symbol">{</a><a id="1503" href="Relation.Binary.PropositionalEquality.Core.html#1503" class="Bound">f</a> <a id="1505" href="Relation.Binary.PropositionalEquality.Core.html#1505" class="Bound">g</a> <a id="1507" class="Symbol">:</a> <a id="1509" class="Symbol">(</a><a id="1510" href="Relation.Binary.PropositionalEquality.Core.html#1510" class="Bound">x</a> <a id="1512" class="Symbol">:</a> <a id="1514" href="Relation.Binary.PropositionalEquality.Core.html#1475" class="Bound">A</a><a id="1515" class="Symbol">)</a> <a id="1517" class="Symbol">→</a> <a id="1519" href="Relation.Binary.PropositionalEquality.Core.html#1487" class="Bound">B</a> <a id="1521" href="Relation.Binary.PropositionalEquality.Core.html#1510" class="Bound">x</a><a id="1522" class="Symbol">}</a> <a id="1524" class="Symbol">→</a>
|
||
<a id="1537" href="Relation.Binary.PropositionalEquality.Core.html#1503" class="Bound">f</a> <a id="1539" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1541" href="Relation.Binary.PropositionalEquality.Core.html#1505" class="Bound">g</a> <a id="1543" class="Symbol">→</a> <a id="1545" class="Symbol">(</a><a id="1546" href="Relation.Binary.PropositionalEquality.Core.html#1546" class="Bound">x</a> <a id="1548" class="Symbol">:</a> <a id="1550" href="Relation.Binary.PropositionalEquality.Core.html#1475" class="Bound">A</a><a id="1551" class="Symbol">)</a> <a id="1553" class="Symbol">→</a> <a id="1555" href="Relation.Binary.PropositionalEquality.Core.html#1503" class="Bound">f</a> <a id="1557" href="Relation.Binary.PropositionalEquality.Core.html#1546" class="Bound">x</a> <a id="1559" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1561" href="Relation.Binary.PropositionalEquality.Core.html#1505" class="Bound">g</a> <a id="1563" href="Relation.Binary.PropositionalEquality.Core.html#1546" class="Bound">x</a>
|
||
<a id="1565" href="Relation.Binary.PropositionalEquality.Core.html#1461" class="Function">cong-app</a> <a id="1574" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1579" href="Relation.Binary.PropositionalEquality.Core.html#1579" class="Bound">x</a> <a id="1581" class="Symbol">=</a> <a id="1583" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="1589" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1662" class="Comment">-- Properties of _≡_</a>
|
||
|
||
<a id="sym"></a><a id="1684" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="1688" class="Symbol">:</a> <a id="1690" href="Relation.Binary.Definitions.html#1498" class="Function">Symmetric</a> <a id="1700" class="Symbol">{</a><a id="1701" class="Argument">A</a> <a id="1703" class="Symbol">=</a> <a id="1705" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a><a id="1706" class="Symbol">}</a> <a id="1708" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="1712" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="1716" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1721" class="Symbol">=</a> <a id="1723" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="trans"></a><a id="1729" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1735" class="Symbol">:</a> <a id="1737" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="1748" class="Symbol">{</a><a id="1749" class="Argument">A</a> <a id="1751" class="Symbol">=</a> <a id="1753" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a><a id="1754" class="Symbol">}</a> <a id="1756" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="1760" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="1766" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1771" href="Relation.Binary.PropositionalEquality.Core.html#1771" class="Bound">eq</a> <a id="1774" class="Symbol">=</a> <a id="1776" href="Relation.Binary.PropositionalEquality.Core.html#1771" class="Bound">eq</a>
|
||
|
||
<a id="subst"></a><a id="1780" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="1786" class="Symbol">:</a> <a id="1788" href="Relation.Binary.Definitions.html#4369" class="Function">Substitutive</a> <a id="1801" class="Symbol">{</a><a id="1802" class="Argument">A</a> <a id="1804" class="Symbol">=</a> <a id="1806" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a><a id="1807" class="Symbol">}</a> <a id="1809" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="1813" href="Relation.Binary.PropositionalEquality.Core.html#647" class="Generalizable">ℓ</a>
|
||
<a id="1815" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="1821" href="Relation.Binary.PropositionalEquality.Core.html#1821" class="Bound">P</a> <a id="1823" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1828" href="Relation.Binary.PropositionalEquality.Core.html#1828" class="Bound">p</a> <a id="1830" class="Symbol">=</a> <a id="1832" href="Relation.Binary.PropositionalEquality.Core.html#1828" class="Bound">p</a>
|
||
|
||
<a id="subst₂"></a><a id="1835" href="Relation.Binary.PropositionalEquality.Core.html#1835" class="Function">subst₂</a> <a id="1842" class="Symbol">:</a> <a id="1844" class="Symbol">∀</a> <a id="1846" class="Symbol">(</a><a id="1847" href="Relation.Binary.PropositionalEquality.Core.html#1847" class="Bound Operator">_∼_</a> <a id="1851" class="Symbol">:</a> <a id="1853" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1857" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="1859" href="Relation.Binary.PropositionalEquality.Core.html#663" class="Generalizable">B</a> <a id="1861" href="Relation.Binary.PropositionalEquality.Core.html#647" class="Generalizable">ℓ</a><a id="1862" class="Symbol">)</a> <a id="1864" class="Symbol">{</a><a id="1865" href="Relation.Binary.PropositionalEquality.Core.html#1865" class="Bound">x</a> <a id="1867" href="Relation.Binary.PropositionalEquality.Core.html#1867" class="Bound">y</a> <a id="1869" href="Relation.Binary.PropositionalEquality.Core.html#1869" class="Bound">u</a> <a id="1871" href="Relation.Binary.PropositionalEquality.Core.html#1871" class="Bound">v</a><a id="1872" class="Symbol">}</a> <a id="1874" class="Symbol">→</a> <a id="1876" href="Relation.Binary.PropositionalEquality.Core.html#1865" class="Bound">x</a> <a id="1878" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1880" href="Relation.Binary.PropositionalEquality.Core.html#1867" class="Bound">y</a> <a id="1882" class="Symbol">→</a> <a id="1884" href="Relation.Binary.PropositionalEquality.Core.html#1869" class="Bound">u</a> <a id="1886" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1888" href="Relation.Binary.PropositionalEquality.Core.html#1871" class="Bound">v</a> <a id="1890" class="Symbol">→</a> <a id="1892" href="Relation.Binary.PropositionalEquality.Core.html#1865" class="Bound">x</a> <a id="1894" href="Relation.Binary.PropositionalEquality.Core.html#1847" class="Bound Operator">∼</a> <a id="1896" href="Relation.Binary.PropositionalEquality.Core.html#1869" class="Bound">u</a> <a id="1898" class="Symbol">→</a> <a id="1900" href="Relation.Binary.PropositionalEquality.Core.html#1867" class="Bound">y</a> <a id="1902" href="Relation.Binary.PropositionalEquality.Core.html#1847" class="Bound Operator">∼</a> <a id="1904" href="Relation.Binary.PropositionalEquality.Core.html#1871" class="Bound">v</a>
|
||
<a id="1906" href="Relation.Binary.PropositionalEquality.Core.html#1835" class="Function">subst₂</a> <a id="1913" class="Symbol">_</a> <a id="1915" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1920" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1925" href="Relation.Binary.PropositionalEquality.Core.html#1925" class="Bound">p</a> <a id="1927" class="Symbol">=</a> <a id="1929" href="Relation.Binary.PropositionalEquality.Core.html#1925" class="Bound">p</a>
|
||
|
||
<a id="resp"></a><a id="1932" href="Relation.Binary.PropositionalEquality.Core.html#1932" class="Function">resp</a> <a id="1937" class="Symbol">:</a> <a id="1939" class="Symbol">∀</a> <a id="1941" class="Symbol">(</a><a id="1942" href="Relation.Binary.PropositionalEquality.Core.html#1942" class="Bound">P</a> <a id="1944" class="Symbol">:</a> <a id="1946" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="1948" class="Symbol">→</a> <a id="1950" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1954" href="Relation.Binary.PropositionalEquality.Core.html#647" class="Generalizable">ℓ</a><a id="1955" class="Symbol">)</a> <a id="1957" class="Symbol">→</a> <a id="1959" href="Relation.Binary.PropositionalEquality.Core.html#1942" class="Bound">P</a> <a id="1961" href="Relation.Binary.Definitions.html#3593" class="Function Operator">Respects</a> <a id="1970" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="1974" href="Relation.Binary.PropositionalEquality.Core.html#1932" class="Function">resp</a> <a id="1979" href="Relation.Binary.PropositionalEquality.Core.html#1979" class="Bound">P</a> <a id="1981" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1986" href="Relation.Binary.PropositionalEquality.Core.html#1986" class="Bound">p</a> <a id="1988" class="Symbol">=</a> <a id="1990" href="Relation.Binary.PropositionalEquality.Core.html#1986" class="Bound">p</a>
|
||
|
||
<a id="respˡ"></a><a id="1993" href="Relation.Binary.PropositionalEquality.Core.html#1993" class="Function">respˡ</a> <a id="1999" class="Symbol">:</a> <a id="2001" class="Symbol">∀</a> <a id="2003" class="Symbol">(</a><a id="2004" href="Relation.Binary.PropositionalEquality.Core.html#2004" class="Bound">∼</a> <a id="2006" class="Symbol">:</a> <a id="2008" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2012" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="2014" href="Relation.Binary.PropositionalEquality.Core.html#647" class="Generalizable">ℓ</a><a id="2015" class="Symbol">)</a> <a id="2017" class="Symbol">→</a> <a id="2019" href="Relation.Binary.PropositionalEquality.Core.html#2004" class="Bound">∼</a> <a id="2021" href="Relation.Binary.Definitions.html#3914" class="Function Operator">Respectsˡ</a> <a id="2031" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="2035" href="Relation.Binary.PropositionalEquality.Core.html#1993" class="Function">respˡ</a> <a id="2041" href="Relation.Binary.PropositionalEquality.Core.html#2041" class="Bound Operator">_∼_</a> <a id="2045" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2050" href="Relation.Binary.PropositionalEquality.Core.html#2050" class="Bound">x∼y</a> <a id="2054" class="Symbol">=</a> <a id="2056" href="Relation.Binary.PropositionalEquality.Core.html#2050" class="Bound">x∼y</a>
|
||
|
||
<a id="respʳ"></a><a id="2061" href="Relation.Binary.PropositionalEquality.Core.html#2061" class="Function">respʳ</a> <a id="2067" class="Symbol">:</a> <a id="2069" class="Symbol">∀</a> <a id="2071" class="Symbol">(</a><a id="2072" href="Relation.Binary.PropositionalEquality.Core.html#2072" class="Bound">∼</a> <a id="2074" class="Symbol">:</a> <a id="2076" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2080" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="2082" href="Relation.Binary.PropositionalEquality.Core.html#647" class="Generalizable">ℓ</a><a id="2083" class="Symbol">)</a> <a id="2085" class="Symbol">→</a> <a id="2087" href="Relation.Binary.PropositionalEquality.Core.html#2072" class="Bound">∼</a> <a id="2089" href="Relation.Binary.Definitions.html#3749" class="Function Operator">Respectsʳ</a> <a id="2099" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="2103" href="Relation.Binary.PropositionalEquality.Core.html#2061" class="Function">respʳ</a> <a id="2109" href="Relation.Binary.PropositionalEquality.Core.html#2109" class="Bound Operator">_∼_</a> <a id="2113" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2118" href="Relation.Binary.PropositionalEquality.Core.html#2118" class="Bound">x∼y</a> <a id="2122" class="Symbol">=</a> <a id="2124" href="Relation.Binary.PropositionalEquality.Core.html#2118" class="Bound">x∼y</a>
|
||
|
||
<a id="resp₂"></a><a id="2129" href="Relation.Binary.PropositionalEquality.Core.html#2129" class="Function">resp₂</a> <a id="2135" class="Symbol">:</a> <a id="2137" class="Symbol">∀</a> <a id="2139" class="Symbol">(</a><a id="2140" href="Relation.Binary.PropositionalEquality.Core.html#2140" class="Bound">∼</a> <a id="2142" class="Symbol">:</a> <a id="2144" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2148" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a> <a id="2150" href="Relation.Binary.PropositionalEquality.Core.html#647" class="Generalizable">ℓ</a><a id="2151" class="Symbol">)</a> <a id="2153" class="Symbol">→</a> <a id="2155" href="Relation.Binary.PropositionalEquality.Core.html#2140" class="Bound">∼</a> <a id="2157" href="Relation.Binary.Definitions.html#4077" class="Function Operator">Respects₂</a> <a id="2167" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
<a id="2171" href="Relation.Binary.PropositionalEquality.Core.html#2129" class="Function">resp₂</a> <a id="2177" href="Relation.Binary.PropositionalEquality.Core.html#2177" class="Bound Operator">_∼_</a> <a id="2181" class="Symbol">=</a> <a id="2183" href="Relation.Binary.PropositionalEquality.Core.html#2061" class="Function">respʳ</a> <a id="2189" href="Relation.Binary.PropositionalEquality.Core.html#2177" class="Bound Operator">_∼_</a> <a id="2193" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="2195" href="Relation.Binary.PropositionalEquality.Core.html#1993" class="Function">respˡ</a> <a id="2201" href="Relation.Binary.PropositionalEquality.Core.html#2177" class="Bound Operator">_∼_</a>
|
||
|
||
<a id="2206" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="2279" class="Comment">-- Properties of _≢_</a>
|
||
|
||
<a id="≢-sym"></a><a id="2301" href="Relation.Binary.PropositionalEquality.Core.html#2301" class="Function">≢-sym</a> <a id="2307" class="Symbol">:</a> <a id="2309" href="Relation.Binary.Definitions.html#1498" class="Function">Symmetric</a> <a id="2319" class="Symbol">{</a><a id="2320" class="Argument">A</a> <a id="2322" class="Symbol">=</a> <a id="2324" href="Relation.Binary.PropositionalEquality.Core.html#661" class="Generalizable">A</a><a id="2325" class="Symbol">}</a> <a id="2327" href="Relation.Binary.PropositionalEquality.Core.html#830" class="Function Operator">_≢_</a>
|
||
<a id="2331" href="Relation.Binary.PropositionalEquality.Core.html#2301" class="Function">≢-sym</a> <a id="2337" href="Relation.Binary.PropositionalEquality.Core.html#2337" class="Bound">x≢y</a> <a id="2341" class="Symbol">=</a> <a id="2344" href="Relation.Binary.PropositionalEquality.Core.html#2337" class="Bound">x≢y</a> <a id="2348" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="2350" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a>
|
||
|
||
<a id="2355" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="2428" class="Comment">-- Convenient syntax for equational reasoning</a>
|
||
|
||
<a id="2475" class="Comment">-- This is a special instance of `Relation.Binary.Reasoning.Setoid`.</a>
|
||
<a id="2544" class="Comment">-- Rather than instantiating the latter with (setoid A), we reimplement</a>
|
||
<a id="2616" class="Comment">-- equation chains from scratch since then goals are printed much more</a>
|
||
<a id="2687" class="Comment">-- readably.</a>
|
||
|
||
<a id="2701" class="Keyword">module</a> <a id="≡-Reasoning"></a><a id="2708" href="Relation.Binary.PropositionalEquality.Core.html#2708" class="Module">≡-Reasoning</a> <a id="2720" class="Symbol">{</a><a id="2721" href="Relation.Binary.PropositionalEquality.Core.html#2721" class="Bound">A</a> <a id="2723" class="Symbol">:</a> <a id="2725" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2729" href="Relation.Binary.PropositionalEquality.Core.html#643" class="Generalizable">a</a><a id="2730" class="Symbol">}</a> <a id="2732" class="Keyword">where</a>
|
||
|
||
<a id="2741" class="Keyword">infix</a> <a id="2748" class="Number">3</a> <a id="2750" href="Relation.Binary.PropositionalEquality.Core.html#3105" class="Function Operator">_∎</a>
|
||
<a id="2755" class="Keyword">infixr</a> <a id="2762" class="Number">2</a> <a id="2764" href="Relation.Binary.PropositionalEquality.Core.html#2864" class="Function Operator">_≡⟨⟩_</a> <a id="2770" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">step-≡</a> <a id="2777" href="Relation.Binary.PropositionalEquality.Core.html#3010" class="Function">step-≡˘</a>
|
||
<a id="2787" class="Keyword">infix</a> <a id="2794" class="Number">1</a> <a id="2796" href="Relation.Binary.PropositionalEquality.Core.html#2806" class="Function Operator">begin_</a>
|
||
|
||
<a id="≡-Reasoning.begin_"></a><a id="2806" href="Relation.Binary.PropositionalEquality.Core.html#2806" class="Function Operator">begin_</a> <a id="2813" class="Symbol">:</a> <a id="2815" class="Symbol">∀{</a><a id="2817" href="Relation.Binary.PropositionalEquality.Core.html#2817" class="Bound">x</a> <a id="2819" href="Relation.Binary.PropositionalEquality.Core.html#2819" class="Bound">y</a> <a id="2821" class="Symbol">:</a> <a id="2823" href="Relation.Binary.PropositionalEquality.Core.html#2721" class="Bound">A</a><a id="2824" class="Symbol">}</a> <a id="2826" class="Symbol">→</a> <a id="2828" href="Relation.Binary.PropositionalEquality.Core.html#2817" class="Bound">x</a> <a id="2830" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2832" href="Relation.Binary.PropositionalEquality.Core.html#2819" class="Bound">y</a> <a id="2834" class="Symbol">→</a> <a id="2836" href="Relation.Binary.PropositionalEquality.Core.html#2817" class="Bound">x</a> <a id="2838" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2840" href="Relation.Binary.PropositionalEquality.Core.html#2819" class="Bound">y</a>
|
||
<a id="2844" href="Relation.Binary.PropositionalEquality.Core.html#2806" class="Function Operator">begin_</a> <a id="2851" href="Relation.Binary.PropositionalEquality.Core.html#2851" class="Bound">x≡y</a> <a id="2855" class="Symbol">=</a> <a id="2857" href="Relation.Binary.PropositionalEquality.Core.html#2851" class="Bound">x≡y</a>
|
||
|
||
<a id="≡-Reasoning._≡⟨⟩_"></a><a id="2864" href="Relation.Binary.PropositionalEquality.Core.html#2864" class="Function Operator">_≡⟨⟩_</a> <a id="2870" class="Symbol">:</a> <a id="2872" class="Symbol">∀</a> <a id="2874" class="Symbol">(</a><a id="2875" href="Relation.Binary.PropositionalEquality.Core.html#2875" class="Bound">x</a> <a id="2877" class="Symbol">{</a><a id="2878" href="Relation.Binary.PropositionalEquality.Core.html#2878" class="Bound">y</a><a id="2879" class="Symbol">}</a> <a id="2881" class="Symbol">:</a> <a id="2883" href="Relation.Binary.PropositionalEquality.Core.html#2721" class="Bound">A</a><a id="2884" class="Symbol">)</a> <a id="2886" class="Symbol">→</a> <a id="2888" href="Relation.Binary.PropositionalEquality.Core.html#2875" class="Bound">x</a> <a id="2890" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2892" href="Relation.Binary.PropositionalEquality.Core.html#2878" class="Bound">y</a> <a id="2894" class="Symbol">→</a> <a id="2896" href="Relation.Binary.PropositionalEquality.Core.html#2875" class="Bound">x</a> <a id="2898" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2900" href="Relation.Binary.PropositionalEquality.Core.html#2878" class="Bound">y</a>
|
||
<a id="2904" class="Symbol">_</a> <a id="2906" href="Relation.Binary.PropositionalEquality.Core.html#2864" class="Function Operator">≡⟨⟩</a> <a id="2910" href="Relation.Binary.PropositionalEquality.Core.html#2910" class="Bound">x≡y</a> <a id="2914" class="Symbol">=</a> <a id="2916" href="Relation.Binary.PropositionalEquality.Core.html#2910" class="Bound">x≡y</a>
|
||
|
||
<a id="≡-Reasoning.step-≡"></a><a id="2923" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">step-≡</a> <a id="2930" class="Symbol">:</a> <a id="2932" class="Symbol">∀</a> <a id="2934" class="Symbol">(</a><a id="2935" href="Relation.Binary.PropositionalEquality.Core.html#2935" class="Bound">x</a> <a id="2937" class="Symbol">{</a><a id="2938" href="Relation.Binary.PropositionalEquality.Core.html#2938" class="Bound">y</a> <a id="2940" href="Relation.Binary.PropositionalEquality.Core.html#2940" class="Bound">z</a><a id="2941" class="Symbol">}</a> <a id="2943" class="Symbol">:</a> <a id="2945" href="Relation.Binary.PropositionalEquality.Core.html#2721" class="Bound">A</a><a id="2946" class="Symbol">)</a> <a id="2948" class="Symbol">→</a> <a id="2950" href="Relation.Binary.PropositionalEquality.Core.html#2938" class="Bound">y</a> <a id="2952" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2954" href="Relation.Binary.PropositionalEquality.Core.html#2940" class="Bound">z</a> <a id="2956" class="Symbol">→</a> <a id="2958" href="Relation.Binary.PropositionalEquality.Core.html#2935" class="Bound">x</a> <a id="2960" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2962" href="Relation.Binary.PropositionalEquality.Core.html#2938" class="Bound">y</a> <a id="2964" class="Symbol">→</a> <a id="2966" href="Relation.Binary.PropositionalEquality.Core.html#2935" class="Bound">x</a> <a id="2968" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2970" href="Relation.Binary.PropositionalEquality.Core.html#2940" class="Bound">z</a>
|
||
<a id="2974" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">step-≡</a> <a id="2981" class="Symbol">_</a> <a id="2983" href="Relation.Binary.PropositionalEquality.Core.html#2983" class="Bound">y≡z</a> <a id="2987" href="Relation.Binary.PropositionalEquality.Core.html#2987" class="Bound">x≡y</a> <a id="2991" class="Symbol">=</a> <a id="2993" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="2999" href="Relation.Binary.PropositionalEquality.Core.html#2987" class="Bound">x≡y</a> <a id="3003" href="Relation.Binary.PropositionalEquality.Core.html#2983" class="Bound">y≡z</a>
|
||
|
||
<a id="≡-Reasoning.step-≡˘"></a><a id="3010" href="Relation.Binary.PropositionalEquality.Core.html#3010" class="Function">step-≡˘</a> <a id="3018" class="Symbol">:</a> <a id="3020" class="Symbol">∀</a> <a id="3022" class="Symbol">(</a><a id="3023" href="Relation.Binary.PropositionalEquality.Core.html#3023" class="Bound">x</a> <a id="3025" class="Symbol">{</a><a id="3026" href="Relation.Binary.PropositionalEquality.Core.html#3026" class="Bound">y</a> <a id="3028" href="Relation.Binary.PropositionalEquality.Core.html#3028" class="Bound">z</a><a id="3029" class="Symbol">}</a> <a id="3031" class="Symbol">:</a> <a id="3033" href="Relation.Binary.PropositionalEquality.Core.html#2721" class="Bound">A</a><a id="3034" class="Symbol">)</a> <a id="3036" class="Symbol">→</a> <a id="3038" href="Relation.Binary.PropositionalEquality.Core.html#3026" class="Bound">y</a> <a id="3040" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3042" href="Relation.Binary.PropositionalEquality.Core.html#3028" class="Bound">z</a> <a id="3044" class="Symbol">→</a> <a id="3046" href="Relation.Binary.PropositionalEquality.Core.html#3026" class="Bound">y</a> <a id="3048" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3050" href="Relation.Binary.PropositionalEquality.Core.html#3023" class="Bound">x</a> <a id="3052" class="Symbol">→</a> <a id="3054" href="Relation.Binary.PropositionalEquality.Core.html#3023" class="Bound">x</a> <a id="3056" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3058" href="Relation.Binary.PropositionalEquality.Core.html#3028" class="Bound">z</a>
|
||
<a id="3062" href="Relation.Binary.PropositionalEquality.Core.html#3010" class="Function">step-≡˘</a> <a id="3070" class="Symbol">_</a> <a id="3072" href="Relation.Binary.PropositionalEquality.Core.html#3072" class="Bound">y≡z</a> <a id="3076" href="Relation.Binary.PropositionalEquality.Core.html#3076" class="Bound">y≡x</a> <a id="3080" class="Symbol">=</a> <a id="3082" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3088" class="Symbol">(</a><a id="3089" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3093" href="Relation.Binary.PropositionalEquality.Core.html#3076" class="Bound">y≡x</a><a id="3096" class="Symbol">)</a> <a id="3098" href="Relation.Binary.PropositionalEquality.Core.html#3072" class="Bound">y≡z</a>
|
||
|
||
<a id="≡-Reasoning._∎"></a><a id="3105" href="Relation.Binary.PropositionalEquality.Core.html#3105" class="Function Operator">_∎</a> <a id="3108" class="Symbol">:</a> <a id="3110" class="Symbol">∀</a> <a id="3112" class="Symbol">(</a><a id="3113" href="Relation.Binary.PropositionalEquality.Core.html#3113" class="Bound">x</a> <a id="3115" class="Symbol">:</a> <a id="3117" href="Relation.Binary.PropositionalEquality.Core.html#2721" class="Bound">A</a><a id="3118" class="Symbol">)</a> <a id="3120" class="Symbol">→</a> <a id="3122" href="Relation.Binary.PropositionalEquality.Core.html#3113" class="Bound">x</a> <a id="3124" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3126" href="Relation.Binary.PropositionalEquality.Core.html#3113" class="Bound">x</a>
|
||
<a id="3130" href="Relation.Binary.PropositionalEquality.Core.html#3105" class="Function Operator">_∎</a> <a id="3133" class="Symbol">_</a> <a id="3135" class="Symbol">=</a> <a id="3137" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="3145" class="Keyword">syntax</a> <a id="3152" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">step-≡</a> <a id="3160" class="Bound">x</a> <a id="3162" class="Bound">y≡z</a> <a id="3166" class="Bound">x≡y</a> <a id="3170" class="Symbol">=</a> <a id="3172" class="Bound">x</a> <a id="3174" class="Function">≡⟨</a> <a id="3178" class="Bound">x≡y</a> <a id="3182" class="Function">⟩</a> <a id="3184" class="Bound">y≡z</a>
|
||
<a id="3190" class="Keyword">syntax</a> <a id="3197" href="Relation.Binary.PropositionalEquality.Core.html#3010" class="Function">step-≡˘</a> <a id="3205" class="Bound">x</a> <a id="3207" class="Bound">y≡z</a> <a id="3211" class="Bound">y≡x</a> <a id="3215" class="Symbol">=</a> <a id="3217" class="Bound">x</a> <a id="3219" class="Function">≡˘⟨</a> <a id="3223" class="Bound">y≡x</a> <a id="3227" class="Function">⟩</a> <a id="3229" class="Bound">y≡z</a>
|
||
</pre></body></html> |