Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-05 16:59 83b13d1c

View on Github →

feat(category_theory/limits): morphisms to equalizer (#5233) The natural bijection for morphisms to an equalizer and the dual.

Estimated changes

Modified src/category_theory/limits/shapes/equalizers.lean

added def category_theory.limits.cofork.is_colimit.hom_iso

added theorem category_theory.limits.cofork.is_colimit.hom_iso_natural

added def category_theory.limits.fork.is_limit.hom_iso

added theorem category_theory.limits.fork.is_limit.hom_iso_natural