Rewriting in slice categories

Stream: maths

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

When proving various facts about over categories, I got myself into the following instance of DTT hell. In this situation, none of the tactics I tried (simp, simp_rw, rw, cases h) can eliminate h. I am able to prove it by writing a motive by hand, however. I am wondering if anybody has an idea of some other piece of automation I could try here.

 axiom C : Type
axiom Hom : C → C → Type
axiom comp {X Y Z : C} : Hom X Y → Hom Y Z → Hom X Z

structure Over (X : C) : Type where
  left : C
  hom : Hom left X

structure OverHom {X : C} (U V : Over X) : Type where
  left : Hom U.left V.left
  w : comp left V.hom = U.hom

def homMk {X : C} (U V : Over X) (f : Hom U.left V.left) (w : comp f V.hom = U.hom) : OverHom U V :=
  OverHom.mk f w

example (A X : C) (f : Over A) (x : (b : Hom X A) × (OverHom (Over.mk _ b) f))
    (h : comp x.2.left f.hom = x.1) :
    HEq (homMk (Over.mk _ (comp x.2.left f.hom)) f x.2.left rfl) x.2 := by
  -- rw [h]; simp_rw [h]; simp only [h]
  -- cases x; cases h
  refine Eq.rec (motive :=
    fun a h' =>
      @HEq
        (OverHom (Over.mk _ a) f)
        (homMk (Over.mk _ a) (f) x.2.left (h' ▸ h))
        (OverHom (Over.mk _ x.1) f)
        x.2
    )
    ?_
    h.symm
  rfl

[Aaron Liu]

My rw! tactic that I made a while ago (see #metaprogramming / tactics > dependent rewrite tactic , but I updated it) works here, but it's not in any public repository yet

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ooh this is awesome, I was just about to write that same tactic!

[Joël Riou]

Using HEq in category theory is probably a bad idea. The better solution is to use a composition with a suitable isomorphism (this can be done using docs#CategoryTheory.eqToHom) in order to get matching source and target of morphisms.

[Kyle Miller]

example (A X : C) (f : Over A) (x : (b : Hom X A) × (OverHom (Over.mk _ b) f)) :
--    (h : comp x.2.left f.hom = x.1) :
    HEq (homMk (Over.mk _ (comp x.2.left f.hom)) f x.2.left rfl) x.2 := by
  obtain ⟨_, g, h⟩ := x
  dsimp at g h
  cases h
  rfl