Walking adjunction.

]]>Adding walking equivalence as an example.

]]>Adding the interval groupoid as the walking isomorphism (page to be created).

]]>Add reference to “free-living” as an alternative phrase.

]]>I realized that the above claim that “the underlying X of the walking X is the initial X” was a little overbroad; the situation is a bit subtler than that. The problem is that the “underlying set” functor $C(I,-)$ of a monoidal category is in general only *lax* monoidal, whereas the universal property of a “walking X qua monoidal category” is relative to *strong* monoidal functors. The argument works much better for things like categories with products, where the relevant categorical structure is preserved by the “underlying set” functor $C(1,-)$. I think we can conclude things about some walking Xs qua monoidal category, by applying the argument to multicategories instead and using the fact that a multicategory embeds fully-faithfully in the monoidal category that it freely generates (since if X is something that makes sense in a multicategory, then the walking X qua monoidal category is the free monoidal category generate by the walking X qua multicategory). But for other walking Xs qua monoidal category the claim doesn’t even make sense. I’ve updated the page walking structure with this.

I don’t see any relationship.

]]>Unsure whether this is any help, but *similar* in spirit seem some characterizations of *indiscrete categories*. Internal pointer: indiscrete category, Section 2. External pointer: e.g. page 13 in pdf of this talk: http://benedikt-ahrens.de/talks/Fields_HoTT_2016.pdf.

I added to walking structure a 2-categorical theorem that implies that usually “the underlying X of the walking X is the initial X”. This fact seems like it should be well-known, but I don’t offhand know a reference for it, can anyone give a pointer?

]]>