instStrict

Mathlib.CategoryTheory.FiberedCategory.BasedCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.BasedCategory.instStrict

English

The bicategory of BasedCategory 𝒮 is a strict bicategory.

Русский

Бикатегория BasedCategory 𝒮 является строгой бикатегорией.

LaTeX

$$$\\text{Bicategory.Strict}(BasedCategory(𝒮))$$$

Lean4

/-- The bicategory structure on `BasedCategory.{v₂, u₂} 𝒮` is strict. -/
instance : Bicategory.Strict (BasedCategory.{v₂, u₂} 𝒮) where

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

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

Разделы

Аффилиация

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