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)