src/Categories/Category/Instance/Thinnings.agda

@@ -4,19 +4,12 @@ module Categories.Category.Instance.Thinnings where
 
 open import Categories.Category.Core
 open import Categories.Category.Helper
-open import Categories.Object.Initial
-open import Data.List.Base using (List; [])
-open import Level using (Level)
+open import Data.List.Base using (List)
 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
@@ -30,9 +23,3 @@ 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 }

src/Thinning.agda

@@ -45,9 +45,3 @@ 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 ¡

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,8 +48,3 @@ 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 θ)