Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeJan 20th 2019
   • PermaLink
   Author: Urs
   Format: MarkdownItexcross-linked this old entry with _[[internal category in homotopy type theory]]_ <a href="https://ncatlab.org/nlab/revision/diff/type-theoretic+definition+of+category/15">diff</a>, <a href="https://ncatlab.org/nlab/revision/type-theoretic+definition+of+category/15">v15</a>, <a href="https://ncatlab.org/nlab/show/type-theoretic+definition+of+category">current</a>

   cross-linked this old entry with internal category in homotopy type theory

   diff, v15, current

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeOct 4th 2021
   • PermaLink
   Author: Urs
   Format: MarkdownItexhereby moving the following old query box discussion out of the entry to here: *** +-- {: .query} _Anonymous from the Peanut Gallery asks_: How do we define small categories type-theoretically? It seems to me that a natural thing to try is to make "small" mean "$\mathrm{Obj}$ is a setoid (ie, element of $\mathrm{Type}_=$)", but then the coherence conditions on the type operator of morphisms make my head explode. (Namely, if $(A, \simeq)$ is a setoid, and $a \simeq a'$, then we expect $\hom(a,b) \triangleq \hom(a',b)$, but I don't see how $\triangleq$ should be defined! What should the type of homs be now, and what properties should they satisfy?) _Ulrik_: The above does define a type of small categories (given that $\mathrm{Type}$ is a type of small types). Adding equality to $\mathrm{Obj}$ (making it a setoid), defines small [[strict categories]]. Then, as you mention, we need an equality on $\mathrm{Type}$ in order to formulate the coherence condition (the type theory might do this automatically, though). To define large categories we need a larger universe of types (just like the situation in set theory). _Toby_: In other words, smallness and strictness are two separate things, although sometimes they go together. If $Type$ is the type of small types (and therefore is itself a moderate type but not a small type) and similarly for $Type_=$, then the definition above gives small categories. If $Type$ is the type of moderate types but $Type_=$ remains the type of small types with equality, then the definition above gives locally small moderate categories. If $Type$ and $Type_=$ are both types of moderate types, then the definition above gives moderate categories. Independently of this, if you change the type of $Obj$ from $Type$ to $Type_=$ (and add some coherence conditions), then you get strict categories. But it seems like there\'s still something to make your head explode: how do we define strict categories in this framework? (The tricky part is the coherence conditions in my previous parenthetical remark above.) You have the right idea that, if $a \simeq a'$, then $\hom(a,b) \triangleq \hom(a',b)$, but what you\'re missing is that $\triangleq$ means isomorphism of setoids. That is, we have a rule $$ \frac{p\coloneq a \simeq a' \quad f\colon\hom(a,b)}{\mathrm{conv}_{a,a'}f\colon\hom(a',b)} ,$$ representing a map of setoids $\mathrm{conv}_{a,a'}\colon \hom(a,b) \to \hom(a',b)$. (There is a similar rule on the other side.) Then you also need some coherence laws stating that $\mathrm{conv}_{a,a} = \id_{\hom(a,b)}$ and $\mathrm{conv}_{a',a''} \circ \mathrm{conv}_{a,a'} = \mathrm{conv}_{a,a''}$ (and two laws on the other side). I *think* that this is all. The definition that I usually use for a [[strict category]], however, is this: a __strict category__ consists of a set (of type $Type_=$, what we\'ve been calling 'setoid' above) $O$, a category (in the weak sense defined here) $C$, and an [[essentially surjective functor]] $\overline{}$ to $C$ from the [[discrete category]] on $O$. We then think of $O$ as the set of objects, the set of morphisms from $a$ to $b$ (for $a,b\colon O$) is $\hom_C(\overline{a},\overline{b})$, etc. (Again, strictness is independent of smallness; $O$ might be a small set, or a large proper class, or whatever.) _Anonymous_: Ulrik, Toby: Thank you for the advice! You're exactly right that what I've been groping for is strictness, not smallness. My true motivation is to implement a few constructions on functor categories in type theory. However, the way that the exponential in presheaf categories is usually defined has been pretty puzzling to me: given the category $\mathrm{Set}^I$, the exponential is defined as $F \Rightarrow G (X) = \mathrm{Set}(I(X, -) \times F, G)$. It's exactly the lack of strict structure on objects in the type-theoretic definition that has left me puzzled. I'll go play with the constructions you've suggested and see if I can make it work for me. However, I do have another question, though this one arises out of curiosity rather than for any practical reason. In impredicative type theories (like the calculus of constructions) you basically give up the powerset axiom in exchange for the ability to index over the universe (i.e., you can define types like $\forall \alpha:\mathrm{Type}. A(\alpha)$). It seems like you would still need a strictness condition to define constructions on functor categories, even though traditional size issues are cunningly rendered unsayable. Has anyone looked at what happens when you formalize category theory in such type theories (or for that matter, in set theories with a set of all sets, like NF)? _Ulrik_: Some quick remarks on your last questions: In impredicative type theory strong sums are inconsistent (by interpreting Girard's paradox again), so you can't form a type of meta-categories (you can still have types of types, you just can't sum over ALL types). As for NF (or NFU), the category of sets is not cartesian closed, which causes a host of problems. =-- *** <a href="https://ncatlab.org/nlab/revision/diff/type-theoretic+definition+of+category/16">diff</a>, <a href="https://ncatlab.org/nlab/revision/type-theoretic+definition+of+category/16">v16</a>, <a href="https://ncatlab.org/nlab/show/type-theoretic+definition+of+category">current</a>

   hereby moving the following old query box discussion out of the entry to here:

   ---

   +– {: .query} Anonymous from the Peanut Gallery asks: How do we define small categories type-theoretically? It seems to me that a natural thing to try is to make “small” mean “$\mathrm{Obj}$ is a setoid (ie, element of $\mathrm{Type}_=$)”, but then the coherence conditions on the type operator of morphisms make my head explode. (Namely, if $(A, \simeq)$ is a setoid, and $a \simeq a'$, then we expect $\hom(a,b) \triangleq \hom(a',b)$, but I don’t see how $\triangleq$ should be defined! What should the type of homs be now, and what properties should they satisfy?)

   Ulrik: The above does define a type of small categories (given that $\mathrm{Type}$ is a type of small types). Adding equality to $\mathrm{Obj}$ (making it a setoid), defines small strict categories. Then, as you mention, we need an equality on $\mathrm{Type}$ in order to formulate the coherence condition (the type theory might do this automatically, though). To define large categories we need a larger universe of types (just like the situation in set theory).

   Toby: In other words, smallness and strictness are two separate things, although sometimes they go together. If $Type$ is the type of small types (and therefore is itself a moderate type but not a small type) and similarly for $Type_=$, then the definition above gives small categories. If $Type$ is the type of moderate types but $Type_=$ remains the type of small types with equality, then the definition above gives locally small moderate categories. If $Type$ and $Type_=$ are both types of moderate types, then the definition above gives moderate categories. Independently of this, if you change the type of $Obj$ from $Type$ to $Type_=$ (and add some coherence conditions), then you get strict categories.

   But it seems like there's still something to make your head explode: how do we define strict categories in this framework? (The tricky part is the coherence conditions in my previous parenthetical remark above.) You have the right idea that, if $a \simeq a'$, then $\hom(a,b) \triangleq \hom(a',b)$, but what you're missing is that $\triangleq$ means isomorphism of setoids. That is, we have a rule

   $$\frac{p\coloneq a \simeq a' \quad f\colon\hom(a,b)}{\mathrm{conv}_{a,a'}f\colon\hom(a',b)} ,$$

   representing a map of setoids $\mathrm{conv}_{a,a'}\colon \hom(a,b) \to \hom(a',b)$. (There is a similar rule on the other side.) Then you also need some coherence laws stating that $\mathrm{conv}_{a,a} = \id_{\hom(a,b)}$ and $\mathrm{conv}_{a',a''} \circ \mathrm{conv}_{a,a'} = \mathrm{conv}_{a,a''}$ (and two laws on the other side). I think that this is all.

   The definition that I usually use for a strict category, however, is this: a strict category consists of a set (of type $Type_=$, what we've been calling ’setoid’ above) $O$, a category (in the weak sense defined here) $C$, and an essentially surjective functor $\overline{}$ to $C$ from the discrete category on $O$. We then think of $O$ as the set of objects, the set of morphisms from $a$ to $b$ (for $a,b\colon O$) is $\hom_C(\overline{a},\overline{b})$, etc. (Again, strictness is independent of smallness; $O$ might be a small set, or a large proper class, or whatever.)

   Anonymous: Ulrik, Toby: Thank you for the advice! You’re exactly right that what I’ve been groping for is strictness, not smallness. My true motivation is to implement a few constructions on functor categories in type theory. However, the way that the exponential in presheaf categories is usually defined has been pretty puzzling to me: given the category $\mathrm{Set}^I$, the exponential is defined as $F \Rightarrow G (X) = \mathrm{Set}(I(X, -) \times F, G)$. It’s exactly the lack of strict structure on objects in the type-theoretic definition that has left me puzzled. I’ll go play with the constructions you’ve suggested and see if I can make it work for me.

   However, I do have another question, though this one arises out of curiosity rather than for any practical reason. In impredicative type theories (like the calculus of constructions) you basically give up the powerset axiom in exchange for the ability to index over the universe (i.e., you can define types like $\forall \alpha:\mathrm{Type}. A(\alpha)$). It seems like you would still need a strictness condition to define constructions on functor categories, even though traditional size issues are cunningly rendered unsayable. Has anyone looked at what happens when you formalize category theory in such type theories (or for that matter, in set theories with a set of all sets, like NF)?

   Ulrik: Some quick remarks on your last questions: In impredicative type theory strong sums are inconsistent (by interpreting Girard’s paradox again), so you can’t form a type of meta-categories (you can still have types of types, you just can’t sum over ALL types). As for NF (or NFU), the category of sets is not cartesian closed, which causes a host of problems. =–

   ---

   diff, v16, current