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
-spaces
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'} → PathP (λ i → E.Hom[ p i ] b′ c′) f₁′ f₂′ → PathP (λ i → E.Hom[ q i ] a′ b′) g₁′ g₂′ → hom[ p ] f₁′ E.∘′ hom[ q ] g₁′ ≡ f₂′ E.∘′ g₂′ p ⟩∘′⟨ q = ap₂ E._∘′_ (from-pathp p) (from-pathp q) _⟩∘′⟨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'} → PathP (λ i → E.Hom[ p i ] b′ c′) f₁′ f₂′ → hom[ p ] f₁′ E.∘′ g′ ≡ f₂′ E.∘′ g′ p ⟩∘′⟨refl = ap₂ E._∘′_ (from-pathp p) refl 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'} → PathP (λ i → E.Hom[ q i ] a′ b′) g₁′ g₂′ → f′ E.∘′ hom[ q ] g₁′ ≡ f′ E.∘′ g₂′ refl⟩∘′⟨ p = ap₂ E._∘′_ refl (from-pathp 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)