moving this old query-box out of the entry, which seems to have resolved itself:

+– {: .query} I removed ’non-ana’, since I don't think that ’strongly equivalent’ would ever be used in an ’ana-’ sense. —Toby

Addendum: Actually, I don't know why I asked whether you meant weakly or strongly here, since obviously one can prove that two ana-equivalent categories are weakly equivalent! It seems that the discussion above used the terms ’equivalence’ and ’ana-equivalence’ where equivalence of categories uses ’strong equivalence’ and ’weak equivalence’ or ’ana-equivalence’; so I just changed it. And then I added another entry, which maybe you should remove if Freyd & Scedrov don't actually address it. On the other hand, if they really talk about weak equivalence instead of ana-equivalence (although if they define it in elementary terms, it's hard to tell the difference), maybe there's no need to say ’ana-’ at all on this page.

=–

]]>

Added the category of Archimedean ordered fields and monotonic field homomorphisms to the list of examples - impredicatively this is just the subset of the power set of the real numbers consisting of the Archimedean ordered subfields of the real numbers.

Peter Wells

]]>added pointer to:

- Birgit Richter, §2.6 in:
*From categories to homotopy theory*, Cambridge Studies in Advanced Mathematics**188**, Cambridge University Press (2020) [doi:10.1017/9781108855891, book webpage, pdf]

added pointer to:

- Emily Riehl, p. 34 in:
*Category Theory in Context*, Dover Publications (2017) [pdf]

added pointer to:

- Saunders MacLane, p. 91 of:
*Categories for the Working Mathematician*, Graduate texts in mathematics, Springer (1971) [doi:10.1007/978-1-4757-4721-8]

added a sentence on and a pointer to the special case of *skeletal groupoids* (a page that had been missing, even as a redirect, but which I am creating now).

It seems to me that this addendum should be superfluous unless the previous sentence was really unclear. So I took the liberty of instead adjusting the lead-in sentence a little, and then appending a sentence pointing to gaunt categories. Also added the qualification that we are talking about strict categories.

(all here)

]]>Point out that skeletal categories can have non-trivial automorphisms.

]]>There are two query boxes on this page.

]]>Clarified that the existing sections pertain to set-level foundations, and added a new section on skeleta in intensional/homotopy type theory.

]]>Most of the “Definition” section belonged in a different section like “Constructions”.

]]>I agree that it doesn’t make sense to talk about a particular category violating the POE. What violates the POE is the *notion* of skeletal category.

A strict category $C$ is skeletal if for all objects $A:Ob(C)$ and $B:Ob(C)$ there is a function $\mathrm{truncIsoToId}(A, B):\vert A \cong B \vert \to A = B$ from the propositional truncation of the set of isomorphisms $\vert A \cong B \vert$ to the identity type $A = B$. (I don’t see how this violates the principle of equivalence btw, skeletal strict categories are perfectly definable in homotopy type theory)

A strict category $C$ is univalent if the canonical function $\mathrm{IdToIso}(A, B):A = B \to A \cong B$ is an equivalence. The homotopy inverse of $\mathrm{IdToIso}(A, B)$ is called $\mathrm{IsoToId}(A, B)$. But since $A = B$ is a proposition for all objects $A$ and $B$ in a strict category, $A \cong B$ is a proposition as well if the strict category is univalent, and thus $A \cong B$ is equivalent to its propositional truncation $\vert A \cong B \vert$. And so the Rezk completion condition on a strict univalent category is what makes a strict univalent category skeletal.

]]>Hurkyl, it is enough for the core of a univalent category to be a setoid, because the Rezk completion condition of a univalent category makes every setoid into a set.

]]>It’s not enough for the core to be a setoid: a univalent category is skeletal iff its core is a *set*.

Furthermore, skeletal categories need not be univalent.

I think the phrase “violate the principle of equivalence” is being used in a very strange way. How can a *category* violate it? AFAICT, the relevant fact in this spirit is that $Ob : Cat \to Set$ does not preserve equivalences.

adding more examples of skeletal categories

Anonymous

]]>strict univalent categories are skeletal but do not violate the principle of equivalence.

Anonymous

]]>have added an Examples-section “Posets as skeleta of prosets” (here). So far it is just a glorified pointer to the new entry *relation between preorders and (0,1)-categories*.

Added coherence isomorphisms for skeleton endo-pseudofunctor.

]]>Slightly changed definition section to explicitly name skeletons vs weak skeletons, and added a simple theorem about the stronger sense of skeletons without without choice.

The changes to the definition section might be controversial, as I named the weaker version a ’weak skeleton’ and defined a skeleton to be the classical notion. If there is more standard terminology it should be put in this section.

]]>Apologies that you had to battle the spam filter Alec, it is suspicious of large edits (but becomes less suspicious the more of an editing history one has, until it eventually allow one free reign :-)).

]]>In the case of quasi-categories, I imagine Lurie’s “minimal inner fibrations” (Higher Topos Theory, 2.3.3) would be the right notion of ∞-skeleton to consider.

I guess then the right thing for simplicial categories is to combine the evident condition on objects with requiring the hom-spaces be minimal Kan fibrations.

]]>Added discussion of skeletons as an endo-2-functor on the 2-category of categories, skeletons of indexed categories and skeletons of fibrations. There is probably a more general discussion to be had at the $\infty$-level, but I’m not sure what $\infty$-skeleta look like at the moment.

]]>Test edit, I can’t seem to get the page to accept the larger edit I’ve made.

]]>