Cartesian closed categories #
Given a category with finite products, the cartesian monoidal structure is provided by the local
instance monoidalOfHasFiniteProducts.
We define exponentiable objects to be closed objects with respect to this monoidal structure,
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.
TODO #
Some of the results here are true more generally for closed objects and for closed monoidal categories, and these could be generalised.
@[inline, reducible]
abbrev
CategoryTheory.Exponentiable
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts 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.
Instances For
def
CategoryTheory.binaryProductExponentiable
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
{X : C}
{Y : C}
(hX : CategoryTheory.Exponentiable X)
(hY : CategoryTheory.Exponentiable 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.
Instances For
def
CategoryTheory.terminalExponentiable
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts 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.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.CartesianClosed
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts 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 monoidal_closed with respect to the cartesian monoidal structure.
Instances For
def
CategoryTheory.CartesianClosed.mk
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
(h : (X : C) → CategoryTheory.IsLeftAdjoint (CategoryTheory.MonoidalCategory.tensorLeft X))
:
Constructor for CartesianClosed C.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.exp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
This is (-)^A.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.exp.adjunction
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
CategoryTheory.Limits.prod.functor.obj A ⊣ CategoryTheory.exp A
The adjunction between A ⨯ - and (-)^A.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.exp.ev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
CategoryTheory.Functor.comp (CategoryTheory.exp A) (CategoryTheory.Limits.prod.functor.obj A) ⟶ CategoryTheory.Functor.id C
The evaluation natural transformation.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.exp.coev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
CategoryTheory.Functor.id C ⟶ CategoryTheory.Functor.comp (CategoryTheory.Limits.prod.functor.obj A) (CategoryTheory.exp A)
The coevaluation natural transformation.
Instances For
theorem
CategoryTheory.exp.ev_coev_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
(B : C)
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
{Z : C}
(h : (CategoryTheory.Functor.id C).obj (A ⨯ B) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id A) ((CategoryTheory.exp.coev A).app B))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.ev A).app (A ⨯ B)) h) = h
@[simp]
theorem
CategoryTheory.exp.ev_coev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
(B : C)
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id A) ((CategoryTheory.exp.coev A).app B))
((CategoryTheory.exp.ev A).app (A ⨯ B)) = CategoryTheory.CategoryStruct.id (A ⨯ B)
theorem
CategoryTheory.exp.coev_ev_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
(B : C)
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
{Z : C}
(h : A ⟹ (CategoryTheory.Functor.id C).obj B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev A).app (A ⟹ B))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp A).map ((CategoryTheory.exp.ev A).app B)) h) = h
@[simp]
theorem
CategoryTheory.exp.coev_ev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
(B : C)
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev A).app (A ⟹ B))
((CategoryTheory.exp A).map ((CategoryTheory.exp.ev A).app B)) = CategoryTheory.CategoryStruct.id (A ⟹ B)
instance
CategoryTheory.instPreservesColimitsObjToQuiverToCategoryStructFunctorToQuiverToCategoryStructCategoryToPrefunctorFunctor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(A : C)
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
CategoryTheory.Limits.PreservesColimits (CategoryTheory.Limits.prod.functor.obj A)
def
CategoryTheory.CartesianClosed.curry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
Currying in a cartesian closed category.
Instances For
def
CategoryTheory.CartesianClosed.uncurry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
Uncurrying in a cartesian closed category.
Instances For
@[simp]
theorem
CategoryTheory.CartesianClosed.homEquiv_apply_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : A ⨯ Y ⟶ X)
:
@[simp]
theorem
CategoryTheory.CartesianClosed.homEquiv_symm_apply_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : Y ⟶ A ⟹ X)
:
theorem
CategoryTheory.CartesianClosed.curry_natural_left_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{X' : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : X ⟶ X')
(g : A ⨯ X' ⟶ Y)
{Z : C}
(h : A ⟹ Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CartesianClosed.curry
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id A) f) g))
h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianClosed.curry g) h)
theorem
CategoryTheory.CartesianClosed.curry_natural_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{X' : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : X ⟶ X')
(g : A ⨯ X' ⟶ Y)
:
theorem
CategoryTheory.CartesianClosed.curry_natural_right_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
{Y' : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : A ⨯ X ⟶ Y)
(g : Y ⟶ Y')
{Z : C}
(h : A ⟹ Y' ⟶ Z)
:
theorem
CategoryTheory.CartesianClosed.curry_natural_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
{Y' : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : A ⨯ X ⟶ Y)
(g : Y ⟶ Y')
:
theorem
CategoryTheory.CartesianClosed.uncurry_natural_right_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
{Y' : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : X ⟶ A ⟹ Y)
(g : Y ⟶ Y')
{Z : C}
(h : Y' ⟶ Z)
:
theorem
CategoryTheory.CartesianClosed.uncurry_natural_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
{Y' : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : X ⟶ A ⟹ Y)
(g : Y ⟶ Y')
:
theorem
CategoryTheory.CartesianClosed.uncurry_natural_left_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{X' : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : X ⟶ X')
(g : X' ⟶ A ⟹ Y)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianClosed.uncurry (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id A) f)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianClosed.uncurry g) h)
theorem
CategoryTheory.CartesianClosed.uncurry_natural_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{X' : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : X ⟶ X')
(g : X' ⟶ A ⟹ Y)
:
@[simp]
theorem
CategoryTheory.CartesianClosed.uncurry_curry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : A ⨯ X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.CartesianClosed.curry_uncurry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : X ⟶ A ⟹ Y)
:
theorem
CategoryTheory.CartesianClosed.curry_eq_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : A ⨯ Y ⟶ X)
(g : Y ⟶ A ⟹ X)
:
theorem
CategoryTheory.CartesianClosed.eq_curry_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : A ⨯ Y ⟶ X)
(g : Y ⟶ A ⟹ X)
:
theorem
CategoryTheory.CartesianClosed.uncurry_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(g : Y ⟶ A ⟹ X)
:
theorem
CategoryTheory.CartesianClosed.curry_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(g : A ⨯ Y ⟶ X)
:
CategoryTheory.CartesianClosed.curry g = CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev A).app Y) ((CategoryTheory.exp A).map g)
theorem
CategoryTheory.CartesianClosed.uncurry_id_eq_ev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
(A : C)
(X : C)
[CategoryTheory.Exponentiable A]
:
CategoryTheory.CartesianClosed.uncurry (CategoryTheory.CategoryStruct.id (A ⟹ X)) = (CategoryTheory.exp.ev A).app X
theorem
CategoryTheory.CartesianClosed.curry_id_eq_coev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
(A : C)
(X : C)
[CategoryTheory.Exponentiable A]
:
CategoryTheory.CartesianClosed.curry (CategoryTheory.CategoryStruct.id (A ⨯ (CategoryTheory.Functor.id C).obj X)) = (CategoryTheory.exp.coev A).app X
theorem
CategoryTheory.CartesianClosed.curry_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
Function.Injective CategoryTheory.CartesianClosed.curry
theorem
CategoryTheory.CartesianClosed.uncurry_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
:
Function.Injective CategoryTheory.CartesianClosed.uncurry
def
CategoryTheory.expTerminalIsoSelf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable (⊤_ C)]
:
Show that the exponential of the terminal object is isomorphic to itself, i.e. X^1 ≅ X.
The typeclass argument is explicit: any instance can be used.
Instances For
def
CategoryTheory.internalizeHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{Y : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : A ⟶ Y)
:
The internal element which points at the given morphism.
Instances For
def
CategoryTheory.pre
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : B ⟶ A)
[CategoryTheory.Exponentiable B]
:
Pre-compose an internal hom with an external hom.
Instances For
theorem
CategoryTheory.prod_map_pre_app_comp_ev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : B ⟶ A)
[CategoryTheory.Exponentiable B]
(X : C)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id B) ((CategoryTheory.pre f).app X))
((CategoryTheory.exp.ev B).app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (A ⟹ X)))
((CategoryTheory.exp.ev A).app X)
theorem
CategoryTheory.uncurry_pre
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : B ⟶ A)
[CategoryTheory.Exponentiable B]
(X : C)
:
CategoryTheory.CartesianClosed.uncurry ((CategoryTheory.pre f).app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (A ⟹ X)))
((CategoryTheory.exp.ev A).app X)
theorem
CategoryTheory.coev_app_comp_pre_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
{X : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
(f : B ⟶ A)
[CategoryTheory.Exponentiable B]
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev A).app X) ((CategoryTheory.pre f).app (A ⨯ X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev B).app X)
((CategoryTheory.exp B).map (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id X)))
@[simp]
@[simp]
theorem
CategoryTheory.pre_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
{A₁ : C}
{A₂ : C}
{A₃ : C}
[CategoryTheory.Exponentiable A₁]
[CategoryTheory.Exponentiable A₂]
[CategoryTheory.Exponentiable A₃]
(f : A₁ ⟶ A₂)
(g : A₂ ⟶ A₃)
:
def
CategoryTheory.internalHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.CartesianClosed C]
:
The internal hom functor given by the cartesian closed structure.
Instances For
@[simp]
theorem
CategoryTheory.zeroMul_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
{I : C}
(t : CategoryTheory.Limits.IsInitial I)
:
(CategoryTheory.zeroMul t).inv = CategoryTheory.Limits.IsInitial.to t (A ⨯ I)
@[simp]
theorem
CategoryTheory.zeroMul_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
{I : C}
(t : CategoryTheory.Limits.IsInitial I)
:
(CategoryTheory.zeroMul t).hom = CategoryTheory.Limits.prod.snd
def
CategoryTheory.zeroMul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
{I : C}
(t : CategoryTheory.Limits.IsInitial I)
:
If an initial object I exists in a CCC, then A ⨯ I ≅ I.
Instances For
def
CategoryTheory.mulZero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
{I : C}
(t : CategoryTheory.Limits.IsInitial I)
:
If an initial object 0 exists in a CCC, then 0 ⨯ A ≅ 0.
Instances For
def
CategoryTheory.powZero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(B : C)
[CategoryTheory.Limits.HasFiniteProducts C]
{I : C}
(t : CategoryTheory.Limits.IsInitial I)
[CategoryTheory.CartesianClosed C]
:
If an initial object 0 exists in a CCC then 0^B ≅ 1 for any B.
Instances For
def
CategoryTheory.prodCoprodDistrib
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Limits.HasBinaryCoproducts C]
[CategoryTheory.CartesianClosed C]
(X : C)
(Y : C)
(Z : C)
:
In a CCC with binary coproducts, the distribution morphism is an isomorphism.
Instances For
theorem
CategoryTheory.strict_initial
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
{I : C}
(t : CategoryTheory.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}
[CategoryTheory.Category.{v, u} C]
{A : C}
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Exponentiable A]
[CategoryTheory.Limits.HasInitial C]
(f : A ⟶ ⊥_ C)
:
theorem
CategoryTheory.initial_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
{I : C}
(B : C)
(t : CategoryTheory.Limits.IsInitial I)
[CategoryTheory.CartesianClosed C]
:
If an initial object 0 exists in a CCC then every morphism from it is monic.
def
CategoryTheory.cartesianClosedOfEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasFiniteProducts C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
[CategoryTheory.Limits.HasFiniteProducts D]
(e : C ≌ D)
[h : CategoryTheory.CartesianClosed C]
:
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.