Theorems · Inductive type · category theory
CategoryTheory.HasLeftDual
{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → C → Type (max u₁ v₁)A class of objects which have a left dual.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
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.Categorystatement · cited by 32,673
- CategoryTheory.MonoidalCategorystatement · cited by 3,095
Cited by31
Results whose statement or proof uses this declaration.
- CategoryTheory.HasLeftDual.leftDualstatement and proof · cited by 17
- CategoryTheory.leftAdjointMatestatement and proof · cited by 13
- CategoryTheory.comp_leftAdjointMatestatement and proof · cited by 1
- CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluationstatement and proof · cited by 1
- CategoryTheory.tensorLeftHomEquiv_whiskerRight_comp_evaluationstatement and proof · cited by 1
- CategoryTheory.leftAdjointMate_compstatement and proof · cited by 1
- CategoryTheory.leftAdjointMate_comp_evaluationstatement and proof · cited by 1
- CategoryTheory.leftAdjointMate_idstatement and proof · cited by 1
- CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeftstatement and proof · cited by 1
- CategoryTheory.coevaluation_comp_leftAdjointMatestatement and proof · cited by 1
- CategoryTheory.LeftRigidCategory.casesOnstatement and proof · cited by 0
- CategoryTheory.hasLeftDualOfEquivalencestatement and proof · cited by 0