\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*{strict category}

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

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

[[!include category theory - contents]]

\hypertarget{strict_categories}{}\section*{{Strict categories}}\label{strict_categories}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{foundational_choices}{Foundational choices}\dotfill \pageref*{foundational_choices} \linebreak
\noindent\hyperlink{set_theory_with_ac}{Set theory with AC}\dotfill \pageref*{set_theory_with_ac} \linebreak
\noindent\hyperlink{set_theory_without_ac}{Set theory without AC}\dotfill \pageref*{set_theory_without_ac} \linebreak
\noindent\hyperlink{type_and_preset_theories_with_equality}{Type and preset theories with equality}\dotfill \pageref*{type_and_preset_theories_with_equality} \linebreak
\noindent\hyperlink{type_and_preset_theories_without_equality}{Type and preset theories without equality}\dotfill \pageref*{type_and_preset_theories_without_equality} \linebreak
\noindent\hyperlink{homotopy_type_theory}{Homotopy type theory}\dotfill \pageref*{homotopy_type_theory} \linebreak
\noindent\hyperlink{fibered_categories}{Fibered categories}\dotfill \pageref*{fibered_categories} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{strict_higher_categories}{Strict higher categories}\dotfill \pageref*{strict_higher_categories} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A \textbf{strict category} is a [[category]] together with the structure of a [[set]] (or [[class]]) on its collection of [[objects]]; in particular, the objects can be compared for [[equality]] (not merely [[isomorphism]]). In contrast, a \textbf{weak category} is a category \emph{without} such structure. Similarly, a \textbf{strict functor} is one which preserves equality of objects: $F(x) = F(y)$ if $x = y$. (NB: this is not inherently size-related---both [[large category|large]] and [[small categories]] can be either strict or weak.)

If we use [[set theory|set-theoretic]] [[foundations]] for category theory, then by definition, a category comes with a set (or class) of objects, and therefore admits the structure of a strict category in a canonical way. Thus, in this case, it is possible to ignore the adjective ``strict'' in ``strict category'', while a ``strict functor'' simply means a ``non-[[anafunctor|ana]] functor'' (the usual default meaning of `functor', but not necessarily the best concept).

If we additionally assume the (possibly global) [[axiom of choice]], then not only is any category [[equivalence of categories|equivalent]] to a canonical strict category, but every (ana-)functor is [[naturally isomorphic functors|naturally isomorphic]] to a strict functor, so the notions have little to no mathematical content. But in other foundations, these facts may not be true.

Moreover, even in set-theoretic foundations with global $AC$, the notion of strict category is not meaningless: calling a category strict signals that we intend to \emph{make use of} the equality relation on its objects. When taking the [[nPOV]], we often adopt the [[philosophy|philosophical]] position that [[category theory]] is fundamentally about weak categories; see the discussion at [[principle of equivalence]]. However, strict categories still do occasionally arise in mathematical practice; see the examples below.

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

In order to formulate a foundation-independent definition, we make the following assumptions. Ignoring [[size issues]], suppose that we have a [[bicategory]] $Cat$ consisting of weak [[categories]], [[functors]] (some of which are [[essentially surjective functor|essentially surjective]]), and [[natural transformations]] (some of which are [[natural isomorphisms]]). Suppose also that we have a [[category]] $Set$ consisting of [[sets]] and [[functions]], and a [[functor]] $Disc\colon Set \to \Cat$ taking each set to the [[discrete category]] on that set. Note that we do not assume the existence of an ``underlying set of objects'' functor $Cat\to Set$.

In this context, a \textbf{strict category} $C$ consists of

\begin{itemize}%
\item a set $Ob(C)$ (to be thought of as the set of [[objects]] of $C$),
\item a category $Wk(C)$ (to be thought of as the underlying weak category of $C$), and
\item an essentially surjective functor $cl(C)\colon Disc(Ob(C)) \to C$ (to be thought of as taking each object of $C$ to its [[clique]], more or less, in $C$).

\end{itemize}
A \textbf{strict functor} $F$ from $C$ to $D$ (both strict categories) consists of

\begin{itemize}%
\item a function $Ob(F)\colon Ob(C) \to Ob(D)$,
\item a functor $Wk(F)\colon Wk(C) \to Wk(D)$, and
\item a natural isomorphism $cl(F)\colon cl(C) ; Wk(F) \to Disc(Ob(F)) ; cl(D)$.

\end{itemize}
Two strict functors $F, G\colon C \to D$ are \textbf{equal} if

\begin{itemize}%
\item $Ob(F) = Ob(G)$ and
\item there is a (necessarily unique) natural isomorphism from $Wk(F)$ to $Wk(G)$ modulo which $cl(F)$ equals $cl(G)$.

\end{itemize}
There is an obvious notion of [[composition]] that defines a [[1-category]] $Str Cat$ of strict categories and (equality classes of) strict functors. Note that this 1-category has a strictly associative and unital composition law, even if $Cat$ is only a [[bicategory]]. (However, $Str Cat$ is not \emph{itself} a strict category, unless the assumed category $Set$ is strict.) We have a [[forgetful functor]] $Ob\colon Str Cat \to Set$ and a [[pseudofunctor]] $Wk\colon Str Cat \to Cat$.

Finally, a \textbf{natural transformation} between two strict functors $F$ and $G$ is simply

\begin{itemize}%
\item a natural transformation from $Wk(F)$ to $Wk(G)$.

\end{itemize}
(That is, a [[natural transformation]] between strict functors is automatically strict.) With these as 2-cells, we have a [[strict 2-category]] of strict categories, strict functors, and natural transformations.

\begin{uremark}
An equivalent definition is that a strict category is an $\mathcal{M}$-[[M-category|category]] whose underlying category of tight morphisms is discrete, while a strict functor is an $\mathcal{M}$-functor. In this case, the tight morphisms (which are necessarily [[isomorphisms]]) are sometimes called \textbf{special isomorphisms}.

\end{uremark}
\hypertarget{foundational_choices}{}\subsection*{{Foundational choices}}\label{foundational_choices}

We now make the above schematic definition explicit in terms of various different foundational systems.

\hypertarget{set_theory_with_ac}{}\subsubsection*{{Set theory with AC}}\label{set_theory_with_ac}

In [[classical mathematics|classical]] [[set theory|set-theoretic]] foundations including the [[axiom of choice]], we take $Cat$ to be the [[strict 2-category]] consisting of (say small) [[categories]], [[functors]], and [[natural transformations]], defined in any of the traditional ways. The functor $Disc\colon Set \to Cat$ is [[left adjoint]] to the functor $Ob\colon Cat \to Set$, and thus $Str Cat$ is a subcategory of the [[Freyd cover]] of $Cat$.

In this case, the functor $Wk\colon Str Cat \to Cat$ has a [[right adjoint]] which takes a category $C$ to the strict category $Disc(Ob(C)) \to C$. The adjunction counit is literally the identity, while the adjunction unit consists of [[equivalences]] (but not isomorphisms) in the strict $2$-category $Str Cat$. Thus, $Str Cat$ is equivalent to $Cat$ (as a bicategory).

The right adjoint $Cat \to Str Cat$ also has a further right adjoint defined as follows: given a strict category $C$, let $C'$ be the category with $Ob(C)$ as its set of objects, and morphisms induced from those in $Wk(C)$. The unit of this adjunction again consists of identities, while the counit consists of equivalences in $Str Cat$.

This analysis applies not only to [[material set theories]] such as [[ZFC]], but also [[structural set theories]] such as [[ETCS]] and [[SEAR]], as long as they have the axiom of choice.

\hypertarget{set_theory_without_ac}{}\subsubsection*{{Set theory without AC}}\label{set_theory_without_ac}

In this case, it is usually best to define [[Cat]] to be the bicategory of categories, [[anafunctors]], and natural transformations. Now although every category has an underlying set of objects, we no longer have a functor $Ob\colon Cat \to Set$. It is still true that every category $C$ admits the structure of a strict category in a canonical way (with $Ob(C)$ its set of objects), but not every strict category necessarily arises in this way, and not every morphism $C \to D$ in $Cat$ (i.e. anafunctor) is a strict functor relative to the canonical strict-category structures of $C$ and $D$. In fact, an anafunctor is a strict functor precisely when it is naturally isomorphic to an ordinary (non-ana) functor.

If we instead defined $Cat$ to consist only of non-ana functors, then everything would happen exactly as with AC, except that neither adjunction would be an equivalence.

\hypertarget{type_and_preset_theories_with_equality}{}\subsubsection*{{Type and preset theories with equality}}\label{type_and_preset_theories_with_equality}

We include under this heading all theories in which the basic objects, generally called [[type theory|types]] or [[presets]] (and sometimes even called `sets'), come with an [[equality]] [[relation]], but the notion of [[set]] is a defined one. Generally, the issue is that types (or presets) do not admit [[quotient object|quotients]], and so a \textbf{set} is defined to be a type equipped with an [[equivalence relation]] called ``equality'' (sometimes called a [[setoid]] in this context, especially if the types or presets are themselves confusingly called `sets').

In this case, it is natural to define a \emph{category} to have only a type/preset of objects, but a set(oid) of morphisms between each pair of objects; see [[type-theoretic definition of category]]. Now every category still has an underlying set of objects, but not every set is the set of objects underlying some category; only the [[completely presented sets]] have this property.

Again, it is true that every category can be made into a strict one in a canonical way, but that not every strict category arises in this way. This is a different sort of failure than in set theory without $AC$, and can happen even in the presence of full $AC$ (even for setoids). For instance, consider the [[discrete category]] on the set of [[real numbers]]. Of course this depends on specifics, but typically, there is no type of real numbers per se but only a type of Cauchy (pre)sequences of rational numbers (see [[Cauchy real number]]). To get the set of real numbers, we must consider this type together with a certain equivalence relation, a setoid. The discrete category on the set of real numbers is essentially the exact same construction, now with a note that parallel morphisms are always defined to be equal. The automatic notion of equality on the objects of this category is equality of Cauchy (pre)sequences, but the desired notion of equality for this discrete category as a strict category is isomorphism, which is equality of real numbers. So while this category may be automatically a strict category, it is a strict category in the wrong way. (This is not a perfect example, since, given $AC$, the discrete category of real numbers is still equivalent to the discrete category of Cauchy sequences and therefore does arise as a canonical strict category, up to equivalence.)

Note that we still have a functor $Disc\colon Set \to Cat$ which regards an equivalence relation on a type $A$ as a groupoid with $A$ as its type of objects. The resulting structure of strict categories behaves much like it does in set theory without AC.

\hypertarget{type_and_preset_theories_without_equality}{}\subsubsection*{{Type and preset theories without equality}}\label{type_and_preset_theories_without_equality}

If types or presets do not come with a notion of equality, as in some preset theories and [[SEAR+?]], then a category does not in general even \emph{have} an ``underlying set of objects'', so a category cannot be made into a strict category in any canonical way. But defining sets as presets with equivalence relations as before, we still have $Disc\colon Set \to Cat$, and we can define strict categories, constructing specific examples as wanted.

\hypertarget{homotopy_type_theory}{}\subsubsection*{{Homotopy type theory}}\label{homotopy_type_theory}

If [[type theory]] is treated as a theory of set-like objects, then it behaves as above, whether [[extensional type theory|extensional]] or [[intensional type theory|intensional]]. However, if we take the point of view of [[homotopy type theory]], then the basic objects of the theory are [[homotopy types]], a.k.a. [[∞-groupoids]]. A \emph{set} is now defined to be an [[h-set]], i.e. a [[truncated object|0-truncated]] type.

Now the natural definition of (1-)category is something like a [[complete Segal space]], where the type of objects is 1-truncated (a [[groupoid]]) and equivalent to the [[core]] of the category. Now (even though identity types exist in HoTT), not every category has an underlying \emph{set} of objects, so again a category cannot be made into a strict category in any canonical way. But again, we still have $Disc\colon Set \to Cat$ and we can define strict categories.

\hypertarget{fibered_categories}{}\subsubsection*{{Fibered categories}}\label{fibered_categories}

In [[Jean Bénabou]]`s 1985 paper \emph{[[Fibered categories and the foundations of naive category theory]]}, it is argued that the right notion of a category in/over another category $\mathbf{B}$ is given by a [[Grothendieck fibration|fibered category]] $p\colon \mathbf{F} \to \mathbf{B}$, possibly with some additional structure corresponding to the ``definability'' (representability of certain sieves of $\mathbf{B}$) of equality of parallel pairs, isomorphisms, etc. (See [[indexed category]] for more motivation.) In this context, equality of objects is available precisely when the fibration is [[split fibration|split]].

In particular, if $\mathbf{B}$ is locally small and has [[pullback|pullbacks]], then an [[internal category]] object $C$ in $\mathbf{B}$ (in the traditional sense) gives rise to an honest functor $\mathbf{B} (-, C)\colon \mathbf{B}^{op} \to Cat$ and so a split fibration $\int_\mathbf{B} \mathbf{B} (-, C) \to \mathbf{B}$ by the [[Grothendieck construction]].

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

There are some at [[M-category]], to put also here.

\hypertarget{strict_higher_categories}{}\subsection*{{Strict higher categories}}\label{strict_higher_categories}

The notion of strict category is related to the notion of strictness in [[higher category theory]].

For instance, a [[2-category]] must have strict categories as its [[hom-categories]] in order to write down the definition of [[strict 2-category]]; a similar remark holds for [[strict 2-functors]]. As such, strictness in the sense of this page matches the usual sense of strictness in a ``local'' sense (every strict 2-category is locally a strict 1-category). However, we now get a notion of \textbf{strict $2$-natural transformation} as a [[2-natural transformation]] that preserves equality (that is, if two objects are equal, then so are the corresponding components of the natural transformation). (All [[modifications]] between strict transformations are automatically strict \ldots{} until we get to $3$-categories, of course!)

On the other hand, the underlying 1-category of a [[strict 2-category]] (its objects and 1-morphisms) need not be a strict 1-category. For instance, this is the case for the strict 2-category $Str Cat$ defined in a structural set theory, such as [[SEAR]], in which there is no equality predicate on sets. For a fully consistent terminology, we could say `locally strict $2$-category' in place of `strict $2$-category', but this is unlikely to catch on. Some system of numbered strictness ($1$-strict, $2$-strict, etc) might also work.

[[!redirects strict category]] [[!redirects strict categories]] [[!redirects strict functor]] [[!redirects strict functors]] [[!redirects strict groupoid]] [[!redirects strict groupoids]] [[!redirects StrCat]] [[!redirects Str Cat]]

[[!redirects weak category]] [[!redirects weak categories]]



\end{document}