instFullCatTypeToCat

Mathlib.CategoryTheory.Category.Cat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instFullCatTypeToCat

← MathLib Explorer

English

The functor typeToCat is full, in addition to being faithful.

Русский

Функтор TypeToCat полон (full).

LaTeX

$$$$\\text{Full}(\\text{typeToCat}).$$$$

Lean4

instance : Functor.Full typeToCat.{u} where
  map_surjective
    F :=
    ⟨Discrete.as ∘ F.obj ∘ Discrete.mk, by
      apply Functor.ext
      · intro x y f
        dsimp
        apply ULift.ext
        cat_disch
      · rintro ⟨x⟩
        apply Discrete.ext
        rfl⟩

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

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

Разделы

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

Аффилиация

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