leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity
bsc-leon-vatthauer/public/Axiom.Extensionality.Propositional.html

64 lines
No EOL
21 KiB
HTML
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!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">--cubical-compatible</a> <a id="286" class="Pragma">--safe</a> <a id="293" class="Symbol">#-}</a>
<a id="298" class="Keyword">module</a> <a id="305" href="Axiom.Extensionality.Propositional.html" class="Module">Axiom.Extensionality.Propositional</a> <a id="340" class="Keyword">where</a>
<a id="347" class="Keyword">open</a> <a id="352" class="Keyword">import</a> <a id="359" href="Function.Base.html" class="Module">Function.Base</a>
<a id="373" class="Keyword">open</a> <a id="378" class="Keyword">import</a> <a id="385" href="Level.html" class="Module">Level</a> <a id="391" class="Keyword">using</a> <a id="397" class="Symbol">(</a><a id="398" href="Agda.Primitive.html#591" class="Postulate">Level</a><a id="403" class="Symbol">;</a> <a id="405" href="Agda.Primitive.html#804" class="Primitive Operator">_⊔_</a><a id="408" class="Symbol">;</a> <a id="410" href="Agda.Primitive.html#774" class="Primitive">suc</a><a id="413" class="Symbol">;</a> <a id="415" href="Level.html#466" class="InductiveConstructor">lift</a><a id="419" class="Symbol">)</a>
<a id="421" class="Keyword">open</a> <a id="426" class="Keyword">import</a> <a id="433" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a>
<a id="454" class="Keyword">open</a> <a id="459" class="Keyword">import</a> <a id="466" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a>
<a id="510" class="Comment">------------------------------------------------------------------------</a>
<a id="583" class="Comment">-- Function extensionality states that if two functions are</a>
<a id="643" class="Comment">-- propositionally equal for every input, then the functions themselves</a>
<a id="715" class="Comment">-- must be propositionally equal.</a>
<a id="Extensionality"></a><a id="750" href="Axiom.Extensionality.Propositional.html#750" class="Function">Extensionality</a> <a id="765" class="Symbol">:</a> <a id="767" class="Symbol">(</a><a id="768" href="Axiom.Extensionality.Propositional.html#768" class="Bound">a</a> <a id="770" href="Axiom.Extensionality.Propositional.html#770" class="Bound">b</a> <a id="772" class="Symbol">:</a> <a id="774" href="Agda.Primitive.html#591" class="Postulate">Level</a><a id="779" class="Symbol">)</a> <a id="781" class="Symbol">→</a> <a id="783" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="787" class="Symbol">_</a>
<a id="789" href="Axiom.Extensionality.Propositional.html#750" class="Function">Extensionality</a> <a id="804" href="Axiom.Extensionality.Propositional.html#804" class="Bound">a</a> <a id="806" href="Axiom.Extensionality.Propositional.html#806" class="Bound">b</a> <a id="808" class="Symbol">=</a>
<a id="812" class="Symbol">{</a><a id="813" href="Axiom.Extensionality.Propositional.html#813" class="Bound">A</a> <a id="815" class="Symbol">:</a> <a id="817" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="821" href="Axiom.Extensionality.Propositional.html#804" class="Bound">a</a><a id="822" class="Symbol">}</a> <a id="824" class="Symbol">{</a><a id="825" href="Axiom.Extensionality.Propositional.html#825" class="Bound">B</a> <a id="827" class="Symbol">:</a> <a id="829" href="Axiom.Extensionality.Propositional.html#813" class="Bound">A</a> <a id="831" class="Symbol">→</a> <a id="833" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="837" href="Axiom.Extensionality.Propositional.html#806" class="Bound">b</a><a id="838" class="Symbol">}</a> <a id="840" class="Symbol">{</a><a id="841" href="Axiom.Extensionality.Propositional.html#841" class="Bound">f</a> <a id="843" href="Axiom.Extensionality.Propositional.html#843" class="Bound">g</a> <a id="845" class="Symbol">:</a> <a id="847" class="Symbol">(</a><a id="848" href="Axiom.Extensionality.Propositional.html#848" class="Bound">x</a> <a id="850" class="Symbol">:</a> <a id="852" href="Axiom.Extensionality.Propositional.html#813" class="Bound">A</a><a id="853" class="Symbol">)</a> <a id="855" class="Symbol">→</a> <a id="857" href="Axiom.Extensionality.Propositional.html#825" class="Bound">B</a> <a id="859" href="Axiom.Extensionality.Propositional.html#848" class="Bound">x</a><a id="860" class="Symbol">}</a> <a id="862" class="Symbol">→</a>
<a id="866" class="Symbol">(∀</a> <a id="869" href="Axiom.Extensionality.Propositional.html#869" class="Bound">x</a> <a id="871" class="Symbol">→</a> <a id="873" href="Axiom.Extensionality.Propositional.html#841" class="Bound">f</a> <a id="875" href="Axiom.Extensionality.Propositional.html#869" class="Bound">x</a> <a id="877" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">≡</a> <a id="879" href="Axiom.Extensionality.Propositional.html#843" class="Bound">g</a> <a id="881" href="Axiom.Extensionality.Propositional.html#869" class="Bound">x</a><a id="882" class="Symbol">)</a> <a id="884" class="Symbol">→</a> <a id="886" href="Axiom.Extensionality.Propositional.html#841" class="Bound">f</a> <a id="888" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">≡</a> <a id="890" href="Axiom.Extensionality.Propositional.html#843" class="Bound">g</a>
<a id="893" class="Comment">-- A variant for implicit function spaces.</a>
<a id="ExtensionalityImplicit"></a><a id="937" href="Axiom.Extensionality.Propositional.html#937" class="Function">ExtensionalityImplicit</a> <a id="960" class="Symbol">:</a> <a id="962" class="Symbol">(</a><a id="963" href="Axiom.Extensionality.Propositional.html#963" class="Bound">a</a> <a id="965" href="Axiom.Extensionality.Propositional.html#965" class="Bound">b</a> <a id="967" class="Symbol">:</a> <a id="969" href="Agda.Primitive.html#591" class="Postulate">Level</a><a id="974" class="Symbol">)</a> <a id="976" class="Symbol">→</a> <a id="978" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="982" class="Symbol">_</a>
<a id="984" href="Axiom.Extensionality.Propositional.html#937" class="Function">ExtensionalityImplicit</a> <a id="1007" href="Axiom.Extensionality.Propositional.html#1007" class="Bound">a</a> <a id="1009" href="Axiom.Extensionality.Propositional.html#1009" class="Bound">b</a> <a id="1011" class="Symbol">=</a>
<a id="1015" class="Symbol">{</a><a id="1016" href="Axiom.Extensionality.Propositional.html#1016" class="Bound">A</a> <a id="1018" class="Symbol">:</a> <a id="1020" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1024" href="Axiom.Extensionality.Propositional.html#1007" class="Bound">a</a><a id="1025" class="Symbol">}</a> <a id="1027" class="Symbol">{</a><a id="1028" href="Axiom.Extensionality.Propositional.html#1028" class="Bound">B</a> <a id="1030" class="Symbol">:</a> <a id="1032" href="Axiom.Extensionality.Propositional.html#1016" class="Bound">A</a> <a id="1034" class="Symbol">→</a> <a id="1036" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1040" href="Axiom.Extensionality.Propositional.html#1009" class="Bound">b</a><a id="1041" class="Symbol">}</a> <a id="1043" class="Symbol">{</a><a id="1044" href="Axiom.Extensionality.Propositional.html#1044" class="Bound">f</a> <a id="1046" href="Axiom.Extensionality.Propositional.html#1046" class="Bound">g</a> <a id="1048" class="Symbol">:</a> <a id="1050" class="Symbol">{</a><a id="1051" href="Axiom.Extensionality.Propositional.html#1051" class="Bound">x</a> <a id="1053" class="Symbol">:</a> <a id="1055" href="Axiom.Extensionality.Propositional.html#1016" class="Bound">A</a><a id="1056" class="Symbol">}</a> <a id="1058" class="Symbol">→</a> <a id="1060" href="Axiom.Extensionality.Propositional.html#1028" class="Bound">B</a> <a id="1062" href="Axiom.Extensionality.Propositional.html#1051" class="Bound">x</a><a id="1063" class="Symbol">}</a> <a id="1065" class="Symbol">→</a>
<a id="1069" class="Symbol">(∀</a> <a id="1072" class="Symbol">{</a><a id="1073" href="Axiom.Extensionality.Propositional.html#1073" class="Bound">x</a><a id="1074" class="Symbol">}</a> <a id="1076" class="Symbol">→</a> <a id="1078" href="Axiom.Extensionality.Propositional.html#1044" class="Bound">f</a> <a id="1080" class="Symbol">{</a><a id="1081" href="Axiom.Extensionality.Propositional.html#1073" class="Bound">x</a><a id="1082" class="Symbol">}</a> <a id="1084" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">≡</a> <a id="1086" href="Axiom.Extensionality.Propositional.html#1046" class="Bound">g</a> <a id="1088" class="Symbol">{</a><a id="1089" href="Axiom.Extensionality.Propositional.html#1073" class="Bound">x</a><a id="1090" class="Symbol">})</a> <a id="1093" class="Symbol">→</a> <a id="1095" class="Symbol">(λ</a> <a id="1098" class="Symbol">{</a><a id="1099" href="Axiom.Extensionality.Propositional.html#1099" class="Bound">x</a><a id="1100" class="Symbol">}</a> <a id="1102" class="Symbol">→</a> <a id="1104" href="Axiom.Extensionality.Propositional.html#1044" class="Bound">f</a> <a id="1106" class="Symbol">{</a><a id="1107" href="Axiom.Extensionality.Propositional.html#1099" class="Bound">x</a><a id="1108" class="Symbol">})</a> <a id="1111" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">≡</a> <a id="1113" class="Symbol">(λ</a> <a id="1116" class="Symbol">{</a><a id="1117" href="Axiom.Extensionality.Propositional.html#1117" class="Bound">x</a><a id="1118" class="Symbol">}</a> <a id="1120" class="Symbol">→</a> <a id="1122" href="Axiom.Extensionality.Propositional.html#1046" class="Bound">g</a> <a id="1124" class="Symbol">{</a><a id="1125" href="Axiom.Extensionality.Propositional.html#1117" class="Bound">x</a><a id="1126" class="Symbol">})</a>
<a id="1131" class="Comment">------------------------------------------------------------------------</a>
<a id="1204" class="Comment">-- Properties</a>
<a id="1219" class="Comment">-- If extensionality holds for a given universe level, then it also</a>
<a id="1287" class="Comment">-- holds for lower ones.</a>
<a id="lower-extensionality"></a><a id="1313" href="Axiom.Extensionality.Propositional.html#1313" class="Function">lower-extensionality</a> <a id="1334" class="Symbol">:</a> <a id="1336" class="Symbol">∀</a> <a id="1338" class="Symbol">{</a><a id="1339" href="Axiom.Extensionality.Propositional.html#1339" class="Bound">a₁</a> <a id="1342" href="Axiom.Extensionality.Propositional.html#1342" class="Bound">b₁</a><a id="1344" class="Symbol">}</a> <a id="1346" href="Axiom.Extensionality.Propositional.html#1346" class="Bound">a₂</a> <a id="1349" href="Axiom.Extensionality.Propositional.html#1349" class="Bound">b₂</a> <a id="1352" class="Symbol">→</a>
<a id="1377" href="Axiom.Extensionality.Propositional.html#750" class="Function">Extensionality</a> <a id="1392" class="Symbol">(</a><a id="1393" href="Axiom.Extensionality.Propositional.html#1339" class="Bound">a₁</a> <a id="1396" href="Agda.Primitive.html#804" class="Primitive Operator">⊔</a> <a id="1398" href="Axiom.Extensionality.Propositional.html#1346" class="Bound">a₂</a><a id="1400" class="Symbol">)</a> <a id="1402" class="Symbol">(</a><a id="1403" href="Axiom.Extensionality.Propositional.html#1342" class="Bound">b₁</a> <a id="1406" href="Agda.Primitive.html#804" class="Primitive Operator">⊔</a> <a id="1408" href="Axiom.Extensionality.Propositional.html#1349" class="Bound">b₂</a><a id="1410" class="Symbol">)</a> <a id="1412" class="Symbol">→</a>
<a id="1437" href="Axiom.Extensionality.Propositional.html#750" class="Function">Extensionality</a> <a id="1452" href="Axiom.Extensionality.Propositional.html#1339" class="Bound">a₁</a> <a id="1455" href="Axiom.Extensionality.Propositional.html#1342" class="Bound">b₁</a>
<a id="1458" href="Axiom.Extensionality.Propositional.html#1313" class="Function">lower-extensionality</a> <a id="1479" href="Axiom.Extensionality.Propositional.html#1479" class="Bound">a₂</a> <a id="1482" href="Axiom.Extensionality.Propositional.html#1482" class="Bound">b₂</a> <a id="1485" href="Axiom.Extensionality.Propositional.html#1485" class="Bound">ext</a> <a id="1489" href="Axiom.Extensionality.Propositional.html#1489" class="Bound">f≡g</a> <a id="1493" class="Symbol">=</a> <a id="1495" href="Relation.Binary.PropositionalEquality.Core.html#1139" class="Function">cong</a> <a id="1500" class="Symbol">(λ</a> <a id="1503" href="Axiom.Extensionality.Propositional.html#1503" class="Bound">h</a> <a id="1505" class="Symbol">→</a> <a id="1507" href="Level.html#479" class="Field">Level.lower</a> <a id="1519" href="Function.Base.html#1040" class="Function Operator">∘</a> <a id="1521" href="Axiom.Extensionality.Propositional.html#1503" class="Bound">h</a> <a id="1523" href="Function.Base.html#1040" class="Function Operator">∘</a> <a id="1525" href="Level.html#466" class="InductiveConstructor">lift</a><a id="1529" class="Symbol">)</a> <a id="1531" href="Function.Base.html#1928" class="Function Operator">$</a>
<a id="1537" href="Axiom.Extensionality.Propositional.html#1485" class="Bound">ext</a> <a id="1541" class="Symbol">(</a><a id="1542" href="Relation.Binary.PropositionalEquality.Core.html#1139" class="Function">cong</a> <a id="1547" class="Symbol">(</a><a id="1548" href="Level.html#466" class="InductiveConstructor">lift</a> <a id="1553" class="Symbol">{</a><a id="1554" class="Argument">ℓ</a> <a id="1556" class="Symbol">=</a> <a id="1558" href="Axiom.Extensionality.Propositional.html#1482" class="Bound">b₂</a><a id="1560" class="Symbol">})</a> <a id="1563" href="Function.Base.html#1040" class="Function Operator">∘</a> <a id="1565" href="Axiom.Extensionality.Propositional.html#1489" class="Bound">f≡g</a> <a id="1569" href="Function.Base.html#1040" class="Function Operator">∘</a> <a id="1571" href="Level.html#479" class="Field">Level.lower</a> <a id="1583" class="Symbol">{</a><a id="1584" class="Argument">ℓ</a> <a id="1586" class="Symbol">=</a> <a id="1588" href="Axiom.Extensionality.Propositional.html#1479" class="Bound">a₂</a><a id="1590" class="Symbol">})</a>
<a id="1594" class="Comment">-- Functional extensionality implies a form of extensionality for</a>
<a id="1660" class="Comment">-- Π-types.</a>
<a id="∀-extensionality"></a><a id="1673" href="Axiom.Extensionality.Propositional.html#1673" class="Function">∀-extensionality</a> <a id="1690" class="Symbol">:</a> <a id="1692" class="Symbol">∀</a> <a id="1694" class="Symbol">{</a><a id="1695" href="Axiom.Extensionality.Propositional.html#1695" class="Bound">a</a> <a id="1697" href="Axiom.Extensionality.Propositional.html#1697" class="Bound">b</a><a id="1698" class="Symbol">}</a> <a id="1700" class="Symbol">→</a> <a id="1702" href="Axiom.Extensionality.Propositional.html#750" class="Function">Extensionality</a> <a id="1717" href="Axiom.Extensionality.Propositional.html#1695" class="Bound">a</a> <a id="1719" class="Symbol">(</a><a id="1720" href="Agda.Primitive.html#774" class="Primitive">suc</a> <a id="1724" href="Axiom.Extensionality.Propositional.html#1697" class="Bound">b</a><a id="1725" class="Symbol">)</a> <a id="1727" class="Symbol">→</a>
<a id="1748" class="Symbol">{</a><a id="1749" href="Axiom.Extensionality.Propositional.html#1749" class="Bound">A</a> <a id="1751" class="Symbol">:</a> <a id="1753" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1757" href="Axiom.Extensionality.Propositional.html#1695" class="Bound">a</a><a id="1758" class="Symbol">}</a> <a id="1760" class="Symbol">(</a><a id="1761" href="Axiom.Extensionality.Propositional.html#1761" class="Bound">B₁</a> <a id="1764" href="Axiom.Extensionality.Propositional.html#1764" class="Bound">B₂</a> <a id="1767" class="Symbol">:</a> <a id="1769" href="Axiom.Extensionality.Propositional.html#1749" class="Bound">A</a> <a id="1771" class="Symbol">→</a> <a id="1773" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1777" href="Axiom.Extensionality.Propositional.html#1697" class="Bound">b</a><a id="1778" class="Symbol">)</a> <a id="1780" class="Symbol">→</a>
<a id="1801" class="Symbol">(∀</a> <a id="1804" href="Axiom.Extensionality.Propositional.html#1804" class="Bound">x</a> <a id="1806" class="Symbol">→</a> <a id="1808" href="Axiom.Extensionality.Propositional.html#1761" class="Bound">B₁</a> <a id="1811" href="Axiom.Extensionality.Propositional.html#1804" class="Bound">x</a> <a id="1813" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">≡</a> <a id="1815" href="Axiom.Extensionality.Propositional.html#1764" class="Bound">B₂</a> <a id="1818" href="Axiom.Extensionality.Propositional.html#1804" class="Bound">x</a><a id="1819" class="Symbol">)</a> <a id="1821" class="Symbol">→</a>
<a id="1842" class="Symbol">(∀</a> <a id="1845" href="Axiom.Extensionality.Propositional.html#1845" class="Bound">x</a> <a id="1847" class="Symbol">→</a> <a id="1849" href="Axiom.Extensionality.Propositional.html#1761" class="Bound">B₁</a> <a id="1852" href="Axiom.Extensionality.Propositional.html#1845" class="Bound">x</a><a id="1853" class="Symbol">)</a> <a id="1855" href="Agda.Builtin.Equality.html#133" class="Datatype Operator">≡</a> <a id="1857" class="Symbol">(∀</a> <a id="1860" href="Axiom.Extensionality.Propositional.html#1860" class="Bound">x</a> <a id="1862" class="Symbol">→</a> <a id="1864" href="Axiom.Extensionality.Propositional.html#1764" class="Bound">B₂</a> <a id="1867" href="Axiom.Extensionality.Propositional.html#1860" class="Bound">x</a><a id="1868" class="Symbol">)</a>
<a id="1870" href="Axiom.Extensionality.Propositional.html#1673" class="Function">∀-extensionality</a> <a id="1887" href="Axiom.Extensionality.Propositional.html#1887" class="Bound">ext</a> <a id="1891" href="Axiom.Extensionality.Propositional.html#1891" class="Bound">B₁</a> <a id="1894" href="Axiom.Extensionality.Propositional.html#1894" class="Bound">B₂</a> <a id="1897" href="Axiom.Extensionality.Propositional.html#1897" class="Bound">B₁≡B₂</a> <a id="1903" class="Keyword">with</a> <a id="1908" href="Axiom.Extensionality.Propositional.html#1887" class="Bound">ext</a> <a id="1912" href="Axiom.Extensionality.Propositional.html#1897" class="Bound">B₁≡B₂</a>
<a id="1918" class="Symbol">...</a> <a id="1922" class="Symbol">|</a> <a id="1924" href="Agda.Builtin.Equality.html#190" class="InductiveConstructor">refl</a> <a id="1929" class="Symbol">=</a> <a id="1931" href="Agda.Builtin.Equality.html#190" class="InductiveConstructor">refl</a>
<a id="1937" class="Comment">-- Extensionality for explicit function spaces implies extensionality</a>
<a id="2007" class="Comment">-- for implicit function spaces.</a>
<a id="implicit-extensionality"></a><a id="2041" href="Axiom.Extensionality.Propositional.html#2041" class="Function">implicit-extensionality</a> <a id="2065" class="Symbol">:</a> <a id="2067" class="Symbol">∀</a> <a id="2069" class="Symbol">{</a><a id="2070" href="Axiom.Extensionality.Propositional.html#2070" class="Bound">a</a> <a id="2072" href="Axiom.Extensionality.Propositional.html#2072" class="Bound">b</a><a id="2073" class="Symbol">}</a> <a id="2075" class="Symbol">→</a>
<a id="2103" href="Axiom.Extensionality.Propositional.html#750" class="Function">Extensionality</a> <a id="2118" href="Axiom.Extensionality.Propositional.html#2070" class="Bound">a</a> <a id="2120" href="Axiom.Extensionality.Propositional.html#2072" class="Bound">b</a> <a id="2122" class="Symbol">→</a>
<a id="2150" href="Axiom.Extensionality.Propositional.html#937" class="Function">ExtensionalityImplicit</a> <a id="2173" href="Axiom.Extensionality.Propositional.html#2070" class="Bound">a</a> <a id="2175" href="Axiom.Extensionality.Propositional.html#2072" class="Bound">b</a>
<a id="2177" href="Axiom.Extensionality.Propositional.html#2041" class="Function">implicit-extensionality</a> <a id="2201" href="Axiom.Extensionality.Propositional.html#2201" class="Bound">ext</a> <a id="2205" href="Axiom.Extensionality.Propositional.html#2205" class="Bound">f≡g</a> <a id="2209" class="Symbol">=</a> <a id="2211" href="Relation.Binary.PropositionalEquality.Core.html#1139" class="Function">cong</a> <a id="2216" href="Function.Base.html#2750" class="Function Operator">_$-</a> <a id="2220" class="Symbol">(</a><a id="2221" href="Axiom.Extensionality.Propositional.html#2201" class="Bound">ext</a> <a id="2225" class="Symbol">(λ</a> <a id="2228" href="Axiom.Extensionality.Propositional.html#2228" class="Bound">x</a> <a id="2230" class="Symbol">→</a> <a id="2232" href="Axiom.Extensionality.Propositional.html#2205" class="Bound">f≡g</a><a id="2235" class="Symbol">))</a>
</pre></body></html>
Reference in a new issue View git blame Copy permalink