Theorems · Definition · category theory
CategoryTheory.Bicategory.Adj.Hom.r
{B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : B} → CategoryTheory.Bicategory.Adj.Hom a b → (b ⟶ a)the right adjoint
- Cited by
- 82 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Bicategory
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 · cited by 32,603
- CategoryTheory.Bicategorystatement and proof · cited by 1,587
- CategoryTheory.Bicategory.Adj.Homstatement and proof · cited by 6
Cited by110
Results whose statement or proof uses this declaration.
- CategoryTheory.Bicategory.Adj.Hom.adjstatement · cited by 46
- CategoryTheory.Bicategory.Adj.Hom₂.τrstatement · cited by 31
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.homstatement · cited by 22
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalencestatement · cited by 13
- CategoryTheory.Bicategory.Adj.iso₂Mkstatement and proof · cited by 5
- CategoryTheory.Bicategory.Adj.Bicategory.associatorproof · cited by 4
- CategoryTheory.Bicategory.Adj.Bicategory.leftUnitorproof · cited by 4
- CategoryTheory.Bicategory.Adj.Bicategory.rightUnitorproof · cited by 4
- CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIsostatement · cited by 3
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMkstatement and proof · cited by 3
- CategoryTheory.Bicategory.Adj.Bicategory.whiskerLeftproof · cited by 2
- CategoryTheory.Bicategory.Adj.Bicategory.whiskerRightproof · cited by 2