Theorems · Definition · category theory

CategoryTheory.Bicategory.LeftExtension.whiskerHom

{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {s t : CategoryTheory.Bicategory.LeftExtension f g} →
            (s ⟶ t) → {x : B} → (h : c ⟶ x) → s.whisker h ⟶ t.whisker h

Construct a morphism between whiskered extensions.

Defined in: Mathlib.CategoryTheory.Bicategory.Extension
Cited by: 1 results in Mathlib
Foundations: Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Bicategory

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

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
CategoryTheory.Bicategory.whiskerRightproof · cited by 531
CategoryTheory.StructuredArrow.Hom.rightproof · cited by 82
CategoryTheory.StructuredArrow.homMkproof · cited by 47
CategoryTheory.Bicategory.precompstatement · cited by 40
CategoryTheory.Bicategory.LeftExtensionstatement and proof · cited by 29
CategoryTheory.Bicategory.LeftExtension.whiskerstatement · cited by 15

Cited by2

Results whose statement or proof uses this declaration.

CategoryTheory.Bicategory.LeftExtension.whiskerIsoproof · cited by 0
CategoryTheory.Bicategory.LeftExtension.whiskerHom_rightstatement and proof · cited by 0