CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> strict category in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> strict category </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/18711/#Item_1" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Strict categories</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="category_theory">Category theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></strong></p> <h2 id="sidebar_concepts">Concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/category">category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Cat">Cat</a></p> </li> </ul> <h2 id="sidebar_universal_constructions">Universal constructions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/universal+construction">universal construction</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/representable+functor">representable functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor">adjoint functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/limit">limit</a>/<a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/weighted+limit">weighted limit</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/end">end</a>/<a class="existingWikiWord" href="/nlab/show/coend">coend</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kan+extension">Kan extension</a></p> </li> </ul> </li> </ul> <h2 id="sidebar_theorems">Theorems</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Yoneda+lemma">Yoneda lemma</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Isbell+duality">Isbell duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Grothendieck+construction">Grothendieck construction</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+functor+theorem">adjoint functor theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monadicity+theorem">monadicity theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/adjoint+lifting+theorem">adjoint lifting theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Tannaka+duality">Tannaka duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Gabriel-Ulmer+duality">Gabriel-Ulmer duality</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/small+object+argument">small object argument</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Freyd-Mitchell+embedding+theorem">Freyd-Mitchell embedding theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a></p> </li> </ul> <h2 id="sidebar_extensions">Extensions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/sheaf+and+topos+theory">sheaf and topos theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/enriched+category+theory">enriched category theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a></p> </li> </ul> <h2 id="sidebar_applications">Applications</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/applications+of+%28higher%29+category+theory">applications of (higher) category theory</a></li> </ul> <div> <p> <a href="/nlab/edit/category+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="strict_categories">Strict categories</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#definition'>Definition</a></li> <li><a href='#foundational_choices'>Foundational choices</a></li> <ul> <li><a href='#set_theory_with_ac'>Set theory with AC</a></li> <li><a href='#set_theory_without_ac'>Set theory without AC</a></li> <li><a href='#type_and_preset_theories_with_equality'>Type and preset theories with equality</a></li> <li><a href='#type_and_preset_theories_without_equality'>Type and preset theories without equality</a></li> <li><a href='#homotopy_type_theory'>Homotopy type theory</a></li> <li><a href='#fibered_categories'>Fibered categories</a></li> </ul> <li><a href='#examples'>Examples</a></li> <li><a href='#strict_higher_categories'>Strict higher categories</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>A <strong>strict category</strong> is a <a class="existingWikiWord" href="/nlab/show/category">category</a> together with the <a class="existingWikiWord" href="/nlab/show/structure">structure</a> of a <a class="existingWikiWord" href="/nlab/show/set">set</a> (or <a class="existingWikiWord" href="/nlab/show/class">class</a>) on its collection of <a class="existingWikiWord" href="/nlab/show/objects">objects</a>; in particular, the objects can be compared for <a class="existingWikiWord" href="/nlab/show/equality">equality</a> (not merely <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphism</a>). In contrast, a <strong>weak category</strong> is a category <em>without</em> such structure. Similarly, a <strong>strict functor</strong> is one which preserves equality of objects: <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>F</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">F(x) = F(y)</annotation></semantics></math> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>=</mo><mi>y</mi></mrow><annotation encoding="application/x-tex">x = y</annotation></semantics></math>. (NB: this is not inherently size-related—both <a class="existingWikiWord" href="/nlab/show/large+category">large</a> and <a class="existingWikiWord" href="/nlab/show/small+categories">small categories</a> can be either strict or weak.)</p> <p>If we use <a class="existingWikiWord" href="/nlab/show/set+theory">set-theoretic</a> <a class="existingWikiWord" href="/nlab/show/foundations">foundations</a> 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-<a class="existingWikiWord" href="/nlab/show/anafunctor">ana</a> functor” (the usual default meaning of ‘functor’, but not necessarily the best concept).</p> <p>If we additionally assume the (possibly global) <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>, then not only is any category <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalent</a> to a canonical strict category, but every (ana-)functor is <a class="existingWikiWord" href="/nlab/show/naturally+isomorphic+functors">naturally isomorphic</a> to a strict functor, so the notions have little to no mathematical content. But in other foundations, these facts may not be true.</p> <p>Moreover, even in set-theoretic foundations with global <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>AC</mi></mrow><annotation encoding="application/x-tex">AC</annotation></semantics></math>, the notion of strict category is not meaningless: calling a category strict signals that we intend to <em>make use of</em> the equality relation on its objects. When taking the <a class="existingWikiWord" href="/nlab/show/nPOV">nPOV</a>, we often adopt the <a class="existingWikiWord" href="/nlab/show/philosophy">philosophical</a> position that <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> is fundamentally about weak categories; see the discussion at <a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a>. However, strict categories still do occasionally arise in mathematical practice; see the examples below.</p> <h2 id="definition">Definition</h2> <p>In order to formulate a foundation-independent definition, we make the following assumptions. Ignoring <a class="existingWikiWord" href="/nlab/show/size+issues">size issues</a>, suppose that we have a <a class="existingWikiWord" href="/nlab/show/bicategory">bicategory</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math> consisting of weak <a class="existingWikiWord" href="/nlab/show/categories">categories</a>, <a class="existingWikiWord" href="/nlab/show/functors">functors</a> (some of which are <a class="existingWikiWord" href="/nlab/show/essentially+surjective+functor">essentially surjective</a>), and <a class="existingWikiWord" href="/nlab/show/natural+transformations">natural transformations</a> (some of which are <a class="existingWikiWord" href="/nlab/show/natural+isomorphisms">natural isomorphisms</a>). Suppose also that we have a <a class="existingWikiWord" href="/nlab/show/category">category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> consisting of <a class="existingWikiWord" href="/nlab/show/sets">sets</a> and <a class="existingWikiWord" href="/nlab/show/functions">functions</a>, and a <a class="existingWikiWord" href="/nlab/show/functor">functor</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Disc</mi><mo lspace="verythinmathspace">:</mo><mi>Set</mi><mo>→</mo><mo lspace="0em" rspace="thinmathspace">Cat</mo></mrow><annotation encoding="application/x-tex">Disc\colon Set \to \Cat</annotation></semantics></math> taking each set to the <a class="existingWikiWord" href="/nlab/show/discrete+category">discrete category</a> on that set. Note that we do not assume the existence of an “underlying set of objects” functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">Cat\to Set</annotation></semantics></math>.</p> <p>In this context, a <strong>strict category</strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> consists of</p> <ul> <li>a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Ob(C)</annotation></semantics></math> (to be thought of as the set of <a class="existingWikiWord" href="/nlab/show/objects">objects</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>),</li> <li>a category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Wk</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Wk(C)</annotation></semantics></math> (to be thought of as the underlying weak category of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>), and</li> <li>an essentially surjective functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>cl</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>Disc</mi><mo stretchy="false">(</mo><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>→</mo><mi>Wk</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">cl(C)\colon Disc(Ob(C)) \to Wk(C)</annotation></semantics></math> (to be thought of as taking each object of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> to its <a class="existingWikiWord" href="/nlab/show/clique">clique</a>, more or less, in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>).</li> </ul> <p>A <strong>strict functor</strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> (both strict categories) consists of</p> <ul> <li>a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo stretchy="false">(</mo><mi>F</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo>→</mo><mi>Ob</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Ob(F)\colon Ob(C) \to Ob(D)</annotation></semantics></math>,</li> <li>a functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Wk</mi><mo stretchy="false">(</mo><mi>F</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>Wk</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo>→</mo><mi>Wk</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Wk(F)\colon Wk(C) \to Wk(D)</annotation></semantics></math>, and</li> <li>a natural isomorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>cl</mi><mo stretchy="false">(</mo><mi>F</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>cl</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo>;</mo><mi>Wk</mi><mo stretchy="false">(</mo><mi>F</mi><mo stretchy="false">)</mo><mo>→</mo><mi>Disc</mi><mo stretchy="false">(</mo><mi>Ob</mi><mo stretchy="false">(</mo><mi>F</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>;</mo><mi>cl</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">cl(F)\colon cl(C) ; Wk(F) \to Disc(Ob(F)) ; cl(D)</annotation></semantics></math>.</li> </ul> <p>Two strict functors <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi><mo>,</mo><mi>G</mi><mo lspace="verythinmathspace">:</mo><mi>C</mi><mo>→</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">F, G\colon C \to D</annotation></semantics></math> are <strong>equal</strong> if</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo stretchy="false">(</mo><mi>F</mi><mo stretchy="false">)</mo><mo>=</mo><mi>Ob</mi><mo stretchy="false">(</mo><mi>G</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Ob(F) = Ob(G)</annotation></semantics></math> and</li> <li>there is a (necessarily unique) natural isomorphism from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Wk</mi><mo stretchy="false">(</mo><mi>F</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Wk(F)</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Wk</mi><mo stretchy="false">(</mo><mi>G</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Wk(G)</annotation></semantics></math> modulo which <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>cl</mi><mo stretchy="false">(</mo><mi>F</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">cl(F)</annotation></semantics></math> equals <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>cl</mi><mo stretchy="false">(</mo><mi>G</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">cl(G)</annotation></semantics></math>.</li> </ul> <p>There is an obvious notion of <a class="existingWikiWord" href="/nlab/show/composition">composition</a> that defines a <a class="existingWikiWord" href="/nlab/show/1-category">1-category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Str</mi><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Str Cat</annotation></semantics></math> of strict categories and (equality classes of) strict functors. Note that this 1-category has a strictly associative and unital composition law, even if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math> is only a <a class="existingWikiWord" href="/nlab/show/bicategory">bicategory</a>. (However, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Str</mi><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Str Cat</annotation></semantics></math> is not <em>itself</em> a strict category, unless the assumed category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> is strict.) We have a <a class="existingWikiWord" href="/nlab/show/forgetful+functor">forgetful functor</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo lspace="verythinmathspace">:</mo><mi>Str</mi><mi>Cat</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">Ob\colon Str Cat \to Set</annotation></semantics></math> and a <a class="existingWikiWord" href="/nlab/show/pseudofunctor">pseudofunctor</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Wk</mi><mo lspace="verythinmathspace">:</mo><mi>Str</mi><mi>Cat</mi><mo>→</mo><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Wk\colon Str Cat \to Cat</annotation></semantics></math>.</p> <p>Finally, a <strong>natural transformation</strong> between two strict functors <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math> is simply</p> <ul> <li>a natural transformation from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Wk</mi><mo stretchy="false">(</mo><mi>F</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Wk(F)</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Wk</mi><mo stretchy="false">(</mo><mi>G</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Wk(G)</annotation></semantics></math>.</li> </ul> <p>(That is, a <a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a> between strict functors is automatically strict.) With these as 2-cells, we have a <a class="existingWikiWord" href="/nlab/show/strict+2-category">strict 2-category</a> of strict categories, strict functors, and natural transformations.</p> <div class="un_remark"> <h6 id="remark">Remark</h6> <p>An equivalent definition is that a strict category is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℳ</mi></mrow><annotation encoding="application/x-tex">\mathcal{M}</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/M-category">category</a> whose underlying category of tight morphisms is discrete, while a strict functor is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℳ</mi></mrow><annotation encoding="application/x-tex">\mathcal{M}</annotation></semantics></math>-functor. In this case, the tight morphisms (which are necessarily <a class="existingWikiWord" href="/nlab/show/isomorphisms">isomorphisms</a>) are sometimes called <strong>special isomorphisms</strong>.</p> </div> <h2 id="foundational_choices">Foundational choices</h2> <p>We now make the above schematic definition explicit in terms of various different foundational systems.</p> <h3 id="set_theory_with_ac">Set theory with AC</h3> <p>In <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical</a> <a class="existingWikiWord" href="/nlab/show/set+theory">set-theoretic</a> foundations including the <a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a>, we take <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math> to be the <a class="existingWikiWord" href="/nlab/show/strict+2-category">strict 2-category</a> consisting of (say small) <a class="existingWikiWord" href="/nlab/show/categories">categories</a>, <a class="existingWikiWord" href="/nlab/show/functors">functors</a>, and <a class="existingWikiWord" href="/nlab/show/natural+transformations">natural transformations</a>, defined in any of the traditional ways. The functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Disc</mi><mo lspace="verythinmathspace">:</mo><mi>Set</mi><mo>→</mo><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Disc\colon Set \to Cat</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/left+adjoint">left adjoint</a> to the functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo lspace="verythinmathspace">:</mo><mi>Cat</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">Ob\colon Cat \to Set</annotation></semantics></math>, and thus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Str</mi><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Str Cat</annotation></semantics></math> is a subcategory of the <a class="existingWikiWord" href="/nlab/show/Freyd+cover">Freyd cover</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math>.</p> <p>In this case, the functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Wk</mi><mo lspace="verythinmathspace">:</mo><mi>Str</mi><mi>Cat</mi><mo>→</mo><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Wk\colon Str Cat \to Cat</annotation></semantics></math> has a <a class="existingWikiWord" href="/nlab/show/right+adjoint">right adjoint</a> which takes a category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> to the strict category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Disc</mi><mo stretchy="false">(</mo><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">Disc(Ob(C)) \to C</annotation></semantics></math>. The adjunction counit is literally the identity, while the adjunction unit consists of <a class="existingWikiWord" href="/nlab/show/equivalences">equivalences</a> (but not isomorphisms) in the strict <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Str</mi><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Str Cat</annotation></semantics></math>. Thus, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Str</mi><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Str Cat</annotation></semantics></math> is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math> (as a bicategory).</p> <p>The right adjoint <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi><mo>→</mo><mi>Str</mi><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat \to Str Cat</annotation></semantics></math> also has a further right adjoint defined as follows: given a strict category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">C'</annotation></semantics></math> be the category with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Ob(C)</annotation></semantics></math> as its set of objects, and morphisms induced from those in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Wk</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Wk(C)</annotation></semantics></math>. The unit of this adjunction again consists of identities, while the counit consists of equivalences in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Str</mi><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Str Cat</annotation></semantics></math>.</p> <p>This analysis applies not only to <a class="existingWikiWord" href="/nlab/show/material+set+theories">material set theories</a> such as <a class="existingWikiWord" href="/nlab/show/ZFC">ZFC</a>, but also <a class="existingWikiWord" href="/nlab/show/structural+set+theories">structural set theories</a> such as <a class="existingWikiWord" href="/nlab/show/ETCS">ETCS</a> and <a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a>, as long as they have the axiom of choice.</p> <h3 id="set_theory_without_ac">Set theory without AC</h3> <p>In this case, it is usually best to define <a class="existingWikiWord" href="/nlab/show/Cat">Cat</a> to be the bicategory of categories, <a class="existingWikiWord" href="/nlab/show/anafunctors">anafunctors</a>, and natural transformations. Now although every category has an underlying set of objects, we no longer have a functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo lspace="verythinmathspace">:</mo><mi>Cat</mi><mo>→</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">Ob\colon Cat \to Set</annotation></semantics></math>. It is still true that every category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> admits the structure of a strict category in a canonical way (with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Ob</mi><mo stretchy="false">(</mo><mi>C</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Ob(C)</annotation></semantics></math> its set of objects), but not every strict category necessarily arises in this way, and not every morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi><mo>→</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">C \to D</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math> (i.e. anafunctor) is a strict functor relative to the canonical strict-category structures of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>. In fact, an anafunctor is a strict functor precisely when it is naturally isomorphic to an ordinary (non-ana) functor.</p> <p>If we instead defined <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Cat</annotation></semantics></math> to consist only of non-ana functors, then everything would happen exactly as with AC, except that neither adjunction would be an equivalence.</p> <h3 id="type_and_preset_theories_with_equality">Type and preset theories with equality</h3> <p>We include under this heading all theories in which the basic objects, generally called <a class="existingWikiWord" href="/nlab/show/type+theory">types</a> or <a class="existingWikiWord" href="/nlab/show/presets">presets</a> (and sometimes even called ‘sets’), come with an <a class="existingWikiWord" href="/nlab/show/equality">equality</a> <a class="existingWikiWord" href="/nlab/show/relation">relation</a>, but the notion of <a class="existingWikiWord" href="/nlab/show/set">set</a> is a defined one. Generally, the issue is that types (or presets) do not admit <a class="existingWikiWord" href="/nlab/show/quotient+object">quotients</a>, and so a <strong>set</strong> is defined to be a type equipped with an <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a> called “equality” (sometimes called a <a class="existingWikiWord" href="/nlab/show/setoid">setoid</a> in this context, especially if the types or presets are themselves confusingly called ‘sets’).</p> <p>In this case, it is natural to define a <em>category</em> to have only a type/preset of objects, but a set(oid) of morphisms between each pair of objects; see <a class="existingWikiWord" href="/nlab/show/type-theoretic+definition+of+category">type-theoretic definition of category</a>. Now every category still has an underlying set of objects, but not every set is the set of objects underlying some category; only the <a class="existingWikiWord" href="/nlab/show/completely+presented+sets">completely presented sets</a> have this property.</p> <p>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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>AC</mi></mrow><annotation encoding="application/x-tex">AC</annotation></semantics></math>, and can happen even in the presence of full <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>AC</mi></mrow><annotation encoding="application/x-tex">AC</annotation></semantics></math> (even for setoids). For instance, consider the <a class="existingWikiWord" href="/nlab/show/discrete+category">discrete category</a> on the set of <a class="existingWikiWord" href="/nlab/show/real+numbers">real numbers</a>. 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 <a class="existingWikiWord" href="/nlab/show/Cauchy+real+number">Cauchy real number</a>). 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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>AC</mi></mrow><annotation encoding="application/x-tex">AC</annotation></semantics></math>, 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.)</p> <p>Note that we still have a functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Disc</mi><mo lspace="verythinmathspace">:</mo><mi>Set</mi><mo>→</mo><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Disc\colon Set \to Cat</annotation></semantics></math> which regards an equivalence relation on a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> as a groupoid with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> as its type of objects. The resulting structure of strict categories behaves much like it does in set theory without AC.</p> <h3 id="type_and_preset_theories_without_equality">Type and preset theories without equality</h3> <p>If types or presets do not come with a notion of equality, as in some preset theories and <a class="existingWikiWord" href="/nlab/show/SEAR%2B%CE%B5">SEAR+ε</a>, then a category does not in general even <em>have</em> 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 <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Disc</mi><mo lspace="verythinmathspace">:</mo><mi>Set</mi><mo>→</mo><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Disc\colon Set \to Cat</annotation></semantics></math>, and we can define strict categories, constructing specific examples as wanted.</p> <h3 id="homotopy_type_theory">Homotopy type theory</h3> <p>If <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> is treated as a theory of set-like objects, then it behaves as above, whether <a class="existingWikiWord" href="/nlab/show/extensional+type+theory">extensional</a> or <a class="existingWikiWord" href="/nlab/show/intensional+type+theory">intensional</a>. However, if we take the point of view of <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, then the basic objects of the theory are <a class="existingWikiWord" href="/nlab/show/homotopy+types">homotopy types</a>, a.k.a. <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-groupoids">∞-groupoids</a>. A <em>set</em> is now defined to be an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>, i.e. a <a class="existingWikiWord" href="/nlab/show/truncated+object">0-truncated</a> type.</p> <p>Now the natural definition of (1-)category is something like a <a class="existingWikiWord" href="/nlab/show/complete+Segal+space">complete Segal space</a>, where the type of objects is 1-truncated (a <a class="existingWikiWord" href="/nlab/show/groupoid">groupoid</a>) and equivalent to the <a class="existingWikiWord" href="/nlab/show/core">core</a> of the category. Now (even though identity types exist in HoTT), not every category has an underlying <em>set</em> of objects, so again a category cannot be made into a strict category in any canonical way. But again, we still have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Disc</mi><mo lspace="verythinmathspace">:</mo><mi>Set</mi><mo>→</mo><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Disc\colon Set \to Cat</annotation></semantics></math> and we can define strict categories.</p> <h3 id="fibered_categories">Fibered categories</h3> <p>In <a class="existingWikiWord" href="/nlab/show/Jean+B%C3%A9nabou">Jean Bénabou</a>‘s 1985 paper <em><span class="newWikiWord">Fibered categories and the foundations of naive category theory<a href="/nlab/new/Fibered+categories+and+the+foundations+of+naive+category+theory">?</a></span></em>, it is argued that the right notion of a category in/over another category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{B}</annotation></semantics></math> is given by a <a class="existingWikiWord" href="/nlab/show/Grothendieck+fibration">fibered category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo lspace="verythinmathspace">:</mo><mstyle mathvariant="bold"><mi>F</mi></mstyle><mo>→</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle></mrow><annotation encoding="application/x-tex">p\colon \mathbf{F} \to \mathbf{B}</annotation></semantics></math>, possibly with some additional structure corresponding to the “definability” (representability of certain sieves of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{B}</annotation></semantics></math>) of equality of parallel pairs, isomorphisms, etc. (See <a class="existingWikiWord" href="/nlab/show/indexed+category">indexed category</a> for more motivation.) In this context, equality of objects is available precisely when the fibration is <a class="existingWikiWord" href="/nlab/show/split+fibration">split</a>.</p> <p>In particular, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{B}</annotation></semantics></math> is locally small and has <a class="existingWikiWord" href="/nlab/show/pullback">pullbacks</a>, then an <a class="existingWikiWord" href="/nlab/show/internal+category">internal category</a> object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{B}</annotation></semantics></math> (in the traditional sense) gives rise to an honest functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><msup><mstyle mathvariant="bold"><mi>B</mi></mstyle> <mi>op</mi></msup><mo>→</mo><mi>Cat</mi></mrow><annotation encoding="application/x-tex">\mathbf{B} (-, C)\colon \mathbf{B}^{op} \to Cat</annotation></semantics></math> and so a split fibration <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo>∫</mo> <mstyle mathvariant="bold"><mi>B</mi></mstyle></msub><mstyle mathvariant="bold"><mi>B</mi></mstyle><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>C</mi><mo stretchy="false">)</mo><mo>→</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle></mrow><annotation encoding="application/x-tex">\int_\mathbf{B} \mathbf{B} (-, C) \to \mathbf{B}</annotation></semantics></math> by the <a class="existingWikiWord" href="/nlab/show/Grothendieck+construction">Grothendieck construction</a>.</p> <h2 id="examples">Examples</h2> <ul> <li>Any model <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>V</mi><mo>,</mo><msub><mo>∈</mo> <mi>V</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(V, \in_V)</annotation></semantics></math> of a <a class="existingWikiWord" href="/nlab/show/material+set+theory">material set theory</a> is a strict category, with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math> being the set of objects of the strict category, and given elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">a \in V</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo>∈</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">b \in V</annotation></semantics></math>, the hom-set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">hom</mi> <mi>V</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{hom}_V(a, b)</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/function+set">function set</a> between the sets<div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>x</mi><mo>∈</mo><mi>V</mi><mo stretchy="false">|</mo><mi>x</mi><msub><mo>∈</mo> <mi>V</mi></msub><mi>a</mi><mo stretchy="false">}</mo><mspace width="2em"></mspace><mi mathvariant="normal">and</mi><mspace width="2em"></mspace><mo stretchy="false">{</mo><mi>x</mi><mo>∈</mo><mi>V</mi><mo stretchy="false">|</mo><mi>x</mi><msub><mo>∈</mo> <mi>V</mi></msub><mi>b</mi><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{x \in V \vert x \in_V a\} \qquad \mathrm{and} \qquad \{x \in V \vert x \in_V b\}</annotation></semantics></math></div></li> </ul> <p>There are some at <a class="existingWikiWord" href="/nlab/show/M-category">M-category</a>, to put also here.</p> <h2 id="strict_higher_categories">Strict higher categories</h2> <p>The notion of strict category is related to the notion of strictness in <a class="existingWikiWord" href="/nlab/show/higher+category+theory">higher category theory</a>.</p> <p>For instance, a <a class="existingWikiWord" href="/nlab/show/2-category">2-category</a> must have strict categories as its <a class="existingWikiWord" href="/nlab/show/hom-categories">hom-categories</a> in order to write down the definition of <a class="existingWikiWord" href="/nlab/show/strict+2-category">strict 2-category</a>; a similar remark holds for <a class="existingWikiWord" href="/nlab/show/strict+2-functors">strict 2-functors</a>. 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 <strong>strict <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-natural transformation</strong> as a <a class="existingWikiWord" href="/nlab/show/2-natural+transformation">2-natural transformation</a> that preserves equality (that is, if two objects are equal, then so are the corresponding components of the natural transformation). (All <a class="existingWikiWord" href="/nlab/show/modifications">modifications</a> between strict transformations are automatically strict … until we get to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>3</mn></mrow><annotation encoding="application/x-tex">3</annotation></semantics></math>-categories, of course!)</p> <p>On the other hand, the underlying 1-category of a <a class="existingWikiWord" href="/nlab/show/strict+2-category">strict 2-category</a> (its objects and 1-morphisms) need not be a strict 1-category. For instance, this is the case for the strict 2-category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Str</mi><mi>Cat</mi></mrow><annotation encoding="application/x-tex">Str Cat</annotation></semantics></math> defined in a structural set theory, such as <a class="existingWikiWord" href="/nlab/show/SEAR">SEAR</a>, in which there is no equality predicate on sets. For a fully consistent terminology, we could say ‘locally strict <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-category’ in place of ‘strict <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-category’, but this is unlikely to catch on. Some system of numbered strictness (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math>-strict, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>2</mn></mrow><annotation encoding="application/x-tex">2</annotation></semantics></math>-strict, etc) might also work.</p> </body></html> </div> <div class="revisedby"> <p> Last revised on February 12, 2025 at 22:41:56. See the <a href="/nlab/history/strict+category" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/strict+category" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/18711/#Item_1">Discuss</a><span class="backintime"><a href="/nlab/revision/strict+category/24" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/strict+category" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/strict+category" accesskey="S" class="navlink" id="history" rel="nofollow">History (24 revisions)</a> <a href="/nlab/show/strict+category/cite" style="color: black">Cite</a> <a href="/nlab/print/strict+category" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/strict+category" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>