Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.
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 :-)).
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.
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.
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.
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.
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.
Clarified that the existing sections pertain to set-level foundations, and added a new section on skeleta in intensional/homotopy type theory.
There are two query boxes on this page.
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)
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).
added pointer to:
added pointer to:
added pointer to:
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.
=–
1 to 24 of 24