From a1046d16e186fe384cba7357b97fcc64ef125c7d Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Thu, 22 Feb 2024 18:04:17 +0100
Subject: [PATCH] minor
---
agda/src/Category/Construction/PreElgotMonads.lagda.md | 4 ++--
agda/src/Category/Construction/StrongPreElgotMonads.lagda.md | 2 +-
agda/src/Monad/Instance/K/EquationalLifting.lagda.md | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/agda/src/Category/Construction/PreElgotMonads.lagda.md b/agda/src/Category/Construction/PreElgotMonads.lagda.md
index 15d6a24..196ed63 100644
--- a/agda/src/Category/Construction/PreElgotMonads.lagda.md
+++ b/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
diff --git a/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md b/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md
index 05f3112..d032fb9 100644
--- a/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md
+++ b/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
diff --git a/agda/src/Monad/Instance/K/EquationalLifting.lagda.md b/agda/src/Monad/Instance/K/EquationalLifting.lagda.md
index 65d2541..2caf14b 100644
--- a/agda/src/Monad/Instance/K/EquationalLifting.lagda.md
+++ b/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