Documentation

InfinityCosmos.ForMathlib.CategoryTheory.Bicategory.Strict.Closed

source
def CategoryTheory.Bicategory.HomWhiskerLeft (C : Type u) [Bicategory C] (X : C) {Y Y' : C} (g : Y ⟶ Y') :
Functor (X ⟶ Y) (X ⟶ Y')

The morphism (X ⟶ Y) ⥤ (X ⟶ Y') induced by a morphism Y ⟶ Y'.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Bicategory.HomWhiskerLeft_map (C : Type u) [Bicategory C] (X : C) {Y Y' : C} (g : Y ⟶ Y') {X✝ Y✝ : X ⟶ Y} (φ : X✝ ⟶ Y✝) :
    (HomWhiskerLeft C X g).map φ = whiskerRight φ g
    source
    @[simp]
    theorem CategoryTheory.Bicategory.HomWhiskerLeft_obj (C : Type u) [Bicategory C] (X : C) {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y) :
    (HomWhiskerLeft C X g).obj f = CategoryStruct.comp f g
    source
    def CategoryTheory.Bicategory.HomWhiskerRight (C : Type u) [Bicategory C] {X X' : C} (Y : C) (f : X ⟶ X') :
    Functor (X' ⟶ Y) (X ⟶ Y)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Bicategory.HomWhiskerRight_map (C : Type u) [Bicategory C] {X X' : C} (Y : C) (f : X ⟶ X') {X✝ Y✝ : X' ⟶ Y} (φ : X✝ ⟶ Y✝) :
      (HomWhiskerRight C Y f).map φ = whiskerLeft f φ
      source
      @[simp]
      theorem CategoryTheory.Bicategory.HomWhiskerRight_obj (C : Type u) [Bicategory C] {X X' : C} (Y : C) (f : X ⟶ X') (g : X' ⟶ Y) :
      (HomWhiskerRight C Y f).obj g = CategoryStruct.comp f g
      source
      def CategoryTheory.Bicategory.HomFunctor (C : Type u) [Bicategory C] [Strict C] :
      Functor Cᵒᵖ (Functor C Cat)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        class CategoryTheory.Bicategory.Strict.CartesianMonoidal (C : Type u) [Bicategory C] [Strict C] extends CategoryTheory.CartesianMonoidalCategory C :
        Type (max (max u v) w)
        Instances
          source
          class CategoryTheory.Bicategory.Strict.CartesianClosed (C : Type u) [Bicategory C] [Strict C] extends CategoryTheory.Bicategory.Strict.CartesianMonoidal C, CategoryTheory.MonoidalClosed C :
          Type (max (max u v) w)
          Instances