Zulip Chat Archive

Stream: general

Topic: to instance or not to instance

Johan Commelin (Oct 26 2021 at 12:24):

Clearly, the following instances form a loop together. Do we have design principles that dictate which should be instance and which should be lemma?

instance {f g : arrow T} (ff : f  g) [is_iso ff.left] [is_iso ff.right] :
  is_iso ff :=
{ out := ⟨⟨inv ff.left, inv ff.right⟩,
          by { ext; dsimp; simp only [is_iso.hom_inv_id] },
          by { ext; dsimp; simp only [is_iso.inv_hom_id] }⟩ }

instance left_is_iso [is_iso sq] : is_iso sq.left :=
{ out := ⟨(inv sq).left, by simp only [ comma.comp_left, is_iso.hom_inv_id, is_iso.inv_hom_id,
    arrow.id_left, eq_self_iff_true, and_self]⟩ }

instance right_is_iso [is_iso sq] : is_iso sq.right :=
{ out := ⟨(inv sq).right, by simp only [ comma.comp_right, is_iso.hom_inv_id, is_iso.inv_hom_id,
    arrow.id_right, eq_self_iff_true, and_self]⟩ }

Gabriel Ebner (Oct 26 2021 at 12:27):

The first one should not be an instance because it loops (at least as far as I can see the types).

Johan Commelin (Oct 26 2021 at 12:28):

The first one alone doesn't loop, right?

Johan Commelin (Oct 26 2021 at 12:29):

But it's somehow an "extensionality instance" if that makes sense. Maybe those are "bad"? Can/should we lint against those?

Gabriel Ebner (Oct 26 2021 at 12:33):

Ah, because ff.left is no longer a morphism between objects in an arrow.

Johan Commelin (Oct 26 2021 at 12:36):

Or at least, if it is, then in a different category. (If you start with f g : arrow (arrow T))

Reid Barton (Oct 26 2021 at 12:49):

Ideally is_iso would not exist as a class at all (there are a lot of ways to prove that a map is an isomorphism and many of them are not "syntactic"). However, the loop-breaking rule is generally that the instance head(s) should get smaller when you apply an instance.

Johan Commelin (Oct 26 2021 at 12:59):

Which in thise case means that nr1 should not be an instance, and the other two are fine, right?

Last updated: Aug 03 2023 at 10:10 UTC