minor

agda/src/Category/Construction/PreElgotMonads.lagda.md

@@ -12,7 +12,7 @@ open import Categories.Category.Core
 ```
 -->
 
-# The (Functor-) Category of Pre-Elgot Monads.
+# The (Functor-)Category of Pre-Elgot Monads.
 
 ```agda
 module Category.Construction.PreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
@@ -25,7 +25,7 @@ open M C
 open MR C
 ```
 
-First we define morphisms between pre-Elgot monads:
+First we look at morphisms between pre-Elgot monads:
 
 ```agda
 module _ (P S : PreElgotMonad) where

agda/src/Category/Construction/StrongPreElgotMonads.lagda.md

@@ -14,7 +14,7 @@ open import Data.Product using (_,_)
 ```
 -->
 
-# The (Functor) Category of Strong Pre-Elgot Monads.
+# The (Functor-)Category of Strong Pre-Elgot Monads.
 
 ```agda
 module Category.Construction.StrongPreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where

agda/src/Monad/Instance/K/EquationalLifting.lagda.md

@@ -12,7 +12,7 @@ open import Categories.Morphism.Properties
 ```
 -->
 
-# K is an equational lifting monad
+# K is an Equational Lifting Monad
 
 ```agda
 module Monad.Instance.K.EquationalLifting {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where