iso to is_iso for types

Stream: general

[Adam Topaz]

Is the following expected behavior?

import category_theory.types

universe u

variables {X Y : Type u} (f : X ≅ Y)

variables {C : Type*} [category_theory.category C] {A B : C} (g : A ≅ B)

example : category_theory.is_iso g.hom := infer_instance -- ok.

example : category_theory.is_iso f.hom := infer_instance -- fails

[Kevin Buzzard]

The iso symbols have different meanings right? I'm not at lean and haven't got my glasses on so can't see whether the squiggles are the same or not

[Adam Topaz]

Those are both category theory isos

[Kevin Buzzard]

So presumably X and Y are being promoted to terms

[Kevin Buzzard]

I see, and the point is that you can let A and B be those coerced terms and then the typeclass system finds it

[Adam Topaz]

Well, the A and B are terms in a type C (which has a category instance)

[Adam Topaz]

I'm just noting that when you have an isomoprhism e between two objects A and B in an arbitrary category C, then typeclass inference finds the is_iso e.hom instance. But when the category is Type u, this fails.

[Kevin Buzzard]

Oh of course you just let Type u be the category, oh I had completely misunderstood, I should go to bed

[Andrew Yang]

I've met this somewhere else. The thing is that the inference somehow finds (λ x, x) ≫ f.hom defeq to f.hom so it goes into an infinite loop.
using attribute [irreducible] category_theory.types fixes it for me, although I don't know if this causes more problem for you.

[Adam Topaz]

Hmm... That's strange.

I guess another option would be to do some bundling.

[Johan Commelin]

@Andrew Yang nice debug. This is quite a sad failure.

[Floris van Doorn]

This could be solved by setting priorities. Either or both of the following lines solve the issue, and could be added globally in the library:

attribute [instance, priority 900] category_theory.is_iso.comp_is_iso
attribute [instance, priority 1100] category_theory.is_iso.of_iso

[Adam Topaz]

#10276

[Johan Commelin]

Please leave a comment that explains the gist of this thread

[Adam Topaz]

done

[Johan Commelin]

@Adam Topaz I meant in the actual code. I left a suggestion.

[Adam Topaz]

Oh, gotcha