Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-30 11:48 afe51c76

View on Github →

feat(category_theory/limits): special shapes (#1339)

  • providing minimal API for limits of special shapes
  • apis for special shapes
  • fintype instances
  • associators, unitors, braidings for binary product
  • map
  • instances
  • assoc lemma
  • coprod
  • fix import
  • names
  • adding some docs
  • updating tutorial on limits
  • minor
  • uniqueness of morphisms to terminal object
  • better treatment of has_terminal
  • various
  • not there yet
  • deleting a dumb file
  • remove constructions for a later PR
  • use @[reassoc]
  • Update src/category_theory/limits/shapes/finite_products.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • improving the colimits tutorial
  • minor
  • notation for prod_obj and sigma_obj.
  • reverting to condition
  • implicit arguments
  • more implicit arguments
  • minor
  • notational for initial and terminal objects
  • various
  • fix notation priorities
  • remove unused case bash tactic
  • fix whitespace
  • comment
  • notations

Estimated changes

deleted def I_0
deleted def I_1
added def I₀
added def I₁
modified def X
modified def Y
modified def cylinder
deleted def cylinder_0
deleted def cylinder_1
added def cylinder₀
added def cylinder₁
deleted def d
modified def mapping_cone
modified def mapping_cylinder
deleted def mapping_cylinder_0
deleted def w