Deploying to gh-pages from @ 385066b 🚀

Author: mortberg

Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html

@@ -117,9 +117,9 @@
 
 <a id="InductiveFinSatAC"></a><a id="3903" href="Cubical.Axiom.Choice.html#3903" class="Function">InductiveFinSatAC</a> <a id="3921" class="Symbol">:</a> <a id="3923" class="Symbol">(</a><a id="3924" href="Cubical.Axiom.Choice.html#3924" class="Bound">n</a> <a id="3926" href="Cubical.Axiom.Choice.html#3926" class="Bound">m</a> <a id="3928" class="Symbol">:</a> <a id="3930" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="3931" class="Symbol">)</a> <a id="3933" class="Symbol">→</a> <a id="3935" class="Symbol">∀</a> <a id="3937" class="Symbol">{</a><a id="3938" href="Cubical.Axiom.Choice.html#3938" class="Bound">ℓ</a><a id="3939" class="Symbol">}</a> <a id="3941" class="Symbol">→</a> <a id="3943" href="Cubical.Axiom.Choice.html#1013" class="Function">satAC</a> <a id="3949" href="Cubical.Axiom.Choice.html#3938" class="Bound">ℓ</a> <a id="3951" href="Cubical.Axiom.Choice.html#3924" class="Bound">n</a> <a id="3953" class="Symbol">(</a><a id="3954" href="Cubical.Data.Fin.Inductive.Base.html#453" class="Function">IndF.Fin</a> <a id="3963" href="Cubical.Axiom.Choice.html#3926" class="Bound">m</a><a id="3964" class="Symbol">)</a>
 <a id="3966" href="Cubical.Axiom.Choice.html#3903" class="Function">InductiveFinSatAC</a> <a id="3984" href="Cubical.Axiom.Choice.html#3984" class="Bound">n</a> <a id="3986" href="Cubical.Axiom.Choice.html#3986" class="Bound">m</a> <a id="3988" class="Symbol">{</a><a id="3989" href="Cubical.Axiom.Choice.html#3989" class="Bound">ℓ</a><a id="3990" class="Symbol">}</a> <a id="3992" class="Symbol">=</a>
-  <a id="3996" href="Cubical.Foundations.Prelude.html#10228" class="Function">subst</a> <a id="4002" class="Symbol">(</a><a id="4003" href="Cubical.Axiom.Choice.html#1013" class="Function">satAC</a> <a id="4009" href="Cubical.Axiom.Choice.html#3989" class="Bound">ℓ</a> <a id="4011" href="Cubical.Axiom.Choice.html#3984" class="Bound">n</a><a id="4012" class="Symbol">)</a> <a id="4014" class="Symbol">(</a><a id="4015" href="Cubical.Foundations.Isomorphism.html#3714" class="Function">isoToPath</a> <a id="4025" class="Symbol">(</a><a id="4026" href="Cubical.Data.Fin.Inductive.Properties.html#4828" class="Function">Iso-Fin-InductiveFin</a> <a id="4047" href="Cubical.Axiom.Choice.html#3986" class="Bound">m</a><a id="4048" class="Symbol">))</a> <a id="4051" class="Symbol">(</a><a id="4052" href="Cubical.Axiom.Choice.html#2141" class="Function">FinSatAC</a> <a id="4061" href="Cubical.Axiom.Choice.html#3984" class="Bound">n</a> <a id="4063" href="Cubical.Axiom.Choice.html#3986" class="Bound">m</a><a id="4064" class="Symbol">)</a>
+  <a id="3996" href="Cubical.Foundations.Prelude.html#10228" class="Function">subst</a> <a id="4002" class="Symbol">(</a><a id="4003" href="Cubical.Axiom.Choice.html#1013" class="Function">satAC</a> <a id="4009" href="Cubical.Axiom.Choice.html#3989" class="Bound">ℓ</a> <a id="4011" href="Cubical.Axiom.Choice.html#3984" class="Bound">n</a><a id="4012" class="Symbol">)</a> <a id="4014" class="Symbol">(</a><a id="4015" href="Cubical.Foundations.Isomorphism.html#3714" class="Function">isoToPath</a> <a id="4025" class="Symbol">(</a><a id="4026" href="Cubical.Data.Fin.Inductive.Properties.html#5105" class="Function">Iso-Fin-InductiveFin</a> <a id="4047" href="Cubical.Axiom.Choice.html#3986" class="Bound">m</a><a id="4048" class="Symbol">))</a> <a id="4051" class="Symbol">(</a><a id="4052" href="Cubical.Axiom.Choice.html#2141" class="Function">FinSatAC</a> <a id="4061" href="Cubical.Axiom.Choice.html#3984" class="Bound">n</a> <a id="4063" href="Cubical.Axiom.Choice.html#3986" class="Bound">m</a><a id="4064" class="Symbol">)</a>
 
 <a id="InductiveFinSatAC∃"></a><a id="4067" href="Cubical.Axiom.Choice.html#4067" class="Function">InductiveFinSatAC∃</a> <a id="4086" class="Symbol">:</a> <a id="4088" class="Symbol">(</a><a id="4089" href="Cubical.Axiom.Choice.html#4089" class="Bound">n</a> <a id="4091" class="Symbol">:</a> <a id="4093" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="4094" class="Symbol">)</a> <a id="4096" class="Symbol">→</a> <a id="4098" href="Cubical.Axiom.Choice.html#1439" class="Function">satAC∃</a> <a id="4105" href="Cubical.Axiom.Choice.html#757" class="Generalizable">ℓ</a> <a id="4107" href="Cubical.Axiom.Choice.html#759" class="Generalizable">ℓ&#39;</a> <a id="4110" class="Symbol">(</a><a id="4111" href="Cubical.Data.Fin.Inductive.Base.html#453" class="Function">IndF.Fin</a> <a id="4120" href="Cubical.Axiom.Choice.html#4089" class="Bound">n</a><a id="4121" class="Symbol">)</a>
 <a id="4123" href="Cubical.Axiom.Choice.html#4067" class="Function">InductiveFinSatAC∃</a> <a id="4142" class="Symbol">{</a><a id="4143" class="Argument">ℓ</a> <a id="4145" class="Symbol">=</a> <a id="4147" href="Cubical.Axiom.Choice.html#4147" class="Bound">ℓ</a><a id="4148" class="Symbol">}</a> <a id="4150" class="Symbol">{</a><a id="4151" href="Cubical.Axiom.Choice.html#4151" class="Bound">ℓ&#39;</a><a id="4153" class="Symbol">}</a> <a id="4155" href="Cubical.Axiom.Choice.html#4155" class="Bound">n</a> <a id="4157" class="Symbol">=</a>
-  <a id="4161" href="Cubical.Foundations.Prelude.html#10228" class="Function">subst</a> <a id="4167" class="Symbol">(</a><a id="4168" href="Cubical.Axiom.Choice.html#1439" class="Function">satAC∃</a> <a id="4175" href="Cubical.Axiom.Choice.html#4147" class="Bound">ℓ</a> <a id="4177" href="Cubical.Axiom.Choice.html#4151" class="Bound">ℓ&#39;</a><a id="4179" class="Symbol">)</a> <a id="4181" class="Symbol">(</a><a id="4182" href="Cubical.Foundations.Isomorphism.html#3714" class="Function">isoToPath</a> <a id="4192" class="Symbol">(</a><a id="4193" href="Cubical.Data.Fin.Inductive.Properties.html#4828" class="Function">Iso-Fin-InductiveFin</a> <a id="4214" href="Cubical.Axiom.Choice.html#4155" class="Bound">n</a><a id="4215" class="Symbol">))</a> <a id="4218" class="Symbol">(</a><a id="4219" href="Cubical.Axiom.Choice.html#3815" class="Function">satAC∃Fin</a> <a id="4229" href="Cubical.Axiom.Choice.html#4155" class="Bound">n</a><a id="4230" class="Symbol">)</a>
+  <a id="4161" href="Cubical.Foundations.Prelude.html#10228" class="Function">subst</a> <a id="4167" class="Symbol">(</a><a id="4168" href="Cubical.Axiom.Choice.html#1439" class="Function">satAC∃</a> <a id="4175" href="Cubical.Axiom.Choice.html#4147" class="Bound">ℓ</a> <a id="4177" href="Cubical.Axiom.Choice.html#4151" class="Bound">ℓ&#39;</a><a id="4179" class="Symbol">)</a> <a id="4181" class="Symbol">(</a><a id="4182" href="Cubical.Foundations.Isomorphism.html#3714" class="Function">isoToPath</a> <a id="4192" class="Symbol">(</a><a id="4193" href="Cubical.Data.Fin.Inductive.Properties.html#5105" class="Function">Iso-Fin-InductiveFin</a> <a id="4214" href="Cubical.Axiom.Choice.html#4155" class="Bound">n</a><a id="4215" class="Symbol">))</a> <a id="4218" class="Symbol">(</a><a id="4219" href="Cubical.Axiom.Choice.html#3815" class="Function">satAC∃Fin</a> <a id="4229" href="Cubical.Axiom.Choice.html#4155" class="Bound">n</a><a id="4230" class="Symbol">)</a>
 </pre></body></html>