Deploying to gh-pages from @ ea2a7ce 🚀

Author: github-merge-queue[bot]

master/Algebra.Construct.LexProduct.Inner.html

@@ -17,7 +17,7 @@
 <a id="625" class="Keyword">open</a> <a id="630" class="Keyword">import</a> <a id="637" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a> <a id="658" class="Keyword">using</a> <a id="664" class="Symbol">(</a><a id="665" href="Relation.Binary.Core.html#896" class="Function">Rel</a><a id="668" class="Symbol">)</a>
 <a id="670" class="Keyword">open</a> <a id="675" class="Keyword">import</a> <a id="682" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="710" class="Keyword">using</a> <a id="716" class="Symbol">(</a><a id="717" href="Relation.Binary.Definitions.html#6907" class="Function">Decidable</a><a id="726" class="Symbol">)</a>
 <a id="728" class="Keyword">open</a> <a id="733" class="Keyword">import</a> <a id="740" href="Relation.Nullary.Decidable.Core.html" class="Module">Relation.Nullary.Decidable.Core</a> <a id="772" class="Keyword">using</a> <a id="778" class="Symbol">(</a><a id="779" href="Relation.Nullary.Decidable.Core.html#2038" class="Field">does</a><a id="783" class="Symbol">;</a> <a id="785" href="Relation.Nullary.Decidable.Core.html#2105" class="InductiveConstructor">yes</a><a id="788" class="Symbol">;</a> <a id="790" href="Relation.Nullary.Decidable.Core.html#2142" class="InductiveConstructor">no</a><a id="792" class="Symbol">)</a>
-<a id="794" class="Keyword">open</a> <a id="799" class="Keyword">import</a> <a id="806" href="Relation.Nullary.Negation.Core.html" class="Module">Relation.Nullary.Negation.Core</a> <a id="837" class="Keyword">using</a> <a id="843" class="Symbol">(</a><a id="844" href="Relation.Nullary.Negation.Core.html#673" class="Function Operator">¬_</a><a id="846" class="Symbol">;</a> <a id="848" href="Relation.Nullary.Negation.Core.html#1355" class="Function">contradiction</a><a id="861" class="Symbol">;</a> <a id="863" href="Relation.Nullary.Negation.Core.html#1435" class="Function">contradiction₂</a><a id="877" class="Symbol">)</a>
+<a id="794" class="Keyword">open</a> <a id="799" class="Keyword">import</a> <a id="806" href="Relation.Nullary.Negation.Core.html" class="Module">Relation.Nullary.Negation.Core</a> <a id="837" class="Keyword">using</a> <a id="843" class="Symbol">(</a><a id="844" href="Relation.Nullary.Negation.Core.html#673" class="Function Operator">¬_</a><a id="846" class="Symbol">;</a> <a id="848" href="Relation.Nullary.Negation.Core.html#1355" class="Function">contradiction</a><a id="861" class="Symbol">;</a> <a id="863" href="Relation.Nullary.Negation.Core.html#1517" class="Function">contradiction₂</a><a id="877" class="Symbol">)</a>
 <a id="879" class="Keyword">import</a> <a id="886" href="Relation.Binary.Reasoning.Setoid.html" class="Module">Relation.Binary.Reasoning.Setoid</a> <a id="919" class="Symbol">as</a> <a id="922" class="Module">≈-Reasoning</a>
 
 <a id="935" class="Keyword">module</a> <a id="942" href="Algebra.Construct.LexProduct.html" class="Module">Algebra.Construct.LexProduct</a>
@@ -105,7 +105,7 @@
 
 <a id="sel"></a><a id="3314" href="Algebra.Construct.LexProduct.html#3314" class="Function">sel</a> <a id="3318" class="Symbol">:</a> <a id="3320" href="Algebra.Definitions.html#3969" class="Function">Selective</a> <a id="3330" href="Algebra.Construct.LexProduct.html#1146" class="Function Operator">_≈₁_</a> <a id="3335" href="Algebra.Bundles.html#1884" class="Function Operator">_∙_</a> <a id="3339" class="Symbol">→</a> <a id="3341" href="Algebra.Definitions.html#3969" class="Function">Selective</a> <a id="3351" href="Algebra.Construct.LexProduct.html#1261" class="Function Operator">_≈₂_</a> <a id="3356" href="Algebra.Construct.LexProduct.html#1242" class="Function Operator">_◦_</a> <a id="3360" class="Symbol">→</a> <a id="3362" href="Algebra.Definitions.html#3969" class="Function">Selective</a> <a id="3372" href="Algebra.Construct.LexProduct.html#1382" class="Function Operator">_≋_</a> <a id="3376" href="Algebra.Construct.LexProduct.html#1701" class="Function Operator">_⊕_</a>
 <a id="3380" href="Algebra.Construct.LexProduct.html#3314" class="Function">sel</a> <a id="3384" href="Algebra.Construct.LexProduct.html#3384" class="Bound">∙-sel</a> <a id="3390" href="Algebra.Construct.LexProduct.html#3390" class="Bound">◦-sel</a> <a id="3396" class="Symbol">(</a><a id="3397" href="Algebra.Construct.LexProduct.html#3397" class="Bound">a</a> <a id="3399" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="3401" href="Algebra.Construct.LexProduct.html#3401" class="Bound">x</a><a id="3402" class="Symbol">)</a> <a id="3404" class="Symbol">(</a><a id="3405" href="Algebra.Construct.LexProduct.html#3405" class="Bound">b</a> <a id="3407" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="3409" href="Algebra.Construct.LexProduct.html#3409" class="Bound">y</a><a id="3410" class="Symbol">)</a> <a id="3412" class="Keyword">with</a> <a id="3417" class="Symbol">(</a><a id="3418" href="Algebra.Construct.LexProduct.html#3397" class="Bound">a</a> <a id="3420" href="Algebra.Bundles.html#1884" class="Function Operator">∙</a> <a id="3422" href="Algebra.Construct.LexProduct.html#3405" class="Bound">b</a><a id="3423" class="Symbol">)</a> <a id="3425" href="Algebra.Construct.LexProduct.html#1026" class="Bound Operator">≟₁</a> <a id="3428" href="Algebra.Construct.LexProduct.html#3397" class="Bound">a</a> <a id="3430" class="Symbol">|</a> <a id="3432" class="Symbol">(</a><a id="3433" href="Algebra.Construct.LexProduct.html#3397" class="Bound">a</a> <a id="3435" href="Algebra.Bundles.html#1884" class="Function Operator">∙</a> <a id="3437" href="Algebra.Construct.LexProduct.html#3405" class="Bound">b</a><a id="3438" class="Symbol">)</a> <a id="3440" href="Algebra.Construct.LexProduct.html#1026" class="Bound Operator">≟₁</a> <a id="3443" href="Algebra.Construct.LexProduct.html#3405" class="Bound">b</a>
-<a id="3445" class="Symbol">...</a> <a id="3449" class="Symbol">|</a> <a id="3451" href="Relation.Nullary.Decidable.Core.html#2142" class="InductiveConstructor">no</a>  <a id="3455" href="Algebra.Construct.LexProduct.html#3455" class="Bound">ab≉a</a> <a id="3460" class="Symbol">|</a> <a id="3462" href="Relation.Nullary.Decidable.Core.html#2142" class="InductiveConstructor">no</a>  <a id="3466" href="Algebra.Construct.LexProduct.html#3466" class="Bound">ab≉b</a>  <a id="3472" class="Symbol">=</a> <a id="3474" href="Relation.Nullary.Negation.Core.html#1435" class="Function">contradiction₂</a> <a id="3489" class="Symbol">(</a><a id="3490" class="Bound">∙-sel</a> <a id="3496" class="Bound">a</a> <a id="3498" class="Bound">b</a><a id="3499" class="Symbol">)</a> <a id="3501" href="Algebra.Construct.LexProduct.html#3455" class="Bound">ab≉a</a> <a id="3506" href="Algebra.Construct.LexProduct.html#3466" class="Bound">ab≉b</a>
+<a id="3445" class="Symbol">...</a> <a id="3449" class="Symbol">|</a> <a id="3451" href="Relation.Nullary.Decidable.Core.html#2142" class="InductiveConstructor">no</a>  <a id="3455" href="Algebra.Construct.LexProduct.html#3455" class="Bound">ab≉a</a> <a id="3460" class="Symbol">|</a> <a id="3462" href="Relation.Nullary.Decidable.Core.html#2142" class="InductiveConstructor">no</a>  <a id="3466" href="Algebra.Construct.LexProduct.html#3466" class="Bound">ab≉b</a>  <a id="3472" class="Symbol">=</a> <a id="3474" href="Relation.Nullary.Negation.Core.html#1517" class="Function">contradiction₂</a> <a id="3489" class="Symbol">(</a><a id="3490" class="Bound">∙-sel</a> <a id="3496" class="Bound">a</a> <a id="3498" class="Bound">b</a><a id="3499" class="Symbol">)</a> <a id="3501" href="Algebra.Construct.LexProduct.html#3455" class="Bound">ab≉a</a> <a id="3506" href="Algebra.Construct.LexProduct.html#3466" class="Bound">ab≉b</a>
 <a id="3511" class="Symbol">...</a> <a id="3515" class="Symbol">|</a> <a id="3517" href="Relation.Nullary.Decidable.Core.html#2105" class="InductiveConstructor">yes</a> <a id="3521" href="Algebra.Construct.LexProduct.html#3521" class="Bound">ab≈a</a> <a id="3526" class="Symbol">|</a> <a id="3528" href="Relation.Nullary.Decidable.Core.html#2142" class="InductiveConstructor">no</a>  <a id="3532" class="Symbol">_</a>     <a id="3538" class="Symbol">=</a> <a id="3540" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a> <a id="3545" class="Symbol">(</a><a id="3546" href="Algebra.Construct.LexProduct.html#3521" class="Bound">ab≈a</a> <a id="3551" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="3553" href="Algebra.Construct.LexProduct.html#1281" class="Function">≈₂-refl</a><a id="3560" class="Symbol">)</a>
 <a id="3562" class="Symbol">...</a> <a id="3566" class="Symbol">|</a> <a id="3568" href="Relation.Nullary.Decidable.Core.html#2142" class="InductiveConstructor">no</a>  <a id="3572" class="Symbol">_</a>    <a id="3577" class="Symbol">|</a> <a id="3579" href="Relation.Nullary.Decidable.Core.html#2105" class="InductiveConstructor">yes</a> <a id="3583" href="Algebra.Construct.LexProduct.html#3583" class="Bound">ab≈b</a>  <a id="3589" class="Symbol">=</a> <a id="3591" href="Data.Sum.Base.html#700" class="InductiveConstructor">inj₂</a> <a id="3596" class="Symbol">(</a><a id="3597" href="Algebra.Construct.LexProduct.html#3583" class="Bound">ab≈b</a> <a id="3602" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="3604" href="Algebra.Construct.LexProduct.html#1281" class="Function">≈₂-refl</a><a id="3611" class="Symbol">)</a>
 <a id="3613" class="Symbol">...</a> <a id="3617" class="Symbol">|</a> <a id="3619" href="Relation.Nullary.Decidable.Core.html#2105" class="InductiveConstructor">yes</a> <a id="3623" href="Algebra.Construct.LexProduct.html#3623" class="Bound">ab≈a</a> <a id="3628" class="Symbol">|</a> <a id="3630" href="Relation.Nullary.Decidable.Core.html#2105" class="InductiveConstructor">yes</a> <a id="3634" href="Algebra.Construct.LexProduct.html#3634" class="Bound">ab≈b</a>  <a id="3640" class="Symbol">=</a> <a id="3642" href="Data.Sum.Base.html#1253" class="Function">map</a> <a id="3646" class="Symbol">(</a><a id="3647" href="Algebra.Construct.LexProduct.html#3623" class="Bound">ab≈a</a> <a id="3652" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,_</a><a id="3654" class="Symbol">)</a> <a id="3656" class="Symbol">(</a><a id="3657" href="Algebra.Construct.LexProduct.html#3634" class="Bound">ab≈b</a> <a id="3662" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,_</a><a id="3664" class="Symbol">)</a> <a id="3666" class="Symbol">(</a><a id="3667" class="Bound">◦-sel</a> <a id="3673" class="Bound">x</a> <a id="3675" class="Bound">y</a><a id="3676" class="Symbol">)</a>

master/Algebra.Construct.LexProduct.html

@@ -29,7 +29,7 @@
 <a id="1013" class="Keyword">open</a> <a id="1018" class="Keyword">import</a> <a id="1025" href="Data.Product.Base.html" class="Module">Data.Product.Base</a> <a id="1043" class="Keyword">using</a> <a id="1049" class="Symbol">(</a><a id="1050" href="Data.Product.Base.html#907" class="Function">∃₂</a><a id="1052" class="Symbol">;</a> <a id="1054" href="Data.Product.Base.html#1618" class="Function Operator">_×_</a><a id="1057" class="Symbol">;</a> <a id="1059" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">_,_</a><a id="1062" class="Symbol">)</a>
 <a id="1064" class="Keyword">open</a> <a id="1069" class="Keyword">import</a> <a id="1076" href="Relation.Binary.Reasoning.MultiSetoid.html" class="Module">Relation.Binary.Reasoning.MultiSetoid</a>
 <a id="1114" class="Keyword">open</a> <a id="1119" class="Keyword">import</a> <a id="1126" href="Relation.Nullary.html" class="Module">Relation.Nullary</a>          <a id="1152" class="Keyword">using</a> <a id="1158" class="Symbol">(</a><a id="1159" href="Relation.Nullary.Negation.Core.html#673" class="Function Operator">¬_</a><a id="1161" class="Symbol">)</a>
-<a id="1163" class="Keyword">open</a> <a id="1168" class="Keyword">import</a> <a id="1175" href="Relation.Nullary.Negation.html" class="Module">Relation.Nullary.Negation</a> <a id="1201" class="Keyword">using</a> <a id="1207" class="Symbol">(</a><a id="1208" href="Relation.Nullary.Negation.Core.html#1584" class="Function">contraposition</a><a id="1222" class="Symbol">)</a>
+<a id="1163" class="Keyword">open</a> <a id="1168" class="Keyword">import</a> <a id="1175" href="Relation.Nullary.Negation.html" class="Module">Relation.Nullary.Negation</a> <a id="1201" class="Keyword">using</a> <a id="1207" class="Symbol">(</a><a id="1208" href="Relation.Nullary.Negation.Core.html#1666" class="Function">contraposition</a><a id="1222" class="Symbol">)</a>
 
 <a id="1225" class="Keyword">module</a> <a id="A"></a><a id="1232" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1232" class="Module">A</a> <a id="1234" class="Symbol">=</a> <a id="1236" href="Algebra.Module.Bundles.html#11309" class="Module">Module</a> <a id="1243" href="Algebra.Module.Morphism.ModuleHomomorphism.html#617" class="Bound">modA</a>
 <a id="1248" class="Keyword">module</a> <a id="B"></a><a id="1255" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1255" class="Module">B</a> <a id="1257" class="Symbol">=</a> <a id="1259" href="Algebra.Module.Bundles.html#11309" class="Module">Module</a> <a id="1266" href="Algebra.Module.Morphism.ModuleHomomorphism.html#622" class="Bound">modB</a>
@@ -52,7 +52,7 @@
   <a id="1873" href="Algebra.Module.Bundles.html#11679" class="Function">B.0ᴹ</a>   <a id="1880" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a>
 
 <a id="fx≉0⇒x≉0"></a><a id="1883" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1883" class="Function">fx≉0⇒x≉0</a> <a id="1892" class="Symbol">:</a> <a id="1894" class="Symbol">∀</a> <a id="1896" class="Symbol">{</a><a id="1897" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1897" class="Bound">x</a><a id="1898" class="Symbol">}</a> <a id="1900" class="Symbol">→</a> <a id="1902" href="Algebra.Module.Morphism.ModuleHomomorphism.html#805" class="Bound">f</a> <a id="1904" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1897" class="Bound">x</a> <a id="1906" href="Algebra.Module.Bundles.html#3180" class="Function Operator">B.≉ᴹ</a> <a id="1911" href="Algebra.Module.Bundles.html#11679" class="Function">B.0ᴹ</a> <a id="1916" class="Symbol">→</a> <a id="1918" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1897" class="Bound">x</a> <a id="1920" href="Algebra.Module.Bundles.html#3180" class="Function Operator">A.≉ᴹ</a> <a id="1925" href="Algebra.Module.Bundles.html#11679" class="Function">A.0ᴹ</a>
-<a id="1930" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1883" class="Function">fx≉0⇒x≉0</a> <a id="1939" class="Symbol">=</a> <a id="1941" href="Relation.Nullary.Negation.Core.html#1584" class="Function">contraposition</a> <a id="1956" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1736" class="Function">x≈0⇒fx≈0</a>
+<a id="1930" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1883" class="Function">fx≉0⇒x≉0</a> <a id="1939" class="Symbol">=</a> <a id="1941" href="Relation.Nullary.Negation.Core.html#1666" class="Function">contraposition</a> <a id="1956" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1736" class="Function">x≈0⇒fx≈0</a>
 
 <a id="1966" class="Comment">-- Zero is a unique output of non-trivial (i.e. - ≉ `const 0`) linear map.</a>
 <a id="x≉0⇒f[x]≉0"></a><a id="2041" href="Algebra.Module.Morphism.ModuleHomomorphism.html#2041" class="Function">x≉0⇒f[x]≉0</a> <a id="2052" class="Symbol">:</a> <a id="2054" class="Symbol">∀</a> <a id="2056" class="Symbol">{</a><a id="2057" href="Algebra.Module.Morphism.ModuleHomomorphism.html#2057" class="Bound">x</a><a id="2058" class="Symbol">}</a> <a id="2060" class="Symbol">→</a> <a id="2062" href="Algebra.Module.Morphism.ModuleHomomorphism.html#1627" class="Function">NonTrivial</a> <a id="2073" href="Algebra.Module.Morphism.ModuleHomomorphism.html#2057" class="Bound">x</a> <a id="2075" class="Symbol">→</a> <a id="2077" href="Algebra.Module.Morphism.ModuleHomomorphism.html#2057" class="Bound">x</a> <a id="2079" href="Algebra.Module.Bundles.html#3180" class="Function Operator">A.≉ᴹ</a> <a id="2084" href="Algebra.Module.Bundles.html#11679" class="Function">A.0ᴹ</a> <a id="2089" class="Symbol">→</a> <a id="2091" href="Algebra.Module.Morphism.ModuleHomomorphism.html#805" class="Bound">f</a> <a id="2093" href="Algebra.Module.Morphism.ModuleHomomorphism.html#2057" class="Bound">x</a> <a id="2095" href="Algebra.Module.Bundles.html#3180" class="Function Operator">B.≉ᴹ</a> <a id="2100" href="Algebra.Module.Bundles.html#11679" class="Function">B.0ᴹ</a>