mkOfLax'

Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pseudofunctor.mkOfLax'

Lean4

/-- Construct a pseudofunctor from a lax functor whose `mapId` and `mapComp` are isomorphisms. -/
@[simps!]
noncomputable def mkOfLax' (F : LaxFunctor B C) [∀ a, IsIso (F.mapId a)]
    [∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] : Pseudofunctor B C :=
  mkOfLax F
    { mapIdIso := fun a => (asIso (F.mapId a)).symm
      mapCompIso := fun f g => (asIso (F.mapComp f g)).symm }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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