From fc605de0a6d46c4cf4f9ebb03a846dfe1121f22d Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 22 Jun 2024 17:13:42 +0200
Subject: [PATCH] Add that slices are unique

---
 .../Instance/Thinnings/Properties.agda        | 33 +++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 src/Categories/Category/Instance/Thinnings/Properties.agda

diff --git a/src/Categories/Category/Instance/Thinnings/Properties.agda b/src/Categories/Category/Instance/Thinnings/Properties.agda
new file mode 100644
index 0000000..a31637e
--- /dev/null
+++ b/src/Categories/Category/Instance/Thinnings/Properties.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Category.Instance.Thinnings.Properties where
+
+open import Categories.Category.Instance.Thinnings
+open import Categories.Category.Slice
+open import Data.List.Base
+open import Level
+open import Relation.Binary.PropositionalEquality
+
+open import Thinning.Triangle
+
+private
+  variable
+    a : Level
+    A : Set a
+    zs : List A
+
+module _ where
+
+  open SliceObj
+  open Slice⇒
+
+  -- Morphisms between two objects in a slice category over thinnings are unique!
+  -- We prove this using triangles.
+  Slice⇒-unique : ∀ {θ φ : SliceObj (Thinnings A) zs} (f g : Slice⇒ (Thinnings A) θ φ) → h f ≡ h g
+  Slice⇒-unique {zs = zs} {θ = θ} {φ = φ} (slicearr {h = hf} ▲) (slicearr {h = hg} △) = triangleUnique ▴ ▵
+    where
+      ▴ : Triangle _ (arr φ) hf (arr θ)
+      ▴ = subst (Triangle _ _ _) ▲ (arr φ ⊚ hf)
+
+      ▵ : Triangle _ (arr φ) hg (arr θ)
+      ▵ = subst (Triangle _ _ _) △ (arr φ ⊚ hg)