Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.types_id

Modification history

2020-04-11 09:58
src/category_theory/types.lean
chore(category_theory/types): add documentation, remove bad simp lemmas and instances, add notation for functions as morphisms (#2383) …
Modified category_theory.types_idView on Github →
2019-09-17 15:50
src/category_theory/types.lean
fix(category_theory): require morphisms are in Type, again (#1412) …
Modified category_theory.types_idView on Github →
2019-05-23 13:50
src/category_theory/types.lean
chore(CommRing/adjunctions): refactor proofs (#1049) …
Modified category_theory.types_idView on Github →
2019-04-01 16:13
src/category_theory/types.lean
feat(category_theory): working in Sort rather than Type (#824)
Modified category_theory.types_idView on Github →
2018-08-18 00:55
category_theory/types.lean
feat(category_theory): opposites, and the category of types (#249)
Added category_theory.types_idView on Github →