Bundled `equiv.symm`

Stream: general

[Anne Baanen]

Since fun_like seems to work out well, why not do the same for equivs? Well, it turns out it's hard to correctly deal with the symm maps. But after a couple days of tinkering, I think I have the solution: the symm maps should be bundled morphisms!

For example:

/-- A `symm_fun E E'` sends a bundled morphism in `E` to its two-sided inverse in `E'` -/
structure symm_fun (E E' : Sort*) {A B : Sort*}
  [fun_like E A (λ _, B)] [fun_like E' B (λ _, A)] :=
(to_fun : E → E')
(symm_apply_apply' : ∀ (e : E) (x : A), to_fun e (e x) = x)
(apply_symm_apply' : ∀ (e : E) (x : B), e (to_fun e x) = x)

...

protected def equiv.symm : symm_fun (α ≃ β) (β ≃ α) :=
{ to_fun := λ e, ⟨e.inv_fun, e.to_fun, e.right_inv, e.left_inv⟩,
  symm_apply_apply' := λ e x, e.left_inv x,
  apply_symm_apply' := λ e x, e.right_inv x }

notation e `⁻¹ₑ`:1035 := equiv.symm e

theorem apply_eq_iff_eq_symm_apply {α β : Sort*} (f : α ≃ β) {x : α} {y : β} :
  f x = y ↔ x = f⁻¹ₑ y :=
equiv.symm.apply_eq_iff_eq_symm_apply f

-- Copy over the lemmas to the `equiv` namespace for now, can be deleted later:
lemma symm_apply_eq {α β} (e : α ≃ β) {x y} : e⁻¹ₑ x = y ↔ x = e y := symm_fun.symm_apply_eq _ _
lemma eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e⁻¹ₑ x ↔ e y = x := symm_fun.eq_symm_apply _ _
theorem symm_symm (e : α ≃ β) : e.symm.symm = e := symm_fun.symm_symm _ _ _

(Full code on branch#bundled-refl-symm-trans)

The main drawback is that parsing of e.symm x is too hard since it has to insert two coe_fns to resolve the dot notation correctly. My proposed solution is to add the e ⁻¹ₑ notation as in the code sample.

What do you think? Have the bundled morphisms gone to my head?

[Anne Baanen]

Thanks to @Yaël Dillies and @Eric Wieser for pushing me to do ... whatever this is.

[Yakov Pechersky]

Doesn't this prevent e.symm.symm = e from being rfl later, once eta expansion for defeq hits?

[Yury G. Kudryashov]

e.symm.symm = e is not rfl unless you coerce both sides to functions.

[Yury G. Kudryashov]

I think that we should have some kind of concrete category theory on top of fun_like.

[Yury G. Kudryashov]

Something like

class fun_like.has_id {A B F : Type*} [fun_like F A (λ _, B)] :=
(id : F)
(id_apply : ∀ a : A, id a = a)

[Anne Baanen]

You mean:

/-- The class `has_id F A` states the bundled `A`-endomorphisms of type `I` include an
identity map `has_id.id`. -/
class has_id (I : Sort u) (A : out_param $ Sort v) [fun_like I A (λ _, A)] : Type u :=
(id [] : I) (id_apply [] : ∀ x, id x = x)

namespace has_id

variables (I : Sort*) {A : Sort*} [fun_like I A (λ _, A)] [i : has_id I A]
include i

@[simp] lemma coe : coe_fn (id I) = _root_.id := funext (id_apply I)

end has_id

:)

[Yury G. Kudryashov]

What if symm becomes a typeclass (defined as your structure but E' is an out_param)?

[Yury G. Kudryashov]

Then we can have has_symm.

[Anne Baanen]

I tried that, but equiv being Sort-typed makes the universe params slightly too hard to infer:

type mismatch at application
  has_id.id (α ≃ α)
term
  α ≃ α
has type
  Sort (max 1 u) : Type (max 1 u)
but is expected to have type
  Sort (max 1 (imax ? ?) (imax ? ?)) : Type (max 1 (imax ? ?) (imax ? ?))

[Anne Baanen]

(The details of the error depend on whether I choose Type u or Sort u for has_id, but the error remains.)

[Yury G. Kudryashov]

I forgot about Sort

[Anne Baanen]

Yury G. Kudryashov said:

What if symm becomes a typeclass (defined as your structure but E' is an out_param)?

This might work, I haven't looked into it too much because there's a _root_.symm confusing matters and I don't feel like manually replacing all the usages of e.symm with (symm e).

[Anne Baanen]

I also tried a class as a predicate on equiv.symm, but that's too hard to infer (and doesn't work with simp) for basically the same reason as is_ring_hom is too hard.

[Yury G. Kudryashov]

Idea for the future: make e.abc look in fun_like.abc if @{some_attr fun_like] def e_type := ..., e : e_type.