Deploying to gh-pages from @ 2530add 🚀

Author: JacquesCarette

Categories.Adjoint.Instance.01-Truncation.html

@@ -40,7 +40,7 @@
     <a id="1449" class="Symbol">}</a>
   <a id="1453" class="Symbol">}</a>
 
-<a id="1456" class="Comment">-- Trunc is left-adjoint to the inclusion functor from Setoids to Groupoids</a>
+<a id="1456" class="Comment">-- Trunc is left-adjoint to the inclusion functor from Posets to Categories</a>
 
 <a id="TruncAdj"></a><a id="1533" href="Categories.Adjoint.Instance.01-Truncation.html#1533" class="Function">TruncAdj</a> <a id="1542" class="Symbol">:</a> <a id="1544" class="Symbol">∀</a> <a id="1546" class="Symbol">{</a><a id="1547" href="Categories.Adjoint.Instance.01-Truncation.html#1547" class="Bound">o</a> <a id="1549" href="Categories.Adjoint.Instance.01-Truncation.html#1549" class="Bound">ℓ</a> <a id="1551" href="Categories.Adjoint.Instance.01-Truncation.html#1551" class="Bound">e</a><a id="1552" class="Symbol">}</a> <a id="1554" class="Symbol">→</a> <a id="1556" href="Categories.Functor.Instance.01-Truncation.html#947" class="Function">Trunc</a> <a id="1562" href="Categories.Adjoint.html#7818" class="Function Operator">⊣</a> <a id="1564" href="Categories.Adjoint.Instance.01-Truncation.html#1029" class="Function">Inclusion</a> <a id="1574" class="Symbol">{</a><a id="1575" href="Categories.Adjoint.Instance.01-Truncation.html#1547" class="Bound">o</a><a id="1576" class="Symbol">}</a> <a id="1578" class="Symbol">{</a><a id="1579" href="Categories.Adjoint.Instance.01-Truncation.html#1549" class="Bound">ℓ</a><a id="1580" class="Symbol">}</a> <a id="1582" href="Categories.Adjoint.Instance.01-Truncation.html#1551" class="Bound">e</a>
 <a id="1584" href="Categories.Adjoint.Instance.01-Truncation.html#1533" class="Function">TruncAdj</a> <a id="1593" class="Symbol">{</a><a id="1594" href="Categories.Adjoint.Instance.01-Truncation.html#1594" class="Bound">o</a><a id="1595" class="Symbol">}</a> <a id="1597" class="Symbol">{</a><a id="1598" href="Categories.Adjoint.Instance.01-Truncation.html#1598" class="Bound">ℓ</a><a id="1599" class="Symbol">}</a> <a id="1601" class="Symbol">{</a><a id="1602" href="Categories.Adjoint.Instance.01-Truncation.html#1602" class="Bound">e</a><a id="1603" class="Symbol">}</a> <a id="1605" class="Symbol">=</a> <a id="1607" class="Keyword">record</a>

Categories.Functor.Instance.01-Truncation.html

@@ -3,9 +3,9 @@
 
 <a id="37" class="Keyword">module</a> <a id="44" href="Categories.Functor.Instance.01-Truncation.html" class="Module">Categories.Functor.Instance.01-Truncation</a> <a id="86" class="Keyword">where</a>
 
-<a id="93" class="Comment">-- (0,1)-trucation of categories as a functor from Cats to Posets.</a>
-<a id="160" class="Comment">--</a>
-<a id="163" class="Comment">-- This is the right-adjoint of the inclusion functor from Posets to</a>
+<a id="93" class="Comment">-- (0,1)-truncation of categories as a functor from Cats to Posets.</a>
+<a id="161" class="Comment">--</a>
+<a id="164" class="Comment">-- This is the left-adjoint of the inclusion functor from Posets to</a>
 <a id="232" class="Comment">-- Cats (see Categories.Functor.Adjoint.Instance.01-Truncation)</a>
 
 <a id="297" class="Keyword">open</a> <a id="302" class="Keyword">import</a> <a id="309" href="Level.html" class="Module">Level</a> <a id="315" class="Keyword">using</a> <a id="321" class="Symbol">(</a><a id="322" href="Agda.Primitive.html#961" class="Primitive Operator">_⊔_</a><a id="325" class="Symbol">)</a>