Deploying to gh-pages from @ c2cf856 🚀

agda · Jun 18, 2024 · 3fd7f8b · 3fd7f8b
1 parent b31b131
commit 3fd7f8b
Show file tree

Hide file tree

Showing 368 changed files with 3,408 additions and 3,410 deletions.
diff --git a/Cubical.Algebra.AbGroup.Base.html b/Cubical.Algebra.AbGroup.Base.html
diff --git a/Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html b/Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html
diff --git a/Cubical.Algebra.AbGroup.Instances.Hom.html b/Cubical.Algebra.AbGroup.Instances.Hom.html
diff --git a/Cubical.Algebra.AbGroup.Instances.IntMod.html b/Cubical.Algebra.AbGroup.Instances.IntMod.html
@@ -70,7 +70,7 @@
 <a id="2254" href="Cubical.Foundations.Isomorphism.html#942" class="Field">Iso.leftInv</a> <a id="2266" class="Symbol">(</a><a id="2267" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="2271" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#1669" class="Function">ℤ/2/2≅ℤ/2</a><a id="2280" class="Symbol">)</a> <a id="2282" class="Symbol">=</a>
   <a id="2286" href="Cubical.HITs.SetQuotients.Properties.html#982" class="Function">SQ.elimProp</a> <a id="2298" class="Symbol">(λ</a> <a id="2301" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2301" class="Bound">_</a> <a id="2303" class="Symbol">→</a> <a id="2305" href="Cubical.HITs.SetQuotients.Base.html#361" class="InductiveConstructor">squash/</a> <a id="2313" class="Symbol">_</a> <a id="2315" class="Symbol">_)</a> <a id="2318" class="Symbol">λ</a> <a id="2320" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2320" class="Bound">_</a> <a id="2322" class="Symbol">→</a> <a id="2324" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
 <a id="2329" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="2333" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#1669" class="Function">ℤ/2/2≅ℤ/2</a> <a id="2343" class="Symbol">=</a> <a id="2345" href="Cubical.Algebra.Group.MorphismProperties.html#2406" class="Function">makeIsGroupHom</a>
-  <a id="2362" class="Symbol">(</a><a id="2363" href="Cubical.HITs.SetQuotients.Properties.html#982" class="Function">SQ.elimProp</a> <a id="2375" class="Symbol">(λ</a> <a id="2378" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2378" class="Bound">_</a> <a id="2380" class="Symbol">→</a> <a id="2382" href="Cubical.Foundations.HLevels.html#16373" class="Function">isPropΠ</a> <a id="2390" class="Symbol">λ</a> <a id="2392" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2392" class="Bound">_</a> <a id="2394" class="Symbol">→</a> <a id="2396" href="Cubical.Data.Fin.Properties.html#1493" class="Function">isSetFin</a> <a id="2405" class="Symbol">_</a> <a id="2407" class="Symbol">_)</a>
+  <a id="2362" class="Symbol">(</a><a id="2363" href="Cubical.HITs.SetQuotients.Properties.html#982" class="Function">SQ.elimProp</a> <a id="2375" class="Symbol">(λ</a> <a id="2378" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2378" class="Bound">_</a> <a id="2380" class="Symbol">→</a> <a id="2382" href="Cubical.Foundations.HLevels.html#16906" class="Function">isPropΠ</a> <a id="2390" class="Symbol">λ</a> <a id="2392" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2392" class="Bound">_</a> <a id="2394" class="Symbol">→</a> <a id="2396" href="Cubical.Data.Fin.Properties.html#1493" class="Function">isSetFin</a> <a id="2405" class="Symbol">_</a> <a id="2407" class="Symbol">_)</a>
   <a id="2412" class="Symbol">λ</a> <a id="2414" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2414" class="Bound">a</a> <a id="2416" class="Symbol">→</a> <a id="2418" href="Cubical.HITs.SetQuotients.Properties.html#982" class="Function">SQ.elimProp</a> <a id="2430" class="Symbol">(λ</a> <a id="2433" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2433" class="Bound">_</a> <a id="2435" class="Symbol">→</a> <a id="2437" href="Cubical.Data.Fin.Properties.html#1493" class="Function">isSetFin</a> <a id="2446" class="Symbol">_</a> <a id="2448" class="Symbol">_)</a> <a id="2451" class="Symbol">λ</a> <a id="2453" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2453" class="Bound">b</a> <a id="2455" class="Symbol">→</a> <a id="2457" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a><a id="2461" class="Symbol">)</a>
 
 <a id="ℤTorsion"></a><a id="2464" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2464" class="Function">ℤTorsion</a> <a id="2473" class="Symbol">:</a> <a id="2475" class="Symbol">(</a><a id="2476" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2476" class="Bound">n</a> <a id="2478" class="Symbol">:</a> <a id="2480" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="2481" class="Symbol">)</a> <a id="2483" class="Symbol">→</a> <a id="2485" href="Cubical.Foundations.Prelude.html#15052" class="Function">isContr</a> <a id="2493" class="Symbol">(</a><a id="2494" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="2498" class="Symbol">(</a><a id="2499" href="Cubical.Algebra.AbGroup.Instances.Int.html#274" class="Function">ℤAbGroup</a> <a id="2508" href="Cubical.Algebra.AbGroup.Properties.html#4524" class="Function Operator">[</a> <a id="2510" class="Symbol">(</a><a id="2511" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="2515" href="Cubical.Algebra.AbGroup.Instances.IntMod.html#2476" class="Bound">n</a><a id="2516" class="Symbol">)</a> <a id="2518" href="Cubical.Algebra.AbGroup.Properties.html#4524" class="Function Operator">]ₜ</a><a id="2520" class="Symbol">))</a>