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] 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 }