208 lines
89 KiB
HTML
208 lines
89 KiB
HTML
|
<!DOCTYPE HTML>
|
|||
|
|
<html><head><meta charset="utf-8"><title>Data.Product</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">-- Products</a>
|
|||
|
|
<a id="118" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
|
|||
|
|
<a id="192" class="Symbol">{-#</a> <a id="196" class="Keyword">OPTIONS</a> <a id="204" class="Pragma">--without-K</a> <a id="216" class="Pragma">--safe</a> <a id="223" class="Symbol">#-}</a>
|
|||
|
|
|
|||
|
|
<a id="228" class="Keyword">module</a> <a id="235" href="Data.Product.html" class="Module">Data.Product</a> <a id="248" class="Keyword">where</a>
|
|||
|
|
|
|||
|
|
<a id="255" class="Keyword">open</a> <a id="260" class="Keyword">import</a> <a id="267" href="Function.Base.html" class="Module">Function.Base</a>
|
|||
|
|
<a id="281" class="Keyword">open</a> <a id="286" class="Keyword">import</a> <a id="293" href="Level.html" class="Module">Level</a>
|
|||
|
|
<a id="299" class="Keyword">open</a> <a id="304" class="Keyword">import</a> <a id="311" href="Relation.Nullary.html" class="Module">Relation.Nullary</a>
|
|||
|
|
<a id="328" class="Keyword">open</a> <a id="333" class="Keyword">import</a> <a id="340" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a>
|
|||
|
|
|
|||
|
|
<a id="363" class="Keyword">private</a>
|
|||
|
|
<a id="373" class="Keyword">variable</a>
|
|||
|
|
<a id="386" href="Data.Product.html#386" class="Generalizable">a</a> <a id="388" href="Data.Product.html#388" class="Generalizable">b</a> <a id="390" href="Data.Product.html#390" class="Generalizable">c</a> <a id="392" href="Data.Product.html#392" class="Generalizable">d</a> <a id="394" href="Data.Product.html#394" class="Generalizable">e</a> <a id="396" href="Data.Product.html#396" class="Generalizable">f</a> <a id="398" href="Data.Product.html#398" class="Generalizable">ℓ</a> <a id="400" href="Data.Product.html#400" class="Generalizable">p</a> <a id="402" href="Data.Product.html#402" class="Generalizable">q</a> <a id="404" href="Data.Product.html#404" class="Generalizable">r</a> <a id="406" class="Symbol">:</a> <a id="408" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
|||
|
|
<a id="418" href="Data.Product.html#418" class="Generalizable">A</a> <a id="420" class="Symbol">:</a> <a id="422" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="426" href="Data.Product.html#386" class="Generalizable">a</a>
|
|||
|
|
<a id="432" href="Data.Product.html#432" class="Generalizable">B</a> <a id="434" class="Symbol">:</a> <a id="436" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="440" href="Data.Product.html#388" class="Generalizable">b</a>
|
|||
|
|
<a id="446" href="Data.Product.html#446" class="Generalizable">C</a> <a id="448" class="Symbol">:</a> <a id="450" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="454" href="Data.Product.html#390" class="Generalizable">c</a>
|
|||
|
|
<a id="460" href="Data.Product.html#460" class="Generalizable">D</a> <a id="462" class="Symbol">:</a> <a id="464" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="468" href="Data.Product.html#392" class="Generalizable">d</a>
|
|||
|
|
<a id="474" href="Data.Product.html#474" class="Generalizable">E</a> <a id="476" class="Symbol">:</a> <a id="478" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="482" href="Data.Product.html#394" class="Generalizable">e</a>
|
|||
|
|
<a id="488" href="Data.Product.html#488" class="Generalizable">F</a> <a id="490" class="Symbol">:</a> <a id="492" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="496" href="Data.Product.html#396" class="Generalizable">f</a>
|
|||
|
|
|
|||
|
|
<a id="499" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
<a id="572" class="Comment">-- Definition of dependent products</a>
|
|||
|
|
|
|||
|
|
<a id="609" class="Keyword">open</a> <a id="614" class="Keyword">import</a> <a id="621" href="Agda.Builtin.Sigma.html" class="Module">Agda.Builtin.Sigma</a> <a id="640" class="Keyword">public</a>
|
|||
|
|
<a id="649" class="Keyword">renaming</a> <a id="658" class="Symbol">(</a><a id="659" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="663" class="Symbol">to</a> <a id="666" class="Field">proj₁</a><a id="671" class="Symbol">;</a> <a id="673" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="677" class="Symbol">to</a> <a id="680" class="Field">proj₂</a><a id="685" class="Symbol">)</a>
|
|||
|
|
<a id="689" class="Keyword">hiding</a> <a id="696" class="Symbol">(</a><a id="697" class="Keyword">module</a> <a id="704" href="Agda.Builtin.Sigma.html#166" class="Module">Σ</a><a id="705" class="Symbol">)</a>
|
|||
|
|
|
|||
|
|
<a id="708" class="Keyword">module</a> <a id="Σ"></a><a id="715" href="Data.Product.html#715" class="Module">Σ</a> <a id="717" class="Symbol">=</a> <a id="719" href="Agda.Builtin.Sigma.html#166" class="Module">Agda.Builtin.Sigma.Σ</a>
|
|||
|
|
<a id="742" class="Keyword">renaming</a> <a id="751" class="Symbol">(</a><a id="752" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="756" class="Symbol">to</a> <a id="759" class="Field">proj₁</a><a id="764" class="Symbol">;</a> <a id="766" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="770" class="Symbol">to</a> <a id="773" class="Field">proj₂</a><a id="778" class="Symbol">)</a>
|
|||
|
|
|
|||
|
|
<a id="781" class="Comment">-- The syntax declaration below is attached to Σ-syntax, to make it</a>
|
|||
|
|
<a id="849" class="Comment">-- easy to import Σ without the special syntax.</a>
|
|||
|
|
|
|||
|
|
<a id="898" class="Keyword">infix</a> <a id="904" class="Number">2</a> <a id="906" href="Data.Product.html#916" class="Function">Σ-syntax</a>
|
|||
|
|
|
|||
|
|
<a id="Σ-syntax"></a><a id="916" href="Data.Product.html#916" class="Function">Σ-syntax</a> <a id="925" class="Symbol">:</a> <a id="927" class="Symbol">(</a><a id="928" href="Data.Product.html#928" class="Bound">A</a> <a id="930" class="Symbol">:</a> <a id="932" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="936" href="Data.Product.html#386" class="Generalizable">a</a><a id="937" class="Symbol">)</a> <a id="939" class="Symbol">→</a> <a id="941" class="Symbol">(</a><a id="942" href="Data.Product.html#928" class="Bound">A</a> <a id="944" class="Symbol">→</a> <a id="946" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="950" href="Data.Product.html#388" class="Generalizable">b</a><a id="951" class="Symbol">)</a> <a id="953" class="Symbol">→</a> <a id="955" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="959" class="Symbol">(</a><a id="960" href="Data.Product.html#386" class="Generalizable">a</a> <a id="962" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="964" href="Data.Product.html#388" class="Generalizable">b</a><a id="965" class="Symbol">)</a>
|
|||
|
|
<a id="967" href="Data.Product.html#916" class="Function">Σ-syntax</a> <a id="976" class="Symbol">=</a> <a id="978" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a>
|
|||
|
|
|
|||
|
|
<a id="981" class="Keyword">syntax</a> <a id="988" href="Data.Product.html#916" class="Function">Σ-syntax</a> <a id="997" class="Bound">A</a> <a id="999" class="Symbol">(λ</a> <a id="1002" class="Bound">x</a> <a id="1004" class="Symbol">→</a> <a id="1006" class="Bound">B</a><a id="1007" class="Symbol">)</a> <a id="1009" class="Symbol">=</a> <a id="1011" class="Function">Σ[</a> <a id="1014" class="Bound">x</a> <a id="1016" class="Function">∈</a> <a id="1018" class="Bound">A</a> <a id="1020" class="Function">]</a> <a id="1022" class="Bound">B</a>
|
|||
|
|
|
|||
|
|
<a id="1025" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
<a id="1098" class="Comment">-- Definition of non-dependent products</a>
|
|||
|
|
|
|||
|
|
<a id="1139" class="Keyword">infixr</a> <a id="1146" class="Number">4</a> <a id="1148" href="Data.Product.html#1235" class="Function Operator">_,′_</a>
|
|||
|
|
<a id="1153" class="Keyword">infixr</a> <a id="1160" class="Number">2</a> <a id="1162" href="Data.Product.html#1167" class="Function Operator">_×_</a>
|
|||
|
|
|
|||
|
|
<a id="_×_"></a><a id="1167" href="Data.Product.html#1167" class="Function Operator">_×_</a> <a id="1171" class="Symbol">:</a> <a id="1173" class="Symbol">∀</a> <a id="1175" class="Symbol">(</a><a id="1176" href="Data.Product.html#1176" class="Bound">A</a> <a id="1178" class="Symbol">:</a> <a id="1180" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1184" href="Data.Product.html#386" class="Generalizable">a</a><a id="1185" class="Symbol">)</a> <a id="1187" class="Symbol">(</a><a id="1188" href="Data.Product.html#1188" class="Bound">B</a> <a id="1190" class="Symbol">:</a> <a id="1192" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1196" href="Data.Product.html#388" class="Generalizable">b</a><a id="1197" class="Symbol">)</a> <a id="1199" class="Symbol">→</a> <a id="1201" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1205" class="Symbol">(</a><a id="1206" href="Data.Product.html#386" class="Generalizable">a</a> <a id="1208" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1210" href="Data.Product.html#388" class="Generalizable">b</a><a id="1211" class="Symbol">)</a>
|
|||
|
|
<a id="1213" href="Data.Product.html#1213" class="Bound">A</a> <a id="1215" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="1217" href="Data.Product.html#1217" class="Bound">B</a> <a id="1219" class="Symbol">=</a> <a id="1221" href="Data.Product.html#916" class="Function">Σ[</a> <a id="1224" href="Data.Product.html#1224" class="Bound">x</a> <a id="1226" href="Data.Product.html#916" class="Function">∈</a> <a id="1228" href="Data.Product.html#1213" class="Bound">A</a> <a id="1230" href="Data.Product.html#916" class="Function">]</a> <a id="1232" href="Data.Product.html#1217" class="Bound">B</a>
|
|||
|
|
|
|||
|
|
<a id="_,′_"></a><a id="1235" href="Data.Product.html#1235" class="Function Operator">_,′_</a> <a id="1240" class="Symbol">:</a> <a id="1242" href="Data.Product.html#418" class="Generalizable">A</a> <a id="1244" class="Symbol">→</a> <a id="1246" href="Data.Product.html#432" class="Generalizable">B</a> <a id="1248" class="Symbol">→</a> <a id="1250" href="Data.Product.html#418" class="Generalizable">A</a> <a id="1252" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="1254" href="Data.Product.html#432" class="Generalizable">B</a>
|
|||
|
|
<a id="1256" href="Data.Product.html#1235" class="Function Operator">_,′_</a> <a id="1261" class="Symbol">=</a> <a id="1263" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a>
|
|||
|
|
|
|||
|
|
<a id="1268" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
<a id="1341" class="Comment">-- Existential quantifiers</a>
|
|||
|
|
|
|||
|
|
<a id="∃"></a><a id="1369" href="Data.Product.html#1369" class="Function">∃</a> <a id="1371" class="Symbol">:</a> <a id="1373" class="Symbol">∀</a> <a id="1375" class="Symbol">{</a><a id="1376" href="Data.Product.html#1376" class="Bound">A</a> <a id="1378" class="Symbol">:</a> <a id="1380" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1384" href="Data.Product.html#386" class="Generalizable">a</a><a id="1385" class="Symbol">}</a> <a id="1387" class="Symbol">→</a> <a id="1389" class="Symbol">(</a><a id="1390" href="Data.Product.html#1376" class="Bound">A</a> <a id="1392" class="Symbol">→</a> <a id="1394" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1398" href="Data.Product.html#388" class="Generalizable">b</a><a id="1399" class="Symbol">)</a> <a id="1401" class="Symbol">→</a> <a id="1403" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1407" class="Symbol">(</a><a id="1408" href="Data.Product.html#386" class="Generalizable">a</a> <a id="1410" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1412" href="Data.Product.html#388" class="Generalizable">b</a><a id="1413" class="Symbol">)</a>
|
|||
|
|
<a id="1415" href="Data.Product.html#1369" class="Function">∃</a> <a id="1417" class="Symbol">=</a> <a id="1419" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="1421" class="Symbol">_</a>
|
|||
|
|
|
|||
|
|
<a id="∄"></a><a id="1424" href="Data.Product.html#1424" class="Function">∄</a> <a id="1426" class="Symbol">:</a> <a id="1428" class="Symbol">∀</a> <a id="1430" class="Symbol">{</a><a id="1431" href="Data.Product.html#1431" class="Bound">A</a> <a id="1433" class="Symbol">:</a> <a id="1435" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1439" href="Data.Product.html#386" class="Generalizable">a</a><a id="1440" class="Symbol">}</a> <a id="1442" class="Symbol">→</a> <a id="1444" class="Symbol">(</a><a id="1445" href="Data.Product.html#1431" class="Bound">A</a> <a id="1447" class="Symbol">→</a> <a id="1449" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1453" href="Data.Product.html#388" class="Generalizable">b</a><a id="1454" class="Symbol">)</a> <a id="1456" class="Symbol">→</a> <a id="1458" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1462" class="Symbol">(</a><a id="1463" href="Data.Product.html#386" class="Generalizable">a</a> <a id="1465" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1467" href="Data.Product.html#388" class="Generalizable">b</a><a id="1468" class="Symbol">)</a>
|
|||
|
|
<a id="1470" href="Data.Product.html#1424" class="Function">∄</a> <a id="1472" href="Data.Product.html#1472" class="Bound">P</a> <a id="1474" class="Symbol">=</a> <a id="1476" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="1478" href="Data.Product.html#1369" class="Function">∃</a> <a id="1480" href="Data.Product.html#1472" class="Bound">P</a>
|
|||
|
|
|
|||
|
|
<a id="∃₂"></a><a id="1483" href="Data.Product.html#1483" class="Function">∃₂</a> <a id="1486" class="Symbol">:</a> <a id="1488" class="Symbol">∀</a> <a id="1490" class="Symbol">{</a><a id="1491" href="Data.Product.html#1491" class="Bound">A</a> <a id="1493" class="Symbol">:</a> <a id="1495" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1499" href="Data.Product.html#386" class="Generalizable">a</a><a id="1500" class="Symbol">}</a> <a id="1502" class="Symbol">{</a><a id="1503" href="Data.Product.html#1503" class="Bound">B</a> <a id="1505" class="Symbol">:</a> <a id="1507" href="Data.Product.html#1491" class="Bound">A</a> <a id="1509" class="Symbol">→</a> <a id="1511" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1515" href="Data.Product.html#388" class="Generalizable">b</a><a id="1516" class="Symbol">}</a>
|
|||
|
|
<a id="1523" class="Symbol">(</a><a id="1524" href="Data.Product.html#1524" class="Bound">C</a> <a id="1526" class="Symbol">:</a> <a id="1528" class="Symbol">(</a><a id="1529" href="Data.Product.html#1529" class="Bound">x</a> <a id="1531" class="Symbol">:</a> <a id="1533" href="Data.Product.html#1491" class="Bound">A</a><a id="1534" class="Symbol">)</a> <a id="1536" class="Symbol">→</a> <a id="1538" href="Data.Product.html#1503" class="Bound">B</a> <a id="1540" href="Data.Product.html#1529" class="Bound">x</a> <a id="1542" class="Symbol">→</a> <a id="1544" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1548" href="Data.Product.html#390" class="Generalizable">c</a><a id="1549" class="Symbol">)</a> <a id="1551" class="Symbol">→</a> <a id="1553" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1557" class="Symbol">(</a><a id="1558" href="Data.Product.html#386" class="Generalizable">a</a> <a id="1560" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1562" href="Data.Product.html#388" class="Generalizable">b</a> <a id="1564" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1566" href="Data.Product.html#390" class="Generalizable">c</a><a id="1567" class="Symbol">)</a>
|
|||
|
|
<a id="1569" href="Data.Product.html#1483" class="Function">∃₂</a> <a id="1572" href="Data.Product.html#1572" class="Bound">C</a> <a id="1574" class="Symbol">=</a> <a id="1576" href="Data.Product.html#1369" class="Function">∃</a> <a id="1578" class="Symbol">λ</a> <a id="1580" href="Data.Product.html#1580" class="Bound">a</a> <a id="1582" class="Symbol">→</a> <a id="1584" href="Data.Product.html#1369" class="Function">∃</a> <a id="1586" class="Symbol">λ</a> <a id="1588" href="Data.Product.html#1588" class="Bound">b</a> <a id="1590" class="Symbol">→</a> <a id="1592" href="Data.Product.html#1572" class="Bound">C</a> <a id="1594" href="Data.Product.html#1580" class="Bound">a</a> <a id="1596" href="Data.Product.html#1588" class="Bound">b</a>
|
|||
|
|
|
|||
|
|
<a id="1599" class="Comment">-- Unique existence (parametrised by an underlying equality).</a>
|
|||
|
|
|
|||
|
|
<a id="∃!"></a><a id="1662" href="Data.Product.html#1662" class="Function">∃!</a> <a id="1665" class="Symbol">:</a> <a id="1667" class="Symbol">{</a><a id="1668" href="Data.Product.html#1668" class="Bound">A</a> <a id="1670" class="Symbol">:</a> <a id="1672" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1676" href="Data.Product.html#386" class="Generalizable">a</a><a id="1677" class="Symbol">}</a> <a id="1679" class="Symbol">→</a> <a id="1681" class="Symbol">(</a><a id="1682" href="Data.Product.html#1668" class="Bound">A</a> <a id="1684" class="Symbol">→</a> <a id="1686" href="Data.Product.html#1668" class="Bound">A</a> <a id="1688" class="Symbol">→</a> <a id="1690" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1694" href="Data.Product.html#398" class="Generalizable">ℓ</a><a id="1695" class="Symbol">)</a> <a id="1697" class="Symbol">→</a> <a id="1699" class="Symbol">(</a><a id="1700" href="Data.Product.html#1668" class="Bound">A</a> <a id="1702" class="Symbol">→</a> <a id="1704" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1708" href="Data.Product.html#388" class="Generalizable">b</a><a id="1709" class="Symbol">)</a> <a id="1711" class="Symbol">→</a> <a id="1713" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1717" class="Symbol">(</a><a id="1718" href="Data.Product.html#386" class="Generalizable">a</a> <a id="1720" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1722" href="Data.Product.html#388" class="Generalizable">b</a> <a id="1724" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1726" href="Data.Product.html#398" class="Generalizable">ℓ</a><a id="1727" class="Symbol">)</a>
|
|||
|
|
<a id="1729" href="Data.Product.html#1662" class="Function">∃!</a> <a id="1732" href="Data.Product.html#1732" class="Bound Operator">_≈_</a> <a id="1736" href="Data.Product.html#1736" class="Bound">B</a> <a id="1738" class="Symbol">=</a> <a id="1740" href="Data.Product.html#1369" class="Function">∃</a> <a id="1742" class="Symbol">λ</a> <a id="1744" href="Data.Product.html#1744" class="Bound">x</a> <a id="1746" class="Symbol">→</a> <a id="1748" href="Data.Product.html#1736" class="Bound">B</a> <a id="1750" href="Data.Product.html#1744" class="Bound">x</a> <a id="1752" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="1754" class="Symbol">(∀</a> <a id="1757" class="Symbol">{</a><a id="1758" href="Data.Product.html#1758" class="Bound">y</a><a id="1759" class="Symbol">}</a> <a id="1761" class="Symbol">→</a> <a id="1763" href="Data.Product.html#1736" class="Bound">B</a> <a id="1765" href="Data.Product.html#1758" class="Bound">y</a> <a id="1767" class="Symbol">→</a> <a id="1769" href="Data.Product.html#1744" class="Bound">x</a> <a id="1771" href="Data.Product.html#1732" class="Bound Operator">≈</a> <a id="1773" href="Data.Product.html#1758" class="Bound">y</a><a id="1774" class="Symbol">)</a>
|
|||
|
|
|
|||
|
|
<a id="1777" class="Comment">-- Syntax</a>
|
|||
|
|
|
|||
|
|
<a id="1788" class="Keyword">infix</a> <a id="1794" class="Number">2</a> <a id="1796" href="Data.Product.html#1806" class="Function">∃-syntax</a>
|
|||
|
|
|
|||
|
|
<a id="∃-syntax"></a><a id="1806" href="Data.Product.html#1806" class="Function">∃-syntax</a> <a id="1815" class="Symbol">:</a> <a id="1817" class="Symbol">∀</a> <a id="1819" class="Symbol">{</a><a id="1820" href="Data.Product.html#1820" class="Bound">A</a> <a id="1822" class="Symbol">:</a> <a id="1824" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1828" href="Data.Product.html#386" class="Generalizable">a</a><a id="1829" class="Symbol">}</a> <a id="1831" class="Symbol">→</a> <a id="1833" class="Symbol">(</a><a id="1834" href="Data.Product.html#1820" class="Bound">A</a> <a id="1836" class="Symbol">→</a> <a id="1838" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1842" href="Data.Product.html#388" class="Generalizable">b</a><a id="1843" class="Symbol">)</a> <a id="1845" class="Symbol">→</a> <a id="1847" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1851" class="Symbol">(</a><a id="1852" href="Data.Product.html#386" class="Generalizable">a</a> <a id="1854" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1856" href="Data.Product.html#388" class="Generalizable">b</a><a id="1857" class="Symbol">)</a>
|
|||
|
|
<a id="1859" href="Data.Product.html#1806" class="Function">∃-syntax</a> <a id="1868" class="Symbol">=</a> <a id="1870" href="Data.Product.html#1369" class="Function">∃</a>
|
|||
|
|
|
|||
|
|
<a id="1873" class="Keyword">syntax</a> <a id="1880" href="Data.Product.html#1806" class="Function">∃-syntax</a> <a id="1889" class="Symbol">(λ</a> <a id="1892" class="Bound">x</a> <a id="1894" class="Symbol">→</a> <a id="1896" class="Bound">B</a><a id="1897" class="Symbol">)</a> <a id="1899" class="Symbol">=</a> <a id="1901" class="Function">∃[</a> <a id="1904" class="Bound">x</a> <a id="1906" class="Function">]</a> <a id="1908" class="Bound">B</a>
|
|||
|
|
|
|||
|
|
<a id="1911" class="Keyword">infix</a> <a id="1917" class="Number">2</a> <a id="1919" href="Data.Product.html#1929" class="Function">∄-syntax</a>
|
|||
|
|
|
|||
|
|
<a id="∄-syntax"></a><a id="1929" href="Data.Product.html#1929" class="Function">∄-syntax</a> <a id="1938" class="Symbol">:</a> <a id="1940" class="Symbol">∀</a> <a id="1942" class="Symbol">{</a><a id="1943" href="Data.Product.html#1943" class="Bound">A</a> <a id="1945" class="Symbol">:</a> <a id="1947" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1951" href="Data.Product.html#386" class="Generalizable">a</a><a id="1952" class="Symbol">}</a> <a id="1954" class="Symbol">→</a> <a id="1956" class="Symbol">(</a><a id="1957" href="Data.Product.html#1943" class="Bound">A</a> <a id="1959" class="Symbol">→</a> <a id="1961" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1965" href="Data.Product.html#388" class="Generalizable">b</a><a id="1966" class="Symbol">)</a> <a id="1968" class="Symbol">→</a> <a id="1970" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1974" class="Symbol">(</a><a id="1975" href="Data.Product.html#386" class="Generalizable">a</a> <a id="1977" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1979" href="Data.Product.html#388" class="Generalizable">b</a><a id="1980" class="Symbol">)</a>
|
|||
|
|
<a id="1982" href="Data.Product.html#1929" class="Function">∄-syntax</a> <a id="1991" class="Symbol">=</a> <a id="1993" href="Data.Product.html#1424" class="Function">∄</a>
|
|||
|
|
|
|||
|
|
<a id="1996" class="Keyword">syntax</a> <a id="2003" href="Data.Product.html#1929" class="Function">∄-syntax</a> <a id="2012" class="Symbol">(λ</a> <a id="2015" class="Bound">x</a> <a id="2017" class="Symbol">→</a> <a id="2019" class="Bound">B</a><a id="2020" class="Symbol">)</a> <a id="2022" class="Symbol">=</a> <a id="2024" class="Function">∄[</a> <a id="2027" class="Bound">x</a> <a id="2029" class="Function">]</a> <a id="2031" class="Bound">B</a>
|
|||
|
|
|
|||
|
|
<a id="2034" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
<a id="2107" class="Comment">-- Operations over dependent products</a>
|
|||
|
|
|
|||
|
|
<a id="2146" class="Keyword">infix</a> <a id="2153" class="Number">4</a> <a id="2155" href="Data.Product.html#2247" class="Function Operator">-,_</a>
|
|||
|
|
<a id="2159" class="Keyword">infixr</a> <a id="2166" class="Number">2</a> <a id="2168" href="Data.Product.html#5362" class="Function Operator">_-×-_</a> <a id="2174" href="Data.Product.html#5447" class="Function Operator">_-,-_</a>
|
|||
|
|
<a id="2180" class="Keyword">infixl</a> <a id="2187" class="Number">2</a> <a id="2189" href="Data.Product.html#5095" class="Function Operator">_<*>_</a>
|
|||
|
|
|
|||
|
|
<a id="2196" class="Comment">-- Sometimes the first component can be inferred.</a>
|
|||
|
|
|
|||
|
|
<a id="-,_"></a><a id="2247" href="Data.Product.html#2247" class="Function Operator">-,_</a> <a id="2251" class="Symbol">:</a> <a id="2253" class="Symbol">∀</a> <a id="2255" class="Symbol">{</a><a id="2256" href="Data.Product.html#2256" class="Bound">A</a> <a id="2258" class="Symbol">:</a> <a id="2260" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2264" href="Data.Product.html#386" class="Generalizable">a</a><a id="2265" class="Symbol">}</a> <a id="2267" class="Symbol">{</a><a id="2268" href="Data.Product.html#2268" class="Bound">B</a> <a id="2270" class="Symbol">:</a> <a id="2272" href="Data.Product.html#2256" class="Bound">A</a> <a id="2274" class="Symbol">→</a> <a id="2276" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2280" href="Data.Product.html#388" class="Generalizable">b</a><a id="2281" class="Symbol">}</a> <a id="2283" class="Symbol">{</a><a id="2284" href="Data.Product.html#2284" class="Bound">x</a><a id="2285" class="Symbol">}</a> <a id="2287" class="Symbol">→</a> <a id="2289" href="Data.Product.html#2268" class="Bound">B</a> <a id="2291" href="Data.Product.html#2284" class="Bound">x</a> <a id="2293" class="Symbol">→</a> <a id="2295" href="Data.Product.html#1369" class="Function">∃</a> <a id="2297" href="Data.Product.html#2268" class="Bound">B</a>
|
|||
|
|
<a id="2299" href="Data.Product.html#2247" class="Function Operator">-,</a> <a id="2302" href="Data.Product.html#2302" class="Bound">y</a> <a id="2304" class="Symbol">=</a> <a id="2306" class="Symbol">_</a> <a id="2308" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="2310" href="Data.Product.html#2302" class="Bound">y</a>
|
|||
|
|
|
|||
|
|
<a id="<_,_>"></a><a id="2313" href="Data.Product.html#2313" class="Function Operator"><_,_></a> <a id="2319" class="Symbol">:</a> <a id="2321" class="Symbol">∀</a> <a id="2323" class="Symbol">{</a><a id="2324" href="Data.Product.html#2324" class="Bound">A</a> <a id="2326" class="Symbol">:</a> <a id="2328" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2332" href="Data.Product.html#386" class="Generalizable">a</a><a id="2333" class="Symbol">}</a> <a id="2335" class="Symbol">{</a><a id="2336" href="Data.Product.html#2336" class="Bound">B</a> <a id="2338" class="Symbol">:</a> <a id="2340" href="Data.Product.html#2324" class="Bound">A</a> <a id="2342" class="Symbol">→</a> <a id="2344" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2348" href="Data.Product.html#388" class="Generalizable">b</a><a id="2349" class="Symbol">}</a> <a id="2351" class="Symbol">{</a><a id="2352" href="Data.Product.html#2352" class="Bound">C</a> <a id="2354" class="Symbol">:</a> <a id="2356" class="Symbol">∀</a> <a id="2358" class="Symbol">{</a><a id="2359" href="Data.Product.html#2359" class="Bound">x</a><a id="2360" class="Symbol">}</a> <a id="2362" class="Symbol">→</a> <a id="2364" href="Data.Product.html#2336" class="Bound">B</a> <a id="2366" href="Data.Product.html#2359" class="Bound">x</a> <a id="2368" class="Symbol">→</a> <a id="2370" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2374" href="Data.Product.html#390" class="Generalizable">c</a><a id="2375" class="Symbol">}</a>
|
|||
|
|
<a id="2385" class="Symbol">(</a><a id="2386" href="Data.Product.html#2386" class="Bound">f</a> <a id="2388" class="Symbol">:</a> <a id="2390" class="Symbol">(</a><a id="2391" href="Data.Product.html#2391" class="Bound">x</a> <a id="2393" class="Symbol">:</a> <a id="2395" href="Data.Product.html#2324" class="Bound">A</a><a id="2396" class="Symbol">)</a> <a id="2398" class="Symbol">→</a> <a id="2400" href="Data.Product.html#2336" class="Bound">B</a> <a id="2402" href="Data.Product.html#2391" class="Bound">x</a><a id="2403" class="Symbol">)</a> <a id="2405" class="Symbol">→</a> <a id="2407" class="Symbol">((</a><a id="2409" href="Data.Product.html#2409" class="Bound">x</a> <a id="2411" class="Symbol">:</a> <a id="2413" href="Data.Product.html#2324" class="Bound">A</a><a id="2414" class="Symbol">)</a> <a id="2416" class="Symbol">→</a> <a id="2418" href="Data.Product.html#2352" class="Bound">C</a> <a id="2420" class="Symbol">(</a><a id="2421" href="Data.Product.html#2386" class="Bound">f</a> <a id="2423" href="Data.Product.html#2409" class="Bound">x</a><a id="2424" class="Symbol">))</a> <a id="2427" class="Symbol">→</a>
|
|||
|
|
<a id="2437" class="Symbol">((</a><a id="2439" href="Data.Product.html#2439" class="Bound">x</a> <a id="2441" class="Symbol">:</a> <a id="2443" href="Data.Product.html#2324" class="Bound">A</a><a id="2444" class="Symbol">)</a> <a id="2446" class="Symbol">→</a> <a id="2448" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="2450" class="Symbol">(</a><a id="2451" href="Data.Product.html#2336" class="Bound">B</a> <a id="2453" href="Data.Product.html#2439" class="Bound">x</a><a id="2454" class="Symbol">)</a> <a id="2456" href="Data.Product.html#2352" class="Bound">C</a><a id="2457" class="Symbol">)</a>
|
|||
|
|
<a id="2459" href="Data.Product.html#2313" class="Function Operator"><</a> <a id="2461" href="Data.Product.html#2461" class="Bound">f</a> <a id="2463" href="Data.Product.html#2313" class="Function Operator">,</a> <a id="2465" href="Data.Product.html#2465" class="Bound">g</a> <a id="2467" href="Data.Product.html#2313" class="Function Operator">></a> <a id="2469" href="Data.Product.html#2469" class="Bound">x</a> <a id="2471" class="Symbol">=</a> <a id="2473" class="Symbol">(</a><a id="2474" href="Data.Product.html#2461" class="Bound">f</a> <a id="2476" href="Data.Product.html#2469" class="Bound">x</a> <a id="2478" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="2480" href="Data.Product.html#2465" class="Bound">g</a> <a id="2482" href="Data.Product.html#2469" class="Bound">x</a><a id="2483" class="Symbol">)</a>
|
|||
|
|
|
|||
|
|
<a id="map"></a><a id="2486" href="Data.Product.html#2486" class="Function">map</a> <a id="2490" class="Symbol">:</a> <a id="2492" class="Symbol">∀</a> <a id="2494" class="Symbol">{</a><a id="2495" href="Data.Product.html#2495" class="Bound">P</a> <a id="2497" class="Symbol">:</a> <a id="2499" href="Data.Product.html#418" class="Generalizable">A</a> <a id="2501" class="Symbol">→</a> <a id="2503" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2507" href="Data.Product.html#400" class="Generalizable">p</a><a id="2508" class="Symbol">}</a> <a id="2510" class="Symbol">{</a><a id="2511" href="Data.Product.html#2511" class="Bound">Q</a> <a id="2513" class="Symbol">:</a> <a id="2515" href="Data.Product.html#432" class="Generalizable">B</a> <a id="2517" class="Symbol">→</a> <a id="2519" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2523" href="Data.Product.html#402" class="Generalizable">q</a><a id="2524" class="Symbol">}</a> <a id="2526" class="Symbol">→</a>
|
|||
|
|
<a id="2534" class="Symbol">(</a><a id="2535" href="Data.Product.html#2535" class="Bound">f</a> <a id="2537" class="Symbol">:</a> <a id="2539" href="Data.Product.html#418" class="Generalizable">A</a> <a id="2541" class="Symbol">→</a> <a id="2543" href="Data.Product.html#432" class="Generalizable">B</a><a id="2544" class="Symbol">)</a> <a id="2546" class="Symbol">→</a> <a id="2548" class="Symbol">(∀</a> <a id="2551" class="Symbol">{</a><a id="2552" href="Data.Product.html#2552" class="Bound">x</a><a id="2553" class="Symbol">}</a> <a id="2555" class="Symbol">→</a> <a id="2557" href="Data.Product.html#2495" class="Bound">P</a> <a id="2559" href="Data.Product.html#2552" class="Bound">x</a> <a id="2561" class="Symbol">→</a> <a id="2563" href="Data.Product.html#2511" class="Bound">Q</a> <a id="2565" class="Symbol">(</a><a id="2566" href="Data.Product.html#2535" class="Bound">f</a> <a id="2568" href="Data.Product.html#2552" class="Bound">x</a><a id="2569" class="Symbol">))</a> <a id="2572" class="Symbol">→</a>
|
|||
|
|
<a id="2580" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="2582" href="Data.Product.html#418" class="Generalizable">A</a> <a id="2584" href="Data.Product.html#2495" class="Bound">P</a> <a id="2586" class="Symbol">→</a> <a id="2588" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="2590" href="Data.Product.html#432" class="Generalizable">B</a> <a id="2592" href="Data.Product.html#2511" class="Bound">Q</a>
|
|||
|
|
<a id="2594" href="Data.Product.html#2486" class="Function">map</a> <a id="2598" href="Data.Product.html#2598" class="Bound">f</a> <a id="2600" href="Data.Product.html#2600" class="Bound">g</a> <a id="2602" class="Symbol">(</a><a id="2603" href="Data.Product.html#2603" class="Bound">x</a> <a id="2605" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="2607" href="Data.Product.html#2607" class="Bound">y</a><a id="2608" class="Symbol">)</a> <a id="2610" class="Symbol">=</a> <a id="2612" class="Symbol">(</a><a id="2613" href="Data.Product.html#2598" class="Bound">f</a> <a id="2615" href="Data.Product.html#2603" class="Bound">x</a> <a id="2617" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="2619" href="Data.Product.html#2600" class="Bound">g</a> <a id="2621" href="Data.Product.html#2607" class="Bound">y</a><a id="2622" class="Symbol">)</a>
|
|||
|
|
|
|||
|
|
<a id="map₁"></a><a id="2625" href="Data.Product.html#2625" class="Function">map₁</a> <a id="2630" class="Symbol">:</a> <a id="2632" class="Symbol">(</a><a id="2633" href="Data.Product.html#418" class="Generalizable">A</a> <a id="2635" class="Symbol">→</a> <a id="2637" href="Data.Product.html#432" class="Generalizable">B</a><a id="2638" class="Symbol">)</a> <a id="2640" class="Symbol">→</a> <a id="2642" href="Data.Product.html#418" class="Generalizable">A</a> <a id="2644" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="2646" href="Data.Product.html#446" class="Generalizable">C</a> <a id="2648" class="Symbol">→</a> <a id="2650" href="Data.Product.html#432" class="Generalizable">B</a> <a id="2652" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="2654" href="Data.Product.html#446" class="Generalizable">C</a>
|
|||
|
|
<a id="2656" href="Data.Product.html#2625" class="Function">map₁</a> <a id="2661" href="Data.Product.html#2661" class="Bound">f</a> <a id="2663" class="Symbol">=</a> <a id="2665" href="Data.Product.html#2486" class="Function">map</a> <a id="2669" href="Data.Product.html#2661" class="Bound">f</a> <a id="2671" href="Function.Base.html#615" class="Function">id</a>
|
|||
|
|
|
|||
|
|
<a id="map₂"></a><a id="2675" href="Data.Product.html#2675" class="Function">map₂</a> <a id="2680" class="Symbol">:</a> <a id="2682" class="Symbol">∀</a> <a id="2684" class="Symbol">{</a><a id="2685" href="Data.Product.html#2685" class="Bound">A</a> <a id="2687" class="Symbol">:</a> <a id="2689" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2693" href="Data.Product.html#386" class="Generalizable">a</a><a id="2694" class="Symbol">}</a> <a id="2696" class="Symbol">{</a><a id="2697" href="Data.Product.html#2697" class="Bound">B</a> <a id="2699" class="Symbol">:</a> <a id="2701" href="Data.Product.html#2685" class="Bound">A</a> <a id="2703" class="Symbol">→</a> <a id="2705" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2709" href="Data.Product.html#388" class="Generalizable">b</a><a id="2710" class="Symbol">}</a> <a id="2712" class="Symbol">{</a><a id="2713" href="Data.Product.html#2713" class="Bound">C</a> <a id="2715" class="Symbol">:</a> <a id="2717" href="Data.Product.html#2685" class="Bound">A</a> <a id="2719" class="Symbol">→</a> <a id="2721" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2725" href="Data.Product.html#390" class="Generalizable">c</a><a id="2726" class="Symbol">}</a> <a id="2728" class="Symbol">→</a>
|
|||
|
|
<a id="2737" class="Symbol">(∀</a> <a id="2740" class="Symbol">{</a><a id="2741" href="Data.Product.html#2741" class="Bound">x</a><a id="2742" class="Symbol">}</a> <a id="2744" class="Symbol">→</a> <a id="2746" href="Data.Product.html#2697" class="Bound">B</a> <a id="2748" href="Data.Product.html#2741" class="Bound">x</a> <a id="2750" class="Symbol">→</a> <a id="2752" href="Data.Product.html#2713" class="Bound">C</a> <a id="2754" href="Data.Product.html#2741" class="Bound">x</a><a id="2755" class="Symbol">)</a> <a id="2757" class="Symbol">→</a> <a id="2759" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="2761" href="Data.Product.html#2685" class="Bound">A</a> <a id="2763" href="Data.Product.html#2697" class="Bound">B</a> <a id="2765" class="Symbol">→</a> <a id="2767" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="2769" href="Data.Product.html#2685" class="Bound">A</a> <a id="2771" href="Data.Product.html#2713" class="Bound">C</a>
|
|||
|
|
<a id="2773" href="Data.Product.html#2675" class="Function">map₂</a> <a id="2778" href="Data.Product.html#2778" class="Bound">f</a> <a id="2780" class="Symbol">=</a> <a id="2782" href="Data.Product.html#2486" class="Function">map</a> <a id="2786" href="Function.Base.html#615" class="Function">id</a> <a id="2789" href="Data.Product.html#2778" class="Bound">f</a>
|
|||
|
|
|
|||
|
|
<a id="2792" class="Comment">-- A version of map where the output can depend on the input</a>
|
|||
|
|
<a id="dmap"></a><a id="2853" href="Data.Product.html#2853" class="Function">dmap</a> <a id="2858" class="Symbol">:</a> <a id="2860" class="Symbol">∀</a> <a id="2862" class="Symbol">{</a><a id="2863" href="Data.Product.html#2863" class="Bound">B</a> <a id="2865" class="Symbol">:</a> <a id="2867" href="Data.Product.html#418" class="Generalizable">A</a> <a id="2869" class="Symbol">→</a> <a id="2871" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2875" href="Data.Product.html#388" class="Generalizable">b</a><a id="2876" class="Symbol">}</a> <a id="2878" class="Symbol">{</a><a id="2879" href="Data.Product.html#2879" class="Bound">P</a> <a id="2881" class="Symbol">:</a> <a id="2883" href="Data.Product.html#418" class="Generalizable">A</a> <a id="2885" class="Symbol">→</a> <a id="2887" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2891" href="Data.Product.html#400" class="Generalizable">p</a><a id="2892" class="Symbol">}</a> <a id="2894" class="Symbol">{</a><a id="2895" href="Data.Product.html#2895" class="Bound">Q</a> <a id="2897" class="Symbol">:</a> <a id="2899" class="Symbol">∀</a> <a id="2901" class="Symbol">{</a><a id="2902" href="Data.Product.html#2902" class="Bound">a</a><a id="2903" class="Symbol">}</a> <a id="2905" class="Symbol">→</a> <a id="2907" href="Data.Product.html#2879" class="Bound">P</a> <a id="2909" href="Data.Product.html#2902" class="Bound">a</a> <a id="2911" class="Symbol">→</a> <a id="2913" href="Data.Product.html#2863" class="Bound">B</a> <a id="2915" href="Data.Product.html#2902" class="Bound">a</a> <a id="2917" class="Symbol">→</a> <a id="2919" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2923" href="Data.Product.html#402" class="Generalizable">q</a><a id="2924" class="Symbol">}</a> <a id="2926" class="Symbol">→</a>
|
|||
|
|
<a id="2935" class="Symbol">(</a><a id="2936" href="Data.Product.html#2936" class="Bound">f</a> <a id="2938" class="Symbol">:</a> <a id="2940" class="Symbol">(</a><a id="2941" href="Data.Product.html#2941" class="Bound">a</a> <a id="2943" class="Symbol">:</a> <a id="2945" href="Data.Product.html#418" class="Generalizable">A</a><a id="2946" class="Symbol">)</a> <a id="2948" class="Symbol">→</a> <a id="2950" href="Data.Product.html#2863" class="Bound">B</a> <a id="2952" href="Data.Product.html#2941" class="Bound">a</a><a id="2953" class="Symbol">)</a> <a id="2955" class="Symbol">→</a> <a id="2957" class="Symbol">(∀</a> <a id="2960" class="Symbol">{</a><a id="2961" href="Data.Product.html#2961" class="Bound">a</a><a id="2962" class="Symbol">}</a> <a id="2964" class="Symbol">(</a><a id="2965" href="Data.Product.html#2965" class="Bound">b</a> <a id="2967" class="Symbol">:</a> <a id="2969" href="Data.Product.html#2879" class="Bound">P</a> <a id="2971" href="Data.Product.html#2961" class="Bound">a</a><a id="2972" class="Symbol">)</a> <a id="2974" class="Symbol">→</a> <a id="2976" href="Data.Product.html#2895" class="Bound">Q</a> <a id="2978" href="Data.Product.html#2965" class="Bound">b</a> <a id="2980" class="Symbol">(</a><a id="2981" href="Data.Product.html#2936" class="Bound">f</a> <a id="2983" href="Data.Product.html#2961" class="Bound">a</a><a id="2984" class="Symbol">))</a> <a id="2987" class="Symbol">→</a>
|
|||
|
|
<a id="2996" class="Symbol">(</a><a id="2997" href="Data.Product.html#2997" class="Bound">(</a><a id="2998" href="Data.Product.html#2998" class="Bound">a</a> <a id="3000" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3002" href="Data.Product.html#3002" class="Bound">b</a><a id="3003" href="Data.Product.html#2997" class="Bound">)</a> <a id="3005" class="Symbol">:</a> <a id="3007" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3009" href="Data.Product.html#418" class="Generalizable">A</a> <a id="3011" href="Data.Product.html#2879" class="Bound">P</a><a id="3012" class="Symbol">)</a> <a id="3014" class="Symbol">→</a> <a id="3016" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3018" class="Symbol">(</a><a id="3019" href="Data.Product.html#2863" class="Bound">B</a> <a id="3021" href="Data.Product.html#2998" class="Bound">a</a><a id="3022" class="Symbol">)</a> <a id="3024" class="Symbol">(</a><a id="3025" href="Data.Product.html#2895" class="Bound">Q</a> <a id="3027" href="Data.Product.html#3002" class="Bound">b</a><a id="3028" class="Symbol">)</a>
|
|||
|
|
<a id="3030" href="Data.Product.html#2853" class="Function">dmap</a> <a id="3035" href="Data.Product.html#3035" class="Bound">f</a> <a id="3037" href="Data.Product.html#3037" class="Bound">g</a> <a id="3039" class="Symbol">(</a><a id="3040" href="Data.Product.html#3040" class="Bound">x</a> <a id="3042" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3044" href="Data.Product.html#3044" class="Bound">y</a><a id="3045" class="Symbol">)</a> <a id="3047" class="Symbol">=</a> <a id="3049" href="Data.Product.html#3035" class="Bound">f</a> <a id="3051" href="Data.Product.html#3040" class="Bound">x</a> <a id="3053" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3055" href="Data.Product.html#3037" class="Bound">g</a> <a id="3057" href="Data.Product.html#3044" class="Bound">y</a>
|
|||
|
|
|
|||
|
|
<a id="zip"></a><a id="3060" href="Data.Product.html#3060" class="Function">zip</a> <a id="3064" class="Symbol">:</a> <a id="3066" class="Symbol">∀</a> <a id="3068" class="Symbol">{</a><a id="3069" href="Data.Product.html#3069" class="Bound">P</a> <a id="3071" class="Symbol">:</a> <a id="3073" href="Data.Product.html#418" class="Generalizable">A</a> <a id="3075" class="Symbol">→</a> <a id="3077" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3081" href="Data.Product.html#400" class="Generalizable">p</a><a id="3082" class="Symbol">}</a> <a id="3084" class="Symbol">{</a><a id="3085" href="Data.Product.html#3085" class="Bound">Q</a> <a id="3087" class="Symbol">:</a> <a id="3089" href="Data.Product.html#432" class="Generalizable">B</a> <a id="3091" class="Symbol">→</a> <a id="3093" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3097" href="Data.Product.html#402" class="Generalizable">q</a><a id="3098" class="Symbol">}</a> <a id="3100" class="Symbol">{</a><a id="3101" href="Data.Product.html#3101" class="Bound">R</a> <a id="3103" class="Symbol">:</a> <a id="3105" href="Data.Product.html#446" class="Generalizable">C</a> <a id="3107" class="Symbol">→</a> <a id="3109" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3113" href="Data.Product.html#404" class="Generalizable">r</a><a id="3114" class="Symbol">}</a> <a id="3116" class="Symbol">→</a>
|
|||
|
|
<a id="3124" class="Symbol">(</a><a id="3125" href="Data.Product.html#3125" class="Bound Operator">_∙_</a> <a id="3129" class="Symbol">:</a> <a id="3131" href="Data.Product.html#418" class="Generalizable">A</a> <a id="3133" class="Symbol">→</a> <a id="3135" href="Data.Product.html#432" class="Generalizable">B</a> <a id="3137" class="Symbol">→</a> <a id="3139" href="Data.Product.html#446" class="Generalizable">C</a><a id="3140" class="Symbol">)</a> <a id="3142" class="Symbol">→</a>
|
|||
|
|
<a id="3150" class="Symbol">(∀</a> <a id="3153" class="Symbol">{</a><a id="3154" href="Data.Product.html#3154" class="Bound">x</a> <a id="3156" href="Data.Product.html#3156" class="Bound">y</a><a id="3157" class="Symbol">}</a> <a id="3159" class="Symbol">→</a> <a id="3161" href="Data.Product.html#3069" class="Bound">P</a> <a id="3163" href="Data.Product.html#3154" class="Bound">x</a> <a id="3165" class="Symbol">→</a> <a id="3167" href="Data.Product.html#3085" class="Bound">Q</a> <a id="3169" href="Data.Product.html#3156" class="Bound">y</a> <a id="3171" class="Symbol">→</a> <a id="3173" href="Data.Product.html#3101" class="Bound">R</a> <a id="3175" class="Symbol">(</a><a id="3176" href="Data.Product.html#3154" class="Bound">x</a> <a id="3178" href="Data.Product.html#3125" class="Bound Operator">∙</a> <a id="3180" href="Data.Product.html#3156" class="Bound">y</a><a id="3181" class="Symbol">))</a> <a id="3184" class="Symbol">→</a>
|
|||
|
|
<a id="3192" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3194" href="Data.Product.html#418" class="Generalizable">A</a> <a id="3196" href="Data.Product.html#3069" class="Bound">P</a> <a id="3198" class="Symbol">→</a> <a id="3200" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3202" href="Data.Product.html#432" class="Generalizable">B</a> <a id="3204" href="Data.Product.html#3085" class="Bound">Q</a> <a id="3206" class="Symbol">→</a> <a id="3208" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3210" href="Data.Product.html#446" class="Generalizable">C</a> <a id="3212" href="Data.Product.html#3101" class="Bound">R</a>
|
|||
|
|
<a id="3214" href="Data.Product.html#3060" class="Function">zip</a> <a id="3218" href="Data.Product.html#3218" class="Bound Operator">_∙_</a> <a id="3222" href="Data.Product.html#3222" class="Bound Operator">_∘_</a> <a id="3226" class="Symbol">(</a><a id="3227" href="Data.Product.html#3227" class="Bound">a</a> <a id="3229" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3231" href="Data.Product.html#3231" class="Bound">p</a><a id="3232" class="Symbol">)</a> <a id="3234" class="Symbol">(</a><a id="3235" href="Data.Product.html#3235" class="Bound">b</a> <a id="3237" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3239" href="Data.Product.html#3239" class="Bound">q</a><a id="3240" class="Symbol">)</a> <a id="3242" class="Symbol">=</a> <a id="3244" class="Symbol">((</a><a id="3246" href="Data.Product.html#3227" class="Bound">a</a> <a id="3248" href="Data.Product.html#3218" class="Bound Operator">∙</a> <a id="3250" href="Data.Product.html#3235" class="Bound">b</a><a id="3251" class="Symbol">)</a> <a id="3253" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3255" class="Symbol">(</a><a id="3256" href="Data.Product.html#3231" class="Bound">p</a> <a id="3258" href="Data.Product.html#3222" class="Bound Operator">∘</a> <a id="3260" href="Data.Product.html#3239" class="Bound">q</a><a id="3261" class="Symbol">))</a>
|
|||
|
|
|
|||
|
|
<a id="curry"></a><a id="3265" href="Data.Product.html#3265" class="Function">curry</a> <a id="3271" class="Symbol">:</a> <a id="3273" class="Symbol">∀</a> <a id="3275" class="Symbol">{</a><a id="3276" href="Data.Product.html#3276" class="Bound">A</a> <a id="3278" class="Symbol">:</a> <a id="3280" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3284" href="Data.Product.html#386" class="Generalizable">a</a><a id="3285" class="Symbol">}</a> <a id="3287" class="Symbol">{</a><a id="3288" href="Data.Product.html#3288" class="Bound">B</a> <a id="3290" class="Symbol">:</a> <a id="3292" href="Data.Product.html#3276" class="Bound">A</a> <a id="3294" class="Symbol">→</a> <a id="3296" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3300" href="Data.Product.html#388" class="Generalizable">b</a><a id="3301" class="Symbol">}</a> <a id="3303" class="Symbol">{</a><a id="3304" href="Data.Product.html#3304" class="Bound">C</a> <a id="3306" class="Symbol">:</a> <a id="3308" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3310" href="Data.Product.html#3276" class="Bound">A</a> <a id="3312" href="Data.Product.html#3288" class="Bound">B</a> <a id="3314" class="Symbol">→</a> <a id="3316" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3320" href="Data.Product.html#390" class="Generalizable">c</a><a id="3321" class="Symbol">}</a> <a id="3323" class="Symbol">→</a>
|
|||
|
|
<a id="3333" class="Symbol">((</a><a id="3335" href="Data.Product.html#3335" class="Bound">p</a> <a id="3337" class="Symbol">:</a> <a id="3339" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3341" href="Data.Product.html#3276" class="Bound">A</a> <a id="3343" href="Data.Product.html#3288" class="Bound">B</a><a id="3344" class="Symbol">)</a> <a id="3346" class="Symbol">→</a> <a id="3348" href="Data.Product.html#3304" class="Bound">C</a> <a id="3350" href="Data.Product.html#3335" class="Bound">p</a><a id="3351" class="Symbol">)</a> <a id="3353" class="Symbol">→</a>
|
|||
|
|
<a id="3363" class="Symbol">((</a><a id="3365" href="Data.Product.html#3365" class="Bound">x</a> <a id="3367" class="Symbol">:</a> <a id="3369" href="Data.Product.html#3276" class="Bound">A</a><a id="3370" class="Symbol">)</a> <a id="3372" class="Symbol">→</a> <a id="3374" class="Symbol">(</a><a id="3375" href="Data.Product.html#3375" class="Bound">y</a> <a id="3377" class="Symbol">:</a> <a id="3379" href="Data.Product.html#3288" class="Bound">B</a> <a id="3381" href="Data.Product.html#3365" class="Bound">x</a><a id="3382" class="Symbol">)</a> <a id="3384" class="Symbol">→</a> <a id="3386" href="Data.Product.html#3304" class="Bound">C</a> <a id="3388" class="Symbol">(</a><a id="3389" href="Data.Product.html#3365" class="Bound">x</a> <a id="3391" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3393" href="Data.Product.html#3375" class="Bound">y</a><a id="3394" class="Symbol">))</a>
|
|||
|
|
<a id="3397" href="Data.Product.html#3265" class="Function">curry</a> <a id="3403" href="Data.Product.html#3403" class="Bound">f</a> <a id="3405" href="Data.Product.html#3405" class="Bound">x</a> <a id="3407" href="Data.Product.html#3407" class="Bound">y</a> <a id="3409" class="Symbol">=</a> <a id="3411" href="Data.Product.html#3403" class="Bound">f</a> <a id="3413" class="Symbol">(</a><a id="3414" href="Data.Product.html#3405" class="Bound">x</a> <a id="3416" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3418" href="Data.Product.html#3407" class="Bound">y</a><a id="3419" class="Symbol">)</a>
|
|||
|
|
|
|||
|
|
<a id="uncurry"></a><a id="3422" href="Data.Product.html#3422" class="Function">uncurry</a> <a id="3430" class="Symbol">:</a> <a id="3432" class="Symbol">∀</a> <a id="3434" class="Symbol">{</a><a id="3435" href="Data.Product.html#3435" class="Bound">A</a> <a id="3437" class="Symbol">:</a> <a id="3439" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3443" href="Data.Product.html#386" class="Generalizable">a</a><a id="3444" class="Symbol">}</a> <a id="3446" class="Symbol">{</a><a id="3447" href="Data.Product.html#3447" class="Bound">B</a> <a id="3449" class="Symbol">:</a> <a id="3451" href="Data.Product.html#3435" class="Bound">A</a> <a id="3453" class="Symbol">→</a> <a id="3455" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3459" href="Data.Product.html#388" class="Generalizable">b</a><a id="3460" class="Symbol">}</a> <a id="3462" class="Symbol">{</a><a id="3463" href="Data.Product.html#3463" class="Bound">C</a> <a id="3465" class="Symbol">:</a> <a id="3467" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3469" href="Data.Product.html#3435" class="Bound">A</a> <a id="3471" href="Data.Product.html#3447" class="Bound">B</a> <a id="3473" class="Symbol">→</a> <a id="3475" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3479" href="Data.Product.html#390" class="Generalizable">c</a><a id="3480" class="Symbol">}</a> <a id="3482" class="Symbol">→</a>
|
|||
|
|
<a id="3494" class="Symbol">((</a><a id="3496" href="Data.Product.html#3496" class="Bound">x</a> <a id="3498" class="Symbol">:</a> <a id="3500" href="Data.Product.html#3435" class="Bound">A</a><a id="3501" class="Symbol">)</a> <a id="3503" class="Symbol">→</a> <a id="3505" class="Symbol">(</a><a id="3506" href="Data.Product.html#3506" class="Bound">y</a> <a id="3508" class="Symbol">:</a> <a id="3510" href="Data.Product.html#3447" class="Bound">B</a> <a id="3512" href="Data.Product.html#3496" class="Bound">x</a><a id="3513" class="Symbol">)</a> <a id="3515" class="Symbol">→</a> <a id="3517" href="Data.Product.html#3463" class="Bound">C</a> <a id="3519" class="Symbol">(</a><a id="3520" href="Data.Product.html#3496" class="Bound">x</a> <a id="3522" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3524" href="Data.Product.html#3506" class="Bound">y</a><a id="3525" class="Symbol">))</a> <a id="3528" class="Symbol">→</a>
|
|||
|
|
<a id="3540" class="Symbol">((</a><a id="3542" href="Data.Product.html#3542" class="Bound">p</a> <a id="3544" class="Symbol">:</a> <a id="3546" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3548" href="Data.Product.html#3435" class="Bound">A</a> <a id="3550" href="Data.Product.html#3447" class="Bound">B</a><a id="3551" class="Symbol">)</a> <a id="3553" class="Symbol">→</a> <a id="3555" href="Data.Product.html#3463" class="Bound">C</a> <a id="3557" href="Data.Product.html#3542" class="Bound">p</a><a id="3558" class="Symbol">)</a>
|
|||
|
|
<a id="3560" href="Data.Product.html#3422" class="Function">uncurry</a> <a id="3568" href="Data.Product.html#3568" class="Bound">f</a> <a id="3570" class="Symbol">(</a><a id="3571" href="Data.Product.html#3571" class="Bound">x</a> <a id="3573" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3575" href="Data.Product.html#3575" class="Bound">y</a><a id="3576" class="Symbol">)</a> <a id="3578" class="Symbol">=</a> <a id="3580" href="Data.Product.html#3568" class="Bound">f</a> <a id="3582" href="Data.Product.html#3571" class="Bound">x</a> <a id="3584" href="Data.Product.html#3575" class="Bound">y</a>
|
|||
|
|
|
|||
|
|
<a id="3587" class="Comment">-- Rewriting dependent products</a>
|
|||
|
|
<a id="assocʳ"></a><a id="3619" href="Data.Product.html#3619" class="Function">assocʳ</a> <a id="3626" class="Symbol">:</a> <a id="3628" class="Symbol">{</a><a id="3629" href="Data.Product.html#3629" class="Bound">B</a> <a id="3631" class="Symbol">:</a> <a id="3633" href="Data.Product.html#418" class="Generalizable">A</a> <a id="3635" class="Symbol">→</a> <a id="3637" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3641" href="Data.Product.html#388" class="Generalizable">b</a><a id="3642" class="Symbol">}</a> <a id="3644" class="Symbol">{</a><a id="3645" href="Data.Product.html#3645" class="Bound">C</a> <a id="3647" class="Symbol">:</a> <a id="3649" class="Symbol">(</a><a id="3650" href="Data.Product.html#3650" class="Bound">a</a> <a id="3652" class="Symbol">:</a> <a id="3654" href="Data.Product.html#418" class="Generalizable">A</a><a id="3655" class="Symbol">)</a> <a id="3657" class="Symbol">→</a> <a id="3659" href="Data.Product.html#3629" class="Bound">B</a> <a id="3661" href="Data.Product.html#3650" class="Bound">a</a> <a id="3663" class="Symbol">→</a> <a id="3665" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3669" href="Data.Product.html#390" class="Generalizable">c</a><a id="3670" class="Symbol">}</a> <a id="3672" class="Symbol">→</a>
|
|||
|
|
<a id="3684" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3686" class="Symbol">(</a><a id="3687" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3689" href="Data.Product.html#418" class="Generalizable">A</a> <a id="3691" href="Data.Product.html#3629" class="Bound">B</a><a id="3692" class="Symbol">)</a> <a id="3694" class="Symbol">(</a><a id="3695" href="Data.Product.html#3422" class="Function">uncurry</a> <a id="3703" href="Data.Product.html#3645" class="Bound">C</a><a id="3704" class="Symbol">)</a> <a id="3706" class="Symbol">→</a> <a id="3708" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3710" href="Data.Product.html#418" class="Generalizable">A</a> <a id="3712" class="Symbol">(λ</a> <a id="3715" href="Data.Product.html#3715" class="Bound">a</a> <a id="3717" class="Symbol">→</a> <a id="3719" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3721" class="Symbol">(</a><a id="3722" href="Data.Product.html#3629" class="Bound">B</a> <a id="3724" href="Data.Product.html#3715" class="Bound">a</a><a id="3725" class="Symbol">)</a> <a id="3727" class="Symbol">(</a><a id="3728" href="Data.Product.html#3645" class="Bound">C</a> <a id="3730" href="Data.Product.html#3715" class="Bound">a</a><a id="3731" class="Symbol">))</a>
|
|||
|
|
<a id="3734" href="Data.Product.html#3619" class="Function">assocʳ</a> <a id="3741" class="Symbol">((</a><a id="3743" href="Data.Product.html#3743" class="Bound">a</a> <a id="3745" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3747" href="Data.Product.html#3747" class="Bound">b</a><a id="3748" class="Symbol">)</a> <a id="3750" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3752" href="Data.Product.html#3752" class="Bound">c</a><a id="3753" class="Symbol">)</a> <a id="3755" class="Symbol">=</a> <a id="3757" class="Symbol">(</a><a id="3758" href="Data.Product.html#3743" class="Bound">a</a> <a id="3760" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3762" class="Symbol">(</a><a id="3763" href="Data.Product.html#3747" class="Bound">b</a> <a id="3765" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3767" href="Data.Product.html#3752" class="Bound">c</a><a id="3768" class="Symbol">))</a>
|
|||
|
|
|
|||
|
|
<a id="assocˡ"></a><a id="3772" href="Data.Product.html#3772" class="Function">assocˡ</a> <a id="3779" class="Symbol">:</a> <a id="3781" class="Symbol">{</a><a id="3782" href="Data.Product.html#3782" class="Bound">B</a> <a id="3784" class="Symbol">:</a> <a id="3786" href="Data.Product.html#418" class="Generalizable">A</a> <a id="3788" class="Symbol">→</a> <a id="3790" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3794" href="Data.Product.html#388" class="Generalizable">b</a><a id="3795" class="Symbol">}</a> <a id="3797" class="Symbol">{</a><a id="3798" href="Data.Product.html#3798" class="Bound">C</a> <a id="3800" class="Symbol">:</a> <a id="3802" class="Symbol">(</a><a id="3803" href="Data.Product.html#3803" class="Bound">a</a> <a id="3805" class="Symbol">:</a> <a id="3807" href="Data.Product.html#418" class="Generalizable">A</a><a id="3808" class="Symbol">)</a> <a id="3810" class="Symbol">→</a> <a id="3812" href="Data.Product.html#3782" class="Bound">B</a> <a id="3814" href="Data.Product.html#3803" class="Bound">a</a> <a id="3816" class="Symbol">→</a> <a id="3818" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3822" href="Data.Product.html#390" class="Generalizable">c</a><a id="3823" class="Symbol">}</a> <a id="3825" class="Symbol">→</a>
|
|||
|
|
<a id="3837" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3839" href="Data.Product.html#418" class="Generalizable">A</a> <a id="3841" class="Symbol">(λ</a> <a id="3844" href="Data.Product.html#3844" class="Bound">a</a> <a id="3846" class="Symbol">→</a> <a id="3848" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3850" class="Symbol">(</a><a id="3851" href="Data.Product.html#3782" class="Bound">B</a> <a id="3853" href="Data.Product.html#3844" class="Bound">a</a><a id="3854" class="Symbol">)</a> <a id="3856" class="Symbol">(</a><a id="3857" href="Data.Product.html#3798" class="Bound">C</a> <a id="3859" href="Data.Product.html#3844" class="Bound">a</a><a id="3860" class="Symbol">))</a> <a id="3863" class="Symbol">→</a> <a id="3865" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3867" class="Symbol">(</a><a id="3868" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="3870" href="Data.Product.html#418" class="Generalizable">A</a> <a id="3872" href="Data.Product.html#3782" class="Bound">B</a><a id="3873" class="Symbol">)</a> <a id="3875" class="Symbol">(</a><a id="3876" href="Data.Product.html#3422" class="Function">uncurry</a> <a id="3884" href="Data.Product.html#3798" class="Bound">C</a><a id="3885" class="Symbol">)</a>
|
|||
|
|
<a id="3887" href="Data.Product.html#3772" class="Function">assocˡ</a> <a id="3894" class="Symbol">(</a><a id="3895" href="Data.Product.html#3895" class="Bound">a</a> <a id="3897" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3899" class="Symbol">(</a><a id="3900" href="Data.Product.html#3900" class="Bound">b</a> <a id="3902" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3904" href="Data.Product.html#3904" class="Bound">c</a><a id="3905" class="Symbol">))</a> <a id="3908" class="Symbol">=</a> <a id="3910" class="Symbol">((</a><a id="3912" href="Data.Product.html#3895" class="Bound">a</a> <a id="3914" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3916" href="Data.Product.html#3900" class="Bound">b</a><a id="3917" class="Symbol">)</a> <a id="3919" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3921" href="Data.Product.html#3904" class="Bound">c</a><a id="3922" class="Symbol">)</a>
|
|||
|
|
|
|||
|
|
<a id="3925" class="Comment">-- Alternate form of associativity for dependent products</a>
|
|||
|
|
<a id="3983" class="Comment">-- where the C parameter is uncurried.</a>
|
|||
|
|
<a id="assocʳ-curried"></a><a id="4022" href="Data.Product.html#4022" class="Function">assocʳ-curried</a> <a id="4037" class="Symbol">:</a> <a id="4039" class="Symbol">{</a><a id="4040" href="Data.Product.html#4040" class="Bound">B</a> <a id="4042" class="Symbol">:</a> <a id="4044" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4046" class="Symbol">→</a> <a id="4048" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4052" href="Data.Product.html#388" class="Generalizable">b</a><a id="4053" class="Symbol">}</a> <a id="4055" class="Symbol">{</a><a id="4056" href="Data.Product.html#4056" class="Bound">C</a> <a id="4058" class="Symbol">:</a> <a id="4060" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="4062" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4064" href="Data.Product.html#4040" class="Bound">B</a> <a id="4066" class="Symbol">→</a> <a id="4068" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4072" href="Data.Product.html#390" class="Generalizable">c</a><a id="4073" class="Symbol">}</a> <a id="4075" class="Symbol">→</a>
|
|||
|
|
<a id="4094" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="4096" class="Symbol">(</a><a id="4097" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="4099" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4101" href="Data.Product.html#4040" class="Bound">B</a><a id="4102" class="Symbol">)</a> <a id="4104" href="Data.Product.html#4056" class="Bound">C</a> <a id="4106" class="Symbol">→</a> <a id="4108" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="4110" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4112" class="Symbol">(λ</a> <a id="4115" href="Data.Product.html#4115" class="Bound">a</a> <a id="4117" class="Symbol">→</a> <a id="4119" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="4121" class="Symbol">(</a><a id="4122" href="Data.Product.html#4040" class="Bound">B</a> <a id="4124" href="Data.Product.html#4115" class="Bound">a</a><a id="4125" class="Symbol">)</a> <a id="4127" class="Symbol">(</a><a id="4128" href="Data.Product.html#3265" class="Function">curry</a> <a id="4134" href="Data.Product.html#4056" class="Bound">C</a> <a id="4136" href="Data.Product.html#4115" class="Bound">a</a><a id="4137" class="Symbol">))</a>
|
|||
|
|
<a id="4140" href="Data.Product.html#4022" class="Function">assocʳ-curried</a> <a id="4155" class="Symbol">((</a><a id="4157" href="Data.Product.html#4157" class="Bound">a</a> <a id="4159" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="4161" href="Data.Product.html#4161" class="Bound">b</a><a id="4162" class="Symbol">)</a> <a id="4164" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="4166" href="Data.Product.html#4166" class="Bound">c</a><a id="4167" class="Symbol">)</a> <a id="4169" class="Symbol">=</a> <a id="4171" class="Symbol">(</a><a id="4172" href="Data.Product.html#4157" class="Bound">a</a> <a id="4174" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="4176" class="Symbol">(</a><a id="4177" href="Data.Product.html#4161" class="Bound">b</a> <a id="4179" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="4181" href="Data.Product.html#4166" class="Bound">c</a><a id="4182" class="Symbol">))</a>
|
|||
|
|
|
|||
|
|
<a id="assocˡ-curried"></a><a id="4186" href="Data.Product.html#4186" class="Function">assocˡ-curried</a> <a id="4201" class="Symbol">:</a> <a id="4203" class="Symbol">{</a><a id="4204" href="Data.Product.html#4204" class="Bound">B</a> <a id="4206" class="Symbol">:</a> <a id="4208" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4210" class="Symbol">→</a> <a id="4212" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4216" href="Data.Product.html#388" class="Generalizable">b</a><a id="4217" class="Symbol">}</a> <a id="4219" class="Symbol">{</a><a id="4220" href="Data.Product.html#4220" class="Bound">C</a> <a id="4222" class="Symbol">:</a> <a id="4224" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="4226" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4228" href="Data.Product.html#4204" class="Bound">B</a> <a id="4230" class="Symbol">→</a> <a id="4232" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4236" href="Data.Product.html#390" class="Generalizable">c</a><a id="4237" class="Symbol">}</a> <a id="4239" class="Symbol">→</a>
|
|||
|
|
<a id="4251" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="4253" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4255" class="Symbol">(λ</a> <a id="4258" href="Data.Product.html#4258" class="Bound">a</a> <a id="4260" class="Symbol">→</a> <a id="4262" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="4264" class="Symbol">(</a><a id="4265" href="Data.Product.html#4204" class="Bound">B</a> <a id="4267" href="Data.Product.html#4258" class="Bound">a</a><a id="4268" class="Symbol">)</a> <a id="4270" class="Symbol">(</a><a id="4271" href="Data.Product.html#3265" class="Function">curry</a> <a id="4277" href="Data.Product.html#4220" class="Bound">C</a> <a id="4279" href="Data.Product.html#4258" class="Bound">a</a><a id="4280" class="Symbol">))</a> <a id="4283" class="Symbol">→</a> <a id="4285" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="4287" class="Symbol">(</a><a id="4288" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="4290" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4292" href="Data.Product.html#4204" class="Bound">B</a><a id="4293" class="Symbol">)</a> <a id="4295" href="Data.Product.html#4220" class="Bound">C</a>
|
|||
|
|
<a id="4297" href="Data.Product.html#4186" class="Function">assocˡ-curried</a> <a id="4312" class="Symbol">(</a><a id="4313" href="Data.Product.html#4313" class="Bound">a</a> <a id="4315" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="4317" class="Symbol">(</a><a id="4318" href="Data.Product.html#4318" class="Bound">b</a> <a id="4320" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="4322" href="Data.Product.html#4322" class="Bound">c</a><a id="4323" class="Symbol">))</a> <a id="4326" class="Symbol">=</a> <a id="4328" class="Symbol">((</a><a id="4330" href="Data.Product.html#4313" class="Bound">a</a> <a id="4332" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="4334" href="Data.Product.html#4318" class="Bound">b</a><a id="4335" class="Symbol">)</a> <a id="4337" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="4339" href="Data.Product.html#4322" class="Bound">c</a><a id="4340" class="Symbol">)</a>
|
|||
|
|
|
|||
|
|
<a id="4343" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
<a id="4416" class="Comment">-- Operations for non-dependent products</a>
|
|||
|
|
|
|||
|
|
<a id="4458" class="Comment">-- Any of the above operations for dependent products will also work for</a>
|
|||
|
|
<a id="4531" class="Comment">-- non-dependent products but sometimes Agda has difficulty inferring</a>
|
|||
|
|
<a id="4601" class="Comment">-- the non-dependency. Primed (′ = \prime) versions of the operations</a>
|
|||
|
|
<a id="4671" class="Comment">-- are therefore provided below that sometimes have better inference</a>
|
|||
|
|
<a id="4740" class="Comment">-- properties.</a>
|
|||
|
|
|
|||
|
|
<a id="zip′"></a><a id="4756" href="Data.Product.html#4756" class="Function">zip′</a> <a id="4761" class="Symbol">:</a> <a id="4763" class="Symbol">(</a><a id="4764" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4766" class="Symbol">→</a> <a id="4768" href="Data.Product.html#432" class="Generalizable">B</a> <a id="4770" class="Symbol">→</a> <a id="4772" href="Data.Product.html#446" class="Generalizable">C</a><a id="4773" class="Symbol">)</a> <a id="4775" class="Symbol">→</a> <a id="4777" class="Symbol">(</a><a id="4778" href="Data.Product.html#460" class="Generalizable">D</a> <a id="4780" class="Symbol">→</a> <a id="4782" href="Data.Product.html#474" class="Generalizable">E</a> <a id="4784" class="Symbol">→</a> <a id="4786" href="Data.Product.html#488" class="Generalizable">F</a><a id="4787" class="Symbol">)</a> <a id="4789" class="Symbol">→</a> <a id="4791" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4793" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="4795" href="Data.Product.html#460" class="Generalizable">D</a> <a id="4797" class="Symbol">→</a> <a id="4799" href="Data.Product.html#432" class="Generalizable">B</a> <a id="4801" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="4803" href="Data.Product.html#474" class="Generalizable">E</a> <a id="4805" class="Symbol">→</a> <a id="4807" href="Data.Product.html#446" class="Generalizable">C</a> <a id="4809" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="4811" href="Data.Product.html#488" class="Generalizable">F</a>
|
|||
|
|
<a id="4813" href="Data.Product.html#4756" class="Function">zip′</a> <a id="4818" href="Data.Product.html#4818" class="Bound">f</a> <a id="4820" href="Data.Product.html#4820" class="Bound">g</a> <a id="4822" class="Symbol">=</a> <a id="4824" href="Data.Product.html#3060" class="Function">zip</a> <a id="4828" href="Data.Product.html#4818" class="Bound">f</a> <a id="4830" href="Data.Product.html#4820" class="Bound">g</a>
|
|||
|
|
|
|||
|
|
<a id="curry′"></a><a id="4833" href="Data.Product.html#4833" class="Function">curry′</a> <a id="4840" class="Symbol">:</a> <a id="4842" class="Symbol">(</a><a id="4843" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4845" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="4847" href="Data.Product.html#432" class="Generalizable">B</a> <a id="4849" class="Symbol">→</a> <a id="4851" href="Data.Product.html#446" class="Generalizable">C</a><a id="4852" class="Symbol">)</a> <a id="4854" class="Symbol">→</a> <a id="4856" class="Symbol">(</a><a id="4857" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4859" class="Symbol">→</a> <a id="4861" href="Data.Product.html#432" class="Generalizable">B</a> <a id="4863" class="Symbol">→</a> <a id="4865" href="Data.Product.html#446" class="Generalizable">C</a><a id="4866" class="Symbol">)</a>
|
|||
|
|
<a id="4868" href="Data.Product.html#4833" class="Function">curry′</a> <a id="4875" class="Symbol">=</a> <a id="4877" href="Data.Product.html#3265" class="Function">curry</a>
|
|||
|
|
|
|||
|
|
<a id="uncurry′"></a><a id="4884" href="Data.Product.html#4884" class="Function">uncurry′</a> <a id="4893" class="Symbol">:</a> <a id="4895" class="Symbol">(</a><a id="4896" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4898" class="Symbol">→</a> <a id="4900" href="Data.Product.html#432" class="Generalizable">B</a> <a id="4902" class="Symbol">→</a> <a id="4904" href="Data.Product.html#446" class="Generalizable">C</a><a id="4905" class="Symbol">)</a> <a id="4907" class="Symbol">→</a> <a id="4909" class="Symbol">(</a><a id="4910" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4912" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="4914" href="Data.Product.html#432" class="Generalizable">B</a> <a id="4916" class="Symbol">→</a> <a id="4918" href="Data.Product.html#446" class="Generalizable">C</a><a id="4919" class="Symbol">)</a>
|
|||
|
|
<a id="4921" href="Data.Product.html#4884" class="Function">uncurry′</a> <a id="4930" class="Symbol">=</a> <a id="4932" href="Data.Product.html#3422" class="Function">uncurry</a>
|
|||
|
|
|
|||
|
|
<a id="dmap′"></a><a id="4941" href="Data.Product.html#4941" class="Function">dmap′</a> <a id="4947" class="Symbol">:</a> <a id="4949" class="Symbol">∀</a> <a id="4951" class="Symbol">{</a><a id="4952" href="Data.Product.html#4952" class="Bound">x</a> <a id="4954" href="Data.Product.html#4954" class="Bound">y</a><a id="4955" class="Symbol">}</a> <a id="4957" class="Symbol">{</a><a id="4958" href="Data.Product.html#4958" class="Bound">X</a> <a id="4960" class="Symbol">:</a> <a id="4962" href="Data.Product.html#418" class="Generalizable">A</a> <a id="4964" class="Symbol">→</a> <a id="4966" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4970" href="Data.Product.html#4952" class="Bound">x</a><a id="4971" class="Symbol">}</a> <a id="4973" class="Symbol">{</a><a id="4974" href="Data.Product.html#4974" class="Bound">Y</a> <a id="4976" class="Symbol">:</a> <a id="4978" href="Data.Product.html#432" class="Generalizable">B</a> <a id="4980" class="Symbol">→</a> <a id="4982" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4986" href="Data.Product.html#4954" class="Bound">y</a><a id="4987" class="Symbol">}</a> <a id="4989" class="Symbol">→</a>
|
|||
|
|
<a id="4999" class="Symbol">((</a><a id="5001" href="Data.Product.html#5001" class="Bound">a</a> <a id="5003" class="Symbol">:</a> <a id="5005" href="Data.Product.html#418" class="Generalizable">A</a><a id="5006" class="Symbol">)</a> <a id="5008" class="Symbol">→</a> <a id="5010" href="Data.Product.html#4958" class="Bound">X</a> <a id="5012" href="Data.Product.html#5001" class="Bound">a</a><a id="5013" class="Symbol">)</a> <a id="5015" class="Symbol">→</a> <a id="5017" class="Symbol">((</a><a id="5019" href="Data.Product.html#5019" class="Bound">b</a> <a id="5021" class="Symbol">:</a> <a id="5023" href="Data.Product.html#432" class="Generalizable">B</a><a id="5024" class="Symbol">)</a> <a id="5026" class="Symbol">→</a> <a id="5028" href="Data.Product.html#4974" class="Bound">Y</a> <a id="5030" href="Data.Product.html#5019" class="Bound">b</a><a id="5031" class="Symbol">)</a> <a id="5033" class="Symbol">→</a>
|
|||
|
|
<a id="5043" class="Symbol">(</a><a id="5044" href="Data.Product.html#5044" class="Bound">(</a><a id="5045" href="Data.Product.html#5045" class="Bound">a</a> <a id="5047" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5049" href="Data.Product.html#5049" class="Bound">b</a><a id="5050" href="Data.Product.html#5044" class="Bound">)</a> <a id="5052" class="Symbol">:</a> <a id="5054" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5056" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5058" href="Data.Product.html#432" class="Generalizable">B</a><a id="5059" class="Symbol">)</a> <a id="5061" class="Symbol">→</a> <a id="5063" href="Data.Product.html#4958" class="Bound">X</a> <a id="5065" href="Data.Product.html#5045" class="Bound">a</a> <a id="5067" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5069" href="Data.Product.html#4974" class="Bound">Y</a> <a id="5071" href="Data.Product.html#5049" class="Bound">b</a>
|
|||
|
|
<a id="5073" href="Data.Product.html#4941" class="Function">dmap′</a> <a id="5079" href="Data.Product.html#5079" class="Bound">f</a> <a id="5081" href="Data.Product.html#5081" class="Bound">g</a> <a id="5083" class="Symbol">=</a> <a id="5085" href="Data.Product.html#2853" class="Function">dmap</a> <a id="5090" href="Data.Product.html#5079" class="Bound">f</a> <a id="5092" href="Data.Product.html#5081" class="Bound">g</a>
|
|||
|
|
|
|||
|
|
<a id="_<*>_"></a><a id="5095" href="Data.Product.html#5095" class="Function Operator">_<*>_</a> <a id="5101" class="Symbol">:</a> <a id="5103" class="Symbol">∀</a> <a id="5105" class="Symbol">{</a><a id="5106" href="Data.Product.html#5106" class="Bound">x</a> <a id="5108" href="Data.Product.html#5108" class="Bound">y</a><a id="5109" class="Symbol">}</a> <a id="5111" class="Symbol">{</a><a id="5112" href="Data.Product.html#5112" class="Bound">X</a> <a id="5114" class="Symbol">:</a> <a id="5116" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5118" class="Symbol">→</a> <a id="5120" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5124" href="Data.Product.html#5106" class="Bound">x</a><a id="5125" class="Symbol">}</a> <a id="5127" class="Symbol">{</a><a id="5128" href="Data.Product.html#5128" class="Bound">Y</a> <a id="5130" class="Symbol">:</a> <a id="5132" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5134" class="Symbol">→</a> <a id="5136" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5140" href="Data.Product.html#5108" class="Bound">y</a><a id="5141" class="Symbol">}</a> <a id="5143" class="Symbol">→</a>
|
|||
|
|
<a id="5153" class="Symbol">((</a><a id="5155" href="Data.Product.html#5155" class="Bound">a</a> <a id="5157" class="Symbol">:</a> <a id="5159" href="Data.Product.html#418" class="Generalizable">A</a><a id="5160" class="Symbol">)</a> <a id="5162" class="Symbol">→</a> <a id="5164" href="Data.Product.html#5112" class="Bound">X</a> <a id="5166" href="Data.Product.html#5155" class="Bound">a</a><a id="5167" class="Symbol">)</a> <a id="5169" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5171" class="Symbol">((</a><a id="5173" href="Data.Product.html#5173" class="Bound">b</a> <a id="5175" class="Symbol">:</a> <a id="5177" href="Data.Product.html#432" class="Generalizable">B</a><a id="5178" class="Symbol">)</a> <a id="5180" class="Symbol">→</a> <a id="5182" href="Data.Product.html#5128" class="Bound">Y</a> <a id="5184" href="Data.Product.html#5173" class="Bound">b</a><a id="5185" class="Symbol">)</a> <a id="5187" class="Symbol">→</a>
|
|||
|
|
<a id="5197" class="Symbol">(</a><a id="5198" href="Data.Product.html#5198" class="Bound">(</a><a id="5199" href="Data.Product.html#5199" class="Bound">a</a> <a id="5201" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5203" href="Data.Product.html#5203" class="Bound">b</a><a id="5204" href="Data.Product.html#5198" class="Bound">)</a> <a id="5206" class="Symbol">:</a> <a id="5208" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5210" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5212" href="Data.Product.html#432" class="Generalizable">B</a><a id="5213" class="Symbol">)</a> <a id="5215" class="Symbol">→</a> <a id="5217" href="Data.Product.html#5112" class="Bound">X</a> <a id="5219" href="Data.Product.html#5199" class="Bound">a</a> <a id="5221" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5223" href="Data.Product.html#5128" class="Bound">Y</a> <a id="5225" href="Data.Product.html#5203" class="Bound">b</a>
|
|||
|
|
<a id="5227" href="Data.Product.html#5095" class="Function Operator">_<*>_</a> <a id="5233" class="Symbol">=</a> <a id="5235" href="Data.Product.html#3422" class="Function">uncurry</a> <a id="5243" href="Data.Product.html#4941" class="Function">dmap′</a>
|
|||
|
|
|
|||
|
|
<a id="5250" class="Comment">-- Operations that can only be defined for non-dependent products</a>
|
|||
|
|
|
|||
|
|
<a id="swap"></a><a id="5317" href="Data.Product.html#5317" class="Function">swap</a> <a id="5322" class="Symbol">:</a> <a id="5324" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5326" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5328" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5330" class="Symbol">→</a> <a id="5332" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5334" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5336" href="Data.Product.html#418" class="Generalizable">A</a>
|
|||
|
|
<a id="5338" href="Data.Product.html#5317" class="Function">swap</a> <a id="5343" class="Symbol">(</a><a id="5344" href="Data.Product.html#5344" class="Bound">x</a> <a id="5346" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5348" href="Data.Product.html#5348" class="Bound">y</a><a id="5349" class="Symbol">)</a> <a id="5351" class="Symbol">=</a> <a id="5353" class="Symbol">(</a><a id="5354" href="Data.Product.html#5348" class="Bound">y</a> <a id="5356" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5358" href="Data.Product.html#5344" class="Bound">x</a><a id="5359" class="Symbol">)</a>
|
|||
|
|
|
|||
|
|
<a id="_-×-_"></a><a id="5362" href="Data.Product.html#5362" class="Function Operator">_-×-_</a> <a id="5368" class="Symbol">:</a> <a id="5370" class="Symbol">(</a><a id="5371" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5373" class="Symbol">→</a> <a id="5375" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5377" class="Symbol">→</a> <a id="5379" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5383" href="Data.Product.html#400" class="Generalizable">p</a><a id="5384" class="Symbol">)</a> <a id="5386" class="Symbol">→</a> <a id="5388" class="Symbol">(</a><a id="5389" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5391" class="Symbol">→</a> <a id="5393" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5395" class="Symbol">→</a> <a id="5397" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5401" href="Data.Product.html#402" class="Generalizable">q</a><a id="5402" class="Symbol">)</a> <a id="5404" class="Symbol">→</a> <a id="5406" class="Symbol">(</a><a id="5407" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5409" class="Symbol">→</a> <a id="5411" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5413" class="Symbol">→</a> <a id="5415" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5419" class="Symbol">_)</a>
|
|||
|
|
<a id="5422" href="Data.Product.html#5422" class="Bound">f</a> <a id="5424" href="Data.Product.html#5362" class="Function Operator">-×-</a> <a id="5428" href="Data.Product.html#5428" class="Bound">g</a> <a id="5430" class="Symbol">=</a> <a id="5432" href="Data.Product.html#5422" class="Bound">f</a> <a id="5434" href="Function.Base.html#5115" class="Function Operator">-⟪</a> <a id="5437" href="Data.Product.html#1167" class="Function Operator">_×_</a> <a id="5441" href="Function.Base.html#5115" class="Function Operator">⟫-</a> <a id="5444" href="Data.Product.html#5428" class="Bound">g</a>
|
|||
|
|
|
|||
|
|
<a id="_-,-_"></a><a id="5447" href="Data.Product.html#5447" class="Function Operator">_-,-_</a> <a id="5453" class="Symbol">:</a> <a id="5455" class="Symbol">(</a><a id="5456" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5458" class="Symbol">→</a> <a id="5460" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5462" class="Symbol">→</a> <a id="5464" href="Data.Product.html#446" class="Generalizable">C</a><a id="5465" class="Symbol">)</a> <a id="5467" class="Symbol">→</a> <a id="5469" class="Symbol">(</a><a id="5470" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5472" class="Symbol">→</a> <a id="5474" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5476" class="Symbol">→</a> <a id="5478" href="Data.Product.html#460" class="Generalizable">D</a><a id="5479" class="Symbol">)</a> <a id="5481" class="Symbol">→</a> <a id="5483" class="Symbol">(</a><a id="5484" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5486" class="Symbol">→</a> <a id="5488" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5490" class="Symbol">→</a> <a id="5492" href="Data.Product.html#446" class="Generalizable">C</a> <a id="5494" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5496" href="Data.Product.html#460" class="Generalizable">D</a><a id="5497" class="Symbol">)</a>
|
|||
|
|
<a id="5499" href="Data.Product.html#5499" class="Bound">f</a> <a id="5501" href="Data.Product.html#5447" class="Function Operator">-,-</a> <a id="5505" href="Data.Product.html#5505" class="Bound">g</a> <a id="5507" class="Symbol">=</a> <a id="5509" href="Data.Product.html#5499" class="Bound">f</a> <a id="5511" href="Function.Base.html#5115" class="Function Operator">-⟪</a> <a id="5514" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a> <a id="5518" href="Function.Base.html#5115" class="Function Operator">⟫-</a> <a id="5521" href="Data.Product.html#5505" class="Bound">g</a>
|
|||
|
|
|
|||
|
|
<a id="5524" class="Comment">-- Rewriting non-dependent products</a>
|
|||
|
|
<a id="assocʳ′"></a><a id="5560" href="Data.Product.html#5560" class="Function">assocʳ′</a> <a id="5568" class="Symbol">:</a> <a id="5570" class="Symbol">(</a><a id="5571" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5573" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5575" href="Data.Product.html#432" class="Generalizable">B</a><a id="5576" class="Symbol">)</a> <a id="5578" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5580" href="Data.Product.html#446" class="Generalizable">C</a> <a id="5582" class="Symbol">→</a> <a id="5584" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5586" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5588" class="Symbol">(</a><a id="5589" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5591" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5593" href="Data.Product.html#446" class="Generalizable">C</a><a id="5594" class="Symbol">)</a>
|
|||
|
|
<a id="5596" href="Data.Product.html#5560" class="Function">assocʳ′</a> <a id="5604" class="Symbol">((</a><a id="5606" href="Data.Product.html#5606" class="Bound">a</a> <a id="5608" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5610" href="Data.Product.html#5610" class="Bound">b</a><a id="5611" class="Symbol">)</a> <a id="5613" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5615" href="Data.Product.html#5615" class="Bound">c</a><a id="5616" class="Symbol">)</a> <a id="5618" class="Symbol">=</a> <a id="5620" class="Symbol">(</a><a id="5621" href="Data.Product.html#5606" class="Bound">a</a> <a id="5623" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5625" class="Symbol">(</a><a id="5626" href="Data.Product.html#5610" class="Bound">b</a> <a id="5628" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5630" href="Data.Product.html#5615" class="Bound">c</a><a id="5631" class="Symbol">))</a>
|
|||
|
|
|
|||
|
|
<a id="assocˡ′"></a><a id="5635" href="Data.Product.html#5635" class="Function">assocˡ′</a> <a id="5643" class="Symbol">:</a> <a id="5645" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5647" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5649" class="Symbol">(</a><a id="5650" href="Data.Product.html#432" class="Generalizable">B</a> <a id="5652" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5654" href="Data.Product.html#446" class="Generalizable">C</a><a id="5655" class="Symbol">)</a> <a id="5657" class="Symbol">→</a> <a id="5659" class="Symbol">(</a><a id="5660" href="Data.Product.html#418" class="Generalizable">A</a> <a id="5662" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5664" href="Data.Product.html#432" class="Generalizable">B</a><a id="5665" class="Symbol">)</a> <a id="5667" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5669" href="Data.Product.html#446" class="Generalizable">C</a>
|
|||
|
|
<a id="5671" href="Data.Product.html#5635" class="Function">assocˡ′</a> <a id="5679" class="Symbol">(</a><a id="5680" href="Data.Product.html#5680" class="Bound">a</a> <a id="5682" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5684" class="Symbol">(</a><a id="5685" href="Data.Product.html#5685" class="Bound">b</a> <a id="5687" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5689" href="Data.Product.html#5689" class="Bound">c</a><a id="5690" class="Symbol">))</a> <a id="5693" class="Symbol">=</a> <a id="5695" class="Symbol">((</a><a id="5697" href="Data.Product.html#5680" class="Bound">a</a> <a id="5699" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5701" href="Data.Product.html#5685" class="Bound">b</a><a id="5702" class="Symbol">)</a> <a id="5704" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5706" href="Data.Product.html#5689" class="Bound">c</a><a id="5707" class="Symbol">)</a>
|
|||
|
|
</pre></body></html>
|