Deploying to gh-pages from @ c68e112 🚀

Author: maxsnew

Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html

@@ -18,7 +18,7 @@
 
 <a id="617" class="Keyword">open</a> <a id="622" class="Keyword">import</a> <a id="629" href="Cubical.HITs.FreeAbGroup.html" class="Module">Cubical.HITs.FreeAbGroup</a>
 <a id="654" class="Keyword">open</a> <a id="659" class="Keyword">import</a> <a id="666" href="Cubical.HITs.FreeGroup.html" class="Module">Cubical.HITs.FreeGroup</a> <a id="689" class="Symbol">as</a> <a id="692" class="Module">FG</a> <a id="695" class="Keyword">hiding</a> <a id="702" class="Symbol">(</a><a id="703" href="Cubical.HITs.FreeGroup.Properties.html#1900" class="Function">rec</a><a id="706" class="Symbol">)</a>
-<a id="708" class="Keyword">open</a> <a id="713" class="Keyword">import</a> <a id="720" href="Cubical.HITs.SetQuotients.html" class="Module">Cubical.HITs.SetQuotients</a> <a id="746" class="Symbol">as</a> <a id="749" class="Module">SQ</a> <a id="752" class="Keyword">hiding</a> <a id="759" class="Symbol">(</a><a id="760" href="Cubical.HITs.SetQuotients.Base.html#192" class="Datatype Operator">_/_</a> <a id="764" class="Symbol">;</a> <a id="766" href="Cubical.HITs.SetQuotients.Properties.html#3035" class="Function">rec</a><a id="769" class="Symbol">)</a>
+<a id="708" class="Keyword">open</a> <a id="713" class="Keyword">import</a> <a id="720" href="Cubical.HITs.SetQuotients.html" class="Module">Cubical.HITs.SetQuotients</a> <a id="746" class="Symbol">as</a> <a id="749" class="Module">SQ</a> <a id="752" class="Keyword">hiding</a> <a id="759" class="Symbol">(</a><a id="760" href="Cubical.HITs.SetQuotients.Base.html#192" class="Datatype Operator">_/_</a> <a id="764" class="Symbol">;</a> <a id="766" href="Cubical.HITs.SetQuotients.Properties.html#3132" class="Function">rec</a><a id="769" class="Symbol">)</a>
 
 <a id="772" class="Keyword">open</a> <a id="777" class="Keyword">import</a> <a id="784" href="Cubical.Algebra.AbGroup.html" class="Module">Cubical.Algebra.AbGroup</a>
 <a id="808" class="Keyword">open</a> <a id="813" class="Keyword">import</a> <a id="820" href="Cubical.Algebra.AbGroup.Instances.Pi.html" class="Module">Cubical.Algebra.AbGroup.Instances.Pi</a>
@@ -531,7 +531,7 @@
  <a id="22119" class="Symbol">→</a> <a id="22121" class="Symbol">((</a><a id="22123" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22123" class="Bound">k</a> <a id="22125" class="Symbol">:</a> <a id="22127" class="Symbol">_)</a> <a id="22130" class="Symbol">→</a> <a id="22132" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="22136" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22067" class="Bound">ϕ</a> <a id="22138" href="Cubical.HITs.SetQuotients.Base.html#266" class="InductiveConstructor Operator">[</a> <a id="22140" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#4283" class="Function">ℤFinGenerator</a> <a id="22154" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22123" class="Bound">k</a> <a id="22156" href="Cubical.HITs.SetQuotients.Base.html#266" class="InductiveConstructor Operator">]</a> <a id="22158" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="22160" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="22164" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22069" class="Bound">ψ</a> <a id="22166" href="Cubical.HITs.SetQuotients.Base.html#266" class="InductiveConstructor Operator">[</a> <a id="22168" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#4283" class="Function">ℤFinGenerator</a> <a id="22182" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22123" class="Bound">k</a> <a id="22184" href="Cubical.HITs.SetQuotients.Base.html#266" class="InductiveConstructor Operator">]</a><a id="22185" class="Symbol">)</a>
  <a id="22188" class="Symbol">→</a> <a id="22190" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22067" class="Bound">ϕ</a> <a id="22192" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="22194" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22069" class="Bound">ψ</a>
 <a id="22196" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#21970" class="Function">ℤ[]/-GroupHom≡</a> <a id="22211" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22211" class="Bound">G</a> <a id="22213" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22213" class="Bound">ϕ</a> <a id="22215" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22215" class="Bound">ψ</a> <a id="22217" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22217" class="Bound">s</a> <a id="22219" class="Symbol">=</a> <a id="22221" href="Cubical.Data.Sigma.Properties.html#13802" class="Function">Σ≡Prop</a> <a id="22228" class="Symbol">(λ</a> <a id="22231" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22231" class="Bound">_</a> <a id="22233" class="Symbol">→</a> <a id="22235" href="Cubical.Algebra.Group.MorphismProperties.html#3139" class="Function">isPropIsGroupHom</a> <a id="22252" class="Symbol">_</a> <a id="22254" class="Symbol">_)</a>
-  <a id="22259" class="Symbol">(</a><a id="22260" href="Cubical.Foundations.Prelude.html#10976" class="Function">funExt</a> <a id="22267" class="Symbol">(</a><a id="22268" href="Cubical.HITs.SetQuotients.Properties.html#959" class="Function">SQ.elimProp</a> <a id="22280" class="Symbol">(λ</a> <a id="22283" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22283" class="Bound">_</a> <a id="22285" class="Symbol">→</a> <a id="22287" href="Cubical.Algebra.Semigroup.Base.html#987" class="Function">GroupStr.is-set</a> <a id="22303" class="Symbol">(</a><a id="22304" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="22308" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22211" class="Bound">G</a><a id="22309" class="Symbol">)</a> <a id="22311" class="Symbol">_</a> <a id="22313" class="Symbol">_)</a>
+  <a id="22259" class="Symbol">(</a><a id="22260" href="Cubical.Foundations.Prelude.html#10976" class="Function">funExt</a> <a id="22267" class="Symbol">(</a><a id="22268" href="Cubical.HITs.SetQuotients.Properties.html#1056" class="Function">SQ.elimProp</a> <a id="22280" class="Symbol">(λ</a> <a id="22283" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22283" class="Bound">_</a> <a id="22285" class="Symbol">→</a> <a id="22287" href="Cubical.Algebra.Semigroup.Base.html#987" class="Function">GroupStr.is-set</a> <a id="22303" class="Symbol">(</a><a id="22304" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="22308" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22211" class="Bound">G</a><a id="22309" class="Symbol">)</a> <a id="22311" class="Symbol">_</a> <a id="22313" class="Symbol">_)</a>
     <a id="22320" class="Symbol">λ</a> <a id="22322" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22322" class="Bound">x</a> <a id="22324" class="Symbol">→</a> <a id="22326" href="Cubical.Foundations.Prelude.html#11583" class="Function">funExt⁻</a> <a id="22334" class="Symbol">(</a><a id="22335" href="Cubical.Foundations.Prelude.html#1407" class="Function">cong</a> <a id="22340" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="22344" class="Symbol">(</a><a id="22345" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#18666" class="Function">agreeOnℤFinGenerator→≡</a>
       <a id="22374" class="Symbol">{</a><a id="22375" class="Argument">ϕ</a> <a id="22377" class="Symbol">=</a> <a id="22379" href="Cubical.Algebra.Group.MorphismProperties.html#6369" class="Function">compGroupHom</a> <a id="22392" class="Symbol">(</a><a id="22393" href="Cubical.HITs.SetQuotients.Base.html#266" class="InductiveConstructor Operator">[_]</a> <a id="22397" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="22399" href="Cubical.Algebra.Group.MorphismProperties.html#2383" class="Function">makeIsGroupHom</a> <a id="22414" class="Symbol">λ</a> <a id="22416" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22416" class="Bound">f</a> <a id="22418" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22418" class="Bound">g</a> <a id="22420" class="Symbol">→</a> <a id="22422" href="Cubical.Foundations.Prelude.html#892" class="Function">refl</a><a id="22426" class="Symbol">)</a> <a id="22428" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22213" class="Bound">ϕ</a><a id="22429" class="Symbol">}</a>
       <a id="22437" class="Symbol">{</a><a id="22438" class="Argument">ψ</a> <a id="22440" class="Symbol">=</a> <a id="22442" href="Cubical.Algebra.Group.MorphismProperties.html#6369" class="Function">compGroupHom</a> <a id="22455" class="Symbol">(</a><a id="22456" href="Cubical.HITs.SetQuotients.Base.html#266" class="InductiveConstructor Operator">[_]</a> <a id="22460" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="22462" href="Cubical.Algebra.Group.MorphismProperties.html#2383" class="Function">makeIsGroupHom</a> <a id="22477" class="Symbol">λ</a> <a id="22479" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22479" class="Bound">f</a> <a id="22481" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22481" class="Bound">g</a> <a id="22483" class="Symbol">→</a> <a id="22485" href="Cubical.Foundations.Prelude.html#892" class="Function">refl</a><a id="22489" class="Symbol">)</a> <a id="22491" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#22215" class="Bound">ψ</a><a id="22492" class="Symbol">}</a>