From 56b1db15a4bc7652fa3e31aebf017346684086e3 Mon Sep 17 00:00:00 2001
From: Marcus Zibrowius <marcus.zibrowius@cantab.net>
Date: Wed, 4 Sep 2024 11:19:45 +0200
Subject: [PATCH] (small corrections)

---
 development-status.md | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/development-status.md b/development-status.md
index 41db71f..0a90044 100644
--- a/development-status.md
+++ b/development-status.md
@@ -400,13 +400,13 @@ choose
 HasRightInverse
 Surjective
 
-#### Inj 01
+#### Inj 01: concrete function injective
 **Injective**
   
-#### Inj 02: bijective ↔ ∃ both inverses
-**Bijective** **RightInverse** **Leftinverse**
+#### Inj 02: concrete function not injective
+if … then … else
 
-**choose**
+Injective
 
 #### Inj 03: injective → fibres are singletons
 range 
@@ -427,11 +427,15 @@ Injective
 
 #### Inj 05: application of StrictMono → application
 
-#### Inj 06: succ has left inverse, using if … then … else
-**succ**  **if … then … else**  **HasLeftInverse**
+#### Inj 06: succ has left inverse
+**HasLeftInverse**
+
+succ
+
+if … then … else
   
 #### Inj 07a & b: extend from ℕ to ℤ
-**if … then … else**
+if … then … else
 
 #### Inj 08: image of self vs preimage of LeftInverse
 **image**