64 lines
21 KiB
HTML
64 lines
21 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Axiom.Extensionality.Propositional</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">-- Results concerning function extensionality for propositional equality</a>
|
||
<a id="179" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="253" class="Symbol">{-#</a> <a id="257" class="Keyword">OPTIONS</a> <a id="265" class="Pragma">--without-K</a> <a id="277" class="Pragma">--safe</a> <a id="284" class="Symbol">#-}</a>
|
||
|
||
<a id="289" class="Keyword">module</a> <a id="296" href="Axiom.Extensionality.Propositional.html" class="Module">Axiom.Extensionality.Propositional</a> <a id="331" class="Keyword">where</a>
|
||
|
||
<a id="338" class="Keyword">open</a> <a id="343" class="Keyword">import</a> <a id="350" href="Function.Base.html" class="Module">Function.Base</a>
|
||
<a id="364" class="Keyword">open</a> <a id="369" class="Keyword">import</a> <a id="376" href="Level.html" class="Module">Level</a> <a id="382" class="Keyword">using</a> <a id="388" class="Symbol">(</a><a id="389" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="394" class="Symbol">;</a> <a id="396" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="399" class="Symbol">;</a> <a id="401" href="Agda.Primitive.html#780" class="Primitive">suc</a><a id="404" class="Symbol">;</a> <a id="406" href="Level.html#457" class="InductiveConstructor">lift</a><a id="410" class="Symbol">)</a>
|
||
<a id="412" class="Keyword">open</a> <a id="417" class="Keyword">import</a> <a id="424" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a>
|
||
<a id="445" class="Keyword">open</a> <a id="450" class="Keyword">import</a> <a id="457" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a>
|
||
|
||
<a id="501" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="574" class="Comment">-- Function extensionality states that if two functions are</a>
|
||
<a id="634" class="Comment">-- propositionally equal for every input, then the functions themselves</a>
|
||
<a id="706" class="Comment">-- must be propositionally equal.</a>
|
||
|
||
<a id="Extensionality"></a><a id="741" href="Axiom.Extensionality.Propositional.html#741" class="Function">Extensionality</a> <a id="756" class="Symbol">:</a> <a id="758" class="Symbol">(</a><a id="759" href="Axiom.Extensionality.Propositional.html#759" class="Bound">a</a> <a id="761" href="Axiom.Extensionality.Propositional.html#761" class="Bound">b</a> <a id="763" class="Symbol">:</a> <a id="765" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="770" class="Symbol">)</a> <a id="772" class="Symbol">→</a> <a id="774" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="778" class="Symbol">_</a>
|
||
<a id="780" href="Axiom.Extensionality.Propositional.html#741" class="Function">Extensionality</a> <a id="795" href="Axiom.Extensionality.Propositional.html#795" class="Bound">a</a> <a id="797" href="Axiom.Extensionality.Propositional.html#797" class="Bound">b</a> <a id="799" class="Symbol">=</a>
|
||
<a id="803" class="Symbol">{</a><a id="804" href="Axiom.Extensionality.Propositional.html#804" class="Bound">A</a> <a id="806" class="Symbol">:</a> <a id="808" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="812" href="Axiom.Extensionality.Propositional.html#795" class="Bound">a</a><a id="813" class="Symbol">}</a> <a id="815" class="Symbol">{</a><a id="816" href="Axiom.Extensionality.Propositional.html#816" class="Bound">B</a> <a id="818" class="Symbol">:</a> <a id="820" href="Axiom.Extensionality.Propositional.html#804" class="Bound">A</a> <a id="822" class="Symbol">→</a> <a id="824" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="828" href="Axiom.Extensionality.Propositional.html#797" class="Bound">b</a><a id="829" class="Symbol">}</a> <a id="831" class="Symbol">{</a><a id="832" href="Axiom.Extensionality.Propositional.html#832" class="Bound">f</a> <a id="834" href="Axiom.Extensionality.Propositional.html#834" class="Bound">g</a> <a id="836" class="Symbol">:</a> <a id="838" class="Symbol">(</a><a id="839" href="Axiom.Extensionality.Propositional.html#839" class="Bound">x</a> <a id="841" class="Symbol">:</a> <a id="843" href="Axiom.Extensionality.Propositional.html#804" class="Bound">A</a><a id="844" class="Symbol">)</a> <a id="846" class="Symbol">→</a> <a id="848" href="Axiom.Extensionality.Propositional.html#816" class="Bound">B</a> <a id="850" href="Axiom.Extensionality.Propositional.html#839" class="Bound">x</a><a id="851" class="Symbol">}</a> <a id="853" class="Symbol">→</a>
|
||
<a id="857" class="Symbol">(∀</a> <a id="860" href="Axiom.Extensionality.Propositional.html#860" class="Bound">x</a> <a id="862" class="Symbol">→</a> <a id="864" href="Axiom.Extensionality.Propositional.html#832" class="Bound">f</a> <a id="866" href="Axiom.Extensionality.Propositional.html#860" class="Bound">x</a> <a id="868" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="870" href="Axiom.Extensionality.Propositional.html#834" class="Bound">g</a> <a id="872" href="Axiom.Extensionality.Propositional.html#860" class="Bound">x</a><a id="873" class="Symbol">)</a> <a id="875" class="Symbol">→</a> <a id="877" href="Axiom.Extensionality.Propositional.html#832" class="Bound">f</a> <a id="879" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="881" href="Axiom.Extensionality.Propositional.html#834" class="Bound">g</a>
|
||
|
||
<a id="884" class="Comment">-- A variant for implicit function spaces.</a>
|
||
|
||
<a id="ExtensionalityImplicit"></a><a id="928" href="Axiom.Extensionality.Propositional.html#928" class="Function">ExtensionalityImplicit</a> <a id="951" class="Symbol">:</a> <a id="953" class="Symbol">(</a><a id="954" href="Axiom.Extensionality.Propositional.html#954" class="Bound">a</a> <a id="956" href="Axiom.Extensionality.Propositional.html#956" class="Bound">b</a> <a id="958" class="Symbol">:</a> <a id="960" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="965" class="Symbol">)</a> <a id="967" class="Symbol">→</a> <a id="969" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="973" class="Symbol">_</a>
|
||
<a id="975" href="Axiom.Extensionality.Propositional.html#928" class="Function">ExtensionalityImplicit</a> <a id="998" href="Axiom.Extensionality.Propositional.html#998" class="Bound">a</a> <a id="1000" href="Axiom.Extensionality.Propositional.html#1000" class="Bound">b</a> <a id="1002" class="Symbol">=</a>
|
||
<a id="1006" class="Symbol">{</a><a id="1007" href="Axiom.Extensionality.Propositional.html#1007" class="Bound">A</a> <a id="1009" class="Symbol">:</a> <a id="1011" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1015" href="Axiom.Extensionality.Propositional.html#998" class="Bound">a</a><a id="1016" class="Symbol">}</a> <a id="1018" class="Symbol">{</a><a id="1019" href="Axiom.Extensionality.Propositional.html#1019" class="Bound">B</a> <a id="1021" class="Symbol">:</a> <a id="1023" href="Axiom.Extensionality.Propositional.html#1007" class="Bound">A</a> <a id="1025" class="Symbol">→</a> <a id="1027" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1031" href="Axiom.Extensionality.Propositional.html#1000" class="Bound">b</a><a id="1032" class="Symbol">}</a> <a id="1034" class="Symbol">{</a><a id="1035" href="Axiom.Extensionality.Propositional.html#1035" class="Bound">f</a> <a id="1037" href="Axiom.Extensionality.Propositional.html#1037" class="Bound">g</a> <a id="1039" class="Symbol">:</a> <a id="1041" class="Symbol">{</a><a id="1042" href="Axiom.Extensionality.Propositional.html#1042" class="Bound">x</a> <a id="1044" class="Symbol">:</a> <a id="1046" href="Axiom.Extensionality.Propositional.html#1007" class="Bound">A</a><a id="1047" class="Symbol">}</a> <a id="1049" class="Symbol">→</a> <a id="1051" href="Axiom.Extensionality.Propositional.html#1019" class="Bound">B</a> <a id="1053" href="Axiom.Extensionality.Propositional.html#1042" class="Bound">x</a><a id="1054" class="Symbol">}</a> <a id="1056" class="Symbol">→</a>
|
||
<a id="1060" class="Symbol">(∀</a> <a id="1063" class="Symbol">{</a><a id="1064" href="Axiom.Extensionality.Propositional.html#1064" class="Bound">x</a><a id="1065" class="Symbol">}</a> <a id="1067" class="Symbol">→</a> <a id="1069" href="Axiom.Extensionality.Propositional.html#1035" class="Bound">f</a> <a id="1071" class="Symbol">{</a><a id="1072" href="Axiom.Extensionality.Propositional.html#1064" class="Bound">x</a><a id="1073" class="Symbol">}</a> <a id="1075" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1077" href="Axiom.Extensionality.Propositional.html#1037" class="Bound">g</a> <a id="1079" class="Symbol">{</a><a id="1080" href="Axiom.Extensionality.Propositional.html#1064" class="Bound">x</a><a id="1081" class="Symbol">})</a> <a id="1084" class="Symbol">→</a> <a id="1086" class="Symbol">(λ</a> <a id="1089" class="Symbol">{</a><a id="1090" href="Axiom.Extensionality.Propositional.html#1090" class="Bound">x</a><a id="1091" class="Symbol">}</a> <a id="1093" class="Symbol">→</a> <a id="1095" href="Axiom.Extensionality.Propositional.html#1035" class="Bound">f</a> <a id="1097" class="Symbol">{</a><a id="1098" href="Axiom.Extensionality.Propositional.html#1090" class="Bound">x</a><a id="1099" class="Symbol">})</a> <a id="1102" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1104" class="Symbol">(λ</a> <a id="1107" class="Symbol">{</a><a id="1108" href="Axiom.Extensionality.Propositional.html#1108" class="Bound">x</a><a id="1109" class="Symbol">}</a> <a id="1111" class="Symbol">→</a> <a id="1113" href="Axiom.Extensionality.Propositional.html#1037" class="Bound">g</a> <a id="1115" class="Symbol">{</a><a id="1116" href="Axiom.Extensionality.Propositional.html#1108" class="Bound">x</a><a id="1117" class="Symbol">})</a>
|
||
|
||
|
||
<a id="1122" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1195" class="Comment">-- Properties</a>
|
||
|
||
<a id="1210" class="Comment">-- If extensionality holds for a given universe level, then it also</a>
|
||
<a id="1278" class="Comment">-- holds for lower ones.</a>
|
||
|
||
<a id="lower-extensionality"></a><a id="1304" href="Axiom.Extensionality.Propositional.html#1304" class="Function">lower-extensionality</a> <a id="1325" class="Symbol">:</a> <a id="1327" class="Symbol">∀</a> <a id="1329" class="Symbol">{</a><a id="1330" href="Axiom.Extensionality.Propositional.html#1330" class="Bound">a₁</a> <a id="1333" href="Axiom.Extensionality.Propositional.html#1333" class="Bound">b₁</a><a id="1335" class="Symbol">}</a> <a id="1337" href="Axiom.Extensionality.Propositional.html#1337" class="Bound">a₂</a> <a id="1340" href="Axiom.Extensionality.Propositional.html#1340" class="Bound">b₂</a> <a id="1343" class="Symbol">→</a>
|
||
<a id="1368" href="Axiom.Extensionality.Propositional.html#741" class="Function">Extensionality</a> <a id="1383" class="Symbol">(</a><a id="1384" href="Axiom.Extensionality.Propositional.html#1330" class="Bound">a₁</a> <a id="1387" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1389" href="Axiom.Extensionality.Propositional.html#1337" class="Bound">a₂</a><a id="1391" class="Symbol">)</a> <a id="1393" class="Symbol">(</a><a id="1394" href="Axiom.Extensionality.Propositional.html#1333" class="Bound">b₁</a> <a id="1397" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1399" href="Axiom.Extensionality.Propositional.html#1340" class="Bound">b₂</a><a id="1401" class="Symbol">)</a> <a id="1403" class="Symbol">→</a>
|
||
<a id="1428" href="Axiom.Extensionality.Propositional.html#741" class="Function">Extensionality</a> <a id="1443" href="Axiom.Extensionality.Propositional.html#1330" class="Bound">a₁</a> <a id="1446" href="Axiom.Extensionality.Propositional.html#1333" class="Bound">b₁</a>
|
||
<a id="1449" href="Axiom.Extensionality.Propositional.html#1304" class="Function">lower-extensionality</a> <a id="1470" href="Axiom.Extensionality.Propositional.html#1470" class="Bound">a₂</a> <a id="1473" href="Axiom.Extensionality.Propositional.html#1473" class="Bound">b₂</a> <a id="1476" href="Axiom.Extensionality.Propositional.html#1476" class="Bound">ext</a> <a id="1480" href="Axiom.Extensionality.Propositional.html#1480" class="Bound">f≡g</a> <a id="1484" class="Symbol">=</a> <a id="1486" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1491" class="Symbol">(λ</a> <a id="1494" href="Axiom.Extensionality.Propositional.html#1494" class="Bound">h</a> <a id="1496" class="Symbol">→</a> <a id="1498" href="Level.html#470" class="Field">Level.lower</a> <a id="1510" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1512" href="Axiom.Extensionality.Propositional.html#1494" class="Bound">h</a> <a id="1514" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1516" href="Level.html#457" class="InductiveConstructor">lift</a><a id="1520" class="Symbol">)</a> <a id="1522" href="Function.Base.html#1919" class="Function Operator">$</a>
|
||
<a id="1528" href="Axiom.Extensionality.Propositional.html#1476" class="Bound">ext</a> <a id="1532" class="Symbol">(</a><a id="1533" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="1538" class="Symbol">(</a><a id="1539" href="Level.html#457" class="InductiveConstructor">lift</a> <a id="1544" class="Symbol">{</a><a id="1545" class="Argument">ℓ</a> <a id="1547" class="Symbol">=</a> <a id="1549" href="Axiom.Extensionality.Propositional.html#1473" class="Bound">b₂</a><a id="1551" class="Symbol">})</a> <a id="1554" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1556" href="Axiom.Extensionality.Propositional.html#1480" class="Bound">f≡g</a> <a id="1560" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1562" href="Level.html#470" class="Field">Level.lower</a> <a id="1574" class="Symbol">{</a><a id="1575" class="Argument">ℓ</a> <a id="1577" class="Symbol">=</a> <a id="1579" href="Axiom.Extensionality.Propositional.html#1470" class="Bound">a₂</a><a id="1581" class="Symbol">})</a>
|
||
|
||
<a id="1585" class="Comment">-- Functional extensionality implies a form of extensionality for</a>
|
||
<a id="1651" class="Comment">-- Π-types.</a>
|
||
|
||
<a id="∀-extensionality"></a><a id="1664" href="Axiom.Extensionality.Propositional.html#1664" class="Function">∀-extensionality</a> <a id="1681" class="Symbol">:</a> <a id="1683" class="Symbol">∀</a> <a id="1685" class="Symbol">{</a><a id="1686" href="Axiom.Extensionality.Propositional.html#1686" class="Bound">a</a> <a id="1688" href="Axiom.Extensionality.Propositional.html#1688" class="Bound">b</a><a id="1689" class="Symbol">}</a> <a id="1691" class="Symbol">→</a> <a id="1693" href="Axiom.Extensionality.Propositional.html#741" class="Function">Extensionality</a> <a id="1708" href="Axiom.Extensionality.Propositional.html#1686" class="Bound">a</a> <a id="1710" class="Symbol">(</a><a id="1711" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="1715" href="Axiom.Extensionality.Propositional.html#1688" class="Bound">b</a><a id="1716" class="Symbol">)</a> <a id="1718" class="Symbol">→</a>
|
||
<a id="1739" class="Symbol">{</a><a id="1740" href="Axiom.Extensionality.Propositional.html#1740" class="Bound">A</a> <a id="1742" class="Symbol">:</a> <a id="1744" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1748" href="Axiom.Extensionality.Propositional.html#1686" class="Bound">a</a><a id="1749" class="Symbol">}</a> <a id="1751" class="Symbol">(</a><a id="1752" href="Axiom.Extensionality.Propositional.html#1752" class="Bound">B₁</a> <a id="1755" href="Axiom.Extensionality.Propositional.html#1755" class="Bound">B₂</a> <a id="1758" class="Symbol">:</a> <a id="1760" href="Axiom.Extensionality.Propositional.html#1740" class="Bound">A</a> <a id="1762" class="Symbol">→</a> <a id="1764" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1768" href="Axiom.Extensionality.Propositional.html#1688" class="Bound">b</a><a id="1769" class="Symbol">)</a> <a id="1771" class="Symbol">→</a>
|
||
<a id="1792" class="Symbol">(∀</a> <a id="1795" href="Axiom.Extensionality.Propositional.html#1795" class="Bound">x</a> <a id="1797" class="Symbol">→</a> <a id="1799" href="Axiom.Extensionality.Propositional.html#1752" class="Bound">B₁</a> <a id="1802" href="Axiom.Extensionality.Propositional.html#1795" class="Bound">x</a> <a id="1804" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1806" href="Axiom.Extensionality.Propositional.html#1755" class="Bound">B₂</a> <a id="1809" href="Axiom.Extensionality.Propositional.html#1795" class="Bound">x</a><a id="1810" class="Symbol">)</a> <a id="1812" class="Symbol">→</a>
|
||
<a id="1833" class="Symbol">(∀</a> <a id="1836" href="Axiom.Extensionality.Propositional.html#1836" class="Bound">x</a> <a id="1838" class="Symbol">→</a> <a id="1840" href="Axiom.Extensionality.Propositional.html#1752" class="Bound">B₁</a> <a id="1843" href="Axiom.Extensionality.Propositional.html#1836" class="Bound">x</a><a id="1844" class="Symbol">)</a> <a id="1846" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1848" class="Symbol">(∀</a> <a id="1851" href="Axiom.Extensionality.Propositional.html#1851" class="Bound">x</a> <a id="1853" class="Symbol">→</a> <a id="1855" href="Axiom.Extensionality.Propositional.html#1755" class="Bound">B₂</a> <a id="1858" href="Axiom.Extensionality.Propositional.html#1851" class="Bound">x</a><a id="1859" class="Symbol">)</a>
|
||
<a id="1861" href="Axiom.Extensionality.Propositional.html#1664" class="Function">∀-extensionality</a> <a id="1878" href="Axiom.Extensionality.Propositional.html#1878" class="Bound">ext</a> <a id="1882" href="Axiom.Extensionality.Propositional.html#1882" class="Bound">B₁</a> <a id="1885" href="Axiom.Extensionality.Propositional.html#1885" class="Bound">B₂</a> <a id="1888" href="Axiom.Extensionality.Propositional.html#1888" class="Bound">B₁≡B₂</a> <a id="1894" class="Keyword">with</a> <a id="1899" href="Axiom.Extensionality.Propositional.html#1878" class="Bound">ext</a> <a id="1903" href="Axiom.Extensionality.Propositional.html#1888" class="Bound">B₁≡B₂</a>
|
||
<a id="1909" class="Symbol">...</a> <a id="1913" class="Symbol">|</a> <a id="1915" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1920" class="Symbol">=</a> <a id="1922" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="1928" class="Comment">-- Extensionality for explicit function spaces implies extensionality</a>
|
||
<a id="1998" class="Comment">-- for implicit function spaces.</a>
|
||
|
||
<a id="implicit-extensionality"></a><a id="2032" href="Axiom.Extensionality.Propositional.html#2032" class="Function">implicit-extensionality</a> <a id="2056" class="Symbol">:</a> <a id="2058" class="Symbol">∀</a> <a id="2060" class="Symbol">{</a><a id="2061" href="Axiom.Extensionality.Propositional.html#2061" class="Bound">a</a> <a id="2063" href="Axiom.Extensionality.Propositional.html#2063" class="Bound">b</a><a id="2064" class="Symbol">}</a> <a id="2066" class="Symbol">→</a>
|
||
<a id="2094" href="Axiom.Extensionality.Propositional.html#741" class="Function">Extensionality</a> <a id="2109" href="Axiom.Extensionality.Propositional.html#2061" class="Bound">a</a> <a id="2111" href="Axiom.Extensionality.Propositional.html#2063" class="Bound">b</a> <a id="2113" class="Symbol">→</a>
|
||
<a id="2141" href="Axiom.Extensionality.Propositional.html#928" class="Function">ExtensionalityImplicit</a> <a id="2164" href="Axiom.Extensionality.Propositional.html#2061" class="Bound">a</a> <a id="2166" href="Axiom.Extensionality.Propositional.html#2063" class="Bound">b</a>
|
||
<a id="2168" href="Axiom.Extensionality.Propositional.html#2032" class="Function">implicit-extensionality</a> <a id="2192" href="Axiom.Extensionality.Propositional.html#2192" class="Bound">ext</a> <a id="2196" href="Axiom.Extensionality.Propositional.html#2196" class="Bound">f≡g</a> <a id="2200" class="Symbol">=</a> <a id="2202" href="Relation.Binary.PropositionalEquality.Core.html#1130" class="Function">cong</a> <a id="2207" href="Function.Base.html#2741" class="Function Operator">_$-</a> <a id="2211" class="Symbol">(</a><a id="2212" href="Axiom.Extensionality.Propositional.html#2192" class="Bound">ext</a> <a id="2216" class="Symbol">(λ</a> <a id="2219" href="Axiom.Extensionality.Propositional.html#2219" class="Bound">x</a> <a id="2221" class="Symbol">→</a> <a id="2223" href="Axiom.Extensionality.Propositional.html#2196" class="Bound">f≡g</a><a id="2226" class="Symbol">))</a>
|
||
</pre></body></html> |