Commit 2018-09-24 08:48 cbfe372d
View on Github →fix(category_theory/functor): make obj_eq_coe a rfl-lemma
This is needed to, for example, let dsimp turn 𝟙 (F.obj X) into 𝟙 (F X).
fix(category_theory/functor): make obj_eq_coe a rfl-lemma
This is needed to, for example, let dsimp turn 𝟙 (F.obj X) into 𝟙 (F X).