Deploying to gh-pages from @ 21da184 🚀

Author: JacquesCarette

Categories.Adjoint.AFT.html

@@ -79,4 +79,5 @@
   <a id="1988" class="Symbol">}</a>
  <a id="1991" class="Symbol">;</a> <a id="1993" href="Categories.Adjoint.html#1669" class="Field">zig</a> <a id="1997" class="Symbol">=</a> <a id="1999" class="Symbol">λ</a> <a id="2001" class="Symbol">{</a><a id="2002" href="Categories.Adjoint.Construction.CoEilenbergMoore.html#2002" class="Bound">A</a><a id="2003" class="Symbol">}</a> <a id="2005" class="Symbol">→</a> <a id="2007" href="Categories.Category.Construction.CoEilenbergMoore.html#607" class="Field">Comodule.identity</a> <a id="2025" href="Categories.Adjoint.Construction.CoEilenbergMoore.html#2002" class="Bound">A</a>
  <a id="2028" class="Symbol">;</a> <a id="2030" href="Categories.Adjoint.html#1742" class="Field">zag</a> <a id="2034" class="Symbol">=</a> <a id="2036" class="Symbol">λ</a> <a id="2038" class="Symbol">{</a><a id="2039" href="Categories.Adjoint.Construction.CoEilenbergMoore.html#2039" class="Bound">B</a><a id="2040" class="Symbol">}</a> <a id="2042" class="Symbol">→</a> <a id="2044" href="Categories.Comonad.html#911" class="Field">Comonad.identityˡ</a> <a id="2062" href="Categories.Adjoint.Construction.CoEilenbergMoore.html#259" class="Bound">M</a>
- <a id="2065" class="Symbol">}</a></pre></body></html>
+ <a id="2065" class="Symbol">}</a>
+</pre></body></html>

Categories.Adjoint.Alternatives.html

@@ -18,7 +18,7 @@
 <a id="603" class="Keyword">open</a> <a id="608" class="Keyword">import</a> <a id="615" href="Categories.Category.Instance.Groupoids.html" class="Module">Categories.Category.Instance.Groupoids</a> <a id="654" class="Keyword">using</a> <a id="660" class="Symbol">(</a><a id="661" href="Categories.Category.Instance.Groupoids.html#1068" class="Function">Groupoids</a><a id="670" class="Symbol">)</a>
 <a id="672" class="Keyword">open</a> <a id="677" class="Keyword">import</a> <a id="684" href="Categories.Category.Instance.Setoids.html" class="Module">Categories.Category.Instance.Setoids</a> <a id="721" class="Keyword">using</a> <a id="727" class="Symbol">(</a><a id="728" href="Categories.Category.Instance.Setoids.html#555" class="Function">Setoids</a><a id="735" class="Symbol">)</a>
 <a id="737" class="Keyword">open</a> <a id="742" class="Keyword">import</a> <a id="749" href="Categories.Functor.html" class="Module">Categories.Functor</a> <a id="768" class="Keyword">using</a> <a id="774" class="Symbol">(</a><a id="775" href="Categories.Functor.Core.html#248" class="Record">Functor</a><a id="782" class="Symbol">;</a> <a id="784" href="Categories.Functor.html#747" class="Function Operator">_∘F_</a><a id="788" class="Symbol">)</a> <a id="790" class="Keyword">renaming</a> <a id="799" class="Symbol">(</a><a id="800" href="Categories.Functor.html#349" class="Function">id</a> <a id="803" class="Symbol">to</a> <a id="806" class="Function">idF</a><a id="809" class="Symbol">)</a>
-<a id="811" class="Keyword">open</a> <a id="816" class="Keyword">import</a> <a id="823" href="Categories.Functor.Instance.0-Truncation.html" class="Module">Categories.Functor.Instance.0-Truncation</a> <a id="864" class="Keyword">using</a> <a id="870" class="Symbol">(</a><a id="871" href="Categories.Functor.Instance.0-Truncation.html#788" class="Function">Trunc</a><a id="876" class="Symbol">)</a>
+<a id="811" class="Keyword">open</a> <a id="816" class="Keyword">import</a> <a id="823" href="Categories.Functor.Instance.0-Truncation.html" class="Module">Categories.Functor.Instance.0-Truncation</a> <a id="864" class="Keyword">using</a> <a id="870" class="Symbol">(</a><a id="871" href="Categories.Functor.Instance.0-Truncation.html#787" class="Function">Trunc</a><a id="876" class="Symbol">)</a>
 <a id="878" class="Keyword">open</a> <a id="883" class="Keyword">import</a> <a id="890" href="Categories.NaturalTransformation.html" class="Module">Categories.NaturalTransformation</a> <a id="923" class="Keyword">using</a> <a id="929" class="Symbol">(</a><a id="930" href="Categories.NaturalTransformation.Core.html#466" class="Record">NaturalTransformation</a><a id="951" class="Symbol">;</a> <a id="953" href="Categories.NaturalTransformation.Core.html#1750" class="Function">ntHelper</a><a id="961" class="Symbol">)</a>
 <a id="963" class="Keyword">open</a> <a id="968" class="Keyword">import</a> <a id="975" href="Categories.NaturalTransformation.NaturalIsomorphism.html" class="Module">Categories.NaturalTransformation.NaturalIsomorphism</a> <a id="1027" class="Keyword">using</a> <a id="1033" class="Symbol">(</a><a id="1034" href="Categories.NaturalTransformation.NaturalIsomorphism.html#4754" class="Function">refl</a><a id="1038" class="Symbol">)</a>
 
@@ -42,7 +42,7 @@
 
 <a id="1547" class="Comment">-- Trunc is left-adjoint to the inclusion functor from Setoids to Groupoids</a>
 
-<a id="TruncAdj"></a><a id="1624" href="Categories.Adjoint.Instance.0-Truncation.html#1624" class="Function">TruncAdj</a> <a id="1633" class="Symbol">:</a> <a id="1635" class="Symbol">∀</a> <a id="1637" class="Symbol">{</a><a id="1638" href="Categories.Adjoint.Instance.0-Truncation.html#1638" class="Bound">o</a> <a id="1640" href="Categories.Adjoint.Instance.0-Truncation.html#1640" class="Bound">ℓ</a> <a id="1642" href="Categories.Adjoint.Instance.0-Truncation.html#1642" class="Bound">e</a><a id="1643" class="Symbol">}</a> <a id="1645" class="Symbol">→</a> <a id="1647" href="Categories.Functor.Instance.0-Truncation.html#788" class="Function">Trunc</a> <a id="1653" href="Categories.Adjoint.html#7818" class="Function Operator">⊣</a> <a id="1655" href="Categories.Adjoint.Instance.0-Truncation.html#1093" class="Function">Inclusion</a> <a id="1665" class="Symbol">{</a><a id="1666" href="Categories.Adjoint.Instance.0-Truncation.html#1638" class="Bound">o</a><a id="1667" class="Symbol">}</a> <a id="1669" class="Symbol">{</a><a id="1670" href="Categories.Adjoint.Instance.0-Truncation.html#1640" class="Bound">ℓ</a><a id="1671" class="Symbol">}</a> <a id="1673" href="Categories.Adjoint.Instance.0-Truncation.html#1642" class="Bound">e</a>
+<a id="TruncAdj"></a><a id="1624" href="Categories.Adjoint.Instance.0-Truncation.html#1624" class="Function">TruncAdj</a> <a id="1633" class="Symbol">:</a> <a id="1635" class="Symbol">∀</a> <a id="1637" class="Symbol">{</a><a id="1638" href="Categories.Adjoint.Instance.0-Truncation.html#1638" class="Bound">o</a> <a id="1640" href="Categories.Adjoint.Instance.0-Truncation.html#1640" class="Bound">ℓ</a> <a id="1642" href="Categories.Adjoint.Instance.0-Truncation.html#1642" class="Bound">e</a><a id="1643" class="Symbol">}</a> <a id="1645" class="Symbol">→</a> <a id="1647" href="Categories.Functor.Instance.0-Truncation.html#787" class="Function">Trunc</a> <a id="1653" href="Categories.Adjoint.html#7818" class="Function Operator">⊣</a> <a id="1655" href="Categories.Adjoint.Instance.0-Truncation.html#1093" class="Function">Inclusion</a> <a id="1665" class="Symbol">{</a><a id="1666" href="Categories.Adjoint.Instance.0-Truncation.html#1638" class="Bound">o</a><a id="1667" class="Symbol">}</a> <a id="1669" class="Symbol">{</a><a id="1670" href="Categories.Adjoint.Instance.0-Truncation.html#1640" class="Bound">ℓ</a><a id="1671" class="Symbol">}</a> <a id="1673" href="Categories.Adjoint.Instance.0-Truncation.html#1642" class="Bound">e</a>
 <a id="1675" href="Categories.Adjoint.Instance.0-Truncation.html#1624" class="Function">TruncAdj</a> <a id="1684" class="Symbol">{</a><a id="1685" href="Categories.Adjoint.Instance.0-Truncation.html#1685" class="Bound">o</a><a id="1686" class="Symbol">}</a> <a id="1688" class="Symbol">{</a><a id="1689" href="Categories.Adjoint.Instance.0-Truncation.html#1689" class="Bound">ℓ</a><a id="1690" class="Symbol">}</a> <a id="1692" class="Symbol">{</a><a id="1693" href="Categories.Adjoint.Instance.0-Truncation.html#1693" class="Bound">e</a><a id="1694" class="Symbol">}</a> <a id="1696" class="Symbol">=</a> <a id="1698" class="Keyword">record</a>
   <a id="1707" class="Symbol">{</a> <a id="1709" href="Categories.Adjoint.html#1473" class="Field">unit</a>   <a id="1716" class="Symbol">=</a> <a id="1718" href="Categories.Adjoint.Instance.0-Truncation.html#1873" class="Function">unit</a>
   <a id="1725" class="Symbol">;</a> <a id="1727" href="Categories.Adjoint.html#1521" class="Field">counit</a> <a id="1734" class="Symbol">=</a> <a id="1736" href="Categories.Adjoint.Instance.0-Truncation.html#2085" class="Function">counit</a>
@@ -53,13 +53,13 @@
     <a id="1823" class="Keyword">open</a> <a id="1828" href="Function.Bundles.html#2043" class="Module">Func</a>
     <a id="1837" class="Keyword">open</a> <a id="1842" href="Categories.Category.Groupoid.html#807" class="Module">Groupoid</a> <a id="1851" class="Keyword">using</a> <a id="1857" class="Symbol">(</a><a id="1858" href="Categories.Category.Groupoid.html#874" class="Field">category</a><a id="1866" class="Symbol">)</a>
 
-    <a id="1873" href="Categories.Adjoint.Instance.0-Truncation.html#1873" class="Function">unit</a> <a id="1878" class="Symbol">:</a> <a id="1880" href="Categories.NaturalTransformation.Core.html#466" class="Record">NaturalTransformation</a> <a id="1902" href="Categories.Adjoint.Instance.0-Truncation.html#806" class="Function">idF</a> <a id="1906" class="Symbol">(</a><a id="1907" href="Categories.Adjoint.Instance.0-Truncation.html#1093" class="Function">Inclusion</a> <a id="1917" href="Categories.Adjoint.Instance.0-Truncation.html#1693" class="Bound">e</a> <a id="1919" href="Categories.Functor.html#747" class="Function Operator">∘F</a> <a id="1922" href="Categories.Functor.Instance.0-Truncation.html#788" class="Function">Trunc</a><a id="1927" class="Symbol">)</a>
+    <a id="1873" href="Categories.Adjoint.Instance.0-Truncation.html#1873" class="Function">unit</a> <a id="1878" class="Symbol">:</a> <a id="1880" href="Categories.NaturalTransformation.Core.html#466" class="Record">NaturalTransformation</a> <a id="1902" href="Categories.Adjoint.Instance.0-Truncation.html#806" class="Function">idF</a> <a id="1906" class="Symbol">(</a><a id="1907" href="Categories.Adjoint.Instance.0-Truncation.html#1093" class="Function">Inclusion</a> <a id="1917" href="Categories.Adjoint.Instance.0-Truncation.html#1693" class="Bound">e</a> <a id="1919" href="Categories.Functor.html#747" class="Function Operator">∘F</a> <a id="1922" href="Categories.Functor.Instance.0-Truncation.html#787" class="Function">Trunc</a><a id="1927" class="Symbol">)</a>
     <a id="1933" href="Categories.Adjoint.Instance.0-Truncation.html#1873" class="Function">unit</a> <a id="1938" class="Symbol">=</a> <a id="1940" class="Keyword">record</a>
       <a id="1953" class="Symbol">{</a> <a id="1955" href="Categories.NaturalTransformation.Core.html#783" class="Field">η</a>           <a id="1967" class="Symbol">=</a> <a id="1969" class="Symbol">λ</a> <a id="1971" href="Categories.Adjoint.Instance.0-Truncation.html#1971" class="Bound">_</a> <a id="1973" class="Symbol">→</a> <a id="1975" class="Keyword">record</a> <a id="1982" class="Symbol">{</a> <a id="1984" href="Categories.Functor.Core.html#432" class="Field">F₀</a> <a id="1987" class="Symbol">=</a> <a id="1989" href="Categories.Adjoint.Instance.0-Truncation.html#241" class="Function">id→</a> <a id="1993" class="Symbol">;</a> <a id="1995" href="Categories.Functor.Core.html#455" class="Field">F₁</a> <a id="1998" class="Symbol">=</a> <a id="2000" href="Categories.Adjoint.Instance.0-Truncation.html#241" class="Function">id→</a> <a id="2004" class="Symbol">}</a>
       <a id="2012" class="Symbol">;</a> <a id="2014" href="Categories.NaturalTransformation.Core.html#827" class="Field">commute</a>     <a id="2026" class="Symbol">=</a> <a id="2028" class="Symbol">λ</a> <a id="2030" href="Categories.Adjoint.Instance.0-Truncation.html#2030" class="Bound">_</a> <a id="2032" class="Symbol">→</a> <a id="2034" href="Categories.NaturalTransformation.NaturalIsomorphism.html#4754" class="Function">refl</a>
       <a id="2045" class="Symbol">;</a> <a id="2047" href="Categories.NaturalTransformation.Core.html#1043" class="Field">sym-commute</a> <a id="2059" class="Symbol">=</a> <a id="2061" class="Symbol">λ</a> <a id="2063" href="Categories.Adjoint.Instance.0-Truncation.html#2063" class="Bound">_</a> <a id="2065" class="Symbol">→</a> <a id="2067" href="Categories.NaturalTransformation.NaturalIsomorphism.html#4754" class="Function">refl</a>
       <a id="2078" class="Symbol">}</a>
 
-    <a id="2085" href="Categories.Adjoint.Instance.0-Truncation.html#2085" class="Function">counit</a> <a id="2092" class="Symbol">:</a> <a id="2094" href="Categories.NaturalTransformation.Core.html#466" class="Record">NaturalTransformation</a> <a id="2116" class="Symbol">(</a><a id="2117" href="Categories.Functor.Instance.0-Truncation.html#788" class="Function">Trunc</a> <a id="2123" href="Categories.Functor.html#747" class="Function Operator">∘F</a> <a id="2126" href="Categories.Adjoint.Instance.0-Truncation.html#1093" class="Function">Inclusion</a> <a id="2136" href="Categories.Adjoint.Instance.0-Truncation.html#1693" class="Bound">e</a><a id="2137" class="Symbol">)</a> <a id="2139" href="Categories.Adjoint.Instance.0-Truncation.html#806" class="Function">idF</a>
+    <a id="2085" href="Categories.Adjoint.Instance.0-Truncation.html#2085" class="Function">counit</a> <a id="2092" class="Symbol">:</a> <a id="2094" href="Categories.NaturalTransformation.Core.html#466" class="Record">NaturalTransformation</a> <a id="2116" class="Symbol">(</a><a id="2117" href="Categories.Functor.Instance.0-Truncation.html#787" class="Function">Trunc</a> <a id="2123" href="Categories.Functor.html#747" class="Function Operator">∘F</a> <a id="2126" href="Categories.Adjoint.Instance.0-Truncation.html#1093" class="Function">Inclusion</a> <a id="2136" href="Categories.Adjoint.Instance.0-Truncation.html#1693" class="Bound">e</a><a id="2137" class="Symbol">)</a> <a id="2139" href="Categories.Adjoint.Instance.0-Truncation.html#806" class="Function">idF</a>
     <a id="2147" href="Categories.Adjoint.Instance.0-Truncation.html#2085" class="Function">counit</a> <a id="2154" class="Symbol">=</a> <a id="2156" href="Categories.NaturalTransformation.Core.html#1750" class="Function">ntHelper</a> <a id="2165" class="Keyword">record</a> <a id="2172" class="Symbol">{</a> <a id="2174" href="Categories.NaturalTransformation.Core.html#1637" class="Field">η</a> <a id="2176" class="Symbol">=</a> <a id="2178" href="Function.Construct.Identity.html#2813" class="Function">Id.function</a><a id="2189" class="Symbol">;</a> <a id="2191" href="Categories.NaturalTransformation.Core.html#1681" class="Field">commute</a> <a id="2199" class="Symbol">=</a> <a id="2201" class="Symbol">λ</a> <a id="2203" class="Symbol">{</a><a id="2204" href="Categories.Adjoint.Instance.0-Truncation.html#2204" class="Bound">_</a><a id="2205" class="Symbol">}</a> <a id="2207" class="Symbol">{</a><a id="2208" href="Categories.Adjoint.Instance.0-Truncation.html#2208" class="Bound">Y</a><a id="2209" class="Symbol">}</a> <a id="2211" href="Categories.Adjoint.Instance.0-Truncation.html#2211" class="Bound">_</a> <a id="2213" class="Symbol">→</a> <a id="2215" href="Relation.Binary.Structures.html#1596" class="Function">Setoid.refl</a> <a id="2227" href="Categories.Adjoint.Instance.0-Truncation.html#2208" class="Bound">Y</a> <a id="2229" class="Symbol">}</a>
 </pre></body></html>