Documentation

Mathlib.CategoryTheory.Closed.Cartesian

Cartesian closed categories #

We define exponentiable objects to be closed objects in a cartesian monoidal category, i.e. (X × -) is a left adjoint.

We say a category is cartesian closed if every object is exponentiable (equivalently, that the category equipped with the cartesian monoidal structure is closed monoidal).

Show that exponential forms a difunctor and define the exponential comparison morphisms.

Implementation Details #

Cartesian closed categories require a CartesianMonoidalCategory instance. If one wishes to state that a category that hasFiniteProducts is cartesian closed, they should first promote the hasFiniteProducts instance to a CartesianMonoidalCategory one using CategoryTheory.ofChosenFiniteProducts.

TODO #

Some of the results here are true more generally for closed objects and for closed monoidal categories, and these could be generalised.

@[reducible, inline]

abbrev CategoryTheory.Exponentiable {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) :

Type (max u v)

An object X is exponentiable if (X × -) is a left adjoint. We define this as being Closed in the cartesian monoidal structure.

Equations

CategoryTheory.Exponentiable X = CategoryTheory.Closed X

@[reducible, inline]

abbrev CategoryTheory.Exponentiable.mk {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (exp : Functor C C) (adj : MonoidalCategory.tensorLeft X ⊣ exp) :

Exponentiable X

Constructor for Exponentiable X which takes as an input an adjunction MonoidalCategory.tensorLeft X ⊣ exp for some functor exp : C ⥤ C.

Equations

CategoryTheory.Exponentiable.mk X exp adj = { rightAdj := exp, adj := adj }

def CategoryTheory.binaryProductExponentiable {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y : C} (hX : Exponentiable X) (hY : Exponentiable Y) :

Exponentiable (MonoidalCategoryStruct.tensorObj X Y)

If X and Y are exponentiable then X ⨯ Y is. This isn't an instance because it's not usually how we want to construct exponentials, we'll usually prove all objects are exponential uniformly.

Equations

CategoryTheory.binaryProductExponentiable hX hY = CategoryTheory.tensorClosed hX hY

def CategoryTheory.terminalExponentiable {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] :

Exponentiable (MonoidalCategoryStruct.tensorUnit C)

The terminal object is always exponentiable. This isn't an instance because most of the time we'll prove cartesian closed for all objects at once, rather than just for this one.

Equations

CategoryTheory.terminalExponentiable = CategoryTheory.unitClosed

@[reducible, inline]

abbrev CategoryTheory.CartesianClosed (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] :

Type (max u v)

A category C is cartesian closed if it has finite products and every object is exponentiable. We define this as MonoidalClosed with respect to the cartesian monoidal structure.

Equations

CategoryTheory.CartesianClosed C = CategoryTheory.MonoidalClosed C

def CategoryTheory.CartesianClosed.mk (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] (exp : (X : C) → Exponentiable X) :

CartesianClosed C

Constructor for CartesianClosed C.

Equations

CategoryTheory.CartesianClosed.mk C exp = { closed := fun (X : C) => exp X }

@[reducible, inline]

abbrev CategoryTheory.exp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : C) [Exponentiable A] :

This is (-)^A.

Equations

CategoryTheory.exp A = CategoryTheory.ihom A

@[reducible, inline]

abbrev CategoryTheory.exp.adjunction {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : C) [Exponentiable A] :

MonoidalCategory.tensorLeft A ⊣ exp A

The adjunction between A ⨯ - and (-)^A.

Equations

CategoryTheory.exp.adjunction A = CategoryTheory.ihom.adjunction A

@[reducible, inline]

abbrev CategoryTheory.exp.ev {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : C) [Exponentiable A] :

(exp A).comp (MonoidalCategory.tensorLeft A) ⟶ Functor.id C

The evaluation natural transformation.

Equations

CategoryTheory.exp.ev A = CategoryTheory.ihom.ev A

@[reducible, inline]

abbrev CategoryTheory.exp.coev {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : C) [Exponentiable A] :

Functor.id C ⟶ (MonoidalCategory.tensorLeft A).comp (exp A)

The coevaluation natural transformation.

Equations

CategoryTheory.exp.coev A = CategoryTheory.ihom.coev A

def CategoryTheory.exp.«term_⟹_» :

Lean.TrailingParserDescr

Morphisms obtained using an exponentiable object.

Equations

One or more equations did not get rendered due to their size.

def CategoryTheory.exp.delabPrefunctorObjExp :

Lean.PrettyPrinter.Delaborator.Delab

Delaborator for Prefunctor.obj

Equations

One or more equations did not get rendered due to their size.

def CategoryTheory.exp.«term_^^_» :

Lean.TrailingParserDescr

Morphisms from an exponentiable object.

Equations

One or more equations did not get rendered due to their size.

theorem CategoryTheory.exp.ev_coev {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A B : C) [Exponentiable A] :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A ((coev A).app B)) ((ev A).app (MonoidalCategoryStruct.tensorObj A B)) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj A B)

theorem CategoryTheory.exp.ev_coev_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A B : C) [Exponentiable A] {Z : C} (h : MonoidalCategoryStruct.tensorObj A B ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A ((coev A).app B)) (CategoryStruct.comp ((ev A).app (MonoidalCategoryStruct.tensorObj A B)) h) = h

theorem CategoryTheory.exp.coev_ev {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A B : C) [Exponentiable A] :

CategoryStruct.comp ((coev A).app (inst✝ ⟹ B)) ((exp A).map ((ev A).app B)) = CategoryStruct.id (inst✝ ⟹ B)

theorem CategoryTheory.exp.coev_ev_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A B : C) [Exponentiable A] {Z : C} (h : inst✝ ⟹ B ⟶ Z) :

CategoryStruct.comp ((coev A).app (inst✝ ⟹ B)) (CategoryStruct.comp ((exp A).map ((ev A).app B)) h) = h

instance CategoryTheory.instPreservesColimitsTensorLeft_1 {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : C) [Exponentiable A] :

Limits.PreservesColimits (MonoidalCategory.tensorLeft A)

def CategoryTheory.CartesianClosed.curry {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] :

(MonoidalCategoryStruct.tensorObj A Y ⟶ X) → (Y ⟶ inst✝ ⟹ X)

Currying in a cartesian closed category.

Equations

CategoryTheory.CartesianClosed.curry = ⇑((CategoryTheory.exp.adjunction A).homEquiv Y X)

def CategoryTheory.CartesianClosed.uncurry {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] :

(Y ⟶ inst✝ ⟹ X) → (MonoidalCategoryStruct.tensorObj A Y ⟶ X)

Uncurrying in a cartesian closed category.

Equations

CategoryTheory.CartesianClosed.uncurry = ⇑((CategoryTheory.exp.adjunction A).homEquiv Y X).symm

theorem CategoryTheory.CartesianClosed.homEquiv_apply_eq {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] (f : MonoidalCategoryStruct.tensorObj A Y ⟶ X) :

((exp.adjunction A).homEquiv Y X) f = curry f

theorem CategoryTheory.CartesianClosed.homEquiv_symm_apply_eq {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] (f : Y ⟶ inst✝ ⟹ X) :

((exp.adjunction A).homEquiv Y X).symm f = uncurry f

theorem CategoryTheory.CartesianClosed.curry_natural_left {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X X' Y A : C} [Exponentiable A] (f : X ⟶ X') (g : MonoidalCategoryStruct.tensorObj A X' ⟶ Y) :

curry (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) g) = CategoryStruct.comp f (curry g)

theorem CategoryTheory.CartesianClosed.curry_natural_left_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X X' Y A : C} [Exponentiable A] (f : X ⟶ X') (g : MonoidalCategoryStruct.tensorObj A X' ⟶ Y) {Z : C} (h : inst✝ ⟹ Y ⟶ Z) :

CategoryStruct.comp (curry (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) g)) h = CategoryStruct.comp f (CategoryStruct.comp (curry g) h)

theorem CategoryTheory.CartesianClosed.curry_natural_right {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Y' A : C} [Exponentiable A] (f : MonoidalCategoryStruct.tensorObj A X ⟶ Y) (g : Y ⟶ Y') :

curry (CategoryStruct.comp f g) = CategoryStruct.comp (curry f) ((exp A).map g)

theorem CategoryTheory.CartesianClosed.curry_natural_right_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Y' A : C} [Exponentiable A] (f : MonoidalCategoryStruct.tensorObj A X ⟶ Y) (g : Y ⟶ Y') {Z : C} (h : inst✝ ⟹ Y' ⟶ Z) :

CategoryStruct.comp (curry (CategoryStruct.comp f g)) h = CategoryStruct.comp (curry f) (CategoryStruct.comp ((exp A).map g) h)

theorem CategoryTheory.CartesianClosed.uncurry_natural_right {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Y' A : C} [Exponentiable A] (f : X ⟶ inst✝ ⟹ Y) (g : Y ⟶ Y') :

uncurry (CategoryStruct.comp f ((exp A).map g)) = CategoryStruct.comp (uncurry f) g

theorem CategoryTheory.CartesianClosed.uncurry_natural_right_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Y' A : C} [Exponentiable A] (f : X ⟶ inst✝ ⟹ Y) (g : Y ⟶ Y') {Z : C} (h : Y' ⟶ Z) :

CategoryStruct.comp (uncurry (CategoryStruct.comp f ((exp A).map g))) h = CategoryStruct.comp (uncurry f) (CategoryStruct.comp g h)

theorem CategoryTheory.CartesianClosed.uncurry_natural_left {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X X' Y A : C} [Exponentiable A] (f : X ⟶ X') (g : X' ⟶ inst✝ ⟹ Y) :

uncurry (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) (uncurry g)

theorem CategoryTheory.CartesianClosed.uncurry_natural_left_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X X' Y A : C} [Exponentiable A] (f : X ⟶ X') (g : X' ⟶ inst✝ ⟹ Y) {Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp (uncurry (CategoryStruct.comp f g)) h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) (CategoryStruct.comp (uncurry g) h)

@[simp]

theorem CategoryTheory.CartesianClosed.uncurry_curry {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] (f : MonoidalCategoryStruct.tensorObj A X ⟶ Y) :

uncurry (curry f) = f

@[simp]

theorem CategoryTheory.CartesianClosed.curry_uncurry {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] (f : X ⟶ inst✝ ⟹ Y) :

curry (uncurry f) = f

theorem CategoryTheory.CartesianClosed.curry_eq_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] (f : MonoidalCategoryStruct.tensorObj A Y ⟶ X) (g : Y ⟶ inst✝ ⟹ X) :

curry f = g ↔ f = uncurry g

theorem CategoryTheory.CartesianClosed.eq_curry_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] (f : MonoidalCategoryStruct.tensorObj A Y ⟶ X) (g : Y ⟶ inst✝ ⟹ X) :

g = curry f ↔ uncurry g = f

theorem CategoryTheory.CartesianClosed.uncurry_eq {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] (g : Y ⟶ inst✝ ⟹ X) :

uncurry g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A g) ((exp.ev A).app X)

theorem CategoryTheory.CartesianClosed.curry_eq {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] (g : MonoidalCategoryStruct.tensorObj A Y ⟶ X) :

curry g = CategoryStruct.comp ((exp.coev A).app Y) ((exp A).map g)

theorem CategoryTheory.CartesianClosed.uncurry_id_eq_ev {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A X : C) [Exponentiable A] :

uncurry (CategoryStruct.id (inst✝ ⟹ X)) = (exp.ev A).app X

theorem CategoryTheory.CartesianClosed.curry_id_eq_coev {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A X : C) [Exponentiable A] :

curry (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A ((Functor.id C).obj X))) = (exp.coev A).app X

theorem CategoryTheory.CartesianClosed.curry_injective {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] :

Function.Injective curry

theorem CategoryTheory.CartesianClosed.uncurry_injective {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y A : C} [Exponentiable A] :

Function.Injective uncurry

def CategoryTheory.expUnitNatIso {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [Exponentiable (MonoidalCategoryStruct.tensorUnit C)] :

Functor.id C ≅ exp (MonoidalCategoryStruct.tensorUnit C)

The exponential with the terminal object is naturally isomorphic to the identity. The typeclass argument is explicit: any instance can be used.

Equations

CategoryTheory.expUnitNatIso = CategoryTheory.MonoidalClosed.unitNatIso

def CategoryTheory.expUnitIsoSelf {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X : C} [Exponentiable (MonoidalCategoryStruct.tensorUnit C)] :

inst✝ ⟹ X ≅ X

The exponential of any object with the terminal object is isomorphic to itself, i.e. X^1 ≅ X. The typeclass argument is explicit: any instance can be used.

Equations

CategoryTheory.expUnitIsoSelf = (CategoryTheory.expUnitNatIso.app X).symm

def CategoryTheory.internalizeHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {Y A : C} [Exponentiable A] (f : A ⟶ Y) :

MonoidalCategoryStruct.tensorUnit C ⟶ inst✝ ⟹ Y

The internal element which points at the given morphism.

Equations

One or more equations did not get rendered due to their size.

def CategoryTheory.pre {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A B : C} [Exponentiable A] (f : B ⟶ A) [Exponentiable B] :

exp A ⟶ exp B

Pre-compose an internal hom with an external hom.

Equations

CategoryTheory.pre f = (CategoryTheory.conjugateEquiv (CategoryTheory.exp.adjunction A) (CategoryTheory.exp.adjunction B)) ((CategoryTheory.MonoidalCategory.tensoringLeft C).map f)

theorem CategoryTheory.prod_map_pre_app_comp_ev {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A B : C} [Exponentiable A] (f : B ⟶ A) [Exponentiable B] (X : C) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft B ((pre f).app X)) ((exp.ev B).app X) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (inst✝ ⟹ X)) ((exp.ev A).app X)

theorem CategoryTheory.uncurry_pre {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A B : C} [Exponentiable A] (f : B ⟶ A) [Exponentiable B] (X : C) :

CartesianClosed.uncurry ((pre f).app X) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (inst✝ ⟹ X)) ((exp.ev A).app X)

theorem CategoryTheory.coev_app_comp_pre_app {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X A B : C} [Exponentiable A] (f : B ⟶ A) [Exponentiable B] :

CategoryStruct.comp ((exp.coev A).app X) ((pre f).app (MonoidalCategoryStruct.tensorObj A X)) = CategoryStruct.comp ((exp.coev B).app X) ((exp B).map (MonoidalCategoryStruct.tensorHom f (CategoryStruct.id X)))

@[simp]

theorem CategoryTheory.pre_id {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : C) [Exponentiable A] :

pre (CategoryStruct.id A) = CategoryStruct.id (exp A)

@[simp]

theorem CategoryTheory.pre_map {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A₁ A₂ A₃ : C} [Exponentiable A₁] [Exponentiable A₂] [Exponentiable A₃] (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) :

pre (CategoryStruct.comp f g) = CategoryStruct.comp (pre g) (pre f)

def CategoryTheory.internalHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [CartesianClosed C] :

Functor Cᵒᵖ (Functor C C)

The internal hom functor given by the cartesian closed structure.

Equations

CategoryTheory.internalHom = { obj := fun (X : Cᵒᵖ) => CategoryTheory.exp (Opposite.unop X), map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) => CategoryTheory.pre f.unop, map_id := ⋯, map_comp := ⋯ }

def CategoryTheory.zeroMul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Exponentiable A] {I : C} (t : Limits.IsInitial I) :

MonoidalCategoryStruct.tensorObj A I ≅ I

If an initial object I exists in a CCC, then A ⨯ I ≅ I.

Equations

CategoryTheory.zeroMul t = { hom := CategoryTheory.CartesianMonoidalCategory.snd A I, inv := t.to (CategoryTheory.MonoidalCategoryStruct.tensorObj A I), hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.zeroMul_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Exponentiable A] {I : C} (t : Limits.IsInitial I) :

(zeroMul t).hom = CartesianMonoidalCategory.snd A I

@[simp]

theorem CategoryTheory.zeroMul_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Exponentiable A] {I : C} (t : Limits.IsInitial I) :

(zeroMul t).inv = t.to (MonoidalCategoryStruct.tensorObj A I)

def CategoryTheory.mulZero {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Exponentiable A] [BraidedCategory C] {I : C} (t : Limits.IsInitial I) :

MonoidalCategoryStruct.tensorObj I A ≅ I

If an initial object 0 exists in a CCC, then 0 ⨯ A ≅ 0.

Equations

CategoryTheory.mulZero t = β_ I A ≪≫ CategoryTheory.zeroMul t

def CategoryTheory.powZero {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (B : C) [BraidedCategory C] {I : C} (t : Limits.IsInitial I) [CartesianClosed C] :

inst✝ ⟹ B ≅ MonoidalCategoryStruct.tensorUnit C

If an initial object 0 exists in a CCC then 0^B ≅ 1 for any B.

Equations

One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.prodCoprodDistrib {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [Limits.HasBinaryCoproducts C] [CartesianClosed C] (X Y Z : C) :

MonoidalCategoryStruct.tensorObj Z X ⨿ MonoidalCategoryStruct.tensorObj Z Y ≅ MonoidalCategoryStruct.tensorObj Z (X ⨿ Y)

In a CCC with binary coproducts, the distribution morphism is an isomorphism.

Equations

One or more equations did not get rendered due to their size.

theorem CategoryTheory.strict_initial {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Exponentiable A] {I : C} (t : Limits.IsInitial I) (f : A ⟶ I) :

If an initial object I exists in a CCC then it is a strict initial object, i.e. any morphism to I is an iso. This actually shows a slightly stronger version: any morphism to an initial object from an exponentiable object is an isomorphism.

instance CategoryTheory.to_initial_isIso {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} [Exponentiable A] [Limits.HasInitial C] (f : A ⟶ ⊥_ C) :

theorem CategoryTheory.initial_mono {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {I : C} (B : C) (t : Limits.IsInitial I) [CartesianClosed C] :

Mono (t.to B)

If an initial object 0 exists in a CCC then every morphism from it is monic.

instance CategoryTheory.Initial.mono_to {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [Limits.HasInitial C] (B : C) [CartesianClosed C] :

Mono (Limits.initial.to B)

noncomputable def CategoryTheory.cartesianClosedOfEquiv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [CartesianClosed C] :

CartesianClosed D

Transport the property of being cartesian closed across an equivalence of categories.

Note we didn't require any coherence between the choice of finite products here, since we transport along the prodComparison isomorphism.

Equations

CategoryTheory.cartesianClosedOfEquiv e = CategoryTheory.MonoidalClosed.ofEquiv e.inverse e.symm.toAdjunction