## 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: Aug 03 2023 at 10:10 UTC