witness

Mathlib.CategoryTheory.UnivLE

URI: https://scilib.ai/kg/mathlib#UnivLE.witness

English

Equivalences between types are the same as isomorphisms of types.

Русский

Эквиваленции между типами совпадают с изоморфизмами типов.

LaTeX

$$$ \\mathrm{equivIsoIso} : X \\equiv Y \\;\\cong\\; X \\cong Y $$$

Lean4

def witness [UnivLE.{max u v, v}] : Type u ⥤ Type v :=
  uliftFunctor.{v, u} ⋙ (uliftFunctor.{u, v}).inv

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

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

Разделы

Аффилиация

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