# Zulip Chat Archive

## Stream: general

### Topic: Motive not type correct in rw

#### Winston Yin (Jul 22 2022 at 19:42):

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 (Jul 22 2022 at 19:48):

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 (Jul 22 2022 at 20:04):

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 (Jul 22 2022 at 20:39):

Would `heq`

be the right thing to use here or no?

#### Winston Yin (Jul 22 2022 at 20:45):

`dsimp`

worked in all cases in my proof, thank you!

#### Kyle Miller (Jul 22 2022 at 20:47):

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

pattern

#### Kyle Miller (Jul 22 2022 at 20:49):

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 (Jul 22 2022 at 20:49):

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

#### Junyan Xu (Jul 22 2022 at 21:41):

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 (Jul 22 2022 at 21:43):

docs#category_theory.eq_to_hom

#### Kyle Miller (Jul 22 2022 at 21:50):

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 (Jul 22 2022 at 22:34):

Does `simpa`

golf it?

#### Kyle Miller (Jul 22 2022 at 22:46):

Yeah, I just didn't want to make it seem like `simpa`

was doing anything to the goal.

#### Adam Topaz (Jul 23 2022 at 01:29):

(deleted)

Last updated: Dec 20 2023 at 11:08 UTC