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> uniqueness of identity proofs 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> uniqueness of identity proofs </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/4570/#Item_20" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="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> <h4 id="foundational_axiom">Foundational axiom</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/foundational+axiom">foundational</a> <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a></strong></p> <ul> <li> <p>basic constructions:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+cartesian+products">axiom of cartesian products</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+disjoint+unions">axiom of disjoint unions</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+the+empty+set">axiom of the empty set</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+fullness">axiom of fullness</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+function+sets">axiom of function sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+power+sets">axiom of power sets</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+quotient+sets">axiom of quotient sets</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/material+set+theory">material axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+extensionality">axiom of extensionality</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+foundation">axiom of foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+anti-foundation">axiom of anti-foundation</a></li> <li><a class="existingWikiWord" href="/nlab/show/Mostowski%27s+axiom">Mostowski's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+pairing">axiom of pairing</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+transitive+closure">axiom of transitive closure</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+union">axiom of union</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/structural+set+theory">structural axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+materialization">axiom of materialization</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theoretic axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axioms+of+set+truncation">axioms of set truncation</a> <ul> <li><a class="existingWikiWord" href="/nlab/show/uniqueness+of+identity+proofs">uniqueness of identity proofs</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></li> <li><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/equality+reflection">equality reflection</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></li> </ul> </li> <li><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theoretic axioms</a>: <ul> <li><a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/Whitehead%27s+principle">Whitehead's principle</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axioms+of+choice">axioms of choice</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+choice">axiom of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+countable+choice">axiom of countable choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+dependent+choice">axiom of dependent choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+excluded+middle">axiom of excluded middle</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+existence">axiom of existence</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+multiple+choice">axiom of multiple choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/Markov%27s+axiom">Markov's axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/presentation+axiom">presentation axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/small+cardinality+selection+axiom">small cardinality selection axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+small+violations+of+choice">axiom of small violations of choice</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+weakly+initial+sets+of+covers">axiom of weakly initial sets of covers</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/large+cardinal+axioms">large cardinal axioms</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+infinity">axiom of infinity</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+universes">axiom of universes</a></li> <li><a class="existingWikiWord" href="/nlab/show/regular+extension+axiom">regular extension axiom</a></li> <li><a class="existingWikiWord" href="/nlab/show/inaccessible+cardinal">inaccessible cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/measurable+cardinal">measurable cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/elementary+embedding">elementary embedding</a></li> <li><a class="existingWikiWord" href="/nlab/show/supercompact+cardinal">supercompact cardinal</a></li> <li><a class="existingWikiWord" href="/nlab/show/Vop%C4%9Bnka%27s+principle">Vopěnka's principle</a></li> </ul> </li> <li> <p>strong axioms</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+separation">axiom of separation</a></li> <li><a class="existingWikiWord" href="/nlab/show/axiom+of+replacement">axiom of replacement</a></li> </ul> </li> <li> <p>further</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/reflection+principle">reflection principle</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+inequality+spaces">axiom of inequality spaces</a></p> </li> </ul> </div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <li><a href='#statement'>Statement</a></li> <ul> <li><a href='#for_individual_types'>For individual types</a></li> <li><a href='#for_type_families_and_universes'>For type families and universes</a></li> <li><a href='#as_a_rule_in_the_type_theory'>As a rule in the type theory</a></li> <li><a href='#uniqueness_of_identity_proofs_for_heterogeneous_identity_types'>Uniqueness of identity proofs for heterogeneous identity types</a></li> </ul> <li><a href='#properties'>Properties</a></li> <ul> <li><a href='#uniqueness_of_identity_proofs_and_univalence'>Uniqueness of identity proofs and univalence</a></li> </ul> <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>, <em>uniqueness of identity proofs</em> or <em>UIP</em> refers to a couple of different axioms and rules applicable to individual <a class="existingWikiWord" href="/nlab/show/types">types</a> to turn them into <a class="existingWikiWord" href="/nlab/show/h-sets">h-sets</a>, <a class="existingWikiWord" href="/nlab/show/type+families">type families</a> to turn them into <a class="existingWikiWord" href="/nlab/show/families+of+sets">families of sets</a> (and in particular, <a class="existingWikiWord" href="/nlab/show/universes">universes</a> to turn them into internal types of sets), as well as the type theory as a whole to turn it into an actual <a class="existingWikiWord" href="/nlab/show/set-level+type+theory">set-level type theory</a>, where all types are <a class="existingWikiWord" href="/nlab/show/h-sets">h-sets</a>. Under certain conditions, uniqueness of identity proofs for universes is incompatible with the <a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a>, and uniqueness of identity proofs for the whole type theory is incompatible with the existence of a <a class="existingWikiWord" href="/nlab/show/univalent+universe">univalent universe</a>.</p> <p>Heuristically, the axiom asserts that for each element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a:A</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>A</mi></mrow><annotation encoding="application/x-tex">b:A</annotation></semantics></math>, every two <a class="existingWikiWord" href="/nlab/show/identification">identification</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p:\mathrm{Id}_A(a, b)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">q:\mathrm{Id}_A(a, b)</annotation></semantics></math> of 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><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{Id}_A(a, b)</annotation></semantics></math> are <a class="existingWikiWord" href="/nlab/show/typal+equality">typally equal</a> to each other. This is equivalent to saying that every identity type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{Id}_A(a, b)</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>.</p> <h2 id="statement">Statement</h2> <p>There are multiple notions of uniqueness of identity proofs: for individual types, for type families and Tarski universes, and for the type theory itself.</p> <h3 id="for_individual_types">For individual types</h3> <p>Given a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, uniqueness of identity proofs is the axiom that for all elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a:A</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>A</mi></mrow><annotation encoding="application/x-tex">b:A</annotation></semantics></math> and identifications <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p:\mathrm{Id}_A(a, b)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">q:\mathrm{Id}_A(a, b)</annotation></semantics></math>, there is an identification <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">UIP</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>q</mi><mo stretchy="false">)</mo><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mrow><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>p</mi><mo>,</mo><mi>q</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{UIP}_A(a, b, p, q):\mathrm{Id}_{\mathrm{Id}_A(a, b)}(p, q)</annotation></semantics></math>. This is the same as stating that there is a dependent function</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">UIP</mi> <mi>A</mi></msub><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>b</mi><mo>:</mo><mi>A</mi></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow></munder><msub><mi mathvariant="normal">Id</mi> <mrow><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>p</mi><mo>,</mo><mi>q</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{UIP}_A:\prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} \prod_{q:\mathrm{Id}_A(a, b)} \mathrm{Id}_{\mathrm{Id}_A(a, b)}(p, q)</annotation></semantics></math></div> <p>Uniqueness of identity proofs implies that <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> is an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>, and can be used in the definition of an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>.</p> <h3 id="for_type_families_and_universes">For type families and universes</h3> <p>Uniqueness of identity proofs for type families <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> says that given a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> with a type family <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(a)</annotation></semantics></math> indexed by elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a:A</annotation></semantics></math>, the typal uniqueness of identity proofs holds for the 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>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(a)</annotation></semantics></math> of every element of the index type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a:A</annotation></semantics></math>. This is the same as stating that there is a dependent function</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">UIP</mi> <mrow><mi>A</mi><mo>,</mo><mi>B</mi></mrow></msub><mo>:</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>b</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>c</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo></mrow></munder><msub><mi mathvariant="normal">Id</mi> <mrow><msub><mi mathvariant="normal">Id</mi> <mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>b</mi><mo>,</mo><mi>c</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>p</mi><mo>,</mo><mi>q</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathrm{UIP}_{A, B}: \prod_{a:A} \prod_{b:B(a)} \prod_{c:B(a)} \prod_{p:\mathrm{Id}_{B(a)}(b, c)} \prod_{q:\mathrm{Id}_{B(a)}(b, c)} \mathrm{Id}_{\mathrm{Id}_{B(a)}(b, c)}(p, q)</annotation></semantics></math></div> <p>This definition of uniqueness of identity proofs could be used in the definition of <a class="existingWikiWord" href="/nlab/show/family+of+sets">family of sets</a>. Since this definition applies to type families, this should probably be called the <strong>familial uniqueness of identity proofs</strong> to distinguish it from the uniqueness of identity proofs axiom above.</p> <p>Since every Tarski universe consists of a type <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> of encodings and a 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> representing the actual small types indexed by the type <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>, with addition structure representing the closure of <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> under all type formers, the familial uniqueness of identity proofs definition works for Tarski universes as well, and this could equivalently be called the <strong>Tarski universe uniqueness of identity proofs</strong>.</p> <h3 id="as_a_rule_in_the_type_theory">As a rule in the type theory</h3> <p>Uniqueness of identity proofs could also be rewritten as a rule instead of an axiom, by making the hypotheses of the axioms into premises of the rule. This makes uniqueness of identity proofs applicable not only to universes, but to the entire type theory. In addition, one could use, in addition to <a class="existingWikiWord" href="/nlab/show/typal+equality">typal equality</a>, either <a class="existingWikiWord" href="/nlab/show/judgmental+equality">judgmental equality</a> or <a class="existingWikiWord" href="/nlab/show/propositional+equality">propositional equality</a>, resulting in <strong>judgmental uniqueness of identity proofs</strong> and <strong>propositional uniqueness of identity proofs</strong>, with the original uniqueness of identity proofs axiom called <strong>typal uniqueness of identity proofs</strong></p> <p>In this manner, uniqueness of identity proofs then becomes the rules:</p> <ul> <li>Judgmental uniqueness of identity proofs</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>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>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>≡</mo><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; type \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash q:\mathrm{Id}_A(a, b)}{\Gamma \vdash p \equiv q:\mathrm{Id}_A(a, b)}</annotation></semantics></math></div> <ul> <li>Propositional uniqueness of identity proofs</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>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>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><mrow><mi>Γ</mi><mo>⊢</mo><mi>p</mi><msub><mo>=</mo> <mrow><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow></msub><mi>q</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; type \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash q:\mathrm{Id}_A(a, b)}{\Gamma \vdash p =_{\mathrm{Id}_A(a, b)} q \; \mathrm{true}}</annotation></semantics></math></div> <ul> <li>Typal uniqueness of identity proofs</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>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>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><mrow><mi>Γ</mi><mo>⊢</mo><msub><mi mathvariant="normal">UIP</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>q</mi><mo stretchy="false">)</mo><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mrow><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>p</mi><mo>,</mo><mi>q</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{\Gamma \vdash A \; type \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash q:\mathrm{Id}_A(a, b)}{\Gamma \vdash \mathrm{UIP}_A(a, b, p, q):\mathrm{Id}_{\mathrm{Id}_A(a, b)}(p, q)}</annotation></semantics></math></div> <p>Uniqueness of identity proofs is a <a class="existingWikiWord" href="/nlab/show/axiom+of+set+truncation">axiom of set truncation</a>, and turns the type theory into a <a class="existingWikiWord" href="/nlab/show/set-level+type+theory">set-level type theory</a>. Judgmental uniqueness of identity proofs holds in <a class="existingWikiWord" href="/nlab/show/XTT">XTT</a>, where it follows from <a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a>.</p> <h3 id="uniqueness_of_identity_proofs_for_heterogeneous_identity_types">Uniqueness of identity proofs for heterogeneous identity types</h3> <p>There is also a notion of uniqueness of identity proofs for <a class="existingWikiWord" href="/nlab/show/heterogeneous+identity+types">heterogeneous identity types</a>, which is given by the following rule:</p> <ul> <li> <p>Judgmental uniqueness of identity proofs for heterogeneous identity types:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mtable displaystyle="false" rowspacing="0.5ex" columnalign="left"><mtr><mtd><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>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mtd></mtr> <mtr><mtd><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>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>y</mi><mo>:</mo><mi>B</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>z</mi><mo>:</mo><mi>B</mi></mtd></mtr> <mtr><mtd><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>r</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr></mtable><mrow><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>≡</mo><mi>r</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B \quad \Gamma \vdash z:B \\ \Gamma \vdash q:\mathrm{hId}_{B}(a, b, p, y, z) \quad \Gamma \vdash r:\mathrm{hId}_{B}(a, b, p, y, z) \end{array} }{\Gamma \vdash q \equiv r:\mathrm{hId}_{B}(a, b, p, y, z)} </annotation></semantics></math></div></li> <li> <p>Propositional uniqueness of identity proofs for heterogeneous identity types:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mtable displaystyle="false" rowspacing="0.5ex" columnalign="left"><mtr><mtd><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>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mtd></mtr> <mtr><mtd><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>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>y</mi><mo>:</mo><mi>B</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>z</mi><mo>:</mo><mi>B</mi></mtd></mtr> <mtr><mtd><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>r</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr></mtable><mrow><mi>Γ</mi><mo>⊢</mo><mi>q</mi><msub><mo>=</mo> <mrow><msub><mi mathvariant="normal">hId</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow></msub><mi>r</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B \quad \Gamma \vdash z:B \\ \Gamma \vdash q:\mathrm{hId}_{B}(a, b, p, y, z) \quad \Gamma \vdash r:\mathrm{hId}_{B}(a, b, p, y, z) \end{array} }{\Gamma \vdash q =_{\mathrm{hId}_{B}(a, b, p, y, z)} r \; \mathrm{true}} </annotation></semantics></math></div></li> <li> <p>Typal uniqueness of identity proofs for heterogeneous identity types:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mtable displaystyle="false" rowspacing="0.5ex" columnalign="left"><mtr><mtd><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>B</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">type</mi></mtd></mtr> <mtr><mtd><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>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>y</mi><mo>:</mo><mi>B</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>z</mi><mo>:</mo><mi>B</mi></mtd></mtr> <mtr><mtd><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>r</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr></mtable><mrow><mi>Γ</mi><mo>⊢</mo><msub><mi mathvariant="normal">UIP</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo>,</mo><mi>q</mi><mo>,</mo><mi>r</mi><mo stretchy="false">)</mo><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mrow><msub><mi mathvariant="normal">hId</mi> <mi>B</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>q</mi><mo>,</mo><mi>r</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B \quad \Gamma \vdash z:B \\ \Gamma \vdash q:\mathrm{hId}_{B}(a, b, p, y, z) \quad \Gamma \vdash r:\mathrm{hId}_{B}(a, b, p, y, z) \end{array} }{\Gamma \vdash \mathrm{UIP}_{B}(a, b, p, y, z, q, r):\mathrm{Id}_{\mathrm{hId}_{B}(a, b, p, y, z)}(q, r)} </annotation></semantics></math></div></li> </ul> <p>and likewise for <a class="existingWikiWord" href="/nlab/show/dependent+heterogeneous+identity+types">dependent heterogeneous identity types</a>:</p> <ul> <li> <p>Judgmental uniqueness of identity proofs for dependent heterogeneous identity types:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mtable displaystyle="false" rowspacing="0.5ex" columnalign="left"><mtr><mtd><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></mtd></mtr> <mtr><mtd><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>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>y</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>z</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <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></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>r</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <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></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr></mtable><mrow><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>≡</mo><mi>r</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <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></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B(a) \quad \Gamma \vdash z:B(b) \\ \Gamma \vdash q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \quad \Gamma \vdash r:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \end{array} }{\Gamma \vdash q \equiv r:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)} </annotation></semantics></math></div></li> <li> <p>Propositional uniqueness of identity proofs for dependent heterogeneous identity types:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mtable displaystyle="false" rowspacing="0.5ex" columnalign="left"><mtr><mtd><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></mtd></mtr> <mtr><mtd><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>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>y</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>z</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <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></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>r</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <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></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr></mtable><mrow><mi>Γ</mi><mo>⊢</mo><mi>q</mi><msub><mo>=</mo> <mrow><msub><mi mathvariant="normal">hId</mi> <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></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow></msub><mi>r</mi><mspace width="thickmathspace"></mspace><mi mathvariant="normal">true</mi></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B(a) \quad \Gamma \vdash z:B(b) \\ \Gamma \vdash q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \quad \Gamma \vdash r:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \end{array} }{\Gamma \vdash q =_{\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)} r \; \mathrm{true}} </annotation></semantics></math></div></li> <li> <p>Typal uniqueness of identity proofs for dependent heterogeneous identity types:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mfrac><mtable displaystyle="false" rowspacing="0.5ex" columnalign="left"><mtr><mtd><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></mtd></mtr> <mtr><mtd><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>A</mi><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>p</mi><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mi>A</mi></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>y</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>z</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>b</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>Γ</mi><mo>⊢</mo><mi>q</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <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></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mspace width="1em"></mspace><mi>Γ</mi><mo>⊢</mo><mi>r</mi><mo>:</mo><msub><mi mathvariant="normal">hId</mi> <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></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mtd></mtr></mtable><mrow><mi>Γ</mi><mo>⊢</mo><msub><mi mathvariant="normal">UIP</mi> <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></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo>,</mo><mi>q</mi><mo>,</mo><mi>r</mi><mo stretchy="false">)</mo><mo>:</mo><msub><mi mathvariant="normal">Id</mi> <mrow><msub><mi mathvariant="normal">hId</mi> <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></msub><mo stretchy="false">(</mo><mi>a</mi><mo>,</mo><mi>b</mi><mo>,</mo><mi>p</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>q</mi><mo>,</mo><mi>r</mi><mo stretchy="false">)</mo></mrow></mfrac></mrow><annotation encoding="application/x-tex">\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B(a) \quad \Gamma \vdash z:B(b) \\ \Gamma \vdash q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \quad \Gamma \vdash r:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \end{array} }{\Gamma \vdash \mathrm{UIP}_{x:A.B(x)}(a, b, p, y, z, q, r):\mathrm{Id}_{\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)}(q, r)} </annotation></semantics></math></div></li> </ul> <h2 id="properties">Properties</h2> <h3 id="uniqueness_of_identity_proofs_and_univalence">Uniqueness of identity proofs and univalence</h3> <p>In this section we assume that the universe is a Tarski universe. Uniqueness of identity proofs is inconsistent with having a <a class="existingWikiWord" href="/nlab/show/univalent+type+with+a+type+family">univalent type with a type family</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></mrow><annotation encoding="application/x-tex">(A, B)</annotation></semantics></math> with at least one term <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a:A</annotation></semantics></math> where the 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>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">B(a)</annotation></semantics></math> is provably not a proposition</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>p</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mi>q</mi><mo>:</mo><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></munder><msub><mi mathvariant="normal">Id</mi> <mrow><mi>B</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mi>p</mi><mo>,</mo><mi>q</mi><mo stretchy="false">)</mo><mo>)</mo></mrow><mo>→</mo><mi>∅</mi></mrow><annotation encoding="application/x-tex">\left(\prod_{p:B(a)} \prod_{q:B(a)} \mathrm{Id}_{B(a)}(p, q)\right) \to \emptyset</annotation></semantics></math></div> <p>because by univalence, <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> is then provably not a set, which contradicts uniqueness of identity proofs. In particular, having a <a class="existingWikiWord" href="/nlab/show/univalent+universe">univalent 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> in the type theory is inconsistent with uniqueness of identity proofs.</p> <p>The familial uniqueness of identity proofs axiom applied to Tarski universes implies that 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 type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(A)</annotation></semantics></math> is a set. This means the type reflection of the internal equivalences <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><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">T(A \simeq_U B)</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>, and the <a class="existingWikiWord" href="/nlab/show/univalence+axiom">univalence axiom</a> then implies that <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> is an <a class="existingWikiWord" href="/nlab/show/h-groupoid">h-groupoid</a>. If <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> has <a class="existingWikiWord" href="/nlab/show/h-sets">h-sets</a> which can be proven not to be an <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>, such as the <a class="existingWikiWord" href="/nlab/show/booleans+type">booleans type</a>, then <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> is provably not an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>.</p> <p>However, unlike the case for uniqueness of identity proofs, the familial uniqueness of identity proofs and the univalence axiom for universes are inconsistent with each other only if the Tarski universe <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> has objects which can be proven not to be an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a>, such as internal univalent Tarski universes <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi><mo>:</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">V:U</annotation></semantics></math> where the type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>V</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(V)</annotation></semantics></math> has terms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo>:</mo><mi>T</mi><mo stretchy="false">(</mo><mi>V</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">A:T(V)</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>T</mi> <mi>V</mi></msub><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T_V(A)</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a> which is not an <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>, such as the <a class="existingWikiWord" href="/nlab/show/booleans+type">booleans type</a>. As a result, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>V</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(V)</annotation></semantics></math> can be proven to not be a set, causing uniqueness of identity proofs for <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> to be inconsistent with the existence of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi><mo>:</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">V:U</annotation></semantics></math> and univalence.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+set+truncation">axiom of set truncation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+K">axiom K</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/boundary+separation">boundary separation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/axiom+of+circle+type+localization">axiom of circle type localization</a></p> </li> </ul> <h2 id="references">References</h2> <ul> <li>“<a href="http://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/pdfs/agroupoidinterpretationoftypetheroy.pdf">The groupoid interpretation of type theory</a>” [PDF], by Martin Hofmann and Thomas Streicher, 1996.</li> </ul> <p>Discussion in <a class="existingWikiWord" href="/nlab/show/Coq">Coq</a> is in</p> <ul> <li>Pierre Corbineau, <em>The K axiom in Coq (almost) for free</em> (<a href="http://coq.inria.fr/files/adt-2fev10-corbineau.pdf">pdf</a>)</li> </ul> <p>For definitional UIP in <a class="existingWikiWord" href="/nlab/show/XTT">XTT</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Jonathan+Sterling">Jonathan Sterling</a>, <a class="existingWikiWord" href="/nlab/show/Carlo+Angiuli">Carlo Angiuli</a>, <a class="existingWikiWord" href="/nlab/show/Daniel+Gratzer">Daniel Gratzer</a>, <em>Cubical syntax for reflection-free extensional equality</em>. In Herman Geuvers, editor, <em>4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)</em>, volume 131 of <em>Leibniz International Proceedings in Informatics (LIPIcs)</em>, pages 31:1-31:25. (<a href="https://arxiv.org/abs/1904.08562">arXiv:1904.08562</a>, <a href="https://doi.org/10.4230/LIPIcs.FCSD.2019.31">doi:10.4230/LIPIcs.FCSD.2019.31</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Jonathan+Sterling">Jonathan Sterling</a>, <a class="existingWikiWord" href="/nlab/show/Carlo+Angiuli">Carlo Angiuli</a>, <a class="existingWikiWord" href="/nlab/show/Daniel+Gratzer">Daniel Gratzer</a>, <em>A Cubical Language for Bishop Sets</em>, Logical Methods in Computer Science, 18 (1), 2022. (<a href="https://arxiv.org/abs/2003.01491">arXiv:2003.01491</a>).</p> </li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on February 24, 2024 at 11:57:28. See the <a href="/nlab/history/uniqueness+of+identity+proofs" 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/uniqueness+of+identity+proofs" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/4570/#Item_20">Discuss</a><span class="backintime"><a href="/nlab/revision/uniqueness+of+identity+proofs/15" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/uniqueness+of+identity+proofs" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/uniqueness+of+identity+proofs" accesskey="S" class="navlink" id="history" rel="nofollow">History (15 revisions)</a> <a href="/nlab/show/uniqueness+of+identity+proofs/cite" style="color: black">Cite</a> <a href="/nlab/print/uniqueness+of+identity+proofs" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/uniqueness+of+identity+proofs" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>