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)