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.
These are just called categories in
I don’t think a set-theoretic definition of this can say “for each object” in defining the hom-sets and so on. Without the type-theoretic language, you have to be explicit about having a fibration over the space of objects with essentially discrete fibers, etc.
I would probably suggest to not give an explicit “set-theoretic” definition at all, but just point to something like Segal space.
Sorry, this is also wrong. The type of all morphisms in a precategory is not generally a set. Whoever you are, Anonymous, you may want to back off a bit and stick to edits that you understand well.
What kind of mathematical object is a precategory?
If we are in homotopy type theory, which has univalence and is though to be the internal language of an -topos, and the interpretation of the precategory definition in simplicial sets is a particular kind of Segal space with homotopically discrete homs, then the definition inside of a -topos doesn’t really define a precategory. One should really be defining it inside of an -topos, paralleling the definition of an internal -category in the article category object in an (infinity,1)-category.
Otherwise, it doesn’t make sense to solely restrict to homotopy type theory, since the type theory definition given above in the homotopy type theory section is also valid in other models of type theory such as Thomas Streicher’s groupoid model of types which do not have univalence, and it doesn’t really make sense to talk about the -category of precategories either, as there are many inequivalent such -categories depending upon the model of type theory.
There are at least two possible notions of “precategory” that one could define in mathematics: there is a type theoretic notion in line with wild category, and there is an -categorical notion in line with H-category object in an (infinity,1)-category. These two concepts are defined in the same way in (the infinity-groupoid interpretation of) homotopy type theory but differ in other type theories: In an extensional type theory or a type theory where all types are -truncated, such that types cannot be interpreted as infinity-groupoids, an H-category whose hom-infinity-groupoids are 0-truncated is not the same as a wild category whose hom-types are sets.
Agreed. I have reverted the last couple of edits. This notion of “precategory” is a type-theoretic notion. The corresponding notions in various kinds of toposes and categories have different names.
I also added a note that, as Guest pointed out, precategories don’t require univalence but make sense in arbitrary intensional type theory.
Anonymous, if you’re reading this, please don’t mix type-theoretic definitions with their semantics in higher categories. We have separate pages for category and internal category, and for group and group object, and so on, even though the latter is the internalization of the former by interpreting a definition in some suitable internal logic. A page precategory should be about the direct definition in type theory; its internalization in some model could be an “internal precategory”, although since there is already the term Segal space it doesn’t seem necessary to introduce a new one.
removed mention of infinity-groupoid from disambiguation header since precategory is a type theory concept, not an infinity-groupoid theory concept, and not all types model infinity-groupoids in all type theories.
Anonymous
FWIW, the term “precategory” appears in the nLab elsewhere – at category object in an (infinity,1)-category the term “internal precategory” refers to a segal space object. E.g. the 1-category Cat is the category of internal precategories in Set. There to the terminology is used to reserve “category” to mean including the additional assumption of Rezk completeness.
And recall that the category of segal space objects in can also be described as the category of -categories equipped with an essentially surjective functor from an -category.
I would probably call it something like a “precategory topos” or “topos precategory”.
The added definition defines a (2, 1)-preorder (equivalently, a locally setoidal prebicategory); I think we should only use the term ’precategory’ for the locally univalent (2,1)-preorders (equivalently, a locally 0-truncated prebicategory) and move the other definition to its own page on (2, 1)-preorders.
@17
On the contrary, I think the term ’category’ or ’precategory’ should refer to the notion whose homs are setoids. This is because in set theories of both the material and the structural flavour, equality of elements in a set and thus in hom-sets of a category is defined as an equivalence relation, and thus when interpreting propositions as types one should similarly lift the equality equivalence relation to setoid structure. Furthermore, most of category theory still makes sense when using setoids rather than sets, and the definition using setoids is more general. One then speaks of locally univalent categories and globally univalent categories, and univalent categories being those which are both locally univalent and globally univalent, with the caveat in that all categories in a univalent universe are locally univalent. The definition using setoids also generalizes better to higher category theory since the additional structure is already there.
The hom-setoid precategories behaves differently than the hom-set precategories. For example, for the definition of a functor between precategories, the functions for objects and of the functor have to be strongly extensional if the hom-types are setoids, while the functions only have to be extensional if the hom-types are sets (function extensionality follows from univalence or having an interval type).
The problem here is that one really needs a concept of -preorder as distinct from -(pre)category in a general intensional type theory, because of the lack of 0-truncation at the -morphism level (the preorder level) in the definition of a -preorder, and the lack of univalence in a general intensional type theory which implies that all preorders are posets and thus 0-truncated.
I think composition of morphisms also has to be strongly extensional for the setoid definition to work. And agreed that the setoid definition should go on its own page.
moved added section w/different definition to (2,1)-preorder and left a comment on this article stating that the locally univalent (2,1)-preorders are the precategories.
Anonymous
strongly extensional means “preserving an apartness relation”, what we are looking for here is “preserving the equivalence relation”.
From the nLab article on equivalence relation:
A set equipped with an equivalence relation is sometimes called a setoid, although at other times that term is used for a pseudo-equivalence relation instead. This terminology is particularly common in foundations of mathematics where quotient sets don’t always exist and the above equivalence to a set cannot be carried out. However, arguably this is a terminological mismatch, and such people should say ‘set’ where they say ‘setoid’ and something else (such as ‘preset’, ‘type’, or ‘completely presented set’) where they say ‘set’. (See Bishop set and page 9 of these lecture notes.)
The homotopy type theory community uses terms differently from other parts of mathematics. In homotopy type theory, a set is a 0-truncated type, and a setoid is a type with an equivalence relation, and a univalent setoid as a setoid which satisfies a Rezk completion condition and thus equivalent to a set, so there are really just setoids and sets.
To reflect usage elsewhere (such as set theory), one really should be talking about 0-truncated types as being 0-truncated, a set as a type with an equivalence relation, and a univalent set as a set which satisfies Rezk completeness and thus equivalent to a 0-truncated type, so there are really just sets and univalent sets.
Similarly with (2, 1)-preorder/precategory/category vs category/locally univalent category/univalent category, etc.
A set equipped with an equivalence relation is sometimes called a setoid, although at other times that term is used for a pseudo-equivalence relation instead.
Is a setoid a type with an equivalence relation, or a set with an equivalence relation? Those two things are different in intensional type theory, in the same way a type with a preorder is different from a proset, and preceding discussion seems to imply that a setoid isn’t 0-truncated.
Setoids are thin pregroupoids so one could call a 0-truncated setoid a strict setoid.
Similarly to the case with ’category’, the term ’set’ is overloaded. One should use ’h-set’ for a 0-truncated type and ’Bishop set’/’setoid’ for a type with a prop-valued equivalence relation to avoid confusion.
In the context of homotopy type theory, it is proper to use the word “set” for a 0-type, because that is the correct notion of set in that foundational system. It’s reasonable to emphasize this by saying “h-set” or “0-type” at the first usage in a particular context, but thereafter it is okay to revert to “set”.
A setoid in intensional type theory does not generally refer to a type with a prop-valued equivalence relation, but a type-valued one. I don’t know of any evidence for the claim in #24 that this is any different in homotopy type theory.
1 to 29 of 29