Def category_theory.has_forget₂.mk'
Modification history
2023-06-30 04:04
src/category_theory/concrete_category/basic.lean
chore(category_theory/concrete_category): reorder universes (#19222) …
Modified category_theory.has_forget₂.mk'View on Github →2021-01-14 08:39
src/category_theory/concrete_category/basic.lean
chore(*): split some long lines (#5742)
Modified category_theory.has_forget₂.mk'View on Github →2020-09-01 12:18
src/category_theory/concrete_category/basic.lean
refactor(algebra/category/*, category_theory/concrete_category): generalize universes for concrete categories (#3687) …
Modified category_theory.has_forget₂.mk'View on Github →