module Cat.Allegory.Reasoning {o β ββ²} (A : Allegory o β ββ²) where
open Allegory A public open Cat.Reasoning (A .Allegory.cat) hiding (module HLevel-instance ; Ob ; Hom ; id ; idl ; idr ; assoc ; _β_) public
Combinators for allegoriesπ
For reasoning about morphisms in allegories, the first thing we need is a convenient syntax for piecing together long arguments by transitivity. The following operators allow us to interweave throwing in an inequality, and rewriting by an equality:
private variable w x y z : Ob f fβ² g gβ² h : Hom x y _β€β¨_β©_ : β (f : Hom x y) β f β€ g β g β€ h β f β€ h _=β¨_β©_ : β (f : Hom x y) β f β‘ g β g β€ h β f β€ h _=Λβ¨_β©_ : β (f : Hom x y) β g β‘ f β g β€ h β f β€ h _β€β : β (f : Hom x y) β f β€ f f β€β¨ p β©β€ q = β€-trans p q f =β¨ p β©= q = subst (_β€ _) (sym p) q f =Λβ¨ p β©=Λ q = subst (_β€ _) p q f β€β = β€-refl infixr 40 _β_ _βΆ_ infixr 2 _=β¨_β©_ _=Λβ¨_β©_ _β€β¨_β©_ infix 3 _β€β
Additionally, we have whiskering operations, derived from the horizontal composition operation by holding one of the operands constant:
_βΆ_ : (f : Hom x y) β g β€ h β f β g β€ f β h _β_ : f β€ g β (h : Hom x y) β f β h β€ g β h f βΆ g = β€-refl β g g β f = g β β€-refl
A few lemmas about the meet operation are also in order. It, unsurprisingly, behaves like the binary operation of a meet-semilattice: We have that is equivalently , and is a commutative, associative idempotent binary operation, which preserves ordering in both of its arguments.
β©-pres-r : g β€ gβ² β f β© g β€ f β© gβ² β©-pres-l : f β€ fβ² β f β© g β€ fβ² β© g β©-distribl : f β (g β© h) β€ (f β g) β© (f β h) β©-distribr : (g β© h) β f β€ (g β f) β© (h β f) β©-assoc : (f β© g) β© h β‘ f β© (g β© h) β©-comm : f β© g β‘ g β© f β©-idempotent : f β© f β‘ f
β©-pres-r w = β©-univ β©-le-l (β€-trans β©-le-r w) β©-pres-l w = β©-univ (β€-trans β©-le-l w) β©-le-r β©-distribl = β©-univ (_ βΆ β©-le-l) (_ βΆ β©-le-r) β©-distribr = β©-univ (β©-le-l β _) (β©-le-r β _) β©-assoc = β€-antisym (β©-univ (β€-trans β©-le-l β©-le-l) (β©-univ (β€-trans β©-le-l β©-le-r) β©-le-r)) (β©-univ (β©-univ β©-le-l (β€-trans β©-le-r β©-le-l)) (β€-trans β©-le-r β©-le-r)) β©-comm = β€-antisym (β©-univ β©-le-r β©-le-l) (β©-univ β©-le-r β©-le-l) β©-idempotent = β€-antisym β©-le-l (β©-univ β€-refl β€-refl)
modularβ² : β {x y z} (f : Hom x y) (g : Hom y z) (h : Hom x z) β (g β f) β© h β€ (g β© (h β f β )) β f modularβ² f g h = (g β f) β© h =Λβ¨ dual _ β©=Λ β ((g β f) β© h) β β β =β¨ ap! (dual-β© A) β©= (β (g β f) β β β© h β ) β =β¨ ap! dual-β β©= β ((f β β g β ) β© h β ) β β β€β¨ dual-β€ (modular (g β ) (f β ) (h β )) β©β€ (f β β (g β β© (f β β β h β ))) β =β¨ dual-β β©= (g β β© (f β β β h β )) β β f β β =β¨ apβ _β_ (dual-β© A) (dual f) β©= (g β β β© (f β β β h β ) β ) β f =β¨ apβ _β_ (apβ _β©_ (dual g) (ap _β (apβ _β_ (dual f) refl) Β·Β· dual-β Β·Β· ap (_β f β ) (dual h))) refl β©= (g β© h β f β ) β f β€β
β -inner : (p : g β gβ² β β‘ h) β (f β g) β (fβ² β gβ²) β β‘ f β h β fβ² β β -inner p = apβ _β_ refl dual-β β sym (assoc _ _ _) β apβ _β_ refl (assoc _ _ _ β apβ _β_ p refl)