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> dependent sum type 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> dependent sum type </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/15823/#Item_5" 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>Dependent sum types</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <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> <h1 id="dependent_sum_types">Dependent sum types</h1> <div class='maruku_toc'> <ul> <li><a href='#Idea'>Idea</a></li> <li><a href='#overview'>Overview</a></li> <li><a href='#definition'>Definition</a></li> <ul> <li><a href='#in_natural_deduction'>In natural deduction</a></li> <ul> <li><a href='#as_a_positive_type'>As a positive type</a></li> <li><a href='#as_a_negative_type'>As a negative type</a></li> <li><a href='#ExtensionalityPrinciple'>Extensionality principle</a></li> </ul> <li><a href='#in_lambdacalculus'>In lambda-calculus</a></li> <ul> <li><a href='#as_a_negative_type_2'>As a negative type</a></li> <li><a href='#as_a_positive_type_2'>As a positive type</a></li> <li><a href='#positive_versus_negative'>Positive versus negative</a></li> </ul> <li><a href='#using_universes_and_dependent_product_types'>Using universes and dependent product types</a></li> </ul> <li><a href='#properties'>Properties</a></li> <ul> <li><a href='#descent_and_large_elimination'>Descent and large elimination</a></li> <li><a href='#typal_congruence_rules'>Typal congruence rules</a></li> <li><a href='#quantification_in_dependent_type_theory'>Quantification in dependent type theory</a></li> </ul> <li><a href='#categorical_interpretation'>Categorical interpretation</a></li> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="Idea">Idea</h2> <p>In <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a>, what is traditionally called the <em>dependent sum type</em> (really: dependent <a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a>) of a <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>d</mi><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mi>D</mi><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo>⊢</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><msub><mi>C</mi> <mi>d</mi></msub><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mi>Type</mi></mrow><annotation encoding="application/x-tex">d \,\colon\, D \;\;\vdash\;\; C_d \,\colon\, Type</annotation></semantics></math> is the type whose <a class="existingWikiWord" href="/nlab/show/terms">terms</a> are <a class="existingWikiWord" href="/nlab/show/ordered+pairs">ordered pairs</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>d</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(d,c)</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>d</mi><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mi>D</mi></mrow><annotation encoding="application/x-tex">d \,\colon\, D</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><msub><mi>C</mi> <mi>d</mi></msub></mrow><annotation encoding="application/x-tex">c \,\colon\, C_d</annotation></semantics></math> — whence also called the <em>dependent pair type</em>.</p> <p>In the <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> <a class="existingWikiWord" href="/nlab/show/categorical+model+of+dependent+type+theory">of dependent type theory</a> in <a class="existingWikiWord" href="/nlab/show/fibration+categories">fibration categories</a>, the dependent sum corresponds to internal <a class="existingWikiWord" href="/nlab/show/coproducts">coproducts</a> over an index type.</p> <p>In the special case that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>d</mi></msub><mspace width="thinmathspace"></mspace><mo>=</mo><mspace width="thinmathspace"></mspace><mi>C</mi></mrow><annotation encoding="application/x-tex">C_d \,=\, C</annotation></semantics></math> is independent of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> this reduces to the <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>D</mi><mo>×</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">D \times C</annotation></semantics></math>, while in the special case that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>=</mo></mrow><annotation encoding="application/x-tex">D =</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/boolean+domain">Bool</a> it reduces to a binary <a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a>.</p> <p>This notion is dual (in fact: adjoint) to the corresponding notion of <a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a>:</p> <div> <p><img src="/nlab/files/DependentFunctionsAndPairs-230120.jpg" width="680" /></p> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/type+former">type former</a>:</th><th>meaning of <a class="existingWikiWord" href="/nlab/show/terms">terms</a>:</th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+function">dependent function</a><br /> / <a class="existingWikiWord" href="/nlab/show/section">section</a> of <a class="existingWikiWord" href="/nlab/show/bundle">bundle</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent coproduct</a> <br /> (aka: dependent sum)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+pair">dependent pair</a> / <br /> <a class="existingWikiWord" href="/nlab/show/generalized+element">element</a> of <a class="existingWikiWord" href="/nlab/show/bundle">bundle</a></td></tr> </tbody></table> </div> <h2 id="overview">Overview</h2> <div> <p>The <a class="existingWikiWord" href="/nlab/show/inference+rules">inference rules</a> for <a class="existingWikiWord" href="/nlab/show/dependent+pair+types">dependent pair types</a> (aka “dependent sum types” or “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>-types”):</p> <div style="margin: -30px 0px 20px 10px"> <img src="/nlab/files/DependentPairTypeInference-230215.jpg" width="770px" /> </div></div> <h2 id="definition">Definition</h2> <p>Like any <a class="existingWikiWord" href="/nlab/show/type+formation">type constructor</a> in <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, the dependent sum type is specified by rules saying when we can <a class="existingWikiWord" href="/nlab/show/type+formation">introduce</a> it as a type, how to <a class="existingWikiWord" href="/nlab/show/term+introduction">construct terms</a> of that type, how to use or “<a class="existingWikiWord" href="/nlab/show/term+elimination">eliminate</a>” terms of that type, and how to <a class="existingWikiWord" href="/nlab/show/computation+rule">compute</a> when we combine the constructors with the eliminators.</p> <h3 id="in_natural_deduction">In natural deduction</h3> <p>We assume that our dependent sum types have typal <a class="existingWikiWord" href="/nlab/show/conversion+rules">conversion rules</a>, as those are the most general of the conversion rules. Both the propositional and judgmental conversion rules imply the typal conversion rules by the structural rules for propositional and judgmental equality respectively.</p> <p>The formation and introduction rules are the same for both the positive and negative dependent sum types</p> <p>Formation rules for dependent sum types:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>⊢</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma \vdash \sum_{x:A} B(x) \; \mathrm{type}}</annotation></semantics></math></div> <p>Introduction rules for dependent sum types:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \mathrm{in}(x, y):\sum_{x:A} B(x)}</annotation></semantics></math></div> <h4 id="as_a_positive_type">As a positive type</h4> <ul> <li>Elimination rules for dependent sum types:</li> </ul> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>z</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><mi>c</mi><mo>:</mo><mi>C</mi><mo stretchy="false">[</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>z</mi><mo stretchy="false">]</mo></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>z</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><msubsup><mi mathvariant="normal">ind</mi> <mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow> <mi>C</mi></msubsup><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo><mo>:</mo><mi>C</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} B(x) \vdash C \; \mathrm{type} \quad \Gamma, x:A, y:B \vdash c:C[\mathrm{in}(x, y)/z]}{\Gamma, z:\sum_{x:A} B(x) \vdash \mathrm{ind}_{\sum_{x:A} B(x)}^C(c):C}</annotation></semantics></math></div> <ul> <li>Computation rules for dependent sum types:</li> </ul> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>z</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><mi>c</mi><mo>:</mo><mi>C</mi><mo stretchy="false">[</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>z</mi><mo stretchy="false">]</mo></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><msubsup><mi>β</mi> <mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow> <mi>C</mi></msubsup><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo><mo>:</mo><msubsup><mi mathvariant="normal">ind</mi> <mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow> <mi>C</mi></msubsup><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">[</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>z</mi><mo stretchy="false">]</mo><msub><mo>=</mo> <mrow><mi>C</mi><mo stretchy="false">[</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>z</mi><mo stretchy="false">]</mo></mrow></msub><mi>c</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} B(x) \vdash C \; \mathrm{type} \quad \Gamma, x:A, y:B \vdash c:C[\mathrm{in}(x, y)/z]}{\Gamma, x:A, y:B \vdash \beta_{\sum_{x:A} B(x)}^C(c):\mathrm{ind}_{\sum_{x:A} B(x)}^C(c)[\mathrm{in}(x, y)/z] =_{C[\mathrm{in}(x, y)/z]} c}</annotation></semantics></math></div> <ul> <li>Uniqueness rules for dependent sum types:</li> </ul> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>z</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>C</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><mi>c</mi><mo>:</mo><mi>C</mi><mo stretchy="false">[</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>z</mi><mo stretchy="false">]</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>z</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>u</mi><mo>:</mo><mi>C</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><msub><mi>i</mi> <mi mathvariant="normal">in</mi></msub><mo stretchy="false">(</mo><mi>u</mi><mo stretchy="false">)</mo><mo>:</mo><mi>u</mi><mo stretchy="false">[</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>z</mi><mo stretchy="false">]</mo><msub><mo>=</mo> <mrow><mi>C</mi><mo stretchy="false">[</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>z</mi><mo stretchy="false">]</mo></mrow></msub><mi>c</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>z</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><msubsup><mi>η</mi> <mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow> <mi>C</mi></msubsup><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo><mo>:</mo><mi>u</mi><msub><mo>=</mo> <mi>C</mi></msub><msubsup><mi mathvariant="normal">ind</mi> <mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow> <mi>C</mi></msubsup><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} B(x) \vdash C \; \mathrm{type} \quad \Gamma, x:A, y:B \vdash c:C[\mathrm{in}(x, y)/z] \quad \Gamma, z:\sum_{x:A} B(x) \vdash u:C \quad \Gamma, x:A, y:B \vdash i_\mathrm{in}(u):u[\mathrm{in}(x, y)/z] =_{C[\mathrm{in}(x, y)/z]} c}{\Gamma, z:\sum_{x:A} B(x) \vdash \eta_{\sum_{x:A} B(x)}^C(c):u =_{C} \mathrm{ind}_{\sum_{x:A} B(x)}^C(c)}</annotation></semantics></math></div> <p>Given a <a class="existingWikiWord" href="/nlab/show/pointed+type">pointed</a> <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a> <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 stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(A, a)</annotation></semantics></math>, the positive dependent sum type results in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{in}(a,-)</annotation></semantics></math> being an <a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a>.</p> <h4 id="as_a_negative_type">As a negative type</h4> <ul> <li>Elimination rules for dependent sum types:</li> </ul> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>z</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi></mrow></mfrac><mspace width="2em"></mspace><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>z</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi><mo stretchy="false">[</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, z:\sum_{x:A} B(x) \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, z:\sum_{x:A} B(x) \vdash \pi_2(z):B[\pi_1(z)/x]}</annotation></semantics></math></div> <ul> <li>Computation rules for dependent sum types:</li> </ul> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><msub><mi>β</mi> <mrow><mi>Σ</mi><mn>1</mn></mrow></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>:</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mi>A</mi></msub><mi>x</mi></mrow></mfrac><mspace width="2em"></mspace><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo>⊢</mo><msub><mi>β</mi> <mrow><mi>Σ</mi><mn>2</mn></mrow></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>:</mo><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><msub><mo>=</mo> <mrow><mi>B</mi><mo stretchy="false">[</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>x</mi><mo stretchy="false">]</mo></mrow></msub><mi>y</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \beta_{\Sigma 1}(x, y):\pi_1(\mathrm{in}(x, y)) =_A x} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, x:A, y:B \vdash \beta_{\Sigma 2}(x, y):\pi_2(\mathrm{in}(x, y)) =_{B[\pi_1(\mathrm{in}(x, y))/x]} y}</annotation></semantics></math></div> <ul> <li>Uniqueness rules for dependent sum types:</li> </ul> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><mrow><mi>Γ</mi><mo>,</mo><mi>z</mi><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><msub><mi>η</mi> <mi>Σ</mi></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>:</mo><mi>z</mi><msub><mo>=</mo> <mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></msub><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo>,</mo><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B \; \mathrm{type}}{\Gamma, z:\sum_{x:A} B(x) \vdash \eta_{\Sigma}(z):z =_{\sum_{x:A} B(x)} \mathrm{in}(\pi_1(z), \pi_2(z))}</annotation></semantics></math></div> <p>Given a <a class="existingWikiWord" href="/nlab/show/pointed+type">pointed</a> <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a> <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 stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(A, a)</annotation></semantics></math>, the negative dependent sum type results in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\pi_2(a,-)</annotation></semantics></math> being a <a class="existingWikiWord" href="/nlab/show/quasi-inverse+function">quasi-inverse function</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{in}(a,-)</annotation></semantics></math>, rather than an <a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a>. Thus, the positive definition is preferred to the negative definition. Alternatively, the negative dependent sum type should be defined as a <a class="existingWikiWord" href="/nlab/show/coinductive+type">coinductive type</a> rather than an <a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a>.</p> <h4 id="ExtensionalityPrinciple">Extensionality principle</h4> <p>The extensionality principle for the dependent sum type states that there is an <a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a> between the <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><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mrow><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></msub><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>a</mi><mo>′</mo><mo>,</mo><mi>b</mi><mo>′</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(a, b) =_{\sum_{x:A} B(x)} (a', b')</annotation></semantics></math> of a dependent sum type and the dependent sum <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>p</mi><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>a</mi><mo>′</mo></mrow></msub><mi>b</mi><msubsup><mo>=</mo> <mi>B</mi> <mi>p</mi></msubsup><mi>b</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">\sum_{p:a =_A a'} b =_B^p b'</annotation></semantics></math> of its component’s identity types:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>,</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>a</mi><mo>′</mo><mo>:</mo><mi>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>b</mi><mo>′</mo><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo>′</mo><mo stretchy="false">)</mo></mrow><mrow><mi>Γ</mi><mo>⊢</mo><msub><mi mathvariant="normal">ext</mi> <mi>Σ</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>a</mi><mo>′</mo><mo>,</mo><mi>b</mi><mo>′</mo><mo stretchy="false">)</mo><mo>:</mo><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>a</mi><mo>′</mo><mo>,</mo><mi>b</mi><mo>′</mo><mo stretchy="false">)</mo><mo>≃</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>p</mi><mo>:</mo><mi>a</mi><msub><mo>=</mo> <mi>A</mi></msub><mi>a</mi><mo>′</mo></mrow></munder><mi>b</mi><msubsup><mo>=</mo> <mi>B</mi> <mi>p</mi></msubsup><mi>b</mi><mo>′</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex"> \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B(a) \quad \Gamma \vdash a':A \quad \Gamma \vdash b':B(a')}{\Gamma \vdash \mathrm{ext}_{\Sigma}(a, b, a', b'):(a, b) =_{\sum_{x:A} B(x)} (a', b') \simeq \sum_{p:a =_A a'} b =_B^p b'} </annotation></semantics></math></div> <p>The comparison function itself is readily obtained by <a class="existingWikiWord" href="/nlab/show/Id-induction">Id-induction</a>. That this indeed constitutes an <a class="existingWikiWord" href="/nlab/show/equivalence+of+types">equivalence of types</a> is shown in <a href="#UFP13">UFP13, Thm. 2.7.2</a>.</p> <p id="ExtensionalityForDependentPairs"> In the notation of <a class="existingWikiWord" href="/nlab/show/dependent+pairs">dependent pairs</a> (<a class="existingWikiWord" href="/nlab/show/dependent+functions+and+dependent+pairs+--+table">here</a>) this reads:</p> <p><img src="/nlab/files/DependentPairExtensionality-230121.jpg" width="700" /></p> <p>Compare to the analogous extensionality principle for <a class="existingWikiWord" href="/nlab/show/dependent+functions">dependent functions</a> (see at <em><a class="existingWikiWord" href="/nlab/show/function+extensionality">function extensionality</a></em>, <a href="function+extensionality#StatementForDependentFunctions">here</a>):</p> <p><img src="/nlab/files/DependentFunctionExtensionality-230121.jpg" width="700" /></p> <p>(In this dependent generality this is a special case of <a href="#UFP13">UFP13, Lem. 2.9.7</a>.)</p> <h3 id="in_lambdacalculus">In lambda-calculus</h3> <p>The presentation of dependent sum type is almost exactly the same as that of <a class="existingWikiWord" href="/nlab/show/product+types">product types</a>, with the simple change that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> may depend on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>. In particular, they can be presented both as a <a class="existingWikiWord" href="/nlab/show/negative+type">negative type</a> or as a <a class="existingWikiWord" href="/nlab/show/positive+type">positive type</a>. In both cases, the rule for building the dependent sum type is the same:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>A</mi><mo lspace="verythinmathspace">:</mo><mi>Type</mi><mspace width="2em"></mspace><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>Type</mi></mrow><mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>Type</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex"> \frac{A\colon Type \qquad x\colon A\vdash B(x)\colon Type}{\sum_{x\colon A} B(x)\colon Type} </annotation></semantics></math></div> <p>but the constructors and eliminators may be different.</p> <h4 id="as_a_negative_type_2">As a negative type</h4> <p>When presented negatively, primacy is given to the eliminators. We specify that there are two ways to eliminate a term of type <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>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></msub><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{x\colon A} B(x)</annotation></semantics></math>: by projecting out the first component, or by projecting out the second.</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>p</mi><mo lspace="verythinmathspace">:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><mrow><msub><mi>π</mi> <mn>1</mn></msub><mi>p</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></mfrac><mspace width="2em"></mspace><mfrac><mrow><mi>p</mi><mo lspace="verythinmathspace">:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><mrow><msub><mi>π</mi> <mn>2</mn></msub><mi>p</mi><mo lspace="verythinmathspace">:</mo><mi>B</mi><mo stretchy="false">(</mo><msub><mi>π</mi> <mn>1</mn></msub><mi>p</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex"> \frac{p \colon \sum_{x\colon A} B(x)}{\pi_1 p\colon A} \qquad \frac{p\colon \sum_{x\colon A} B(x)}{\pi_2 p\colon B(\pi_1 p)}</annotation></semantics></math></div> <p>This then determines the form of the constructors: in order to construct a term of type <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>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></msub><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{x\colon A} B(x)</annotation></semantics></math>, we have to specify what value that term should yield when all the eliminators are applied to it. In other words, we have to specify a pair of elements, one <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a\colon A</annotation></semantics></math> (to be the value of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>1</mn></msub><mi>p</mi></mrow><annotation encoding="application/x-tex">\pi_1 p</annotation></semantics></math>) and one <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo lspace="verythinmathspace">:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">b\colon B(a)</annotation></semantics></math> (to be the value of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>2</mn></msub><mi>p</mi></mrow><annotation encoding="application/x-tex">\pi_2 p</annotation></semantics></math>).</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>a</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi><mspace width="2em"></mspace><mi>b</mi><mo lspace="verythinmathspace">:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><mrow><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex"> \frac{a\colon A \qquad b\colon B(a)}{(a,b)\colon \sum_{x\colon A} B(x)} </annotation></semantics></math></div> <p>Finally, we have computation rules which say that the relationship between the constructors and the eliminators is as we hoped. We always have <a class="existingWikiWord" href="/nlab/show/beta+reduction">beta reduction</a> rules</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>π</mi> <mn>1</mn></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><msub><mo>→</mo> <mi>β</mi></msub><mi>a</mi><mspace width="2em"></mspace><msub><mi>π</mi> <mn>2</mn></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><msub><mo>→</mo> <mi>β</mi></msub><mi>b</mi></mrow><annotation encoding="application/x-tex"> \pi_1(a,b) \to_\beta a \qquad \pi_2(a,b) \to_\beta b </annotation></semantics></math></div> <p>and we may or may not choose to have an <a class="existingWikiWord" href="/nlab/show/eta+reduction">eta reduction</a> rule</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msub><mi>π</mi> <mn>1</mn></msub><mi>p</mi><mo>,</mo><msub><mi>π</mi> <mn>2</mn></msub><mi>p</mi><mo stretchy="false">)</mo><msub><mo>→</mo> <mi>η</mi></msub><mi>p</mi></mrow><annotation encoding="application/x-tex"> (\pi_1 p, \pi_2 p) \to_\eta p </annotation></semantics></math></div> <h4 id="as_a_positive_type_2">As a positive type</h4> <p>When presented positively, primacy is given to the constructors. We specify that the way to construct something of type <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>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></msub><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{x\colon A} B(x)</annotation></semantics></math> is to give a term <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a\colon A</annotation></semantics></math> and a term <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi><mo lspace="verythinmathspace">:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">b\colon B(a)</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>a</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi><mspace width="2em"></mspace><mi>b</mi><mo lspace="verythinmathspace">:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><mrow><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex"> \frac{a\colon A \qquad b\colon B(a)}{(a,b)\colon \sum_{x\colon A} B(x)} </annotation></semantics></math></div> <p>Of course, this is the same as the constructor obtained from the negative presentation. However, the eliminator is different. Now, in order to say how to <em>use</em> something of type <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>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></msub><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{x\colon A} B(x)</annotation></semantics></math>, we have to specify how we should behave for all possible ways that it could have been constructed. In other words, we have to say, <em>assuming</em> that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math> were of the form <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>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(a,b)</annotation></semantics></math>, what we want to do. Thus we end up with the following rule:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mrow><mi>z</mi><mo lspace="verythinmathspace">:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>C</mi><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>Type</mi><mspace width="2em"></mspace><mi>p</mi><mo lspace="verythinmathspace">:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mspace width="2em"></mspace><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo lspace="verythinmathspace">:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>c</mi><mo lspace="verythinmathspace">:</mo><mi>C</mi><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><mrow><mi>let</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>p</mi><mi>in</mi><mi>c</mi><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mi>C</mi><mo stretchy="false">(</mo><mi>p</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex"> \frac{z\colon \sum_{x\colon A} B(x) \vdash C(z)\colon Type\qquad p\colon \sum_{x\colon A} B(x) \qquad x\colon A, y\colon B(x) \vdash c\colon C((x,y))}{let (x,y) = p in c \;\colon C(p)} </annotation></semantics></math></div> <p>We need a term <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math> in the context of two variables of types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, and the destructor or match “binds those variables” to the two components of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi></mrow><annotation encoding="application/x-tex">p</annotation></semantics></math>. Note that the “ordered pair” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(x,y)</annotation></semantics></math> in the destructor is just a part of the syntax; it is not an instance of the <em>constructor</em> ordered pair.</p> <p>Now we have the <a class="existingWikiWord" href="/nlab/show/beta+reduction">beta reduction</a> rule:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>let</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mi>in</mi><mi>c</mi><mspace width="thickmathspace"></mspace><msub><mo>→</mo> <mi>β</mi></msub><mspace width="thickmathspace"></mspace><mi>c</mi><mo stretchy="false">[</mo><mi>a</mi><mo stretchy="false">/</mo><mi>x</mi><mo>,</mo><mi>b</mi><mo stretchy="false">/</mo><mi>y</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex"> let (x,y) = (a,b) \,in c \;\to_\beta\; c[a/x, b/y] </annotation></semantics></math></div> <p>In other words, if we build an ordered pair and then break it apart, what we get is just the things we put into it. (The notation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi><mo stretchy="false">[</mo><mi>a</mi><mo stretchy="false">/</mo><mi>x</mi><mo>,</mo><mi>b</mi><mo stretchy="false">/</mo><mi>y</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">c[a/x, b/y]</annotation></semantics></math> means to substitute <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi></mrow><annotation encoding="application/x-tex">a</annotation></semantics></math> for <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> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math> for <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> in the term <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math>).</p> <p>And (if we wish) the <a class="existingWikiWord" href="/nlab/show/eta+reduction">eta reduction</a> rule, which is a little more subtle:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>let</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>p</mi><mi>in</mi><mi>c</mi><mo stretchy="false">[</mo><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>z</mi><mo stretchy="false">]</mo><mspace width="thickmathspace"></mspace><msub><mo>→</mo> <mi>η</mi></msub><mspace width="thickmathspace"></mspace><mi>c</mi><mo stretchy="false">[</mo><mi>p</mi><mo stretchy="false">/</mo><mi>z</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex"> let (x,y) = p in c[(x,y)/z] \;\to_\eta\; c[p/z] </annotation></semantics></math></div> <p>This says that if we break something of type <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>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi></mrow></msub><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> \sum_{x\colon A} B(x)</annotation></semantics></math> into its components, but then we only use those two components by way of putting them back together into an ordered pair, then we might as well just not have broken it down in the first place.</p> <p>Positively defined dependent sum types are naturally expressed as <a class="existingWikiWord" href="/nlab/show/inductive+types">inductive types</a>. For instance, in <a class="existingWikiWord" href="/nlab/show/Coq">Coq</a> syntax we have</p> <pre><code>Inductive sig (A:Type) (B:A->Type) : Type := | exist : forall (x:A), B x -> sig A B.</code></pre> <p>(Coq then implements beta-reduction, but not eta-reduction. However, eta-equivalence is provable with the internally defined <a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>, using the dependent eliminator mentioned above.)</p> <p>Arguably, negatively defined products should be naturally expressed as <a class="existingWikiWord" href="/nlab/show/coinductive+type">coinductive type</a>s, but this is not exactly the case for the presentation of coinductive types used in Coq.</p> <h4 id="positive_versus_negative">Positive versus negative</h4> <p>In ordinary “nonlinear” <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, the positive and negative dependent sum types are equivalent, just as in the case of <a class="existingWikiWord" href="/nlab/show/product+types">product types</a>. They manifestly have the same constructor, while we can define the eliminators in terms of each other as follows:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable displaystyle="true" columnalign="right left right left right left right left right left" columnspacing="0em"><mtr><mtd><msub><mi>π</mi> <mn>1</mn></msub><mi>p</mi></mtd> <mtd><mspace width="thickmathspace"></mspace><mo>≔</mo><mspace width="thickmathspace"></mspace><mi>let</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>p</mi><mspace width="thinmathspace"></mspace><mi>in</mi><mspace width="thinmathspace"></mspace><mi>x</mi></mtd></mtr> <mtr><mtd><msub><mi>π</mi> <mn>2</mn></msub><mi>p</mi></mtd> <mtd><mspace width="thickmathspace"></mspace><mo>≔</mo><mspace width="thickmathspace"></mspace><mi>let</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>p</mi><mspace width="thinmathspace"></mspace><mi>in</mi><mspace width="thinmathspace"></mspace><mi>y</mi></mtd></mtr> <mtr><mtd><mi>let</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>p</mi><mi>in</mi><mi>c</mi></mtd> <mtd><mspace width="thickmathspace"></mspace><mo>≔</mo><mspace width="thickmathspace"></mspace><mi>c</mi><mo stretchy="false">[</mo><msub><mi>π</mi> <mn>1</mn></msub><mi>p</mi><mo stretchy="false">/</mo><mi>x</mi><mo>,</mo><msub><mi>π</mi> <mn>2</mn></msub><mi>p</mi><mo stretchy="false">/</mo><mi>y</mi><mo stretchy="false">]</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \begin{aligned} \pi_1 p &\;\coloneqq\; let (x,y) = p \,in\, x\\ \pi_2 p &\;\coloneqq\; let (x,y) = p \,in\, y\\ let (x,y) = p in c &\;\coloneqq\; c[\pi_1 p / x, \pi_2 p / y] \end{aligned} </annotation></semantics></math></div> <p>The <a class="existingWikiWord" href="/nlab/show/computation+rules">computation rules</a> then also correspond, just as for <a class="existingWikiWord" href="/nlab/show/product+types">product types</a>.</p> <p>Also just as for <a class="existingWikiWord" href="/nlab/show/product+types">product types</a>, in order to recover the important <em>dependent</em> eliminator for the positive product type from the eliminators for the negative product type, we need the latter to satisfy the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>η</mi></mrow><annotation encoding="application/x-tex">\eta</annotation></semantics></math>-conversion rule so as to make the above definition well-typed. By inserting a transport, we can make do with a <a href="/nlab/show/eta-conversion#Propositional">propositional</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">\eta</annotation></semantics></math>-conversion, which is also provable from the dependent eliminator.</p> <p>One might expect that in “<a class="existingWikiWord" href="/nlab/show/dependent+linear+type+theory">dependent linear type theory</a>” the positive and negative dependent sums would become different. However, the meaning of the quoted phrase is unclear.</p> <h3 id="using_universes_and_dependent_product_types">Using universes and dependent product types</h3> <p>Dependent sum types could be defined directly from universes, dependent product types, and function types - the last of which are definable from dependent product types. Given a <a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>, the dependent sum type of the type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A \vdash B(x)</annotation></semantics></math> is defined as the dependent product type</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≔</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>P</mi><mo>:</mo><mi>U</mi></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>→</mo><mi>P</mi><mo stretchy="false">)</mo><mo>→</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">\sum_{x:A} B(x) \coloneqq \prod_{P:U} \prod_{x:A} (B(x) \to P) \to P</annotation></semantics></math></div> <p>This was the first definition of dependent sum types in dependent type theory, appearing in <a class="existingWikiWord" href="/nlab/show/Per+Martin-L%C3%B6f">Per Martin-Löf</a>‘s <a href="#ML71">original 1971 paper</a> on dependent type theory.</p> <h2 id="properties">Properties</h2> <h3 id="descent_and_large_elimination">Descent and large elimination</h3> <p>The <a class="existingWikiWord" href="/nlab/show/descent">descent</a> for the positive dependent sum type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mi>x</mi><mo>:</mo><mi>A</mi><mo>.</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\Sigma x:A.B(x)</annotation></semantics></math> states that given any type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>C</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A, y:B(x) \vdash C(x, y)</annotation></semantics></math> one can construct a type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>z</mi><mo>:</mo><mi>Σ</mi><mi>x</mi><mo>:</mo><mi>A</mi><mo>.</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><msubsup><mi mathvariant="normal">descFam</mi> <mrow><mi>Σ</mi><mi>x</mi><mo>:</mo><mi>A</mi><mo>.</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow> <mi>C</mi></msubsup><mo stretchy="false">(</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">z:\Sigma x:A.B(x) \vdash \mathrm{descFam}_{\Sigma x:A.B(x)}^{C}(z)</annotation></semantics></math> with families of <a class="existingWikiWord" href="/nlab/show/equivalences+of+types">equivalences of types</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><msubsup><mi mathvariant="normal">descEquiv</mi> <mrow><mi>Σ</mi><mi>x</mi><mo>:</mo><mi>A</mi><mo>.</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow> <mi>C</mi></msubsup><mo>:</mo><msubsup><mi mathvariant="normal">descFam</mi> <mrow><mi>Σ</mi><mi>x</mi><mo>:</mo><mi>A</mi><mo>.</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow> <mi>C</mi></msubsup><mo stretchy="false">(</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≃</mo><mi>C</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A, y:B(x) \vdash \mathrm{descEquiv}_{\Sigma x:A.B(x)}^C:\mathrm{descFam}_{\Sigma x:A.B(x)}^{C}(\mathrm{in}(x, y)) \simeq C(x, y)</annotation></semantics></math></div> <p>Large elimination for positive dependent sum types strengthens the equivalences of types in descent to <a class="existingWikiWord" href="/nlab/show/judgmental+equality+of+types">judgmental equality of types</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>,</mo><mi>y</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>⊢</mo><msubsup><mi mathvariant="normal">descFam</mi> <mrow><mi>Σ</mi><mi>x</mi><mo>:</mo><mi>A</mi><mo>.</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow> <mi>C</mi></msubsup><mo stretchy="false">(</mo><mi mathvariant="normal">in</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≡</mo><mi>C</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">x:A, y:B(x) \vdash \mathrm{descFam}_{\Sigma x:A.B(x)}^{C}(\mathrm{in}(x, y)) \equiv C(x, y) \; \mathrm{type}</annotation></semantics></math></div> <h3 id="typal_congruence_rules">Typal congruence rules</h3> <p>These are called <em>typal congruence rules</em> because they are the analogue of the judgmental <a class="existingWikiWord" href="/nlab/show/congruence+rules">congruence rules</a> which use <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a> and <a class="existingWikiWord" href="/nlab/show/equivalence+types">equivalence types</a> instead of <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a>:</p> <p> <div class='num_theorem'> <h6>Theorem</h6> <p>Given types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">A'</annotation></semantics></math> and type families <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A \vdash B(x)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mo>′</mo><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A \vdash B'(x)</annotation></semantics></math> and equivalences <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>e</mi> <mi>A</mi></msub><mo>:</mo><mi>A</mi><mo>≃</mo><mi>A</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">e_A:A \simeq A'</annotation></semantics></math> and dependent function of equivalences <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>e</mi> <mi>B</mi></msub><mo>:</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></msub><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>B</mi><mo>′</mo><mo stretchy="false">(</mo><msub><mi>e</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">e_B:\prod_{x:A} B(x) \simeq B'(e_A(x))</annotation></semantics></math>, there is an equivalence</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">congform</mi> <mi>Σ</mi></msub><mo stretchy="false">(</mo><msub><mi>e</mi> <mi>A</mi></msub><mo>,</mo><msub><mi>e</mi> <mi>B</mi></msub><mo stretchy="false">)</mo><mo>:</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>)</mo></mrow><mo>≃</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>)</mo></mrow></mrow><annotation encoding="application/x-tex">\mathrm{congform}_\Sigma(e_A, e_B):\left(\prod_{x:A} B(x)\right) \simeq \left(\prod_{x:A} B(x)\right)</annotation></semantics></math></div> <p></p> </div> </p> <p> <div class='proof'> <h6>Proof</h6> <p>This is theorem 11.1.6 of <a href="#Rijke22">Rijke 2022</a>, and a proof of this is given in that reference.</p> </div> </p> <p>The typal congruence rules for dependent sum types are very important for proving various other theorems in dependent type theory. For example,</p> <p> <div class='num_theorem'> <h6>Theorem</h6> <p>Given a <a class="existingWikiWord" href="/nlab/show/univalent">univalent</a> <a class="existingWikiWord" href="/nlab/show/Tarski+universe">Tarski universe</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>U</mi><mo>,</mo><mi>T</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(U, T)</annotation></semantics></math> and a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math>-small type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">A:U</annotation></semantics></math>, the dependent sum type <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>B</mi><mo>:</mo><mi>U</mi></mrow></msub><mi>T</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>T</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{B:U} T(B) \simeq T(A)</annotation></semantics></math> is contractible.</p> </div> </p> <p> <div class='proof'> <h6>Proof</h6> <p>By univalence, for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">A:U</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo>:</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">B:U</annotation></semantics></math>, transport across the universal type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi></mrow><annotation encoding="application/x-tex">T</annotation></semantics></math> is an equivalence of types</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">ua</mi><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo><mo>:</mo><mi mathvariant="normal">isEquiv</mi><mo stretchy="false">(</mo><msub><mi mathvariant="normal">transport</mi> <mrow><mi>x</mi><mo>:</mo><mi>U</mi><mo>.</mo><mi>T</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{ua}(A, B):\mathrm{isEquiv}(\mathrm{transport}_{x:U.T(x)}(A, B))</annotation></semantics></math></div> <p>and thus we have the equivalence</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">pair</mi><mo stretchy="false">(</mo><msub><mi mathvariant="normal">transport</mi> <mrow><mi>x</mi><mo>:</mo><mi>U</mi><mo>.</mo><mi>T</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo><mo>,</mo><mi mathvariant="normal">ua</mi><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>:</mo><mo stretchy="false">(</mo><mi>A</mi><msub><mo>=</mo> <mi>U</mi></msub><mi>B</mi><mo stretchy="false">)</mo><mo>≃</mo><mo stretchy="false">(</mo><mi>T</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>T</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{pair}(\mathrm{transport}_{x:U.T(x)}(A, B), \mathrm{ua}(A, B)):(A =_U B) \simeq (T(B) \simeq T(A))</annotation></semantics></math></div> <p>and thus by the typal congruence rule of dependent sum types, we have</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">congform</mi> <mi>Σ</mi></msub><mo stretchy="false">(</mo><msub><mi mathvariant="normal">id</mi> <mi>U</mi></msub><mo>,</mo><mi>λ</mi><mi>B</mi><mo>:</mo><mi>U</mi><mo>.</mo><mi mathvariant="normal">pair</mi><mo stretchy="false">(</mo><msub><mi mathvariant="normal">transport</mi> <mrow><mi>x</mi><mo>:</mo><mi>U</mi><mo>.</mo><mi>T</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo><mo>,</mo><mi mathvariant="normal">ua</mi><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>:</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>B</mi><mo>:</mo><mi>U</mi></mrow></munder><mo stretchy="false">(</mo><mi>A</mi><msub><mo>=</mo> <mi>U</mi></msub><mi>B</mi><mo stretchy="false">)</mo><mo>)</mo></mrow><mo>≃</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>B</mi><mo>:</mo><mi>U</mi></mrow></munder><mo stretchy="false">(</mo><mi>T</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>T</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>)</mo></mrow></mrow><annotation encoding="application/x-tex">\mathrm{congform}_\Sigma(\mathrm{id}_U, \lambda B:U.\mathrm{pair}(\mathrm{transport}_{x:U.T(x)}(A, B), \mathrm{ua}(A, B))):\left(\sum_{B:U} (A =_U B)\right) \simeq \left(\sum_{B:U} (T(B) \simeq T(A))\right)</annotation></semantics></math></div> <p>Since the type <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>B</mi><mo>:</mo><mi>U</mi></mrow></msub><mo stretchy="false">(</mo><mi>A</mi><msub><mo>=</mo> <mi>U</mi></msub><mi>B</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{B:U} (A =_U B)</annotation></semantics></math> is contractible for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">A:U</annotation></semantics></math>, the above equivalence implies that <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>B</mi><mo>:</mo><mi>U</mi></mrow></msub><mo stretchy="false">(</mo><mi>T</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>T</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{B:U} (T(B) \simeq T(A))</annotation></semantics></math> is also contractible.</p> </div> </p> <h3 id="quantification_in_dependent_type_theory">Quantification in dependent type theory</h3> <p>Given a family of types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A \vdash B(x)</annotation></semantics></math>, the <a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a> is defined as the <a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of the dependent sum type</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>∃</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>.</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≔</mo><mrow><mo>[</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>]</mo></mrow></mrow><annotation encoding="application/x-tex">\exists x:A.B(x) \coloneqq \left[\sum_{x:A} B(x)\right]</annotation></semantics></math></div> <p>The <a class="existingWikiWord" href="/nlab/show/uniqueness+quantifier">uniqueness quantifier</a> is defined as the <a class="existingWikiWord" href="/nlab/show/isContr">isContr</a> <a class="existingWikiWord" href="/nlab/show/modality">modality</a> of the dependent sum type</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>∃</mo><mo>!</mo><mi>x</mi><mo>:</mo><mi>A</mi><mo>.</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≔</mo><mi mathvariant="normal">isContr</mi><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>)</mo></mrow></mrow><annotation encoding="application/x-tex">\exists! x:A.B(x) \coloneqq \mathrm{isContr}\left(\sum_{x:A} B(x)\right)</annotation></semantics></math></div> <p>There is also a quantifier which states that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> holds for at most one element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">x:A</annotation></semantics></math>, defined by the <a class="existingWikiWord" href="/nlab/show/isProp">isProp</a> <a class="existingWikiWord" href="/nlab/show/modality">modality</a> of the dependent sum type:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">isProp</mi><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>)</mo></mrow></mrow><annotation encoding="application/x-tex">\mathrm{isProp}\left(\sum_{x:A} B(x)\right)</annotation></semantics></math></div> <p>In each of the last two cases, one could prove that each dependent type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(x)</annotation></semantics></math> has to be a <a class="existingWikiWord" href="/nlab/show/mere+proposition">mere proposition</a>.</p> <p>Given a natural number <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo>:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">n:\mathbb{N}</annotation></semantics></math> and given a family of types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">x:A \vdash B(x)</annotation></semantics></math>, we can similarly write down <a class="existingWikiWord" href="/nlab/show/quantifiers">quantifiers</a> to say that</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> holds for exactly <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> elements:<div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mo>[</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mrow><mo>[</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>]</mo></mrow><mo>)</mo></mrow><mo>≃</mo><mi mathvariant="normal">Fin</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>]</mo></mrow></mrow><annotation encoding="application/x-tex">\left[\left(\sum_{x:A} \left[B(x)\right]\right) \simeq \mathrm{Fin}(n)\right]</annotation></semantics></math></div></li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> holds for at most <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> elements:<div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mo>[</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mrow><mo>[</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>]</mo></mrow><mo>)</mo></mrow><mo>↪</mo><mi mathvariant="normal">Fin</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>]</mo></mrow></mrow><annotation encoding="application/x-tex">\left[\left(\sum_{x:A} \left[B(x)\right]\right) \hookrightarrow \mathrm{Fin}(n)\right]</annotation></semantics></math></div></li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> holds for at least <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> elements:<div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mo>[</mo><mi mathvariant="normal">Fin</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>↪</mo><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mrow><mo>[</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>]</mo></mrow><mo>)</mo></mrow><mo>]</mo></mrow></mrow><annotation encoding="application/x-tex">\left[\mathrm{Fin}(n) \hookrightarrow \left(\sum_{x:A} \left[B(x)\right]\right)\right]</annotation></semantics></math></div> <p>where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>≃</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A \simeq B</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/equivalence+type">equivalence type</a> between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>↪</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A \hookrightarrow B</annotation></semantics></math> is the type of <a class="existingWikiWord" href="/nlab/show/embeddings">embeddings</a> between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>, and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">Fin</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{Fin}(n)</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/finite+set">finite set</a> with <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> elements.</p> </li> </ul> <h2 id="categorical_interpretation">Categorical interpretation</h2> <p>Under <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a>, a dependent type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo lspace="verythinmathspace">:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">x\colon A \vdash B(x)\colon Type</annotation></semantics></math> corresponds to a <a class="existingWikiWord" href="/nlab/show/fibration">fibration</a> or <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><mi>B</mi><mo>→</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">B\to A</annotation></semantics></math>. In this case, the dependent sum is just the <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>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math>. This requires the dependent sum type to satisfy both <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>β</mi></mrow><annotation encoding="application/x-tex">\beta</annotation></semantics></math>- and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>η</mi></mrow><annotation encoding="application/x-tex">\eta</annotation></semantics></math>-conversion.</p> <p>There is also another interpretation in category theory of the dependent sum type over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>A</mi><mo>⊢</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mrow><annotation encoding="application/x-tex">x:A \vdash B(x) \; \mathrm{type}</annotation></semantics></math> as the <a class="existingWikiWord" href="/nlab/show/initial">initial</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>-indexed <a class="existingWikiWord" href="/nlab/show/wide+cospan">wide cospan</a> over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(x)</annotation></semantics></math>, the object <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>x</mi><mo>:</mo><mi>A</mi></mrow></msub><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{x:A} B(x)</annotation></semantics></math> with a family of morphisms</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">in</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>→</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></munder><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{in}_A(x):B(x) \to \sum_{x:A} B(x)</annotation></semantics></math></div> <p>such that for any other object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> with a family of morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">f(x):B(x) \to C</annotation></semantics></math>, there exists a unique morphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>u</mi> <mi>C</mi></msub><mo>:</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>x</mi><mo>:</mo><mi>A</mi></mrow></msub><mi>B</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>→</mo><mi>C</mi></mrow><annotation encoding="application/x-tex">u_C:\sum_{x:A} B(x) \to C</annotation></semantics></math> such that</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>u</mi> <mi>C</mi></msub><mo>∘</mo><msub><mi mathvariant="normal">in</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>=</mo><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">u_C \circ \mathrm{in}_A(x) = f(x)</annotation></semantics></math></div> <p>This corresponds to the positive dependent sum types.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a>, <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/telescope+type">telescope type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/product+type">product type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/dependent+pushout+type">dependent pushout type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/record+type">record type</a></p> </li> </ul> <h2 id="references">References</h2> <p>A textbook account could be found in section 4.6 of:</p> <ul> <li id="Rijke22"><a class="existingWikiWord" href="/nlab/show/Egbert+Rijke">Egbert Rijke</a>, <em><a class="existingWikiWord" href="/nlab/show/Introduction+to+Homotopy+Type+Theory">Introduction to Homotopy Type Theory</a></em>, Cambridge Studies in Advanced Mathematics, Cambridge University Press (<a href="https://arxiv.org/abs/2212.11082">arXiv:2212.11082</a>)</li> </ul> <p>Discussion in a context of <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>:</p> <ul> <li id="UFP13"><a class="existingWikiWord" href="/nlab/show/Univalent+Foundations+Project">Univalent Foundations Project</a>, <em><a class="existingWikiWord" href="/nlab/show/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics">Homotopy Type Theory – Univalent Foundations of Mathematics</a></em> (2013) [<a href="http://homotopytypetheory.org/book/">web</a>, <a href="http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf">pdf</a>]</li> </ul> <p>For the definition of dependent sum types in terms of universes, dependent product types, and function types, see:</p> <ul> <li id="ML71"><a class="existingWikiWord" href="/nlab/show/Per+Martin-L%C3%B6f">Per Martin-Löf</a>, <em>A Theory of Types</em>, unpublished note (1971) [<a href="https://raw.githubusercontent.com/michaelt/martin-lof/master/pdfs/martin-loef1971%20-%20A%20Theory%20of%20Types.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/MartinLoef1971-ATheoryOfTypes.pdf" title="pdf">pdf</a>]</li> </ul> <p>See also most references at <em><a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a></em>.</p> </body></html> </div> <div class="revisedby"> <p> Last revised on May 17, 2024 at 14:43:19. See the <a href="/nlab/history/dependent+sum+type" 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/dependent+sum+type" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/15823/#Item_5">Discuss</a><span class="backintime"><a href="/nlab/revision/dependent+sum+type/26" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/dependent+sum+type" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/dependent+sum+type" accesskey="S" class="navlink" id="history" rel="nofollow">History (26 revisions)</a> <a href="/nlab/show/dependent+sum+type/cite" style="color: black">Cite</a> <a href="/nlab/print/dependent+sum+type" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/dependent+sum+type" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>