Theorems · Definition · category theory

CategoryTheory.Functor.ColimitTypeRel

{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J (Type w₀)) → (j : J) × F.obj j → (j : J) × F.obj j → Prop

Given F : J ⥤ Type w₀, this is the relation Σ j, F.obj j which generates an equivalence relation such that the quotient identifies to the colimit type of F.

Defined in

Mathlib.CategoryTheory.Limits.Types.ColimitType

Cited by

21 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category