monoCoprodType — Mathlib

English

The category of types carries a canonical MonoCoprod structure: left injection into a binary coproduct of types is mono.

Русский

Категория типов имеет каноническую структуру MonoCoprod: левое инъектное отображение в бинарный coproduct типов моно.

LaTeX

$$$\\text{MonoCoprod}(\\mathsf{Type}_u)$$$

Lean4

instance monoCoprodType : MonoCoprod (Type u) :=
  MonoCoprod.mk' fun A B => by
    refine ⟨BinaryCofan.mk (Sum.inl : A ⟶ A ⊕ B) Sum.inr, ?_, ?_⟩
    ·
      exact
        BinaryCofan.IsColimit.mk _
          (fun f₁ f₂ x => by
            rcases x with x | x
            exacts [f₁ x, f₂ x])
          (fun f₁ f₂ => by rfl) (fun f₁ f₂ => by rfl)
          (fun f₁ f₂ m h₁ h₂ => by
            funext x
            rcases x with x | x
            · exact congr_fun h₁ x
            · exact congr_fun h₂ x)
    · rw [mono_iff_injective]
      intro a₁ a₂ h
      simpa using h

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