rewriting along equality of functors

Stream: general

[Sina]

Is there a minimal example demonstrating that rewriting along equality of functors is not a good idea?

[Joël Riou]

The problem is not really whether you want to do it or not: most of the time, you just cannot do it!

import Mathlib.CategoryTheory.Functor.Category

namespace CategoryTheory

variable {C D E : Type _} [Category C] [Category D] [Category E] (F G : C ⥤ D) (H : D ⥤ E)

example {X Y : C} (f : X ⟶ Y) (h : F ⋙ H = G ⋙ H) [IsIso (H.map (F.map f))] :
    IsIso (H.map (G.map f)) := by
  rw [← Functor.comp_map]
  rw [← h] -- tactic 'rewrite' failed, motive is not type correct
  dsimp
  infer_instance

end CategoryTheory

Most of the time, if we can work with the data of functors isomorphisms rather than relying on equalities, it is generally advisable to do so: many functors are defined only up to a unique isomorphisms, so that it is not mathematically meaningful to use equalities of functors. However, some arguably meaningful equalities of functors do appear sometimes: for example, I have used this in 1) https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Localization/Predicate.html and 2) in the proof of the Dold-Kan equivalence. For 1), I just do not see how I could have done it without using the equalities of functors that are part of the universal property of a localized category. For 2), I found it was more convenient to do some rw in equalities of functors rather than showing all the constructions could be transported by isomorphisms.

[Sina]

@Joël Riou I guess i don't understand, from the type-theoretic perspective, why sometimes rw along equality of functors work and sometimes it does not?

[Kevin Buzzard]

One issue from a type-theoretic perspective is that equality is defined as an inductive type, and the theorem that if x=y then P(x)=P(y) (called the "principle of substitution" by logicians) is the axiom of recursion for equality in Lean, and in particular it's an axiom, so when checking that a diagram commutes you can't just "unravel everything", because you run into something for which there is no definition and which you can't "evaluate" or "unfold". A consequence of this is that if a = b are integers, but the proof isn't refl, and if M(n) is an abelian group attached to each integer, then M(a)=M(b) but the proof isn't refl and involves an axiom which turns out to be hard to work with. Given a term of type M(a) you can't just coerce it to having type M(b) for example, because coercions will only work for definitional equality. The way we address this is by instead of trying to make the equality work, we use an isomorphism M(a) \iso M(b) and prove theorems about this isomorphism instead. Equality of terms is fine but equality of types is problematic in dependent type theory. Equality of functors involves a lot of equality of types and if the proof isn't refl then you get this problem all over the place.

[Sina]

Kevin Buzzard said:

One issue from a type-theoretic perspective is that equality is defined as an inductive type, and the theorem that if x=y then P(x)=P(y) (called the "principle of explosion" by logicians) is the axiom of recursion for equality in Lean, and in particular it's an axiom, so when checking that a diagram commutes you can't just "unravel everything", because you run into something for which there is no definition and which you can't "evaluate" or "unfold". A consequence of this is that if a = b are integers, but the proof isn't refl, and if M(n) is an abelian group attached to each integer, then M(a)=M(b) but the proof isn't refl and involves an axiom which turns out to be hard to work with. Given a term of type M(a) you can't just coerce it to having type M(b) for example, because coercions will only work for definitional equality. The way we address this is by instead of trying to make the equality work, we use an isomorphism M(a) \iso M(b) and prove theorems about this isomorphism instead. Equality of terms is fine but equality of types is problematic in dependent type theory. Equality of functors involves a lot of equality of types and if the proof isn't refl then you get this problem all over the place.

Thanks, this is helpful! I guess, like your example of groups indexed by integers, this is about the dependently-typed structure of categories, say as opposed to the situation with groups and group homomorphisms, since to check equality of functors F and G, Lean needs to construct a proof of Ff = Gf for any morphism f : X -> Y but, a priori, Ff and Gf are terms of two different types which are not necessarily definitionally equal. That is why, in most cases rw fails for equality of functors.

[Mario Carneiro]

Kevin Buzzard said:

the theorem that if x=y then P(x)=P(y) (called the "principle of explosion" by logicians)

I think that property would be called equality congruence, or the substitution property of equality. The principle of explosion is False -> P (or P -> not P -> Q depending on the foundations)

[Kevin Buzzard]

Thanks! Fixed -- sorry for spreading misinformation.