category theory documentation

Stream: maths

[Simon Hudon]

Is there a transcript of the rationale behind the design decisions of the category theory part? Specifically, I'd like to know what were the pros and cons of defining category as a type class versus as a structure.

[Johan Commelin]

I guess one of the big pros of using a type class is that Lean will do more work for you... more automation. And the category theory tries to maximize automation as much as possible.
(There is still a lot more to be done, and in fact more has been done in Scott's repositories. Quite often you will see proof obligations in the category-lib written out explicitly that are transparent in Scott's repos because he has better automation than mathlib.)

[Reid Barton]

The main pro is it lets you write a ⟶ b

[Simon Hudon]

@Reid Barton That's a good point. At the same time, that's also a downside because this notation does not tell you which category you're talking of and, I don't know if it's the corner of category theory that I'm in but it seems to be often relevant to distinguish.

[Simon Hudon]

@Johan Commelin Can you give me examples of automation that are made possible that way?

[Johan Commelin]

@Simon Hudon Maybe it is not so much automation as it is brevity. Now you don't have to feed Lean the category structure when writing down functors or limits (or hom-sets).

[Johan Commelin]

Are you saying that you often have multiple category structures on the same type?

[Reid Barton]

You can always use @category.hom explicitly but it might be more convenient (or not) to create synonyms of the underlying type for the different category structures

[Simon Hudon]

Yes. Often might be over stating it as I'm a very fresh category noob. Let's say I'm seeing a repetition in the proofs I find the hardest and this confusion contributes to it

[Simon Hudon]

But Johan, I'm not suggesting that you write functor C 𝒞 D 𝒟; rather I'd let 𝒞 and 𝒟 stand for both the carrier type and the data+proofs by using has_coe_to_sort (please don't kill me @Scott Morrison, I know you're sick of coercions but maybe this time ...)

[Simon Hudon]

You can always use @category.hom explicitly but it might be more convenient (or not) to create synonyms of the underlying type for the different category structures

Maybe you're right. I could write a reducible definition so that I don't have to feed both the type and the instance. It does not make up for the other shortcoming of type classes though: with category.{u}, inference is often hindered.

[Mario Carneiro]

small_category was supposed to help with that, but I guess it doesn't get used much in favor of more generality

[Simon Hudon]

I thought so. That's too bad!

[Reid Barton]

But Johan, I'm not suggesting that you write functor C 𝒞 D 𝒟; rather I'd let 𝒞 and 𝒟 stand for both the carrier type and the data+proofs by using has_coe_to_sort (please don't kill me @Scott Morrison, I know you're sick of coercions but maybe this time ...)

This sounds like bundled vs unbundled categories (e.g. https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.1/src/category_theory/bundled.lean). I'm not sure whether bundled categories were ever considered as the primary interface. It seems like it could be a viable option. It's possible that Scott just chose to use unbundled ones on the basis that other structures (groups, etc.) are unbundled.

[Johan Commelin]

Instead of a reducible type, you could also create a local abbreviation for @category.hom, right?

[Simon Hudon]

I didn't know you could make abbreviation local. Is that useful?

[Simon Hudon]

@Reid Barton That looks good! I might steal it for myself. Do you see a downside to having the coercion?

[Reid Barton]

Like at lines 22-23?

[Reid Barton]

To be honest, I've hardly used this at all. I was going to prove that Cat has colimits, but I didn't get very far.

[Johan Commelin]

@Simon Hudon I think they have tspace as abbreviation for @topological_space in the topological_space.lean file.

[Reid Barton]

there's some local notation `cont` := @continuous _ _ I think

[Johan Commelin]

git grep tspace
analysis/topology/continuity.lean:local notation `tspace` := topological_space

[Johan Commelin]

So my memory partly failed me.

[Simon Hudon]

Ah! Ok! It's a local notation, not an an abbreviation

[Johan Commelin]

Right... (I don't even know the difference...)

[Reid Barton]

the difference is nobody knows what abbreviation does :smile:

[Reid Barton]

Coercions tend to break down once you have implicit parameters inside the term being coerced that Lean needs to infer.

[Simon Hudon]

Haha! Abbreviation is sometimes useful but if you use it wrong it's pretty annoying because it doesn't come with equations and you can decide to unfold it. And yet, it's not notation because it is represented in the syntax tree, it has a type, etc

[Simon Hudon]

I've seen that, it's true. I hear coercion used to be better in Lean 2.

[Reid Barton]

Maybe an example would be if we had over X : Cat, where X : C and C : Cat, then in A : over X, Lean might play dumb and pretend not to be able to figure out what C is

[Simon Hudon]

Did it happen with this example?

[Reid Barton]

This is just hypothetical because I never got as far as doing things like that with bundled categories

[Reid Barton]

I guess one could test with something like def over {C : Cat} (X : C) : Cat := C (not the right definition, but it shouldn't matter) and then try to use the coercion

[Reid Barton]

It also might only fail when Lean needs to use information from outside the thing being coerced to infer implicit arguments inside it--not sure

[Simon Hudon]

I mostly ran into trouble when using coercion to function types and never with coerce to sort. And one reason I would run into trouble was that I coerced to a polymorphic function type and I needed to infer some of the type parameters and Lean would just give up

[Simon Hudon]

I think I'll run an experiment with reformulating mathlib that way and see how difficult it is

[Reid Barton]

Yeah, I can't remember having any issues with coercions to sort either

[Simon Hudon]

I just had a quick look and the following works:

structure cat : Type.{max (u+1) v+1} :=
(carrier : Type u)
[inst : category.{v} carrier]

instance has_coe_to_sort.cat : has_coe_to_sort cat.{u v} :=
{ S := Type u,
  coe := cat.carrier }

def Hom {C : cat.{u v}} (x y : C) : Type v := @category.hom _ C.inst x y

variables {C : cat.{u v}} (x y : C)

#check Hom x y

[Simon Hudon]

And then I can define the following notation:

notation x ` ⟶[` c `] ` y := Hom c x y
#check Hom C x y
-- x ⟶[C] y : Type v

local infix ` ⟶ ` := Hom _

#check Hom C x y
-- x ⟶ y : Type v

[Reid Barton]

A bonus is that we can now give the category of types the correct name, namely Set

[Johan Commelin]

@Simon Hudon Don't you mean to make the argument C to Hom explicit?

[Simon Hudon]

@Johan Commelin Yes you're right! I changed it in my file and didn't bother fixing it here but it does matter you're right

[Simon Hudon]

@Reid Barton Wouldn't you define Set using set_theory instead?

[Reid Barton]

Nope!

[Reid Barton]

It would be messy, and equivalent anyways

[Reid Barton]

set_theory sets have notions like global membership/subset predicates, which aren't relevant to Set

[Simon Hudon]

Oh! That simplifies a lot! I was trying to understand pushouts and pullbacks and on ncatlab.org, they refer to Set a lot so I kind of pulled back from them

[Reid Barton]

The dictionary for reading mathematics is Type = set, and set = subset

[Reid Barton]

(outside of set theory of course)

[Simon Hudon]

Ooooh

[Yury G. Kudryashov]

I have a suggestion about documentation requirements in category_theory/: for every category, the docstring should say what are the objects and what are the morphisms; if this can be stated with and without category theory language, then both descriptions should be there.

[Yury G. Kudryashov]

Same for functors.

[Yury G. Kudryashov]

My motivation: I was trying to read and understand docs#sSet.to_Top and nearby definitions.

[Yury G. Kudryashov]

To understand it, I have to follow each definition, read the docstring, combine them in my head, then hope that I'm right.

[Adam Topaz]

Sorry, I should have been more descriptive there :see_no_evil:

[Adam Topaz]

To be fair, this is "standard" terminology: https://en.wikipedia.org/wiki/Simplicial_set#Geometric_realization
But I of course agree that expanding the documentation would be helpful.

[Yury G. Kudryashov]

Of course, this is a standard terminology for someone who knows all this. I was looking at this to understand the definition of singular homology given here and I never thought about it in terms of category theory.