Deploying to gh-pages from @ 8add6fd 🚀

Author: github-merge-queue[bot]

master/Algebra.Properties.Semiring.Binomial.html

@@ -22,7 +22,7 @@
 <a id="615" class="Keyword">open</a> <a id="620" class="Keyword">import</a> <a id="627" href="Data.Nat.Combinatorics.html" class="Module">Data.Nat.Combinatorics</a>
   <a id="652" class="Keyword">using</a> <a id="658" class="Symbol">(</a><a id="659" href="Data.Nat.Combinatorics.Base.html#1622" class="Function Operator">_C_</a><a id="662" class="Symbol">;</a> <a id="664" href="Data.Nat.Combinatorics.html#2974" class="Function">nCn≡1</a><a id="669" class="Symbol">;</a> <a id="671" href="Data.Nat.Combinatorics.html#3195" class="Function">nC1≡n</a><a id="676" class="Symbol">;</a> <a id="678" href="Data.Nat.Combinatorics.html#4831" class="Function">nCk+nC[k+1]≡[n+1]C[k+1]</a><a id="701" class="Symbol">)</a>
 <a id="703" class="Keyword">open</a> <a id="708" class="Keyword">import</a> <a id="715" href="Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="735" class="Symbol">as</a> <a id="738" class="Module">ℕ</a>
-  <a id="742" class="Keyword">using</a> <a id="748" class="Symbol">(</a><a id="749" href="Data.Nat.Properties.html#5072" class="Function">&lt;⇒&lt;ᵇ</a><a id="753" class="Symbol">;</a> <a id="755" href="Data.Nat.Properties.html#13416" class="Function">n&lt;1+n</a><a id="760" class="Symbol">;</a> <a id="762" href="Data.Nat.Properties.html#46678" class="Function">n∸n≡0</a><a id="767" class="Symbol">;</a> <a id="769" href="Data.Nat.Properties.html#47194" class="Function">∸-suc</a><a id="774" class="Symbol">)</a>
+  <a id="742" class="Keyword">using</a> <a id="748" class="Symbol">(</a><a id="749" href="Data.Nat.Properties.html#5072" class="Function">&lt;⇒&lt;ᵇ</a><a id="753" class="Symbol">;</a> <a id="755" href="Data.Nat.Properties.html#13416" class="Function">n&lt;1+n</a><a id="760" class="Symbol">;</a> <a id="762" href="Data.Nat.Properties.html#46995" class="Function">n∸n≡0</a><a id="767" class="Symbol">;</a> <a id="769" href="Data.Nat.Properties.html#47511" class="Function">∸-suc</a><a id="774" class="Symbol">)</a>
 <a id="776" class="Keyword">open</a> <a id="781" class="Keyword">import</a> <a id="788" href="Data.Fin.Base.html" class="Module">Data.Fin.Base</a> <a id="802" class="Symbol">as</a> <a id="805" class="Module">Fin</a>
   <a id="811" class="Keyword">using</a> <a id="817" class="Symbol">(</a><a id="818" href="Data.Fin.Base.html#1132" class="Datatype">Fin</a><a id="821" class="Symbol">;</a> <a id="823" href="Data.Fin.Base.html#1154" class="InductiveConstructor">zero</a><a id="827" class="Symbol">;</a> <a id="829" href="Data.Fin.Base.html#1175" class="InductiveConstructor">suc</a><a id="832" class="Symbol">;</a> <a id="834" href="Data.Fin.Base.html#1240" class="Function">toℕ</a><a id="837" class="Symbol">;</a> <a id="839" href="Data.Fin.Base.html#1825" class="Function">fromℕ</a><a id="844" class="Symbol">;</a> <a id="846" href="Data.Fin.Base.html#3055" class="Function">inject₁</a><a id="853" class="Symbol">)</a>
 <a id="855" class="Keyword">open</a> <a id="860" class="Keyword">import</a> <a id="867" href="Data.Fin.Patterns.html" class="Module">Data.Fin.Patterns</a> <a id="885" class="Keyword">using</a> <a id="891" class="Symbol">(</a><a id="892" href="Data.Fin.Patterns.html#422" class="InductiveConstructor">0F</a><a id="894" class="Symbol">)</a>
@@ -150,7 +150,7 @@
     <a id="5378" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a> <a id="5382" class="Symbol">=</a> <a id="5384" href="Data.Fin.Properties.html#16121" class="Function">toℕ-inject₁</a> <a id="5396" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a>
 
     <a id="5403" href="Algebra.Properties.Semiring.Binomial.html#5403" class="Function">[n-k]≡[n-j]</a> <a id="5415" class="Symbol">:</a> <a id="5417" href="Algebra.Properties.Semiring.Binomial.html#5221" class="Function">[n-k]</a> <a id="5423" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="5425" href="Algebra.Properties.Semiring.Binomial.html#5297" class="Function">[n-j]</a>
-    <a id="5435" href="Algebra.Properties.Semiring.Binomial.html#5403" class="Function">[n-k]≡[n-j]</a> <a id="5447" class="Symbol">=</a> <a id="5449" href="Relation.Binary.PropositionalEquality.Core.html#2080" class="Function">≡.trans</a> <a id="5457" class="Symbol">(</a><a id="5458" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="5463" class="Symbol">(</a><a id="5464" href="Algebra.Properties.Semiring.Binomial.html#4566" class="Bound">n</a> <a id="5466" href="Data.Nat.Base.html#4462" class="Primitive Operator">∸_</a><a id="5468" class="Symbol">)</a> <a id="5470" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a><a id="5473" class="Symbol">)</a> <a id="5475" class="Symbol">(</a><a id="5476" href="Data.Nat.Properties.html#47194" class="Function">∸-suc</a> <a id="5482" class="Symbol">(</a><a id="5483" href="Data.Fin.Properties.html#6538" class="Function">toℕ&lt;n</a> <a id="5489" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a><a id="5490" class="Symbol">))</a>
+    <a id="5435" href="Algebra.Properties.Semiring.Binomial.html#5403" class="Function">[n-k]≡[n-j]</a> <a id="5447" class="Symbol">=</a> <a id="5449" href="Relation.Binary.PropositionalEquality.Core.html#2080" class="Function">≡.trans</a> <a id="5457" class="Symbol">(</a><a id="5458" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="5463" class="Symbol">(</a><a id="5464" href="Algebra.Properties.Semiring.Binomial.html#4566" class="Bound">n</a> <a id="5466" href="Data.Nat.Base.html#4462" class="Primitive Operator">∸_</a><a id="5468" class="Symbol">)</a> <a id="5470" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a><a id="5473" class="Symbol">)</a> <a id="5475" class="Symbol">(</a><a id="5476" href="Data.Nat.Properties.html#47511" class="Function">∸-suc</a> <a id="5482" class="Symbol">(</a><a id="5483" href="Data.Fin.Properties.html#6538" class="Function">toℕ&lt;n</a> <a id="5489" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a><a id="5490" class="Symbol">))</a>
 
 <a id="5494" class="Comment">------------------------------------------------------------------------</a>
 <a id="5567" class="Comment">-- Now, a lemma characterising the sum of the term₁ and term₂ expressions</a>
@@ -177,7 +177,7 @@
 <a id="6400" class="Comment">{- remembering that i = fromℕ n, definitionally -}</a>
   <a id="6453" class="Keyword">rewrite</a> <a id="6461" href="Data.Fin.Properties.html#7562" class="Function">toℕ-fromℕ</a> <a id="6471" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
     <a id="6477" class="Symbol">|</a> <a id="6479" href="Data.Nat.Combinatorics.html#2974" class="Function">nCn≡1</a> <a id="6485" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
-    <a id="6491" class="Symbol">|</a> <a id="6493" href="Data.Nat.Properties.html#46678" class="Function">n∸n≡0</a> <a id="6499" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
+    <a id="6491" class="Symbol">|</a> <a id="6493" href="Data.Nat.Properties.html#46995" class="Function">n∸n≡0</a> <a id="6499" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
     <a id="6505" class="Symbol">|</a> <a id="6507" href="Algebra.Properties.Semiring.Binomial.html#5652" class="Function">n&lt;ᵇ1+n</a> <a id="6514" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
     <a id="6520" class="Symbol">=</a> <a id="6522" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
   <a id="6530" href="Algebra.Properties.Semiring.Binomial.html#497" class="Bound">x</a> <a id="6532" href="Algebra.Bundles.html#18634" class="Field Operator">*</a> <a id="6534" class="Symbol">((</a><a id="6536" href="Algebra.Properties.Semiring.Binomial.html#497" class="Bound">x</a> <a id="6538" href="Algebra.Definitions.RawSemiring.html#1256" class="Function Operator">^</a> <a id="6540" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a> <a id="6542" href="Algebra.Bundles.html#18634" class="Field Operator">*</a> <a id="6544" href="Algebra.Bundles.html#18688" class="Field">1#</a><a id="6546" class="Symbol">)</a> <a id="6548" href="Algebra.Bundles.html#18605" class="Field Operator">+</a> <a id="6550" href="Algebra.Bundles.html#18663" class="Field">0#</a><a id="6552" class="Symbol">)</a> <a id="6554" href="Algebra.Bundles.html#18605" class="Field Operator">+</a> <a id="6556" href="Algebra.Bundles.html#18663" class="Field">0#</a> <a id="6559" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="6562" href="Algebra.Structures.html#15044" class="Function">+-identityʳ</a> <a id="6574" class="Symbol">_</a> <a id="6576" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>

master/Codata.Musical.Colist.Infinite-merge.html

@@ -13,7 +13,7 @@
 <a id="386" class="Keyword">open</a> <a id="391" class="Keyword">import</a> <a id="398" href="Codata.Musical.Colist.html" class="Module">Codata.Musical.Colist</a> <a id="420" class="Symbol">as</a> <a id="423" class="Module">Colist</a> <a id="430" class="Keyword">hiding</a> <a id="437" class="Symbol">(</a><a id="438" href="Codata.Musical.Colist.Base.html#2138" class="Function Operator">_⋎_</a><a id="441" class="Symbol">)</a>
 <a id="443" class="Keyword">open</a> <a id="448" class="Keyword">import</a> <a id="455" href="Data.Nat.Base.html" class="Module">Data.Nat.Base</a> <a id="469" class="Keyword">using</a> <a id="475" class="Symbol">(</a><a id="476" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="477" class="Symbol">;</a> <a id="479" href="Agda.Builtin.Nat.html#221" class="InductiveConstructor">zero</a><a id="483" class="Symbol">;</a> <a id="485" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a><a id="488" class="Symbol">;</a> <a id="490" href="Data.Nat.Base.html#1697" class="Datatype Operator">_≤_</a><a id="493" class="Symbol">;</a> <a id="495" href="Data.Nat.Base.html#8018" class="Function Operator">_≥′_</a><a id="499" class="Symbol">;</a> <a id="501" href="Data.Nat.Base.html#7870" class="Function Operator">_&lt;′_</a><a id="505" class="Symbol">;</a> <a id="507" href="Data.Nat.Base.html#7711" class="Datatype Operator">_≤′_</a><a id="511" class="Symbol">)</a>
 <a id="513" class="Keyword">open</a> <a id="518" class="Keyword">import</a> <a id="525" href="Data.Nat.Induction.html" class="Module">Data.Nat.Induction</a> <a id="544" class="Keyword">using</a> <a id="550" class="Symbol">(</a><a id="551" href="Data.Nat.Induction.html#1666" class="Function">&lt;′-wellFounded</a><a id="565" class="Symbol">)</a>
-<a id="567" class="Keyword">open</a> <a id="572" class="Keyword">import</a> <a id="579" href="Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="599" class="Keyword">using</a> <a id="605" class="Symbol">(</a><a id="606" href="Data.Nat.Properties.html#64349" class="Function">s≤′s</a><a id="610" class="Symbol">)</a>
+<a id="567" class="Keyword">open</a> <a id="572" class="Keyword">import</a> <a id="579" href="Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="599" class="Keyword">using</a> <a id="605" class="Symbol">(</a><a id="606" href="Data.Nat.Properties.html#64666" class="Function">s≤′s</a><a id="610" class="Symbol">)</a>
 <a id="612" class="Keyword">open</a> <a id="617" class="Keyword">import</a> <a id="624" href="Data.Product.Base.html" class="Module">Data.Product.Base</a> <a id="642" class="Symbol">as</a> <a id="645" class="Module">Product</a> <a id="653" class="Keyword">using</a> <a id="659" class="Symbol">(</a><a id="660" href="Data.Product.Base.html#1618" class="Function Operator">_×_</a><a id="663" class="Symbol">;</a> <a id="665" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">_,_</a><a id="668" class="Symbol">;</a> <a id="670" href="Data.Product.Base.html#852" class="Function">∃</a><a id="671" class="Symbol">;</a> <a id="673" href="Data.Product.Base.html#907" class="Function">∃₂</a><a id="675" class="Symbol">;</a> <a id="677" href="Data.Product.Base.html#636" class="Field">proj₁</a><a id="682" class="Symbol">;</a> <a id="684" href="Data.Product.Base.html#650" class="Field">proj₂</a><a id="689" class="Symbol">)</a>
 <a id="691" class="Keyword">open</a> <a id="696" class="Keyword">import</a> <a id="703" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a> <a id="717" class="Keyword">using</a> <a id="723" class="Symbol">(</a><a id="724" href="Data.Sum.Base.html#625" class="Datatype Operator">_⊎_</a><a id="727" class="Symbol">;</a> <a id="729" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a><a id="733" class="Symbol">;</a> <a id="735" href="Data.Sum.Base.html#700" class="InductiveConstructor">inj₂</a><a id="739" class="Symbol">;</a> <a id="741" href="Data.Sum.Base.html#980" class="Function Operator">[_,_]′</a><a id="747" class="Symbol">)</a>
 <a id="749" class="Keyword">open</a> <a id="754" class="Keyword">import</a> <a id="761" href="Data.Sum.Properties.html" class="Module">Data.Sum.Properties</a> <a id="781" class="Keyword">using</a> <a id="787" class="Symbol">(</a><a id="788" href="Data.Sum.Properties.html#871" class="Function">inj₁-injective</a><a id="802" class="Symbol">;</a> <a id="804" href="Data.Sum.Properties.html#960" class="Function">inj₂-injective</a><a id="818" class="Symbol">)</a>
@@ -198,7 +198,7 @@
     <a id="6832" class="Symbol">...</a> <a id="6836" class="Symbol">|</a> <a id="6838" href="Data.Sum.Base.html#700" class="InductiveConstructor">inj₂</a> <a id="6843" href="Codata.Musical.Colist.Infinite-merge.html#6843" class="Bound">q</a> <a id="6845" class="Symbol">|</a> <a id="6847" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a> <a id="6852" class="Symbol">|</a> <a id="6854" href="Codata.Musical.Colist.Infinite-merge.html#6854" class="Bound">q≤p</a> <a id="6858" class="Symbol">=</a>
       <a id="6866" href="Data.Product.Base.html#2173" class="Function">Product.map</a> <a id="6878" href="Codata.Musical.Colist.Relation.Unary.Any.html#888" class="InductiveConstructor">there</a>
                <a id="6899" class="Symbol">(</a><a id="6900" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="6905" class="Symbol">(</a><a id="6906" href="Codata.Musical.Colist.Relation.Unary.Any.html#888" class="InductiveConstructor">there</a> <a id="6912" href="Function.Base.html#1134" class="Function Operator">∘</a> <a id="6914" class="Symbol">(</a><a id="6915" href="Function.Bundles.html#7416" class="Field">Inverse.from</a> <a id="6928" class="Symbol">(</a><a id="6929" href="Codata.Musical.Colist.Infinite-merge.html#2979" class="Function">Any-⋎P</a> <a id="6936" class="Bound">xs</a><a id="6938" class="Symbol">))</a> <a id="6941" href="Function.Base.html#1134" class="Function Operator">∘</a> <a id="6943" href="Data.Sum.Base.html#700" class="InductiveConstructor">inj₂</a><a id="6947" class="Symbol">))</a>
-               <a id="6965" class="Symbol">(</a><a id="6966" class="Bound">rec</a> <a id="6970" class="Symbol">(</a><a id="6971" href="Data.Nat.Properties.html#64349" class="Function">s≤′s</a> <a id="6976" href="Codata.Musical.Colist.Infinite-merge.html#6854" class="Bound">q≤p</a><a id="6979" class="Symbol">))</a>
+               <a id="6965" class="Symbol">(</a><a id="6966" class="Bound">rec</a> <a id="6970" class="Symbol">(</a><a id="6971" href="Data.Nat.Properties.html#64666" class="Function">s≤′s</a> <a id="6976" href="Codata.Musical.Colist.Infinite-merge.html#6854" class="Bound">q≤p</a><a id="6979" class="Symbol">))</a>
 
   <a id="6985" href="Codata.Musical.Colist.Infinite-merge.html#6985" class="Function">to∘from</a> <a id="6993" class="Symbol">=</a> <a id="6995" class="Symbol">λ</a> <a id="6997" href="Codata.Musical.Colist.Infinite-merge.html#6997" class="Bound">p</a> <a id="6999" class="Symbol">→</a> <a id="7001" href="Codata.Musical.Colist.Infinite-merge.html#5084" class="Function">from-injective</a> <a id="7016" class="Symbol">_</a> <a id="7018" class="Symbol">_</a> <a id="7020" class="Symbol">(</a><a id="7021" href="Data.Product.Base.html#650" class="Field">proj₂</a> <a id="7027" class="Symbol">(</a><a id="7028" href="Codata.Musical.Colist.Infinite-merge.html#6245" class="Function">to</a> <a id="7031" href="Codata.Musical.Colist.Infinite-merge.html#4649" class="Bound">xss</a> <a id="7035" class="Symbol">(</a><a id="7036" href="Codata.Musical.Colist.Infinite-merge.html#4802" class="Function">from</a> <a id="7041" href="Codata.Musical.Colist.Infinite-merge.html#6997" class="Bound">p</a><a id="7042" class="Symbol">)))</a>