Deploying to gh-pages from @ 7d8f0d4 🚀

agda · Jun 19, 2024 · df4fbfa · df4fbfa
1 parent 5fb6d43
commit df4fbfa
Show file tree

Hide file tree

Showing 17 changed files with 426 additions and 431 deletions.
diff --git a/Cubical.Algebra.Group.GroupPath.html b/Cubical.Algebra.Group.GroupPath.html
diff --git a/Cubical.Algebra.Group.Instances.Unit.html b/Cubical.Algebra.Group.Instances.Unit.html
@@ -94,7 +94,7 @@
 
 <a id="isContr→≡UnitGroup"></a><a id="3045" href="Cubical.Algebra.Group.Instances.Unit.html#3045" class="Function">isContr→≡UnitGroup</a> <a id="3064" class="Symbol">:</a> <a id="3066" class="Symbol">{</a><a id="3067" href="Cubical.Algebra.Group.Instances.Unit.html#3067" class="Bound">G</a> <a id="3069" class="Symbol">:</a> <a id="3071" href="Cubical.Algebra.Group.Base.html#1230" class="Function">Group</a> <a id="3077" href="Agda.Primitive.html#915" class="Primitive">ℓ-zero</a><a id="3083" class="Symbol">}</a> <a id="3085" class="Symbol">→</a> <a id="3087" href="Cubical.Foundations.Prelude.html#15052" class="Function">isContr</a> <a id="3095" class="Symbol">(</a><a id="3096" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="3100" href="Cubical.Algebra.Group.Instances.Unit.html#3067" class="Bound">G</a><a id="3101" class="Symbol">)</a> <a id="3103" class="Symbol">→</a> <a id="3105" href="Cubical.Algebra.Group.Instances.Unit.html#599" class="Function">UnitGroup₀</a> <a id="3116" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="3118" href="Cubical.Algebra.Group.Instances.Unit.html#3067" class="Bound">G</a>
 <a id="3120" href="Cubical.Algebra.Group.Instances.Unit.html#3045" class="Function">isContr→≡UnitGroup</a> <a id="3139" href="Cubical.Algebra.Group.Instances.Unit.html#3139" class="Bound">c</a> <a id="3141" class="Symbol">=</a>
-  <a id="3145" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="3149" class="Symbol">(</a><a id="3150" href="Cubical.Algebra.Group.GroupPath.html#1402" class="Function">GroupPath</a> <a id="3160" class="Symbol">_</a> <a id="3162" class="Symbol">_)</a>
+  <a id="3145" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="3149" class="Symbol">(</a><a id="3150" href="Cubical.Algebra.Group.GroupPath.html#1443" class="Function">GroupPath</a> <a id="3160" class="Symbol">_</a> <a id="3162" class="Symbol">_)</a>
     <a id="3169" class="Symbol">(</a><a id="3170" href="Cubical.Algebra.Group.MorphismProperties.html#8392" class="Function">invGroupEquiv</a> <a id="3184" class="Symbol">((</a><a id="3186" href="Cubical.Data.Unit.Properties.html#2419" class="Function">isContr→≃Unit</a> <a id="3200" href="Cubical.Algebra.Group.Instances.Unit.html#3139" class="Bound">c</a><a id="3201" class="Symbol">)</a>
                   <a id="3221" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="3223" class="Symbol">(</a><a id="3224" href="Cubical.Algebra.Group.MorphismProperties.html#2406" class="Function">makeIsGroupHom</a> <a id="3239" class="Symbol">(λ</a> <a id="3242" href="Cubical.Algebra.Group.Instances.Unit.html#3242" class="Bound">_</a> <a id="3244" href="Cubical.Algebra.Group.Instances.Unit.html#3244" class="Bound">_</a> <a id="3246" class="Symbol">→</a> <a id="3248" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a><a id="3252" class="Symbol">))))</a>
 

diff --git a/Cubical.Algebra.Group.IsomorphismTheorems.html b/Cubical.Algebra.Group.IsomorphismTheorems.html
@@ -112,7 +112,7 @@
 
   <a id="4024" class="Comment">-- The SIP lets us turn the isomorphism theorem into a path</a>
   <a id="4086" href="Cubical.Algebra.Group.IsomorphismTheorems.html#4086" class="Function">pathThm1</a> <a id="4095" class="Symbol">:</a> <a id="4097" href="Cubical.Algebra.Group.IsomorphismTheorems.html#1212" class="Function">imϕ</a> <a id="4101" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="4103" href="Cubical.Algebra.Group.IsomorphismTheorems.html#1015" class="Bound">G</a> <a id="4105" href="Cubical.Algebra.Group.QuotientGroup.html#3029" class="Function Operator">/</a> <a id="4107" href="Cubical.Algebra.Group.IsomorphismTheorems.html#1108" class="Function">kerNormalSubgroup</a>
-  <a id="4127" href="Cubical.Algebra.Group.IsomorphismTheorems.html#4086" class="Function">pathThm1</a> <a id="4136" class="Symbol">=</a> <a id="4138" href="Cubical.Algebra.Group.GroupPath.html#4286" class="Function">uaGroup</a> <a id="4146" class="Symbol">(</a><a id="4147" href="Cubical.Algebra.Group.MorphismProperties.html#10885" class="Function">GroupIso→GroupEquiv</a> <a id="4167" href="Cubical.Algebra.Group.IsomorphismTheorems.html#3823" class="Function">isoThm1</a><a id="4174" class="Symbol">)</a>
+  <a id="4127" href="Cubical.Algebra.Group.IsomorphismTheorems.html#4086" class="Function">pathThm1</a> <a id="4136" class="Symbol">=</a> <a id="4138" href="Cubical.Algebra.Group.GroupPath.html#4327" class="Function">uaGroup</a> <a id="4146" class="Symbol">(</a><a id="4147" href="Cubical.Algebra.Group.MorphismProperties.html#10885" class="Function">GroupIso→GroupEquiv</a> <a id="4167" href="Cubical.Algebra.Group.IsomorphismTheorems.html#3823" class="Function">isoThm1</a><a id="4174" class="Symbol">)</a>
 
   <a id="4179" href="Cubical.Algebra.Group.IsomorphismTheorems.html#4179" class="Function">surjImIso</a> <a id="4189" class="Symbol">:</a> <a id="4191" href="Cubical.Algebra.Group.Morphisms.html#2293" class="Function">isSurjective</a> <a id="4204" href="Cubical.Algebra.Group.IsomorphismTheorems.html#1031" class="Bound">ϕ</a> <a id="4206" class="Symbol">→</a> <a id="4208" href="Cubical.Algebra.Group.Morphisms.html#1296" class="Function">GroupIso</a> <a id="4217" href="Cubical.Algebra.Group.IsomorphismTheorems.html#1212" class="Function">imϕ</a> <a id="4221" href="Cubical.Algebra.Group.IsomorphismTheorems.html#1017" class="Bound">H</a>
   <a id="4225" href="Cubical.Algebra.Group.IsomorphismTheorems.html#4179" class="Function">surjImIso</a> <a id="4235" href="Cubical.Algebra.Group.IsomorphismTheorems.html#4235" class="Bound">surj</a> <a id="4240" class="Symbol">=</a>