Encoding of categories and equality of hom-set

Stream: mathlib4

[Nicolas Rolland]

I am wondering how to use Functor.ext
As a exercise, given F = G, how can one use Functor.ext to prove that F = G ?

aesop_cat succeeds. is there any way to see the steps it takes ? set_option trace.aesop true

import Mathlib.CategoryTheory.Category.Cat

open CategoryTheory

universe v u
variable {C D : Cat.{u,v}}
variable (F G : C ⥤ D)

-- what does F = G mean ?
def usingFunctorEq  ( h : F = G)  : F = G  :=
  have h_obj (x : C) :   F.obj x = G.obj x  :=  sorry
  have h_map (x y : C) (f : x ⟶ y)  : F.map f =   eqToHom (h_obj x) ≫ G.map f ≫ eqToHom (h_obj y).symm := sorry
  Functor.ext h_obj h_map

---

More discussion :

The encoding of categories creates a type for each hom-set for each pair of object :
Given a category C, x ⟶ y is the type of those morphisms in C which go from x to y. With this encoding, any morphism has explicit type level domain and codomain.

While having strong type constraint is very handy in most cases, when proving equality of functors it becomes a bit of a problem :

To prove that two functors are equal, one should prove that objets are sent to the same objects, and morphisms are sent to the same morphism.

Said otherwise, to prove that F = G : C ⥤ D, one has to prove F.obj x = G.obj x for every x : C, and F.map f = G.map f for every f : x ⟶ y.

But F.map f = G.map f is type incorrect : F.map f : F.obj x ⟶ F.obj y while G.map f : G.obj x ⟶ G.obj y.

That's why the signature of Functor.ext is

Functor.ext
(h_obj : ∀ X, F.obj X = G.obj X)
(h_map : ∀ X Y f,   F.map f = eqToHom (h_obj X) ≫ G.map f ≫ eqToHom (h_obj Y).symm) :  F = G

Taking the equivalent point of view of categories as monad of span(set), with a less typed morphisms for a category, one could go around that problem and equivalently prove F.map f = G.map f , F.obj (dom f) = G.obj (dom f) and F.obj (cod f) = G.obj (cod f).

Being able to switch between the 2 representations for categories (explicitely typed hom-set VS implicitly typed) might be useful ?

[Nicolas Rolland]

With set_option trace.aesop.proof true one can view the proof for the equality of hom maps given the equality of functors.... and the given proof does not type check unfortunately

This translates, according the the trace

import Mathlib.CategoryTheory.Category.Cat

open CategoryTheory

universe v u
variable {C D : Cat.{u,v}}
variable (F G : C ⥤ D)

set_option trace.aesop true
set_option trace.aesop.proof true

def usingFunctorEq  ( h : F = G)  : F = G  :=
  have h_obj (x : C) :   F.obj x = G.obj x  :=  by rw [h]
  have h_map (x y : C) (f : x ⟶ y)  : F.map f = eqToHom (h_obj x) ≫ G.map f ≫ eqToHom (h_obj y).symm := by
   aesop

  Functor.ext h_obj h_map

to this funky program

import Mathlib.CategoryTheory.Category.Cat

open CategoryTheory

universe v u
variable {C D : Cat.{u,v}}
variable (F G : C ⥤ D)

set_option trace.aesop true
set_option trace.aesop.proof true

def usingFunctorEq  ( h : F = G)  : F = G  :=
  have h_obj (x : C) :   F.obj x = G.obj x  :=  by rw [h]
  have h_map (x y : C) (f : x ⟶ y)  : F.map f = eqToHom (h_obj x) ≫ G.map f ≫ eqToHom (h_obj y).symm :=
      Eq.ndrec (motive := fun G ↦
        ∀ (h_obj : ∀ (x : ↑C), F.obj x = G.obj x),
          F.map f = CategoryTheory.eqToHom (h_obj x) ≫ G.map f ≫ CategoryTheory.eqToHom (Eq.symm (h_obj y)))
        (fun h_obj ↦
          of_eq_true
            (Eq.trans
              (congrArg (Eq (F.map f))
                (Eq.trans
                  (congrArg (CategoryTheory.CategoryStruct.comp (𝟙 (F.obj x)))
                    (CategoryTheory.Category.comp_id (F.map f)))
                  (CategoryTheory.Category.id_comp (F.map f))))
              (eq_self (F.map f))))
        h h_obj

  Functor.ext h_obj h_map

How can I get rid of the type error in the solution given, to analyse what's really going on by myself... ?

[Kim Morrison]

Does

import Mathlib.CategoryTheory.Category.Cat

open CategoryTheory

universe v u
variable {C D : Cat.{u,v}}
variable (F G : C ⥤ D)

def usingFunctorEq  (h : F = G)  : F = G := show_term by
  fapply Functor.ext
  · subst h
    simp
  · intro X Y f
    subst h
    simp

help?

[Nicolas Rolland]

Thank you :pray:

Would you know why rw [h] wouldn't work here, while subst h does ?
It tries to find a motive ?

def usingFunctorEq  ( h : F = G)  : F = G  := show_term by
  fapply Functor.ext
  . subst h
    simp
  . intro X Y f
    rewrite [h] -- tactic 'rewrite' failed, motive is not type correct
    simp

This feels a bit like cheating though, of course equalities cut through everything, like saying exact h
I don't see how to use Functor.ext in other context