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 ▴ ▵)