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