fun_setoid

Stream: general

[Reid Barton]

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 Top using subtype.setoid and 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 fun_setoid (in 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?