Merge pull request #503 from jacquescomeaux/truncation-typos

Fix documentation typos for (0,1)-truncation

Author: JacquesCarette

src/Categories/Adjoint/Instance/01-Truncation.agda

@@ -39,7 +39,7 @@ Inclusion {c} {ℓ₁} e = record
     }
   }
 
--- Trunc is left-adjoint to the inclusion functor from Setoids to Groupoids
+-- Trunc is left-adjoint to the inclusion functor from Posets to Categories
 
 TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e
 TruncAdj {o} {ℓ} {e} = record

src/Categories/Functor/Instance/01-Truncation.agda

@@ -2,9 +2,9 @@
 
 module Categories.Functor.Instance.01-Truncation where
 
--- (0,1)-trucation of categories as a functor from Cats to Posets.
+-- (0,1)-truncation of categories as a functor from Cats to Posets.
 --
--- This is the right-adjoint of the inclusion functor from Posets to
+-- This is the left-adjoint of the inclusion functor from Posets to
 -- Cats (see Categories.Functor.Adjoint.Instance.01-Truncation)
 
 open import Level using (_⊔_)