Theorems · Definition · category theory

CategoryTheory.Bicategory.InducedBicategory.Hom.hom

{B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} → {X Y : CategoryTheory.Bicategory.InducedBicategory C F} → X.Hom Y → (F X ⟶ F Y)

The morphism in C underlying the morphism in InducedBicategory C F.

Defined in

Mathlib.CategoryTheory.Bicategory.InducedBicategory

Cited by

36 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Bicategory