Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-14 20:14 2065438d

View on Github →

feat(category_theory/comma): some limits in the over category and iterated slices (#2131)

  • iterated slice and limits in over category
  • A bit more docs
  • changes from review
  • removed simp attributes
  • over prod map left
  • Update src/category_theory/comma.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • simplify equivalence definition
  • fix indentation
  • make lemmas simp again
  • removed simp
  • fix equalizers proof

Estimated changes