Deploying to gh-pages from @ 9429496 🚀

Author: github-merge-queue[bot]

master/Algebra.Lattice.Morphism.Construct.Composition.html

@@ -60,6 +60,6 @@
     <a id="2272" class="Symbol">→</a> <a id="2274" href="Algebra.Lattice.Morphism.Structures.html#2924" class="Record">IsLatticeIsomorphism</a> <a id="2295" href="Algebra.Lattice.Morphism.Construct.Composition.html#942" class="Bound">L₁</a> <a id="2298" href="Algebra.Lattice.Morphism.Construct.Composition.html#1006" class="Bound">L₃</a> <a id="2301" class="Symbol">(</a><a id="2302" href="Algebra.Lattice.Morphism.Construct.Composition.html#1146" class="Bound">g</a> <a id="2304" href="Function.Base.html#1115" class="Function Operator">∘</a> <a id="2306" href="Algebra.Lattice.Morphism.Construct.Composition.html#1107" class="Bound">f</a><a id="2307" class="Symbol">)</a>
   <a id="2311" href="Algebra.Lattice.Morphism.Construct.Composition.html#2177" class="Function">isLatticeIsomorphism</a> <a id="2332" href="Algebra.Lattice.Morphism.Construct.Composition.html#2332" class="Bound">f-iso</a> <a id="2338" href="Algebra.Lattice.Morphism.Construct.Composition.html#2338" class="Bound">g-iso</a> <a id="2344" class="Symbol">=</a> <a id="2346" class="Keyword">record</a>
     <a id="2357" class="Symbol">{</a> <a id="2359" href="Algebra.Lattice.Morphism.Structures.html#3005" class="Field">isLatticeMonomorphism</a> <a id="2381" class="Symbol">=</a> <a id="2383" href="Algebra.Lattice.Morphism.Construct.Composition.html#1742" class="Function">isLatticeMonomorphism</a> <a id="2405" href="Algebra.Lattice.Morphism.Structures.html#3005" class="Function">F.isLatticeMonomorphism</a> <a id="2429" href="Algebra.Lattice.Morphism.Structures.html#3005" class="Field">G.isLatticeMonomorphism</a>
-    <a id="2457" class="Symbol">;</a> <a id="2459" href="Algebra.Lattice.Morphism.Structures.html#3061" class="Field">surjective</a>            <a id="2481" class="Symbol">=</a> <a id="2483" href="Function.Construct.Composition.html#1220" class="Function">Func.surjective</a> <a id="2499" class="Symbol">_</a> <a id="2501" class="Symbol">_</a> <a id="2503" class="Symbol">(</a><a id="2504" href="Algebra.Lattice.Bundles.Raw.html#591" class="Field Operator">_≈_</a> <a id="2508" href="Algebra.Lattice.Morphism.Construct.Composition.html#1006" class="Bound">L₃</a><a id="2510" class="Symbol">)</a> <a id="2512" href="Algebra.Lattice.Morphism.Structures.html#3061" class="Function">F.surjective</a> <a id="2525" href="Algebra.Lattice.Morphism.Structures.html#3061" class="Field">G.surjective</a>
+    <a id="2457" class="Symbol">;</a> <a id="2459" href="Algebra.Lattice.Morphism.Structures.html#3061" class="Field">surjective</a>            <a id="2481" class="Symbol">=</a> <a id="2483" href="Function.Construct.Composition.html#1427" class="Function">Func.surjective</a> <a id="2499" class="Symbol">_</a> <a id="2501" class="Symbol">_</a> <a id="2503" class="Symbol">(</a><a id="2504" href="Algebra.Lattice.Bundles.Raw.html#591" class="Field Operator">_≈_</a> <a id="2508" href="Algebra.Lattice.Morphism.Construct.Composition.html#1006" class="Bound">L₃</a><a id="2510" class="Symbol">)</a> <a id="2512" href="Algebra.Lattice.Morphism.Structures.html#3061" class="Function">F.surjective</a> <a id="2525" href="Algebra.Lattice.Morphism.Structures.html#3061" class="Field">G.surjective</a>
     <a id="2542" class="Symbol">}</a> <a id="2544" class="Keyword">where</a> <a id="2550" class="Keyword">module</a> <a id="2557" href="Algebra.Lattice.Morphism.Construct.Composition.html#2557" class="Module">F</a> <a id="2559" class="Symbol">=</a> <a id="2561" href="Algebra.Lattice.Morphism.Structures.html#2924" class="Module">IsLatticeIsomorphism</a> <a id="2582" href="Algebra.Lattice.Morphism.Construct.Composition.html#2332" class="Bound">f-iso</a><a id="2587" class="Symbol">;</a> <a id="2589" class="Keyword">module</a> <a id="2596" href="Algebra.Lattice.Morphism.Construct.Composition.html#2596" class="Module">G</a> <a id="2598" class="Symbol">=</a> <a id="2600" href="Algebra.Lattice.Morphism.Structures.html#2924" class="Module">IsLatticeIsomorphism</a> <a id="2621" href="Algebra.Lattice.Morphism.Construct.Composition.html#2338" class="Bound">g-iso</a>
 </pre></body></html>

master/Algebra.Lattice.Morphism.Construct.Identity.html

@@ -42,6 +42,6 @@
   <a id="1298" href="Algebra.Lattice.Morphism.Construct.Identity.html#1298" class="Function">isLatticeIsomorphism</a> <a id="1319" class="Symbol">:</a> <a id="1321" href="Algebra.Lattice.Morphism.Structures.html#2924" class="Record">IsLatticeIsomorphism</a> <a id="1342" href="Function.Base.html#704" class="Function">id</a>
   <a id="1347" href="Algebra.Lattice.Morphism.Construct.Identity.html#1298" class="Function">isLatticeIsomorphism</a> <a id="1368" class="Symbol">=</a> <a id="1370" class="Keyword">record</a>
     <a id="1381" class="Symbol">{</a> <a id="1383" href="Algebra.Lattice.Morphism.Structures.html#3005" class="Field">isLatticeMonomorphism</a> <a id="1405" class="Symbol">=</a> <a id="1407" href="Algebra.Lattice.Morphism.Construct.Identity.html#1134" class="Function">isLatticeMonomorphism</a>
-    <a id="1433" class="Symbol">;</a> <a id="1435" href="Algebra.Lattice.Morphism.Structures.html#3061" class="Field">surjective</a> <a id="1446" class="Symbol">=</a> <a id="1448" href="Function.Construct.Identity.html#1179" class="Function">Id.surjective</a> <a id="1462" class="Symbol">_</a>
+    <a id="1433" class="Symbol">;</a> <a id="1435" href="Algebra.Lattice.Morphism.Structures.html#3061" class="Field">surjective</a> <a id="1446" class="Symbol">=</a> <a id="1448" href="Function.Construct.Identity.html#1385" class="Function">Id.surjective</a> <a id="1462" class="Symbol">_</a>
     <a id="1468" class="Symbol">}</a>
 </pre></body></html>

master/Algebra.Lattice.Properties.BooleanAlgebra.Expression.html

@@ -172,7 +172,7 @@
     <a id="7220" class="Keyword">using</a> <a id="7226" class="Symbol">(</a><a id="7227" href="Effect.Applicative.html#1145" class="Field">pure</a><a id="7231" class="Symbol">;</a> <a id="7233" href="Effect.Applicative.html#1349" class="Function">zipWith</a><a id="7240" class="Symbol">)</a> <a id="7242" class="Keyword">renaming</a> <a id="7251" class="Symbol">(</a><a id="7252" href="Effect.Functor.html#710" class="Function Operator">_&lt;$&gt;_</a> <a id="7258" class="Symbol">to</a> <a id="7261" class="Function Operator">map</a><a id="7264" class="Symbol">)</a>
 
   <a id="7269" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7269" class="Function Operator">⟦_⟧Id</a> <a id="7275" class="Symbol">:</a> <a id="7277" class="Symbol">∀</a> <a id="7279" class="Symbol">{</a><a id="7280" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7280" class="Bound">n</a><a id="7281" class="Symbol">}</a> <a id="7283" class="Symbol">→</a> <a id="7285" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#1296" class="Datatype">Expr</a> <a id="7290" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7280" class="Bound">n</a> <a id="7292" class="Symbol">→</a> <a id="7294" href="Data.Vec.Base.html#1119" class="Datatype">Vec</a> <a id="7298" href="Algebra.Lattice.Bundles.html#5889" class="Field">Carrier</a> <a id="7306" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7280" class="Bound">n</a> <a id="7308" class="Symbol">→</a> <a id="7310" href="Algebra.Lattice.Bundles.html#5889" class="Field">Carrier</a>
-  <a id="7320" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7269" class="Function Operator">⟦_⟧Id</a> <a id="7326" class="Symbol">=</a> <a id="7328" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#1633" class="Function Operator">Semantics.⟦_⟧</a> <a id="7342" href="Function.Identity.Effectful.html#656" class="Function">Identity.applicative</a>
+  <a id="7320" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7269" class="Function Operator">⟦_⟧Id</a> <a id="7326" class="Symbol">=</a> <a id="7328" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#1633" class="Function Operator">Semantics.⟦_⟧</a> <a id="7342" href="Function.Identity.Effectful.html#753" class="Function">Identity.applicative</a>
 
   <a id="7366" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7366" class="Function Operator">⟦_⟧Vec</a> <a id="7373" class="Symbol">:</a> <a id="7375" class="Symbol">∀</a> <a id="7377" class="Symbol">{</a><a id="7378" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7378" class="Bound">m</a> <a id="7380" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7380" class="Bound">n</a><a id="7381" class="Symbol">}</a> <a id="7383" class="Symbol">→</a> <a id="7385" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#1296" class="Datatype">Expr</a> <a id="7390" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7380" class="Bound">n</a> <a id="7392" class="Symbol">→</a> <a id="7394" href="Data.Vec.Base.html#1119" class="Datatype">Vec</a> <a id="7398" class="Symbol">(</a><a id="7399" href="Data.Vec.Base.html#1119" class="Datatype">Vec</a> <a id="7403" href="Algebra.Lattice.Bundles.html#5889" class="Field">Carrier</a> <a id="7411" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7378" class="Bound">m</a><a id="7412" class="Symbol">)</a> <a id="7414" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7380" class="Bound">n</a> <a id="7416" class="Symbol">→</a> <a id="7418" href="Data.Vec.Base.html#1119" class="Datatype">Vec</a> <a id="7422" href="Algebra.Lattice.Bundles.html#5889" class="Field">Carrier</a> <a id="7430" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7378" class="Bound">m</a>
   <a id="7434" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#7366" class="Function Operator">⟦_⟧Vec</a> <a id="7441" class="Symbol">=</a> <a id="7443" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#1633" class="Function Operator">Semantics.⟦_⟧</a> <a id="7457" href="Data.Vec.Effectful.html#992" class="Function">Vec.applicative</a>