From 0c59dc7dc1d2a205df2aa3857354cfb950d7a5d5 Mon Sep 17 00:00:00 2001
From: Julin S <48789920+ju-sh@users.noreply.github.com>
Date: Thu, 19 Oct 2023 14:43:34 +0530
Subject: [PATCH] Fix typo

Fix another typo.
---
 tex/chSigmaBool.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tex/chSigmaBool.tex b/tex/chSigmaBool.tex
index 52d0212..d2feb37 100644
--- a/tex/chSigmaBool.tex
+++ b/tex/chSigmaBool.tex
@@ -801,7 +801,7 @@ \section{Finite functions}
 co-domain, without mentioning the name of the instance of \C{finType}
 for the domain. One can thus write the term \C{\{ffun 'I_7 -> nat\}}
 but the term \C{\{ffun nat -> nat\}} would raise an error message, and
-their cannot be a registered instance of finite type for \C{nat}.
+there cannot be a registered instance of finite type for \C{nat}.
 
 Other utilities let one apply a finite function as a regular function
 or build a finite function from a regular function.