instSplitEpiCategoryType — Mathlib

English

The category of Type u is a SplitEpiCategory: every epi between types splits.

Русский

Категория типов Type u является SplitEpiCategory: каждый эпи-морфизм между типами разворачивается.

LaTeX

$$$ \\text{SplitEpiCategory}(\\text{Type } u) $$$

Lean4

instance : SplitEpiCategory (Type u) where
  isSplitEpi_of_epi f
    hf :=
    IsSplitEpi.mk' <|
      { section_ := Function.surjInv <| (epi_iff_surjective f).1 hf
        id := funext <| Function.rightInverse_surjInv <| (epi_iff_surjective f).1 hf }

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