src/Categories/Category/Instance/Thinnings/Properties.agda

@@ -1,33 +0,0 @@
-{-# 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)

src/Thinning/Triangle.agda

@@ -1,55 +0,0 @@
-{-# 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 ▴)
-
--- 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 ▴ ▵)