Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Structure vs stuff?

Shea Levy (Nov 25 2020 at 19:57):

From the nLab article, I'm having a hard time being confident in determining whether something is "structure" and whether something is "stuff". Does anyone have a good way to get an intuition for this, ideally without referring to properties of forgetful functors? Maybe some more examples of objects with extra stuff and some with extra structure?

My current vague guess is we can distinguish operations vs subsets? So equipping a set with a total order adds structure (subset of $S \times S$) but equipping a set with addition adds stuff?

Shea Levy (Nov 25 2020 at 20:01):

This section could be a bit more helpful :sweat_smile: https://ncatlab.org/nlab/show/structure#examples

Dan Doel (Nov 25 2020 at 20:06):

'Stuff' is objects, 'structure' is arrows, 'property' is equations between arrows.

Amar Hadzihasanovic (Nov 25 2020 at 20:08):

I usually think of “stuff” as some extra information on morphisms...

Amar Hadzihasanovic (Nov 25 2020 at 20:11):

For example, you could think of a category of sets and “functions implemented in a specific programming language”. The implementation is “stuff” on the functions.

Dan Doel (Nov 25 2020 at 20:16):

Does that fit into the stuff/structure/properties thing?

I think the way that would work with what I said would that you could have the same set 'within' distinct programming languages, and that would show up as multiple non-isomorphic objects that are 'forgotten' to the same set (so, the forgetful functor is not faithful).

Amar Hadzihasanovic (Nov 25 2020 at 20:17):

I know you don't want to refer to properties of forgetful functors, but I do think it is helpful: a functor that “forgets only stuff” is one that, essentially, can only “forget the distinction” between some parallel morphisms.

Amar Hadzihasanovic (Nov 25 2020 at 20:19):

Dan Doel said:

'Stuff' is objects, 'structure' is arrows, 'property' is equations between arrows.

I think you need to do swap “stuff” and “property” here?

Dan Doel (Nov 25 2020 at 20:20):

Do I? I thought I had finally vaguely understood this stuff. :)

Shea Levy (Nov 25 2020 at 20:22):

This is why I want to avoid the functor interpretation :smile: Can we ground this in pre-categorical examples? E.g. we can presumably all agree commutativity of a monoid is a property. Is there anything that is unambiguously structure vs unambiguously stuff?

Shea Levy (Nov 25 2020 at 20:24):

Taking a stab, maybe "pointedness" of a pointed set is structure since the point was in a sense "already there" but not specially identified

Dan Doel (Nov 25 2020 at 20:25):

Is a semigroup being a monoid a property? Or is the unit of a monoid structure on a semigroup?

Shea Levy (Nov 25 2020 at 20:26):

I think it's structure?

Dan Doel (Nov 25 2020 at 20:26):

Yeah, but what is your pre-categorical argument for that?

Dan Doel (Nov 25 2020 at 20:26):

That's the answer the forgetful functor gives, but why?

Fawzi Hreiki (Nov 25 2020 at 20:27):

Well if we want the theory to be algebraic, we need to have a chosen element

Shea Levy (Nov 25 2020 at 20:27):

It's more than a property because it gives the specific element

Shea Levy (Nov 25 2020 at 20:32):

To be clear, I'm not expecting to get a precise answer without referring to the category theory concepts. Just an intuition

Dan Doel (Nov 25 2020 at 20:34):

The reason the forgetful functor says structure is that semigroup maps needn't preserve the unit element, if they exist, while monoid maps must. But I think if you consider semigroup equivalences in HoTT instead, they automatically preserve units, so that makes it look like a property.

Dan Doel (Nov 25 2020 at 20:34):

At least, if I'm remembering the right example when I was thinking about this before.

Dan Doel (Nov 25 2020 at 20:37):

And if you consider congruences there might be another example where something looks like structure, but the category version would say it's a property.

Shea Levy (Nov 25 2020 at 20:38):

Maybe another example that might help or confuse things: if we pair a set $S$ with a proposition $a \le b$ for all $a, b \in S$, the relation to me seems more like structure where as if we pair a set $S$ with a set $hom(a, b)$ for all $a, b \in S$ the hom set to me is more like stuff

Shea Levy (Nov 25 2020 at 20:39):

(maybe some arbitrary order $\prec$ would be better here since you can more naturally impose many of those on the same set)

Dan Doel (Nov 25 2020 at 20:52):

I think maybe group inverse is an example of the map vs. congruence thing? Monoid maps automatically preserve group inverses, so that version says it's a property, but congruences might say it's property-like structure.

Dan Doel (Nov 25 2020 at 20:53):

Your informal heuristic probably argues that group-inverse is structure, too, because it's "giving" the inverse of each element.

Shea Levy (Nov 25 2020 at 20:57):

Hmm yeah... Less confident in that now honestly.

Dan Doel (Nov 25 2020 at 20:58):

My point isn't that you're wrong, it's that this classification is somewhat arbitrary.

Shea Levy (Nov 25 2020 at 20:58):

Sure. I'm trying to get at the central cases though, I'm still not sure I get what stuff is, beyond the underlying set itself.

Shea Levy (Nov 25 2020 at 20:59):

I guess if we take X to the free foo on generators in X that might add stuff if foo has some operators?

Reid Barton (Nov 25 2020 at 21:00):

I thought "stuff" was typically another sort

Reid Barton (Nov 25 2020 at 21:00):

e.g. a ring and a module over the ring is a ring with extra stuff

Shea Levy (Nov 25 2020 at 21:01):

Is a relation a sort in this context? Does it change if we're proof-relevant or not?

Dan Doel (Nov 25 2020 at 21:01):

Well, your earlier example correctly classifies things, I think. Equipping a set with an ordering relation is structure, because distinct order-preserving maps go to distinct maps. But forgetting the hom structure might leave you with duplicate maps on $S$, so that's 'stuff' I think.

Reid Barton (Nov 25 2020 at 21:01):

No, a relation is similar to a function--both are structure

Reid Barton (Nov 25 2020 at 21:02):

After all, you (Dan excepted) can encode an operation by the relation that is its graph

Shea Levy (Nov 25 2020 at 21:03):

Dan excepted due to non-intuitionistic? Me too then I'm afraid :sweat_smile:

Reid Barton (Nov 25 2020 at 21:04):

OK, then you might be confused by mathematicians.

Dan Doel (Nov 25 2020 at 21:06):

So I guess you can see the extra 'stuff' in two ways. It's 'stuff' because it's equipping $S$ with additional sets of things. But it's also 'stuff' because you have more arrows generated by mappings between those equipped sets, like @Amar Hadzihasanovic said.

Dan Doel (Nov 25 2020 at 21:06):

Rather than just maps on $S$.

Shea Levy (Nov 25 2020 at 21:07):

Dan Doel said:

Well, your earlier example correctly classifies things, I think. Equipping a set with an ordering relation is structure, because distinct order-preserving maps go to distinct maps. But forgetting the hom structure might leave you with duplicate maps on $S$, so that's 'stuff' I think.

Is this essentially saying that a "map" from a category includes mapping on the hom structure, while a "map" from a partial order merely needs to preserve the existence of the order structure?

Morgan Rogers (he/him) (Nov 25 2020 at 21:08):

Was property/stuff/structure as a trichotomy ever meant to be more than a heuristic for making sense of properties of functors?

Dan Doel (Nov 25 2020 at 21:09):

Yeah. You can view them the same way, because the latter includes a 'map' between the orders. But all such maps are equivalent, because they're propositions.

Shea Levy (Nov 25 2020 at 21:09):

The sense I've always gotten was that the functor properties formalized informal language that mathematicians might use

Dan Doel (Nov 25 2020 at 21:12):

It does, but it got arbitrarily formalized in terms of categories instead of one of at least two other ways, because biased category theorists decided to codify it. :)

Reid Barton (Nov 25 2020 at 21:15):

Structure vs. properties I think is pretty widely understood, but stuff vs. structure is not so standard. For instance a scheme is a topological space equipped with a "structure sheaf"--which is definitely stuff and not structure by any version of this definition.

Reid Barton (Nov 25 2020 at 21:17):

The more basic distinction is structure is anything that's data, and properties are, well, properties.

Reid Barton (Nov 25 2020 at 21:17):

"Property" means it comes after "such that" in the definition.

Shea Levy (Nov 25 2020 at 21:20):

I'd say necessary (though not, perhaps, sufficient, see Dan's example of monoid vs semigroup) for "property" is that it follows from the structure/stuff. A given group is abelian or it isn't.

Nathanael Arkor (Nov 25 2020 at 21:26):

Reid Barton said:

I thought "stuff" was typically another sort

I had assumed that "stuff" corresponded to sorts, "structure" to operations, and "properties" to equations, though now I see that this doesn't quite match some of the examples on the nLab page (e.g. an inner product on a vector space, which I would have thought was structure).

Nathanael Arkor (Nov 25 2020 at 21:26):

If it did match up, it seems like quite a neat way of capturing this trichotomy from an algebraic perspective.

Shea Levy (Nov 25 2020 at 21:27):

Is $\exists$ an operation or an equation? :smile:

Shea Levy (Nov 25 2020 at 21:28):

Dan Doel said:

It does, but it got arbitrarily formalized in terms of categories instead of one of at least two other ways, because biased category theorists decided to codify it. :)

Can you spell out the two other ways a bit more?

Amar Hadzihasanovic (Nov 25 2020 at 21:32):

Nathanael Arkor said:

I had assumed that "stuff" corresponded to sorts, "structure" to operations, and "properties" to equations, though now I see that this doesn't quite match some of the examples on the nLab page (e.g. an inner product on a vector space, which I would have thought was structure).

The “inner product” seems like a confusing example because it certainly is structure if one considers e.g. isometries or short maps as the morphisms of inner product spaces. I guess the author considers it as “stuff” if one takes all linear maps as morphisms.

Dan Doel (Nov 25 2020 at 21:34):

@Shea Levy A 'congruence' is a relation that respects algebraic operations. Those are generally more flexible than homomorphisms. So if you do the same analysis with respect to those, you'll get more things categorized as structure instead of properties when it's ambiguous, I think. And probably the same with stuff.

The opposite direction is to use isomorphisms instead of homomorphisms, which classifies more things as properties instead of structure.

Shea Levy (Nov 25 2020 at 21:36):

Dan Doel said:

Shea Levy A 'congruence' is a relation that respects algebraic operations. Those are generally more flexible than homomorphisms. So if you do the same analysis with respect to those, you'll get more things categorized as structure instead of properties when it's ambiguous, I think. And probably the same with stuff.

The opposite direction is to use isomorphisms instead of homomorphisms, which classifies more things as properties instead of structure.

Hmm so if we're using isomorphisms then in the single sorted case there is no structure at all right?

Shea Levy (Nov 25 2020 at 21:37):

Or maybe that's set-theoretic bias sneaking in

Dan Doel (Nov 25 2020 at 21:37):

Single sorted case of what?

Amar Hadzihasanovic (Nov 25 2020 at 21:38):

So there seems to be at least two different kinds of “stuff”:

• extra information on objects that is not taken into account by morphisms;
• extra information on morphisms...

Shea Levy (Nov 25 2020 at 21:38):

Dan Doel said:

Single sorted case of what?

Any single-sorted theory, an isomorphism on the underlying set will always preserve whatever else right?

Dan Doel (Nov 25 2020 at 21:39):

I don't think isomorphisms of sets automatically preserve binary operations on sets.

Shea Levy (Nov 25 2020 at 21:40):

It's interesting to see I'm not alone in uncertainty here. Would it be helpful to collect a few examples that have pretty strong agreement?

1. Equipping a set of objects with a hom-set for each pair of objects is definitely stuff
2. A group being abelian is definitely properties
3. ??? is definitely structure

Shea Levy (Nov 25 2020 at 21:40):

Dan Doel said:

I don't think isomorphisms of sets automatically preserve binary operations on sets.

:face_palm: right, was thinking of equality of sets

Amar Hadzihasanovic (Nov 25 2020 at 21:40):

The first kind corresponds to forgetful functors that are essentially surjective, full, faithful, but not injective on objects.
The second to forgetful functors that are essentially surjective, full, injective on objects, but not faithful.

Nathanael Arkor (Nov 25 2020 at 21:45):

Shea Levy said:

Is $\exists$ an operation or an equation? :smile:

On its own, certainly an operation (but perhaps one conferred by the meta-theory itself!).

John Baez (Nov 25 2020 at 22:41):

Shea Levy said:

From the nLab article, I'm having a hard time being confident in determining whether something is "structure" and whether something is "stuff". Does anyone have a good way to get an intuition for this, ideally without referring to properties of forgetful functors? Maybe some more examples of objects with extra stuff and some with extra structure?

My current vague guess is we can distinguish operations vs subsets? So equipping a set with a total order adds structure (subset of $S \times S$) but equipping a set with addition adds stuff?

Equipping a set with a total order or an addition adds structure.

Equipping a set with another set adds stuff.

John Baez (Nov 25 2020 at 22:43):

Amar Hadzihasanovic said:

Dan Doel said:

'Stuff' is objects, 'structure' is arrows, 'property' is equations between arrows.

I think you need to do swap “stuff” and “property” here?

No, Dan has it exactly right.

We often describe mathematical gadgets by first giving some stuff, then some structure, then some properties.

Here's a good example: a semigroup is

• a set $S$
• together with a function $m: S \times S \to S$
• such that $m$ is associative.

The set is stuff, the function is structure, and the associative law is a property.

Shea Levy (Nov 25 2020 at 22:44):

Why is an inner product extra structure then?

John Baez (Nov 25 2020 at 22:45):

Because it's a function.

Shea Levy (Nov 25 2020 at 22:45):

Erm, stuff

John Baez (Nov 25 2020 at 22:45):

An inner product on a vector space is not extra stuff.

Shea Levy (Nov 25 2020 at 22:45):

"objects being equipped with “extra stuff” (for instance a vector space equipped with an inner product)." is nlab wrong here?

John Baez (Nov 25 2020 at 22:48):

John Baez said:

We often describe mathematical gadgets by first giving some stuff, then some structure, then some properties.

Here's a good example: a semigroup is

• a set $S$
• together with a function $m: S \times S \to S$
• such that $m$ is associative.

The set is stuff, the function is structure, and the associative law is a property.

Note that we can't describe the structure until we have the stuff.

We can't describe the property until we have the structure.

That's how it works.

Also note that:

• the stuff is choosing an object in a category (an object $S \in \mathsf{Set}$ in this example).
• the structure is choosing a morphism in a category ($m: S \times S \to S$).
• the property is choosing an equation between morphisms in a category.

John Baez (Nov 25 2020 at 22:49):

Shea Levy said:

"objects being equipped with “extra stuff” (for instance a vector space equipped with an inner product)." is nlab wrong here?

Yes, that sounds wrong to me. Can you point me to it? I can't imagine any way for it to be correct.

Nathanael Arkor (Nov 25 2020 at 22:56):

@John Baez: see bullet point 3 here.

John Baez (Nov 25 2020 at 22:57):

Dan Doel said:

Is a semigroup being a monoid a property? Or is the unit of a monoid structure on a semigroup?

This is a fun example. We can do this one either way, but it makes a big difference.

1) We can say "a monoid is a semigroup $S$ together with an element $1 \in S$ such that $1 \cdot s = s = s \cdot 1$ for all $s \in S$. Here the unit extra structure.

2) We can say "a monoid is a semigroup $S$ such that there exists an element $e \in S$ such that $e \cdot s = s = s \cdot e$ for all $s \in S$. Here the existence of the unit is a property.

What's the difference? The difference is visible when we consider morphisms between monoids! Structure is preserved by morphisms. It makes no sense for properties to be preserved by morphisms. (For example, it makes no sense to talk about "a homomorphism between groups that preserves abelianness.")

1) In the first approach, a monoid homomorphism is a semigroup homomorphism $f: S \to S'$ such that $S$ and $S'$ are monoids and $f$ preserves the unit.

2) n the first approach, a monoid homomorphism would be just a semigroup homomorphism $f: S \to S'$ such that $S$ and $S'$ are monoids... it doesn't make sense to say $f$ preserves the existence of the unit.

1) is the usual definition of monoid homomorphism, which means we normally treat the unit as extra structure.

John Baez (Nov 25 2020 at 22:58):

Nathanael Arkor said:

John Baez: see bullet point 3 here.

Okay, thanks. That's complete crap. I'll fix it.

John Baez (Nov 25 2020 at 23:02):

Reid Barton said:

I thought "stuff" was typically another sort

Yes.

Nathanael Arkor said:

I had assumed that "stuff" corresponded to sorts, "structure" to operations, and "properties" to equations.

Yes, that's a good way to think about it... though structure can consist of relations as well as operations.

though now I see that this doesn't quite match some of the examples on the nLab page (e.g. an inner product on a vector space, which I would have thought was structure).

That example was wrong. It's gone now. An inner product is just structure. I wonder who put in that example.

Nathanael Arkor (Nov 25 2020 at 23:10):

Perfect, that clears up my remaining confusion, thank you!

sarahzrf (Nov 25 2020 at 23:38):

oooh nice to hear that's been changed

sarahzrf (Nov 25 2020 at 23:38):

that particular example tripped me up for a while

sarahzrf (Nov 25 2020 at 23:38):

...maybe i should try getting into the habit of editing the nlab when i realize something is wrong.

sarahzrf (Nov 25 2020 at 23:47):

anyway tho: my 2 cents on this topic is that what made some of this click for me was that "equipping your objects with (n + 1)-stuff" means equipping your morphisms with n-stuff, and as base cases:

• to equip with (-1)-stuff is just to require some properties
• to equip with (-2)-stuff is to do nothing whatsoever

sarahzrf (Nov 25 2020 at 23:57):

so

• an abelian group is a group plus (-1)-stuff (properties)—note that no extra requirements are placed on the morphisms
• a group is a set plus 0-stuff (structure)—you have to equip the morphisms with (-1)-stuff (impose properties on the functions between the underlying sets)
• a monoid is a semigroup plus 0-stuff (structure)—monoids aren't a full subcategory of semigroups! (but it's "property-like" structure)
• a ringed space is a topological space plus 1-stuff (stuff)—you have to equip the morphisms with 0-stuff, in the sense that you toss out some of the equations between them, or "require the equations to be equipped with (-1)-stuff", when you add the extra component to the morphisms that goes between the sheaves of rings.

John Baez (Nov 26 2020 at 01:29):

sarahzrf said:

...maybe i should try getting into the habit of editing the nlab when i realize something is wrong.

Please do! And when you edit it, leave a comment in the box saying what you did. That way, if you make a mistake, the residents will probably notice and fix it... so you don't have to agonize so much over whether you're right (though it's good to feel pretty sure before you make a correction).

Amar Hadzihasanovic (Nov 26 2020 at 06:54):

John Baez said:

Amar Hadzihasanovic said:

Dan Doel said:

'Stuff' is objects, 'structure' is arrows, 'property' is equations between arrows.

I think you need to do swap “stuff” and “property” here?

No, Dan has it exactly right.

Maybe we are thinking of different perspectives (which may be dual in some sense? I'm not sure).

From the “forgetful functor” perspective, if I have an underlying structure,

• imposing properties selects some objects, so the forgetful functor is not essentially surjective;
• imposing structure selects some morphisms, so the forgetful functor is not full;
• imposing stuff selects some equations between morphisms, so the forgetful functor is not faithful.

Hence the “backwards” way I was thinking of the correspondence.
How do the two relate?

Todd Trimble (Nov 29 2020 at 21:11):

John Baez said:

Reid Barton said:

I thought "stuff" was typically another sort

Yes.

Nathanael Arkor said:

I had assumed that "stuff" corresponded to sorts, "structure" to operations, and "properties" to equations.

Yes, that's a good way to think about it... though structure can consist of relations as well as operations.

though now I see that this doesn't quite match some of the examples on the nLab page (e.g. an inner product on a vector space, which I would have thought was structure).

That example was wrong. It's gone now. An inner product is just structure. I wonder who put in that example.

Urs Schreiber.

Paolo Perrone (Dec 04 2020 at 03:05):

One thing that bugs me a little is that a monoidal category should be a category with extra "structure", or maybe "2-structure", not "stuff". I feel like the ladder for n-categories should be: property, structure, 2-structure, 3-structure...and stuff at the last place. Not property, structure, stuff, 2-stuff... and so on.
However, this is rather subjective, it's only the way I find most helpful.

Dan Doel (Dec 04 2020 at 04:45):

I figured if you were doing stuff like that, then "stuff, structure, property" would become "0-stuff, 1-stuff, 2-stuff."

Dan Doel (Dec 04 2020 at 04:48):

Like, adding equations to some algebraic theory is adding 2-cells. And it only cuts off there because the higher cells are assumed to be trivial.

Chad Nester (Dec 04 2020 at 06:24):

Having done my time in the KZ-monad “structure versus property” rabbit hole, I can’t say I find the formal distinctions between these things terribly helpful “on the ground”, as it were.

I propose an alternative:

Structure is what you have. Properties are what you want. Stuff is what you get.

Jason Erbele (Dec 04 2020 at 06:57):

And if you try sometimes, you get what you need.

John Baez (Dec 04 2020 at 16:02):

Paolo Perrone said:

One thing that bugs me a little is that a monoidal category should be a category with extra "structure", or maybe "2-structure", not "stuff". I feel like the ladder for n-categories should be: property, structure, 2-structure, 3-structure...and stuff at the last place. Not property, structure, stuff, 2-stuff... and so on.
However, this is rather subjective, it's only the way I find most helpful.

The terms "stuff, structure, property" were originally developed in a categorical context (categories of sets with extra stuff), so they sound a bit strange when applied to a 2-categorical context (2-categories of categories with extra 2-stuff).

In the categorical context it's very easy to believe that if you need to equip your morphisms with extra structure then you are equipping your objects with extra stuff. For example a pair of sets is a set with extra stuff (namely another set), and morphisms between pairs of sets are functions with extra structure (namely another function), not merely an extra property.

We follow the same rules in the 2-categorical context. A monoidal functor is a functor equipped with extra structure (the laxator $\phi_{x,y} : F(x) \otimes F(y) \to F(x \otimes y)$ and unit laxator $\phi_0 : F(1) \to 1$), so a monoidal category is a category equipped with extra stuff.

A pair of categories is a category equipped with extra 2-stuff, since a morphism between a pair of categories (a pair of functors) is a functor equipped with extra stuff.

John Baez (Dec 04 2020 at 16:04):

You probably know all this and just wish "stuff" in the 2-categorical context was redefined to mean "2-stuff", "structure" was redefined to mean "stuff", and so on - boosting the level of everything.

John Baez (Dec 04 2020 at 16:05):

I can sympathize with that urge, but when you get deep into n-category theory that convention would be very confusing; we want a convention where categories can be seen as discrete 2-categories without changing all the terminology regarding them.

John Baez (Dec 04 2020 at 16:10):

Another way to put it:

Properties of something are either true or false. (E.g. a group is either abelian or not.)

Structures on something form a set. (E.g. there's a set of ways you can make a set into a group.)

Stuffs on something form a category. (E.g. there's a category of ways to make a functor between monoidal categories into a monoidal functor.)

2-stuffs on something form a 2-category. (E.g. there's a 2-category of ways to make a category into a monoidal category.)

Etc.

Shea Levy (Dec 04 2020 at 16:28):

John Baez said:

Another way to put it:

Properties of something are either true or false. (E.g. a group is either abelian or not.)

Structures on something form a set. (E.g. there's a set of ways you can make a set into a group.)

Stuffs on something form a category. (E.g. there's a category of ways to make a functor between monoidal categories into a monoidal functor.)

2-stuffs on something form a 2-category. (E.g. there's a 2-category of ways to make a category into a monoidal category.)

Etc.

Could you call a property that turns out to always hold -2-stuff? :sweat_smile:

John Baez (Dec 04 2020 at 17:23):

Yes, I probably did in my paper Lectures on n-categories and cohomology, which introduced the world to n-stuff. (It was invented by James Dolan.)

Paolo Perrone (Dec 04 2020 at 18:22):

What I mean is that, to me, stuff always deserves the "last place". In 2-dimensional contexts, saying "structure, stuff, 2-stuff" instead of "structure, 2-structure, stuff" to me sounds a bit as if we said "braided, symmetric, 2-symmetric monoidal bicategory" instead of "braided, sylleptic, symmetric monoidal bicategory". To me, "stuff", like "symmetry", should always be the last one.

In any case, this is by far not a hill I want to die on - different people find different terminology suggestive. The power of category theory is precisely that it unifies different backgrounds, so it's normal that not everyone likes every convention - as long as we agree on the math.

Dan Doel (Dec 04 2020 at 18:26):

The analogous notions in HoTT come up pretty regularly. I would imagine if one were doing a similar synthetic category theory, they'd be pretty important.

Fawzi Hreiki (Dec 05 2020 at 20:29):

I have a tangential question about this stuff (pun intended) but I don't think it's worth making a new topic. On the nlab page for stuff, structure property, the definitions are given in terms of a functor $F: C \rightarrow D$ forgetting stuff/structure/properties. But it seems more natural to talk instead about $F$ preserving stuff/structure/properties.

I think it's reasonable to say that $F$ preserves stuff iff it is faithful and that it preserves structure iff it is full. I want to say that $F$ preserves properties iff it is essentially surjective but in the cases that it is not full or faithful, I'm not really sure what properties it would be preserving. Are there any natural examples that might shed light on this?

Dan Doel (Dec 05 2020 at 21:32):

I don't know if this helps, but I think the 'forgets' stuff is because you can turn it around, and treat that functor as a display map. Then the 'forgetful' display map tells you what is being equipped to things in $D$ to form things in $C$. If you used displayed categories, then you would get $C$ as the total category of a family of categories $B(x)$ displayed over $D$. And then 'stuff, structure, property' is talking about how 'truncated' these things are, like hlevels in HoTT.

Dan Doel (Dec 05 2020 at 21:38):

So, in HoTT, where you work with things displayed a lot, $\mathsf{isGroupoid}(B(x))$ means you're equipping with stuff (I think), and the forgetful functor $\mathsf{fst} : Σ_{x:D} B(x) → D$ forgets that stuff. At least, modulo groupoids vs categories.

Dan Doel (Dec 05 2020 at 22:16):

An extra sort will have an $\mathsf{hSet}$ in $B$ making it a groupoid (corner cases aside, and assuming set theoretic algebra). The type of binary operations $A → A → A$ with $A$ being an $\mathsf{hSet}$ is itself an $\mathsf{hSet}$. Equations between values in an $\mathsf{hSet}$ are an $\mathsf{hProp}$ (that's the definition).