From 896dc3d29684bdecd906330a62d250ccbeb18f6a Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Wed, 14 Feb 2024 12:03:47 +0100
Subject: [PATCH] update index

---
 agda/src/index.lagda.md | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/agda/src/index.lagda.md b/agda/src/index.lagda.md
index 519eef8..8aab6ea 100644
--- a/agda/src/index.lagda.md
+++ b/agda/src/index.lagda.md
@@ -57,6 +57,13 @@ Afterwards we also introduce categories of iteration algebras with iteration pre
 open import Category.Construction.ElgotAlgebras
 ```
 
+we can form products and exponentials in a canonical way:
+
+```agda
+open import Category.Construction.ElgotAlgebras.Products
+open import Category.Construction.ElgotAlgebras.Exponentials
+```
+
 Free Elgot algebras are free objects in the category of Elgot algebras, we will be needing a notion of stability for them:
 
 ```agda
@@ -67,7 +74,7 @@ open import Algebra.Elgot.Stable
 In a CCC stability follows directly
 ```agda
 open import Algebra.Elgot.Properties
-``` 
+```
 
 With this in hand we can now define *KX* as a *free Elgot algebra* and proof that under *stability* it is a strong monad.
 
@@ -83,7 +90,7 @@ 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 (strong) pre-Elgot monad.
+and lastly we formalize the notion of *(strong) pre-Elgot monad* and show that **K** is the initial (strong) pre-Elgot monad.
 
 ```agda
 open import Monad.PreElgot