adhesive

Mathlib.CategoryTheory.Adhesive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Type.adhesive

English

The category of types (Type) is adhesive.

Русский

Категория типов (Type) является адгезивной.

LaTeX

$$$\operatorname{Adhesive}(\text{Type }u)$$$

Lean4

instance adhesive : Adhesive (Type u) :=
  ⟨fun {_ _ _ _ f _ _ _ _} H => (IsPushout.isVanKampen_inl _ (Types.isCoprodOfMono f) _ _ _ H.flip).flip⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru