Commit 2020-11-03 15:50 918e28ca
View on Github →feat(category_theory/limits/types): explicit description of equalizers in Type (#4880) Cf https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/concrete.20limits.20in.20Type. Adds equivalent conditions for a fork in Type to be a equalizer, and a proof that the subtype is an equalizer. (cc: @adamtopaz @kbuzzard)