diff --git a/src/index.lagda.md b/src/index.lagda.md index aa53dbd..c39b722 100644 --- a/src/index.lagda.md +++ b/src/index.lagda.md @@ -80,9 +80,10 @@ open import Monad.Instance.K.Commutative open import Monad.Instance.K.EquationalLifting ``` -and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is the initial pre-Elgot monad. +and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is the initial (strong) pre-Elgot monad. ```agda open import Monad.PreElgot open import Monad.Instance.K.PreElgot +open import Monad.Instance.K.StrongPreElgot ``` \ No newline at end of file