Deploying to gh-pages from @ 5331251 🚀

Author: JacquesCarette

Categories.Adjoint.AFT.html

@@ -199,5 +199,5 @@
           <a id="5979" class="Symbol">}</a>
 
     <a id="5986" href="Categories.Adjoint.AFT.html#5986" class="Function">solutionSet⇒adjoint</a> <a id="6006" class="Symbol">:</a> <a id="6008" href="Agda.Builtin.Sigma.html#165" class="Record">Σ</a> <a id="6010" class="Symbol">(</a><a id="6011" href="Categories.Functor.Core.html#248" class="Record">Functor</a> <a id="6019" href="Categories.Adjoint.AFT.html#943" class="Bound">D</a> <a id="6021" href="Categories.Adjoint.AFT.html#941" class="Bound">C</a><a id="6022" class="Symbol">)</a> <a id="6024" class="Symbol">(λ</a> <a id="6027" href="Categories.Adjoint.AFT.html#6027" class="Bound">L</a> <a id="6029" class="Symbol">→</a> <a id="6031" href="Categories.Adjoint.AFT.html#6027" class="Bound">L</a> <a id="6033" href="Categories.Adjoint.html#7818" class="Function Operator">⊣</a> <a id="6035" href="Categories.Adjoint.AFT.html#929" class="Bound">R</a><a id="6036" class="Symbol">)</a>
-    <a id="6042" href="Categories.Adjoint.AFT.html#5986" class="Function">solutionSet⇒adjoint</a> <a id="6062" class="Symbol">=</a> <a id="6064" href="Categories.Adjoint.Properties.html#11580" class="Function">universalMophisms⇒adjoint</a> <a id="6090" href="Categories.Adjoint.AFT.html#5780" class="Function">solutionSet′⇒universalMorphism</a>
+    <a id="6042" href="Categories.Adjoint.AFT.html#5986" class="Function">solutionSet⇒adjoint</a> <a id="6062" class="Symbol">=</a> <a id="6064" href="Categories.Adjoint.Properties.html#14071" class="Function">universalMophisms⇒adjoint</a> <a id="6090" href="Categories.Adjoint.AFT.html#5780" class="Function">solutionSet′⇒universalMorphism</a>
 </pre></body></html>

Categories.Adjoint.Equivalence.Properties.html

@@ -46,7 +46,7 @@
   <a id="1643" class="Keyword">module</a> <a id="adjoint"></a><a id="1650" href="Categories.Adjoint.Monadic.Crude.html#1650" class="Module">adjoint</a> <a id="1658" class="Symbol">=</a> <a id="1660" href="Categories.Adjoint.html#1260" class="Module">Adjoint</a> <a id="1668" href="Categories.Adjoint.Monadic.Crude.html#476" class="Bound">adjoint</a>
 
   <a id="T"></a><a id="1679" href="Categories.Adjoint.Monadic.Crude.html#1679" class="Function">T</a> <a id="1681" class="Symbol">:</a> <a id="1683" href="Categories.Monad.html#454" class="Record">Monad</a> <a id="1689" href="Categories.Adjoint.Monadic.Crude.html#355" class="Bound">𝒞</a>
-  <a id="1693" href="Categories.Adjoint.Monadic.Crude.html#1679" class="Function">T</a> <a id="1695" class="Symbol">=</a> <a id="1697" href="Categories.Adjoint.Properties.html#9436" class="Function">adjoint⇒monad</a> <a id="1711" href="Categories.Adjoint.Monadic.Crude.html#476" class="Bound">adjoint</a>
+  <a id="1693" href="Categories.Adjoint.Monadic.Crude.html#1679" class="Function">T</a> <a id="1695" class="Symbol">=</a> <a id="1697" href="Categories.Adjoint.Properties.html#11927" class="Function">adjoint⇒monad</a> <a id="1711" href="Categories.Adjoint.Monadic.Crude.html#476" class="Bound">adjoint</a>
 
   <a id="𝒞ᵀ"></a><a id="1722" href="Categories.Adjoint.Monadic.Crude.html#1722" class="Function">𝒞ᵀ</a> <a id="1725" class="Symbol">:</a> <a id="1727" href="Categories.Category.Core.html#442" class="Record">Category</a> <a id="1736" class="Symbol">_</a> <a id="1738" class="Symbol">_</a> <a id="1740" class="Symbol">_</a>
   <a id="1744" href="Categories.Adjoint.Monadic.Crude.html#1722" class="Function">𝒞ᵀ</a> <a id="1747" class="Symbol">=</a> <a id="1749" href="Categories.Category.Construction.EilenbergMoore.html#734" class="Function">EilenbergMoore</a> <a id="1764" href="Categories.Adjoint.Monadic.Crude.html#1679" class="Function">T</a>

Categories.Adjoint.Monadic.Crude.html

@@ -36,7 +36,7 @@
   <a id="997" class="Keyword">module</a> <a id="adjoint"></a><a id="1004" href="Categories.Adjoint.Monadic.Properties.html#1004" class="Module">adjoint</a> <a id="1012" class="Symbol">=</a> <a id="1014" href="Categories.Adjoint.html#1260" class="Module">Adjoint</a> <a id="1022" href="Categories.Adjoint.Monadic.Properties.html#342" class="Bound">adjoint</a>
 
   <a id="T"></a><a id="1033" href="Categories.Adjoint.Monadic.Properties.html#1033" class="Function">T</a> <a id="1035" class="Symbol">:</a> <a id="1037" href="Categories.Monad.html#454" class="Record">Monad</a> <a id="1043" href="Categories.Adjoint.Monadic.Properties.html#216" class="Bound">𝒞</a>
-  <a id="1047" href="Categories.Adjoint.Monadic.Properties.html#1033" class="Function">T</a> <a id="1049" class="Symbol">=</a> <a id="1051" href="Categories.Adjoint.Properties.html#9436" class="Function">adjoint⇒monad</a> <a id="1065" href="Categories.Adjoint.Monadic.Properties.html#342" class="Bound">adjoint</a>
+  <a id="1047" href="Categories.Adjoint.Monadic.Properties.html#1033" class="Function">T</a> <a id="1049" class="Symbol">=</a> <a id="1051" href="Categories.Adjoint.Properties.html#11927" class="Function">adjoint⇒monad</a> <a id="1065" href="Categories.Adjoint.Monadic.Properties.html#342" class="Bound">adjoint</a>
 
   <a id="𝒞ᵀ"></a><a id="1076" href="Categories.Adjoint.Monadic.Properties.html#1076" class="Function">𝒞ᵀ</a> <a id="1079" class="Symbol">:</a> <a id="1081" href="Categories.Category.Core.html#442" class="Record">Category</a> <a id="1090" class="Symbol">_</a> <a id="1092" class="Symbol">_</a> <a id="1094" class="Symbol">_</a>
   <a id="1098" href="Categories.Adjoint.Monadic.Properties.html#1076" class="Function">𝒞ᵀ</a> <a id="1101" class="Symbol">=</a> <a id="1103" href="Categories.Category.Construction.EilenbergMoore.html#734" class="Function">EilenbergMoore</a> <a id="1118" href="Categories.Adjoint.Monadic.Properties.html#1033" class="Function">T</a>

Categories.Adjoint.Monadic.Properties.html

@@ -26,7 +26,7 @@
 <a id="669" class="Keyword">record</a> <a id="IsMonadicAdjunction"></a><a id="676" href="Categories.Adjoint.Monadic.html#676" class="Record">IsMonadicAdjunction</a> <a id="696" class="Symbol">{</a><a id="697" href="Categories.Adjoint.Monadic.html#697" class="Bound">L</a> <a id="699" class="Symbol">:</a> <a id="701" href="Categories.Functor.Core.html#248" class="Record">Functor</a> <a id="709" href="Categories.Adjoint.Monadic.html#555" class="Generalizable">𝒞</a> <a id="711" href="Categories.Adjoint.Monadic.html#557" class="Generalizable">𝒟</a><a id="712" class="Symbol">}</a> <a id="714" class="Symbol">{</a><a id="715" href="Categories.Adjoint.Monadic.html#715" class="Bound">R</a> <a id="717" class="Symbol">:</a> <a id="719" href="Categories.Functor.Core.html#248" class="Record">Functor</a> <a id="727" href="Categories.Adjoint.Monadic.html#557" class="Generalizable">𝒟</a> <a id="729" href="Categories.Adjoint.Monadic.html#555" class="Generalizable">𝒞</a><a id="730" class="Symbol">}</a> <a id="732" class="Symbol">(</a><a id="733" href="Categories.Adjoint.Monadic.html#733" class="Bound">adjoint</a> <a id="741" class="Symbol">:</a> <a id="743" href="Categories.Adjoint.Monadic.html#697" class="Bound">L</a> <a id="745" href="Categories.Adjoint.html#7818" class="Function Operator">⊣</a> <a id="747" href="Categories.Adjoint.Monadic.html#715" class="Bound">R</a><a id="748" class="Symbol">)</a> <a id="750" class="Symbol">:</a> <a id="752" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="756" class="Symbol">(</a><a id="757" href="Level.html#602" class="Function">levelOfTerm</a> <a id="769" href="Categories.Adjoint.Monadic.html#709" class="Bound">𝒞</a> <a id="771" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="773" href="Level.html#602" class="Function">levelOfTerm</a> <a id="785" href="Categories.Adjoint.Monadic.html#711" class="Bound">𝒟</a><a id="786" class="Symbol">)</a> <a id="788" class="Keyword">where</a>
   <a id="796" class="Keyword">private</a>
     <a id="IsMonadicAdjunction.T"></a><a id="808" href="Categories.Adjoint.Monadic.html#808" class="Function">T</a> <a id="810" class="Symbol">:</a> <a id="812" href="Categories.Monad.html#454" class="Record">Monad</a> <a id="818" href="Categories.Adjoint.Monadic.html#709" class="Bound">𝒞</a>
-    <a id="824" href="Categories.Adjoint.Monadic.html#808" class="Function">T</a> <a id="826" class="Symbol">=</a> <a id="828" href="Categories.Adjoint.Properties.html#9436" class="Function">adjoint⇒monad</a> <a id="842" href="Categories.Adjoint.Monadic.html#733" class="Bound">adjoint</a>
+    <a id="824" href="Categories.Adjoint.Monadic.html#808" class="Function">T</a> <a id="826" class="Symbol">=</a> <a id="828" href="Categories.Adjoint.Properties.html#11927" class="Function">adjoint⇒monad</a> <a id="842" href="Categories.Adjoint.Monadic.html#733" class="Bound">adjoint</a>
 
   <a id="853" class="Keyword">field</a>
     <a id="IsMonadicAdjunction.Comparison⁻¹"></a><a id="863" href="Categories.Adjoint.Monadic.html#863" class="Field">Comparison⁻¹</a> <a id="876" class="Symbol">:</a> <a id="878" href="Categories.Functor.Core.html#248" class="Record">Functor</a> <a id="886" class="Symbol">(</a><a id="887" href="Categories.Category.Construction.EilenbergMoore.html#734" class="Function">EilenbergMoore</a> <a id="902" href="Categories.Adjoint.Monadic.html#808" class="Function">T</a><a id="903" class="Symbol">)</a> <a id="905" href="Categories.Adjoint.Monadic.html#711" class="Bound">𝒟</a>