Triangles #5

Merged
Taneb merged 3 commits from tri into main 2024-06-22 16:14:23 +01:00
2 changed files with 88 additions and 0 deletions

View File

@ -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)

View File

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