Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Bicategory.Adj.Hom.l

{B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : B} → CategoryTheory.Bicategory.Adj.Hom a b → (a ⟶ b)

the left adjoint

Defined in
Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Cited by
89 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
CategoryTheory.Bicategory
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.Bicategory.Adj.Hom.adj · cited by 46Hom.adjCategoryTheory.Bicategory.Adj.Hom₂.τl · cited by 34Hom₂.τlCategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.hom · cited by 22DescentDataAsCoalgebra.homCategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence · cited by 13DescentDataAsCoalgebra.co…CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra · cited by 6Pseudofunctor.toDescentDa…CategoryTheory.Bicategory.Adj.forget₁ · cited by 5Adj.forget₁CategoryTheory.Bicategory.Adj.iso₂Mk · cited by 5Adj.iso₂MkCategoryTheory.Bicategory.Adj.Bicategory.associator · cited by 4Bicategory.associatorCategoryTheory.Bicategory.Adj.Bicategory.leftUnitor · cited by 4Bicategory.leftUnitorCategoryTheory.Bicategory.Adj.Bicategory.rightUnitor · cited by 4Bicategory.rightUnitorCategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso · cited by 3Pseudofunctor.toDescentDa…CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk · cited by 3DescentDataAsCoalgebra.is…CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeft · cited by 2Bicategory.whiskerLeftCategoryTheory.Bicategory.Adj.Bicategory.whiskerRight · cited by 2Bicategory.whiskerRightCategoryTheory.Bicategory.Adj.Hom₂.ext · cited by 2Hom₂.extQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Bicategory · cited by 1587CategoryTheory.BicategoryCategoryTheory.Bicategory.Adj.Hom · cited by 6Adj.HomHom.lCITED BYCITES

Cites3

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

Cited by119

Results whose statement or proof uses this declaration.