Deploying to gh-pages from @ 47e508e 🚀

Author: felixwellen

Cubical.Data.Everything.html

@@ -52,7 +52,7 @@
 <a id="1302" href="Cubical.Data.FinSet.Base.html#1265" class="Function">isPropIsFinSet</a> <a id="1317" href="Cubical.Data.FinSet.Base.html#1317" class="Bound">p</a> <a id="1319" href="Cubical.Data.FinSet.Base.html#1319" class="Bound">q</a> <a id="1321" class="Symbol">=</a> <a id="1323" href="Cubical.Data.Sigma.Properties.html#13672" class="Function">Σ≡PropEquiv</a> <a id="1335" class="Symbol">(λ</a> <a id="1338" href="Cubical.Data.FinSet.Base.html#1338" class="Bound">_</a> <a id="1340" class="Symbol">→</a> <a id="1342" href="Cubical.HITs.PropositionalTruncation.Properties.html#5547" class="Function">isPropPropTrunc</a><a id="1357" class="Symbol">)</a> <a id="1359" class="Symbol">.</a><a id="1360" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="1364" class="Symbol">(</a>
   <a id="1368" href="Cubical.HITs.PropositionalTruncation.Properties.html#3562" class="Function">Prop.elim2</a>
     <a id="1383" class="Symbol">(λ</a> <a id="1386" href="Cubical.Data.FinSet.Base.html#1386" class="Bound">_</a> <a id="1388" href="Cubical.Data.FinSet.Base.html#1388" class="Bound">_</a> <a id="1390" class="Symbol">→</a> <a id="1392" href="Cubical.Data.Nat.Properties.html#3705" class="Function">isSetℕ</a> <a id="1399" class="Symbol">_</a> <a id="1401" class="Symbol">_)</a>
-    <a id="1408" class="Symbol">(λ</a> <a id="1411" href="Cubical.Data.FinSet.Base.html#1411" class="Bound">p</a> <a id="1413" href="Cubical.Data.FinSet.Base.html#1413" class="Bound">q</a> <a id="1415" class="Symbol">→</a> <a id="1417" href="Cubical.Data.Fin.Properties.html#14121" class="Function">Fin-inj</a> <a id="1425" class="Symbol">_</a> <a id="1427" class="Symbol">_</a> <a id="1429" class="Symbol">(</a><a id="1430" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="1433" class="Symbol">(</a><a id="1434" href="Cubical.Foundations.Equiv.html#3576" class="Function">invEquiv</a> <a id="1443" class="Symbol">(</a><a id="1444" href="Cubical.Data.SumFin.Properties.html#1914" class="Function">SumFin≃Fin</a> <a id="1455" class="Symbol">_)</a> <a id="1458" href="Cubical.Data.FinSet.Base.html#432" class="Function Operator">⋆</a> <a id="1460" class="Symbol">(</a><a id="1461" href="Cubical.Foundations.Equiv.html#3576" class="Function">invEquiv</a> <a id="1470" href="Cubical.Data.FinSet.Base.html#1411" class="Bound">p</a><a id="1471" class="Symbol">)</a> <a id="1473" href="Cubical.Data.FinSet.Base.html#432" class="Function Operator">⋆</a> <a id="1475" href="Cubical.Data.FinSet.Base.html#1413" class="Bound">q</a> <a id="1477" href="Cubical.Data.FinSet.Base.html#432" class="Function Operator">⋆</a> <a id="1479" href="Cubical.Data.SumFin.Properties.html#1914" class="Function">SumFin≃Fin</a> <a id="1490" class="Symbol">_)))</a>
+    <a id="1408" class="Symbol">(λ</a> <a id="1411" href="Cubical.Data.FinSet.Base.html#1411" class="Bound">p</a> <a id="1413" href="Cubical.Data.FinSet.Base.html#1413" class="Bound">q</a> <a id="1415" class="Symbol">→</a> <a id="1417" href="Cubical.Data.Fin.Properties.html#14121" class="Function">Fin-inj</a> <a id="1425" class="Symbol">_</a> <a id="1427" class="Symbol">_</a> <a id="1429" class="Symbol">(</a><a id="1430" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="1433" class="Symbol">(</a><a id="1434" href="Cubical.Foundations.Equiv.html#3576" class="Function">invEquiv</a> <a id="1443" class="Symbol">(</a><a id="1444" href="Cubical.Data.SumFin.Properties.html#1971" class="Function">SumFin≃Fin</a> <a id="1455" class="Symbol">_)</a> <a id="1458" href="Cubical.Data.FinSet.Base.html#432" class="Function Operator">⋆</a> <a id="1460" class="Symbol">(</a><a id="1461" href="Cubical.Foundations.Equiv.html#3576" class="Function">invEquiv</a> <a id="1470" href="Cubical.Data.FinSet.Base.html#1411" class="Bound">p</a><a id="1471" class="Symbol">)</a> <a id="1473" href="Cubical.Data.FinSet.Base.html#432" class="Function Operator">⋆</a> <a id="1475" href="Cubical.Data.FinSet.Base.html#1413" class="Bound">q</a> <a id="1477" href="Cubical.Data.FinSet.Base.html#432" class="Function Operator">⋆</a> <a id="1479" href="Cubical.Data.SumFin.Properties.html#1971" class="Function">SumFin≃Fin</a> <a id="1490" class="Symbol">_)))</a>
     <a id="1499" class="Symbol">(</a><a id="1500" href="Cubical.Data.FinSet.Base.html#1317" class="Bound">p</a> <a id="1502" class="Symbol">.</a><a id="1503" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a><a id="1506" class="Symbol">)</a> <a id="1508" class="Symbol">(</a><a id="1509" href="Cubical.Data.FinSet.Base.html#1319" class="Bound">q</a> <a id="1511" class="Symbol">.</a><a id="1512" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a><a id="1515" class="Symbol">))</a>
 
 <a id="1519" class="Comment">-- isFinOrd is Set</a>

Cubical.Data.FinData.FinSet.html

@@ -52,9 +52,9 @@
 
   <a id="1266" href="Cubical.Data.FinSet.FiniteChoice.html#1266" class="Function">choice≃&#39;</a> <a id="1275" class="Symbol">:</a> <a id="1277" class="Symbol">((</a><a id="1279" href="Cubical.Data.FinSet.FiniteChoice.html#1279" class="Bound">x</a> <a id="1281" class="Symbol">:</a> <a id="1283" href="Cubical.Data.FinSet.FiniteChoice.html#1183" class="Bound">X</a><a id="1284" class="Symbol">)</a> <a id="1286" class="Symbol">→</a> <a id="1288" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥</a> <a id="1290" href="Cubical.Data.FinSet.FiniteChoice.html#1214" class="Bound">Y</a> <a id="1292" href="Cubical.Data.FinSet.FiniteChoice.html#1279" class="Bound">x</a> <a id="1294" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a><a id="1296" class="Symbol">)</a> <a id="1298" href="Agda.Builtin.Cubical.Equiv.html#1012" class="Function Operator">≃</a> <a id="1300" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥</a> <a id="1302" class="Symbol">((</a><a id="1304" href="Cubical.Data.FinSet.FiniteChoice.html#1304" class="Bound">x</a> <a id="1306" class="Symbol">:</a> <a id="1308" href="Cubical.Data.FinSet.FiniteChoice.html#1183" class="Bound">X</a><a id="1309" class="Symbol">)</a> <a id="1311" class="Symbol">→</a> <a id="1313" href="Cubical.Data.FinSet.FiniteChoice.html#1214" class="Bound">Y</a> <a id="1315" href="Cubical.Data.FinSet.FiniteChoice.html#1304" class="Bound">x</a><a id="1316" class="Symbol">)</a> <a id="1318" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a>
   <a id="1323" href="Cubical.Data.FinSet.FiniteChoice.html#1266" class="Function">choice≃&#39;</a> <a id="1332" class="Symbol">=</a>
-      <a id="1340" href="Cubical.Foundations.Equiv.html#9591" class="Function">equivΠ</a> <a id="1347" class="Symbol">{</a><a id="1348" class="Argument">B&#39;</a> <a id="1351" class="Symbol">=</a> <a id="1353" class="Symbol">λ</a> <a id="1355" href="Cubical.Data.FinSet.FiniteChoice.html#1355" class="Bound">x</a> <a id="1357" class="Symbol">→</a> <a id="1359" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥</a> <a id="1361" href="Cubical.Data.FinSet.FiniteChoice.html#1214" class="Bound">Y</a> <a id="1363" class="Symbol">(</a><a id="1364" href="Cubical.Foundations.Equiv.html#3136" class="Function">invEq</a> <a id="1370" href="Cubical.Data.FinSet.FiniteChoice.html#1252" class="Function">e</a> <a id="1372" href="Cubical.Data.FinSet.FiniteChoice.html#1355" class="Bound">x</a><a id="1373" class="Symbol">)</a> <a id="1375" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a><a id="1377" class="Symbol">}</a> <a id="1379" href="Cubical.Data.FinSet.FiniteChoice.html#1252" class="Function">e</a> <a id="1381" class="Symbol">(</a><a id="1382" href="Cubical.Data.FinSet.Properties.html#2653" class="Function">transpFamily</a> <a id="1395" href="Cubical.Data.FinSet.FiniteChoice.html#1195" class="Bound">p</a><a id="1396" class="Symbol">)</a>
+      <a id="1340" href="Cubical.Foundations.Equiv.html#9591" class="Function">equivΠ</a> <a id="1347" class="Symbol">{</a><a id="1348" class="Argument">B&#39;</a> <a id="1351" class="Symbol">=</a> <a id="1353" class="Symbol">λ</a> <a id="1355" href="Cubical.Data.FinSet.FiniteChoice.html#1355" class="Bound">x</a> <a id="1357" class="Symbol">→</a> <a id="1359" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥</a> <a id="1361" href="Cubical.Data.FinSet.FiniteChoice.html#1214" class="Bound">Y</a> <a id="1363" class="Symbol">(</a><a id="1364" href="Cubical.Foundations.Equiv.html#3136" class="Function">invEq</a> <a id="1370" href="Cubical.Data.FinSet.FiniteChoice.html#1252" class="Function">e</a> <a id="1372" href="Cubical.Data.FinSet.FiniteChoice.html#1355" class="Bound">x</a><a id="1373" class="Symbol">)</a> <a id="1375" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a><a id="1377" class="Symbol">}</a> <a id="1379" href="Cubical.Data.FinSet.FiniteChoice.html#1252" class="Function">e</a> <a id="1381" class="Symbol">(</a><a id="1382" href="Cubical.Data.FinSet.Properties.html#2760" class="Function">transpFamily</a> <a id="1395" href="Cubical.Data.FinSet.FiniteChoice.html#1195" class="Bound">p</a><a id="1396" class="Symbol">)</a>
     <a id="1402" href="Cubical.Data.FinSet.FiniteChoice.html#271" class="Function Operator">⋆</a> <a id="1404" href="Cubical.Data.FinSet.FiniteChoice.html#636" class="Function">choice≃Fin</a> <a id="1415" class="Symbol">_</a>
-    <a id="1421" href="Cubical.Data.FinSet.FiniteChoice.html#271" class="Function Operator">⋆</a> <a id="1423" href="Cubical.HITs.PropositionalTruncation.Properties.html#5614" class="Function">propTrunc≃</a> <a id="1434" class="Symbol">(</a><a id="1435" href="Cubical.Foundations.Equiv.html#3576" class="Function">invEquiv</a> <a id="1444" class="Symbol">(</a><a id="1445" href="Cubical.Foundations.Equiv.html#9591" class="Function">equivΠ</a> <a id="1452" class="Symbol">{</a><a id="1453" class="Argument">B&#39;</a> <a id="1456" class="Symbol">=</a> <a id="1458" class="Symbol">λ</a> <a id="1460" href="Cubical.Data.FinSet.FiniteChoice.html#1460" class="Bound">x</a> <a id="1462" class="Symbol">→</a> <a id="1464" href="Cubical.Data.FinSet.FiniteChoice.html#1214" class="Bound">Y</a> <a id="1466" class="Symbol">(</a><a id="1467" href="Cubical.Foundations.Equiv.html#3136" class="Function">invEq</a> <a id="1473" href="Cubical.Data.FinSet.FiniteChoice.html#1252" class="Function">e</a> <a id="1475" href="Cubical.Data.FinSet.FiniteChoice.html#1460" class="Bound">x</a><a id="1476" class="Symbol">)}</a> <a id="1479" href="Cubical.Data.FinSet.FiniteChoice.html#1252" class="Function">e</a> <a id="1481" class="Symbol">(</a><a id="1482" href="Cubical.Data.FinSet.Properties.html#2653" class="Function">transpFamily</a> <a id="1495" href="Cubical.Data.FinSet.FiniteChoice.html#1195" class="Bound">p</a><a id="1496" class="Symbol">)))</a>
+    <a id="1421" href="Cubical.Data.FinSet.FiniteChoice.html#271" class="Function Operator">⋆</a> <a id="1423" href="Cubical.HITs.PropositionalTruncation.Properties.html#5614" class="Function">propTrunc≃</a> <a id="1434" class="Symbol">(</a><a id="1435" href="Cubical.Foundations.Equiv.html#3576" class="Function">invEquiv</a> <a id="1444" class="Symbol">(</a><a id="1445" href="Cubical.Foundations.Equiv.html#9591" class="Function">equivΠ</a> <a id="1452" class="Symbol">{</a><a id="1453" class="Argument">B&#39;</a> <a id="1456" class="Symbol">=</a> <a id="1458" class="Symbol">λ</a> <a id="1460" href="Cubical.Data.FinSet.FiniteChoice.html#1460" class="Bound">x</a> <a id="1462" class="Symbol">→</a> <a id="1464" href="Cubical.Data.FinSet.FiniteChoice.html#1214" class="Bound">Y</a> <a id="1466" class="Symbol">(</a><a id="1467" href="Cubical.Foundations.Equiv.html#3136" class="Function">invEq</a> <a id="1473" href="Cubical.Data.FinSet.FiniteChoice.html#1252" class="Function">e</a> <a id="1475" href="Cubical.Data.FinSet.FiniteChoice.html#1460" class="Bound">x</a><a id="1476" class="Symbol">)}</a> <a id="1479" href="Cubical.Data.FinSet.FiniteChoice.html#1252" class="Function">e</a> <a id="1481" class="Symbol">(</a><a id="1482" href="Cubical.Data.FinSet.Properties.html#2760" class="Function">transpFamily</a> <a id="1495" href="Cubical.Data.FinSet.FiniteChoice.html#1195" class="Bound">p</a><a id="1496" class="Symbol">)))</a>
 
 <a id="1501" class="Keyword">module</a> <a id="1508" href="Cubical.Data.FinSet.FiniteChoice.html#1508" class="Module">_</a>
   <a id="1512" class="Symbol">(</a><a id="1513" href="Cubical.Data.FinSet.FiniteChoice.html#1513" class="Bound">X</a> <a id="1515" class="Symbol">:</a> <a id="1517" href="Cubical.Data.FinSet.Base.html#2241" class="Function">FinSet</a> <a id="1524" href="Cubical.Data.FinSet.FiniteChoice.html#622" class="Generalizable">ℓ</a><a id="1525" class="Symbol">)</a>

Cubical.Data.FinSet.Base.html

@@ -42,7 +42,7 @@
   <a id="996" href="Cubical.Data.FinSet.Induction.html#981" class="Function">𝟘</a> <a id="998" class="Symbol">=</a> <a id="1000" href="Cubical.Data.Empty.Base.html#162" class="Function">⊥*</a> <a id="1003" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1005" class="Number">0</a> <a id="1007" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1009" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="1011" href="Cubical.Data.Empty.Properties.html#611" class="Function">uninhabEquiv</a> <a id="1024" href="Cubical.Data.Empty.Base.html#222" class="Function">Empty.rec*</a> <a id="1035" href="Cubical.Data.Empty.Base.html#187" class="Function">Empty.rec</a> <a id="1045" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a>
 
   <a id="1051" href="Cubical.Data.FinSet.Induction.html#1051" class="Function">𝟙</a> <a id="1053" class="Symbol">:</a> <a id="1055" href="Cubical.Data.FinSet.Base.html#2241" class="Function">FinSet</a> <a id="1062" href="Cubical.Data.FinSet.Induction.html#961" class="Bound">ℓ</a>
-  <a id="1066" href="Cubical.Data.FinSet.Induction.html#1051" class="Function">𝟙</a> <a id="1068" class="Symbol">=</a> <a id="1070" href="Cubical.Data.Unit.Base.html#212" class="Function">Unit*</a> <a id="1076" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1078" href="Cubical.Data.FinSet.Properties.html#1711" class="Function">isContr→isFinSet</a> <a id="1095" class="Symbol">(</a><a id="1096" href="Cubical.Data.Unit.Properties.html#2670" class="Function">isContrUnit*</a><a id="1108" class="Symbol">)</a>
+  <a id="1066" href="Cubical.Data.FinSet.Induction.html#1051" class="Function">𝟙</a> <a id="1068" class="Symbol">=</a> <a id="1070" href="Cubical.Data.Unit.Base.html#212" class="Function">Unit*</a> <a id="1076" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1078" href="Cubical.Data.FinSet.Properties.html#1818" class="Function">isContr→isFinSet</a> <a id="1095" class="Symbol">(</a><a id="1096" href="Cubical.Data.Unit.Properties.html#2670" class="Function">isContrUnit*</a><a id="1108" class="Symbol">)</a>
 
   <a id="1113" href="Cubical.Data.FinSet.Induction.html#1113" class="Function Operator">_+_</a> <a id="1117" class="Symbol">:</a> <a id="1119" href="Cubical.Data.FinSet.Base.html#2241" class="Function">FinSet</a> <a id="1126" href="Cubical.Data.FinSet.Induction.html#961" class="Bound">ℓ</a> <a id="1128" class="Symbol">→</a> <a id="1130" href="Cubical.Data.FinSet.Base.html#2241" class="Function">FinSet</a> <a id="1137" href="Cubical.Data.FinSet.Induction.html#961" class="Bound">ℓ</a> <a id="1139" class="Symbol">→</a> <a id="1141" href="Cubical.Data.FinSet.Base.html#2241" class="Function">FinSet</a> <a id="1148" href="Cubical.Data.FinSet.Induction.html#961" class="Bound">ℓ</a>
   <a id="1152" href="Cubical.Data.FinSet.Induction.html#1152" class="Bound">X</a> <a id="1154" href="Cubical.Data.FinSet.Induction.html#1113" class="Function Operator">+</a> <a id="1156" href="Cubical.Data.FinSet.Induction.html#1156" class="Bound">Y</a> <a id="1158" class="Symbol">=</a> <a id="1160" href="Cubical.Data.FinSet.Induction.html#1152" class="Bound">X</a> <a id="1162" class="Symbol">.</a><a id="1163" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="1167" href="Cubical.Data.Sum.Base.html#207" class="Datatype Operator">⊎</a> <a id="1169" href="Cubical.Data.FinSet.Induction.html#1156" class="Bound">Y</a> <a id="1171" class="Symbol">.</a><a id="1172" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="1176" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1178" href="Cubical.Data.FinSet.Constructors.html#4246" class="Function">isFinSet⊎</a> <a id="1188" href="Cubical.Data.FinSet.Induction.html#1152" class="Bound">X</a> <a id="1190" href="Cubical.Data.FinSet.Induction.html#1156" class="Bound">Y</a>
@@ -68,7 +68,7 @@
   <a id="1585" href="Cubical.Data.FinSet.Induction.html#1522" class="Function">𝔽in≃Fin</a> <a id="1593" class="Symbol">(</a><a id="1594" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="1598" href="Cubical.Data.FinSet.Induction.html#1598" class="Bound">n</a><a id="1599" class="Symbol">)</a> <a id="1601" class="Symbol">=</a> <a id="1603" href="Cubical.Data.Sum.Properties.html#4799" class="Function">⊎-equiv</a> <a id="1611" href="Cubical.Data.FinSet.Induction.html#1408" class="Function">𝟙≃Unit</a> <a id="1618" class="Symbol">(</a><a id="1619" href="Cubical.Data.FinSet.Induction.html#1522" class="Function">𝔽in≃Fin</a> <a id="1627" href="Cubical.Data.FinSet.Induction.html#1598" class="Bound">n</a><a id="1628" class="Symbol">)</a>
 
   <a id="1633" href="Cubical.Data.FinSet.Induction.html#1633" class="Function">𝔽in≃Finℕ</a> <a id="1642" class="Symbol">:</a> <a id="1644" class="Symbol">(</a><a id="1645" href="Cubical.Data.FinSet.Induction.html#1645" class="Bound">n</a> <a id="1647" class="Symbol">:</a> <a id="1649" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="1650" class="Symbol">)</a> <a id="1652" class="Symbol">→</a> <a id="1654" href="Cubical.Data.FinSet.Induction.html#1260" class="Function">𝔽in</a> <a id="1658" href="Cubical.Data.FinSet.Induction.html#1645" class="Bound">n</a> <a id="1660" class="Symbol">.</a><a id="1661" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="1665" href="Agda.Builtin.Cubical.Equiv.html#1012" class="Function Operator">≃</a> <a id="1667" href="Cubical.Data.FinSet.Induction.html#698" class="Function">Finℕ</a> <a id="1672" href="Cubical.Data.FinSet.Induction.html#1645" class="Bound">n</a>
-  <a id="1676" href="Cubical.Data.FinSet.Induction.html#1633" class="Function">𝔽in≃Finℕ</a> <a id="1685" href="Cubical.Data.FinSet.Induction.html#1685" class="Bound">n</a> <a id="1687" class="Symbol">=</a> <a id="1689" href="Cubical.Data.FinSet.Induction.html#1522" class="Function">𝔽in≃Fin</a> <a id="1697" href="Cubical.Data.FinSet.Induction.html#1685" class="Bound">n</a> <a id="1699" href="Cubical.Data.FinSet.Induction.html#287" class="Function Operator">⋆</a> <a id="1701" href="Cubical.Data.SumFin.Properties.html#1914" class="Function">SumFin≃Fin</a> <a id="1712" href="Cubical.Data.FinSet.Induction.html#1685" class="Bound">n</a>
+  <a id="1676" href="Cubical.Data.FinSet.Induction.html#1633" class="Function">𝔽in≃Finℕ</a> <a id="1685" href="Cubical.Data.FinSet.Induction.html#1685" class="Bound">n</a> <a id="1687" class="Symbol">=</a> <a id="1689" href="Cubical.Data.FinSet.Induction.html#1522" class="Function">𝔽in≃Fin</a> <a id="1697" href="Cubical.Data.FinSet.Induction.html#1685" class="Bound">n</a> <a id="1699" href="Cubical.Data.FinSet.Induction.html#287" class="Function Operator">⋆</a> <a id="1701" href="Cubical.Data.SumFin.Properties.html#1971" class="Function">SumFin≃Fin</a> <a id="1712" href="Cubical.Data.FinSet.Induction.html#1685" class="Bound">n</a>
 
   <a id="1717" class="Comment">-- 𝔽in preserves addition</a>