monoidColimitType — Mathlib

English

An instance provides a monoid structure on the colimit type for a diagram F: J ⥤ MonCat.

Русский

Для диаграммы F: J ⥤ MonCat существует моноидная структура на ColimitType F.

LaTeX

$$$\text{MonCat.Colimits.monoidColimitType}(F) \text{ is a Monoid.}$$$

Lean4

instance monoidColimitType : Monoid (ColimitType F)
    where
  one := Quotient.mk _ one
  mul := Quotient.map₂ mul fun _ x' rx y _ ry => Setoid.trans (Relation.mul_1 _ _ y rx) (Relation.mul_2 x' _ _ ry)
  one_mul := Quotient.ind fun _ => Quotient.sound <| Relation.one_mul _
  mul_one := Quotient.ind fun _ => Quotient.sound <| Relation.mul_one _
  mul_assoc := Quotient.ind fun _ => Quotient.ind₂ fun _ _ => Quotient.sound <| Relation.mul_assoc _ _ _

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