From 19141b121b350faf81c56f48e9fc1f0946f4a77d Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Thu, 20 Jun 2024 09:29:49 +0200
Subject: [PATCH 1/3] Add thinning from empty list

---
 src/Thinning.agda | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Thinning.agda b/src/Thinning.agda
index ffed3d7..05440f4 100644
--- a/src/Thinning.agda
+++ b/src/Thinning.agda
@@ -45,3 +45,9 @@ end ∘ end = end
 include α ∘ include β = include (α ∘ β)
 include α ∘ exclude β = exclude (α ∘ β)
 exclude α ∘ β = exclude (α ∘ β)
+
+-- There is always a Thinning from the empty list to any list. Here we exclude
+-- at every step.
+¡ : Thinning A [] xs
+¡ {xs = []} = end
+¡ {xs = x ∷ xs} = exclude ¡
-- 
2.44.1


From a0a743ac717008c242221746418b39b6dc9f0997 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Thu, 20 Jun 2024 09:31:14 +0200
Subject: [PATCH 2/3] Show that it's unique

---
 src/Thinning/Properties.agda | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Thinning/Properties.agda b/src/Thinning/Properties.agda
index a77a20a..6559fc8 100644
--- a/src/Thinning/Properties.agda
+++ b/src/Thinning/Properties.agda
@@ -2,7 +2,7 @@
 
 module Thinning.Properties where
 
-open import Data.List.Base using (List)
+open import Data.List.Base using (List; [])
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
@@ -48,3 +48,8 @@ assoc (exclude θ) (include φ) (include ψ) = cong exclude (assoc θ φ ψ)
 assoc (exclude θ) (include φ) (exclude ψ) = cong exclude (assoc (exclude θ) (include φ) ψ)
 assoc (exclude θ) (exclude φ) (include ψ) = cong exclude (assoc (exclude θ) φ ψ)
 assoc (exclude θ) (exclude φ) (exclude ψ) = cong exclude (assoc (exclude θ) (exclude φ) ψ)
+
+-- ¡ is the only Thinning from []
+¡-unique : (θ : Thinning A [] xs) → ¡ ≡ θ
+¡-unique end = refl
+¡-unique (exclude θ) = cong exclude (¡-unique θ)
-- 
2.44.1


From 19d2e98ef07aa34e4ff954e0d6fd304dcca73db1 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Thu, 20 Jun 2024 10:25:38 +0200
Subject: [PATCH 3/3] Define initial object structure

---
 src/Categories/Category/Instance/Thinnings.agda | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/src/Categories/Category/Instance/Thinnings.agda b/src/Categories/Category/Instance/Thinnings.agda
index e37abeb..fef4546 100644
--- a/src/Categories/Category/Instance/Thinnings.agda
+++ b/src/Categories/Category/Instance/Thinnings.agda
@@ -4,12 +4,19 @@ module Categories.Category.Instance.Thinnings where
 
 open import Categories.Category.Core
 open import Categories.Category.Helper
-open import Data.List.Base using (List)
+open import Categories.Object.Initial
+open import Data.List.Base using (List; [])
+open import Level using (Level)
 open import Relation.Binary.PropositionalEquality
 
 open import Thinning
 open import Thinning.Properties
 
+private
+  variable
+    a : Level
+    A : Set a
+
 Thinnings : ∀ {a} (A : Set a) → Category a a a
 Thinnings A = categoryHelper record
   { Obj = List A
@@ -23,3 +30,9 @@ Thinnings A = categoryHelper record
   ; equiv = isEquivalence
   ; ∘-resp-≈ = cong₂ _∘_
   }
+
+[]-isInitial : IsInitial (Thinnings A) []
+[]-isInitial = record { !-unique = ¡-unique }
+
+initial : Initial (Thinnings A)
+initial = record { ⊥-is-initial = []-isInitial }
-- 
2.44.1