Skip to content

Commit

Permalink
Deploying to gh-pages from @ 573426b 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@mortberg
mortberg committed Jan 24, 2024
1 parent a03f8d3 commit 0f198eb
Show file tree
Hide file tree
Showing 181 changed files with 10,565 additions and 7,252 deletions.
66 changes: 31 additions & 35 deletions Cubical.Algebra.AbGroup.Base.html
View file

Large diffs are not rendered by default.

17 changes: 17 additions & 0 deletions Cubical.Algebra.AbGroup.Instances.DirectProduct.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Algebra.AbGroup.Instances.DirectProduct</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Symbol">#-}</a>
<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html" class="Module">Cubical.Algebra.AbGroup.Instances.DirectProduct</a> <a id="79" class="Keyword">where</a>

<a id="86" class="Keyword">open</a> <a id="91" class="Keyword">import</a> <a id="98" href="Cubical.Data.Sigma.html" class="Module">Cubical.Data.Sigma</a>
<a id="117" class="Keyword">open</a> <a id="122" class="Keyword">import</a> <a id="129" href="Cubical.Algebra.AbGroup.Base.html" class="Module">Cubical.Algebra.AbGroup.Base</a>
<a id="158" class="Keyword">open</a> <a id="163" class="Keyword">import</a> <a id="170" href="Cubical.Algebra.Group.DirProd.html" class="Module">Cubical.Algebra.Group.DirProd</a>

<a id="AbDirProd"></a><a id="201" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#201" class="Function">AbDirProd</a> <a id="211" class="Symbol">:</a> <a id="213" class="Symbol">∀</a> <a id="215" class="Symbol">{</a><a id="216" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#216" class="Bound">ℓ</a> <a id="218" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#218" class="Bound">ℓ&#39;</a><a id="220" class="Symbol">}</a> <a id="222" class="Symbol">→</a> <a id="224" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="232" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#216" class="Bound">ℓ</a> <a id="234" class="Symbol">→</a> <a id="236" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="244" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#218" class="Bound">ℓ&#39;</a> <a id="247" class="Symbol">→</a> <a id="249" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="257" class="Symbol">(</a><a id="258" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="264" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#216" class="Bound">ℓ</a> <a id="266" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#218" class="Bound">ℓ&#39;</a><a id="268" class="Symbol">)</a>
<a id="270" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#201" class="Function">AbDirProd</a> <a id="280" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#280" class="Bound">G</a> <a id="282" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#282" class="Bound">H</a> <a id="284" class="Symbol">=</a>
<a id="288" href="Cubical.Algebra.AbGroup.Base.html#3356" class="Function">Group→AbGroup</a> <a id="302" class="Symbol">(</a><a id="303" href="Cubical.Algebra.Group.DirProd.html#409" class="Function">DirProd</a> <a id="311" class="Symbol">(</a><a id="312" href="Cubical.Algebra.AbGroup.Base.html#3237" class="Function">AbGroup→Group</a> <a id="326" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#280" class="Bound">G</a><a id="327" class="Symbol">)</a> <a id="329" class="Symbol">(</a><a id="330" href="Cubical.Algebra.AbGroup.Base.html#3237" class="Function">AbGroup→Group</a> <a id="344" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#282" class="Bound">H</a><a id="345" class="Symbol">))</a> <a id="348" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#363" class="Function">comm</a>
<a id="355" class="Keyword">where</a>
<a id="363" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#363" class="Function">comm</a> <a id="368" class="Symbol">:</a> <a id="370" class="Symbol">(</a><a id="371" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#371" class="Bound">x</a> <a id="373" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#373" class="Bound">y</a> <a id="375" class="Symbol">:</a> <a id="377" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="381" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#280" class="Bound">G</a> <a id="383" href="Cubical.Data.Sigma.Base.html#461" class="Function Operator">×</a> <a id="385" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="389" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#282" class="Bound">H</a><a id="390" class="Symbol">)</a> <a id="392" class="Symbol">→</a> <a id="394" class="Symbol">_</a> <a id="396" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="398" class="Symbol">_</a>
<a id="402" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#363" class="Function">comm</a> <a id="407" class="Symbol">(</a><a id="408" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#408" class="Bound">g1</a> <a id="411" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="413" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#413" class="Bound">h1</a><a id="415" class="Symbol">)</a> <a id="417" class="Symbol">(</a><a id="418" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#418" class="Bound">g2</a> <a id="421" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="423" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#423" class="Bound">h2</a><a id="425" class="Symbol">)</a> <a id="427" class="Symbol">=</a>
<a id="433" href="Cubical.Data.Sigma.Properties.html#1955" class="Function">ΣPathP</a> <a id="440" class="Symbol">(</a><a id="441" href="Cubical.Algebra.AbGroup.Base.html#1121" class="Function">AbGroupStr.+Comm</a> <a id="458" class="Symbol">(</a><a id="459" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="463" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#280" class="Bound">G</a><a id="464" class="Symbol">)</a> <a id="466" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#408" class="Bound">g1</a> <a id="469" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#418" class="Bound">g2</a>
<a id="482" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="484" href="Cubical.Algebra.AbGroup.Base.html#1121" class="Function">AbGroupStr.+Comm</a> <a id="501" class="Symbol">(</a><a id="502" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="506" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#282" class="Bound">H</a><a id="507" class="Symbol">)</a> <a id="509" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#413" class="Bound">h1</a> <a id="512" href="Cubical.Algebra.AbGroup.Instances.DirectProduct.html#423" class="Bound">h2</a><a id="514" class="Symbol">)</a>
</pre></body></html>
8 changes: 4 additions & 4 deletions Cubical.Algebra.AbGroup.Instances.Hom.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,19 +118,19 @@

<a id="3750" class="Comment">-- Morphism addition is associative</a>
<a id="3788" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3788" class="Function">HomAdd-assoc</a> <a id="3801" class="Symbol">:</a> <a id="3803" class="Symbol">(</a><a id="3804" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3804" class="Bound">f</a> <a id="3806" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3806" class="Bound">g</a> <a id="3808" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3808" class="Bound">h</a> <a id="3810" class="Symbol">:</a> <a id="3812" href="Cubical.Algebra.AbGroup.Base.html#4258" class="Function">AbGroupHom</a> <a id="3823" href="Cubical.Algebra.AbGroup.Instances.Hom.html#561" class="Bound">A</a> <a id="3825" href="Cubical.Algebra.AbGroup.Instances.Hom.html#577" class="Bound">B</a><a id="3826" class="Symbol">)</a> <a id="3828" class="Symbol">→</a> <a id="3830" class="Symbol">(</a><a id="3831" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3804" class="Bound">f</a> <a id="3833" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3716" class="Function Operator">+ₕ</a> <a id="3836" class="Symbol">(</a><a id="3837" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3806" class="Bound">g</a> <a id="3839" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3716" class="Function Operator">+ₕ</a> <a id="3842" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3808" class="Bound">h</a><a id="3843" class="Symbol">))</a> <a id="3846" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="3848" class="Symbol">((</a><a id="3850" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3804" class="Bound">f</a> <a id="3852" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3716" class="Function Operator">+ₕ</a> <a id="3855" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3806" class="Bound">g</a><a id="3856" class="Symbol">)</a> <a id="3858" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3716" class="Function Operator">+ₕ</a> <a id="3861" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3808" class="Bound">h</a><a id="3862" class="Symbol">)</a>
<a id="3866" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3788" class="Function">HomAdd-assoc</a> <a id="3879" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3879" class="Bound">f</a> <a id="3881" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3881" class="Bound">g</a> <a id="3883" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3883" class="Bound">h</a> <a id="3885" class="Symbol">=</a> <a id="3887" href="Cubical.Algebra.Group.MorphismProperties.html#6861" class="Function">GroupHom≡</a> <a id="3897" class="Symbol">(</a><a id="3898" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="3905" class="Symbol">λ</a> <a id="3907" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3907" class="Bound">a</a> <a id="3909" class="Symbol">→</a> <a id="3911" href="Cubical.Algebra.AbGroup.Base.html#1225" class="Function">+Assoc</a> <a id="3918" class="Symbol">_</a> <a id="3920" class="Symbol">_</a> <a id="3922" class="Symbol">_)</a>
<a id="3866" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3788" class="Function">HomAdd-assoc</a> <a id="3879" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3879" class="Bound">f</a> <a id="3881" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3881" class="Bound">g</a> <a id="3883" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3883" class="Bound">h</a> <a id="3885" class="Symbol">=</a> <a id="3887" href="Cubical.Algebra.Group.MorphismProperties.html#7005" class="Function">GroupHom≡</a> <a id="3897" class="Symbol">(</a><a id="3898" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="3905" class="Symbol">λ</a> <a id="3907" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3907" class="Bound">a</a> <a id="3909" class="Symbol">→</a> <a id="3911" href="Cubical.Algebra.AbGroup.Base.html#1225" class="Function">+Assoc</a> <a id="3918" class="Symbol">_</a> <a id="3920" class="Symbol">_</a> <a id="3922" class="Symbol">_)</a>

<a id="3928" class="Comment">-- Morphism addition is commutative</a>
<a id="3966" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3966" class="Function">HomAdd-comm</a> <a id="3978" class="Symbol">:</a> <a id="3980" class="Symbol">(</a><a id="3981" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3981" class="Bound">f</a> <a id="3983" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3983" class="Bound">g</a> <a id="3985" class="Symbol">:</a> <a id="3987" href="Cubical.Algebra.AbGroup.Base.html#4258" class="Function">AbGroupHom</a> <a id="3998" href="Cubical.Algebra.AbGroup.Instances.Hom.html#561" class="Bound">A</a> <a id="4000" href="Cubical.Algebra.AbGroup.Instances.Hom.html#577" class="Bound">B</a><a id="4001" class="Symbol">)</a> <a id="4003" class="Symbol">→</a> <a id="4005" class="Symbol">(</a><a id="4006" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3981" class="Bound">f</a> <a id="4008" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3716" class="Function Operator">+ₕ</a> <a id="4011" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3983" class="Bound">g</a><a id="4012" class="Symbol">)</a> <a id="4014" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="4016" class="Symbol">(</a><a id="4017" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3983" class="Bound">g</a> <a id="4019" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3716" class="Function Operator">+ₕ</a> <a id="4022" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3981" class="Bound">f</a><a id="4023" class="Symbol">)</a>
<a id="4027" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3966" class="Function">HomAdd-comm</a> <a id="4039" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4039" class="Bound">f</a> <a id="4041" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4041" class="Bound">g</a> <a id="4043" class="Symbol">=</a> <a id="4045" href="Cubical.Algebra.Group.MorphismProperties.html#6861" class="Function">GroupHom≡</a> <a id="4055" class="Symbol">(</a><a id="4056" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="4063" class="Symbol">λ</a> <a id="4065" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4065" class="Bound">a</a> <a id="4067" class="Symbol">→</a> <a id="4069" href="Cubical.Algebra.AbGroup.Base.html#1121" class="Function">+Comm</a> <a id="4075" class="Symbol">_</a> <a id="4077" class="Symbol">_)</a>
<a id="4027" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3966" class="Function">HomAdd-comm</a> <a id="4039" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4039" class="Bound">f</a> <a id="4041" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4041" class="Bound">g</a> <a id="4043" class="Symbol">=</a> <a id="4045" href="Cubical.Algebra.Group.MorphismProperties.html#7005" class="Function">GroupHom≡</a> <a id="4055" class="Symbol">(</a><a id="4056" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="4063" class="Symbol">λ</a> <a id="4065" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4065" class="Bound">a</a> <a id="4067" class="Symbol">→</a> <a id="4069" href="Cubical.Algebra.AbGroup.Base.html#1121" class="Function">+Comm</a> <a id="4075" class="Symbol">_</a> <a id="4077" class="Symbol">_)</a>

<a id="4083" class="Comment">-- zero is right identity</a>
<a id="4111" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4111" class="Function">HomAdd-zero</a> <a id="4123" class="Symbol">:</a> <a id="4125" class="Symbol">(</a><a id="4126" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4126" class="Bound">f</a> <a id="4128" class="Symbol">:</a> <a id="4130" href="Cubical.Algebra.AbGroup.Base.html#4258" class="Function">AbGroupHom</a> <a id="4141" href="Cubical.Algebra.AbGroup.Instances.Hom.html#561" class="Bound">A</a> <a id="4143" href="Cubical.Algebra.AbGroup.Instances.Hom.html#577" class="Bound">B</a><a id="4144" class="Symbol">)</a> <a id="4146" class="Symbol">→</a> <a id="4148" class="Symbol">(</a><a id="4149" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4126" class="Bound">f</a> <a id="4151" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3716" class="Function Operator">+ₕ</a> <a id="4154" href="Cubical.Algebra.AbGroup.Instances.Hom.html#1530" class="Function">zero</a><a id="4158" class="Symbol">)</a> <a id="4160" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="4162" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4126" class="Bound">f</a>
<a id="4166" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4111" class="Function">HomAdd-zero</a> <a id="4178" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4178" class="Bound">f</a> <a id="4180" class="Symbol">=</a> <a id="4182" href="Cubical.Algebra.Group.MorphismProperties.html#6861" class="Function">GroupHom≡</a> <a id="4192" class="Symbol">(</a><a id="4193" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="4200" class="Symbol">λ</a> <a id="4202" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4202" class="Bound">a</a> <a id="4204" class="Symbol">→</a> <a id="4206" href="Cubical.Algebra.AbGroup.Instances.Hom.html#983" class="Function">idrB</a> <a id="4211" class="Symbol">_)</a>
<a id="4166" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4111" class="Function">HomAdd-zero</a> <a id="4178" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4178" class="Bound">f</a> <a id="4180" class="Symbol">=</a> <a id="4182" href="Cubical.Algebra.Group.MorphismProperties.html#7005" class="Function">GroupHom≡</a> <a id="4192" class="Symbol">(</a><a id="4193" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="4200" class="Symbol">λ</a> <a id="4202" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4202" class="Bound">a</a> <a id="4204" class="Symbol">→</a> <a id="4206" href="Cubical.Algebra.AbGroup.Instances.Hom.html#983" class="Function">idrB</a> <a id="4211" class="Symbol">_)</a>

<a id="4217" class="Comment">-- -ₕ is right inverse</a>
<a id="4242" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4242" class="Function">HomInv-invr</a> <a id="4254" class="Symbol">:</a> <a id="4256" class="Symbol">(</a><a id="4257" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4257" class="Bound">f</a> <a id="4259" class="Symbol">:</a> <a id="4261" href="Cubical.Algebra.AbGroup.Base.html#4258" class="Function">AbGroupHom</a> <a id="4272" href="Cubical.Algebra.AbGroup.Instances.Hom.html#561" class="Bound">A</a> <a id="4274" href="Cubical.Algebra.AbGroup.Instances.Hom.html#577" class="Bound">B</a><a id="4275" class="Symbol">)</a> <a id="4277" class="Symbol">→</a> <a id="4279" class="Symbol">(</a><a id="4280" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4257" class="Bound">f</a> <a id="4282" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3716" class="Function Operator">+ₕ</a> <a id="4285" class="Symbol">(</a><a id="4286" href="Cubical.Algebra.AbGroup.Instances.Hom.html#3734" class="Function Operator">-ₕ</a> <a id="4289" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4257" class="Bound">f</a><a id="4290" class="Symbol">))</a> <a id="4293" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="4295" href="Cubical.Algebra.AbGroup.Instances.Hom.html#1530" class="Function">zero</a>
<a id="4302" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4242" class="Function">HomInv-invr</a> <a id="4314" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4314" class="Bound">f</a> <a id="4316" class="Symbol">=</a> <a id="4318" href="Cubical.Algebra.Group.MorphismProperties.html#6861" class="Function">GroupHom≡</a> <a id="4328" class="Symbol">(</a><a id="4329" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="4336" class="Symbol">λ</a> <a id="4338" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4338" class="Bound">a</a> <a id="4340" class="Symbol">→</a> <a id="4342" href="Cubical.Algebra.AbGroup.Instances.Hom.html#1041" class="Function">invrB</a> <a id="4348" class="Symbol">_)</a>
<a id="4302" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4242" class="Function">HomInv-invr</a> <a id="4314" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4314" class="Bound">f</a> <a id="4316" class="Symbol">=</a> <a id="4318" href="Cubical.Algebra.Group.MorphismProperties.html#7005" class="Function">GroupHom≡</a> <a id="4328" class="Symbol">(</a><a id="4329" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="4336" class="Symbol">λ</a> <a id="4338" href="Cubical.Algebra.AbGroup.Instances.Hom.html#4338" class="Bound">a</a> <a id="4340" class="Symbol">→</a> <a id="4342" href="Cubical.Algebra.AbGroup.Instances.Hom.html#1041" class="Function">invrB</a> <a id="4348" class="Symbol">_)</a>


<a id="4353" class="Comment">-- Abelian group structure on AbGroupHom A B</a>
Expand Down
Loading

0 comments on commit 0f198eb

Please sign in to comment.