From d2557b6967143a99df4c414ad48de8f664e06fda Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 22 Jun 2024 16:44:33 +0200
Subject: [PATCH 1/3] Add triangle definitions

---
 src/Thinning/Triangle.agda | 48 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 src/Thinning/Triangle.agda

diff --git a/src/Thinning/Triangle.agda b/src/Thinning/Triangle.agda
new file mode 100644
index 0000000..63bf062
--- /dev/null
+++ b/src/Thinning/Triangle.agda
@@ -0,0 +1,48 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Thinning.Triangle where
+
+open import Level
+open import Data.List.Base
+open import Relation.Binary.PropositionalEquality
+
+open import Thinning
+
+private
+  variable
+    a : Level
+    A : Set a
+    x : A
+    xs ys zs : List A
+    θ φ ψ : Thinning A xs ys
+
+-- Thinning triangles
+------------------------------------------------------------------------
+
+-- These are a sort of inductive view of "φ ∘ θ ≡ ψ" that's much easier to work
+-- with than a more direct definition. This helps a lot when working with slice
+-- categories!
+
+-- I choose the order of arguments to match composition order. The names are by
+-- the second argument, with "occlude" as another word that rhymes. Any aptitude
+-- is purely accidental.
+
+data Triangle (A : Set a) : Thinning A ys zs → Thinning A xs ys → Thinning A xs zs → Set a where
+  end : Triangle A end end end
+  include : Triangle A θ φ ψ → Triangle A (include {x = x} θ) (include φ) (include ψ)
+  occlude : Triangle A θ φ ψ → Triangle A (exclude {x = x} θ) φ           (exclude ψ)
+  exclude : Triangle A θ φ ψ → Triangle A (include {x = x} θ) (exclude φ) (exclude ψ)
+
+-- We can construct a triangle by composition
+_⊚_ : (θ : Thinning A ys zs) (φ : Thinning A xs ys) → Triangle A θ φ (θ ∘ φ)
+end ⊚ end = end
+include θ ⊚ include φ = include (θ ⊚ φ)
+include θ ⊚ exclude φ = exclude (θ ⊚ φ)
+exclude θ ⊚ φ         = occlude (θ ⊚ φ)
+
+-- We can deconstruct a triangle into a proof of equality to the composition
+untriangle : Triangle A θ φ ψ → θ ∘ φ ≡ ψ
+untriangle end = refl
+untriangle (include ▴) = cong include (untriangle ▴)
+untriangle (occlude ▴) = cong exclude (untriangle ▴)
+untriangle (exclude ▴) = cong exclude (untriangle ▴)
-- 
2.44.1


From 3e2ea540300473d310ddae8546494d3216d12bc7 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 22 Jun 2024 16:52:06 +0200
Subject: [PATCH 2/3] Add a uniqueness property

---
 src/Thinning/Triangle.agda | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Thinning/Triangle.agda b/src/Thinning/Triangle.agda
index 63bf062..2942c2c 100644
--- a/src/Thinning/Triangle.agda
+++ b/src/Thinning/Triangle.agda
@@ -14,7 +14,7 @@ private
     A : Set a
     x : A
     xs ys zs : List A
-    θ φ ψ : Thinning A xs ys
+    θ φ φ′ ψ : Thinning A xs ys
 
 -- Thinning triangles
 ------------------------------------------------------------------------
@@ -46,3 +46,10 @@ untriangle end = refl
 untriangle (include ▴) = cong include (untriangle ▴)
 untriangle (occlude ▴) = cong exclude (untriangle ▴)
 untriangle (exclude ▴) = cong exclude (untriangle ▴)
+
+-- If we have two triangles with common edges, the third edge must also be equal
+triangleUnique : Triangle A θ φ ψ → Triangle A θ φ′ ψ → φ ≡ φ′
+triangleUnique end end = refl
+triangleUnique (include ▴) (include ▵) = cong include (triangleUnique ▴ ▵)
+triangleUnique (occlude ▴) (occlude ▵) = triangleUnique ▴ ▵
+triangleUnique (exclude ▴) (exclude ▵) = cong exclude (triangleUnique ▴ ▵)
-- 
2.44.1


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 3/3] 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)
-- 
2.44.1