instExponentialIdealSubterminalsSubterminalInclusion

English

In a cartesian closed setting, the subcategory of subterminal objects forms an exponential ideal.

Русский

При наличии кардинально замкнутого произведения подкатегория субтерминальных объектов образует экспоненциальный идеал.

LaTeX

$$$ \\text{ExponentialIdeal} (subterminalInclusion C) $$$

Lean4

/-- The subcategory of subterminal objects is an exponential ideal. -/
instance : ExponentialIdeal (subterminalInclusion C) :=
  by
  apply ExponentialIdeal.mk'
  intro B A
  refine ⟨⟨A ⟹ B.1, fun Z g h => ?_⟩, ⟨Iso.refl _⟩⟩
  exact uncurry_injective (B.2 (CartesianClosed.uncurry g) (CartesianClosed.uncurry h))

Похожие утверждения