Theorems · Inductive type · category theory
CategoryTheory.FreeBicategory.Hom
{B : Type u} → [Quiver B] → B → B → Type (max u v)1-morphisms in the free bicategory.
- Defined in
- Mathlib.CategoryTheory.Bicategory.Free
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Quiver
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiverstatement · cited by 405
Cited by46
Results whose statement or proof uses this declaration.
- CategoryTheory.FreeBicategory.normalizeAuxstatement and proof · cited by 9
- CategoryTheory.FreeBicategory.Hom.belowstatement and proof · cited by 4
- CategoryTheory.FreeBicategory.Hom.brecOn.gostatement and proof · cited by 4
- CategoryTheory.FreeBicategory.normalizeIsostatement and proof · cited by 4
- CategoryTheory.FreeBicategory.Hom.brecOn.eqstatement and proof · cited by 3
- CategoryTheory.FreeBicategory.homCategory'statement · cited by 2
- CategoryTheory.FreeBicategory.Hom.brecOnstatement and proof · cited by 1
- CategoryTheory.FreeBicategory.Hom.casesOnstatement and proof · cited by 1
- CategoryTheory.FreeBicategory.inclusionPathAuxstatement · cited by 1
- CategoryTheory.FreeBicategory.Hom.comp.injstatement and proof · cited by 1
- CategoryTheory.FreeBicategory.Hom.comp.noConfusionstatement and proof · cited by 1
- CategoryTheory.FreeBicategory.Hom.of.injstatement · cited by 1