Sigma types or Parameters?

Stream: mathlib4

[Pieter Cuijpers]

I'm doing a bit of Order Theory, hoping to make connections with pointless topology at a later stage.
At first, I thought there was no fundamental difference between defining partial orders as:
class PartialOrder (space : Type u) := (le := space -> space -> Prop) (reflexive : ...) (transitive: ...) (antisymmetric: ...)
or as
class PartialOrder := (space : Type u) (le := space -> space -> Prop) (reflexive : ...) (transitive: ...) (antisymmetric: ...)

Furthermore, I was happy to go along with the first, because it allows us to write
class PartialOrder (space : Type u) extends LE space := (reflexive : ...) (transitive: ...) (antisymmetric: ...)
giving nice $\leq$ notation in the mix.

However... when I next tried a bit of category theory defining
class Category := (Obj : Type u) (Morph: Obj -> Obj -> Type v) (Conc : Morph -> Morph -> Morph) (Id : Obj -> Morph)

And subsequently try to prove that Partial Orders as Obj are a Category (with order preserving maps defined as Morph and concatenation of functions as Conc and identity as Id), the first definition does not typecheck while the second one does. The reason for this is that the first definition is a Type u -> Type u : Type u+1, while the second one is a Sigma type.

In ordinary terms, the first definition is "parameterized" (the space over which we have defined the partial order is a parameter of the class) while the second definition has the space as a given field. Practically, in the second definition there is a projection PartialOrder.space that gives you the space, which does not exist in the first definition.

Of course, this does in principle not stop me from using the Category definition, since I can use Sigma space, Partial Order space as a suitable type for Obj. However it does raise the question: How do we determine which of the two definitions is preferable for a library like Mathlib4? When is one type of definition preferred over the other? I imagine it really depends on what your goal is... .

I hope it's clear what I mean.
Curious to hear your thoughts...

[Scott Morrison]

Note that in mathlib we have both: see category for the unbundled version, and Cat for the bundled version.

[Scott Morrison]

Essentially, when the subject of your argument is elements of a structure, it is more convenient to have unbundled structures, and when the subject is relationships between such structures, it is more convenient to have the bundled structures.

[Floris van Doorn]

We have gained a lot of experience on this in mathlib 3: we have e.g. docs#partial_order for generic use throughout most of the library, and docs#PartialOrder for the category of partial orders.

[Pieter Cuijpers]

Ah cool, I suspected there should be knowledge embedded here. I haven't really looked at Mathlib 3 yet. Just started with theorem provers a few months ago and decided on Lean4 since "things seem to be going that way". So I "made do" with what was in Mathlib4 as a source of inspiration and am now mostly defining my own structures as part of the learning process. Ultimately, I can see myself contributing to Mathlib4, so whenever I can I try to think about "how it should be done" next to "how I would do it".

[Pieter Cuijpers]

Do I understand correctly that category_theory.bundled basically performs the Sigma construction I mentioned above, but then for arbitrary constructions?

[Floris van Doorn]

correct