Triangles #5

Merged
Taneb merged 3 commits from tri into main 2024-06-22 16:14:23 +01:00
1 changed files with 33 additions and 0 deletions
Showing only changes of commit fc605de0a6 - Show all commits

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)