Theorems · Inductive type · category theory

MonCat.Colimits.Relation

{J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → MonCat.Colimits.Prequotient F → MonCat.Colimits.Prequotient F → Prop

The relation on Prequotient saying when two expressions are equal because of the monoid laws, or because one element is mapped to another by a morphism in the diagram.

Defined in

Mathlib.Algebra.Category.MonCat.Colimits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category