Structures · Category theory
CategoryTheory.HasRightDual
A class of objects which have a right dual.
- Shape
- One type argument · adds rightDual, exact
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances2
- CategoryTheory.Functor
- FGModuleCat
How is a type an instance?
Loading the hierarchy index…
Assumed by20
- CategoryTheory.HasRightDual.rightDual
- CategoryTheory.rightAdjointMate
- CategoryTheory.coevaluation_comp_rightAdjointMate
- CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight
- CategoryTheory.rightAdjointMate_id
- CategoryTheory.rightAdjointMate_comp_evaluation
- CategoryTheory.comp_rightAdjointMate
- CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_evaluation
- CategoryTheory.tensorRightHomEquiv_whiskerLeft_comp_evaluation
- CategoryTheory.rightAdjointMate_comp
- CategoryTheory.leftDual_rightDual
- CategoryTheory.hasRightDualOfEquivalence
- CategoryTheory.hasRightDualTensor
- CategoryTheory.HasRightDual.exact
- CategoryTheory.comp_rightAdjointMate_assoc
- CategoryTheory.rightDualTensorIso
- CategoryTheory.BraidedCategory.hasLeftDualOfHasRightDual
- CategoryTheory.rightAdjointMate_comp_evaluation_assoc
- CategoryTheory.hasLeftDualRightDual
- CategoryTheory.coevaluation_comp_rightAdjointMate_assoc
Ancestors0
No ancestors.