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> tripos 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> tripos </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/4057/#Item_7" 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="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> <li><a href='#definition'>Definition</a></li> <li><a href='#examples'>Examples</a></li> <ul> <li><a href='#Topos'>Coming from toposes</a></li> <li><a href='#Heyt'>Coming from complete Heyting algebras</a></li> <li><a href='#PCA'>Coming from partial combinatory algebras</a></li> </ul> <li><a href='#from_triposes_to_toposes'>From triposes to toposes</a></li> <ul> <li><a href='#weak_triposes'>Weak triposes</a></li> <li><a href='#a_synthetic_view_of_triposes'>A “synthetic” view of triposes</a></li> </ul> <li><a href='#relation_to_valued_sets'>Relation to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>-valued sets</a></li> <ul> <li><a href='#theorem_higgs'>Theorem (Higgs)</a></li> </ul> <li><a href='#relation_to_exact_completion'>Relation to exact completion</a></li> <li><a href='#internal_logic'>Internal logic</a></li> <li><a href='#references'>References</a></li> </ul> </div> <h2 id="idea">Idea</h2> <p>A <strong>tripos</strong> is a <a class="existingWikiWord" href="/nlab/show/first-order+hyperdoctrine">first-order hyperdoctrine with equality</a> satisfying an additional property that allows it to interpret <a class="existingWikiWord" href="/nlab/show/impredicative+logic">impredicative</a> <a class="existingWikiWord" href="/nlab/show/higher-order+logic">higher-order logic</a> as well. In particular, every tripos gives rise to a corresponding <a class="existingWikiWord" href="/nlab/show/topos">topos</a>.</p> <p>The notion of tripos, due to <a class="existingWikiWord" href="/nlab/show/Andrew+Pitts">Andrew Pitts</a>, is useful for giving a unified account of two very different classes of toposes: <a class="existingWikiWord" href="/nlab/show/localic+topos">localic toposes</a> and <a class="existingWikiWord" href="/nlab/show/realizability+topos">realizability toposes</a>.</p> <p>The name ‘tripos’ is to be credited to <a class="existingWikiWord" href="/nlab/show/Peter+Johnstone">Peter Johnstone</a>, who was the thesis advisor of Pitts. It can be read as an acronym for “Topos Representing Indexed Partially Ordered Set”, but it is memorable also as a pun, referring to a famous examination at Cambridge University where Pitts, Johnstone, and <a class="existingWikiWord" href="/nlab/show/Martin+Hyland">Hyland</a> work.</p> <h2 id="definition">Definition</h2> <p>Recall that the data of a first-order hyperdoctrine <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> consists of a <a class="existingWikiWord" href="/nlab/show/syntactic+category">category of terms</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math>, assumed to have <a class="existingWikiWord" href="/nlab/show/finite+products">finite products</a>, and a <a class="existingWikiWord" href="/nlab/show/functor">functor</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo>:</mo><msubsup><mi>C</mi> <mi>T</mi> <mi>op</mi></msubsup><mo>→</mo><mi>HeytAlg</mi></mrow><annotation encoding="application/x-tex">Pred_T: C_{T}^{op} \to HeytAlg</annotation></semantics></math></div> <p>to the category of <a class="existingWikiWord" href="/nlab/show/Heyting+algebras">Heyting algebras</a>, satisfying suitable properties (including <a class="existingWikiWord" href="/nlab/show/quantifiers">quantifiers</a>, i.e., left and right adjoints to “pullback maps” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Pred_T(f)</annotation></semantics></math>)<sup id="fnref:1"><a href="#fn:1" rel="footnote">1</a></sup>. We often abbreviate <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Pred_T(f)</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup></mrow><annotation encoding="application/x-tex">f^\ast</annotation></semantics></math>, calling it a <em>pullback map</em>. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> is a Heyting algebra, we let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mo stretchy="false">|</mo><mi>H</mi><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">{|H|}</annotation></semantics></math> denote the underlying set.</p> <div class="num_defn"> <h6 id="definition_2">Definition</h6> <p>A <strong>tripos</strong> is a first-order hyperdoctrine <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> together with, for every object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math>, an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>c</mi></mrow><annotation encoding="application/x-tex">P c</annotation></semantics></math> and an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>in</mi> <mi>c</mi></msub><mo>∈</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>c</mi><mo>×</mo><mi>P</mi><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">in_c \in Pred_T(c \times P c)</annotation></semantics></math> such that for any object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math> and element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>∈</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>c</mi><mo>×</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p \in Pred_T(c \times b)</annotation></semantics></math>, there exists a map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>χ</mi><mo lspace="verythinmathspace">:</mo><mi>b</mi><mo>→</mo><mi>P</mi><mi>c</mi></mrow><annotation encoding="application/x-tex">\chi \colon b \to P c</annotation></semantics></math> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><msub><mn>1</mn> <mi>c</mi></msub><mo>×</mo><mi>χ</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><msub><mi>in</mi> <mi>c</mi></msub><mo stretchy="false">)</mo><mo>=</mo><mi>p</mi></mrow><annotation encoding="application/x-tex">Pred_T(1_c \times \chi)(in_c) = p</annotation></semantics></math>. (N.B.: such <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>χ</mi></mrow><annotation encoding="application/x-tex">\chi</annotation></semantics></math> need not be unique.)</p> </div> <p>Another way of phrasing the definition is that to each object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> there is an assigned object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(c)</annotation></semantics></math> and an assigned <em><a class="existingWikiWord" href="/nlab/show/epimorphism">epimorphism</a></em></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>P</mi><mi>c</mi><mo stretchy="false">)</mo><mo>→</mo><mrow><mo stretchy="false">|</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">|</mo></mrow><mo stretchy="false">(</mo><mi>c</mi><mo>×</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\hom(-, P c) \to {|Pred_T|}(c \times -)</annotation></semantics></math></div> <p>of set-valued functors; the <a class="existingWikiWord" href="/nlab/show/predicate">predicate</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>in</mi> <mi>c</mi></msub></mrow><annotation encoding="application/x-tex">in_c</annotation></semantics></math> is the value of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>id</mi> <mi>c</mi></msub></mrow><annotation encoding="application/x-tex">id_c</annotation></semantics></math> under the assigned epimorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mi>P</mi><mi>c</mi><mo>,</mo><mi>P</mi><mi>c</mi><mo stretchy="false">)</mo><mo>→</mo><mrow><mo stretchy="false">|</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>c</mi><mo>×</mo><mi>P</mi><mi>c</mi><mo stretchy="false">)</mo><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">\hom(P c, P c) \to {|Pred_T(c \times P c)|}</annotation></semantics></math> (<em>à la</em> <a class="existingWikiWord" href="/nlab/show/Yoneda+lemma">Yoneda lemma</a>).</p> <p>The <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>in</mi> <mi>c</mi></msub></mrow><annotation encoding="application/x-tex">in_c</annotation></semantics></math> are called <em>generic predicates</em>. In particular, put <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo>=</mo><mi>P</mi><mn>1</mn></mrow><annotation encoding="application/x-tex">P = P 1</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>in</mi><mo>=</mo><msub><mi>in</mi> <mn>1</mn></msub><mo>∈</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>P</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">in = in_1 \in Pred_T(P)</annotation></semantics></math>, with corresponding epimorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>P</mi><mo stretchy="false">)</mo><mo>→</mo><mrow><mo stretchy="false">|</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">\hom(-, P) \to {|Pred_T|}</annotation></semantics></math>. If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed</a>, we then have <a class="existingWikiWord" href="/nlab/show/epimorphism">epis</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><msup><mi>P</mi> <mi>c</mi></msup><mo stretchy="false">)</mo><mo>≅</mo><mi>hom</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>P</mi><mo stretchy="false">)</mo><mo>∘</mo><mo stretchy="false">(</mo><mi>c</mi><mo>×</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msup><mo stretchy="false">)</mo> <mi>op</mi></msup><mo>→</mo><mrow><mo stretchy="false">|</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">|</mo></mrow><mo>∘</mo><mo stretchy="false">(</mo><mi>c</mi><mo>×</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><msup><mo stretchy="false">)</mo> <mi>op</mi></msup><mo>=</mo><mrow><mo stretchy="false">|</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">|</mo></mrow><mo stretchy="false">(</mo><mi>c</mi><mo>×</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\hom(-, P^c) \cong \hom(-, P) \circ (c \times -)^{op} \to {|Pred_T|} \circ (c \times -)^{op} = {|Pred_T|}(c \times -)</annotation></semantics></math></div> <p>and in this way the single generic predicate <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>P</mi><mo>,</mo><mi>in</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(P, in)</annotation></semantics></math> can be used to generate a generic predicate over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math>, as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msup><mi>P</mi> <mi>c</mi></msup><mo>,</mo><msub><mi>in</mi> <mi>c</mi></msub><mo>=</mo><mo stretchy="false">(</mo><msub><mi>eval</mi> <mi>c</mi></msub><msup><mo stretchy="false">)</mo> <mo>*</mo></msup><mo stretchy="false">(</mo><mi>in</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(P^c, in_c = (eval_c)^\ast(in))</annotation></semantics></math>, i.e., a generic predicate over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math> is obtained by pulling back along the <a class="existingWikiWord" href="/nlab/show/evaluation">evaluation</a> map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>eval</mi> <mi>c</mi></msub><mo lspace="verythinmathspace">:</mo><mi>c</mi><mo>×</mo><msup><mi>P</mi> <mi>c</mi></msup><mo>→</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">eval_c \colon c \times P^c \to P</annotation></semantics></math>. (N.B.: this need not reproduce the original generic predicates, but the resulting tripos structure may be compared with the original tripos structure in both directions: there are maps <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>c</mi><mo>→</mo><msup><mi>P</mi> <mi>c</mi></msup></mrow><annotation encoding="application/x-tex">P c \to P^c</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>P</mi> <mi>c</mi></msup><mo>→</mo><mi>P</mi><mi>c</mi></mrow><annotation encoding="application/x-tex">P^c \to P c</annotation></semantics></math>, with the generic predicates in the two triposes pulling back to each other along these maps.)</p> <p>In practice, the category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> will indeed often be <a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed</a> (frequently taking <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub><mo>=</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">C_T = Set</annotation></semantics></math> in fact), and triposes are frequently formed in the manner just described, starting with a generic predicate over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> and pulling it back along the maps <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>eval</mi> <mi>c</mi></msub></mrow><annotation encoding="application/x-tex">eval_c</annotation></semantics></math> to get a generic predicate over any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math>.</p> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>The surjective natural transformation defining the suitably generic predicate in a tripos of course induces a <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a> (but not necessarily <a class="existingWikiWord" href="/nlab/show/poset">posetal</a>) structure on each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow></msub><mo stretchy="false">(</mo><mi>Y</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_{C_T}(Y, X)</annotation></semantics></math>, the posetal reflection of which gives the Heyting algebra <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>Y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(Y)</annotation></semantics></math>. Accordingly, we can specify a tripos with category of terms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> by specifying an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>∈</mo><mi>Ob</mi><mo stretchy="false">(</mo><msub><mi>C</mi> <mi>T</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">X \in Ob(C_T)</annotation></semantics></math> and putting <a class="existingWikiWord" href="/nlab/show/Heyting+prealgebra">Heyting prealgebra</a> structure on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow></msub><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom_{C_T}(-, X)</annotation></semantics></math> in such a way as to yield all the first-order hyperdoctrine structure, with the identity morphism on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> playing the role of the suitably generic predicate.</p> </div> <h2 id="examples">Examples</h2> <h3 id="Topos">Coming from toposes</h3> <p>Every <a class="existingWikiWord" href="/nlab/show/topos">topos</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> gives rise to a tripos in an obvious way, using <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub><mo>=</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">C_T = E</annotation></semantics></math> and</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo>=</mo><mi>Sub</mi><mo lspace="verythinmathspace">:</mo><msup><mi>E</mi> <mi>op</mi></msup><mo>→</mo><mi>HeytAlg</mi><mo>,</mo></mrow><annotation encoding="application/x-tex">Pred_T = Sub \colon E^{op} \to HeytAlg,</annotation></semantics></math></div> <p>taking an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi></mrow><annotation encoding="application/x-tex">e</annotation></semantics></math> to the Heyting algebra of <a class="existingWikiWord" href="/nlab/show/subobjects">subobjects</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Sub</mi><mo stretchy="false">(</mo><mi>e</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Sub(e)</annotation></semantics></math>. Here of course we have not just an epimorphism but an <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphism</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><msup><mi>Ω</mi> <mi>c</mi></msup><mo stretchy="false">)</mo><mo>→</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>c</mi><mo>×</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mo>,</mo></mrow><annotation encoding="application/x-tex">\hom(-, \Omega^c) \to Pred_T(c \times -),</annotation></semantics></math></div> <p>obtained by pulling back the generic predicate <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo lspace="verythinmathspace">:</mo><mn>1</mn><mo>→</mo><mi>Ω</mi></mrow><annotation encoding="application/x-tex">t \colon 1 \to \Omega</annotation></semantics></math> over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math> along <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>eval</mi><mo lspace="verythinmathspace">:</mo><mi>c</mi><mo>×</mo><msup><mi>Ω</mi> <mi>c</mi></msup><mo>→</mo><mi>Ω</mi></mrow><annotation encoding="application/x-tex">eval \colon c \times \Omega^c \to \Omega</annotation></semantics></math>.</p> <h3 id="Heyt">Coming from complete Heyting algebras</h3> <p>If <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> is a <a class="existingWikiWord" href="/nlab/show/complete+Heyting+algebra">complete Heyting algebra</a>, we can take <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub><mo>=</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">C_T = Set</annotation></semantics></math>, and put</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo>=</mo><mi>hom</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>H</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><msup><mi>Set</mi> <mi>op</mi></msup><mo>→</mo><mi>HeytAlg</mi><mo>.</mo></mrow><annotation encoding="application/x-tex">Pred_T = \hom(-, H) \colon Set^{op} \to HeytAlg.</annotation></semantics></math></div> <p>Completeness of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> is used to ensure that for each function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f \colon X \to Y</annotation></semantics></math>, the Heyting algebra map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo><mo lspace="verythinmathspace">:</mo><msup><mi>H</mi> <mi>Y</mi></msup><mo>→</mo><msup><mi>H</mi> <mi>X</mi></msup></mrow><annotation encoding="application/x-tex">Pred_T(f) \colon H^Y \to H^X</annotation></semantics></math> has a left and right adjoint. The identity map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>H</mi><mo stretchy="false">)</mo><mo>→</mo><msub><mi>Pred</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">\hom(-, H) \to Pred_T</annotation></semantics></math> is the epimorphism we use to generate the tripos structure, taking of course <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>H</mi><mo>,</mo><msub><mn>1</mn> <mi>H</mi></msub><mo>∈</mo><msup><mi>H</mi> <mi>H</mi></msup><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(H, 1_H \in H^H)</annotation></semantics></math> as the generic predicate over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math>.</p> <h3 id="PCA">Coming from partial combinatory algebras</h3> <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 <a class="existingWikiWord" href="/nlab/show/partial+combinatory+algebra">partial combinatory algebra</a> (PCA), we can form a tripos in the following manner. Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub><mo>=</mo><mi>Set</mi></mrow><annotation encoding="application/x-tex">C_T = Set</annotation></semantics></math>. For each set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>, one can put a <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a> structure on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><msup><mo stretchy="false">)</mo> <mi>X</mi></msup></mrow><annotation encoding="application/x-tex">P(A)^X</annotation></semantics></math> [here, the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(A)</annotation></semantics></math> refers to the actual powerset 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> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>] as follows: given <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>,</mo><mi>g</mi><mo>∈</mo><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><msup><mo stretchy="false">)</mo> <mi>X</mi></msup></mrow><annotation encoding="application/x-tex">f, g \in P(A)^X</annotation></semantics></math>, let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Hom</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom(f, g)</annotation></semantics></math> be the set 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> in <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> such that for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f(x)</annotation></semantics></math>, <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> applied to <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> is defined and an element of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">g(x)</annotation></semantics></math>. We will of course take <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>≤</mo><mi>g</mi></mrow><annotation encoding="application/x-tex">f \leq g</annotation></semantics></math> just in case <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Hom</mi><mo stretchy="false">(</mo><mi>f</mi><mo>,</mo><mi>g</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom(f, g)</annotation></semantics></math> is inhabited. The relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>≤</mo></mrow><annotation encoding="application/x-tex">\leq</annotation></semantics></math> is reflexive and transitive, by functional completeness for PCA’s. It is straightforward that for a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">f \colon X \to Y</annotation></semantics></math>, the pullback map</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><msup><mo stretchy="false">)</mo> <mi>f</mi></msup><mo lspace="verythinmathspace">:</mo><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><msup><mo stretchy="false">)</mo> <mi>Y</mi></msup><mo>→</mo><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><msup><mo stretchy="false">)</mo> <mi>X</mi></msup></mrow><annotation encoding="application/x-tex">P(A)^f \colon P(A)^Y \to P(A)^X</annotation></semantics></math></div> <p>preserves the <a class="existingWikiWord" href="/nlab/show/preorder">preorder</a> structure. Now define <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Pred_T(X)</annotation></semantics></math> to be the poset obtained from the preorder <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><msup><mo stretchy="false">)</mo> <mi>X</mi></msup></mrow><annotation encoding="application/x-tex">P(A)^X</annotation></semantics></math> by posetal reflection. With the help of functional completeness, it may be shown that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Pred_T(X)</annotation></semantics></math> is in fact a Heyting algebra, and we get in this way a hyperdoctrine; see <a href="http://ncatlab.org/nlab/show/partial+combinatory+algebra#realizability_toposes_11">here</a> for details. Notice in this case we have, by construction, an epimorphism between set-valued functors</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>hom</mi> <mi>Set</mi></msub><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo>,</mo><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>→</mo><mrow><mo stretchy="false">|</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">|</mo></mrow></mrow><annotation encoding="application/x-tex">\hom_{Set}(-, P(A)) \to {|Pred_T|}</annotation></semantics></math></div> <p>and thus we obtain a tripos, called the <em>realizability tripos</em> associated with the PCA <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>.</p> <h2 id="from_triposes_to_toposes">From triposes to toposes</h2> <p>Every first-order hyperdoctrine <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo>=</mo><mo stretchy="false">(</mo><msub><mi>C</mi> <mi>T</mi></msub><mo>,</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T = (C_T, Pred_T)</annotation></semantics></math> gives rise to a <a class="existingWikiWord" href="/nlab/show/bicategory+of+relations">bicategory of relations</a>, whose objects are the objects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> and where <a class="existingWikiWord" href="/nlab/show/1-morphism">1-cells</a> from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math> are triples <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>Y</mi><mo>,</mo><mi>r</mi><mo>∈</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo>×</mo><mi>Y</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(X, Y, r \in Pred_T(X \times Y))</annotation></semantics></math>, thus thinking of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math> as a “relation” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">r \colon X \to Y</annotation></semantics></math>. Thus <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>=</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo>×</mo><mi>Y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\hom(X, Y) = Pred_T(X \times Y)</annotation></semantics></math>, and we define hom-composition in the usual way for relational composition, by expressing the formula <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>r</mi><mo>∘</mo><mi>s</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo>=</mo><msub><mo>∃</mo> <mi>y</mi></msub><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>s</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(r \circ s)(x, z) = \exists_y r(x, y) \wedge s(y, z)</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/internal+logic">internally</a> in the hyperdoctrine:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo>×</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>×</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>Y</mi><mo>×</mo><mi>Z</mi><mo stretchy="false">)</mo></mtd> <mtd><mover><mo>→</mo><mrow><msubsup><mi>π</mi> <mrow><mi>X</mi><mo>×</mo><mi>Y</mi></mrow> <mo>*</mo></msubsup><mo>×</mo><msubsup><mi>π</mi> <mrow><mi>Y</mi><mo>×</mo><mi>Z</mi></mrow> <mo>*</mo></msubsup></mrow></mover></mtd> <mtd><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo>×</mo><mi>Y</mi><mo>×</mo><mi>Y</mi><mo>×</mo><mi>Z</mi><mo stretchy="false">)</mo><mo>×</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo>×</mo><mi>Y</mi><mo>×</mo><mi>Y</mi><mo>×</mo><mi>Z</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mover><mo>→</mo><mo>∧</mo></mover></mtd> <mtd><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo>×</mo><mi>Y</mi><mo>×</mo><mi>Y</mi><mo>×</mo><mi>Z</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mover><mo>→</mo><mrow><mo stretchy="false">(</mo><mn>1</mn><mo>×</mo><mi>δ</mi><mo>×</mo><mn>1</mn><msup><mo stretchy="false">)</mo> <mo>*</mo></msup></mrow></mover></mtd> <mtd><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo>×</mo><mi>Y</mi><mo>×</mo><mi>Z</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mover><mo>→</mo><mrow><msub><mo>∃</mo> <mrow><mn>1</mn><mo>×</mo><mo>!</mo><mo>×</mo><mn>1</mn></mrow></msub></mrow></mover></mtd> <mtd><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo>×</mo><mi>Z</mi><mo stretchy="false">)</mo><mo>.</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ Pred_T(X \times Y) \times Pred_T(Y \times Z) & \stackrel{\pi_{X \times Y}^\ast \times \pi_{Y \times Z}^\ast}{\to} & Pred_T(X \times Y \times Y \times Z) \times Pred_T(X \times Y \times Y \times Z) \\ & \stackrel{\wedge}{\to} & Pred_T(X \times Y \times Y \times Z) \\ & \stackrel{(1 \times \delta \times 1)^\ast}{\to} & Pred_T(X \times Y \times Z) \\ & \stackrel{\exists_{1 \times ! \times 1}}{\to} & Pred_T(X \times Z). } </annotation></semantics></math></div> <p>This gives in fact a <a class="existingWikiWord" href="/nlab/show/dagger-category">dagger-category</a> <a class="existingWikiWord" href="/nlab/show/enriched+category">enriched</a> in <a class="existingWikiWord" href="/nlab/show/poset">posets</a>, where <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><msup><mo stretchy="false">)</mo> <mo>†</mo></msup><mo>:</mo><mi>hom</mi><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>→</mo><mi>hom</mi><mo stretchy="false">(</mo><mi>Y</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(-)^\dagger: \hom(X, Y) \to \hom(Y, X)</annotation></semantics></math> is the evident isomorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo>×</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>→</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>Y</mi><mo>×</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Pred_T(X \times Y) \to Pred_T(Y \times X)</annotation></semantics></math>. The <em>opposite</em> of a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">r \colon X \to Y</annotation></semantics></math> is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>r</mi> <mo>†</mo></msup><mo lspace="verythinmathspace">:</mo><mi>Y</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">r^\dagger \colon Y \to X</annotation></semantics></math>, and a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">r \colon X \to X</annotation></semantics></math> is <em>symmetric</em> if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>r</mi> <mo>†</mo></msup><mo>=</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">r^\dagger = r</annotation></semantics></math>. In summary, we get an <a class="existingWikiWord" href="/nlab/show/allegory">allegory</a> (bicategories of relations being essentially equivalent to unitary pretabular allegories).</p> <p>In this context, a <em><a class="existingWikiWord" href="/nlab/show/partial+equivalence+relation">partial equivalence relation</a></em>, or PER, may be defined as a symmetric idempotent map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">r \colon X \to X</annotation></semantics></math>. (In slightly more detail, a partial equivalence relation means we drop reflexivity from the notion of equivalence relation, so we mean transitivity <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mi>r</mi><mo>≤</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">r r \leq r</annotation></semantics></math> plus symmetry <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>r</mi> <mo>†</mo></msup><mo>=</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">r^\dagger = r</annotation></semantics></math>. However, for any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">r \colon X \to X</annotation></semantics></math>, it is a consequence of Freyd’s modular law for allegories that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>≤</mo><mi>r</mi><msup><mi>r</mi> <mo>†</mo></msup><mi>r</mi></mrow><annotation encoding="application/x-tex">r \leq r r^\dagger r</annotation></semantics></math>, so that transitivity and symmetry combined yield</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>≤</mo><mi>r</mi><msup><mi>r</mi> <mo>†</mo></msup><mi>r</mi><mo>=</mo><mi>r</mi><mi>r</mi><mi>r</mi><mo>≤</mo><mi>r</mi><mi>r</mi></mrow><annotation encoding="application/x-tex">r \leq r r^\dagger r = r r r \leq r r</annotation></semantics></math></div> <p>in addition to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mi>r</mi><mo>≤</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">r r \leq r</annotation></semantics></math>, meaning that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math> is in fact idempotent.)</p> <p>We will be interested in <a class="existingWikiWord" href="/nlab/show/split+idempotent">splitting</a> not all <a class="existingWikiWord" href="/nlab/show/idempotents">idempotents</a> (as in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math>-based or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Pos</mi></mrow><annotation encoding="application/x-tex">Pos</annotation></semantics></math>-based <a class="existingWikiWord" href="/nlab/show/Cauchy+completion">Cauchy completion</a>), but just the symmetric idempotents = PERs, in view of the following theorem.</p> <div class="num_theorem"> <h6 id="theorem">Theorem</h6> <p>Let <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> be a tripos, and let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Rel</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">Rel_T</annotation></semantics></math> be the bicategory of relations obtained from <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>. Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Split</mi> <mi>per</mi></msub><mo stretchy="false">(</mo><msub><mi>Rel</mi> <mi>T</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Split_{per}(Rel_T)</annotation></semantics></math> be the bicategory obtained by splitting the PERs. Then the locally discrete bicategory of maps (whose 1-cells are left adjoints or total functional relations) in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Split</mi> <mi>per</mi></msub><mo stretchy="false">(</mo><msub><mi>Rel</mi> <mi>T</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Split_{per}(Rel_T)</annotation></semantics></math> is a topos.</p> </div> <p>In the case of a <a href="#Topos">tripos induced from a topos <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></a>, this construction yields back <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>, since every partial equivalence relation (as a morphism of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Rel</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">Rel_T</annotation></semantics></math>) factors through a suitable subquotient object in <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>.</p> <p>In the case of a <a href="#PCA">realizability tripos</a> associated with a PCA <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math>, this construction yields the realizability topos 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>. In the particular case where <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/Kleene%27s+first+algebra">Kleene's first algebra</a> (the PCA whose elements are natural numbers taken as codes for computer programs taking natural number input and producing natural number output if they halt, with obvious application partial function), this is also called the <a class="existingWikiWord" href="/nlab/show/effective+topos">effective topos</a>.</p> <p>Before we undertake a conceptual analysis of this theorem, we give in the next section some details for the tripos attached to a complete Heyting algebra, described <a href="#Heyt">here</a>. The description of the resulting topos coincides with that of <span class="newWikiWord">Higgs<a href="/nlab/new/Denis+Higgs">?</a></span>, in his treatment of localic toposes in terms of Boolean-valued or Heyting-valued set theory (<em>à la</em> Scott and Solovay).</p> <h3 id="weak_triposes">Weak triposes</h3> <p>In <a href="#Pitts02">Pitts 2002</a> it is observed that a somewhat weaker condition than suffices to ensure that the above construction yields a topos.</p> <div class="num_defn"> <h6 id="definition_3">Definition</h6> <p>A <strong>weak tripos</strong> is a first-order hyperdoctrine <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> together with, for every object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>c</mi></mrow><annotation encoding="application/x-tex">c</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math>, an object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi><mi>c</mi></mrow><annotation encoding="application/x-tex">P c</annotation></semantics></math> and an element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>in</mi> <mi>c</mi></msub><mo>∈</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>c</mi><mo>×</mo><mi>P</mi><mi>c</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">in_c \in Pred_T(c \times P c)</annotation></semantics></math> such that for any object <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>b</mi></mrow><annotation encoding="application/x-tex">b</annotation></semantics></math> and element <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>p</mi><mo>∈</mo><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>c</mi><mo>×</mo><mi>b</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">p \in Pred_T(c \times b)</annotation></semantics></math>, the following sentence is satisfied in the <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a> of <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>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>∀</mo><mi>i</mi><mo>:</mo><mi>b</mi><mo>.</mo><mo>∃</mo><mi>s</mi><mo>:</mo><mi>P</mi><mi>c</mi><mo>.</mo><mo>∀</mo><mi>x</mi><mo>:</mo><mi>c</mi><mo>.</mo><msub><mo>∈</mo> <mi>c</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>s</mi><mo stretchy="false">)</mo><mo>⇔</mo><mi>p</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>i</mi><mo stretchy="false">)</mo><mo>.</mo></mrow><annotation encoding="application/x-tex"> \forall i:b. \exists s:P c. \forall x:c. \in_c(x,s) \Leftrightarrow p(x,i). </annotation></semantics></math></div></div> <p>This generalization is not vacuous either. For instance, it is shown in <a href="#Pitts02">Pitts 2002</a> that for any infinite <a class="existingWikiWord" href="/nlab/show/Boolean+algebra">Boolean algebra</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>B</mi></mrow><annotation encoding="application/x-tex">B</annotation></semantics></math> there is a weak tripos over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>FinSet</mi></mrow><annotation encoding="application/x-tex">FinSet</annotation></semantics></math>, constructed analogously to the tripos attached to a complete Heyting algebra. (We don’t need <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> to be complete since we have only finite sets in the base; but we do need <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> to be Boolean rather than just Heyting in order to prove that this is a weak tripos. The resulting topos has <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> as its poset of <a class="existingWikiWord" href="/nlab/show/subterminal+objects">subterminal objects</a>; it is unknown whether every (not necessarily complete) Heyting algebra can occur as the poset of subterminals in an elementary topos.)</p> <p>In fact, it also seems unnecessary for the hyperdoctrine <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> to have equality, since in constructing a topos we equip every object with a <em>new</em> partial equivalence relation to become its “equality”. However, the above construction that goes through a bicategory of relations does rely on the existence of equality, as does the statement of the universal property of this construction (since equality in <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> gives an embedding of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> as “constant objects” in its associated topos, which is the <a class="existingWikiWord" href="/nlab/show/unit+of+an+adjunction">unit of an adjunction</a>).</p> <h3 id="a_synthetic_view_of_triposes">A “synthetic” view of triposes</h3> <p>Every tripos <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> over a topos <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> gives rise to a so-called “constant objects” functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Δ</mi> <mi>P</mi></msub><mo>:</mo><mi>S</mi><mo>→</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">\Delta_P : S \to E</annotation></semantics></math> where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> is the topos <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi><mo stretchy="false">[</mo><mi>P</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">S[P]</annotation></semantics></math> induced by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>. It sends <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>I</mi><mo>,</mo><msub><mi mathvariant="normal">eq</mi> <mi>I</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(I,\mathrm{eq}_I)</annotation></semantics></math> where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi mathvariant="normal">eq</mi> <mi>I</mi></msub></mrow><annotation encoding="application/x-tex">\mathrm{eq}_I</annotation></semantics></math> is the equality predicate on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> in the sense of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math>. For the constant objects functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Δ</mi> <mi>P</mi></msub><mo>:</mo><mi>S</mi><mo>→</mo><mi>E</mi></mrow><annotation encoding="application/x-tex">\Delta_P : S \to E</annotation></semantics></math> we know that</p> <ol> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Δ</mi> <mi>P</mi></msub></mrow><annotation encoding="application/x-tex">\Delta_P</annotation></semantics></math> preserves finite limits</p> </li> <li> <p>every <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> appears as subquotient of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Δ</mi> <mi>P</mi></msub><mi>I</mi></mrow><annotation encoding="application/x-tex">\Delta_P I</annotation></semantics></math> for some <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math></p> </li> <li> <p>there is a subobject <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>t</mi><mo>:</mo><mi>T</mi><mo>↣</mo><msub><mi>Δ</mi> <mi>P</mi></msub><mi>Σ</mi></mrow><annotation encoding="application/x-tex">t : T \rightarrowtail \Delta_P\Sigma</annotation></semantics></math> such that every mono <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>m</mi><mo>:</mo><mi>X</mi><mo>↣</mo><msub><mi>Δ</mi> <mi>P</mi></msub><mi>I</mi></mrow><annotation encoding="application/x-tex">m : X \rightarrowtail \Delta_P I</annotation></semantics></math> appears as pullback of <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> along <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Δ</mi> <mi>P</mi></msub><mi>f</mi></mrow><annotation encoding="application/x-tex">\Delta_P f</annotation></semantics></math> for some (typically not unique) map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>I</mi><mo>→</mo><mi>Σ</mi></mrow><annotation encoding="application/x-tex">f : I \to \Sigma</annotation></semantics></math> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math></p> </li> </ol> <p>and that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> is obtained from the subobject fibration of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> by change of base along along <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Δ</mi> <mi>P</mi></msub></mrow><annotation encoding="application/x-tex">\Delta_P</annotation></semantics></math>. It follows from observations in Pitts’ thesis that this way triposes over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> correspond up to equivalence to functors <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> to toposes <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> validates the above conditions (1)-(3). Moreover, <em>weak</em> triposes over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> correspond to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> which validate only conditions (1) and (2). Such <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> are inverse image parts of localic geometric morphisms iff <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>F</mi></mrow><annotation encoding="application/x-tex">F</annotation></semantics></math> has a right adjoint.</p> <p>Somewhat surprisingly the “chaotic” functor <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∇</mo></mrow><annotation encoding="application/x-tex">\nabla</annotation></semantics></math> from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Set</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{Set}</annotation></semantics></math> to the topos of reflexive graphs is a weak tripos in the above sense. For every non-empty set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> the functor <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><msup><mo stretchy="false">)</mo> <mi>I</mi></msup><mo>:</mo><mstyle mathvariant="bold"><mi>Set</mi></mstyle><mo>→</mo><mstyle mathvariant="bold"><mi>Set</mi></mstyle></mrow><annotation encoding="application/x-tex">(-)^I : \mathbf{Set} \to \mathbf{Set}</annotation></semantics></math> is a weak tripos. For non-isomorphic finite non-empty sets <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>I</mi></mrow><annotation encoding="application/x-tex">I</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>J</mi></mrow><annotation encoding="application/x-tex">J</annotation></semantics></math> the functors <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><msup><mo stretchy="false">)</mo> <mi>I</mi></msup></mrow><annotation encoding="application/x-tex">(-)^I</annotation></semantics></math> and <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><msup><mo stretchy="false">)</mo> <mi>J</mi></msup></mrow><annotation encoding="application/x-tex">(-)^J</annotation></semantics></math> are not equivalent. Thus, nonequivalent weak triposes over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Set</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{Set}</annotation></semantics></math> can give rise to equivalent toposes. It is an open question whether this is also possible for genuine non-weak triposes over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Set</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{Set}</annotation></semantics></math>.</p> <h2 id="relation_to_valued_sets">Relation to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>-valued sets</h2> <p>Consider the tripos <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo>=</mo><msub><mi>T</mi> <mi>H</mi></msub></mrow><annotation encoding="application/x-tex">T = T_H</annotation></semantics></math> obtained from a complete Heyting algebra <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> (<a href="#Heyt">example 2</a>), or more exactly the bicategory of relations obtained from this. Let us describe explicitly the bicategory obtained by splitting the PERs:</p> <ul> <li> <p>An object in the PER-splitting completion in this case is a set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> equipped with a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>×</mo><mi>X</mi><mo>→</mo><mi>H</mi></mrow><annotation encoding="application/x-tex">e \colon X \times X \to H</annotation></semantics></math> which is symmetric and transitive in the sense described above. This boils down to having, for all elements <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>,</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo>∈</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">x, y, z \in X</annotation></semantics></math>,</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>e</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">e(x, y) = e(y, x)</annotation></semantics></math></div><div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>e</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>e</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>e</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>z</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">e(x, y) \wedge e(y, z) \leq e(x, z)</annotation></semantics></math></div> <p>This is also known as an <em><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>-valued set</em>. (We do not assume reflexivity, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊤</mo><mo>≤</mo><mi>e</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\top \leq e(x, x)</annotation></semantics></math> for all <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi></mrow><annotation encoding="application/x-tex">x</annotation></semantics></math>.) The function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi></mrow><annotation encoding="application/x-tex">e</annotation></semantics></math> can be thought of as a measure of equality.</p> </li> <li> <p>A morphism from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(X, e_X)</annotation></semantics></math> to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>Y</mi><mo>,</mo><msub><mi>e</mi> <mi>Y</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(Y, e_Y)</annotation></semantics></math> is a relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">r \colon X \to Y</annotation></semantics></math>, or a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>×</mo><mi>Y</mi><mo>→</mo><mi>H</mi></mrow><annotation encoding="application/x-tex">r \colon X \times Y \to H</annotation></semantics></math>, such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>∘</mo><msub><mi>e</mi> <mi>X</mi></msub><mo>=</mo><mi>r</mi><mo>=</mo><msub><mi>e</mi> <mi>Y</mi></msub><mo>∘</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">r \circ e_X = r = e_Y \circ r</annotation></semantics></math>. (Cf. <a class="existingWikiWord" href="/nlab/show/Karoubi+envelope">Karoubi envelope</a>.) The conditions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>∘</mo><msub><mi>e</mi> <mi>X</mi></msub><mo>≤</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">r \circ e_X \leq r</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>e</mi> <mi>Y</mi></msub><mo>∘</mo><mi>r</mi><mo>≤</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">e_Y \circ r \leq r</annotation></semantics></math> mean we have a two-sided “action”:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>,</mo><mspace width="2em"></mspace><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∧</mo><msub><mi>e</mi> <mi>Y</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>y</mi><mo>′</mo><mo stretchy="false">)</mo><mo>≤</mo><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo>′</mo><mo stretchy="false">)</mo><mo>.</mo></mrow><annotation encoding="application/x-tex">e_X(x', x) \wedge r(x, y) \leq r(x', y), \qquad r(x, y) \wedge e_Y(y, y') \leq r(x, y').</annotation></semantics></math></div> <p>The condition <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>≤</mo><mi>r</mi><mo>∘</mo><msub><mi>e</mi> <mi>X</mi></msub></mrow><annotation encoding="application/x-tex">r \leq r \circ e_X</annotation></semantics></math> means</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>≤</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mrow><mi>x</mi><mo>′</mo><mo>∈</mo><mi>X</mi></mrow></munder><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo><mo>∧</mo><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">r(x, y) \leq \bigvee_{x' \in X} e_X(x, x') \wedge r(x', y)</annotation></semantics></math></div> <p>but since <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>e</mi> <mi>X</mi></msub></mrow><annotation encoding="application/x-tex">e_X</annotation></semantics></math> is symmetric and transitive, we have</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mtd> <mtd><mo>≤</mo></mtd> <mtd><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mrow><mi>x</mi><mo>′</mo><mo>∈</mo><mi>X</mi></mrow></munder><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo><mo>∧</mo><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>=</mo></mtd> <mtd><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mrow><mi>x</mi><mo>′</mo></mrow></munder><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo><mo>∧</mo><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>≤</mo></mtd> <mtd><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mrow><mi>x</mi><mo>′</mo></mrow></munder><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo><mo>∧</mo><mi>e</mi><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>e</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ r(x, y) & \leq & \bigvee_{x' \in X} e_X(x, x') \wedge r(x', y)\\ & = & \bigvee_{x'} e_X(x, x') \wedge e_X(x', x) \wedge r(x', y)\\ & \leq & \bigvee_{x'} e_X(x, x') \wedge e(x', x) \leq e(x, x) } </annotation></semantics></math></div> <p>so that in fact we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>≤</mo><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">r(x, y) \leq e_X(x, x)</annotation></semantics></math>. Similarly we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>≤</mo><mi>e</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">r(x, y) \leq e(y, y)</annotation></semantics></math>, and these two conditions conversely imply <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>≤</mo><mi>r</mi><mo>∘</mo><msub><mi>e</mi> <mi>X</mi></msub></mrow><annotation encoding="application/x-tex">r \leq r \circ e_X</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>≤</mo><msub><mi>e</mi> <mi>Y</mi></msub><mo>∘</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">r \leq e_Y \circ r</annotation></semantics></math>, as may be easily checked.</p> </li> </ul> <p>Such morphisms <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math> are called <em>relations between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>-valued sets</em>. Such relations in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Split</mi> <mi>per</mi></msub><mo stretchy="false">(</mo><msub><mi>Rel</mi> <mi>T</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Split_{per}(Rel_T)</annotation></semantics></math> may be composed just as they are in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Rel</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">Rel_T</annotation></semantics></math>, and if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi></mrow><annotation encoding="application/x-tex">r</annotation></semantics></math> is an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>-valued relation, so is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>r</mi> <mo>†</mo></msup></mrow><annotation encoding="application/x-tex">r^\dagger</annotation></semantics></math>. On the other hand, as described at <a class="existingWikiWord" href="/nlab/show/Karoubi+envelope">Karoubi envelope</a>, the identity from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>e</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(X, e)</annotation></semantics></math> to itself is given by the relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi></mrow><annotation encoding="application/x-tex">e</annotation></semantics></math> (clearly the identity <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mn>1</mn> <mi>X</mi></msub></mrow><annotation encoding="application/x-tex">1_X</annotation></semantics></math> doesn’t work!). The result <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Split</mi> <mi>per</mi></msub><mo stretchy="false">(</mo><msub><mi>Rel</mi> <mi>T</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Split_{per}(Rel_T)</annotation></semantics></math> is also a bicategory of relations (although, as we will eventually see, much more is true).</p> <p>A relation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo lspace="verythinmathspace">:</mo><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">)</mo><mo>→</mo><mo stretchy="false">(</mo><mi>Y</mi><mo>,</mo><msub><mi>e</mi> <mi>Y</mi></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">r \colon (X, e_X) \to (Y, e_Y)</annotation></semantics></math> between PERs is <em>functional</em> if</p> <ul> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>∘</mo><msup><mi>r</mi> <mo>†</mo></msup><mo>≤</mo><msub><mn>1</mn> <mrow><mo stretchy="false">(</mo><mi>Y</mi><mo>,</mo><msub><mi>e</mi> <mi>Y</mi></msub><mo stretchy="false">)</mo></mrow></msub><mo>=</mo><msub><mi>e</mi> <mi>Y</mi></msub></mrow><annotation encoding="application/x-tex">r \circ r^\dagger \leq 1_{(Y, e_Y)} = e_Y</annotation></semantics></math> (“well-definedness”).</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>e</mi> <mi>X</mi></msub><mo>=</mo><msub><mn>1</mn> <mrow><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">)</mo></mrow></msub><mo>≤</mo><msup><mi>r</mi> <mo>†</mo></msup><mo>∘</mo><mi>r</mi></mrow><annotation encoding="application/x-tex">e_X = 1_{(X, e_X)} \leq r^\dagger \circ r</annotation></semantics></math> (“totality”);</p> </li> </ul> <p>The first of these conditions means</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msup><mi>r</mi> <mo>†</mo></msup><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo>′</mo><mo stretchy="false">)</mo><mo>=</mo><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo>′</mo><mo stretchy="false">)</mo><mo>≤</mo><msub><mi>e</mi> <mi>Y</mi></msub><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>y</mi><mo>′</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">r^\dagger(y, x) \wedge r(x, y') = r(x, y) \wedge r(x, y') \leq e_Y(y, y')</annotation></semantics></math></div> <p>The second condition means</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo><mo>≤</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mrow><mi>y</mi><mo>∈</mo><mi>Y</mi></mrow></munder><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∧</mo><msup><mi>r</mi> <mo>†</mo></msup><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">e_X(x, x') \leq \bigvee_{y \in Y} r(x, y) \wedge r^\dagger(y, x')</annotation></semantics></math></div> <p>which certainly implies <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≤</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mi>y</mi></msub><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">e_X(x, x) \leq \bigvee_y r(x, y)</annotation></semantics></math>. Conversely, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≤</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mi>y</mi></msub><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">e_X(x, x) \leq \bigvee_y r(x, y)</annotation></semantics></math>, we have</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo></mtd> <mtd><mo>≤</mo></mtd> <mtd><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>∧</mo><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>≤</mo></mtd> <mtd><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mi>y</mi></munder><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∧</mo><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>≤</mo></mtd> <mtd><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mi>y</mi></munder><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∧</mo><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>′</mo><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>≤</mo></mtd> <mtd><munder><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mi>y</mi></munder><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>∧</mo><msup><mi>r</mi> <mo>†</mo></msup><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo>′</mo><mo stretchy="false">)</mo><mo>.</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex">\array{ e_X(x, x') & \leq & e_X(x, x) \wedge e_X(x, x') \\ & \leq & \bigvee_y r(x, y) \wedge e_X(x, x') \\ & \leq & \bigvee_y r(x, y) \wedge r(x', y) \\ & \leq & \bigvee_y r(x, y) \wedge r^\dagger(y, x'). } </annotation></semantics></math></div> <p>Thus totality of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">r \colon X \to Y</annotation></semantics></math> is equivalent to</p> <ul> <li><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>e</mi> <mi>X</mi></msub><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo><mo>≤</mo><msub><mo lspace="thinmathspace" rspace="thinmathspace">⋁</mo> <mrow><mi>y</mi><mo>∈</mo><mi>Y</mi></mrow></msub><mi>r</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">e_X(x, x) \leq \bigvee_{y \in Y} r(x, y)</annotation></semantics></math></li> </ul> <div class="num_theorem"> <h6 id="theorem_higgs">Theorem (Higgs)</h6> <p>For a complete Heyting algebra <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>, the category of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>-valued sets and functional relations between <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>-valued sets is equivalent to the topos of <a class="existingWikiWord" href="/nlab/show/sheaf">sheaves</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>.</p> </div> <p>Thus all <a class="existingWikiWord" href="/nlab/show/localic+topos">localic toposes</a> arise as toposes of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math>-valued sets, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> is the Heyting algebra of subobjects of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>1</mn></mrow><annotation encoding="application/x-tex">1</annotation></semantics></math>.</p> <p>Compare the description by Walters of sheaves over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>H</mi></mrow><annotation encoding="application/x-tex">H</annotation></semantics></math> as certain types of Cauchy-complete categories enriched in a bicategory. Notice that in that description, the homs are symmetric (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>hom</mi><mo stretchy="false">(</mo><mi>x</mi><mo>,</mo><mi>y</mi><mo stretchy="false">)</mo><mo>=</mo><mi>hom</mi><mo stretchy="false">(</mo><mi>y</mi><mo>,</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\hom(x, y) = \hom(y, x)</annotation></semantics></math>), so that the Cauchy completion or idempotent-splitting completion is the same as the completion by splitting symmetric idempotents.</p> <div class="num_remark"> <h6 id="remark_2">Remark</h6> <p>The triposes over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> of this form are precisely those for which the preorder imposed on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>Set</mi></msub><mo stretchy="false">(</mo><mi>X</mi><mo>,</mo><mi>P</mi><mo stretchy="false">)</mo><mo>≃</mo><msup><mi>P</mi> <mi>X</mi></msup></mrow><annotation encoding="application/x-tex">Hom_{Set}(X, P) \simeq P^X</annotation></semantics></math> is the straightforward <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>-ary product of the preorder imposed on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Hom</mi> <mi>Set</mi></msub><mo stretchy="false">(</mo><mn>1</mn><mo>,</mo><mi>P</mi><mo stretchy="false">)</mo><mo>≃</mo><mi>P</mi></mrow><annotation encoding="application/x-tex">Hom_{Set}(1, P) \simeq P</annotation></semantics></math>, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>P</mi></mrow><annotation encoding="application/x-tex">P</annotation></semantics></math> is the carrier of the generic predicate; in all other cases, the former is a finer-grained preorder than the latter. Thus, in some sense, triposes over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Set</mi></mrow><annotation encoding="application/x-tex">Set</annotation></semantics></math> are a generalization of the notion of “complete Heyting algebra” taking advantage of the ability to use preorder rather than poset structure to allow for a weakening of the condition of completeness.</p> <p>An example taking advantage of this generalization is given by <a href="#PCA">realizability triposes</a>. See also <a class="existingWikiWord" href="/nlab/show/realizability">realizability</a>.</p> </div> <h2 id="relation_to_exact_completion">Relation to exact completion</h2> <p>As stated above, the topos obtained from a tripos can be described as the category of PERs in the bicategory of relations, and functional relations between them. In different language, the bicategory of PERs or symmetric idempotents and relations between them is a <a class="existingWikiWord" href="/nlab/show/power+allegory">power allegory</a>, and the process of passing to functional relations is just the standard process of passing from power allegories to toposes.</p> <p>The process of splitting symmetric idempotents in the bicategory of relations can be analyzed into two steps, the first related to taking a regular completion, and the second to taking an <a class="existingWikiWord" href="/nlab/show/exact+completion">exact completion</a> of a regular category. More exactly, they are analogues on the allegorical side of these two types of completion.</p> <p>The two steps are as follows, starting with a bicategory of relations (or perhaps preferably a <a class="existingWikiWord" href="/nlab/show/framed+bicategory">framed bicategory</a> of relations). Splitting symmetric idempotents can be obtained by</p> <ul> <li> <p>First splitting the coreflexive morphisms (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo lspace="verythinmathspace">:</mo><mi>X</mi><mo>→</mo><mi>X</mi></mrow><annotation encoding="application/x-tex">r \colon X \to X</annotation></semantics></math> is coreflexive if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>r</mi><mo>≤</mo><msub><mn>1</mn> <mi>X</mi></msub></mrow><annotation encoding="application/x-tex">r \leq 1_X</annotation></semantics></math>). This results in a tabular bicategory of relations or a <a class="existingWikiWord" href="/nlab/show/allegory">unitary tabular allegory</a>, which is essentially the same as obtaining a regular category.</p> </li> <li> <p>Then, in the unitary tabular allegory, split equivalence relations. In allegorical language, this results in an effective (unitary tabular) allegory (Freyd-Scedrov, page 213); on the categorical side, it means we pass from a regular category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>C</mi></mrow><annotation encoding="application/x-tex">C</annotation></semantics></math> to its <a class="existingWikiWord" href="/nlab/show/regular+and+exact+completions">exact completion</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mrow><mi>ex</mi><mo stretchy="false">/</mo><mi>reg</mi></mrow></msub></mrow><annotation encoding="application/x-tex">C_{ex/reg}</annotation></semantics></math>.</p> </li> </ul> <h2 id="internal_logic">Internal logic</h2> <p>Of course, the topos obtained from a tripos has an <a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>. But a tripos itself has an internal logic in which the “types” are the objects of the base category and the propositions are those of the fiber category. In fact, the internal logic of a topos is often presented in a way that actually only makes use of the tripos of subobjects of the topos. The type constructors of this internal logic correspond to objects with universal properties in the base category; so in a general tripos there would be only <a class="existingWikiWord" href="/nlab/show/product+types">product types</a> and <a class="existingWikiWord" href="/nlab/show/power+types">power types</a>. If the base category is cartesian closed, then the latter would decompose into <a class="existingWikiWord" href="/nlab/show/function+types">function types</a> and a <a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a>. However, note that these “functions” are less general than the morphisms in the topos constructed from the tripos; in the internal language of the tripos the latter manifest as <a class="existingWikiWord" href="/nlab/show/anafunctions">anafunctions</a>.</p> <h2 id="references">References</h2> <ul id="PittsThesis"> <li><a class="existingWikiWord" href="/nlab/show/Andrew+Pitts">Andrew Pitts</a>, <em>The theory of <a class="existingWikiWord" href="/nlab/show/triposes">triposes</a></em>, thesis, <a href="http://www.cl.cam.ac.uk/~amp12/papers/thet/thet.pdf">pdf</a></li> </ul> <ul id="Pitts02"> <li><a class="existingWikiWord" href="/nlab/show/Andrew+Pitts">Andrew Pitts</a>, <em>Tripos theory in retrospect</em>, <a href="http://www.cl.cam.ac.uk/~amp12/papers/tritr/tritr.pdf">pdf</a></li> </ul> <ul> <li><a class="existingWikiWord" href="/nlab/show/Peter+Freyd">Peter Freyd</a> and Andre Scedrov, <em>Categories, Allegories</em>, North-Holland 1990.</li> </ul> <div class="footnotes"><hr /><ol><li id="fn:1"> <p>In fact one may “quantify” along any term = morphism in the base category <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math>, i.e., each <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>Pred</mi> <mi>T</mi></msub><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Pred_T(f)</annotation></semantics></math> has a left adjoint and a right adjoint, merely if we assume this of projection and diagonal maps and if we assume an appropriate <a href="http://ncatlab.org/nlab/show/Frobenius+reciprocity#frobenius_laws_and_frobenius_reciprocity_11">Frobenius law</a>, as one generally does for first-order hyperdoctrines. However, the status of corresponding <a class="existingWikiWord" href="/nlab/show/Beck-Chevalley+conditions">Beck-Chevalley conditions</a> for <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> diagrams in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> is another matter; the original treatment by Pitts assumed more than is actually necessary. Namely, it was assumed that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math> is finitely complete and the Beck-Chevalley condition holds for <em>all</em> pullbacks in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math>. In actuality, for tripos theory, it is enough to assume Beck-Chevalley only for certain pullbacks which exist by virtue of the finite product structure of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>C</mi> <mi>T</mi></msub></mrow><annotation encoding="application/x-tex">C_T</annotation></semantics></math>. <a href="#fnref:1" rev="footnote">↩</a></p> </li></ol></div></body></html> </div> <div class="revisedby"> <p> Last revised on August 28, 2019 at 09:53:51. See the <a href="/nlab/history/tripos" 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/tripos" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/4057/#Item_7">Discuss</a><span class="backintime"><a href="/nlab/revision/tripos/25" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/tripos" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/tripos" accesskey="S" class="navlink" id="history" rel="nofollow">History (25 revisions)</a> <a href="/nlab/show/tripos/cite" style="color: black">Cite</a> <a href="/nlab/print/tripos" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/tripos" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>