Def CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCoconeIsColimit

Modification history

2023-03-08 06:41

Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean

feat: port CategoryTheory.Limits.Constructions.Equalizers (#2700)

Added CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCoconeIsColimit View on Github →