Theorems · Definition · category theory
CategoryTheory.Bicategory.Adj.obj
{B : Type u} → [inst : CategoryTheory.Bicategory B] → CategoryTheory.Bicategory.Adj B → BIf a : Adj B, a.obj : B is the underlying object of the bicategory B.
- Cited by
- 128 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- CategoryTheory.Bicategory
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 and proof · cited by 1,587
- CategoryTheory.Bicategory.Adjstatement and proof · cited by 131
Cited by152
Results whose statement or proof uses this declaration.
- CategoryTheory.Bicategory.Adj.Hom₂.τlstatement · cited by 34
- CategoryTheory.Bicategory.Adj.Hom₂.τrstatement · cited by 31
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.objstatement · cited by 29
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.homstatement · cited by 22
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.homstatement · cited by 18
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalencestatement · cited by 13
- CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebrastatement and proof · cited by 6
- CategoryTheory.Bicategory.Adj.forget₁proof · cited by 5
- CategoryTheory.Bicategory.Adj.iso₂Mkstatement · cited by 5
- CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIsostatement · cited by 3
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMkstatement · cited by 3
- CategoryTheory.Bicategory.Adj.Hom₂.extstatement · cited by 2