\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{type-theoretic definition of category}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{category_theory}{}\paragraph*{{Category theory}}\label{category_theory}

[[!include category theory - contents]]

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{typetheoretic_definition_of_category}{}\section*{{Type-theoretic definition of category}}\label{typetheoretic_definition_of_category}

\noindent\hyperlink{motivation}{Motivation}\dotfill \pageref*{motivation} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{discussion}{Discussion}\dotfill \pageref*{discussion} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak


\hypertarget{motivation}{}\subsection*{{Motivation}}\label{motivation}

There are two main styles of definition of [[category]] in the literature: one which immediately generalises to the usual definition of [[internal category]] and one which immediately generalises to the usual definition of [[enriched category]]. Here we consider the latter definition, and show how it may naturally be expressed in [[dependent type theory]].

Note that in a [[type theory]] without [[identity types]], where [[types]] are [[presets]] (without an inherent [[equality predicate]]), it is not manifestly possible to express so-called [[evil]] ideas in category theory; thus categories are not necessarily [[strict category|strict]]. In [[homotopy type theory]], we have identity types, but they are not [[extensional type theory|extensional]]; thus it is also possible to define non-strict categories there (but there is a subtlety; see below).

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

In a [[dependent type theory]] with [[dependent record type|dependent record types]] we can define a type of categories as follows.

We use a two-dimensional syntax, which is convenient to allow inference of [[implicit parameter|implicit parameters]], and to signify notation. We read the horizontal line as a rule, so for instance the second line means that whenever $a$ and $b$ have type $\mathrm{Obj}$, then we have a type $\hom(a,b)$ (with equality).

The notation $p\coloneq P$ signifies that $p$ is a proof of the [[proposition]] $P$ (under [[propositions as types]] or [[propositions as some types]], this may be the same as $p\colon P$, but many type theories treat propositions as distinct from types).

\begin{displaymath}
\begin{aligned}
  \biggl\{&\mathrm{Obj}\colon\mathrm{Type}, \\
    &\frac{a,b\colon\mathrm{Obj}}{\hom(a,b)\colon\mathrm{Type}_=}, \\
    &\frac{a\colon\mathrm{Obj}}{1_a\colon\hom(a,a)}, \\
    &\frac{f\colon\hom(b,c) \quad g\colon\hom(a,b)}{f\circ g\colon\hom(a,c)}, \\
    &\frac{g\colon\hom(a,b)}{\mathrm{left}\text{-}\mathrm{unit}\coloneq 1_b\circ g=g}, \\
    &\frac{f\colon\hom(a,b)}{\mathrm{right}\text{-}\mathrm{unit}\coloneq f\circ 1_a=f}, \\
    &\frac{f\colon\hom(c,d) \quad
        g\colon\hom(b,c) \quad h\colon\hom(a,b)}{\circ\text{-}\mathrm{assoc}\coloneq f\circ(g\circ h) =
        (f\circ g)\circ h} \\
  &\!\biggr\}
\end{aligned}
\end{displaymath}
Here, $\mathrm{Type}$ is a type of types, and $\mathrm{Type}_=$ is a type of types with equality predicates (we may or may not have $\mathrm{Type}=\mathrm{Type}_=$). Specifically:

\begin{itemize}%
\item In [[extensional type theory]] (with extensional [[identity types]]), we have $\mathrm{Type} = \mathrm{Type}_=$, and the above definition simply makes no use of the equality predicate on the type of objects. In this case we obtain [[strict categories]], although that is not immediately visible from the definition.


\item In dependent type theory without identity types, basically the only option for $\mathrm{Type}_=$ is the type of [[setoids]]. In this case we obtain a notion of non-strict category, since the type of objects has no equality predicate at all.


\item In [[homotopy type theory]], it is natural to take $\mathrm{Type}_=$ to be the type of [[h-sets]]: types whose identity/path types behave extensionally. We should also restrict the [[homotopy level]] of the type of objects, however, since a true 1-category should have no more than a 1-groupoid of objects; thus $\mathrm{Type}$ in the definition above is really the type of [[h-groupoids]] instead of the type of \emph{all} small types. That is, we should take $\mathrm{Obj}$ to be $1$-truncated in addition to taking each $\hom(a,b)$ to be $0$-truncated.

This gives a notion of non-strict category (since there is no equality predicate on a $1$-truncated type other than isomorphism). However, it is not quite the right definition of ``$1$-category'' in homotopy type theory, because nothing requires that the paths in $\mathrm{Obj}$ are the same as the isomorphisms defined categorically. We need to impose a version of the ``completeness'' condition on a [[complete Segal space]]; in other words, we require that the [[core]] of the category be the [[equivalence of groupoids|equivalent]] as a [[groupoid]] to the original type of objects.



\end{itemize}
\hypertarget{discussion}{}\subsection*{{Discussion}}\label{discussion}

The defined type of categories cannot itself be a member of $\mathrm{Type}$, otherwise we run into [[Girard's paradox]]. This is related to the size issues for categories.

\emph{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?)

\emph{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).

\emph{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

\begin{displaymath}
\frac{p\coloneq a \simeq a' \quad f\colon\hom(a,b)}{\mathrm{conv}_{a,a'}f\colon\hom(a',b)} ,
\end{displaymath}
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 \emph{think} that this is all.

The definition that I usually use for a [[strict category]], however, is this: a \textbf{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.)

\emph{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)?

\emph{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.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[fully formal definition of ETCS]]


\item [[internal category in homotopy type theory]]



\end{itemize}
[[!redirects type-theoretic definition of category]] [[!redirects type-theoretic definition of a category]] [[!redirects type-theoretic definition of categories]] [[!redirects type-theoretic definitions of category]] [[!redirects type-theoretic definitions of a category]] [[!redirects type-theoretic definitions of categories]] [[!redirects preset-theoretic definition of category]] [[!redirects preset-theoretic definition of a category]] [[!redirects preset-theoretic definition of categories]] [[!redirects preset-theoretic definitions of category]] [[!redirects preset-theoretic definitions of a category]] [[!redirects preset-theoretic definitions of categories]]



\end{document}