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> HoTT methods for homotopy theorists 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> HoTT methods for homotopy theorists </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/9330/#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>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="homotopy_theory">Homotopy theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a>, <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-category+theory">(∞,1)-category theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a></strong></p> <p>flavors: <a class="existingWikiWord" href="/nlab/show/stable+homotopy+theory">stable</a>, <a class="existingWikiWord" href="/nlab/show/equivariant+homotopy+theory">equivariant</a>, <a class="existingWikiWord" href="/nlab/show/rational+homotopy+theory">rational</a>, <a class="existingWikiWord" href="/nlab/show/p-adic+homotopy+theory">p-adic</a>, <a class="existingWikiWord" href="/nlab/show/proper+homotopy+theory">proper</a>, <a class="existingWikiWord" href="/nlab/show/geometric+homotopy+theory">geometric</a>, <a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+theory">cohesive</a>, <a class="existingWikiWord" href="/nlab/show/directed+homotopy+theory">directed</a>…</p> <p>models: <a class="existingWikiWord" href="/nlab/show/topological+homotopy+theory">topological</a>, <a class="existingWikiWord" href="/nlab/show/simplicial+homotopy+theory">simplicial</a>, <a class="existingWikiWord" href="/nlab/show/localic+homotopy+theory">localic</a>, …</p> <p>see also <strong><a class="existingWikiWord" href="/nlab/show/algebraic+topology">algebraic topology</a></strong></p> <p><strong>Introductions</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Introduction+to+Topology+--+2">Introduction to Basic Homotopy Theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Introduction+to+Homotopy+Theory">Introduction to Abstract Homotopy Theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometry+of+physics+--+homotopy+types">geometry of physics – homotopy types</a></p> </li> </ul> <p><strong>Definitions</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy">homotopy</a>, <a class="existingWikiWord" href="/nlab/show/higher+homotopy">higher homotopy</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type">homotopy type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Pi-algebra">Pi-algebra</a>, <a class="existingWikiWord" href="/nlab/show/spherical+object+and+Pi%28A%29-algebra">spherical object and Pi(A)-algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+coherent+category+theory">homotopy coherent category theory</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopical+category">homotopical category</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/model+category">model category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/category+of+fibrant+objects">category of fibrant objects</a>, <a class="existingWikiWord" href="/nlab/show/cofibration+category">cofibration category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Waldhausen+category">Waldhausen category</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+category">homotopy category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Ho%28Top%29">Ho(Top)</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-category">(∞,1)-category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/homotopy+category+of+an+%28%E2%88%9E%2C1%29-category">homotopy category of an (∞,1)-category</a></li> </ul> </li> </ul> <p><strong>Paths and cylinders</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/left+homotopy">left homotopy</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/cylinder+object">cylinder object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mapping+cone">mapping cone</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/right+homotopy">right homotopy</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/path+object">path object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/mapping+cocone">mapping cocone</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/generalized+universal+bundle">universal bundle</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/interval+object">interval object</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+localization">homotopy localization</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/infinitesimal+interval+object">infinitesimal interval object</a></p> </li> </ul> </li> </ul> <p><strong>Homotopy groups</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+group">homotopy group</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+group">fundamental group</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/fundamental+group+of+a+topos">fundamental group of a topos</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Brown-Grossman+homotopy+group">Brown-Grossman homotopy group</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/categorical+homotopy+groups+in+an+%28%E2%88%9E%2C1%29-topos">categorical homotopy groups in an (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+homotopy+groups+in+an+%28%E2%88%9E%2C1%29-topos">geometric homotopy groups in an (∞,1)-topos</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+%E2%88%9E-groupoid">fundamental ∞-groupoid</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+groupoid">fundamental groupoid</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/path+groupoid">path groupoid</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+%E2%88%9E-groupoid+in+a+locally+%E2%88%9E-connected+%28%E2%88%9E%2C1%29-topos">fundamental ∞-groupoid in a locally ∞-connected (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+%E2%88%9E-groupoid+of+a+locally+%E2%88%9E-connected+%28%E2%88%9E%2C1%29-topos">fundamental ∞-groupoid of a locally ∞-connected (∞,1)-topos</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+%28%E2%88%9E%2C1%29-category">fundamental (∞,1)-category</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/fundamental+category">fundamental category</a></li> </ul> </li> </ul> <p><strong>Basic facts</strong></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/fundamental+group+of+the+circle+is+the+integers">fundamental group of the circle is the integers</a></li> </ul> <p><strong>Theorems</strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+theorem+of+covering+spaces">fundamental theorem of covering spaces</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Freudenthal+suspension+theorem">Freudenthal suspension theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Blakers-Massey+theorem">Blakers-Massey theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/higher+homotopy+van+Kampen+theorem">higher homotopy van Kampen theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/nerve+theorem">nerve theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+theorem">Whitehead's theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Hurewicz+theorem">Hurewicz theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Galois+theory">Galois theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+hypothesis">homotopy hypothesis</a>-theorem</p> </li> </ul> </div></div> <h4 id="topos_theory"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>∞</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\infty,1)</annotation></semantics></math>-Topos Theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-topos+theory">(∞,1)-topos theory</a></strong></p> <h2 id="sidebar_background">Background</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/%28%E2%88%9E%2C1%29-category">(∞,1)-category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-functor">(∞,1)-functor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-presheaf">(∞,1)-presheaf</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-category+of+%28%E2%88%9E%2C1%29-presheaves">(∞,1)-category of (∞,1)-presheaves</a></p> </li> </ul> <h2 id="sidebar_definitions">Definitions</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/elementary+%28%E2%88%9E%2C1%29-topos">elementary (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-site">(∞,1)-site</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/reflective+sub-%28%E2%88%9E%2C1%29-category">reflective sub-(∞,1)-category</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/localization+of+an+%28%E2%88%9E%2C1%29-category">localization of an (∞,1)-category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+localization">topological localization</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hypercompletion">hypercompletion</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-category+of+%28%E2%88%9E%2C1%29-sheaves">(∞,1)-category of (∞,1)-sheaves</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-sheaf">(∞,1)-sheaf</a>/<a class="existingWikiWord" href="/nlab/show/%E2%88%9E-stack">∞-stack</a>/<a class="existingWikiWord" href="/nlab/show/derived+stack">derived stack</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-topos">(∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28n%2C1%29-topos">(n,1)-topos</a>, <a class="existingWikiWord" href="/nlab/show/n-topos">n-topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/truncated">n-truncated object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/connected">n-connected object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">(1,1)-topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/presheaf">presheaf</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sheaf">sheaf</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%282%2C1%29-topos">(2,1)-topos</a>, <a class="existingWikiWord" href="/nlab/show/2-topos">2-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/%282%2C1%29-presheaf">(2,1)-presheaf</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-quasitopos">(∞,1)-quasitopos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/separated+%28%E2%88%9E%2C1%29-presheaf">separated (∞,1)-presheaf</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/quasitopos">quasitopos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/separated+presheaf">separated presheaf</a></li> </ul> </li> <li> <p><span class="newWikiWord">(2,1)-quasitopos<a href="/nlab/new/%282%2C1%29-quasitopos">?</a></span></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/separated+%282%2C1%29-presheaf">separated (2,1)-presheaf</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C2%29-topos">(∞,2)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2Cn%29-topos">(∞,n)-topos</a></p> </li> </ul> <h2 id="sidebar_characterization">Characterization</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/universal+colimits">universal colimits</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/groupoid+object+in+an+%28%E2%88%9E%2C1%29-category">groupoid object in an (∞,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/effective+epimorphism">effective epimorphism</a></li> </ul> </li> </ul> <h2 id="sidebar_morphisms">Morphisms</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-geometric+morphism">(∞,1)-geometric morphism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29Topos">(∞,1)Topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Lawvere+distribution">Lawvere distribution</a></p> </li> </ul> <h2 id="sidebar_extra">Extra stuff, structure and property</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/hypercomplete+%28%E2%88%9E%2C1%29-topos">hypercomplete (∞,1)-topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/hypercomplete+object">hypercomplete object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Whitehead+theorem">Whitehead theorem</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/over-%28%E2%88%9E%2C1%29-topos">over-(∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/n-localic+%28%E2%88%9E%2C1%29-topos">n-localic (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/locally+n-connected+%28n%2C1%29-topos">locally n-connected (n,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structured+%28%E2%88%9E%2C1%29-topos">structured (∞,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/geometry+%28for+structured+%28%E2%88%9E%2C1%29-toposes%29">geometry (for structured (∞,1)-toposes)</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/locally+%E2%88%9E-connected+%28%E2%88%9E%2C1%29-topos">locally ∞-connected (∞,1)-topos</a>, <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-connected+%28%E2%88%9E%2C1%29-topos">∞-connected (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/local+%28%E2%88%9E%2C1%29-topos">local (∞,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/concrete+%28%E2%88%9E%2C1%29-sheaf">concrete (∞,1)-sheaf</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+%28%E2%88%9E%2C1%29-topos">cohesive (∞,1)-topos</a></p> </li> </ul> <h2 id="sidebar_models">Models</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/models+for+%E2%88%9E-stack+%28%E2%88%9E%2C1%29-toposes">models for ∞-stack (∞,1)-toposes</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/model+category">model category</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/model+structure+on+functors">model structure on functors</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/model+site">model site</a>/<a class="existingWikiWord" href="/nlab/show/sSet-site">sSet-site</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/model+structure+on+simplicial+presheaves">model structure on simplicial presheaves</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/descent+for+simplicial+presheaves">descent for simplicial presheaves</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Verity+on+descent+for+strict+omega-groupoid+valued+presheaves">descent for presheaves with values in strict ∞-groupoids</a></p> </li> </ul> </li> </ul> <h2 id="sidebar_constructions">Constructions</h2> <p><strong>structures in a <a class="existingWikiWord" href="/nlab/show/cohesive+%28%E2%88%9E%2C1%29-topos">cohesive (∞,1)-topos</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/shape+of+an+%28%E2%88%9E%2C1%29-topos">shape</a> / <a class="existingWikiWord" href="/nlab/show/coshape+of+an+%28%E2%88%9E%2C1%29-topos">coshape</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohomology">cohomology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+groups+in+an+%28%E2%88%9E%2C1%29-topos">homotopy</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/fundamental+%E2%88%9E-groupoid+in+a+locally+%E2%88%9E-connected+%28%E2%88%9E%2C1%29-topos">fundamental ∞-groupoid in a locally ∞-connected (∞,1)-topos</a>/<a class="existingWikiWord" href="/nlab/show/fundamental+%E2%88%9E-groupoid+of+a+locally+%E2%88%9E-connected+%28%E2%88%9E%2C1%29-topos">of a locally ∞-connected (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/categorical+homotopy+groups+in+an+%28%E2%88%9E%2C1%29-topos">categorical</a>/<a class="existingWikiWord" href="/nlab/show/geometric+homotopy+groups+in+an+%28%E2%88%9E%2C1%29-topos">geometric</a> homotopy groups</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Postnikov+tower+in+an+%28%E2%88%9E%2C1%29-category">Postnikov tower</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Whitehead+tower+in+an+%28%E2%88%9E%2C1%29-topos">Whitehead tower</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/rational+homotopy+theory+in+an+%28%E2%88%9E%2C1%29-topos">rational homotopy</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/dimension">dimension</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+dimension">homotopy dimension</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohomological+dimension">cohomological dimension</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/covering+dimension">covering dimension</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Heyting+dimension">Heyting dimension</a></p> </li> </ul> </li> </ul> <div> <p> <a href="/nlab/edit/%28infinity%2C1%29-topos+-+contents">Edit this sidebar</a> </p> </div></div></div> <h4 id="type_theory">Type theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a></strong> <a class="existingWikiWord" href="/nlab/show/metalanguage">metalanguage</a>, <a class="existingWikiWord" href="/nlab/show/practical+foundations">practical foundations</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/judgement">judgement</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hypothetical+judgement">hypothetical judgement</a>, <a class="existingWikiWord" href="/nlab/show/sequent">sequent</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/antecedents">antecedents</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo></mrow><annotation encoding="application/x-tex">\vdash</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/consequent">consequent</a>, <a class="existingWikiWord" href="/nlab/show/succedents">succedents</a></li> </ul> </li> </ul> <ol> <li><a class="existingWikiWord" href="/nlab/show/type+formation+rule">type formation rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+introduction+rule">term introduction rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+elimination+rule">term elimination rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/computation+rule">computation rule</a></li> </ol> <p><strong><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></strong> (<a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent</a>, <a class="existingWikiWord" href="/nlab/show/intensional+type+theory">intensional</a>, <a class="existingWikiWord" href="/nlab/show/observational+type+theory">observational type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>)</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/calculus+of+constructions">calculus of constructions</a></li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/syntax">syntax</a></strong> <a class="existingWikiWord" href="/nlab/show/object+language">object language</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/theory">theory</a>, <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>/<a class="existingWikiWord" href="/nlab/show/type">type</a> (<a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/definition">definition</a>/<a class="existingWikiWord" href="/nlab/show/proof">proof</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a> (<a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/theorem">theorem</a></p> </li> </ul> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></strong> = <br /> <strong><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/programs+as+proofs">programs as proofs</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation type theory/category theory</a></strong></p> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/logic">logic</a></th><th><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> (<a class="existingWikiWord" href="/nlab/show/internal+logic+of+set+theory">internal logic</a> of)</th><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object">object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/predicate">predicate</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/family+of+sets">family of sets</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/display+morphism">display morphism</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof">proof</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/element">element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/generalized+element">generalized element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/term">term</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+rule">cut rule</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/composition">composition</a> of <a class="existingWikiWord" href="/nlab/show/classifying+morphisms">classifying morphisms</a> / <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> of <a class="existingWikiWord" href="/nlab/show/display+maps">display maps</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/substitution">substitution</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/introduction+rule">introduction rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/counit">counit</a> for hom-tensor adjunction</td><td style="text-align: left;">lambda</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/elimination+rule">elimination rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unit">unit</a> for hom-tensor adjunction</td><td style="text-align: left;">application</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+elimination">cut elimination</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">one of the <a class="existingWikiWord" href="/nlab/show/zigzag+identities">zigzag identities</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/beta+reduction">beta reduction</a></td></tr> <tr><td style="text-align: left;">identity elimination for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">the other <a class="existingWikiWord" href="/nlab/show/zigzag+identity">zigzag identity</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/eta+conversion">eta conversion</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/true">true</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/singleton">singleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-2%29-truncated+object">(-2)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+0">h-level 0</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/false">false</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>, <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated+object">(-1)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>, <a class="existingWikiWord" href="/nlab/show/mere+proposition">mere proposition</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product">product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product+type">product type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/sum+type">sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> (into <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> (into <a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> (into <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/negation">negation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> into <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> into <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> into <a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subterminal+objects">subterminal objects</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a> (of family of <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/existential+quantification">existential quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum+type">dependent sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/bijection+set">bijection set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+of+isomorphisms">object of isomorphisms</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+type">equivalence type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+set">support set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+object">support object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/propositional+truncation">propositional truncation</a>/<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-image">n-image</a> of <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> into <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/n-truncation">n-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-truncation+modality">n-truncation modality</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equality">equality</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/diagonal+function">diagonal function</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+subset">diagonal subset</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+relation">diagonal relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/path+space+object">path space object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>/<a class="existingWikiWord" href="/nlab/show/path+type">path type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/completely+presented+set">completely presented set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/discrete+object">discrete object</a>/<a class="existingWikiWord" href="/nlab/show/0-truncated+object">0-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+2">h-level 2</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/set">set</a>/<a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> with <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/groupoid+object+in+an+%28infinity%2C1%29-category">internal 0-groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>/<a class="existingWikiWord" href="/nlab/show/setoid">setoid</a> with its <a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relation">pseudo-equivalence relation</a> an actual <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+class">equivalence class</a>/<a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient">quotient</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+type">quotient type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a>, <a class="existingWikiWord" href="/nlab/show/W-type">W-type</a>, <a class="existingWikiWord" href="/nlab/show/M-type">M-type</a></td></tr> <tr><td style="text-align: left;">higher <a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/higher+inductive+type">higher inductive type</a></td></tr> <tr><td style="text-align: left;">-</td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/0-truncated">0-truncated</a> <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+inductive+type">quotient inductive type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinduction">coinduction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/limit">limit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinductive+type">coinductive type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/preset">preset</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a> without <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+of+discourse">domain of discourse</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universe">universe</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modality">modality</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/closure+operator">closure operator</a>, (<a class="existingWikiWord" href="/nlab/show/idempotent+monad">idempotent</a>) <a class="existingWikiWord" href="/nlab/show/monad">monad</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a>, <a class="existingWikiWord" href="/nlab/show/monad+%28in+computer+science%29">monad (in computer science)</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;">(<a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric</a>, <a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed</a>) <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a>/<a class="existingWikiWord" href="/nlab/show/quantum+computation">quantum computation</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof+net">proof net</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/string+diagram">string diagram</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quantum+circuit">quantum circuit</a></td></tr> <tr><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a></td><td style="text-align: left;"></td><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/diagonal">diagonal</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/no-cloning+theorem">no-cloning theorem</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/synthetic+mathematics">synthetic mathematics</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+specific+embedded+programming+language">domain specific embedded programming language</a></td></tr> </tbody></table> </div> <p><strong><a class="existingWikiWord" href="/nlab/show/homotopy+levels">homotopy levels</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-type+theory">2-type theory</a>, <a class="existingWikiWord" href="/michaelshulman/show/2-categorical+logic">2-categorical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory+-+contents">homotopy type theory - contents</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type">homotopy type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/univalence">univalence</a>, <a class="existingWikiWord" href="/nlab/show/function+extensionality">function extensionality</a>, <a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+type+theory">cohesive homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/directed+homotopy+type+theory">directed homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/HoTT+methods+for+homotopy+theorists">HoTT methods for homotopy theorists</a></p> </li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/semantics">semantics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>, <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/display+map">display map</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+a+topos">internal logic of a topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Mitchell-Benabou+language">Mitchell-Benabou language</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kripke-Joyal+semantics">Kripke-Joyal semantics</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/type-theoretic+model+category">type-theoretic model category</a></li> </ul> </li> </ul> <div> <p> <a href="/nlab/edit/type+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <p>This page on aspects of <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> is meant for readers who are interested in <a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a> but not (necessarily) in <a class="existingWikiWord" href="/nlab/show/formal+logic">formal logic</a> and <a class="existingWikiWord" href="/nlab/show/formal+proof">formal proof</a>. This page is meant to help answer the question:</p> <blockquote> <p>I am a homotopy theorist; what can homotopy type theory do for me?</p> </blockquote> <p>See also at <em><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory+FAQ">homotopy type theory FAQ</a></em> the section <em><a href="homotopy+type+theory+FAQ#WhyShouldICareForHomotopyTheorists">Why should I care? – For homotopy theorists</a></em>.</p> <p>Since homotopy theory takes place in <a class="existingWikiWord" href="/nlab/show/model+categories">model categories</a> and similar categorical structures, the input from homotopy type theory is via its <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a>. In this sense the question which this page is meant to help to answer is</p> <blockquote> <p>I am a homotopy theorist; which methods can I learn from the <a class="existingWikiWord" href="/nlab/show/categorical+semantics+of+homotopy+type+theory">categorical semantics of homotopy type theory</a>?</p> </blockquote> <p>For the moment this page will mostly list pointers with brief comments to other entries where details are given. You should maybe read it like an instructional exercise list and follow the pointers for help.</p> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#BasicDictionary'>Basic dictionary for the internal language</a></li> <ul> <li><a href='#'>{}</a></li> </ul> <li><a href='#homotopy_pullbacks'>Homotopy pullbacks</a></li> <li><a href='#detecting_truncation'>Detecting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-truncation</a></li> <li><a href='#Induction'>Homotopy algebras over homotopy monads</a></li> <li><a href='#detecting_connectedness'>Detecting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-connectedness</a></li> <li><a href='#homotopy_pushouts'>Homotopy pushouts</a></li> <li><a href='#constructing_truncation'>Constructing <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-truncation</a></li> <li><a href='#specific_hott_proofs_in_homotopy_theory'>Specific HoTT proofs in homotopy theory</a></li> <ul> <li><a href='#blakersmassey_theorem'>Blakers-Massey theorem</a></li> <li><a href='#essential_uniqueness_of_group_units'>Essential uniqueness of group units</a></li> <li><a href='#equivalence_of_notions_of_stabilizer_groups'>Equivalence of notions of stabilizer <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groups</a></li> </ul> </ul> </div> <h2 id="BasicDictionary">Basic dictionary for the internal language</h2> <p>Starting from (<a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-category+theory">homotopy</a>) <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>, the corresponding (<a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy</a>) <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> is simply a formal language for denoting familiar constructions, as indicated in the following table.</p> <table><thead><tr><th>(<a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-category+theory">homotopy</a>) <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th>(<a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy</a>) <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/semantics">semantics</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/syntax">syntax</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object">object</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">x : X</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/fibration">fibration</a>(<a class="existingWikiWord" href="/nlab/show/display+map">display map</a>) <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>A</mi></mtd></mtr> <mtr><mtd><msup><mo stretchy="false">↓</mo> <mpadded width="0"><mi>p</mi></mpadded></msup></mtd></mtr> <mtr><mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{A \\ \downarrow^{\mathrlap{p}} \\ X}</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>X</mi><mo>⊢</mo><mi>A</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">x : X \vdash A(x) : Type</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/section">section</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>X</mi></mtd> <mtd></mtd> <mtd><mover><mo>→</mo><mi>t</mi></mover></mtd> <mtd></mtd> <mtd><mi>A</mi></mtd></mtr> <mtr><mtd></mtd> <mtd><msub><mrow></mrow> <mpadded width="0" lspace="-100%width"><mi>id</mi></mpadded></msub><mo>↘</mo></mtd> <mtd></mtd> <mtd><msub><mo>↙</mo> <mi>p</mi></msub></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ X &&\stackrel{t}{\to}&& A \\ & {}_{\mathllap{id}}\searrow && \swarrow_{p} \\ && X}</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/term">term</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>X</mi><mo>⊢</mo><mi>t</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x : X \vdash t(x) : A(x)</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><msup><mi>f</mi> <mo>*</mo></msup><mi>A</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>A</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><msup><mo stretchy="false">↓</mo> <mpadded width="0"><mi>p</mi></mpadded></msup></mtd></mtr> <mtr><mtd><mi>Y</mi></mtd> <mtd><mover><mo>→</mo><mi>f</mi></mover></mtd> <mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ f^* A &\to& A \\ \downarrow && \downarrow^{\mathrlap{p}} \\ Y &\stackrel{f}{\to} & X }</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/substitution">substitution</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>Y</mi><mo>⊢</mo><mi>A</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">y : Y \vdash A(f(y)) : Type</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/direct+image">direct image</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>A</mi></mtd> <mtd></mtd> <mtd><msub><mi>f</mi> <mo>*</mo></msub><mi>A</mi></mtd></mtr> <mtr><mtd><msup><mrow></mrow> <mpadded width="0" lspace="-100%width"><mi>p</mi></mpadded></msup><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><msup><mo stretchy="false">↓</mo> <mrow><msub><mi>f</mi> <mo>*</mo></msub><mi>p</mi></mrow></msup></mtd></mtr> <mtr><mtd><mi>X</mi></mtd> <mtd><mover><mo>→</mo><mi>f</mi></mover></mtd> <mtd><mi>Y</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ A && f_* A \\ {}^{\mathllap{p}}\downarrow && \downarrow ^{f_* p}\\ X &\stackrel{f}{\to}& Y}</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>Y</mi><mo>⊢</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo><mrow><mi>x</mi><mo>:</mo><mi>X</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow></munder><mi>A</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> y : Y \vdash \underset{x : X(y)}{\prod } A(x) : Type</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a href="locally%20cartesian%20closed%20category#EquivalentCharacterizations">internal hom in slice</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>X</mi><mo>×</mo><msup><mi>f</mi> <mo>*</mo></msup><mi>A</mi></mtd> <mtd></mtd> <mtd><msub><mi>f</mi> <mo>*</mo></msub><msup><mi>f</mi> <mo>*</mo></msup><mi>A</mi></mtd> <mtd><mo>=</mo><mo stretchy="false">[</mo><mi>X</mi><mo>,</mo><mi>A</mi><msub><mo stretchy="false">]</mo> <mi>Y</mi></msub></mtd></mtr> <mtr><mtd><msup><mrow></mrow> <mpadded width="0" lspace="-100%width"><mrow></mrow></mpadded></msup><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>X</mi></mtd> <mtd><mover><mo>→</mo><mi>f</mi></mover></mtd> <mtd><mi>Y</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ X \times f^* A && f_* f^* A & = [X,A]_Y \\ {}^{\mathllap{}}\downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>Y</mi><mo>⊢</mo><mi>X</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>→</mo><mi>A</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> y : Y \vdash X(y) \to A(y) : Type</annotation></semantics></math></td></tr> <tr><td style="text-align: left;">postcomposition <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>A</mi></mtd> <mtd><mo>=</mo></mtd> <mtd><msub><mi>f</mi> <mo>!</mo></msub><mi>A</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>X</mi></mtd> <mtd><mover><mo>→</mo><mi>f</mi></mover></mtd> <mtd><mi>Y</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ A &=& f_! A \\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>Y</mi><mo>⊢</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo><mrow><mi>x</mi><mo>:</mo><mi>X</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow></munder><mi>A</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">y : Y \vdash \underset{x : X(y)}{\sum} A(x) : Type</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/fiber+product">fiber</a><a class="existingWikiWord" href="/nlab/show/product">product</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>X</mi><mo>×</mo><msup><mi>f</mi> <mo>*</mo></msup><mi>A</mi></mtd> <mtd><mo>=</mo></mtd> <mtd><msub><mi>f</mi> <mo>!</mo></msub><msup><mi>f</mi> <mo>*</mo></msup><mi>A</mi></mtd> <mtd><mo>=</mo><mi>X</mi><msub><mo>×</mo> <mi>Y</mi></msub><mi>A</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>X</mi></mtd> <mtd><mover><mo>→</mo><mi>f</mi></mover></mtd> <mtd><mi>Y</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ X \times f^* A &=& f_! f^* A & = X \times_Y A\\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product+type">product type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>Y</mi><mo>⊢</mo><mi>X</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>×</mo><mi>A</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">y : Y \vdash X(y) \times A(y) : Type</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Beck-Chevalley+condition">Beck-Chevalley condition</a> of <a class="existingWikiWord" href="/nlab/show/codomain+fibration">codomain fibration</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/substitution">substitution</a> commutes with <a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/path+space+object">path space object</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><msup><mi>A</mi> <mi>I</mi></msup></mtd></mtr> <mtr><mtd><msup><mo stretchy="false">↓</mo> <mpadded width="0"><mrow><mo stretchy="false">(</mo><msub><mi>d</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>d</mi> <mn>0</mn></msub><mo stretchy="false">)</mo></mrow></mpadded></msup></mtd></mtr> <mtr><mtd><mi>A</mi><mo>×</mo><mi>A</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{A^I \\ \downarrow^{\mathrlap{(d_1,d_0)}} \\ A \times A}</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>,</mo><mi>b</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mo stretchy="false">(</mo><mi>a</mi><mo>=</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">a,b : A \vdash (a = b)</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/truncated+object+in+an+%28infinity%2C1%29-category">(-2)-truncated morphism</a>/<a class="existingWikiWord" href="/nlab/show/equivalence+in+an+%28infinity%2C1%29-category">equivalence</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>Y</mi></mtd></mtr> <mtr><mtd><msup><mo stretchy="false">↓</mo> <mpadded width="0"><mo>≃</mo></mpadded></msup></mtd></mtr> <mtr><mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{Y \\ \downarrow^{\mathrlap{\simeq}} \\ X}</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/true">true</a>/<a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>X</mi><mo>⊢</mo><mn>1</mn><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">x : X \vdash 1 : Type</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/truncated+object+in+an+%28infinity%2C1%29-category">(-1)-truncated morphism</a>/<a class="existingWikiWord" href="/nlab/show/monomorphism+in+an+%28infinity%2C1%29-category">monomorphism</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>ϕ</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{\phi \\ \downarrow \\ X}</annotation></semantics></math></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>X</mi><mo>⊢</mo><mi>ϕ</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">x : X \vdash \phi(x) : Type</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/direct+image">direct image</a> of <a class="existingWikiWord" href="/nlab/show/truncated+object+in+an+%28infinity%2C1%29-category">(-1)-truncated morphism</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universal+quantifier">universal quantifier</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>Y</mi><mo>⊢</mo><munder><mo>∀</mo><mrow><mi>x</mi><mo>∈</mo><mi>X</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow></munder><mi>ϕ</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">y : Y \vdash \underset{x \in X(y)}{\forall} \phi(x) : Type</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/truncated+object+of+an+%28infinity%2C1%29-category">(-1)-truncation</a> of postcomposition of <a class="existingWikiWord" href="/nlab/show/truncated+object+in+an+%28infinity%2C1%29-category">(-1)-truncated morphism</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>Y</mi><mo>⊢</mo><munder><mo>∃</mo><mrow><mi>x</mi><mo>∈</mo><mi>X</mi><mo stretchy="false">(</mo><mi>y</mi><mo stretchy="false">)</mo></mrow></munder><mi>ϕ</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">y : Y \vdash \underset{x \in X(y)}{\exists} \phi(x) : Type</annotation></semantics></math></td></tr> </tbody></table> <p>The symbols in the right column may be formally manipulated according to the rules of <em><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></em>. For the case of ordinary categories, this table defines a <a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Lang</mi><mo>:</mo><mi>LocallyCartesianClosedCategories</mi><mo>→</mo><mi>DependentTypeTheories</mi></mrow><annotation encoding="application/x-tex"> Lang : LocallyCartesianClosedCategories \to DependentTypeTheories </annotation></semantics></math></div> <p>from <em><a class="existingWikiWord" href="/nlab/show/locally+cartesian+closed+categories">locally cartesian closed categories</a></em> to <em><a class="existingWikiWord" href="/nlab/show/dependent+type+theories">dependent type theories</a></em> that sends each category to its <em><a class="existingWikiWord" href="/nlab/show/internal+language">internal language</a></em>.</p> <p>The important fact is that</p> <div class="num_theorem"> <h6 id="theorem">Theorem</h6> <p>The functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Lang</mi></mrow><annotation encoding="application/x-tex">Lang</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalence of categories</a>.</p> </div> <p>This is discussed at <em><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a></em>. So the (dependent) type theory is just an equivalent way of talking about a (locally cartesian closed category).</p> <p>For the case of <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-categories">(∞,1)-categories</a>/<a class="existingWikiWord" href="/nlab/show/homotopy+theories">homotopy theories</a> that we are interested in here, there remain some things to be fully worked out, but it is clear that we get an analogous construction</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Lang</mi><mo>:</mo><mi>LocallyCartesianClosed</mi><mo stretchy="false">(</mo><mn>∞</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo><mi>Categories</mi><mo>→</mo><mi>HomotopyTypeTheory</mi></mrow><annotation encoding="application/x-tex"> Lang : LocallyCartesianClosed(\infty,1)Categories \to HomotopyTypeTheory </annotation></semantics></math></div> <p>from <a class="existingWikiWord" href="/nlab/show/locally+cartesian+closed+%28%E2%88%9E%2C1%29-categories">locally cartesian closed (∞,1)-categories</a> to <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> which is expected to be an <a class="existingWikiWord" href="/nlab/show/equivalence+of+%28%E2%88%9E%2C1%29-categories">equivalence of (∞,1)-categories</a>.</p> <p>As the above table shows, from the perspective of <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> <a class="existingWikiWord" href="/nlab/show/categories">categories</a> <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{C}</annotation></semantics></math> are regarded systematically via the collection of their <a class="existingWikiWord" href="/nlab/show/slice+categories">slice categories</a> (their associated “<a class="existingWikiWord" href="/nlab/show/hyperdoctrines">hyperdoctrines</a>”). If <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{C}</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/locally+cartesian+closed+category">locally cartesian closed category</a> then every <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f : X \to Y</annotation></semantics></math> in <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{C}</annotation></semantics></math> induces an <a class="existingWikiWord" href="/nlab/show/adjoint+triple">adjoint triple</a> of functors between the corresponding slice categories</p> <div class="un_remark" style="border:solid #0000cc;background: #add8e6;border-width:2px 1px;padding:0 1em;margin:0 1em;"> <h6 id="">{}</h6> <p>(<a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊣</mo></mrow><annotation encoding="application/x-tex">\dashv</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/base+change">base change</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊣</mo></mrow><annotation encoding="application/x-tex">\dashv</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a>) = <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mi>f</mi></msub><mo>⊣</mo><msup><mi>f</mi> <mo>*</mo></msup><mo>⊣</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mi>f</mi></msub><mo stretchy="false">)</mo><mo>:</mo><msub><mi>𝒞</mi> <mrow><mo stretchy="false">/</mo><mi>X</mi></mrow></msub><mo>→</mo><msub><mi>𝒞</mi> <mrow><mo stretchy="false">/</mo><mi>Y</mi></mrow></msub></mrow><annotation encoding="application/x-tex">(\sum_f \dashv f^* \dashv \prod_f) : \mathcal{C}_{/X} \to \mathcal{C}_{/Y}</annotation></semantics></math>.</p> </div> <p>Many familiar constructions are usefully expressed entirely in terms of these <a class="existingWikiWord" href="/nlab/show/adjoint+triples">adjoint triples</a>. For instance the <a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> in a slice category.</p> <p>While this is in principle clear/well known, the systematic use of the base change adjoint triple enforced by type theory turns out to lead to various elegant constructions that have not found much attention before, and which can be useful in applications.</p> <h2 id="homotopy_pullbacks">Homotopy pullbacks</h2> <p>The yoga of <a class="existingWikiWord" href="/nlab/show/homotopy+pullbacks">homotopy pullbacks</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+fibers">homotopy fibers</a>, <a class="existingWikiWord" href="/nlab/show/loop+space+objects">loop space objects</a>, <a class="existingWikiWord" href="/nlab/show/fiber+sequences">fiber sequences</a> etc. is basic to <a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a>, and of course is also fairly elementary. Homotopy type theory can hardly add a previously unknown fact here. Nevertheless, it is noteworthy that many of these constructions, elementary as they are, look <em>even simpler</em> when formulated in homotopy type theory.</p> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/homotopy+pullback">homotopy pullback</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>A</mi><msubsup><mo>×</mo> <mi>C</mi> <mi>h</mi></msubsup><mi>B</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>B</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd><msub><mo>⇙</mo> <mo>≃</mo></msub></mtd> <mtd><msup><mo stretchy="false">↓</mo> <mpadded width="0"><mi>g</mi></mpadded></msup></mtd></mtr> <mtr><mtd><mi>A</mi></mtd> <mtd><mover><mo>→</mo><mi>f</mi></mover></mtd> <mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{A \times_C^h B &\to& B \\ \downarrow &\swArrow_{\simeq}& \downarrow^{\mathrlap{g}} \\ A &\stackrel{f}{\to}& X}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo><mrow><mi>a</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>b</mi><mo>:</mo><mi>B</mi></mrow></munder><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mi>g</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\underset{a : A, b : B}{\sum} (f(a) = g(b))</annotation></semantics></math> / <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>a</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>b</mi><mo>:</mo><mi>B</mi><mo>;</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mi>g</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{ a : A, b : B ; (f(a) = g(b)) \}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/homotopy+fiber">homotopy fiber</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>hfib</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mtd> <mtd><mo>→</mo></mtd> <mtd><mo>*</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd><msub><mo>⇙</mo> <mo>≃</mo></msub></mtd> <mtd><msup><mo stretchy="false">↓</mo> <mpadded width="0"><mrow></mrow></mpadded></msup></mtd></mtr> <mtr><mtd><mi>A</mi></mtd> <mtd><mover><mo>→</mo><mi>f</mi></mover></mtd> <mtd><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{hfib(f) &\to& * \\ \downarrow &\swArrow_{\simeq}& \downarrow^{\mathrlap{}} \\ A &\stackrel{f}{\to}& X}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow></msub><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mo>*</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{a : A} (f(a) = *)</annotation></semantics></math> / <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">{</mo><mi>a</mi><mo>:</mo><mi>A</mi><mo>;</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo>=</mo><mo>*</mo><mo stretchy="false">)</mo><mo stretchy="false">}</mo></mrow><annotation encoding="application/x-tex">\{ a : A ; (f(a) = *) \}</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/mapping+cocylinder">mapping cocylinder</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>CoCyl</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>X</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><msup><mo stretchy="false">↓</mo> <mpadded width="0"><mi>f</mi></mpadded></msup></mtd></mtr> <mtr><mtd><msup><mi>Y</mi> <mi>I</mi></msup></mtd> <mtd><mover><mo>→</mo><mrow><msub><mi>d</mi> <mn>0</mn></msub></mrow></mover></mtd> <mtd><mi>Y</mi></mtd></mtr> <mtr><mtd><msup><mo stretchy="false">↓</mo> <mpadded width="0"><mrow><msub><mi>d</mi> <mn>1</mn></msub></mrow></mpadded></msup></mtd></mtr> <mtr><mtd><mi>Y</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ CoCyl(f) &\to& X \\ \downarrow && \downarrow^{\mathrlap{f}} \\ Y^I &\stackrel{d_0}{\to} & Y \\ \downarrow^{\mathrlap{d_1}} \\ Y } </annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mi>Y</mi><mo>⊢</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo><mrow><mi>x</mi><mo>:</mo><mi>X</mi></mrow></munder><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">y : Y \vdash \underset{x : X}{\sum} (f(x) = y)</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/free+loop+space+object">free loop space object</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>ℒ</mi><mi>X</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>X</mi></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd><msub><mo>⇙</mo> <mo>≃</mo></msub></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>X</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>X</mi><mo>×</mo><mi>X</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{\mathcal{L}X &\to& X \\ \downarrow &\swArrow_{\simeq}& \downarrow \\ X &\to& X \times X}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo><mrow><mi>x</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>X</mi></mrow></munder><mo stretchy="false">(</mo><mi>x</mi><mo>=</mo><mi>y</mi><mo stretchy="false">)</mo><mi>and</mi><mo stretchy="false">(</mo><mi>x</mi><mo>=</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\underset{x,y : X}{\sum} (x = y) and (x = y)</annotation></semantics></math></td></tr> </tbody></table> <ul> <li><a class="existingWikiWord" href="/nlab/show/pasting+law">pasting law</a> (…)</li> </ul> <h2 id="detecting_truncation">Detecting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-truncation</h2> <p>The central insight (due to <a class="existingWikiWord" href="/nlab/show/Vladimir+Voevodsky">Vladimir Voevodsky</a>) that boosts dependent type theory with identity types to genuine homotopy type theory is that in terms of <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a> there are simple natural expressions for <a class="existingWikiWord" href="/nlab/show/n-truncated">n-truncation</a> and detection of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-truncation of objects and morphisms. Translated via <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> to <a class="existingWikiWord" href="/nlab/show/homotopy+theory">homotopy theory</a>, these formulas turn out to refomulate some basic yoga of model category computation in a new way that hasn’t received attention before in homotopy theory, emphasizing the base change adjoint triple.</p> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;">object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/%28-2%29-truncated">(-2)-truncated</a>/<a class="existingWikiWord" href="/nlab/show/contractible">contractible</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/isContr">isContr</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>=</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>X</mi></mrow></msub><msub><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>y</mi><mo>:</mo><mi>X</mi></mrow></msub><mo stretchy="false">(</mo><mi>x</mi><mo>=</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(X) = \sum_{x : X} \prod_{y : X} (x = y)</annotation></semantics></math></td></tr> <tr><td style="text-align: left;">morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/%28-2%29-truncated">(-2)-truncated</a>/<a class="existingWikiWord" href="/nlab/show/equivalence+in+an+%28infinity%2C1%29-category">equivalence</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/isEquiv">isEquiv</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo>≔</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>x</mi><mo>:</mo><mi>X</mi></mrow></msub><mi>isContr</mi><mo stretchy="false">(</mo><mi>hfiber</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(f) \coloneqq \prod_{x : {X}} isContr(hfiber(f,x) </annotation></semantics></math></td></tr> </tbody></table> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>In the <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-category">(∞,1)-category</a> <a class="existingWikiWord" href="/nlab/show/%E2%88%9EGrpd">∞Grpd</a> it is true that a morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f : X \to Y</annotation></semantics></math> is an equivalence precisely if for all global points <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>y</mi><mo>:</mo><mo>*</mo><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">y : * \to Y</annotation></semantics></math> the corresponding homotopy fiber of <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> is contractible. The same simple statement is not available <em>in the “external” logic</em> for a general <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-category">(∞,1)-category</a>, simply because there an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math> may not even have enough global points (it may be non-trivial and have no global point).</p> <p>The above is useful in that it says that <em>in the <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a></em> of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>∞</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\infty,1)</annotation></semantics></math>-category, the simple statement familiar form <a class="existingWikiWord" href="/nlab/show/%E2%88%9EGrpd">∞Grpd</a> is true generally, after all.</p> </div> <h2 id="Induction">Homotopy algebras over homotopy monads</h2> <p>We have seen that homtopy type theory naturally describes <a class="existingWikiWord" href="/nlab/show/homotopy+pullbacks">homotopy pullbacks</a> and some other finite <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-limits">(∞,1)-limits</a> in terms of <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a> and the <a class="existingWikiWord" href="/nlab/show/base+change">base change</a> <a class="existingWikiWord" href="/nlab/show/adjoint+triple">adjoint triple</a>. The <a class="existingWikiWord" href="/nlab/show/duality">dual</a> notion, <em><a class="existingWikiWord" href="/nlab/show/homotopy+colimits">homotopy colimits</a></em>, is conceived of in homotopy type theory as a (vast) generalization of the basic notion of <em><a class="existingWikiWord" href="/nlab/show/induction">induction</a></em> and <em><a class="existingWikiWord" href="/nlab/show/recursion">recursion</a></em>, subsumed type-theoretically in the notion of <em><a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a></em>, roughly a kind of <a class="existingWikiWord" href="/nlab/show/type">type</a> that is given by <a class="existingWikiWord" href="/nlab/show/generators+and+relations">generators and relations</a>.</p> <p>Traditionally inductive types are in category theory <a class="existingWikiWord" href="/nlab/show/categorical+semantics">interpreted</a> as <em><a class="existingWikiWord" href="/nlab/show/algebras+over+an+endofunctor">algebras over an endofunctor</a></em>. While useful, this is a concept somewhat alien to usual constructions in category theory or homotopy theory. The natural notion is instead that of an <a class="existingWikiWord" href="/nlab/show/algebra+over+a+monad">algebra over a monad</a>. While an <a class="existingWikiWord" href="/nlab/show/algebra+over+an+endofunctor">algebra over an endofunctor</a> may be thought of as a monad-algebra over a <a class="existingWikiWord" href="/nlab/show/free+monad">free monad</a>, from the point of view of homotopy theory it still seems unnatural to restrict attention to free monads.</p> <p>However, after generalization to <em><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a></em> this is rectified: here the homotopy-theoretic notion of <a class="existingWikiWord" href="/nlab/show/induction">induction</a> turns out to be about <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-algebras+over+an+%28%E2%88%9E%2C1%29-monad">∞-algebras over an (∞,1)-monad</a>, as one would hope, and a <em><a class="existingWikiWord" href="/nlab/show/higher+inductive+type">higher inductive type</a></em> is an <a class="existingWikiWord" href="/nlab/show/initial+algebras+of+a+presentable+%28%E2%88%9E%2C1%29-monad">initial algebras of a presentable (∞,1)-monad</a>.</p> <p>(…)</p> <h2 id="detecting_connectedness">Detecting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-connectedness</h2> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-connected+object+of+an+%28infinity%2C1%29-topos">(-1)-connected object</a>/ <a class="existingWikiWord" href="/nlab/show/inhabited+object">inhabited object</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>isInhab</mi><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo><mo>≔</mo><mo>.</mo><mo>.</mo><mo>.</mo></mrow><annotation encoding="application/x-tex">isInhab(X) \coloneqq ...</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-connected+object+of+an+%28infinity%2C1%29-topos">(-1)-connected morphism</a>/ <a class="existingWikiWord" href="/nlab/show/effective+epimorphism+in+an+%28infinity%2C1%29-category">effective epimorphism</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f : X \to Y</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>y</mi><mo>:</mo><mi>Y</mi></mrow></msub><mi>isInhab</mi><mo stretchy="false">(</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>X</mi></mrow></msub><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\prod_{y : Y} isInhab(\sum_{x : X} (f(x) = y))</annotation></semantics></math></td></tr> </tbody></table> <h2 id="homotopy_pushouts">Homotopy pushouts</h2> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/homotopy+pushout">homotopy pushout</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>C</mi></mtd> <mtd><mover><mo>→</mo><mi>g</mi></mover></mtd> <mtd><mi>B</mi></mtd></mtr> <mtr><mtd><msup><mrow></mrow> <mpadded width="0" lspace="-100%width"><mi>f</mi></mpadded></msup><mo stretchy="false">↓</mo></mtd> <mtd><msub><mo>⇙</mo> <mo>≃</mo></msub></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mi>A</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>A</mi><msubsup><mo lspace="thinmathspace" rspace="thinmathspace">∐</mo> <mi>C</mi> <mi>h</mi></msubsup><mi>B</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ C &\stackrel{g}{\to}& B \\ {}^{\mathllap{f}}\downarrow &\swArrow_{\simeq}& \downarrow \\ A &\to& A \coprod_C^h B}</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>hpushout</mi><mo stretchy="false">(</mo><mi>A</mi><mspace width="thinmathspace"></mspace><mi>B</mi><mspace width="thinmathspace"></mspace><mi>C</mi><mo>:</mo><mi>Type</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo>:</mo><mi>C</mi><mo>→</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>g</mi><mo>:</mo><mi>C</mi><mo>→</mo><mi>B</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi><mo>≔</mo><mrow><mo>{</mo><mrow><mtable><mtr><mtd><mi>inl</mi><mo>:</mo><mi>B</mi><mo>→</mo><mi>hpushout</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>inr</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>hpushout</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>glue</mi><msub><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>c</mi><mo>:</mo><mi>C</mi></mrow></msub><mo stretchy="false">(</mo><mi>inl</mi><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>=</mo><mi>inr</mi><mo stretchy="false">(</mo><mi>g</mi><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow></mrow></mrow><annotation encoding="application/x-tex">hpushout (A\,B\,C : Type) (f : C \to A) (g : C \to B) : Type \coloneqq \left\{ \array{inl : B \to hpushout(f,g) \\ inr : A \to hpushout(f,g) \\ glue \prod_{c : C} (inl(f(c)) = inr(g(c)))} \right.</annotation></semantics></math></td></tr> </tbody></table> <p>(…)</p> <h2 id="constructing_truncation">Constructing <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>-truncation</h2> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/truncated+object+in+an+%28infinity%2C1%29-category">(-1)-truncation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>τ</mi> <mrow><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn></mrow></msub><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\tau_{-1}(-)</annotation></semantics></math></td><td style="text-align: left;"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>supp</mi><mo stretchy="false">(</mo><mi>X</mi><mo>:</mo><mi>Type</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi><mo>≔</mo><mrow><mo>{</mo><mrow><mtable><mtr><mtd><mi>proj</mi><mo>:</mo><mi>X</mi><mo>→</mo><mi>supp</mi><mi>X</mi></mtd></mtr> <mtr><mtd><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo><mrow><mi>x</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>supp</mi><mi>X</mi></mrow></munder><mo stretchy="false">(</mo><mi>x</mi><mo>=</mo><mi>y</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow></mrow></mrow><annotation encoding="application/x-tex">supp(X : Type) : Type \coloneqq \left\{ \array{ proj : X \to supp X \\ \underset{x, y : supp X}{\prod} (x = y) }\right. </annotation></semantics></math></td></tr> </tbody></table> <h2 id="specific_hott_proofs_in_homotopy_theory">Specific HoTT proofs in homotopy theory</h2> <p>We list in the following theorems in homotopy theory together with such proofs of them in terms of homotopy type theory language that are either new (to the best of our knowledge), or else that are at least considerably simpler than earlier proofs with traditional homotopy theory tools.</p> <h3 id="blakersmassey_theorem">Blakers-Massey theorem</h3> <p>see at <em><a class="existingWikiWord" href="/nlab/show/Blakers-Massey+theorem">Blakers-Massey theorem</a></em></p> <h3 id="essential_uniqueness_of_group_units">Essential uniqueness of group units</h3> <p>(…)</p> <h3 id="equivalence_of_notions_of_stabilizer_groups">Equivalence of notions of stabilizer <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-groups</h3> <p>(…) <a href="http://nforum.mathforge.org/discussion/3454/stabilizer-subgroup/?Focus=28287#Comment_28287">…</a></p> <p>(…)</p> </body></html> </div> <div class="revisedby"> <p> Last revised on December 1, 2018 at 13:41:57. See the <a href="/nlab/history/HoTT+methods+for+homotopy+theorists" 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/HoTT+methods+for+homotopy+theorists" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/9330/#Item_1">Discuss</a><span class="backintime"><a href="/nlab/revision/HoTT+methods+for+homotopy+theorists/18" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/HoTT+methods+for+homotopy+theorists" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/HoTT+methods+for+homotopy+theorists" accesskey="S" class="navlink" id="history" rel="nofollow">History (18 revisions)</a> <a href="/nlab/show/HoTT+methods+for+homotopy+theorists/cite" style="color: black">Cite</a> <a href="/nlab/print/HoTT+methods+for+homotopy+theorists" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/HoTT+methods+for+homotopy+theorists" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>