Theorems · Definition · category theory

CategoryTheory.Bicategory.InducedBicategory.mkHom

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

Synonym for Hom.mk which makes unification easier.

Defined in: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Cited by: 3 results in Mathlib
Foundations: Depth 4 from the axioms · uses no axioms
Assumes: CategoryTheory.Bicategory

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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.Bicategorystatement and proof · cited by 1,587
CategoryTheory.Bicategory.InducedBicategorystatement and proof · cited by 39

Cited by4

Results whose statement or proof uses this declaration.

CategoryTheory.Bicategory.InducedBicategory.mkHom₂statement · cited by 1
CategoryTheory.Bicategory.InducedBicategory.mkHom_eqToHomstatement · cited by 0
CategoryTheory.Bicategory.InducedBicategory.bicategory_whiskerLeft_homstatement · cited by 0
CategoryTheory.Bicategory.InducedBicategory.bicategory_whiskerRight_homstatement · cited by 0