A simple heterogenous equality pb

Stream: new members

[Nicolas Rolland]

Hi,

I would like to prove the following simple lemma, but I can't manage what to do here.
Here is the code

import Mathlib.CategoryTheory.EqToHom
import Mathlib.CategoryTheory.Functor.Const

open CategoryTheory

universe v₁ vm u₁ u um
variable {J : Type u₁} [Category.{v₁} J]
variable {M : Type um } [Category.{vm} M]
variable {F G H: J ⥤ M} (α : F ⟶ G) (β : G ⟶ H)


@[ext]
structure MyCone  (F : J ⥤ M) where
  pt : M
  π : (Functor.const J).obj pt ⟶ F

structure MyConeMorphism   (x y : MyCone F) where
  hom : x.pt ⟶ y.pt

instance : Category (MyCone F) where
  Hom x y:=  MyConeMorphism x y
  id x := { hom := 𝟙 x.pt }
  comp f g := { hom := f.hom ≫ g.hom }

def pc (α : F ⟶ G) : MyCone F ⥤ MyCone G  where
  obj c :=  {pt := c.pt, π := c.π  ≫ α }
  map {X Y} m := { hom := m.hom }

def eqobj  (x : MyCone F):
    (((pc (α ≫ β)).obj x)) =  ((pc α ⋙ pc β).obj x) :=
  MyCone.ext rfl (by simp;exact (Category.assoc _ _ _).symm)

---------------------------------------------------------------------
-- We want (pc (α ≫ β)).map m  = (pc α ⋙ pc β).map m
-- but that's not type correct, so we need instead

def howToGetThat? (x y : MyCone F) (m : x ⟶ y) :
   eqToHom (eqobj _ _ x ) ≫ ((pc α ⋙ pc β).map m) = ((pc (α ≫ β)).map m ≫ eqToHom (eqobj _ _ y))
   :=  sorry

I don't know how to get that, although it looks quite simple...

PS : with some "bounded definitional equality", it would be easy as both side have the same definition..

---------------------------------------------------------------------
def eq1 (x y: MyCone F) (m : x ⟶ y) :
  (pc (α ≫ β)).map m = { hom := m.hom }  := rfl

def eq2 (x y: MyCone F) (m : x ⟶ y) :
   (pc α ⋙ pc β).map m = { hom := m.hom }  := rfl

[Giacomo Stevanato]

You could use heterogeneous equality:

def howToGetThat? (x y : MyCone F) (m : x ⟶ y) : HEq ((pc (α ≫ β)).map m) ((pc α ⋙ pc β).map m)
  := sorry

or alternatively prove the equality of the two types involved and use that to cast one of the two sides of the equality

def howToGetThat? (x y : MyCone F) (m : x ⟶ y) : (pc (α ≫ β)).map m = cast (by simp[eqobj]) ((pc α ⋙ pc β).map m)
  := sorry

[Nicolas Rolland]

I think those are equivalent questions. I wonder how to prove any of those.

[Eric Wieser]

Don't these fall into "equality of objects is evil"?

[Nicolas Rolland]

There might be some categorical interpretation under which this falls under "evil" (grounded or not..)

But this is more a math or Lean question : The 2 definitions reduce to identical expressions, which differ only in type. And we have a proof that those types are equal.

So I would expect some way of proving that they are HEq / castable / Eq with the eqToHoms.
Using HEq for instance I think it reduces to this example.

example (x y: MyCone F) (m : x ⟶ y) :
  HEq ({ hom := m.hom } : (pc (α ≫ β)).obj x ⟶ (pc (α ≫ β)).obj y )
     ({ hom := m.hom } : (pc α ⋙ pc β).obj x ⟶ (pc α ⋙ pc β).obj y) := by
     sorry