Theorems · Inductive type · category theory

CategoryTheory.Bicategory.InducedBicategory.Hom

{B : Type u_1} →
  {C : Type u_2} →
    [CategoryTheory.Bicategory C] →
      {F : B → C} →
        CategoryTheory.Bicategory.InducedBicategory C F → CategoryTheory.Bicategory.InducedBicategory C F → Type u_4

InducedBicategory.Hom X Y is a type-alias for morphisms between X Y : B viewed as objects of B with the induced bicategory structure. This is given a CategoryStruct instance below, where the identity and composition is induced from C.

Defined in: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Cited by: 5 results in Mathlib
Foundations: Depth 1 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.

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Bicategorystatement · cited by 1,587
CategoryTheory.Bicategory.InducedBicategorystatement · cited by 39

Cited by11

Results whose statement or proof uses this declaration.

CategoryTheory.Bicategory.InducedBicategory.Hom.homstatement and proof · cited by 36
CategoryTheory.Bicategory.InducedBicategory.Hom.extstatement and proof · cited by 2
CategoryTheory.Bicategory.InducedBicategory.Hom.casesOnstatement and proof · cited by 0
CategoryTheory.Bicategory.InducedBicategory.Hom.ctorIdxstatement and proof · cited by 0
CategoryTheory.Bicategory.InducedBicategory.Hom.ext_iffstatement and proof · cited by 0
CategoryTheory.Bicategory.InducedBicategory.Hom.noConfusionstatement and proof · cited by 0
CategoryTheory.Bicategory.InducedBicategory.Hom.noConfusionTypestatement and proof · cited by 0
CategoryTheory.Bicategory.InducedBicategory.Hom.recOnstatement and proof · cited by 0
CategoryTheory.Bicategory.InducedBicategory.bicategory_Homstatement · cited by 0
CategoryTheory.Bicategory.InducedBicategory.bicategory_comp_homstatement and proof · cited by 0
CategoryTheory.Bicategory.InducedBicategory.categoryStruct_comp_homstatement and proof · cited by 0