Motive not type correct in rw

Stream: general

[Winston Yin]

I'm writing a proof in which something similar to the following situation happens over and over:

import category_theory.closed.monoidal

open opposite
open category_theory

example {V : Type (u+1)} [large_category V]
  [monoidal_category V] [monoidal_closed V] (X : V) :
  (ihom (unop (op X))).map = (ihom X).map :=
begin
  -- rw unop_op, --rewrite tactic failed, motive is not type correct
  refl --succeeds
end

Likewise, simp_rw unop_op, simp only [unop_op] also don't work. I'm not actually proving the above, but rather having many expressions like (ihom (unop (op X))).map or (ihom.ev (unop (op X.V))).app in a more complicated goal. The way I've cheesed it is to do the following:

...
-- goal contains (ihom (unop (op X))).map
have : (ihom (unop (op X))).map = (ihom X).map := rfl,
rw this,
-- goal now contains (ihom X).map instead
...

This kind of thing is very tedious and inelegant, appearing more than 4 times in the same proof. Is there any way to avoid this?

[Kyle Miller]

You can do dsimp here (unop_op is already a rfl simp lemma, so dsimp knows about it). The problem seems to be that ihom has an instance argument (closed) that leads to these motive problems when rw/simp tries to rewrite rather than doing a sequences of rfl proofs.

[Kyle Miller]

The next level of dependent type issues is that "equalities of functors are evil," I think.

Simp would need to be able to generate a lemma like this to be able to navigate down into the argument to map, but it already has some type errors related to the motive issue:

example {C : Type*} [category C] {D : Type*} [category D] {F F' : C ⥤ D} (h : F = F') :
  F.map = F'.map := sorry
/-
14:9: type mismatch at application
  F.map = F'.map
term
  F'.map
has type
  Π {X Y : C}, (X ⟶ Y) → (F'.obj X ⟶ F'.obj Y)
but is expected to have type
  Π {X Y : C}, (X ⟶ Y) → (F.obj X ⟶ F.obj Y)
-/

[Winston Yin]

Would heq be the right thing to use here or no?

[Winston Yin]

dsimp worked in all cases in my proof, thank you!

[Kyle Miller]

By the way, there's a library note about the dsimp, simp pattern

[Kyle Miller]

I'd say avoid heq here since that's going in the direction of equality of objects. Less philosophically, it also seems like it would be difficult to apply (though not impossible).

[Winston Yin]

I had read that before touching the category theory API but now it makes sense

[Junyan Xu]

We use docs#eq_to_hom when we must talk about equality between functors, for example in docs#algebraic_geometry.PresheafedSpace.ext, because simp lemmas tend to work better with eq_to_hom than with heq. (A morphism between presheafed space consists of a morphism of the underlying topological spaces and a morphism of presheaves whose target depends on the morphism of spaces; a presheaf is a functor, so if the morphisms on the spaces agree then you get a non-defeq equality between functors and you have to use eq_to_hom to go between them.)

[Kyle Miller]

docs#category_theory.eq_to_hom

[Kyle Miller]

I'm sure there's a better way to write it, but here's a way to use eq_to_hom to sort of rewrite using unop_op X.

import category_theory.closed.monoidal

open opposite
open category_theory

universes u

example {V : Type (u+1)} [large_category V]
  [monoidal_category V] [monoidal_closed V] (X : V) :
  (ihom (unop (op X))).map = (ihom X).map :=
begin
  ext Y Z f,
  have := (category_theory.eq_to_hom (congr_arg (λ (x : V), ihom x) (unop_op X))).naturality f,
  simp at this,
  exact this,
end

[Kevin Buzzard]

Does simpa golf it?

[Kyle Miller]

Yeah, I just didn't want to make it seem like simpa was doing anything to the goal.

[Adam Topaz]

(deleted)