ιColimitType_eq_iff — Mathlib

English

Let F be a functor from a category J to Types. For elements x ∈ F(j) and y ∈ F(j'), the equality of their images in the colimit type is equivalent to them being related by the equivalence relation generated by the ColimitTypeRel associated to F.

Русский

Пусть F : J ⥤ Type является функтором. Для элементов x ∈ F(j) и y ∈ F(j') равенство их изображений в типе колимита эквивалентно тому, что пары ⟨j, x⟩ и ⟨j', y⟩ эквивалентны относительно отношения, порождаемого F.ColimitTypeRel.

LaTeX

$$$ F.\iotaColimitType j x = F.\iotaColimitType j' y \iff \operatorname{Relation.EqvGen} F.ColimitTypeRel \langle j, x \rangle \langle j', y \rangle $$$

Lean4

theorem ιColimitType_eq_iff {j j' : J} (x : F.obj j) (y : F.obj j') :
    F.ιColimitType j x = F.ιColimitType j' y ↔ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩ :=
  Quot.eq

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