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> propositions as types 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> propositions as types </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/203/#Item_19" 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="constructivism_realizability_computability">Constructivism, Realizability, Computability</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/realizability">realizability</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/computability">computability</a></strong></p> <p><a class="existingWikiWord" href="/nlab/show/intuitionistic+mathematics">intuitionistic mathematics</a></p> <p><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>, <a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>, <a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></p> <h3 id="constructive_mathematics">Constructive mathematics</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">topos</a>, <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-topos">homotopy topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/canonical+form">canonical form</a>, <a class="existingWikiWord" href="/nlab/show/univalence">univalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>, <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/decidable+equality">decidable equality</a>, <a class="existingWikiWord" href="/nlab/show/decidable+subset">decidable subset</a>, <a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited set</a>, <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></p> </li> </ul> <h3 id="realizability">Realizability</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+topos">realizability topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+model">realizability model</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+interpretation">realizability interpretation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/effective+topos">effective topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kleene%27s+first+algebra">Kleene's first algebra</a>, <a class="existingWikiWord" href="/nlab/show/Kleene%27s+second+algebra">Kleene's second algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/function+realizability">function realizability</a></p> </li> </ul> <h3 id="computability">Computability</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/computability">computability</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computation">computation</a>, <a class="existingWikiWord" href="/nlab/show/computational+type+theory">computational type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+function">computable function</a>, <a class="existingWikiWord" href="/nlab/show/partial+recursive+function">partial recursive function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+analysis">computable analysis</a>, <a class="existingWikiWord" href="/nlab/show/constructive+analysis">constructive analysis</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Type+Two+Theory+of+Effectivity">Type Two Theory of Effectivity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+function+%28analysis%29">computable function (analysis)</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/exact+real+computer+arithmetic">exact real computer arithmetic</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+set">computable set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/persistent+homology">persistent homology</a>, <a class="existingWikiWord" href="/nlab/show/effective+homology">effective homology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+physics">computable physics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Church-Turing+thesis">Church-Turing thesis</a></p> </li> </ul> </div></div> <h4 id="category_theory"><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mn>0</mn><mo>,</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(0,1)</annotation></semantics></math>-Category theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category+theory">(0,1)-category theory</a></strong>: <a class="existingWikiWord" href="/nlab/show/logic">logic</a>, <a class="existingWikiWord" href="/nlab/show/order+theory">order theory</a></p> <p><strong><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-category">(0,1)-category</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+preorders+and+%280%2C1%29-categories">relation between preorders and (0,1)-categories</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proset">proset</a>, <a class="existingWikiWord" href="/nlab/show/partially+ordered+set">partially ordered set</a> (<a class="existingWikiWord" href="/nlab/show/directed+set">directed set</a>, <a class="existingWikiWord" href="/nlab/show/total+order">total order</a>, <a class="existingWikiWord" href="/nlab/show/linear+order">linear order</a>)</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/top">top</a>, <a class="existingWikiWord" href="/nlab/show/true">true</a>,</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/bottom">bottom</a>, <a class="existingWikiWord" href="/nlab/show/false">false</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/monotone+function">monotone function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/implication">implication</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/filter">filter</a>, <a class="existingWikiWord" href="/nlab/show/interval">interval</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/lattice">lattice</a>, <a class="existingWikiWord" href="/nlab/show/semilattice">semilattice</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/meet">meet</a>, <a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a>, <a class="existingWikiWord" href="/nlab/show/and">and</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/join">join</a>, <a class="existingWikiWord" href="/nlab/show/logical+disjunction">logical disjunction</a>, <a class="existingWikiWord" href="/nlab/show/or">or</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/compact+element">compact element</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/lattice+of+subobjects">lattice of subobjects</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/complete+lattice">complete lattice</a>, <a class="existingWikiWord" href="/nlab/show/algebraic+lattice">algebraic lattice</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/distributive+lattice">distributive lattice</a>, <a class="existingWikiWord" href="/nlab/show/completely+distributive+lattice">completely distributive lattice</a>, <a class="existingWikiWord" href="/nlab/show/canonical+extension">canonical extension</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hyperdoctrine">hyperdoctrine</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/first-order+hyperdoctrine">first-order</a>, <a class="existingWikiWord" href="/nlab/show/Boolean+hyperdoctrine">Boolean</a>, <a class="existingWikiWord" href="/nlab/show/coherent+hyperdoctrine">coherent</a>, <a class="existingWikiWord" href="/nlab/show/tripos">tripos</a></li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/%280%2C1%29-topos">(0,1)-topos</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Heyting+algebra">Heyting algebra</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/regular+element">regular element</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Boolean+algebra">Boolean algebra</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/frame">frame</a>, <a class="existingWikiWord" href="/nlab/show/locale">locale</a></p> </li> </ul> <h2 id="theorems">Theorems</h2> <ul> <li><a class="existingWikiWord" href="/nlab/show/Stone+duality">Stone duality</a></li> </ul> </div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#idea'>Idea</a></li> <ul> <li><a href='#general_idea'>General idea</a></li> <li><a href='#PropositionsAsSomeTypes'>Propositions as some types</a></li> <li><a href='#in_homotopy_type_theory'>In homotopy type theory</a></li> <li><a href='#propositions_as_sets_in_set_theory'>Propositions as sets in set theory</a></li> </ul> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> <ul> <li><a href='#general'>General</a></li> <li><a href='#ReferencesHistory'>History</a></li> </ul> </ul> </div> <h2 id="idea">Idea</h2> <h3 id="general_idea">General idea</h3> <p>In <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, the paradigm of <strong>propositions as types</strong> says that <a class="existingWikiWord" href="/nlab/show/propositions">propositions</a> and <a class="existingWikiWord" href="/nlab/show/types">types</a> are essentially the same. A proposition is identified with the type (collection) of all its <a class="existingWikiWord" href="/nlab/show/proofs">proofs</a>, and a type is identified with the proposition that it has a <a class="existingWikiWord" href="/nlab/show/term">term</a> (so that each of its terms is in turn a proof of the corresponding proposition).</p> <blockquote> <p>… to show that a proposition is true in type theory corresponds to exhibiting an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo></mrow><annotation encoding="application/x-tex">[</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/term">term</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">]</annotation></semantics></math> of the type corresponding to that proposition. We regard the elements of this type as <em>evidence</em> or <em>witnesses</em> that the proposition is true. (They are sometimes even called <em>proofs</em>… (from <a class="existingWikiWord" href="/nlab/show/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics">Homotopy Type Theory – Univalent Foundations of Mathematics</a>, section 1.11)</p> </blockquote> <p>Not all type theories follow this paradigm; among those that do, <a class="existingWikiWord" href="/nlab/show/Martin-L%C3%B6f+type+theories">Martin-Löf type theories</a> are the most famous. In its variant as <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> the paradigm is also central, but receives some refinements, see at <a class="existingWikiWord" href="/nlab/show/propositions+as+some+types">propositions as some types</a>.</p> <p>Even when the paradigm is not adopted, however, there is still a close relationship between logical and type-theoretic operations, called the <strong>Curry–Howard isomorphism</strong> or (if it is not clear in which category this <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphism</a> is supposed to exist) the <strong>Curry–Howard correspondence</strong>. Or maybe better (<a href="#Harper">Harper</a>) the <strong><a class="existingWikiWord" href="/nlab/show/Brouwer-Heyting-Kolmogorov+interpretation">Brouwer-Heyting-Kolmogorov interpretation</a></strong>. This correspondence is most precise and well-developed for <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a>, but could also be developed for <a class="existingWikiWord" href="/nlab/show/classical+logic">classical logic</a>.</p> <p>Accordingly, <a class="existingWikiWord" href="/nlab/show/logic">logical</a> operations on propositions have immediate analogs on <a class="existingWikiWord" href="/nlab/show/types">types</a>. For instance logical <em><a class="existingWikiWord" href="/nlab/show/and">and</a></em> corresponds to forming 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>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A \times B</annotation></semantics></math> (a <a class="existingWikiWord" href="/nlab/show/proof">proof</a> 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> and a proof of <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>), the <a class="existingWikiWord" href="/nlab/show/universal+quantifier">universal quantifier</a> corresponds to <a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a>, the <a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a> to <a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a>. In <a class="existingWikiWord" href="/nlab/show/classical+mathematics">classical mathematics</a>, the <a class="existingWikiWord" href="/nlab/show/law+of+double+negation">law of double negation</a> corresponds to a <a class="existingWikiWord" href="/nlab/show/global+choice+operator">global choice operator</a>.</p> <p>Furthermore, most structures traditionally involving <a class="existingWikiWord" href="/nlab/show/predicates">predicates</a> or <a class="existingWikiWord" href="/nlab/show/relations">relations</a> are defined as type-valued type families. For instance, <a class="existingWikiWord" href="/nlab/show/setoids">setoids</a> or <a class="existingWikiWord" href="/nlab/show/Bishop+sets">Bishop sets</a> are usually defined to have a <a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relation">pseudo-equivalence relation</a> in the propositions as types paradigm, rather than a <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a> as typical in the <a class="existingWikiWord" href="/nlab/show/propositions+as+some+types">propositions as some types</a> paradigm. However, in classical mathematics, the <a class="existingWikiWord" href="/nlab/show/global+choice+operator">global choice operator</a> representing the <a class="existingWikiWord" href="/nlab/show/law+of+double+negation">law of double negation</a> in propositions as types implies that the <a class="existingWikiWord" href="/nlab/show/boolean+domain">boolean domain</a> is the <a class="existingWikiWord" href="/nlab/show/type+of+all+propositions">type of all propositions</a>, so predicates or relations can simply be defined as functions into the boolean domain.</p> <h3 id="PropositionsAsSomeTypes">Propositions as some types</h3> <p>A related paradigm may be called <strong><a class="existingWikiWord" href="/nlab/show/propositions+as+some+types">propositions as some types</a></strong>, in which propositions are identified with particular types, but not all types are regarded as propositions. Generally, the propositions are the “types with at most one <a class="existingWikiWord" href="/nlab/show/term">term</a>”. This is the paradigm usually used in the <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> of <a class="existingWikiWord" href="/nlab/show/categories">categories</a> such as <a class="existingWikiWord" href="/nlab/show/toposes">toposes</a>, as well as in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>. In this case, the type-theoretic operations on types either restrict to the propositions to give logical operations (for <a class="existingWikiWord" href="/nlab/show/conjunction">conjunction</a>, <a class="existingWikiWord" href="/nlab/show/implication">implication</a>, and the <a class="existingWikiWord" href="/nlab/show/universal+quantifier">universal quantifier</a>), or have to be “reflected” therein (for <a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a> and the <a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a>). The reflector operation is called a <a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a>.</p> <h3 id="in_homotopy_type_theory">In homotopy type theory</h3> <p>We consider aspects of the interpretation of <em>propositions as types</em> in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, see (<a href="#HoTTBook">HoTT book, section 1.11</a>).</p> <p>In <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> where types may be thought of as <a class="existingWikiWord" href="/nlab/show/homotopy+types">homotopy types</a> (<a class="existingWikiWord" href="/nlab/show/%E2%88%9E-groupoids">∞-groupoids</a>) (or rather <a class="existingWikiWord" href="/nlab/show/geometric+homotopy+types">geometric homotopy types</a> (<a class="existingWikiWord" href="/nlab/show/%E2%88%9E-stacks">∞-stacks</a>,<a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-sheaves">(∞,1)-sheaves</a>), more generally), we may think for <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> any type of</p> <ul> <li> <p>the <a class="existingWikiWord" href="/nlab/show/objects">objects</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> are <a class="existingWikiWord" href="/nlab/show/proofs">proofs</a> of some proposition;</p> </li> <li> <p>the <a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a> 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> are equivalences between these proofs;</p> </li> <li> <p>the <a class="existingWikiWord" href="/nlab/show/2-morphisms">2-morphisms</a> 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> are equivalences between these equivalences, and so on.</p> </li> </ul> <p>So in terms of the notion of <a class="existingWikiWord" href="/nlab/show/n-connected+object+of+an+%28infinity%2C1%29-topos">n-connected</a> and <a class="existingWikiWord" href="/nlab/show/truncated">n-truncated objects in an (∞,1)-category</a> we have</p> <ul> <li> <p>if <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 <a class="existingWikiWord" href="/nlab/show/%28-1%29-connected">(-1)-connected</a> then the corresponding proposition is <a class="existingWikiWord" href="/nlab/show/true">true</a>;</p> </li> <li> <p>if <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 <a class="existingWikiWord" href="/nlab/show/%28-2%29-truncated">(-2)-truncated</a> (a <a class="existingWikiWord" href="/nlab/show/%28-2%29-groupoid">(-2)-groupoid</a>) then the corresponding proposition is true by a unique proof which is uniquely equivalent to itself, etc.;</p> </li> <li> <p>if <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 <a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated">(-1)-truncated</a> (a <a class="existingWikiWord" href="/nlab/show/%28-1%29-groupoid">(-1)-groupoid</a>) then the corresponding proposition may be true or <a class="existingWikiWord" href="/nlab/show/false">false</a>, but if it is true it is to by a unique proof as above;</p> </li> <li> <p>if <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 <a class="existingWikiWord" href="/nlab/show/0-truncated">0-truncated</a> then there may be more than one proof, but none equivalent to itself in an interesting way;</p> </li> <li> <p>if <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 <a class="existingWikiWord" href="/nlab/show/1-truncated">1-truncated</a> then there may be proofs of the corresponding proposition that are equivalent to themselves in interesting ways.</p> </li> </ul> <p>We would not say homotopy type theory has propositions as types in the same way that Martin–Löf type theory has; only the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mn>1</mn><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(-1)</annotation></semantics></math>-truncated types are propositions as such. That is, in HoTT we have propositions as <em>some</em> types. In this case the <a class="existingWikiWord" href="/nlab/show/bracket+types">bracket types</a> can be identified with a particular <a class="existingWikiWord" href="/nlab/show/higher+inductive+type">higher inductive type</a> called <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>isInhab</mi></mrow><annotation encoding="application/x-tex">isInhab</annotation></semantics></math>.</p> <h3 id="propositions_as_sets_in_set_theory">Propositions as sets in set theory</h3> <p>There is an analogue of the “propositions as types” in <a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a>, called <strong>propositions as sets</strong>. Instead of working in the external logic, one interprets certain set-theoretic operations as representing the predicate logic:</p> <ul> <li> <p>Any <a class="existingWikiWord" href="/nlab/show/set">set</a> represents a proposition</p> </li> <li> <p>The <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a> represents <a class="existingWikiWord" href="/nlab/show/falsehood">falsehood</a></p> </li> <li> <p>Any <a class="existingWikiWord" href="/nlab/show/singleton">singleton</a> represents <a class="existingWikiWord" href="/nlab/show/truth">truth</a></p> </li> <li> <p>The binary cartesian product of two sets is <a class="existingWikiWord" href="/nlab/show/conjunction">conjunction</a> of propositions</p> </li> <li> <p>The function set between two sets is <a class="existingWikiWord" href="/nlab/show/implication">implication</a> of propositions</p> </li> <li> <p>The function set from a set to the empty set is <a class="existingWikiWord" href="/nlab/show/negation">negation</a> of propositions</p> </li> <li> <p>Given a family of sets, the indexed <a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a> of the family of sets is <a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a></p> </li> <li> <p>The binary <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> of two sets is the <a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a> of propositions</p> </li> <li> <p>The indexed <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> of a family of sets is the <a class="existingWikiWord" href="/nlab/show/existential+quantifier">existential quantifier</a></p> </li> <li> <p>Equality is given by the <a class="existingWikiWord" href="/nlab/show/diagonal+subset">diagonal subset</a></p> </li> </ul> <p>Compare with <a class="existingWikiWord" href="/nlab/show/propositions+as+subsingletons">propositions as subsingletons</a>, which is the usual interpretation of the <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> of a set theory via set-theoretic operations on sets.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/proof+relevance">proof relevance</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/theory">theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>/<a class="existingWikiWord" href="/nlab/show/type">type</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>, <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/propositions+as+projections">propositions as projections</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/propositions+as+some+types">propositions as some types</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/propositional+logic+as+a+dependent+type+theory">propositional logic as a dependent type theory</a></p> </li> </ul> <h2 id="references">References</h2> <h3 id="general">General</h3> <p>Early account for <a class="existingWikiWord" href="/nlab/show/intuitionistic+type+theory">intuitionistic type theory</a>:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Per+Martin-L%C3%B6f">Per Martin-Löf</a> (notes by <a class="existingWikiWord" href="/nlab/show/Giovanni+Sambin">Giovanni Sambin</a>), <em>Intuitionistic type theory</em>, noted of a Lecture in Padua 1984, Bibliopolis (1984) [<a href="https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/MartinLofIntuitionisticTypeTheory.pdf" title="pdf">pdf</a>]</p> </li> <li id="Girard89"> <p><a class="existingWikiWord" href="/nlab/show/Jean-Yves+Girard">Jean-Yves Girard</a> (translated and with appendiced by <a class="existingWikiWord" href="/nlab/show/Paul+Taylor">Paul Taylor</a> and <a class="existingWikiWord" href="/nlab/show/Yves+Lafont">Yves Lafont</a>), Chapter 3 of: <em>Proofs and Types</em>, Cambridge University Press (1989) [<a href="">ISBN:978-0-521-37181-0</a>, <a href="http://www.paultaylor.eu/stable/Proofs+Types.html">webpage</a>, <a href="https://www.paultaylor.eu/stable/prot.pdf">pdf</a>]</p> </li> </ul> <p>With a notion of <a class="existingWikiWord" href="/nlab/show/propositional+truncation">propositional truncation</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Steve+Awodey">Steve Awodey</a>, <a class="existingWikiWord" href="/nlab/show/Andrej+Bauer">Andrej Bauer</a>, <em>Propositions as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo></mrow><annotation encoding="application/x-tex">[</annotation></semantics></math>Types<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">]</annotation></semantics></math></em>, Journal of Logic and Computation, <strong>14</strong> (2004) 447-471 [<a href="https://doi.org/10.1093/logcom/14.4.447">doi:10.1093/logcom/14.4.447</a>, <a href="http://andrej.com/papers/brackets_letter.pdf">pdf</a>]</li> </ul> <p>Textbook accounts:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Simon+Thompson">Simon Thompson</a>, <em><a class="existingWikiWord" href="/nlab/show/Type+Theory+and+Functional+Programming">Type Theory and Functional Programming</a></em>, Addison-Wesley (1991) [ISBN:0-201-41667-0, <a href="http://www.cs.kent.ac.uk/people/staff/sjt/TTFP">webpage</a>, <a href="http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf">pdf</a>, <a href="https://www.elsevier.com/books/lectures-on-the-curry-howard-isomorphism/sorensen/978-0-444-52077-7">ISBN:9780444520777</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Bart+Jacobs">Bart Jacobs</a>, Section 10.2 of <em>Categorical Logic and Type Theory</em>, Studies in Logic and the Foundations of Mathematics <strong>141</strong>, Elsevier (1998) [<a href="https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/141">ISBN:978-0-444-50170-7</a>, <a href="https://people.mpi-sws.org/~dreyer/courses/catlogic/jacobs.pdf">pdf</a>]</p> </li> <li> <p>Morten Heine Sørensen, Pawel Urzyczyn, <em>Lectures on the Curry-Howard isomorphism</em>, Studies in Logic <strong>149</strong>, Elsevier (2006) [<a href="https://www.elsevier.com/books/lectures-on-the-curry-howard-isomorphism/sorensen/978-0-444-52077-7">ISBN:9780444520777</a>, <a href="https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf">pdf</a>]</p> </li> </ul> <p>Exposition:</p> <ul> <li id="Harper"> <p><a class="existingWikiWord" href="/nlab/show/Robert+Harper">Robert Harper</a>, <em>Extensionality, Intensionality, and Brouwer’s Dictum</em> (2012) [<a href="http://existentialtype.wordpress.com/2012/08/11/extensionality-intensionality-and-brouwers-dictum/">blog</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Philip+Wadler">Philip Wadler</a>, <em>Propositions as Types</em>, Communications of the ACM <strong>58</strong> 12 (2015) 75–84 [<a href="https://doi.org/10.1145/2699407">doi:10.1145/2699407</a>, <a href="https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf">pdf</a>, <a href="https://www.youtube.com/watch?v=IOiZatlZtGU">video</a>]</p> </li> </ul> <p>See also:</p> <ul> <li>Wikipedia, <em><a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard correspondence</a></em></li> </ul> <p>Discussion in view of <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>:</p> <ul> <li id="HoTTBook"><a class="existingWikiWord" href="/nlab/show/Univalent+Foundations+Project">Univalent Foundations Project</a>, Section 1.11 in: <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>, <a class="existingWikiWord" href="/nlab/show/Planet+Math">PM</a> <a href="http://planetmath.org/node/87534">wiki version</a>]</li> </ul> <h3 id="ReferencesHistory">History</h3> <p>An influential original article was</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/William+Howard">William Howard</a>, <em>The formulae-as-types notion of construction</em>. In J. Roger Seldin, Jonathan P.; Hindley, (ed.s), <em>To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism</em>, pages 479–490. Academic Press, 1980. original paper manuscript from 1969. (Cited <p>on pages 53, 54, 100, and 430.) (<a href="http://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf">pdf</a>)</p> </li> </ul> <p>The origins of this manuscript and its publication are recounted in a 2014 email from Howard to Philip Wadler:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/William+Howard">William Howard</a>, <a href="http://wadler.blogspot.fr/2014/08/howard-on-curry-howard.html">email</a>.</li> </ul> <p>This influential note brought <a class="existingWikiWord" href="/nlab/show/Dana+Scott">Dana Scott</a> to write “Constructive Validity” (a precursor of type theory) and also strongly influenced <a class="existingWikiWord" href="/nlab/show/Per+Martin-L%C3%B6f">Per Martin-Löf</a>. Independently and at about the same time, the idea was also found by <a class="existingWikiWord" href="/nlab/show/N.G.+de+Bruijn">N.G. de Bruijn</a> for the <a class="existingWikiWord" href="/nlab/show/Automath">Automath</a> system.</p> <p><a class="existingWikiWord" href="/nlab/show/Dana+Scott">Dana Scott</a>, <a class="existingWikiWord" href="/nlab/show/William+Howard">William Howard</a>, <a class="existingWikiWord" href="/nlab/show/Per+Martin-L%C3%B6f">Per Martin-Löf</a>, and <a class="existingWikiWord" href="/nlab/show/William+Tait">William Tait</a> were all involved in the late 60s and early 70s, mainly in Chicago.</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/William+Tait">William Tait</a>, <em>The completeness of intuitionistic first-order logic</em>. Unpublished manuscript.</li> </ul> <p>Also <a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a> was there, lecturing on <a class="existingWikiWord" href="/nlab/show/hyperdoctrines">hyperdoctrines</a>. Lawvere told <a class="existingWikiWord" href="/nlab/show/Steve+Awodey">Steve Awodey</a> that the basic example of a morphism of hyperdoctrines from the proof-relevant one to the proof-irrelevant one was influenced by Kreisel, not Howard, who attended Lawvere’s Chicago lectures in the 60s. See pages 2 and 3 of</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/William+Lawvere">William Lawvere</a> interviewed by Felice Cardone, <em>The role of Cartesian closed categories in foundations</em>, March 2000 (<a href="https://dl.dropboxusercontent.com/u/92056191/Archive/temporary_new_material/lawvere-cardone-2000/lawvere-cardone-2000.pdf">link</a>)</li> </ul> <p>But the story started earlier with what has been called the <a class="existingWikiWord" href="/nlab/show/BHK+interpretation">BHK interpretation</a> of <a class="existingWikiWord" href="/nlab/show/intuitionistic+logic">intuitionistic logic</a>, highlighted for instance in (<a href="#Troelstra91">Troelstra 91</a>), which identifies a proposition with the collection of its proofs. This view goes back to an observation of Kolmogorov that the formalisation of Brouwer’s ideas by Heyting in 1930 can be semantically interpreted as a calculus of ‘Aufgaben’ - problems (and solutions), reported in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Andrey+Kolmogorov">Andrey Kolmogorov</a>, <em>Zur Deutung der intuitionistischen Logik</em>, Math. Z. <strong>35</strong> (1932) pp.58-65. (<a href="http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=GDZPPN002373467">gdz</a>)</li> </ul> <p>A historical account is in the section on types in</p> <ul> <li>Hindley J. Roger; Cardone Felice, <em>History of Lambda-calculus and Combinatory Logic</em>. Handbook of the History of Logic. Volume 5. Logic from Russell to Church (edited by D. Gabbay and J. Woods), Elsevier, 2009, pp. 723-817 (<a href="http://www.di.unito.it/~felice/pdf/lambdacomb.pdf">pdf</a>, <a href="http://www.di.unito.it/~felice/pdf/erratalist.pdf">errata</a>)</li> </ul> <p>and in section 5 of</p> <ul> <li id="Troelstra91"><a class="existingWikiWord" href="/nlab/show/Anne+Sjerp+Troelstra">Anne Sjerp Troelstra</a>, <em>History of Constructivism in the 20th Century</em>, 1991 (<a href="https://www.illc.uva.nl/Research/Publications/Reports/ML-1991-05.text.pdf">preprint</a>)</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on February 12, 2025 at 21:36:14. See the <a href="/nlab/history/propositions+as+types" 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/propositions+as+types" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/203/#Item_19">Discuss</a><span class="backintime"><a href="/nlab/revision/propositions+as+types/49" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/propositions+as+types" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/propositions+as+types" accesskey="S" class="navlink" id="history" rel="nofollow">History (49 revisions)</a> <a href="/nlab/show/propositions+as+types/cite" style="color: black">Cite</a> <a href="/nlab/print/propositions+as+types" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/propositions+as+types" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>