Reid Barton (May 11 2019 at 00:22):
Some change to mathlib in the last month or so (I don't know which) caused
lean-homotopy-theory to break because Lean now wants to synthesize a
setoid instance on the hom types of
fun_setoid from core, while I want to use a different one. I don't really understand how this is possible; for now I'm working around it by setting an instance priority. But, I am pretty sure that
init/funext.lean) should not be a global instance, just an instance for the scope of the proof of
funext. Maybe that can be changed in 3.5.0?
Last updated: May 09 2021 at 20:11 UTC