Theorems · Definition · category theory
CategoryTheory.Bicategory.Adj.Hom.adj
{B : Type u} →
[inst : CategoryTheory.Bicategory B] →
{a b : B} → (self : CategoryTheory.Bicategory.Adj.Hom a b) → CategoryTheory.Bicategory.Adjunction self.l self.rthe adjunction
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Bicategory
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Bicategorystatement and proof · cited by 1,587
- CategoryTheory.Bicategory.Adj.Hom.lstatement · cited by 89
- CategoryTheory.Bicategory.Adjunctionstatement · cited by 83
- CategoryTheory.Bicategory.Adj.Hom.rstatement · cited by 82
- CategoryTheory.Bicategory.Adj.Homstatement and proof · cited by 6
Cited by60
Results whose statement or proof uses this declaration.
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalencestatement and proof · cited by 13
- CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraproof · cited by 6
- CategoryTheory.Bicategory.Adj.iso₂Mkstatement and proof · cited by 5
- CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIsostatement · cited by 3
- CategoryTheory.Bicategory.Adj.Hom₂.extproof · cited by 2
- CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τlstatement · cited by 1
- CategoryTheory.Bicategory.Adj.counit_naturalitystatement and proof · cited by 1
- CategoryTheory.Bicategory.Adj.hom₂_extproof · cited by 1
- CategoryTheory.Bicategory.Adj.left_triangle_componentsstatement and proof · cited by 1
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.mk.injstatement and proof · cited by 1
- CategoryTheory.Bicategory.Adj.right_triangle_componentsstatement and proof · cited by 1
- CategoryTheory.Bicategory.Adj.unit_naturalitystatement and proof · cited by 1