Functor to Cat

Stream: mathlib4

[Nicolas Rolland]

Could anyone confirm it's impossible to write a functor (J ⥤ M) ⥤ Cat which to a functor associates its category of cone ?

(because of the equality non-sense of #mathlib4 > equality of cones )

I still can't believe it

[Adam Topaz]

I think it should be possible to write down such a functor. But it would probably be better to write it as a pseudofunctor!

[Kim Morrison]

As Adam says. The pseudo functor would be more useful :-).

Nevertheless I just wrote down

variable {J M : Type*} [Category J] [Category M]

def coneFunctor : (J ⥤ M) ⥤ Cat where
  ...

without too much trouble (it's 18 lines, uses Functor.ext).

[Kim Morrison]

(it's a good exercise, so for whatever reason you believed it was impossible, I encourage you to try it first)

import Mathlib

open CategoryTheory Limits

variable {J M : Type*} [Category J] [Category M]

@[simp] theorem Cones.hom_eqToHom {F : J ⥤ M} {X Y : Cone F} (h : X = Y) :
(eqToHom h).hom = eqToHom (congrArg Cone.pt h) := by cases h; simp

def coneFunctor : (J ⥤ M) ⥤ Cat where
obj F := Cat.of (Cone F)
map f := Cones.postcompose f
map_id F := by
dsimp
fapply CategoryTheory.Functor.ext
· intro X
simp [Cones.postcompose]
· intro X Y f
ext
simp
map_comp f g := by
dsimp
fapply CategoryTheory.Functor.ext
· intro X
simp [Cones.postcompose]
· intro X Y f
ext
simp

[Eric Wieser]

What's the statement of the pseudo-functor version?

[Adam Topaz]

import Mathlib

open CategoryTheory Limits

variable {J M : Type*} [Category J] [Category M]

def coneFunctor : Pseudofunctor (LocallyDiscrete (J ⥤ M)) Cat := sorry

[Nicolas Rolland]

Adam Topaz said:

I think it should be possible to write down such a functor. But it would probably be better to write it as a pseudofunctor!

Why would it be better to write it as a pseudo functor ?

[Nicolas Rolland]

Kim Morrison said:

(it's a good exercise, so for whatever reason you believed it was impossible, I encourage you to try it first)

The reason I thought it was impossible is the previous discussion where the equality postcompose (α ≫ β) = postcompose α ⋙ postcompose β, used here, was hailed as "evil" and triggered a philosophical debate on equality...

I still have two questions, which have a common answer I suppose :

• if that's a good exercice (it is !), doesn't that illustrate some lemmas are missing in the library ?
• why would the pseudo functor be any more useful ?

A priori, functors are more useful. they have more properties.
I dont dislike pseudo functors (especially, and famously, to Cat!!), but what's with this obsession ?

[Kim Morrison]

@Nicolas Rolland, could I suggest that this discussion seems to be going in circles a bit, and that perhaps rather than talking about what we "like" or think is "evil", you go and write some code, and make PRs? I think using the library, and trying to extend it, is the best way to understand the point we're trying to make.

In any case, the basic point is that generic casting via equality, or using heterogeneous equality, is intrinsically painful. The fault here is partly just the usual "dependent type theory hell", but also partly that informal mathematics tends to sweep casting under the rug because it is tedious and tends to always work out, even if the reasoning is sometimes subtle. Using casting operations specific to the context at hand (e.g. using eqToHom to promote an equality of objects to a morphism, or using a 2-functor to send equalities of morphisms to 2-morphisms) is more ergonomic, and easy to do reasoning about.

[Kim Morrison]

To be clear, no one said "evil" had anything to do with "impossible", I think that might be you jumping to a conclusion. :-) But as above, there's no need for philosophical debate here, instead we can debate with the typechecker! (And remembering our promise that so far we haven't run into anything insurmountable in this direction, despite having come quite far.)

[Nicolas Rolland]

Kim Morrison said:

Nicolas Rolland, could I suggest that this discussion seems to be going in circles a bit, and that perhaps rather than talking about what we "like" or think is "evil", you go and write some code, and make PRs? I think using the library, and trying to extend it, is the best way to understand the point we're trying to make.

Many points were made, philosophical, categorical-ish, with different kind of arguments (of which I only understand the ergonomical one)

I am all in favor of extending the library and making PR (I did a few) for this equality which you use.
I do not see why it should not be in the library.

In any case, the basic point is that generic casting via equality, or using heterogeneous equality, is intrinsically painful. The fault here is partly just the usual "dependent type theory hell", but also partly that informal mathematics tends to sweep casting under the rug because it is tedious and tends to always work out, even if the reasoning is sometimes subtle. Using casting operations specific to the context at hand (e.g. using eqToHom to promote an equality of objects to a morphism, or using a 2-functor to send equalities of morphisms to 2-morphisms) is more ergonomic, and easy to do reasoning about.

Right but having a plain functor allows all this too.
And having only a pseudo functor is less powerful.
I don't see where is the benefit.

Unless to say we rely on the simp infrastructure somehow, in a way unavailable to functor, nor to functor viewed as pseudo-functor.... ? It would be useful to have a clear example of this.

[Mario Carneiro]

Nicolas Rolland said:

Right but having a plain functor allows all this too.
And having only a pseudo functor is less powerful.
I don't see where is the benefit.

A functor is "more powerful", sure, but in what way? Perhaps you are thinking that because you have an equality you can now use rw and simp where you couldn't before. And you can, but this is a trap, because now you have introduced a cast operation into a piece of data, and this will cause issues with second order rewrites when you later try to reason about the term you just constructed.

Trust me, we've all been through this. The library design decision here is to argue that the "original sin" was having an equality sitting around where it can only be used in ways that are misuse. Hence the "evil" moniker and the preference for using pseudofunctors instead.

Note that none of the issues involved with using strict functors (and object equality more generally) are actually impossible to overcome, they are just very painful. The statement with functors is stronger, and occasionally a situation comes up where you actually need strict functoriality for mathematical reasons, and in that case you just have to power through it. But because the problems that arise on this path are well known, we would like to make sure that there are really no alternatives before going this route.

[Nicolas Rolland]

Thank you, I understand better what is at play here.
If I rephrase to make this ergonomical issue clearer, in a nutshell :

Having pseudo functors is more usable, as they have already, built-in, at categorical level, some official slot for those pesky 'eqToHom casts' .
They are the simplest honest categorical structure dealing natively with the unfortunate limitation of this encoding of categories (where each pair of objects yields a different hom-set type - thus "dependent type theory hell")

Mario Carneiro said:

Nicolas Rolland said:

Right but having a plain functor allows all this too.
And having only a pseudo functor is less powerful.
I don't see where is the benefit.

A functor is "more powerful", sure, but in what way? Perhaps you are thinking that because you have an equality you can now use rw and simp where you couldn't before. And you can, but this is a trap, because now you have introduced a cast operation into a piece of data, and this will cause issues with second order rewrites when you later try to reason about the term you just constructed.

I imagined we could easily turn a functor into a pseudo when necessary. and come back to plain functor world when we can after the eqToHom business is cared for. This is true categorically, but ergonomically, as you later expose, having functors requires to power thought it.

Mario Carneiro said:

Trust me, we've all been through this. The library design decision here is to argue that the "original sin" was having an equality sitting around where it can only be used in ways that are misuse. Hence the "evil" moniker and the preference for using pseudofunctors instead.

This moniker seems a bit overloaded.

Mario Carneiro said:

Note that none of the issues involved with using strict functors (and object equality more generally) are actually impossible to overcome, they are just very painful. The statement with functors is stronger, and occasionally a situation comes up where you actually need strict functoriality for mathematical reasons, and in that case you just have to power through it. But because the problems that arise on this path are well known, we would like to make sure that there are really no alternatives before going this route.

If I rephrase : As long as what you want to get out of a functor is also provided by having a pseudo, dont fight the encoding and embrace the pseudo.

[Another encoding, more natively suited for plain functors I suppose, would probably be as triple in Set, where we would have one type for all the morphisms ... Having conversion back and forth could be useful to get the best of both worlds ]

[Joël Riou]

Nicolas Rolland said:

I imagined we could easily turn a functor into a pseudo when necessary. and come back to plain functor world when we can after the eqToHom business is cared for. This is true categorically, but ergonomically, as you later expose, having functors requires to power thought it.

We have API to turn a functor into a pseudo-functor. Conversely, it is possible to obtain an equality of functors from an isomorphim docs#CategoryTheory.Functor.ext_of_iso