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