open import Cat.Prelude

module Cat.Strict.Reasoning {o β} (C : Precategory o β) (ob-set : is-set β C β) where

open Precategory C


# Reasoning with strict categoriesπ

When working with strict categories, transports of morphisms along paths between objects is (annoyingly) common; this module puts all of the frustration in one place.

We provide shorthand operators for transporting morphisms.

cast-hom : β {x x' y y' : Ob} β x β‘ x' β y β‘ y' β Hom x y β Hom x' y'
cast-hom p q f = transport (Ξ» i β Hom (p i) (q i)) f

cast-cod : β {x y y' : Ob} β y β‘ y' β Hom x y β Hom x y'
cast-cod p f = subst (Ξ» y β Hom _ y) p f

cast-dom : β {x x' y : Ob} β x β‘ x' β Hom x y β Hom x' y
cast-dom p f = subst (Ξ» x β Hom x _) p f


We also characterize transports in identities and composites.

cast-id : β {x x'} β (p : x β‘ x') β cast-hom p p id β‘ id
cast-id p = J (Ξ» x p β cast-hom p p id β‘ id) (transport-refl id) p

cast-id-swap : β {x x'} β (p : x β‘ x') β cast-cod p id β‘ cast-dom (sym p) id
cast-id-swap p = J (Ξ» _ p β cast-cod p id β‘ cast-dom (sym p) id) refl p

cast-β
: β {x x' y z z'} {f : Hom y z} {g : Hom x y}
β (p : x β‘ x') (q : z β‘ z')
β cast-hom p q (f β g) β‘ cast-cod q f β cast-dom p g
cast-β {f = f} {g = g} p q =
Jβ (Ξ» _ _ p q β cast-hom p q (f β g) β‘ cast-cod q f β cast-dom p g)
(transport-refl _ β sym (apβ _β_ (transport-refl _) (transport-refl _)))
p q

cast-cod-β
: β {x y z z'} {f : Hom y z} {g : Hom x y}
β (p : z β‘ z')
β cast-cod p (f β g) β‘ cast-cod p f β g
cast-cod-β {f = f} {g = g} p =
J (Ξ» _ p β cast-cod p (f β g) β‘ cast-cod p f β g)
(transport-refl _ β ap (_β g) (sym (transport-refl _)))
p

cast-dom-β
: β {x x' y z} {f : Hom y z} {g : Hom x y}
β (p : x β‘ x')
β cast-dom p (f β g) β‘ f β cast-dom p g
cast-dom-β {f = f} {g = g} p =
J (Ξ» _ p β cast-dom p (f β g) β‘ f β cast-dom p g)
(transport-refl _ β ap (f β_) (sym (transport-refl _)))
p


We also provide some lemmas for working with right/left identity laws that are off by a cast.

cast-cod-idr : β {x x' y : Ob} β (f : Hom x y) β (p : x' β‘ x)
β f β cast-cod p id β‘ cast-dom (sym p) f
cast-cod-idr {y = y} f p =
J (Ξ» x p β β (f : Hom x y) β f β cast-cod p id β‘ cast-dom (sym p) f)
(Ξ» f β  ap (f β_) (transport-refl _) Β·Β· idr _ Β·Β· sym (transport-refl _))
p f

cast-dom-idl : β {x y y' : Ob} β (f : Hom x y) β (p : y' β‘ y)
β cast-dom p id β f β‘ cast-cod (sym p) f
cast-dom-idl {x = x} f p =
J (Ξ» y p β β (f : Hom x y) β cast-dom p id β f β‘ cast-cod (sym p) f)
(Ξ» f β ap (_β f) (transport-refl _) Β·Β· idl _ Β·Β· sym (transport-refl _))
p f


It doesnβt matter what path you transport along, as is strict.

recast
: β {x x' y y'} {f : Hom x y}
β (p p' : x β‘ x') (q q' : y β‘ y')
β cast-hom p q f β‘ cast-hom p' q' f
recast {x} {x'} {y} {y'} {f} p p' q q' =
transport
(Ξ» i β cast-hom (ob-set x x' p' p i) (ob-set y y' q' q i) f β‘ cast-hom p' q' f)
refl

recast-dom
: β {x x' y} {f : Hom x y}
β (p p' : x β‘ x')
β cast-dom p f β‘ cast-dom p' f
recast-dom {x} {x'} {y'} {f} p p' =
transport (Ξ» i β cast-dom (ob-set x x' p' p i) f β‘ cast-dom p' f) refl

recast-cod
: β {x y y'} {f : Hom x y}
β (p p' : y β‘ y')
β cast-cod p f β‘ cast-cod p' f
recast-cod {x} {y} {y'} {f} p p' =
transport (Ξ» i β cast-cod (ob-set y y' p' p i) f β‘ cast-cod p' f) refl