Deploying to gh-pages from @ c2e7c13 🚀

Author: JacquesCarette

Categories.Adjoint.AFT.html

@@ -162,7 +162,7 @@
                 <a id="4596" class="Symbol">{</a> <a id="4598" href="Categories.Diagram.Cone.html#717" class="Field">arr</a>     <a id="4606" class="Symbol">=</a> <a id="4608" href="Categories.Functor.Core.html#806" class="Function">R.₁</a> <a id="4612" class="Symbol">(</a><a id="4613" href="Categories.Diagram.Limit.html#1271" class="Function">LimF′.rep</a> <a id="4623" class="Symbol">(</a><a id="4624" href="Categories.Adjoint.AFT.html#4210" class="Function">K-conv</a> <a id="4631" href="Categories.Adjoint.AFT.html#4429" class="Bound">K</a><a id="4632" class="Symbol">))</a> <a id="4635" href="Categories.Category.Core.html#656" class="Function Operator">D.∘</a> <a id="4639" href="Categories.Category.Construction.Comma.html#1060" class="Field">CommaObj.f</a> <a id="4650" href="Categories.Diagram.Cone.html#578" class="Field">N</a>
                 <a id="4668" class="Symbol">;</a> <a id="4670" href="Categories.Diagram.Cone.html#742" class="Field">commute</a> <a id="4678" class="Symbol">=</a> <a id="4680" class="Symbol">λ</a> <a id="4682" class="Symbol">{</a><a id="4683" href="Categories.Adjoint.AFT.html#4683" class="Bound">j</a><a id="4684" class="Symbol">}</a> <a id="4686" class="Symbol">→</a> <a id="4688" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
                   <a id="4712" href="Categories.Diagram.Limit.html#1169" class="Function">LimRF′.proj</a> <a id="4724" href="Categories.Adjoint.AFT.html#4683" class="Bound">j</a> <a id="4726" href="Categories.Category.Core.html#656" class="Function Operator">D.∘</a> <a id="4730" href="Categories.Functor.Core.html#806" class="Function">R.₁</a> <a id="4734" class="Symbol">(</a><a id="4735" href="Categories.Diagram.Limit.html#1271" class="Function">LimF′.rep</a> <a id="4745" class="Symbol">(</a><a id="4746" href="Categories.Adjoint.AFT.html#4210" class="Function">K-conv</a> <a id="4753" href="Categories.Adjoint.AFT.html#4429" class="Bound">K</a><a id="4754" class="Symbol">))</a> <a id="4757" href="Categories.Category.Core.html#656" class="Function Operator">D.∘</a> <a id="4761" href="Categories.Category.Construction.Comma.html#1060" class="Field">CommaObj.f</a> <a id="4772" href="Categories.Diagram.Cone.html#578" class="Field">N</a>
-                    <a id="4794" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="4797" href="Categories.Morphism.Reasoning.Core.html#3113" class="Function">pullˡ</a> <a id="4803" class="Symbol">(</a><a id="4804" href="Categories.Functor.Properties.html#2211" class="Function Operator">[</a> <a id="4806" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a> <a id="4808" href="Categories.Functor.Properties.html#2211" class="Function Operator">]-resp-∘</a> <a id="4817" href="Categories.Diagram.Limit.html#1636" class="Function">LimF′.commute</a><a id="4830" class="Symbol">)</a> <a id="4832" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
+                    <a id="4794" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="4797" href="Categories.Morphism.Reasoning.Core.html#3113" class="Function">pullˡ</a> <a id="4803" class="Symbol">(</a><a id="4804" href="Categories.Functor.Properties.html#2548" class="Function Operator">[</a> <a id="4806" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a> <a id="4808" href="Categories.Functor.Properties.html#2548" class="Function Operator">]-resp-∘</a> <a id="4817" href="Categories.Diagram.Limit.html#1636" class="Function">LimF′.commute</a><a id="4830" class="Symbol">)</a> <a id="4832" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
                   <a id="4852" href="Categories.Functor.Core.html#806" class="Function">R.₁</a> <a id="4856" class="Symbol">(</a><a id="4857" href="Categories.Category.Construction.Comma.html#1451" class="Field">Comma⇒.h</a> <a id="4866" class="Symbol">(</a><a id="4867" href="Categories.Diagram.Cone.html#415" class="Function">ψ</a> <a id="4869" href="Categories.Adjoint.AFT.html#4683" class="Bound">j</a><a id="4870" class="Symbol">))</a> <a id="4873" href="Categories.Category.Core.html#656" class="Function Operator">D.∘</a> <a id="4877" href="Categories.Category.Construction.Comma.html#1060" class="Field">CommaObj.f</a> <a id="4888" href="Categories.Diagram.Cone.html#578" class="Field">N</a>
                     <a id="4910" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="4913" href="Categories.Category.Construction.Comma.html#1481" class="Field">Comma⇒.commute</a> <a id="4928" class="Symbol">(</a><a id="4929" href="Categories.Diagram.Cone.html#415" class="Function">ψ</a> <a id="4931" href="Categories.Adjoint.AFT.html#4683" class="Bound">j</a><a id="4932" class="Symbol">)</a> <a id="4934" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
                   <a id="4954" href="Categories.Category.Construction.Comma.html#1060" class="Field">CommaObj.f</a> <a id="4965" class="Symbol">(</a><a id="4966" href="Categories.Functor.Core.html#432" class="Field">F.F₀</a> <a id="4971" href="Categories.Adjoint.AFT.html#4683" class="Bound">j</a><a id="4972" class="Symbol">)</a> <a id="4974" href="Categories.Category.Core.html#656" class="Function Operator">D.∘</a> <a id="4978" href="Categories.Category.Core.html#630" class="Function">D.id</a>

Categories.Adjoint.Construction.CoEilenbergMoore.html

@@ -54,7 +54,7 @@
 <a id="1369" href="Categories.Adjoint.Construction.CoEilenbergMoore.html#1336" class="Function">UC≃M</a> <a id="1374" class="Symbol">=</a> <a id="1376" href="Categories.NaturalTransformation.NaturalIsomorphism.html#2810" class="Function">niHelper</a> <a id="1385" class="Symbol">(</a><a id="1386" class="Keyword">record</a>
  <a id="1394" class="Symbol">{</a> <a id="1396" href="Categories.NaturalTransformation.NaturalIsomorphism.html#2606" class="Field">η</a> <a id="1398" class="Symbol">=</a> <a id="1400" class="Symbol">λ</a> <a id="1402" href="Categories.Adjoint.Construction.CoEilenbergMoore.html#1402" class="Bound">_</a> <a id="1404" class="Symbol">→</a> <a id="1406" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="1409" href="Categories.Category.Core.html#630" class="Function">C.id</a>
  <a id="1415" class="Symbol">;</a> <a id="1417" href="Categories.NaturalTransformation.NaturalIsomorphism.html#2648" class="Field">η⁻¹</a> <a id="1421" class="Symbol">=</a> <a id="1423" class="Symbol">λ</a> <a id="1425" href="Categories.Adjoint.Construction.CoEilenbergMoore.html#1425" class="Bound">_</a> <a id="1427" class="Symbol">→</a> <a id="1429" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="1432" href="Categories.Category.Core.html#630" class="Function">C.id</a>
- <a id="1438" class="Symbol">;</a> <a id="1440" href="Categories.NaturalTransformation.NaturalIsomorphism.html#2690" class="Field">commute</a> <a id="1448" class="Symbol">=</a> <a id="1450" class="Symbol">λ</a> <a id="1452" href="Categories.Adjoint.Construction.CoEilenbergMoore.html#1452" class="Bound">f</a> <a id="1454" class="Symbol">→</a> <a id="1456" href="Categories.Functor.Properties.html#2461" class="Function Operator">[</a> <a id="1458" href="Categories.Comonad.html#529" class="Field">M.F</a> <a id="1462" href="Categories.Functor.Properties.html#2461" class="Function Operator">]-resp-square</a> <a id="1476" href="Categories.Morphism.Reasoning.Core.html#1309" class="Function">id-comm-sym</a>
+ <a id="1438" class="Symbol">;</a> <a id="1440" href="Categories.NaturalTransformation.NaturalIsomorphism.html#2690" class="Field">commute</a> <a id="1448" class="Symbol">=</a> <a id="1450" class="Symbol">λ</a> <a id="1452" href="Categories.Adjoint.Construction.CoEilenbergMoore.html#1452" class="Bound">f</a> <a id="1454" class="Symbol">→</a> <a id="1456" href="Categories.Functor.Properties.html#2798" class="Function Operator">[</a> <a id="1458" href="Categories.Comonad.html#529" class="Field">M.F</a> <a id="1462" href="Categories.Functor.Properties.html#2798" class="Function Operator">]-resp-square</a> <a id="1476" href="Categories.Morphism.Reasoning.Core.html#1309" class="Function">id-comm-sym</a>
  <a id="1489" class="Symbol">;</a> <a id="1491" href="Categories.NaturalTransformation.NaturalIsomorphism.html#2760" class="Field">iso</a> <a id="1495" class="Symbol">=</a> <a id="1497" class="Symbol">λ</a> <a id="1499" href="Categories.Adjoint.Construction.CoEilenbergMoore.html#1499" class="Bound">_</a> <a id="1501" class="Symbol">→</a> <a id="1503" class="Keyword">record</a>
     <a id="1514" class="Symbol">{</a> <a id="1516" href="Categories.Morphism.html#1586" class="Field">isoˡ</a> <a id="1521" class="Symbol">=</a> <a id="1523" href="Categories.Morphism.Reasoning.Core.html#4013" class="Function">elimˡ</a> <a id="1529" href="Categories.Functor.Core.html#511" class="Function">identity</a> <a id="1538" href="Categories.Category.Core.html#3061" class="Function Operator">○</a> <a id="1540" href="Categories.Functor.Core.html#511" class="Function">identity</a>
     <a id="1553" class="Symbol">;</a> <a id="1555" href="Categories.Morphism.html#1612" class="Field">isoʳ</a> <a id="1560" class="Symbol">=</a> <a id="1562" href="Categories.Morphism.Reasoning.Core.html#4013" class="Function">elimˡ</a> <a id="1568" href="Categories.Functor.Core.html#511" class="Function">identity</a> <a id="1577" href="Categories.Category.Core.html#3061" class="Function Operator">○</a> <a id="1579" href="Categories.Functor.Core.html#511" class="Function">identity</a>

Categories.Adjoint.Construction.CoKleisli.html

@@ -93,7 +93,7 @@
    <a id="3309" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3312" href="Categories.Adjoint.Construction.CoKleisli.html#3033" class="Bound">f</a> <a id="3314" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3316" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3319" href="Categories.Category.Core.html#630" class="Function">C.id</a>                       <a id="3346" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a>
   <a id="3350" href="Categories.Adjoint.Construction.CoKleisli.html#3350" class="Function">from-commute</a> <a id="3363" class="Symbol">:</a> <a id="3365" class="Symbol">{</a><a id="3366" href="Categories.Adjoint.Construction.CoKleisli.html#3366" class="Bound">X</a> <a id="3368" href="Categories.Adjoint.Construction.CoKleisli.html#3368" class="Bound">Y</a> <a id="3370" class="Symbol">:</a> <a id="3372" href="Categories.Category.Core.html#559" class="Function">Obj</a><a id="3375" class="Symbol">}</a> <a id="3377" class="Symbol">→</a> <a id="3379" class="Symbol">(</a><a id="3380" href="Categories.Adjoint.Construction.CoKleisli.html#3380" class="Bound">f</a> <a id="3382" class="Symbol">:</a> <a id="3384" href="Categories.Adjoint.Construction.CoKleisli.html#3366" class="Bound">X</a> <a id="3386" href="Categories.Category.Core.html#575" class="Function Operator">⇒</a> <a id="3388" href="Categories.Adjoint.Construction.CoKleisli.html#3368" class="Bound">Y</a><a id="3389" class="Symbol">)</a> <a id="3391" class="Symbol">→</a> <a id="3393" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3396" href="Categories.Category.Core.html#630" class="Function">C.id</a> <a id="3401" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3403" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3406" href="Categories.Adjoint.Construction.CoKleisli.html#3380" class="Bound">f</a> <a id="3408" href="Categories.Category.Core.html#595" class="Function Operator">≈</a> <a id="3410" class="Symbol">(</a><a id="3411" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3414" class="Symbol">(</a><a id="3415" href="Categories.Adjoint.Construction.CoKleisli.html#3380" class="Bound">f</a> <a id="3417" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3419" href="Categories.NaturalTransformation.Core.html#783" class="Function">M.ε.η</a> <a id="3425" href="Categories.Adjoint.Construction.CoKleisli.html#3366" class="Bound">X</a><a id="3426" class="Symbol">)</a> <a id="3428" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3430" href="Categories.NaturalTransformation.Core.html#783" class="Function">M.δ.η</a> <a id="3436" href="Categories.Adjoint.Construction.CoKleisli.html#3366" class="Bound">X</a><a id="3437" class="Symbol">)</a> <a id="3439" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3441" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3444" href="Categories.Category.Core.html#630" class="Function">C.id</a>
   <a id="3451" href="Categories.Adjoint.Construction.CoKleisli.html#3350" class="Function">from-commute</a> <a id="3464" class="Symbol">{</a><a id="3465" href="Categories.Adjoint.Construction.CoKleisli.html#3465" class="Bound">X</a><a id="3466" class="Symbol">}</a> <a id="3468" class="Symbol">{</a><a id="3469" href="Categories.Adjoint.Construction.CoKleisli.html#3469" class="Bound">Y</a><a id="3470" class="Symbol">}</a> <a id="3472" href="Categories.Adjoint.Construction.CoKleisli.html#3472" class="Bound">f</a> <a id="3474" class="Symbol">=</a> <a id="3476" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
-      <a id="3488" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3491" href="Categories.Category.Core.html#630" class="Function">C.id</a> <a id="3496" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3498" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3501" href="Categories.Adjoint.Construction.CoKleisli.html#3472" class="Bound">f</a>                            <a id="3530" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="3533" href="Categories.Functor.Properties.html#2461" class="Function Operator">[</a> <a id="3535" href="Categories.Comonad.html#529" class="Field">M.F</a> <a id="3539" href="Categories.Functor.Properties.html#2461" class="Function Operator">]-resp-square</a> <a id="3553" href="Categories.Morphism.Reasoning.Core.html#1309" class="Function">id-comm-sym</a> <a id="3565" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
+      <a id="3488" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3491" href="Categories.Category.Core.html#630" class="Function">C.id</a> <a id="3496" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3498" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3501" href="Categories.Adjoint.Construction.CoKleisli.html#3472" class="Bound">f</a>                            <a id="3530" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="3533" href="Categories.Functor.Properties.html#2798" class="Function Operator">[</a> <a id="3535" href="Categories.Comonad.html#529" class="Field">M.F</a> <a id="3539" href="Categories.Functor.Properties.html#2798" class="Function Operator">]-resp-square</a> <a id="3553" href="Categories.Morphism.Reasoning.Core.html#1309" class="Function">id-comm-sym</a> <a id="3565" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
       <a id="3573" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3576" href="Categories.Adjoint.Construction.CoKleisli.html#3472" class="Bound">f</a> <a id="3578" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3580" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3583" href="Categories.Category.Core.html#630" class="Function">C.id</a>                            <a id="3615" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="3618" href="Categories.Morphism.Reasoning.Core.html#3964" class="Function">introʳ</a> <a id="3625" class="Symbol">(</a><a id="3626" href="Categories.Comonad.html#911" class="Field">Comonad.identityˡ</a> <a id="3644" href="Categories.Adjoint.Construction.CoKleisli.html#262" class="Bound">M</a><a id="3645" class="Symbol">)</a> <a id="3647" href="Categories.Category.Core.html#2837" class="Function Operator">⟩∘⟨refl</a> <a id="3655" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
       <a id="3663" class="Symbol">(</a><a id="3664" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3667" href="Categories.Adjoint.Construction.CoKleisli.html#3472" class="Bound">f</a> <a id="3669" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3671" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3674" class="Symbol">(</a><a id="3675" href="Categories.NaturalTransformation.Core.html#783" class="Function">M.ε.η</a> <a id="3681" href="Categories.Adjoint.Construction.CoKleisli.html#3465" class="Bound">X</a><a id="3682" class="Symbol">)</a> <a id="3684" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3686" href="Categories.NaturalTransformation.Core.html#783" class="Function">M.δ.η</a> <a id="3692" href="Categories.Adjoint.Construction.CoKleisli.html#3465" class="Bound">X</a><a id="3693" class="Symbol">)</a> <a id="3695" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3697" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3700" href="Categories.Category.Core.html#630" class="Function">C.id</a> <a id="3705" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="3708" href="Categories.Morphism.Reasoning.Core.html#3113" class="Function">pullˡ</a> <a id="3714" class="Symbol">(</a><a id="3715" href="Relation.Binary.Structures.html#1622" class="Function">sym</a> <a id="3719" href="Categories.Functor.Core.html#565" class="Function">homomorphism</a><a id="3731" class="Symbol">)</a> <a id="3733" href="Categories.Category.Core.html#2837" class="Function Operator">⟩∘⟨refl</a> <a id="3741" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
       <a id="3749" class="Symbol">(</a><a id="3750" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3753" class="Symbol">(</a><a id="3754" href="Categories.Adjoint.Construction.CoKleisli.html#3472" class="Bound">f</a> <a id="3756" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3758" href="Categories.NaturalTransformation.Core.html#783" class="Function">M.ε.η</a> <a id="3764" href="Categories.Adjoint.Construction.CoKleisli.html#3465" class="Bound">X</a><a id="3765" class="Symbol">)</a> <a id="3767" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3769" href="Categories.NaturalTransformation.Core.html#783" class="Function">M.δ.η</a> <a id="3775" href="Categories.Adjoint.Construction.CoKleisli.html#3465" class="Bound">X</a><a id="3776" class="Symbol">)</a> <a id="3778" href="Categories.Category.Core.html#656" class="Function Operator">∘</a> <a id="3780" href="Categories.Functor.Core.html#455" class="Function">F₁</a> <a id="3783" href="Categories.Category.Core.html#630" class="Function">C.id</a>    <a id="3791" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a>