Zulip Chat Archive

Stream: maths

Topic: category theory documentation


view this post on Zulip Simon Hudon (Jan 01 2019 at 16:03):

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.

view this post on Zulip Johan Commelin (Jan 01 2019 at 17:28):

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.)

view this post on Zulip Reid Barton (Jan 01 2019 at 18:02):

The main pro is it lets you write a ⟶ b

view this post on Zulip Simon Hudon (Jan 01 2019 at 18:32):

@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.

view this post on Zulip Simon Hudon (Jan 01 2019 at 18:32):

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

view this post on Zulip Johan Commelin (Jan 01 2019 at 18:34):

@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).

view this post on Zulip Johan Commelin (Jan 01 2019 at 18:34):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 18:48):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 18:48):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 18:51):

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 ...)

view this post on Zulip Simon Hudon (Jan 01 2019 at 18:54):

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.

view this post on Zulip Mario Carneiro (Jan 01 2019 at 18:55):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 18:57):

I thought so. That's too bad!

view this post on Zulip Reid Barton (Jan 01 2019 at 18:58):

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.

view this post on Zulip Johan Commelin (Jan 01 2019 at 19:00):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 19:06):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 19:07):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 19:07):

Like at lines 22-23?

view this post on Zulip Reid Barton (Jan 01 2019 at 19:07):

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.

view this post on Zulip Johan Commelin (Jan 01 2019 at 19:08):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 19:10):

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

view this post on Zulip Johan Commelin (Jan 01 2019 at 19:11):

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

view this post on Zulip Johan Commelin (Jan 01 2019 at 19:11):

So my memory partly failed me.

view this post on Zulip Simon Hudon (Jan 01 2019 at 19:11):

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

view this post on Zulip Johan Commelin (Jan 01 2019 at 19:12):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 19:12):

the difference is nobody knows what abbreviation does :smile:

view this post on Zulip Reid Barton (Jan 01 2019 at 19:13):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 19:13):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 19:14):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 19:14):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 19:16):

Did it happen with this example?

view this post on Zulip Reid Barton (Jan 01 2019 at 19:16):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 19:17):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 19:18):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 19:22):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 19:28):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 19:29):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 19:38):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 19:41):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 19:45):

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

view this post on Zulip Johan Commelin (Jan 01 2019 at 20:22):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 20:23):

@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

view this post on Zulip Simon Hudon (Jan 01 2019 at 20:24):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 20:37):

Nope!

view this post on Zulip Reid Barton (Jan 01 2019 at 20:38):

It would be messy, and equivalent anyways

view this post on Zulip Reid Barton (Jan 01 2019 at 20:41):

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

view this post on Zulip Simon Hudon (Jan 01 2019 at 20:44):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 20:46):

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

view this post on Zulip Reid Barton (Jan 01 2019 at 20:46):

(outside of set theory of course)

view this post on Zulip Simon Hudon (Jan 01 2019 at 20:47):

Ooooh


Last updated: May 10 2021 at 08:14 UTC