Category theory PR

Stream: general

[Scott Morrison]

Hi @Mario Carneiro, I didn’t understand your suggestion to use “functor.id (protected)”. What is “protected”?

[Scott Morrison]

Worked it out.

[Mario Carneiro]

Hm, I see that you renamed the identity functor to category.identity and the identity natural transformation to functor.identity. I assume you did that so that you can use projection notation, but I think it's more confusing than is worth it. What do the mathematicians here think?

[Scott Morrison]

Oh, I'm not at all attached to projection notation here: I'd guessed that was what you'd tell me to do!

[Scott Morrison]

As far as I'm concerned I would be happy with any of:
C.identity, Functor.id C, Functor.identity C, or 1 : C ↝ C.

[Scott Morrison]

(I know how to arrange for any of those, just want to know what is preferred.)

[Johan Commelin]

My order of preference would be 4,1,3,2

[Mario Carneiro]

Johan, Would you prefer to see 1 X or functor.id C X in a goal printout talking about the identity functor applied to an object X?

[Mario Carneiro]

(this isn't a rhetorical question)

[Scott Morrison]

@Mario Carneiro, I'm confused why we would want to put protected on the definition of the identity functor. What is the motivation there? It seems if we're going to hide that, we should also hide the lemmas about it.

[Scott Morrison]

@Mario Carneiro, seeing that comparison, I really dislike 1 X!

[Mario Carneiro]

because id is already a global definition, and we don't want to interfere with that

[Scott Morrison]

How about functor.identity C?

[Mario Carneiro]

plus there are like 5 different ids going around and I'd like to know which is which

[Scott Morrison]

No need to collide with the global id

[Scott Morrison]

or the category.id

[Scott Morrison]

... :-)

[Mario Carneiro]

the name collision is deliberate though, it's a consistent naming scheme

[Scott Morrison]

In fact, I now really dislike the has_one instances for both C ↝ C and F ↝ F, and want to remove both.

[Mario Carneiro]

I'm surprised this bothers you given that we already have 𝟙 X

[Scott Morrison]

Okay... so functor.id C, nat_trans.id F, and the only use of the symbol 1 will be 𝟙 X.

[Mario Carneiro]

I'm okay with that

[Mario Carneiro]

the protection is not needed for the theorems since they usually have more specific names that don't collide with core

[Mario Carneiro]

they are still namespaced in functor though so you will need to use the prefix unless you have opened it

[Johan Commelin]

Johan, Would you prefer to see 1 X or functor.id C X in a goal printout talking about the identity functor applied to an object X?

I think I would prefer something like that id_ C or 1_ C.

[Mario Carneiro]

How about using local notations for that?

[Johan Commelin]

That might work.

[Mario Carneiro]

You probably don't need the C most of the time either

[Johan Commelin]

Yes, but it might help to remind you of which cat you're working with.

[Mario Carneiro]

Well if it shows up as 1_ X then it's inferrable from context

[Johan Commelin]

I might think that is the identity morphism of X

[Mario Carneiro]

that's the completely different 𝟙 X :P

[Scott Morrison]

Yeah, I think we want to make expressions that look even vaguely like 1 X unambiguous

[Scott Morrison]

and my preference is that the only similar looking expressions are 𝟙 X, the identity morphism on X.

[Scott Morrison]

If only there was a triple struck 1

[Mario Carneiro]

I keep being reminded of equiv.refl as the only notation for the identity equiv

[Johan Commelin]

Hmm, I prefer 𝟙 C

[Johan Commelin]

If we have 𝟙 X already.

[Mario Carneiro]

I think that will be a thing too

[Johan Commelin]

After all, it is the identity morphism on C in Cat.

[Johan Commelin]

Aah, and they will be defeq, but we can't have only one definition?

[Scott Morrison]

Yeah... that's a bit of a sore point. Cat is of course a 2-category, and thinking of it as a 1-category by just ignoring the top level invites trouble.

[Mario Carneiro]

so that means 𝟙 C is not (or will be) defeq to functor.id C?

[Mario Carneiro]

or does 𝟙 C just not typecheck?

[Scott Morrison]

At present it just doesn't typecheck

[Scott Morrison]

Let me investigate this point for a few minutes.

[Scott Morrison]

Arranging for 𝟙 C to typecheck may not be impossible, but it will take quite a bit of work which hasn't otherwise been necessary, so I'd like to kick that back to some TODO list. :-)

[Johan Commelin]

Sure, I'm completely fine with that (-;

[Scott Morrison]

For now you just write functor.id C when you want the identity functor.

[Johan Commelin]

Sounds like we might want has_id notation.

[Johan Commelin]

And then all sorts of things can be instances of has_id, and you can write a doublestroke 1 in front of them.

[Mario Carneiro]

and what would the type of generic.id be?

[Johan Commelin]

What's that?

[Mario Carneiro]

if you have a typeclass, you have to decide in advance what the type of the thing is

[Johan Commelin]

You are talking with a "cargo cult Leaner"

[Johan Commelin]

So, you mean the type of has_id?

[Mario Carneiro]

well, has_id will be a class that contains an identity operation, and that identity operation will have some type

[Johan Commelin]

Aah, I see.

[Johan Commelin]

Yeah... depends...

[Johan Commelin]

And it depends a bit too much to be a dependent type.

[Mario Carneiro]

I suspect this will be a sticking point in any such plans

[Mario Carneiro]

category theory just has too much overloading here to make sense of it

[Mario Carneiro]

Congratulations to Scott for his perseverance in improving this PR for mathlib and even going back to change his library, which could not have been an easy task.

[Scott Morrison]

Phew... I think I've rewritten everything about 4 times now. It does keep getting less bad as a result, whatever that signifies. :-)

[Mario Carneiro]

now that we've got the basic definitions, how about the less basic ones? :D

[Scott Morrison]

Don't worry, there's a category_theory_2 branch ready to turn into a PR. :-)

[Scott Morrison]

I'm just having to google how rebasing works!

[Scott Morrison]

okay... rebasing is still confusing me, but there's a second PR now!

[Johan Commelin]

Cool! Awesome! Congratulations!

[Kevin Buzzard]

Oh the first PR has been merged! Fabulous!

[Scott Morrison]

Hi @Reid Barton sometime soon we should do some coordination to combine the category theory development you've been doing in your homotopy theory repo with mine.

[Patrick Massot]

This should definitely be one of our small groups in Orsay (although you can start online of course).