rachel/rachel.cafe
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
94f3f88067
rachel.cafe/misc/Relation.Binary.PropositionalEquality.html

148 lines
55 KiB
HTML
Raw Normal View History

add some agda stuff
2022-06-23 22:12:24 +02:00
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Relation.Binary.PropositionalEquality</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 (intensional) equality</a>
<a id="146" class="Comment">------------------------------------------------------------------------</a>
<a id="220" class="Symbol">{-#</a> <a id="224" class="Keyword">OPTIONS</a> <a id="232" class="Pragma">--without-K</a> <a id="244" class="Pragma">--safe</a> <a id="251" class="Symbol">#-}</a>
<a id="256" class="Keyword">module</a> <a id="263" href="Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="301" class="Keyword">where</a>
<a id="308" class="Keyword">import</a> <a id="315" href="Axiom.Extensionality.Propositional.html" class="Module">Axiom.Extensionality.Propositional</a> <a id="350" class="Symbol">as</a> <a id="353" class="Module">Ext</a>
<a id="357" class="Keyword">open</a> <a id="362" class="Keyword">import</a> <a id="369" href="Axiom.UniquenessOfIdentityProofs.html" class="Module">Axiom.UniquenessOfIdentityProofs</a>
<a id="402" class="Keyword">open</a> <a id="407" class="Keyword">import</a> <a id="414" href="Function.Base.html" class="Module">Function.Base</a> <a id="428" class="Keyword">using</a> <a id="434" class="Symbol">(</a><a id="435" href="Function.Base.html#615" class="Function">id</a><a id="437" class="Symbol">;</a> <a id="439" href="Function.Base.html#1031" class="Function Operator">_∘_</a><a id="442" class="Symbol">)</a>
<a id="444" class="Keyword">open</a> <a id="449" class="Keyword">import</a> <a id="456" href="Function.Equality.html" class="Module">Function.Equality</a> <a id="474" class="Keyword">using</a> <a id="480" class="Symbol">(</a><a id="481" href="Function.Equality.html#889" class="Record">Π</a><a id="482" class="Symbol">;</a> <a id="484" href="Function.Equality.html#1218" class="Function Operator">_⟶_</a><a id="487" class="Symbol">;</a> <a id="489" href="Function.Equality.html#2978" class="Function">≡-setoid</a><a id="497" class="Symbol">)</a>
<a id="499" class="Keyword">open</a> <a id="504" class="Keyword">import</a> <a id="511" href="Level.html" class="Module">Level</a> <a id="517" class="Keyword">using</a> <a id="523" class="Symbol">(</a><a id="524" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="529" class="Symbol">;</a> <a id="531" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="534" class="Symbol">)</a>
<a id="536" class="Keyword">open</a> <a id="541" class="Keyword">import</a> <a id="548" href="Data.Product.html" class="Module">Data.Product</a> <a id="561" class="Keyword">using</a> <a id="567" class="Symbol">(</a><a id="568" href="Data.Product.html#1369" class="Function">∃</a><a id="569" class="Symbol">)</a>
<a id="572" class="Keyword">open</a> <a id="577" class="Keyword">import</a> <a id="584" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="601" class="Keyword">using</a> <a id="607" class="Symbol">(</a><a id="608" href="Relation.Nullary.html#1648" class="InductiveConstructor">yes</a> <a id="612" class="Symbol">;</a> <a id="614" href="Relation.Nullary.html#1685" class="InductiveConstructor">no</a><a id="616" class="Symbol">)</a>
<a id="618" class="Keyword">open</a> <a id="623" class="Keyword">import</a> <a id="630" href="Relation.Nullary.Decidable.Core.html" class="Module">Relation.Nullary.Decidable.Core</a>
<a id="662" class="Keyword">open</a> <a id="667" class="Keyword">import</a> <a id="674" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="690" class="Keyword">open</a> <a id="695" class="Keyword">import</a> <a id="702" href="Relation.Binary.Indexed.Heterogeneous.html" class="Module">Relation.Binary.Indexed.Heterogeneous</a>
<a id="742" class="Keyword">using</a> <a id="748" class="Symbol">(</a><a id="749" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#789" class="Record">IndexedSetoid</a><a id="762" class="Symbol">)</a>
<a id="764" class="Keyword">import</a> <a id="771" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html" class="Module">Relation.Binary.Indexed.Heterogeneous.Construct.Trivial</a>
<a id="829" class="Symbol">as</a> <a id="832" class="Module">Trivial</a>
<a id="841" class="Keyword">private</a>
<a id="851" class="Keyword">variable</a>
<a id="864" href="Relation.Binary.PropositionalEquality.html#864" class="Generalizable">a</a> <a id="866" href="Relation.Binary.PropositionalEquality.html#866" class="Generalizable">b</a> <a id="868" href="Relation.Binary.PropositionalEquality.html#868" class="Generalizable">c</a> <a id="870" href="Relation.Binary.PropositionalEquality.html#870" class="Generalizable">ℓ</a> <a id="872" href="Relation.Binary.PropositionalEquality.html#872" class="Generalizable">p</a> <a id="874" class="Symbol">:</a> <a id="876" href="Agda.Primitive.html#597" class="Postulate">Level</a>
<a id="886" href="Relation.Binary.PropositionalEquality.html#886" class="Generalizable">A</a> <a id="888" class="Symbol">:</a> <a id="890" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="894" href="Relation.Binary.PropositionalEquality.html#864" class="Generalizable">a</a>
<a id="900" href="Relation.Binary.PropositionalEquality.html#900" class="Generalizable">B</a> <a id="902" class="Symbol">:</a> <a id="904" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="908" href="Relation.Binary.PropositionalEquality.html#866" class="Generalizable">b</a>
<a id="914" href="Relation.Binary.PropositionalEquality.html#914" class="Generalizable">C</a> <a id="916" class="Symbol">:</a> <a id="918" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="922" href="Relation.Binary.PropositionalEquality.html#868" class="Generalizable">c</a>
<a id="925" class="Comment">------------------------------------------------------------------------</a>
<a id="998" class="Comment">-- Re-export contents modules that make up the parts</a>
<a id="1052" class="Keyword">open</a> <a id="1057" class="Keyword">import</a> <a id="1064" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a> <a id="1107" class="Keyword">public</a>
<a id="1114" class="Keyword">open</a> <a id="1119" class="Keyword">import</a> <a id="1126" href="Relation.Binary.PropositionalEquality.Properties.html" class="Module">Relation.Binary.PropositionalEquality.Properties</a> <a id="1175" class="Keyword">public</a>
<a id="1182" class="Keyword">open</a> <a id="1187" class="Keyword">import</a> <a id="1194" href="Relation.Binary.PropositionalEquality.Algebra.html" class="Module">Relation.Binary.PropositionalEquality.Algebra</a> <a id="1240" class="Keyword">public</a>
<a id="1248" class="Comment">------------------------------------------------------------------------</a>
<a id="1321" class="Comment">-- Pointwise equality</a>
<a id="1344" class="Keyword">infix</a> <a id="1350" class="Number">4</a> <a id="1352" href="Relation.Binary.PropositionalEquality.html#1471" class="Function Operator">_≗_</a>
<a id="_→-setoid_"></a><a id="1357" href="Relation.Binary.PropositionalEquality.html#1357" class="Function Operator">_→-setoid_</a> <a id="1368" class="Symbol">:</a> <a id="1370" class="Symbol">∀</a> <a id="1372" class="Symbol">(</a><a id="1373" href="Relation.Binary.PropositionalEquality.html#1373" class="Bound">A</a> <a id="1375" class="Symbol">:</a> <a id="1377" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1381" href="Relation.Binary.PropositionalEquality.html#864" class="Generalizable">a</a><a id="1382" class="Symbol">)</a> <a id="1384" class="Symbol">(</a><a id="1385" href="Relation.Binary.PropositionalEquality.html#1385" class="Bound">B</a> <a id="1387" class="Symbol">:</a> <a id="1389" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1393" href="Relation.Binary.PropositionalEquality.html#866" class="Generalizable">b</a><a id="1394" class="Symbol">)</a> <a id="1396" class="Symbol">→</a> <a id="1398" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1405" class="Symbol">_</a> <a id="1407" class="Symbol">_</a>
<a id="1409" href="Relation.Binary.PropositionalEquality.html#1409" class="Bound">A</a> <a id="1411" href="Relation.Binary.PropositionalEquality.html#1357" class="Function Operator">→-setoid</a> <a id="1420" href="Relation.Binary.PropositionalEquality.html#1420" class="Bound">B</a> <a id="1422" class="Symbol">=</a> <a id="1424" href="Function.Equality.html#2978" class="Function">≡-setoid</a> <a id="1433" href="Relation.Binary.PropositionalEquality.html#1409" class="Bound">A</a> <a id="1435" class="Symbol">(</a><a id="1436" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1370" class="Function">Trivial.indexedSetoid</a> <a id="1458" class="Symbol">(</a><a id="1459" href="Relation.Binary.PropositionalEquality.Properties.html#3972" class="Function">setoid</a> <a id="1466" href="Relation.Binary.PropositionalEquality.html#1420" class="Bound">B</a><a id="1467" class="Symbol">))</a>
<a id="_≗_"></a><a id="1471" href="Relation.Binary.PropositionalEquality.html#1471" class="Function Operator">_≗_</a> <a id="1475" class="Symbol">:</a> <a id="1477" class="Symbol">(</a><a id="1478" href="Relation.Binary.PropositionalEquality.html#1478" class="Bound">f</a> <a id="1480" href="Relation.Binary.PropositionalEquality.html#1480" class="Bound">g</a> <a id="1482" class="Symbol">:</a> <a id="1484" href="Relation.Binary.PropositionalEquality.html#886" class="Generalizable">A</a> <a id="1486" class="Symbol">→</a> <a id="1488" href="Relation.Binary.PropositionalEquality.html#900" class="Generalizable">B</a><a id="1489" class="Symbol">)</a> <a id="1491" class="Symbol">→</a> <a id="1493" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1497" class="Symbol">_</a>
<a id="1499" href="Relation.Binary.PropositionalEquality.html#1471" class="Function Operator">_≗_</a> <a id="1503" class="Symbol">{</a><a id="1504" class="Argument">A</a> <a id="1506" class="Symbol">=</a> <a id="1508" href="Relation.Binary.PropositionalEquality.html#1508" class="Bound">A</a><a id="1509" class="Symbol">}</a> <a id="1511" class="Symbol">{</a><a id="1512" class="Argument">B</a> <a id="1514" class="Symbol">=</a> <a id="1516" href="Relation.Binary.PropositionalEquality.html#1516" class="Bound">B</a><a id="1517" class="Symbol">}</a> <a id="1519" class="Symbol">=</a> <a id="1521" href="Relation.Binary.Bundles.html#1098" class="Field Operator">Setoid._≈_</a> <a id="1532" class="Symbol">(</a><a id="1533" href="Relation.Binary.PropositionalEquality.html#1508" class="Bound">A</a> <a id="1535" href="Relation.Binary.PropositionalEquality.html#1357" class="Function Operator">→-setoid</a> <a id="1544" href="Relation.Binary.PropositionalEquality.html#1516" class="Bound">B</a><a id="1545" class="Symbol">)</a>
<a id=":→-to-Π"></a><a id="1548" href="Relation.Binary.PropositionalEquality.html#1548" class="Function">:→-to-Π</a> <a id="1556" class="Symbol">:</a> <a id="1558" class="Symbol">∀</a> <a id="1560" class="Symbol">{</a><a id="1561" href="Relation.Binary.PropositionalEquality.html#1561" class="Bound">A</a> <a id="1563" class="Symbol">:</a> <a id="1565" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1569" href="Relation.Binary.PropositionalEquality.html#864" class="Generalizable">a</a><a id="1570" class="Symbol">}</a> <a id="1572" class="Symbol">{</a><a id="1573" href="Relation.Binary.PropositionalEquality.html#1573" class="Bound">B</a> <a id="1575" class="Symbol">:</a> <a id="1577" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#789" class="Record">IndexedSetoid</a> <a id="1591" href="Relation.Binary.PropositionalEquality.html#1561" class="Bound">A</a> <a id="1593" href="Relation.Binary.PropositionalEquality.html#866" class="Generalizable">b</a> <a id="1595" href="Relation.Binary.PropositionalEquality.html#870" class="Generalizable">ℓ</a><a id="1596" class="Symbol">}</a> <a id="1598" class="Symbol">→</a>
<a id="1610" class="Symbol">((</a><a id="1612" href="Relation.Binary.PropositionalEquality.html#1612" class="Bound">x</a> <a id="1614" class="Symbol">:</a> <a id="1616" href="Relation.Binary.PropositionalEquality.html#1561" class="Bound">A</a><a id="1617" class="Symbol">)</a> <a id="1619" class="Symbol">→</a> <a id="1621" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#879" class="Field">IndexedSetoid.Carrier</a> <a id="1643" href="Relation.Binary.PropositionalEquality.html#1573" class="Bound">B</a> <a id="1645" href="Relation.Binary.PropositionalEquality.html#1612" class="Bound">x</a><a id="1646" class="Symbol">)</a> <a id="1648" class="Symbol">→</a> <a id="1650" href="Function.Equality.html#889" class="Record">Π</a> <a id="1652" class="Symbol">(</a><a id="1653" href="Relation.Binary.PropositionalEquality.Properties.html#3972" class="Function">setoid</a> <a id="1660" href="Relation.Binary.PropositionalEquality.html#1561" class="Bound">A</a><a id="1661" class="Symbol">)</a> <a id="1663" href="Relation.Binary.PropositionalEquality.html#1573" class="Bound">B</a>
<a id="1665" href="Relation.Binary.PropositionalEquality.html#1548" class="Function">:→-to-Π</a> <a id="1673" class="Symbol">{</a><a id="1674" class="Argument">B</a> <a id="1676" class="Symbol">=</a> <a id="1678" href="Relation.Binary.PropositionalEquality.html#1678" class="Bound">B</a><a id="1679" class="Symbol">}</a> <a id="1681" href="Relation.Binary.PropositionalEquality.html#1681" class="Bound">f</a> <a id="1683" class="Symbol">=</a> <a id="1685" class="Keyword">record</a>
<a id="1694" class="Symbol">{</a> <a id="1696" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a> <a id="1702" class="Symbol">=</a> <a id="1704" href="Relation.Binary.PropositionalEquality.html#1681" class="Bound">f</a>
<a id="1708" class="Symbol">;</a> <a id="1710" href="Function.Equality.html#1131" class="Field">cong</a> <a id="1716" class="Symbol">=</a> <a id="1718" class="Symbol">λ</a> <a id="1720" class="Symbol">{</a> <a id="1722" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1727" class="Symbol">→</a> <a id="1729" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#909" class="Function">IndexedSetoid.refl</a> <a id="1748" href="Relation.Binary.PropositionalEquality.html#1678" class="Bound">B</a> <a id="1750" class="Symbol">}</a>
<a id="1754" class="Symbol">}</a>
<a id="1758" class="Keyword">where</a> <a id="1764" class="Keyword">open</a> <a id="1769" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#789" class="Module">IndexedSetoid</a> <a id="1783" href="Relation.Binary.PropositionalEquality.html#1678" class="Bound">B</a> <a id="1785" class="Keyword">using</a> <a id="1791" class="Symbol">(</a><a id="1792" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#909" class="Field Operator">_≈_</a><a id="1795" class="Symbol">)</a>
<a id="→-to-⟶"></a><a id="1798" href="Relation.Binary.PropositionalEquality.html#1798" class="Function">→-to-⟶</a> <a id="1805" class="Symbol">:</a> <a id="1807" class="Symbol">∀</a> <a id="1809" class="Symbol">{</a><a id="1810" href="Relation.Binary.PropositionalEquality.html#1810" class="Bound">A</a> <a id="1812" class="Symbol">:</a> <a id="1814" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1818" href="Relation.Binary.PropositionalEquality.html#864" class="Generalizable">a</a><a id="1819" class="Symbol">}</a> <a id="1821" class="Symbol">{</a><a id="1822" href="Relation.Binary.PropositionalEquality.html#1822" class="Bound">B</a> <a id="1824" class="Symbol">:</a> <a id="1826" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1833" href="Relation.Binary.PropositionalEquality.html#866" class="Generalizable">b</a> <a id="1835" href="Relation.Binary.PropositionalEquality.html#870" class="Generalizable">ℓ</a><a id="1836" class="Symbol">}</a> <a id="1838" class="Symbol">→</a>
<a id="1849" class="Symbol">(</a><a id="1850" href="Relation.Binary.PropositionalEquality.html#1810" class="Bound">A</a> <a id="1852" class="Symbol">→</a> <a id="1854" href="Relation.Binary.Bundles.html#1072" class="Field">Setoid.Carrier</a> <a id="1869" href="Relation.Binary.PropositionalEquality.html#1822" class="Bound">B</a><a id="1870" class="Symbol">)</a> <a id="1872" class="Symbol">→</a> <a id="1874" href="Relation.Binary.PropositionalEquality.Properties.html#3972" class="Function">setoid</a> <a id="1881" href="Relation.Binary.PropositionalEquality.html#1810" class="Bound">A</a> <a id="1883" href="Function.Equality.html#1218" class="Function Operator">⟶</a> <a id="1885" href="Relation.Binary.PropositionalEquality.html#1822" class="Bound">B</a>
<a id="1887" href="Relation.Binary.PropositionalEquality.html#1798" class="Function">→-to-⟶</a> <a id="1894" class="Symbol">=</a> <a id="1896" href="Relation.Binary.PropositionalEquality.html#1548" class="Function">:→-to-Π</a>
<a id="1905" class="Comment">------------------------------------------------------------------------</a>
<a id="1978" class="Comment">-- Inspect</a>
<a id="1990" class="Comment">-- Inspect can be used when you want to pattern match on the result r</a>
<a id="2060" class="Comment">-- of some expression e, and you also need to &quot;remember&quot; that r ≡ e.</a>
<a id="2130" class="Comment">-- See README.Inspect for an explanation of how/why to use this.</a>
<a id="2196" class="Keyword">record</a> <a id="Reveal_·_is_"></a><a id="2203" href="Relation.Binary.PropositionalEquality.html#2203" class="Record Operator">Reveal_·_is_</a> <a id="2216" class="Symbol">{</a><a id="2217" href="Relation.Binary.PropositionalEquality.html#2217" class="Bound">A</a> <a id="2219" class="Symbol">:</a> <a id="2221" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2225" href="Relation.Binary.PropositionalEquality.html#864" class="Generalizable">a</a><a id="2226" class="Symbol">}</a> <a id="2228" class="Symbol">{</a><a id="2229" href="Relation.Binary.PropositionalEquality.html#2229" class="Bound">B</a> <a id="2231" class="Symbol">:</a> <a id="2233" href="Relation.Binary.PropositionalEquality.html#2217" class="Bound">A</a> <a id="2235" class="Symbol">→</a> <a id="2237" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2241" href="Relation.Binary.PropositionalEquality.html#866" class="Generalizable">b</a><a id="2242" class="Symbol">}</a>
<a id="2264" class="Symbol">(</a><a id="2265" href="Relation.Binary.PropositionalEquality.html#2265" class="Bound">f</a> <a id="2267" class="Symbol">:</a> <a id="2269" class="Symbol">(</a><a id="2270" href="Relation.Binary.PropositionalEquality.html#2270" class="Bound">x</a> <a id="2272" class="Symbol">:</a> <a id="2274" href="Relation.Binary.PropositionalEquality.html#2217" class="Bound">A</a><a id="2275" class="Symbol">)</a> <a id="2277" class="Symbol">→</a> <a id="2279" href="Relation.Binary.PropositionalEquality.html#2229" class="Bound">B</a> <a id="2281" href="Relation.Binary.PropositionalEquality.html#2270" class="Bound">x</a><a id="2282" class="Symbol">)</a> <a id="2284" class="Symbol">(</a><a id="2285" href="Relation.Binary.PropositionalEquality.html#2285" class="Bound">x</a> <a id="2287" class="Symbol">:</a> <a id="2289" href="Relation.Binary.PropositionalEquality.html#2217" class="Bound">A</a><a id="2290" class="Symbol">)</a> <a id="2292" class="Symbol">(</a><a id="2293" href="Relation.Binary.PropositionalEquality.html#2293" class="Bound">y</a> <a id="2295" class="Symbol">:</a> <a id="2297" href="Relation.Binary.PropositionalEquality.html#2229" class="Bound">B</a> <a id="2299" href="Relation.Binary.PropositionalEquality.html#2285" class="Bound">x</a><a id="2300" class="Symbol">)</a> <a id="2302" class="Symbol">:</a>
<a id="2324" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2328" class="Symbol">(</a><a id="2329" href="Relation.Binary.PropositionalEquality.html#2225" class="Bound">a</a> <a id="2331" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2333" href="Relation.Binary.PropositionalEquality.html#2241" class="Bound">b</a><a id="2334" class="Symbol">)</a> <a id="2336" class="Keyword">where</a>
<a id="2344" class="Keyword">constructor</a> <a id="[_]"></a><a id="2356" href="Relation.Binary.PropositionalEquality.html#2356" class="InductiveConstructor Operator">[_]</a>
<a id="2362" class="Keyword">field</a> <a id="Reveal_·_is_.eq"></a><a id="2368" href="Relation.Binary.PropositionalEquality.html#2368" class="Field">eq</a> <a id="2371" class="Symbol">:</a> <a id="2373" href="Relation.Binary.PropositionalEquality.html#2265" class="Bound">f</a> <a id="2375" href="Relation.Binary.PropositionalEquality.html#2285" class="Bound">x</a> <a id="2377" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2379" href="Relation.Binary.PropositionalEquality.html#2293" class="Bound">y</a>
<a id="inspect"></a><a id="2382" href="Relation.Binary.PropositionalEquality.html#2382" class="Function">inspect</a> <a id="2390" class="Symbol">:</a> <a id="2392" class="Symbol">∀</a> <a id="2394" class="Symbol">{</a><a id="2395" href="Relation.Binary.PropositionalEquality.html#2395" class="Bound">A</a> <a id="2397" class="Symbol">:</a> <a id="2399" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2403" href="Relation.Binary.PropositionalEquality.html#864" class="Generalizable">a</a><a id="2404" class="Symbol">}</a> <a id="2406" class="Symbol">{</a><a id="2407" href="Relation.Binary.PropositionalEquality.html#2407" class="Bound">B</a> <a id="2409" class="Symbol">:</a> <a id="2411" href="Relation.Binary.PropositionalEquality.html#2395" class="Bound">A</a> <a id="2413" class="Symbol">→</a> <a id="2415" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2419" href="Relation.Binary.PropositionalEquality.html#866" class="Generalizable">b</a><a id="2420" class="Symbol">}</a>
<a id="2432" class="Symbol">(</a><a id="2433" href="Relation.Binary.PropositionalEquality.html#2433" class="Bound">f</a> <a id="2435" class="Symbol">:</a> <a id="2437" class="Symbol">(</a><a id="2438" href="Relation.Binary.PropositionalEquality.html#2438" class="Bound">x</a> <a id="2440" class="Symbol">:</a> <a id="2442" href="Relation.Binary.PropositionalEquality.html#2395" class="Bound">A</a><a id="2443" class="Symbol">)</a> <a id="2445" class="Symbol">→</a> <a id="2447" href="Relation.Binary.PropositionalEquality.html#2407" class="Bound">B</a> <a id="2449" href="Relation.Binary.PropositionalEquality.html#2438" class="Bound">x</a><a id="2450" class="Symbol">)</a> <a id="2452" class="Symbol">(</a><a id="2453" href="Relation.Binary.PropositionalEquality.html#2453" class="Bound">x</a> <a id="2455" class="Symbol">:</a> <a id="2457" href="Relation.Binary.PropositionalEquality.html#2395" class="Bound">A</a><a id="2458" class="Symbol">)</a> <a id="2460" class="Symbol">→</a> <a id="2462" href="Relation.Binary.PropositionalEquality.html#2203" class="Record Operator">Reveal</a> <a id="2469" href="Relation.Binary.PropositionalEquality.html#2433" class="Bound">f</a> <a id="2471" href="Relation.Binary.PropositionalEquality.html#2203" class="Record Operator">·</a> <a id="2473" href="Relation.Binary.PropositionalEquality.html#2453" class="Bound">x</a> <a id="2475" href="Relation.Binary.PropositionalEquality.html#2203" class="Record Operator">is</a> <a id="2478" href="Relation.Binary.PropositionalEquality.html#2433" class="Bound">f</a> <a id="2480" href="Relation.Binary.PropositionalEquality.html#2453" class="Bound">x</a>
<a id="2482" href="Relation.Binary.PropositionalEquality.html#2382" class="Function">inspect</a> <a id="2490" href="Relation.Binary.PropositionalEquality.html#2490" class="Bound">f</a> <a id="2492" href="Relation.Binary.PropositionalEquality.html#2492" class="Bound">x</a> <a id="2494" class="Symbol">=</a> <a id="2496" href="Relation.Binary.PropositionalEquality.html#2356" class="InductiveConstructor Operator">[</a> <a id="2498" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2503" href="Relation.Binary.PropositionalEquality.html#2356" class="InductiveConstructor Operator">]</a>
<a id="2506" class="Comment">------------------------------------------------------------------------</a>
<a id="2579" class="Comment">-- Propositionality</a>
<a id="isPropositional"></a><a id="2600" href="Relation.Binary.PropositionalEquality.html#2600" class="Function">isPropositional</a> <a id="2616" class="Symbol">:</a> <a id="2618" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2622" href="Relation.Binary.PropositionalEquality.html#864" class="Generalizable">a</a> <a id="2624" class="Symbol">→</a> <a id="2626" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2630" href="Relation.Binary.PropositionalEquality.html#864" class="Generalizable">a</a>
<a id="2632" href="Relation.Binary.PropositionalEquality.html#2600" class="Function">isPropositional</a> <a id="2648" href="Relation.Binary.PropositionalEquality.html#2648" class="Bound">A</a> <a id="2650" class="Symbol">=</a> <a id="2652" class="Symbol">(</a><a id="2653" href="Relation.Binary.PropositionalEquality.html#2653" class="Bound">a</a> <a id="2655" href="Relation.Binary.PropositionalEquality.html#2655" class="Bound">b</a> <a id="2657" class="Symbol">:</a> <a id="2659" href="Relation.Binary.PropositionalEquality.html#2648" class="Bound">A</a><a id="2660" class="Symbol">)</a> <a id="2662" class="Symbol">→</a> <a id="2664" href="Relation.Binary.PropositionalEquality.html#2653" class="Bound">a</a> <a id="2666" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2668" href="Relation.Binary.PropositionalEquality.html#2655" class="Bound">b</a>
<a id="2671" class="Comment">------------------------------------------------------------------------</a>
<a id="2744" class="Comment">-- More complex rearrangement lemmas</a>
<a id="2782" class="Comment">-- A lemma that is very similar to Lemma 2.4.3 from the HoTT book.</a>
<a id="naturality"></a><a id="2850" href="Relation.Binary.PropositionalEquality.html#2850" class="Function">naturality</a> <a id="2861" class="Symbol">:</a> <a id="2863" class="Symbol">∀</a> <a id="2865" class="Symbol">{</a><a id="2866" href="Relation.Binary.PropositionalEquality.html#2866" class="Bound">x</a> <a id="2868" href="Relation.Binary.PropositionalEquality.html#2868" class="Bound">y</a><a id="2869" class="Symbol">}</a> <a id="2871" class="Symbol">{</a><a id="2872" href="Relation.Binary.PropositionalEquality.html#2872" class="Bound">x≡y</a> <a id="2876" class="Symbol">:</a> <a id="2878" href="Relation.Binary.PropositionalEquality.html#2866" class="Bound">x</a> <a id="2880" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2882" href="Relation.Binary.PropositionalEquality.html#2868" class="Bound">y</a><a id="2883" class="Symbol">}</a> <a id="2885" class="Symbol">{</a><a id="2886" href="Relation.Binary.PropositionalEquality.html#2886" class="Bound">f</a> <a id="2888" href="Relation.Binary.PropositionalEquality.html#2888" class="Bound">g</a> <a id="2890" class="Symbol">:</a> <a id="2892" href="Relation.Binary.PropositionalEquality.html#886" class="Generalizable">A</a> <a id="2894" class="Symbol">→</a> <a id="2896" href="Relation.Binary.PropositionalEquality.html#900" class="Generalizable">B</a><a id="2897" class="Symbol">}</a>
<a id="2912" class="Symbol">(</a><a id="2913" href="Relation.Binary.PropositionalEquality.html#2913" class="Bound">f≡g</a> <a id="2917" class="Symbol">:</a> <a id="2919" class="Symbol">∀</a> <a id="2921" href="Relation.Binary.PropositionalEquality.html#2921" class="Bound">x</a> <a id="2923" class="Symbol">→</a> <a id="2925" href="Relation.Binary.PropositionalEquality.html#2886" class="Bound">f</a> <a id="2927" href="Relation.Binary.PropositionalEquality.html#2921" class="Bound">x</a> <a id="2929" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2931" href="Relation.Binary.PropositionalEquality.html#2888" class="Bound">g</a> <a id="2933" href="Relation.Binary.PropositionalEquality.html#2921" class="Bound">x</a><a id="2934" class="Symbol">)</a> <a id="2936" class="Symbol">→</a>
<a id="2951" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="2957" class="Symbol">(</a><a id="2958" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="2963" href="Relation.Binary.PropositionalEquality.html#2886" class="Bound">f</a> <a id="2965" href="Relation.Binary.PropositionalEquality.html#2872" class="Bound">x≡y</a><a id="2968" class="Symbol">)</a> <a id="2970" class="Symbol">(</a><a id="2971" href="Relation.Binary.PropositionalEquality.html#2913" class="Bound">f≡g</a> <a id="2975" href="Relation.Binary.PropositionalEquality.html#2868" class="Bound">y</a><a id="2976" class="Symbol">)</a> <a id="2978" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2980" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="2986" class="Symbol">(</a><a id="2987" href="Relation.Binary.PropositionalEquality.html#2913" class="Bound">f≡g</a> <a id="2991" href="Relation.Binary.PropositionalEquality.html#2866" class="Bound">x</a><a id="2992" class="Symbol">)</a> <a id="2994" class="Symbol">(</a><a id="2995" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3000" href="Relation.Binary.PropositionalEquality.html#2888" class="Bound">g</a> <a id="3002" href="Relation.Binary.PropositionalEquality.html#2872" class="Bound">x≡y</a><a id="3005" class="Symbol">)</a>
<a id="3007" href="Relation.Binary.PropositionalEquality.html#2850" class="Function">naturality</a> <a id="3018" class="Symbol">{</a><a id="3019" class="Argument">x</a> <a id="3021" class="Symbol">=</a> <a id="3023" href="Relation.Binary.PropositionalEquality.html#3023" class="Bound">x</a><a id="3024" class="Symbol">}</a> <a id="3026" class="Symbol">{</a><a id="3027" class="Argument">x≡y</a> <a id="3031" class="Symbol">=</a> <a id="3033" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a><a id="3037" class="Symbol">}</a> <a id="3039" href="Relation.Binary.PropositionalEquality.html#3039" class="Bound">f≡g</a> <a id="3043" class="Symbol">=</a>
<a id="3047" href="Relation.Binary.PropositionalEquality.html#3039" class="Bound">f≡g</a> <a id="3051" href="Relation.Binary.PropositionalEquality.html#3023" class="Bound">x</a> <a id="3067" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="3070" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3074" class="Symbol">(</a><a id="3075" href="Relation.Binary.PropositionalEquality.Properties.html#843" class="Function">trans-reflʳ</a> <a id="3087" class="Symbol">_)</a> <a id="3090" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="3094" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3100" class="Symbol">(</a><a id="3101" href="Relation.Binary.PropositionalEquality.html#3039" class="Bound">f≡g</a> <a id="3105" href="Relation.Binary.PropositionalEquality.html#3023" class="Bound">x</a><a id="3106" class="Symbol">)</a> <a id="3108" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="3114" href="Relation.Binary.PropositionalEquality.Core.html#3105" class="Function Operator">∎</a>
<a id="3118" class="Keyword">where</a> <a id="3124" class="Keyword">open</a> <a id="3129" href="Relation.Binary.PropositionalEquality.Core.html#2708" class="Module">≡-Reasoning</a>
<a id="3142" class="Comment">-- A lemma that is very similar to Corollary 2.4.4 from the HoTT book.</a>
<a id="cong-≡id"></a><a id="3214" href="Relation.Binary.PropositionalEquality.html#3214" class="Function">cong-≡id</a> <a id="3223" class="Symbol">:</a> <a id="3225" class="Symbol">∀</a> <a id="3227" class="Symbol">{</a><a id="3228" href="Relation.Binary.PropositionalEquality.html#3228" class="Bound">f</a> <a id="3230" class="Symbol">:</a> <a id="3232" href="Relation.Binary.PropositionalEquality.html#886" class="Generalizable">A</a> <a id="3234" class="Symbol">→</a> <a id="3236" href="Relation.Binary.PropositionalEquality.html#886" class="Generalizable">A</a><a id="3237" class="Symbol">}</a> <a id="3239" class="Symbol">{</a><a id="3240" href="Relation.Binary.PropositionalEquality.html#3240" class="Bound">x</a> <a id="3242" class="Symbol">:</a> <a id="3244" href="Relation.Binary.PropositionalEquality.html#886" class="Generalizable">A</a><a id="3245" class="Symbol">}</a> <a id="3247" class="Symbol">(</a><a id="3248" href="Relation.Binary.PropositionalEquality.html#3248" class="Bound">f≡id</a> <a id="3253" class="Symbol">:</a> <a id="3255" class="Symbol">∀</a> <a id="3257" href="Relation.Binary.PropositionalEquality.html#3257" class="Bound">x</a> <a id="3259" class="Symbol">→</a> <a id="3261" href="Relation.Binary.PropositionalEquality.html#3228" class="Bound">f</a> <a id="3263" href="Relation.Binary.PropositionalEquality.html#3257" class="Bound">x</a> <a id="3265" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3267" href="Relation.Binary.PropositionalEquality.html#3257" class="Bound">x</a><a id="3268" class="Symbol">)</a> <a id="3270" class="Symbol">→</a>
<a id="3283" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3288" href="Relation.Binary.PropositionalEquality.html#3228" class="Bound">f</a> <a id="3290" class="Symbol">(</a><a id="3291" href="Relation.Binary.PropositionalEquality.html#3248" class="Bound">f≡id</a> <a id="3296" href="Relation.Binary.PropositionalEquality.html#3240" class="Bound">x</a><a id="3297" class="Symbol">)</a> <a id="3299" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3301" href="Relation.Binary.PropositionalEquality.html#3248" class="Bound">f≡id</a> <a id="3306" class="Symbol">(</a><a id="3307" href="Relation.Binary.PropositionalEquality.html#3228" class="Bound">f</a> <a id="3309" href="Relation.Binary.PropositionalEquality.html#3240" class="Bound">x</a><a id="3310" class="Symbol">)</a>
<a id="3312" href="Relation.Binary.PropositionalEquality.html#3214" class="Function">cong-≡id</a> <a id="3321" class="Symbol">{</a><a id="3322" class="Argument">f</a> <a id="3324" class="Symbol">=</a> <a id="3326" href="Relation.Binary.PropositionalEquality.html#3326" class="Bound">f</a><a id="3327" class="Symbol">}</a> <a id="3329" class="Symbol">{</a><a id="3330" href="Relation.Binary.PropositionalEquality.html#3330" class="Bound">x</a><a id="3331" class="Symbol">}</a> <a id="3333" href="Relation.Binary.PropositionalEquality.html#3333" class="Bound">f≡id</a> <a id="3338" class="Symbol">=</a>
<a id="3342" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3347" href="Relation.Binary.PropositionalEquality.html#3326" class="Bound">f</a> <a id="3349" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a> <a id="3389" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="3392" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3396" class="Symbol">(</a><a id="3397" href="Relation.Binary.PropositionalEquality.Properties.html#843" class="Function">trans-reflʳ</a> <a id="3409" class="Symbol">_)</a> <a id="3412" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="3416" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3422" class="Symbol">(</a><a id="3423" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3428" href="Relation.Binary.PropositionalEquality.html#3326" class="Bound">f</a> <a id="3430" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3434" class="Symbol">)</a> <a id="3436" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="3463" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="3466" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3471" class="Symbol">(</a><a id="3472" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3478" class="Symbol">_)</a> <a id="3481" class="Symbol">(</a><a id="3482" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3486" class="Symbol">(</a><a id="3487" href="Relation.Binary.PropositionalEquality.Properties.html#1148" class="Function">trans-symʳ</a> <a id="3498" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3502" class="Symbol">))</a> <a id="3505" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="3509" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3515" class="Symbol">(</a><a id="3516" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3521" href="Relation.Binary.PropositionalEquality.html#3326" class="Bound">f</a> <a id="3523" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3527" class="Symbol">)</a> <a id="3529" class="Symbol">(</a><a id="3530" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3536" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a> <a id="3541" class="Symbol">(</a><a id="3542" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3546" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3550" class="Symbol">))</a> <a id="3556" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="3559" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3563" class="Symbol">(</a><a id="3564" href="Relation.Binary.PropositionalEquality.Properties.html#925" class="Function">trans-assoc</a> <a id="3576" class="Symbol">(</a><a id="3577" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3582" href="Relation.Binary.PropositionalEquality.html#3326" class="Bound">f</a> <a id="3584" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3588" class="Symbol">))</a> <a id="3591" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="3595" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3601" class="Symbol">(</a><a id="3602" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3608" class="Symbol">(</a><a id="3609" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3614" href="Relation.Binary.PropositionalEquality.html#3326" class="Bound">f</a> <a id="3616" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3620" class="Symbol">)</a> <a id="3622" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3626" class="Symbol">)</a> <a id="3628" class="Symbol">(</a><a id="3629" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3633" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3637" class="Symbol">)</a> <a id="3642" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="3645" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3650" class="Symbol">(λ</a> <a id="3653" href="Relation.Binary.PropositionalEquality.html#3653" class="Bound">p</a> <a id="3655" class="Symbol">→</a> <a id="3657" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3663" href="Relation.Binary.PropositionalEquality.html#3653" class="Bound">p</a> <a id="3665" class="Symbol">(</a><a id="3666" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3670" class="Symbol">_))</a> <a id="3674" class="Symbol">(</a><a id="3675" href="Relation.Binary.PropositionalEquality.html#2850" class="Function">naturality</a> <a id="3686" href="Relation.Binary.PropositionalEquality.html#3333" class="Bound">f≡id</a><a id="3690" class="Symbol">)</a> <a id="3692" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="3696" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3702" class="Symbol">(</a><a id="3703" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3709" href="Relation.Binary.PropositionalEquality.html#4125" class="Function">f²x≡x</a> <a id="3715" class="Symbol">(</a><a id="3716" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3721" href="Function.Base.html#615" class="Function">id</a> <a id="3724" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3728" class="Symbol">))</a> <a id="3731" class="Symbol">(</a><a id="3732" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3736" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3740" class="Symbol">)</a> <a id="3743" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="3746" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3751" class="Symbol">(λ</a> <a id="3754" href="Relation.Binary.PropositionalEquality.html#3754" class="Bound">p</a> <a id="3756" class="Symbol">→</a> <a id="3758" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3764" class="Symbol">(</a><a id="3765" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3771" href="Relation.Binary.PropositionalEquality.html#4125" class="Function">f²x≡x</a> <a id="3777" href="Relation.Binary.PropositionalEquality.html#3754" class="Bound">p</a><a id="3778" class="Symbol">)</a> <a id="3780" class="Symbol">(</a><a id="3781" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3785" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3789" class="Symbol">))</a> <a id="3792" class="Symbol">(</a><a id="3793" href="Relation.Binary.PropositionalEquality.Properties.html#1565" class="Function">cong-id</a> <a id="3801" class="Symbol">_)</a> <a id="3804" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="3808" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3814" class="Symbol">(</a><a id="3815" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3821" href="Relation.Binary.PropositionalEquality.html#4125" class="Function">f²x≡x</a> <a id="3827" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3831" class="Symbol">)</a> <a id="3833" class="Symbol">(</a><a id="3834" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3838" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3842" class="Symbol">)</a> <a id="3855" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="3858" href="Relation.Binary.PropositionalEquality.Properties.html#925" class="Function">trans-assoc</a> <a id="3870" href="Relation.Binary.PropositionalEquality.html#4125" class="Function">f²x≡x</a> <a id="3876" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="3880" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3886" href="Relation.Binary.PropositionalEquality.html#4125" class="Function">f²x≡x</a> <a id="3892" class="Symbol">(</a><a id="3893" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3899" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a> <a id="3904" class="Symbol">(</a><a id="3905" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="3909" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3913" class="Symbol">))</a> <a id="3927" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="3930" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="3935" class="Symbol">(</a><a id="3936" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3942" class="Symbol">_)</a> <a id="3945" class="Symbol">(</a><a id="3946" href="Relation.Binary.PropositionalEquality.Properties.html#1148" class="Function">trans-symʳ</a> <a id="3957" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a><a id="3961" class="Symbol">)</a> <a id="3963" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="3967" href="Relation.Binary.PropositionalEquality.Core.html#1729" class="Function">trans</a> <a id="3973" href="Relation.Binary.PropositionalEquality.html#4125" class="Function">f²x≡x</a> <a id="3979" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="4014" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="4017" href="Relation.Binary.PropositionalEquality.Properties.html#843" class="Function">trans-reflʳ</a> <a id="4029" class="Symbol">_</a> <a id="4031" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="4035" href="Relation.Binary.PropositionalEquality.html#3333" class="Bound">f≡id</a> <a id="4040" class="Symbol">(</a><a id="4041" href="Relation.Binary.PropositionalEquality.html#3326" class="Bound">f</a> <a id="4043" href="Relation.Binary.PropositionalEquality.html#3330" class="Bound">x</a><a id="4044" class="Symbol">)</a> <a id="4082" href="Relation.Binary.PropositionalEquality.Core.html#3105" class="Function Operator">∎</a>
<a id="4086" class="Keyword">where</a> <a id="4092" class="Keyword">open</a> <a id="4097" href="Relation.Binary.PropositionalEquality.Core.html#2708" class="Module">≡-Reasoning</a><a id="4108" class="Symbol">;</a> <a id="4110" href="Relation.Binary.PropositionalEquality.html#4110" class="Function">fx≡x</a> <a id="4115" class="Symbol">=</a> <a id="4117" href="Relation.Binary.PropositionalEquality.html#3333" class="Bound">f≡id</a> <a id="4122" href="Relation.Binary.PropositionalEquality.html#3330" class="Bound">x</a><a id="4123" class="Symbol">;</a> <a id="4125" href="Relation.Binary.PropositionalEquality.html#4125" class="Function">f²x≡x</a> <a id="4131" class="Symbol">=</a> <a id="4133" href="Relation.Binary.PropositionalEquality.html#3333" class="Bound">f≡id</a> <a id="4138" class="Symbol">(</a><a id="4139" href="Relation.Binary.PropositionalEquality.html#3326" class="Bound">f</a> <a id="4141" href="Relation.Binary.PropositionalEquality.html#3330" class="Bound">x</a><a id="4142" class="Symbol">)</a>
<a id="4145" class="Keyword">module</a> <a id="4152" href="Relation.Binary.PropositionalEquality.html#4152" class="Module">_</a> <a id="4154" class="Symbol">(</a><a id="4155" href="Relation.Binary.PropositionalEquality.html#4155" class="Bound Operator">_≟_</a> <a id="4159" class="Symbol">:</a> <a id="4161" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="4171" class="Symbol">{</a><a id="4172" class="Argument">A</a> <a id="4174" class="Symbol">=</a> <a id="4176" href="Relation.Binary.PropositionalEquality.html#886" class="Generalizable">A</a><a id="4177" class="Symbol">}</a> <a id="4179" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a><a id="4182" class="Symbol">)</a> <a id="4184" class="Symbol">{</a><a id="4185" href="Relation.Binary.PropositionalEquality.html#4185" class="Bound">x</a> <a id="4187" href="Relation.Binary.PropositionalEquality.html#4187" class="Bound">y</a> <a id="4189" class="Symbol">:</a> <a id="4191" href="Relation.Binary.PropositionalEquality.html#886" class="Generalizable">A</a><a id="4192" class="Symbol">}</a> <a id="4194" class="Keyword">where</a>
<a id="4203" href="Relation.Binary.PropositionalEquality.html#4203" class="Function">≡-≟-identity</a> <a id="4216" class="Symbol">:</a> <a id="4218" class="Symbol">(</a><a id="4219" href="Relation.Binary.PropositionalEquality.html#4219" class="Bound">eq</a> <a id="4222" class="Symbol">:</a> <a id="4224" href="Relation.Binary.PropositionalEquality.html#4185" class="Bound">x</a> <a id="4226" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="4228" href="Relation.Binary.PropositionalEquality.html#4187" class="Bound">y</a><a id="4229" class="Symbol">)</a> <a id="4231" class="Symbol">→</a> <a id="4233" href="Relation.Binary.PropositionalEquality.html#4185" class="Bound">x</a> <a id="4235" href="Relation.Binary.PropositionalEquality.html#4155" class="Bound Operator">≟</a> <a id="4237" href="Relation.Binary.PropositionalEquality.html#4187" class="Bound">y</a> <a id="4239" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="4241" href="Relation.Nullary.html#1648" class="InductiveConstructor">yes</a> <a id="4245" href="Relation.Binary.PropositionalEquality.html#4219" class="Bound">eq</a>
<a id="4250" href="Relation.Binary.PropositionalEquality.html#4203" class="Function">≡-≟-identity</a> <a id="4263" href="Relation.Binary.PropositionalEquality.html#4263" class="Bound">eq</a> <a id="4266" class="Symbol">=</a> <a id="4268" href="Relation.Nullary.Decidable.Core.html#3413" class="Function">dec-yes-irr</a> <a id="4280" class="Symbol">(</a><a id="4281" href="Relation.Binary.PropositionalEquality.html#4185" class="Bound">x</a> <a id="4283" href="Relation.Binary.PropositionalEquality.html#4155" class="Bound Operator">≟</a> <a id="4285" href="Relation.Binary.PropositionalEquality.html#4187" class="Bound">y</a><a id="4286" class="Symbol">)</a> <a id="4288" class="Symbol">(</a><a id="4289" href="Axiom.UniquenessOfIdentityProofs.html#2688" class="Function">Decidable⇒UIP.≡-irrelevant</a> <a id="4316" href="Relation.Binary.PropositionalEquality.html#4155" class="Bound Operator">_≟_</a><a id="4319" class="Symbol">)</a> <a id="4321" href="Relation.Binary.PropositionalEquality.html#4263" class="Bound">eq</a>
<a id="4327" href="Relation.Binary.PropositionalEquality.html#4327" class="Function">≢-≟-identity</a> <a id="4340" class="Symbol">:</a> <a id="4342" href="Relation.Binary.PropositionalEquality.html#4185" class="Bound">x</a> <a id="4344" href="Relation.Binary.PropositionalEquality.Core.html#830" class="Function Operator">≢</a> <a id="4346" href="Relation.Binary.PropositionalEquality.html#4187" class="Bound">y</a> <a id="4348" class="Symbol">→</a> <a id="4350" href="Data.Product.html#1369" class="Function">∃</a> <a id="4352" class="Symbol">λ</a> <a id="4354" href="Relation.Binary.PropositionalEquality.html#4354" class="Bound">¬eq</a> <a id="4358" class="Symbol">→</a> <a id="4360" href="Relation.Binary.PropositionalEquality.html#4185" class="Bound">x</a> <a id="4362" href="Relation.Binary.PropositionalEquality.html#4155" class="Bound Operator">≟</a> <a id="4364" href="Relation.Binary.PropositionalEquality.html#4187" class="Bound">y</a> <a id="4366" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="4368" href="Relation.Nullary.html#1685" class="InductiveConstructor">no</a> <a id="4371" href="Relation.Binary.PropositionalEquality.html#4354" class="Bound">¬eq</a>
<a id="4377" href="Relation.Binary.PropositionalEquality.html#4327" class="Function">≢-≟-identity</a> <a id="4390" href="Relation.Binary.PropositionalEquality.html#4390" class="Bound">¬eq</a> <a id="4394" class="Symbol">=</a> <a id="4396" href="Relation.Nullary.Decidable.Core.html#3287" class="Function">dec-no</a> <a id="4403" class="Symbol">(</a><a id="4404" href="Relation.Binary.PropositionalEquality.html#4185" class="Bound">x</a> <a id="4406" href="Relation.Binary.PropositionalEquality.html#4155" class="Bound Operator">≟</a> <a id="4408" href="Relation.Binary.PropositionalEquality.html#4187" class="Bound">y</a><a id="4409" class="Symbol">)</a> <a id="4411" href="Relation.Binary.PropositionalEquality.html#4390" class="Bound">¬eq</a>
<a id="4416" class="Comment">------------------------------------------------------------------------</a>
<a id="4489" class="Comment">-- DEPRECATED NAMES</a>
<a id="4509" class="Comment">------------------------------------------------------------------------</a>
<a id="4582" class="Comment">-- Please use the new names as continuing support for the old names is</a>
<a id="4653" class="Comment">-- not guaranteed.</a>
<a id="4673" class="Comment">-- Version 1.0</a>
<a id="Extensionality"></a><a id="4689" href="Relation.Binary.PropositionalEquality.html#4689" class="Function">Extensionality</a> <a id="4704" class="Symbol">=</a> <a id="4706" href="Axiom.Extensionality.Propositional.html#741" class="Function">Ext.Extensionality</a>
<a id="4725" class="Symbol">{-#</a> <a id="4729" class="Keyword">WARNING_ON_USAGE</a> <a id="4746" class="Pragma">Extensionality</a>
<a id="4761" class="String">&quot;Warning: Extensionality was deprecated in v1.0.
Please use Extensionality from `Axiom.Extensionality.Propositional` instead.&quot;</a>
<a id="4888" class="Symbol">#-}</a>
<a id="extensionality-for-lower-levels"></a><a id="4892" href="Relation.Binary.PropositionalEquality.html#4892" class="Function">extensionality-for-lower-levels</a> <a id="4924" class="Symbol">=</a> <a id="4926" href="Axiom.Extensionality.Propositional.html#1304" class="Function">Ext.lower-extensionality</a>
<a id="4951" class="Symbol">{-#</a> <a id="4955" class="Keyword">WARNING_ON_USAGE</a> <a id="4972" class="Pragma">extensionality-for-lower-levels</a>
<a id="5004" class="String">&quot;Warning: extensionality-for-lower-levels was deprecated in v1.0.
Please use lower-extensionality from `Axiom.Extensionality.Propositional` instead.&quot;</a>
<a id="5154" class="Symbol">#-}</a>
<a id="∀-extensionality"></a><a id="5158" href="Relation.Binary.PropositionalEquality.html#5158" class="Function">∀-extensionality</a> <a id="5175" class="Symbol">=</a> <a id="5177" href="Axiom.Extensionality.Propositional.html#1664" class="Function">Ext.∀-extensionality</a>
<a id="5198" class="Symbol">{-#</a> <a id="5202" class="Keyword">WARNING_ON_USAGE</a> <a id="5219" class="Pragma">∀-extensionality</a>
<a id="5236" class="String">&quot;Warning: ∀-extensionality was deprecated in v1.0.
Please use ∀-extensionality from `Axiom.Extensionality.Propositional` instead.&quot;</a>
<a id="5367" class="Symbol">#-}</a>
</pre></body></html>
Reference in New Issue Copy Permalink