open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Reasoning as Cat

module
  Cat.Displayed.Reasoning
    {o' β„“' o'' β„“''}
    {B : Precategory o' β„“'}
    (E : Displayed B o'' β„“'')
  where

Reasoning in displayed categoriesπŸ”—

private
  module E = Displayed E
  module B = Cat B
  _ = Displayed.Hom[_] -- anchor for the reference below

Contrary to the reasoning combinators for precategories, reasoning in a displayed category is much harder. The core of the problem is that the type Displayed.Hom[_] of displayed morphisms is dependent, so all but the most trivial paths over it will similarly be dependent paths. We prefer to work instead with non-dependent paths and substitution, using the from-pathp and to-pathp combinators to adjust to the situation.

A fundamental operator is moving a morphism between displayed depending on a path in the base category, so we provide a shorthand syntax for that here. You can think of this as being an abbreviation for subst because… that’s what it is.

hom[_] : βˆ€ {a b x y} {f g : B.Hom a b} β†’ f ≑ g β†’ E.Hom[ f ] x y β†’ E.Hom[ g ] x y
hom[ p ] f' = subst (Ξ» h β†’ E.Hom[ h ] _ _) p f'

hom[_]⁻ : βˆ€ {a b x y} {f g : B.Hom a b} β†’ g ≑ f β†’ E.Hom[ f ] x y β†’ E.Hom[ g ] x y
hom[ p ]⁻ f' = hom[ sym p ] f'

Since equality in the base is a proposition, we can always adjust the path we’re transporting over to get something more convenient.

reindex
  : βˆ€ {a b x y} {f g : B.Hom a b} (p q : f ≑ g) {f' : E.Hom[ f ] x y}
  β†’ hom[ p ] f' ≑ hom[ q ] f'
reindex p q {f'} = ap (Ξ» e β†’ hom[ e ] f') (B.Hom-set _ _ _ _ p q)

cast[]
  : βˆ€ {a b x y} {f g : B.Hom a b} {f' : E.Hom[ f ] x y} {g' : E.Hom[ g ] x y}
  β†’ {p q : f ≑ g}
  β†’ f' E.≑[ p ] g'
  β†’ f' E.≑[ q ] g'
cast[] {f = f} {g = g} {f' = f'} {g' = g'} {p = p} {q = q} r =
  coe0β†’1 (Ξ» i β†’ f' E.≑[ B.Hom-set _ _ f g p q i ] g') r

Next come the most important lemmas: Moving substitution in and out of composite morphisms. The whisker-r combinator says that substituting on the right of a composition is the same thing as composing first, then adjusting by a path which leaves the β€œleft” composite unchanged.

hom[]-βˆ™
  : βˆ€ {a b x y} {f g h : B.Hom a b} (p : f ≑ g) (q : g ≑ h)
      {f' : E.Hom[ f ] x y}
  β†’ hom[ q ] (hom[ p ] f') ≑ hom[ p βˆ™ q ] f'
hom[]-βˆ™ p q = sym (subst-βˆ™ (Ξ» h β†’ E.Hom[ h ] _ _) _ _ _)

duplicate
  : βˆ€ {a b x y} {f f' g : B.Hom a b} (p : f ≑ g) (q : f' ≑ g) (r : f ≑ f')
      {f' : E.Hom[ f ] x y}
  β†’ hom[ p ] f' ≑ hom[ q ] (hom[ r ] f')
duplicate p q r = reindex _ _ βˆ™ sym (hom[]-βˆ™ r q)

To understand why these whiskering lemmas have such complicated types, recall that the β€œdisplayed composition” operator has type

so if we have some path the composite will have type but the composite has type Hence the need to adjust that composite: we can’t just get rid of the transport 

whisker-r
  : βˆ€ {a b c} {f : B.Hom b c} {g g₁ : B.Hom a b} {a' b' c'}
      {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
  β†’ (p : g ≑ g₁)
  β†’ f' E.∘' hom[ p ] g' ≑ hom[ ap (f B.∘_) p ] (f' E.∘' g')
whisker-r {f = f} {a' = a'} {_} {c'} {f'} {g'} p i =
  comp (Ξ» j β†’ E.Hom[ f B.∘ p (i ∨ j) ] a' c') (βˆ‚ i) Ξ» where
    j (i = i0) β†’ f' E.∘' transport-filler (Ξ» i β†’ E.Hom[ p i ] _ _) g' j
    j (i = i1) β†’ hom[ ap (f B.∘_) p ] (f' E.∘' g')
    j (j = i0) β†’ transport-filler (Ξ» i β†’ E.Hom[ f B.∘ p i ] _ _) (f' E.∘' g') i

whisker-l
  : βˆ€ {a b c} {f f₁ : B.Hom b c} {g : B.Hom a b} {a' b' c'}
      {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
  β†’ (p : f ≑ f₁)
  β†’ hom[ p ] f' E.∘' g' ≑ hom[ ap (B._∘ g) p ] (f' E.∘' g')
whisker-l {g = g} {a'} {_} {c'} {f' = f'} {g' = g'} p i =
  comp (Ξ» j β†’ E.Hom[ p (i ∨ j) B.∘ g ] a' c') (βˆ‚ i) Ξ» where
    j (i = i0) β†’ transport-filler (Ξ» i β†’ E.Hom[ p i ] _ _) f' j E.∘' g'
    j (i = i1) β†’ hom[ ap (B._∘ g) p ] (f' E.∘' g')
    j (j = i0) β†’ transport-filler (Ξ» i β†’ E.Hom[ p i B.∘ g ] _ _) (f' E.∘' g') i

unwhisker-r
  : βˆ€ {a b c} {f : B.Hom b c} {g g₁ : B.Hom a b} {a' b' c'}
      {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
  β†’ (p : f B.∘ g ≑ f B.∘ g₁) (q : g ≑ g₁)
  β†’ hom[ p ] (f' E.∘' g') ≑ f' E.∘' hom[ q ] g'
unwhisker-r p q = reindex _ _ βˆ™ sym (whisker-r _)

unwhisker-l
  : βˆ€ {a b c} {f f₁ : B.Hom b c} {g : B.Hom a b} {a' b' c'}
      {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
  β†’ (p : f B.∘ g ≑ f₁ B.∘ g) (q : f ≑ f₁)
  β†’ hom[ p ] (f' E.∘' g') ≑ hom[ q ] f' E.∘' g'
unwhisker-l p q = reindex _ _ βˆ™ sym (whisker-l _)

The rest of this module is made up of grueling applications of the three lemmas above:

smashr
  : βˆ€ {a b c} {f : B.Hom b c} {g g₁ : B.Hom a b} {h : B.Hom a c} {a' b' c'}
      {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
  β†’ (p : g ≑ g₁) (q : f B.∘ g₁ ≑ h)
  β†’ hom[ q ] (f' E.∘' hom[ p ] g') ≑ hom[ ap (f B.∘_) p βˆ™ q ] (f' E.∘' g')
smashr p q = ap hom[ q ] (whisker-r p) βˆ™ hom[]-βˆ™ _ _

smashl
  : βˆ€ {a b c} {f f₁ : B.Hom b c} {g : B.Hom a b} {h : B.Hom a c} {a' b' c'}
      {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
  β†’ (p : f ≑ f₁) (q : f₁ B.∘ g ≑ h)
  β†’ hom[ q ] (hom[ p ] f' E.∘' g') ≑ hom[ ap (B._∘ g) p βˆ™ q ] (f' E.∘' g')
smashl p q = ap hom[ q ] (whisker-l p) βˆ™ hom[]-βˆ™ _ _

expandl
  : βˆ€ {a b c} {f f₁ : B.Hom b c} {g : B.Hom a b} {h : B.Hom a c} {a' b' c'}
      {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
  β†’ (p : f ≑ f₁) (q : f B.∘ g ≑ h)
  β†’ hom[ q ] (f' E.∘' g') ≑ hom[ ap (B._∘ g) (sym p) βˆ™ q ] (hom[ p ] f' E.∘' g')
expandl p q = reindex q _ βˆ™ (sym $ smashl _ _)

expandr
  : βˆ€ {a b c} {f : B.Hom b c} {g g₁ : B.Hom a b} {h : B.Hom a c} {a' b' c'}
      {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
  β†’ (p : g ≑ g₁) (q : f B.∘ g ≑ h)
  β†’ hom[ q ] (f' E.∘' g') ≑ hom[ ap (f B.∘_) (sym p) βˆ™ q ] (f' E.∘' hom[ p ] g')
expandr p q = reindex q _ βˆ™ (sym $ smashr _ _)

yank
  : βˆ€ {a b c d}
      {f : B.Hom c d} {g : B.Hom b c} {h : B.Hom a b} {i : B.Hom a c} {j : B.Hom b d}
      {a' b' c' d'}
      {f' : E.Hom[ f ] c' d'} {g' : E.Hom[ g ] b' c'} {h' : E.Hom[ h ] a' b'}
      (p : g B.∘ h ≑ i) (q : f B.∘ g ≑ j) (r : f B.∘ i ≑ j B.∘ h)
  β†’ (f' E.∘' hom[ p ](g' E.∘' h')) E.≑[ r ] hom[ q ] (f' E.∘' g') E.∘' h'
yank {f' = f'} {g' = g'} {h' = h'} p q r = to-pathp $
  hom[ r ] (f' E.∘' hom[ p ] (g' E.∘' h'))                                             β‰‘βŸ¨ smashr p r βŸ©β‰‘
  hom[ ap (B._∘_ _) p βˆ™ r ] (f' E.∘' g' E.∘' h')                                       β‰‘βŸ¨ ap hom[ _ ] (sym (from-pathp Ξ» i β†’ E.assoc' f' g' h' (~ i))) βŸ©β‰‘
  hom[ ap (B._∘_ _) p βˆ™ r  ] (hom[ sym (B.assoc _ _ _) ] ((f' E.∘' g') E.∘' h'))       β‰‘βŸ¨ hom[]-βˆ™ _ _ βŸ©β‰‘
  hom[ sym (B.assoc _ _ _) βˆ™ (ap (B .Precategory._∘_ _) p βˆ™ r)] ((f' E.∘' g') E.∘' h') β‰‘βŸ¨ reindex _ _ βŸ©β‰‘
  hom[ (ap (B._∘ _) q) ] ((f' E.∘' g') E.∘' h')                                        β‰‘Λ˜βŸ¨ whisker-l q βŸ©β‰‘Λ˜
  hom[ q ] (f' E.∘' g') E.∘' h' ∎

cancel
  : βˆ€ {a b} {f g : B.Hom a b} (p q : f ≑ g) {a' b'}
    {f' : E.Hom[ f ] a' b'} {g' : E.Hom[ g ] a' b'}
  β†’ PathP (Ξ» i β†’ E.Hom[ q i ] a' b') f' g'
  β†’ hom[ p ] f' ≑ g'
cancel p q r = reindex p q βˆ™ from-pathp r

kill₁
  : βˆ€ {a b} {a' b'} {f g h : B.Hom a b} {h₁' : E.Hom[ f ] a' b'} {hβ‚‚' : E.Hom[ g ] a' b'}
  β†’ (p : f ≑ g) (q : g ≑ h)
  β†’ PathP (Ξ» i β†’ E.Hom[ p i ] a' b') h₁' hβ‚‚'
  β†’ hom[ p βˆ™ q ] h₁' ≑ hom[ q ] hβ‚‚'
kill₁ p q r = sym (hom[]-βˆ™ _ _) βˆ™ ap hom[ q ] (from-pathp r)


revive₁ : βˆ€ {a b} {f g h : B.Hom a b}
           {a' b'} {f' : E.Hom[ f ] a' b'} {g' : E.Hom[ g ] a' b'}
       β†’ {p : f ≑ g} {q : f ≑ h}
       β†’ f' E.≑[ p ] g'
       β†’ hom[ q ] f' ≑ hom[ sym p βˆ™ q ] g'
revive₁ {f' = f'} {g' = g'} {p = p} {q = q} p' =
  hom[ q ] f'             β‰‘βŸ¨ reindex _ _ βŸ©β‰‘
  hom[ p βˆ™ sym p βˆ™ q ] f' β‰‘βŸ¨ kill₁ p (sym p βˆ™ q) p' βŸ©β‰‘
  hom[ sym p βˆ™ q ] g'     ∎

-- Idea: p is equal to some composite p' βˆ™ q, but it's misassociated or
-- something. We combine the reindexing to fix the association and
-- killing the first parameter to "weave" here.
weave
  : βˆ€ {a b} {a' b'} {f g h : B.Hom a b} {h₁' : E.Hom[ f ] a' b'} {hβ‚‚' : E.Hom[ g ] a' b'}
  β†’ (p : f ≑ h) (p' : f ≑ g) (q : g ≑ h)
  β†’ PathP (Ξ» i β†’ E.Hom[ p' i ] a' b') h₁' hβ‚‚'
  β†’ hom[ p ] h₁' ≑ hom[ q ] hβ‚‚'
weave p p' q s =
    reindex p (p' βˆ™ q)
  βˆ™ kill₁ p' q s

split
  : βˆ€ {a b c} {f f₁ : B.Hom b c} {g g₁ : B.Hom a b} {a' b' c'}
      {f' : E.Hom[ f ] b' c'} {g' : E.Hom[ g ] a' b'}
      (p : f ≑ f₁) (q : g ≑ g₁)
  β†’ hom[ apβ‚‚ B._∘_ p q ] (f' E.∘' g') ≑ hom[ p ] f' E.∘' hom[ q ] g'
split p q =
     reindex _ (apβ‚‚ B._∘_ p refl βˆ™ apβ‚‚ B._∘_ refl q)
  Β·Β· sym (hom[]-βˆ™ _ _)
  Β·Β· ap hom[ _ ] (sym (whisker-l p)) βˆ™ sym (whisker-r q)

liberate
  : βˆ€ {a b x y} {f : B.Hom a b} {f' : E.Hom[ f ] x y}
      (p : f ≑ f)
    β†’ hom[ p ] f' ≑ f'
liberate p = reindex p refl βˆ™ transport-refl _

hom[]⟩⟨_
  : βˆ€ {a b} {f f' : B.Hom a b} {a' b'} {p : f ≑ f'}
      {f' g' : E.Hom[ f ] a' b'}
  β†’ f' ≑ g'
  β†’ hom[ p ] f' ≑ hom[ p ] g'
hom[]⟩⟨_ = ap hom[ _ ]

_⟩∘'⟨_
  : βˆ€ {a b c} {f f' : B.Hom b c} {g g' : B.Hom a b} {a' b' c'}
      {f₁' : E.Hom[ f ] b' c'} {fβ‚‚' : E.Hom[ f' ] b' c'}
      {g₁' : E.Hom[ g ] a' b'} {gβ‚‚' : E.Hom[ g' ] a' b'}
      {p : f ≑ f'} {q : g ≑ g'}
  β†’ f₁' E.≑[ p ] fβ‚‚'
  β†’ g₁' E.≑[ q ] gβ‚‚'
  β†’ f₁' E.∘' g₁' E.≑[ apβ‚‚ B._∘_ p q ] fβ‚‚' E.∘' gβ‚‚'
(p ⟩∘'⟨ q) i = p i E.∘' q i

_⟩∘'⟨refl
  : βˆ€ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {a' b' c'}
      {f₁' : E.Hom[ f ] b' c'} {fβ‚‚' : E.Hom[ f' ] b' c'} {g' : E.Hom[ g ] a' b'}
      {p : f ≑ f'}
  β†’ f₁' E.≑[ p ] fβ‚‚'
  β†’ f₁' E.∘' g' E.≑[ p B.⟩∘⟨refl ] fβ‚‚' E.∘' g'
_⟩∘'⟨refl {g' = g'} p = apd (Ξ» _ β†’ E._∘' g') p

refl⟩∘'⟨_
  : βˆ€ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {a' b' c'}
      {f' : E.Hom[ f ] b' c'}
      {g₁' : E.Hom[ g ] a' b'} {gβ‚‚' : E.Hom[ g' ] a' b'}
      {q : g ≑ g'}
  β†’ g₁' E.≑[ q ] gβ‚‚'
  β†’ f' E.∘' g₁' E.≑[ B.refl⟩∘⟨ q ] f' E.∘' gβ‚‚'
refl⟩∘'⟨_ {f' = f'} p = apd (Ξ» _ β†’ f' E.∘'_) p

split⟩⟨_
  : βˆ€ {a b c} {f f' : B.Hom b c} {g g' : B.Hom a b} {a' b' c'}
      {f₁' : E.Hom[ f ] b' c'} {fβ‚‚' : E.Hom[ f' ] b' c'}
      {g₁' : E.Hom[ g ] a' b'} {gβ‚‚' : E.Hom[ g' ] a' b'}
      {p : f ≑ f'} {q : g ≑ g'}
  β†’ hom[ p ] f₁' E.∘' hom[ q ] g₁' ≑ fβ‚‚' E.∘' gβ‚‚'
  β†’ hom[ apβ‚‚ B._∘_ p q ] (f₁' E.∘' g₁') ≑ fβ‚‚' E.∘' gβ‚‚'
split⟩⟨ p = split _ _ βˆ™ p

infixr 5 _⟩∘'⟨_ refl⟩∘'⟨_ _⟩∘'⟨refl
infixl 4 split⟩⟨_ hom[]⟩⟨_

hom[] : βˆ€ {a b x y} {f g : B.Hom a b} {p : f ≑ g} β†’ E.Hom[ f ] x y β†’ E.Hom[ g ] x y
hom[] {p = p} f' = hom[ p ] f'

pulll-indexr
  : βˆ€ {a b c d} {f : B.Hom c d} {g : B.Hom b c} {h : B.Hom a b} {ac : B.Hom a c}
      {a' : E.Ob[ a ]} {b' : E.Ob[ b ]} {c' : E.Ob[ c ]} {d' : E.Ob[ d ]}
      {f' : E.Hom[ f ] c' d'}
      {g' : E.Hom[ g ] b' c'}
      {h' : E.Hom[ h ] a' b'}
      {fg' : E.Hom[ f B.∘ g ] b' d'}
  β†’ (p : g B.∘ h ≑ ac)
  β†’ (f' E.∘' g' ≑ fg')
  β†’ f' E.∘' hom[ p ] (g' E.∘' h') ≑ hom[ B.pullr p ] (fg' E.∘' h')
pulll-indexr p q = whisker-r _ βˆ™
  sym ( reindex _ (sym (B.assoc _ _ _) βˆ™ ap (_ B.∘_) p) Β·Β· sym (hom[]-βˆ™ _ _)
    ·· ap hom[] ( ap hom[] (ap (E._∘' _) (sym q))
                βˆ™ from-pathp (symP (E.assoc' _ _ _))))

Using these tools, we can define displayed versions of the usual category reasoning combinators.

open Cat B
open Displayed E

private variable
  u w x y z : Ob
  a b c d f g h i : Hom x y
  u' w' x' y' y'' z' : Ob[ x ]
  a' b' c' d' f' g' h' i' : Hom[ a ] x' y'

wrap
  : βˆ€ {f g : Hom x y} {f' : Hom[ f ] x' y'}
  β†’ (p : f ≑ g)
  β†’ f' ≑[ p ] hom[ p ] f'
wrap p = to-pathp refl

wrapl
  : βˆ€ {f h : Hom y z} {g : Hom x y} {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'}
  β†’ (p : f ≑ h)
  β†’ f' ∘' g' ≑[ ap (_∘ g) p ] hom[ p ] f' ∘' g'
wrapl p = to-pathp (unwhisker-l (ap (_∘ _) p) p)

unwrap
  : βˆ€ {f g : Hom x y} {f' : Hom[ f ] x' y'}
  β†’ (p : f ≑ g)
  β†’ hom[ p ] f' ≑[ sym p ] f'
unwrap p = to-pathp⁻ refl

wrapr
  : βˆ€ {f : Hom y z} {g h : Hom x y} {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'}
  β†’ (p : g ≑ h)
  β†’ f' ∘' g' ≑[ ap (f ∘_) p ] f' ∘' hom[ p ] g'
wrapr p = to-pathp (unwhisker-r (ap (_ ∘_) p) p)

unwrapl
  : βˆ€ {f h : Hom y z} {g : Hom x y} {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'}
  β†’ (p : f ≑ h)
  β†’ hom[ p ] f' ∘' g' ≑[ ap (_∘ g) (sym p) ] f' ∘' g'
unwrapl p = to-pathp⁻ (whisker-l p)

unwrapr
  : βˆ€ {f : Hom y z} {g h : Hom x y} {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'}
  β†’ (p : g ≑ h)
  β†’ f' ∘' hom[ p ]  g' ≑[ ap (f ∘_) (sym p) ] f' ∘' g'
unwrapr p = to-pathp⁻ (whisker-r p)

ShiftingsπŸ”—

When working with displayed categories, we prefer to write all of our laws using PathP, as this is conceptually cleaner and avoids coherence issues. However, when performing equational reasoning, we use regular paths and hom[_]. To resolve this mismatch, we define the following combinators.

module _ {f' : Hom[ f ] x' y'} {g' : Hom[ g ] x' y'} (p : f ≑ g) where abstract
  shiftl : f' ≑[ p ] g' β†’ hom[ p ] f' ≑ g'
  shiftl q i = from-pathp (Ξ» j β†’ q (i ∨ j)) i

  shiftr : f' ≑[ p ] g' β†’ f' ≑ hom[ p ]⁻ g'
  shiftr q i = from-pathp (Ξ» j β†’ q (i ∧ ~ j)) (~ i)

Path actionsπŸ”—

Due to the plethora of PathP, we can no longer perform ap as easily. This is especially true when we have a PathP as well as a path between two hom[_]. These combinators allow us to more ergonomically handle that situation.

module _ {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'} {p : f ∘ g ≑ a} where abstract

  apl' : βˆ€ {h' : Hom[ h ] y' z'} {q : h ∘ g ≑ a}
          β†’ {f≑h : f ≑ h}
          β†’ f' ≑[ f≑h ] h'
          β†’ hom[ p ] (f' ∘' g') ≑ hom[ q ] (h' ∘' g')
  apl' {h' = h'} {q = q} {f≑h = f≑h} f'≑h' =
    hom[ p ] (f' ∘' g')                       β‰‘βŸ¨ hom[]⟩⟨ (ap (_∘' g') (shiftr _ f'≑h')) ⟩
    hom[ p ] (hom[ f≑h ]⁻ h' ∘' g')           β‰‘βŸ¨ smashl _ _ ⟩
    hom[ ap (_∘ g) (sym f≑h) βˆ™ p ] (h' ∘' g') β‰‘βŸ¨ reindex _ _ ⟩
    hom[ q ] (h' ∘' g') ∎

  apr' : βˆ€ {h' : Hom[ h ] x' y'} {q : f ∘ h ≑ a}
          β†’ {g≑h : g ≑ h}
          β†’ g' ≑[ g≑h ] h'
          β†’ hom[ p ] (f' ∘' g') ≑ hom[ q ] (f' ∘' h')
  apr' {h' = h'} {q = q} {g≑h = g≑h} g'≑h' =
    hom[ p ] (f' ∘' g')                       β‰‘βŸ¨ hom[]⟩⟨ ap (f' ∘'_) (shiftr _ g'≑h') ⟩
    hom[ p ] (f' ∘' hom[ g≑h ]⁻ h')           β‰‘βŸ¨ smashr _ _ ⟩
    hom[ ap (f ∘_) (sym g≑h) βˆ™ p ] (f' ∘' h') β‰‘βŸ¨ reindex _ _ ⟩
    hom[ q ] (f' ∘' h') ∎

Generalized category lawsπŸ”—

In the definition of displayed categories, the identity and associativity laws are defined over idl, idr, and assoc. However, we often run into situations where we need to apply these equations over different equations! These combinators do just that.

module _ {f' : Hom[ f ] x' y'} where abstract
  idl[] : {p : id ∘ f ≑ f} β†’ hom[ p ] (id' ∘' f') ≑ f'
  idl[] {p = p} = reindex p (idl _) βˆ™ from-pathp (idl' f')

  idr[] : {p : f ∘ id ≑ f} β†’ hom[ p ] (f' ∘' id') ≑ f'
  idr[] {p = p} = reindex p (idr _) βˆ™ from-pathp (idr' f')

assoc[] : βˆ€ {a' : Hom[ a ] y' z'} {b' : Hom[ b ] x' y'} {c' : Hom[ c ] w' x'}
            {p : a ∘ (b ∘ c) ≑ d} {q : (a ∘ b) ∘ c ≑ d}
          β†’ hom[ p ] (a' ∘' (b' ∘' c')) ≑ hom[ q ] ((a' ∘' b') ∘' c')
assoc[] {a = a} {b = b} {c =  c} {a' = a'} {b' = b'} {c' = c'} {p = p} {q = q} =
  hom[ p ] (a' ∘' b' ∘' c')                         β‰‘βŸ¨ hom[]⟩⟨ shiftr (assoc a b c) (assoc' a' b' c') ⟩
  hom[ p ] (hom[ assoc a b c ]⁻ ((a' ∘' b') ∘' c')) β‰‘βŸ¨ hom[]-βˆ™ _ _ ⟩
  hom[ sym (assoc a b c) βˆ™ p ] ((a' ∘' b') ∘' c')   β‰‘βŸ¨ reindex _ q ⟩
  hom[ q ] ((a' ∘' b') ∘' c')                       ∎

Identity morphismsπŸ”—

These are the displayed counterparts to the identity morphism combinators for categories.

module _ {a' : Hom[ a ] x' x'}
         (p : a ≑ id) (p' : a' ≑[ p ] id') where abstract
  eliml' : βˆ€ {f' : Hom[ f ] y' x'} β†’ {q : a ∘ f ≑ f} β†’ a' ∘' f' ≑[ q ] f'
  eliml' {f = f} {f' = f'} {q = q} = to-pathp $
    hom[ q ] (a' ∘' f')      β‰‘βŸ¨ apl' p' ⟩
    hom[ idl f ] (id' ∘' f') β‰‘βŸ¨ idl[] ⟩
    f' ∎

  elimr' : βˆ€ {f' : Hom[ f ] x' y'} β†’ {q : f ∘ a ≑ f} β†’ f' ∘' a' ≑[ q ] f'
  elimr' {f = f} {f' = f'} {q = q} = to-pathp $
    hom[ q ] (f' ∘' a')      β‰‘βŸ¨ apr' p' ⟩
    hom[ idr f ] (f' ∘' id') β‰‘βŸ¨ idr[] ⟩
    f' ∎

  introl' : βˆ€ {f' : Hom[ f ] y' x'} β†’ {q : f ≑ a ∘ f} β†’ f' ≑[ q ] a' ∘' f'
  introl' {f' = f'} {q = q} i = eliml' {f' = f'} {q = sym q} (~ i)

  intror' : βˆ€ {f' : Hom[ f ] x' y'} β†’ {q : f ≑ f ∘ a} β†’ f' ≑[ q ] f' ∘' a'
  intror' {f' = f'} {q = q} i = elimr' {f' = f'} {q = sym q} (~ i)

ReassociationsπŸ”—

These are the displayed counterparts to the reassociation combinators for categories.

module _ {a' : Hom[ a ] y' z'} {b' : Hom[ b ] x' y'} {c' : Hom[ c ] x' z'}
         (p : a ∘ b ≑ c) (p' : a' ∘' b' ≑[ p ] c') where abstract

  pulll' : βˆ€ {f' : Hom[ f ] w' x'} {q : a ∘ (b ∘ f) ≑ c ∘ f}
           β†’ a' ∘' (b' ∘' f') ≑[ q ] c' ∘' f'
  pulll' {f = f} {f' = f'} {q = q} = to-pathp $
    hom[ q ] (a' ∘' b' ∘' f')                       β‰‘βŸ¨ assoc[] ⟩
    hom[ sym (assoc a b f) βˆ™ q ] ((a' ∘' b') ∘' f') β‰‘βŸ¨ apl' p' ⟩
    hom[ refl ] (c' ∘' f')                          β‰‘βŸ¨ liberate _ ⟩
    c' ∘' f'                                        ∎

  pulll[] : βˆ€ {f' : Hom[ f ] w' x'}
           β†’ a' ∘' (b' ∘' f') ≑[ pulll p ] c' ∘' f'
  pulll[] = pulll'

  pullr' : βˆ€ {f' : Hom[ f ] z' w'} {q : (f ∘ a) ∘ b ≑ f ∘ c}
         β†’ (f' ∘' a') ∘' b' ≑[ q ] f' ∘' c'
  pullr' {f = f} {f' = f'} {q = q} = to-pathp $
    hom[ q ] ((f' ∘' a') ∘' b')             β‰‘Λ˜βŸ¨ assoc[] ⟩
    hom[ assoc f a b βˆ™ q ] (f' ∘' a' ∘' b') β‰‘βŸ¨ apr' p' ⟩
    hom[ refl ] (f' ∘' c')                  β‰‘βŸ¨ liberate _ ⟩
    f' ∘' c'                                ∎

  pullr[] : βˆ€ {f' : Hom[ f ] z' w'}
          β†’ (f' ∘' a') ∘' b' ≑[ pullr p ] f' ∘' c'
  pullr[] = pullr'

module _ {a' : Hom[ a ] y' z'} {b' : Hom[ b ] x' y'} {c' : Hom[ c ] x' z'}
         (p : c ≑ a ∘ b) (p' : c' ≑[ p ] a' ∘' b') where abstract

  pushl' : βˆ€ {f' : Hom[ f ] w' x'} {q : c ∘ f ≑ a ∘ (b ∘ f)}
           β†’ c' ∘' f' ≑[ q ] a' ∘' (b' ∘' f')
  pushl' {f' = f'} {q = q} i =
    pulll' (sym p) (Ξ» j β†’ p' (~ j)) {f' = f'} {q = sym q} (~ i)

  pushl[] : βˆ€ {f' : Hom[ f ] w' x'}
           β†’ c' ∘' f' ≑[ pushl p ] a' ∘' (b' ∘' f')
  pushl[] = pushl'

  pushr' : βˆ€ {f' : Hom[ f ] z' w'} {q : f ∘ c ≑ (f ∘ a) ∘ b}
           β†’ f' ∘' c' ≑[ q ] (f' ∘' a') ∘' b'
  pushr' {f' = f'} {q = q} i =
    pullr' (sym p) (Ξ» j β†’ p' (~ j)) {f' = f'} {q = sym q} (~ i)

  pushr[] : βˆ€ {f' : Hom[ f ] z' w'}
           β†’ f' ∘' c' ≑[ pushr p ] (f' ∘' a') ∘' b'
  pushr[] = pushr'

module _ {f' : Hom[ f ] y' z'} {h' : Hom[ h ] x' y'}
         {g' : Hom[ g ] y'' z'} {i' : Hom[ i ] x' y''}
         (p : f ∘ h ≑ g ∘ i) (p' : f' ∘' h' ≑[ p ] g' ∘' i') where abstract

  extendl' : βˆ€ {b' : Hom[ b ] w' x'} {q : f ∘ (h ∘ b) ≑ g ∘ (i ∘ b)}
             β†’ f' ∘' (h' ∘' b') ≑[ q ] g' ∘' (i' ∘' b')
  extendl' {b = b} {b' = b'} {q = q} = to-pathp $
    hom[ q ] (f' ∘' h' ∘' b')                       β‰‘βŸ¨ assoc[] ⟩
    hom[ sym (assoc f h b) βˆ™ q ] ((f' ∘' h') ∘' b') β‰‘βŸ¨ apl' p' ⟩
    hom[ sym (assoc g i b) ] ((g' ∘' i') ∘' b')     β‰‘βŸ¨ shiftl _ (Ξ» j β†’ (assoc' g' i' b') (~ j)) ⟩
    g' ∘' i' ∘' b'                                  ∎

  extendr' : βˆ€ {a' : Hom[ a ] z' w'} {q : (a ∘ f) ∘ h ≑ (a ∘ g) ∘ i}
             β†’ (a' ∘' f') ∘' h' ≑[ q ] (a' ∘' g') ∘' i'
  extendr' {a = a} {a' = a'} {q = q} = to-pathp $
    hom[ q ] ((a' ∘' f') ∘' h')             β‰‘Λ˜βŸ¨ assoc[] ⟩
    hom[ assoc a f h βˆ™ q ] (a' ∘' f' ∘' h') β‰‘βŸ¨ apr' p' ⟩
    hom[ assoc a g i ] (a' ∘'(g' ∘' i'))    β‰‘βŸ¨ shiftl _ (assoc' a' g' i') ⟩
    (a' ∘' g') ∘' i' ∎

  extend-inner' : βˆ€ {a' : Hom[ a ] z' u'} {b' : Hom[ b ] w' x'}
                    {q : a ∘ f ∘ h ∘ b ≑ a ∘ g ∘ i ∘ b}
                  β†’ a' ∘' f' ∘' h' ∘' b' ≑[ q ] a' ∘' g' ∘' i' ∘' b'
  extend-inner' {a = a} {b = b} {a' = a'} {b' = b'} {q = q} = to-pathp $
    hom[ q ] (a' ∘' f' ∘' h' ∘' b')                                   β‰‘βŸ¨ apr' (assoc' f' h' b') ⟩
    hom[ ap (a ∘_) (sym (assoc f h b)) βˆ™ q ] (a' ∘' (f' ∘' h') ∘' b') β‰‘βŸ¨ apr' (Ξ» j β†’ p' j ∘' b') ⟩
    hom[ ap (a ∘_) (sym (assoc g i b)) ] (a' ∘' (g' ∘' i') ∘' b')     β‰‘βŸ¨ shiftl _ (Ξ» j β†’ a' ∘' assoc' g' i' b' (~ j)) ⟩
    a' ∘' g' ∘' i' ∘' b' ∎

  extendl[] : βˆ€ {b' : Hom[ b ] w' x'}
             β†’ f' ∘' (h' ∘' b') ≑[ extendl p ] g' ∘' (i' ∘' b')
  extendl[] = extendl'

  extendr[] : βˆ€ {a' : Hom[ a ] z' w'}
             β†’ (a' ∘' f') ∘' h' ≑[ extendr p ] (a' ∘' g') ∘' i'
  extendr[] = extendr'

CancellationπŸ”—

These are the displayed counterparts to the cancellation combinators for categories

module _ {a' : Hom[ a ] y' x'} {b' : Hom[ b ] x' y'}
         (p : a ∘ b ≑ id) (p' : a' ∘' b' ≑[ p ] id') where abstract

  cancell' : βˆ€ {f' : Hom[ f ] z' x'} {q : a ∘ b ∘ f ≑ f}
             β†’ a' ∘' b' ∘' f' ≑[ q ] f'
  cancell' {f = f} {f' = f'} {q = q} = to-pathp $
    hom[ q ] (a' ∘' b' ∘' f')                       β‰‘βŸ¨ assoc[] ⟩
    hom[ sym (assoc a b f) βˆ™ q ] ((a' ∘' b') ∘' f') β‰‘βŸ¨ shiftl _ (eliml' p p') ⟩
    f'                                              ∎

  cancell[] : βˆ€ {f' : Hom[ f ] z' x'}
             β†’ a' ∘' b' ∘' f' ≑[ cancell p ] f'
  cancell[] = cancell'

  cancelr' : βˆ€ {f' : Hom[ f ] x' z'} {q : (f ∘ a) ∘ b ≑ f}
             β†’ (f' ∘' a') ∘' b' ≑[ q ] f'
  cancelr' {f = f} {f' = f'} {q = q} = to-pathp $
    hom[ q ] ((f' ∘' a') ∘' b')             β‰‘Λ˜βŸ¨ assoc[] ⟩
    hom[ assoc f a b βˆ™ q ] (f' ∘' a' ∘' b') β‰‘βŸ¨ shiftl _ (elimr' p p') ⟩
    f' ∎

  cancelr[] : βˆ€ {f' : Hom[ f ] x' z'}
             β†’ (f' ∘' a') ∘' b' ≑[ cancelr p ] f'
  cancelr[] = cancelr'

  cancel-inner' : βˆ€ {f' : Hom[ f ] x' z'} {g' : Hom[ g ] w' x'}
    β†’ {q : (f ∘ a) ∘ (b ∘ g) ≑ f ∘ g}
    β†’ (f' ∘' a') ∘' (b' ∘' g') ≑[ q ] f' ∘' g'
  cancel-inner' = cast[] $ pullr[] _ cancell[]

  cancel-inner[] : βˆ€ {f' : Hom[ f ] x' z'} {g' : Hom[ g ] w' x'}
    β†’ (f' ∘' a') ∘' (b' ∘' g') ≑[ cancel-inner p ] f' ∘' g'
  cancel-inner[] = cancel-inner'

  insertl' : βˆ€ {f' : Hom[ f ] z' x'} {q : f ≑ a ∘ b ∘ f }
             β†’ f' ≑[ q ] a' ∘' b' ∘' f'
  insertl' {f = f} {f' = f'} {q = q} i = cancell' {f' = f'} {q = sym q} (~ i)

  insertr' : βˆ€ {f' : Hom[ f ] x' z'} {q : f ≑ (f ∘ a) ∘ b }
             β†’ f' ≑[ q ] (f' ∘' a') ∘' b'
  insertr' {f = f} {f' = f'} {q = q} i = cancelr' {f' = f'} {q = sym q} (~ i)