Mapping functions over equality of functor compositions

Stream: Is there code for X?

[Slavomir Kaslev]

Is there a way to prove the equality want, given an equality between composition of functors:

import Mathlib.CategoryTheory.Functor.Basic

open CategoryTheory

variable {A : Type} [Category A]
variable {B : Type} [Category B]
variable {C : Type} [Category C]
variable {D : Type} [Category D]
variable {P : A ⥤ B} {Q : B ⥤ D}
variable {R : A ⥤ C} {S : C ⥤ D}
variable (h : P ⋙ Q = R ⋙ S)

def want {x y : A} (f : x ⟶ y) : Eq ((P ⋙ Q).map f) ((R ⋙ S).map f) := sorry

def good : (P ⋙ Q).obj = (R ⋙ S).obj := by funext; congr
def ok (x) : (P ⋙ Q).obj x = (R ⋙ S).obj x := by congr
def hok {x y : A} (f : x ⟶ y) : HEq ((P ⋙ Q).map f) ((R ⋙ S).map f) := by rw [h]
def hmm {x y : A} {f : x ⟶ y} : (P ⋙ Q).map f = cast (by rw [good h]) ((R ⋙ S).map f) := sorry

want doesn't typecheck as defined though the types Lean complains are provably equal.

[Lawrence Wu (llllvvuu)]

Your statement doesn’t typecheck because you don’t have defeq. HEq is probably the best you can get, you may also be recommended to use a natural isomorphism P ⋙ Q ≅ R ⋙ S instead.

[Adam Topaz]

the usual answer is to not use equality of functors, but rather an isomorphism, and replace your cast by a composition with the isomorphism component.

[Aaron Liu]

import Mathlib.CategoryTheory.Functor.Basic
import Mathlib.CategoryTheory.EqToHom

open CategoryTheory

variable {A : Type} [Category A]
variable {B : Type} [Category B]
variable {C : Type} [Category C]
variable {D : Type} [Category D]
variable {P : A ⥤ B} {Q : B ⥤ D}
variable {R : A ⥤ C} {S : C ⥤ D}
variable (h : P ⋙ Q = R ⋙ S)

def good : (P ⋙ Q).obj = (R ⋙ S).obj := by funext; congr
def ok (x) : (P ⋙ Q).obj x = (R ⋙ S).obj x := by congr
def hok {x y : A} (f : x ⟶ y) : HEq ((P ⋙ Q).map f) ((R ⋙ S).map f) := by rw [h]
def okok {x y : A} (f : x ⟶ y) : ((P ⋙ Q).map f) ≫ eqToHom (ok h y) = eqToHom (ok h x) ≫ ((R ⋙ S).map f) := by
  rw [← heq_iff_eq, heq_eqToHom_comp_iff, comp_eqToHom_heq_iff]
  exact hok h f

[Slavomir Kaslev]

Thanks! Completely agree with the usual answer of using isomorphisms instead of equality.
However, the equality comes from the definition of the category of elements of a functor (want attempts for MWE of this original question) and cannot be changed.