Deploying to gh-pages from @ 46bfebd 🚀

Author: JacquesCarette

Categories.Adjoint.Properties.html

@@ -32,7 +32,7 @@
 <a id="1741" class="Keyword">open</a> <a id="1746" class="Keyword">import</a> <a id="1753" href="Categories.Morphism.Universal.html" class="Module">Categories.Morphism.Universal</a> <a id="1783" class="Keyword">using</a> <a id="1789" class="Symbol">(</a><a id="1790" href="Categories.Morphism.Universal.html#259" class="Record">UniversalMorphism</a><a id="1807" class="Symbol">)</a>
 <a id="1809" class="Keyword">import</a> <a id="1816" href="Categories.Yoneda.Properties.html" class="Module">Categories.Yoneda.Properties</a> <a id="1845" class="Symbol">as</a> <a id="1848" class="Module">YP</a> <a id="1851" class="Keyword">using</a> <a id="1857" class="Symbol">(</a><a id="1858" href="Categories.Yoneda.Properties.html#5232" class="Function">yoneda-NI</a><a id="1867" class="Symbol">)</a>
 
-<a id="1870" class="Keyword">import</a> <a id="1877" href="Categories.Diagram.Duality.html" class="Module">Categories.Diagram.Duality</a> <a id="1904" class="Symbol">as</a> <a id="1907" class="Module">Duality</a> <a id="1915" class="Keyword">using</a> <a id="1921" class="Symbol">(</a><a id="1922" href="Categories.Diagram.Duality.html#4047" class="Function">coLimit⇒Colimit</a><a id="1937" class="Symbol">;</a> <a id="1939" href="Categories.Diagram.Duality.html#4418" class="Function">Colimit⇒coLimit</a><a id="1954" class="Symbol">)</a>
+<a id="1870" class="Keyword">import</a> <a id="1877" href="Categories.Diagram.Duality.html" class="Module">Categories.Diagram.Duality</a> <a id="1904" class="Symbol">as</a> <a id="1907" class="Module">Duality</a> <a id="1915" class="Keyword">using</a> <a id="1921" class="Symbol">(</a><a id="1922" href="Categories.Diagram.Duality.html#4074" class="Function">coLimit⇒Colimit</a><a id="1937" class="Symbol">;</a> <a id="1939" href="Categories.Diagram.Duality.html#4445" class="Function">Colimit⇒coLimit</a><a id="1954" class="Symbol">)</a>
 
 <a id="1957" class="Keyword">import</a> <a id="1964" href="Categories.Morphism.Reasoning.html" class="Module">Categories.Morphism.Reasoning</a> <a id="1994" class="Symbol">as</a> <a id="1997" class="Module">MR</a> <a id="2000" class="Keyword">using</a> <a id="2006" class="Symbol">(</a><a id="2007" href="Categories.Morphism.Reasoning.Core.html#3412" class="Function">pushʳ</a><a id="2012" class="Symbol">;</a> <a id="2014" href="Categories.Morphism.Reasoning.Core.html#3113" class="Function">pullˡ</a><a id="2019" class="Symbol">;</a> <a id="2021" href="Categories.Morphism.Reasoning.Core.html#3550" class="Function">pushˡ</a><a id="2026" class="Symbol">;</a> <a id="2028" href="Categories.Morphism.Reasoning.Core.html#3851" class="Function">elimʳ</a><a id="2033" class="Symbol">;</a> <a id="2035" href="Categories.Morphism.Reasoning.Core.html#8324" class="Function">center</a><a id="2041" class="Symbol">;</a> <a id="2043" href="Categories.Morphism.Reasoning.Core.html#8456" class="Function">center⁻¹</a><a id="2051" class="Symbol">;</a>
   <a id="2055" href="Categories.Morphism.Reasoning.Core.html#4013" class="Function">elimˡ</a><a id="2060" class="Symbol">;</a> <a id="2062" href="Categories.Morphism.Reasoning.Core.html#7916" class="Function">cancelˡ</a><a id="2069" class="Symbol">;</a> <a id="2071" href="Categories.Morphism.Reasoning.Core.html#2979" class="Function">pullʳ</a><a id="2076" class="Symbol">;</a> <a id="2078" href="Categories.Morphism.Reasoning.Core.html#7730" class="Function">cancelʳ</a><a id="2085" class="Symbol">;</a> <a id="2087" href="Categories.Morphism.Reasoning.Core.html#1309" class="Function">id-comm-sym</a><a id="2098" class="Symbol">)</a>
@@ -168,7 +168,7 @@
     <a id="8633" class="Keyword">module</a> <a id="8640" href="Categories.Adjoint.Properties.html#8640" class="Module">F</a> <a id="8642" class="Symbol">=</a> <a id="8644" href="Categories.Functor.Core.html#248" class="Module">Functor</a> <a id="8652" href="Categories.Adjoint.Properties.html#8596" class="Bound">F</a>
 
   <a id="8657" href="Categories.Adjoint.Properties.html#8657" class="Function">lapc</a> <a id="8662" class="Symbol">:</a> <a id="8664" href="Categories.Diagram.Colimit.html#961" class="Record">Colimit</a> <a id="8672" href="Categories.Adjoint.Properties.html#8596" class="Bound">F</a> <a id="8674" class="Symbol">→</a> <a id="8676" href="Categories.Diagram.Colimit.html#961" class="Record">Colimit</a> <a id="8684" class="Symbol">(</a><a id="8685" href="Categories.Adjoint.Properties.html#8546" class="Bound">L</a> <a id="8687" href="Categories.Functor.html#747" class="Function Operator">∘F</a> <a id="8690" href="Categories.Adjoint.Properties.html#8596" class="Bound">F</a><a id="8691" class="Symbol">)</a>
-  <a id="8695" href="Categories.Adjoint.Properties.html#8657" class="Function">lapc</a> <a id="8700" href="Categories.Adjoint.Properties.html#8700" class="Bound">col</a> <a id="8704" class="Symbol">=</a> <a id="8706" href="Categories.Diagram.Duality.html#4047" class="Function">Duality.coLimit⇒Colimit</a> <a id="8730" href="Categories.Adjoint.Properties.html#8560" class="Bound">D</a> <a id="8732" class="Symbol">(</a><a id="8733" href="Categories.Adjoint.RAPL.html#835" class="Function">rapl</a> <a id="8738" class="Symbol">(</a><a id="8739" href="Categories.Adjoint.html#3885" class="Function">Adjoint.op</a> <a id="8750" href="Categories.Adjoint.Properties.html#8582" class="Bound">L⊣R</a><a id="8753" class="Symbol">)</a> <a id="8755" href="Categories.Functor.Core.html#816" class="Function">F.op</a> <a id="8760" class="Symbol">(</a><a id="8761" href="Categories.Diagram.Duality.html#4418" class="Function">Duality.Colimit⇒coLimit</a> <a id="8785" href="Categories.Adjoint.Properties.html#8558" class="Bound">C</a> <a id="8787" href="Categories.Adjoint.Properties.html#8700" class="Bound">col</a><a id="8790" class="Symbol">))</a>
+  <a id="8695" href="Categories.Adjoint.Properties.html#8657" class="Function">lapc</a> <a id="8700" href="Categories.Adjoint.Properties.html#8700" class="Bound">col</a> <a id="8704" class="Symbol">=</a> <a id="8706" href="Categories.Diagram.Duality.html#4074" class="Function">Duality.coLimit⇒Colimit</a> <a id="8730" href="Categories.Adjoint.Properties.html#8560" class="Bound">D</a> <a id="8732" class="Symbol">(</a><a id="8733" href="Categories.Adjoint.RAPL.html#835" class="Function">rapl</a> <a id="8738" class="Symbol">(</a><a id="8739" href="Categories.Adjoint.html#3885" class="Function">Adjoint.op</a> <a id="8750" href="Categories.Adjoint.Properties.html#8582" class="Bound">L⊣R</a><a id="8753" class="Symbol">)</a> <a id="8755" href="Categories.Functor.Core.html#816" class="Function">F.op</a> <a id="8760" class="Symbol">(</a><a id="8761" href="Categories.Diagram.Duality.html#4445" class="Function">Duality.Colimit⇒coLimit</a> <a id="8785" href="Categories.Adjoint.Properties.html#8558" class="Bound">C</a> <a id="8787" href="Categories.Adjoint.Properties.html#8700" class="Bound">col</a><a id="8790" class="Symbol">))</a>
 
 <a id="8794" class="Comment">-- adjoint functors induce monads and comonads</a>
 <a id="8841" class="Keyword">module</a> <a id="8848" href="Categories.Adjoint.Properties.html#8848" class="Module">_</a> <a id="8850" class="Symbol">{</a><a id="8851" href="Categories.Adjoint.Properties.html#8851" class="Bound">L</a> <a id="8853" class="Symbol">:</a> <a id="8855" href="Categories.Functor.Core.html#248" class="Record">Functor</a> <a id="8863" href="Categories.Adjoint.Properties.html#2142" class="Generalizable">C</a> <a id="8865" href="Categories.Adjoint.Properties.html#2144" class="Generalizable">D</a><a id="8866" class="Symbol">}</a> <a id="8868" class="Symbol">{</a><a id="8869" href="Categories.Adjoint.Properties.html#8869" class="Bound">R</a> <a id="8871" class="Symbol">:</a> <a id="8873" href="Categories.Functor.Core.html#248" class="Record">Functor</a> <a id="8881" href="Categories.Adjoint.Properties.html#2144" class="Generalizable">D</a> <a id="8883" href="Categories.Adjoint.Properties.html#2142" class="Generalizable">C</a><a id="8884" class="Symbol">}</a> <a id="8886" class="Symbol">(</a><a id="8887" href="Categories.Adjoint.Properties.html#8887" class="Bound">L⊣R</a> <a id="8891" class="Symbol">:</a> <a id="8893" href="Categories.Adjoint.Properties.html#8851" class="Bound">L</a> <a id="8895" href="Categories.Adjoint.html#7818" class="Function Operator">⊣</a> <a id="8897" href="Categories.Adjoint.Properties.html#8869" class="Bound">R</a><a id="8898" class="Symbol">)</a> <a id="8900" class="Keyword">where</a>

Categories.Category.Cocomplete.Finitely.Properties.html

@@ -21,7 +21,7 @@
 <a id="656" class="Keyword">open</a> <a id="661" class="Keyword">import</a> <a id="668" href="Categories.Functor.html" class="Module">Categories.Functor</a>
 
 <a id="finiteColimit"></a><a id="688" href="Categories.Category.Cocomplete.Finitely.Properties.html#688" class="Function">finiteColimit</a> <a id="702" class="Symbol">:</a> <a id="704" class="Symbol">(</a><a id="705" href="Categories.Category.Cocomplete.Finitely.Properties.html#705" class="Bound">shape</a> <a id="711" class="Symbol">:</a> <a id="713" href="Categories.Category.Finite.Fin.html#2800" class="Record">FinCatShape</a><a id="724" class="Symbol">)</a> <a id="726" class="Symbol">(</a><a id="727" href="Categories.Category.Cocomplete.Finitely.Properties.html#727" class="Bound">F</a> <a id="729" class="Symbol">:</a> <a id="731" href="Categories.Functor.Core.html#248" class="Record">Functor</a> <a id="739" class="Symbol">(</a><a id="740" href="Categories.Category.Finite.Fin.html#4291" class="Function">FinCategory</a> <a id="752" href="Categories.Category.Cocomplete.Finitely.Properties.html#705" class="Bound">shape</a><a id="757" class="Symbol">)</a> <a id="759" href="Categories.Category.Cocomplete.Finitely.Properties.html#189" class="Bound">C</a><a id="760" class="Symbol">)</a> <a id="762" class="Symbol">→</a> <a id="764" href="Categories.Diagram.Colimit.html#961" class="Record">Colimit</a> <a id="772" href="Categories.Category.Cocomplete.Finitely.Properties.html#727" class="Bound">F</a>
-<a id="774" href="Categories.Category.Cocomplete.Finitely.Properties.html#688" class="Function">finiteColimit</a> <a id="788" href="Categories.Category.Cocomplete.Finitely.Properties.html#788" class="Bound">shape</a> <a id="794" href="Categories.Category.Cocomplete.Finitely.Properties.html#794" class="Bound">F</a> <a id="796" class="Symbol">=</a> <a id="798" href="Categories.Diagram.Duality.html#4047" class="Function">coLimit⇒Colimit</a> <a id="814" class="Symbol">(</a><a id="815" href="Categories.Category.Complete.Finitely.Properties.html#7916" class="Function">finiteLimit</a> <a id="827" href="Categories.Category.Finite.Fin.html#2988" class="Function">shape.op</a> <a id="836" href="Categories.Functor.Core.html#816" class="Function">F.op</a><a id="840" class="Symbol">)</a>
+<a id="774" href="Categories.Category.Cocomplete.Finitely.Properties.html#688" class="Function">finiteColimit</a> <a id="788" href="Categories.Category.Cocomplete.Finitely.Properties.html#788" class="Bound">shape</a> <a id="794" href="Categories.Category.Cocomplete.Finitely.Properties.html#794" class="Bound">F</a> <a id="796" class="Symbol">=</a> <a id="798" href="Categories.Diagram.Duality.html#4074" class="Function">coLimit⇒Colimit</a> <a id="814" class="Symbol">(</a><a id="815" href="Categories.Category.Complete.Finitely.Properties.html#7916" class="Function">finiteLimit</a> <a id="827" href="Categories.Category.Finite.Fin.html#2988" class="Function">shape.op</a> <a id="836" href="Categories.Functor.Core.html#816" class="Function">F.op</a><a id="840" class="Symbol">)</a>
   <a id="844" class="Keyword">where</a> <a id="850" class="Keyword">module</a> <a id="857" href="Categories.Category.Cocomplete.Finitely.Properties.html#857" class="Module">shape</a> <a id="863" class="Symbol">=</a> <a id="865" href="Categories.Category.Finite.Fin.html#2800" class="Module">FinCatShape</a> <a id="877" href="Categories.Category.Cocomplete.Finitely.Properties.html#788" class="Bound">shape</a>
         <a id="891" class="Keyword">module</a> <a id="898" href="Categories.Category.Cocomplete.Finitely.Properties.html#898" class="Module">F</a> <a id="900" class="Symbol">=</a> <a id="902" href="Categories.Functor.Core.html#248" class="Module">Functor</a> <a id="910" href="Categories.Category.Cocomplete.Finitely.Properties.html#794" class="Bound">F</a>
 </pre></body></html>