Structures · Category theory
CategoryTheory.Closed
An object X is (right) closed if (X ⊗ -) is a left adjoint.
- Shape
- One type argument · adds rightAdj, adj
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances2
- CategoryTheory.Functor
- CategoryTheory.Cat
How is a type an instance?
Loading the hierarchy index…
Assumed by124
- CategoryTheory.ihom
- CategoryTheory.MonoidalClosed.uncurry
- CategoryTheory.MonoidalClosed.curry
- CategoryTheory.ihom.ev
- CategoryTheory.MonoidalClosed.pre
- CategoryTheory.ihom.adjunction
- CategoryTheory.ihom.coev
- CategoryTheory.MonoidalClosed.uncurry_curry
- CategoryTheory.MonoidalClosed.curry'
- CategoryTheory.MonoidalClosed.comp
- CategoryTheory.zeroMul
- CategoryTheory.MonoidalClosed.uncurry_injective
- CategoryTheory.MonoidalClosed.uncurry_eq
- CategoryTheory.MonoidalClosed.uncurry_natural_left
- CategoryTheory.curryRightUnitorHom
- CategoryTheory.MonoidalClosed.id
- CategoryTheory.Closed.adj
- CategoryTheory.MonoidalClosed.ihomCurry
- CategoryTheory.MonoidalClosed.compTranspose
- CategoryTheory.Over.sections
- CategoryTheory.MonoidalClosed.ihomUncurry
- CategoryTheory.MonoidalClosed.uncurry_id_eq_ev
- CategoryTheory.MonoidalClosed.curry_natural_left
- CategoryTheory.MonoidalClosed.curry_uncurry
- CategoryTheory.MonoidalClosed.uncurry'
- CategoryTheory.Over.sectionsUncurry
- CategoryTheory.MonoidalClosed.uncurry_natural_right
- CategoryTheory.MonoidalClosed.curry_natural_right
- CategoryTheory.Over.sectionsCurry
- CategoryTheory.mulZero
- CategoryTheory.ihom.ev_naturality
- CategoryTheory.MonoidalClosed.comp_eq
- CategoryTheory.MonoidalClosed.compTranspose_eq
- CategoryTheory.MonoidalClosed.curryHomEquiv'
- CategoryTheory.MonoidalClosed.whiskerLeft_curry'_ihom_ev_app
- CategoryTheory.MonoidalClosed.curry_injective
- CategoryTheory.MonoidalClosed.whiskerLeft_curry'_comp
- CategoryTheory.MonoidalClosed.whiskerLeft_curry_ihom_ev_app
- CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev
- CategoryTheory.MonoidalClosed.curry_pre_app
- CategoryTheory.MonoidalClosed.uncurry_uncurry_ihomCurry
- CategoryTheory.MonoidalClosed.pre_id
- CategoryTheory.MonoidalClosed.homEquiv_apply_eq
- CategoryTheory.Over.sectionsCurry_sectionUncurry
- CategoryTheory.MonoidalClosed.uncurry_ihomUncurry
- CategoryTheory.MonoidalClosed.ihomCurryIso
- CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq
- CategoryTheory.MonoidalClosed.curry'_whiskerRight_comp
- CategoryTheory.Over.sectionsUncurry_sectionsCurry
- CategoryTheory.Over.toOverSectionsAdj
Ancestors0
No ancestors.