Theorems · Theorem · category theory
CategoryTheory.Oplax.LaxTrans.whiskerRight_as_app
∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
{F G H : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B),
(CategoryTheory.Oplax.LaxTrans.whiskerRight Γ ι).as.app a =
CategoryTheory.Bicategory.whiskerRight (Γ.as.app a) (ι.app a)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.Bicategorystatement and proof · cited by 1,587
- Prefunctor.objstatement · cited by 1,241
- CategoryTheory.PrelaxFunctor.toPrelaxFunctorStructstatement · cited by 1,154
- CategoryTheory.PrelaxFunctorStruct.toPrefunctorstatement · cited by 1,142
- CategoryTheory.Bicategory.whiskerRightstatement · cited by 531
- CategoryTheory.OplaxFunctorstatement and proof · cited by 253
- CategoryTheory.OplaxFunctor.toPrelaxFunctorstatement · cited by 246
- CategoryTheory.Oplax.LaxTrans.appstatement · cited by 48
- CategoryTheory.Oplax.LaxTrans.Modification.appstatement and proof · cited by 32
- CategoryTheory.Oplax.LaxTrans.Hom.asstatement and proof · cited by 24
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.