{-# 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 ▴)