<ol>
<li><p>Define an <strong>IR system</strong> be a family <span class="math-container">$U \in \mathrm{Set}$</span> and a function <span class="math-container">$\phi \in U \to \mathrm{Set}$</span>.</p>
<p>IR systems form a domain. The least element is <span class="math-container">$\bot = (\emptyset, !)$</span>. The order relationship <span class="math-container">$(U, \phi) \leq (U', \phi')$</span> holds when <span class="math-container">$U \subseteq U'$</span>, and for all <span class="math-container">$c \in U$</span>, we have <span class="math-container">$\phi(c) = \phi'(c)$</span>. (Limits are computed in the obvious way, by union.)</p>
</li>
<li><p><strong>Pataraia's Theorem</strong>: Suppose <span class="math-container">$D$</span> is a domain, and <span class="math-container">$f : D \to D$</span> is a monotone
function on <span class="math-container">$D$</span>. Then <span class="math-container">$f$</span> has a least fixed point.</p>
</li>
</ol>
<p>So for any monotone function on IR systems (i.e., basically any sensible inductive-recursive definition), it has a least fixed point.</p>
<p>Pataraia's theorem is provable in the internal language of any topos, since it is a proof in intuitionistic bounded ZF. (I reproduce the proof below.)</p>
<p>However, the definition of IR system uses a function <span class="math-container">$\phi : U \to \mathrm{Set}$</span>, so we need a well-behaved universe of small sets to interpret this.</p>
<p>In his 2004 paper, <a href="https://www2.mathematik.tu-darmstadt.de/%7Estreicher/NOTES/UniTop.pdf" rel="nofollow noreferrer"><em>Universes in Toposes</em></a>, Thomas Streicher says that not all topoi have such a universe (in particular, the free topos doesn't). but he says that Set, realisability models, and Grothendieck topoi all have universes. (Fair warning: I've read this paper, but haven't tried to reproduce his proofs!)</p>
<hr />
<p><strong>Proof of Pataraia's theorem</strong></p>
<p>Define an <span class="math-container">$f$</span>-inflationary set to be be a set <span class="math-container">$U \subseteq D$</span> which
contains <span class="math-container">$\bot$</span>, is closed under <span class="math-container">$f$</span> (i.e., if <span class="math-container">$x \in U$</span>, then <span class="math-container">$f(x)
\in S$</span>), and contains joins of directed sets in <span class="math-container">$U$</span>.</p>
<p>Let <span class="math-container">$S$</span> be the intersection of all <span class="math-container">$f$</span>-inflationary sets (i.e, the
least <span class="math-container">$f$</span>-inflationary set). Now, note that:</p>
<ol>
<li><span class="math-container">$S$</span> itself a domain, since <span class="math-container">$\bot \in S$</span>, and it contains directed joins by definition.</li>
<li>The restriction <span class="math-container">$f : S \to S$</span> is inflationary (i.e., for all
<span class="math-container">$x \in S$</span>, <span class="math-container">$x \leq f(x)$</span>).</li>
</ol>
<p>Next, let <span class="math-container">$E(S)$</span> to be the set of inflationary, monotone maps <span class="math-container">$S \to S$</span>.</p>
<p>Now, <span class="math-container">$E(S)$</span> is a domain. Its least element is the identity function
<span class="math-container">$\mathit{id}_S$</span>, and the order and joins are computed pointwise.</p>
<p><span class="math-container">$E(S)$</span> is also a directed set itself. Suppose you have <span class="math-container">$f$</span> and <span class="math-container">$g$</span> in
<span class="math-container">$E(S)$</span>.  Then, it is clear that <span class="math-container">$f \circ g \in E(S)$</span>, and because both
<span class="math-container">$f$</span> and <span class="math-container">$g$</span> are increasing, <span class="math-container">$f \leq f \circ g$</span> and <span class="math-container">$g \leq f \circ g$</span>.</p>
<p>Hence, the lub (call it <span class="math-container">$m$</span>) of <span class="math-container">$E(C)$</span> is itself an element of <span class="math-container">$E(C)$</span>.
So <span class="math-container">$m$</span> is itself an inflationary, monotone map. Since <span class="math-container">$f$</span> is an
element of <span class="math-container">$E(C)$</span>, we know that <span class="math-container">$f \circ m \in E(C)$</span>, and so <span class="math-container">$f \circ
m \leq m$</span>. Since <span class="math-container">$f$</span> is inflationary, we also have that <span class="math-container">$m \leq f\circ
m$</span>.</p>
<p>So for every element <span class="math-container">$s \in S$</span>, we have <span class="math-container">$f(m(s)) = m(s)$</span>.</p>
<p>So <span class="math-container">$m(\bot)$</span> is the least fixed point of <span class="math-container">$f$</span>.</p>

CC BY-SA 4.0
2022-01-24T15:21:05.250Z
Hi Neel! Indeed, I was trying to sketch this argument since our discussion but got a bit turned around. Some of this is linguistic (categorical universes aren't exactly like sets internally, so they don't automatically have subset relation assigned to them and the obvious choice of requiring a monic `el(A) >-> el(B)` is sensible, but doesn't make them a partial order, merely a pre-order, etc). Some of my confusion was a bit more foundational though...
daniel gratzer
CC BY-SA 4.0
2022-01-24T15:21:57.003Z
[sorry, character limit]...  because the literature seems to claim that IR is equivalent to a very large large cardinal axiom (a Mahlo cardinal), but having a universe in a topos is "just" equivalent to a strongly inaccessible cardinal! Is the difference being made up for in the subobject classifier and does this in turn mean that IR is actually quite weak in classical ZFC, for instance?
daniel gratzer
CC BY-SA 4.0
2022-01-24T15:31:16.757Z
Let me try and drag this out further. Let's say I have a universe in a topos which is big enough to classify the subobject classifier. This is true in $\mathbf{Set}$ if I have just one Grothendieck universe. I then can use IR to build a hierarchy of universes, each containing the subobject classifier. But now I seem to have gone from 1 universe + universe of propositions to a hierarchy + a universe of propositions which shouldn't be possible, should it?
daniel gratzer
CC BY-SA 4.0
2022-01-24T17:38:17.520Z
Are IR systems actually a domain? Domains need to have joins of _all_ directed sets, but maybe size limitations on the sort of unions a universe is closed under cause it to not quite be a domain? Something along those lines seem like a point where the proof might subtly fail.
Dan Doel
CC BY-SA 4.0
2022-01-24T18:11:33.037Z
Hi Neel, I am nearly certain that there must be some mistake somewhere. ZFC+U is consistent with "there does not exist a mahlo cardinal", so if this argument sufficed to show exhibit initial algebras for all IR functors, it would also prove that ZFC is inconsistent with one Grothendieck universe.
Jonathan Sterling
CC BY-SA 4.0
2022-01-25T17:36:05.500Z
@DanDoel I think I have just about convinced myself that you are right. For each small set $x$, we can define an IR system $(\{x\}, x \mapsto \mathbb{N})$. Then the code part of the join of all these things will be the non-small set of all small sets, which is not an IR system per my definition. For this to work you have to bound the cardinality of the $U$'s so that their union is itself small.
Neel Krishnaswami
CC BY-SA 4.0
2022-06-06T22:49:16.847Z
[Here](https://hub.darcs.net/dolio/agda-share/browse/IRDomain.agda) is a formalization of the argument. I was going to also formalize the argument that a system corresponding to the identity partial function is a problem, but I couldn't think of a simple way of formalizing the correspondence (it's not very 'structural').
Dan Doel
CC BY-SA 4.0
2022-01-24T15:01:35.687Z
2022-01-24T15:01:35.687Z
Neel Krishnaswami
<p>This is mostly a reaction to the questions posed in the comments to Neel's answer.</p>
<p>Partial maps <span class="math-container">$A \rightharpoonup B$</span> between sets <span class="math-container">$A$</span> and <span class="math-container">$B$</span> form a domain, where we view such maps as single-valued relations. Given a transitive universe of sets <span class="math-container">$U$</span> (which is a set) and any <span class="math-container">$I \in U$</span>, we have <span class="math-container">$I \subseteq U$</span>. Therefore, maps <span class="math-container">$I \to U$</span> where <span class="math-container">$I \in U$</span> are just partial maps <span class="math-container">$U \rightharpoonup U$</span>, so they form a domain.</p>
<p>If we want to use a domain-theoretic argument to establish that a semantic model has inductive-recursive (IR) types, as sketched by Neel, then <em>the model</em> has to contain a universe that plays the role of <span class="math-container">$U$</span> above. But the type theory being modeled need not have a universe. I believe this is where some of the confusion might be coming from.</p>
<p>A type theory with inductive-recursive types but without a universe carries a lot less punch than one with an additional universe. For instance, consider MLTT (something like <span class="math-container">$\Pi$</span>, <span class="math-container">$\Sigma$</span>, <span class="math-container">$\mathrm{Id}$</span>, <span class="math-container">$0$</span>, <span class="math-container">$1$</span>, <span class="math-container">$+$</span>, <span class="math-container">$\mathbb{N}$</span>). It is modeled by <span class="math-container">$V_\kappa$</span> where <span class="math-container">$\kappa$</span> is strongly inaccessible. If we take <span class="math-container">$\kappa$</span> to be the least strongly inaccessible cardinal, then <span class="math-container">$V_\kappa$</span> contains no inaccessibles, so no MLTT universes. By the above arguments such <span class="math-container">$V_\kappa$</span> still models inductive-recursive types. The conclusion is that IR types alone do not beget a universe.</p>
<p>But now consider MLTT with a universe <span class="math-container">$U_0$</span> and IR types. The IR types allow us to define an inductively generated type of codes (a universe) and a decoding function from codes to types, closed under any operations that are already known to exist, and in particular <span class="math-container">$\Pi$</span> and <span class="math-container">$\Sigma$</span>.</p>
<p>So we can construct a universe <span class="math-container">$U_1$</span> which contains <span class="math-container">$U_0$</span> (all universes in this discussion are also closed under <span class="math-container">$\mathbb{N}$</span>, <span class="math-container">$\Sigma$</span> and <span class="math-container">$\Pi$</span>). And then we can construct <span class="math-container">$U_2$</span> which contains <span class="math-container">$U_1$</span>, and so on.</p>
<p>More generally, given any type <span class="math-container">$A$</span>, we may construct a universe <span class="math-container">$\mathsf{Univ}(A)$</span> which contains <span class="math-container">$A$</span>. Then we may define a family <span class="math-container">$n : \mathbb{N} \vdash U(n) \; \mathsf{type}$</span> by <span class="math-container">$U_{n+1} = \mathsf{Univ}(U_n)$</span>. So we have a hierarchy of universes, indexed <em>internally</em> by <span class="math-container">$\mathbb{N}$</span>.</p>
<p>But that's nothing. With a slight improvement, we may construct a universe <span class="math-container">$\mathsf{Univ}(I, A)$</span> which contains any type family <span class="math-container">$i : I \vdash A(i) \, \mathsf{type}$</span>. This allows us to generate a universe above any sequence of universes, so we have uncountably many universes.</p>
<p>But that is nothing. We may construct a universe <span class="math-container">$\mathcal{U}$</span> which is closed under <span class="math-container">$\mathsf{Univ}$</span>, i.e., given any <span class="math-container">$A : I \to \mathcal{U}$</span>, there will be a universe <span class="math-container">$\mathsf{Univ}(I, A)$</span> in <span class="math-container">$\mathcal{U}$</span> which exceeds <span class="math-container">$A$</span>. So not only does <span class="math-container">$\mathcal{U}$</span> contain very many universes, they are also unbounded.</p>
<p>I recommend reading Eric Palmgren's <a href="http://www2.math.uu.se/%7Epalmgren/universe.pdf" rel="nofollow noreferrer">On universes in type theory</a> and Anton Setzer's <a href="https://doi.org/10.1007/s001530050140" rel="nofollow noreferrer">Extending Martin-Löf Type Theory by one Mahlo-universe</a>.</p>

CC BY-SA 4.0
2022-01-25T13:34:00.637Z
Hello, this does indeed address some but not all of my confusion, since one can seemingly ask for 2 inaccessible cardinals such that $V \in U$ forms an internal universe. If we have IR for types which are $U$-small through Neel's construction, we can then kick off the universe hierarchy with $V$ and obtain a sequence of universes again. It seems like we must require some additional properties of $U$ for this to be sensible, right?
daniel gratzer
CC BY-SA 4.0
2022-01-25T13:40:36.240Z
Also, I forgot to write this in my first comment: thank you for the response and references :)
daniel gratzer
CC BY-SA 4.0
2022-01-25T14:19:01.603Z
This is very interesting, but I do not think it addresses the question at hand. I think a good first step would be for someone to explain why they believe that IR codes in the sense of Dybjer and Setzer are the same things as monotone maps in the domain of IR systems. Once that is explained, I think we will be able to narrow down an answer to this question.
Jonathan Sterling
CC BY-SA 4.0
2022-01-25T16:47:07.557Z
I'm also not exactly clear on what sort of I-R definitions are being modeled. Does the domain construction only model "small" I-R, which is no stronger than more plain inductive types? I admittedly usually forget to think about that, because the "large" version is what people are wondering about. The "IR systems" naively look like the "large" version (to me), though. And one of the reasons for inventing the "large" version is that the MLTT universe is just another special case, and a theory can't have such I-R definitions and not have a universe. It can only lack an internal Mahlo universe.
Dan Doel
CC BY-SA 4.0
2022-01-25T17:51:29.110Z
Here is something else I don't quite understand. I see how you can think of an I-R system as a partial map. I think the set of all partial maps that are the identity on $I \in U$ is directed. Presumably the join of this directed set is the total identity on $U$. This is fine for the domain of partial maps, but how does the total function decompose into an I-R system? It seems like it would require $U \in U$. So, is it not the case that not all partial maps are given by an I-R system?
Dan Doel
CC BY-SA 4.0
2022-01-26T08:09:47.060Z
I am definitely talking about the "large" version, if by that you mean that the "recursive" in "I-R" is allowed to map into types.
Andrej Bauer
CC BY-SA 4.0
2022-01-26T08:12:11.043Z
@JonathanSterling: Do you think one should say more than "observe that an I-R schema defines a monotone map on I-R systems, as defined in Neel's answer"?
Andrej Bauer
CC BY-SA 4.0
2022-01-26T10:44:55.067Z
I think you should say a little more --- there seems to be a pretty big distance between this setting where you have access to the material subset relation and monotone functions, and the logic of a topos where there is no subset relation between arbitrary objects. So while I grant that it may be possible to turn what you and Neel are suggesting into a topos-valid proof, it is currently not type-checking for me.
Jonathan Sterling
CC BY-SA 4.0
2022-01-25T13:05:05.093Z
2022-01-25T13:29:05.960Z
2022-01-25T13:29:05.960Z
Andrej Bauer
<p>It is well-known that various flavors of induction-recursion are consistent*. Typically, this is proven by showing that the standard model of type theory in sets can be extended to include induction-recursion. I'm interested in what is known about modeling induction-recursion in settings other than <span class="math-container">$\mathbf{Set}$</span>.</p>
<p>To be more concrete: is it known whether every Grothendieck topos models induction-recursion? I'm perfectly happy to ignore questions of strictness in these models, so that this can be rephrased as asking whether the strictly positive functors one uses to model IR admit initial algebras in all Grothendieck topoi.</p>
<p>If it helps to clarify this question: in recent work Fiore, Pitts, and Steenkamp 2021 have shown that it is possible to construct QWI types in a wide class of models, including all Grothendieck topoi. I'm hoping for a similar result applied to some form of induction-recursion.</p>
<p>In my (cursory) literature survey, it appears that this question is nearly addressed by Ghani, Malatesta, Nordval Forsberg, and Setzer 2013. They provide a model of their &quot;fibred data types&quot; (which subsume IR) in a split fibration satisfying several conditions regarding presentable objects. They do not, however, make any comment on whether these assumptions are satisfied in a category other than <span class="math-container">$\mathbf{Set}$</span>, and their assumption of working only with the morphisms defining a splitting makes it difficult to compute whether their assumptions are validated for the (splitting, I suppose) of a the codomain fibration of a Grothendieck topos. It also appears that this question is settled for <em>small</em> induction-recursion, which Malatesta, Altenkirch, Ghani, Hancock, and McBride 2013 seem to have reduced to indexed inductive types, which can be modeled in a Grothendieck topos.</p>
<p>(*) Assuming a suitable large cardinal axiom I'm accepting without comment for the remainder of this question.</p>
<p>Bibliography:</p>
<ul>
<li><p>N. Ghani, L. Malatesta, F. N. Forsberg and A. Setzer, &quot;Fibred Data Types,&quot; 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013, pp. 243-252, <a href="https://doi.org/10.1109/LICS.2013.30" rel="noreferrer">https://doi.org/10.1109/LICS.2013.30</a>.</p>
</li>
<li><p>Hancock, P., McBride, C., Ghani, N., Malatesta, L., &amp; Altenkirch, T. (2013). Small induction recursion. Typed Lambda Calculus and Applications: 11th International Conference. <a href="https://doi.org/10.1007/978-3-642-38946-7_13" rel="noreferrer">https://doi.org/10.1007/978-3-642-38946-7_13</a></p>
</li>
<li><p>Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp. Quotients, inductive types, and quotient inductive types. Available on arxiv <a href="https://arxiv.org/abs/2101.02994" rel="noreferrer">https://arxiv.org/abs/2101.02994</a></p>
</li>
</ul>

CC BY-SA 4.0
2022-01-24T12:44:29.753Z
Please can you include paper titles (and ideally also links) rather than just author names and years when referencing papers?
varkor
CC BY-SA 4.0
2022-01-24T12:50:25.260Z
@varkor I have added more precise references to the question.
daniel gratzer
<type-theory><ct.category-theory><denotational-semantics>
Induction-recursion in models other than $\mathbf{Set}$
daniel gratzer
# Induction-recursion in models other than $\mathbf{Set}$

(Asked by: username_0 on 2022-01-24)

It is well-known that various flavors of induction-recursion are consistent\*. Typically, this is proven by showing that the standard model of type theory in sets can be extended to include induction-recursion. I'm interested in what is known about modeling induction-recursion in settings other than $\mathbf{Set}$.

To be more concrete: is it known whether every Grothendieck topos models induction-recursion? I'm perfectly happy to ignore questions of strictness in these models, so that this can be rephrased as asking whether the strictly positive functors one uses to model IR admit initial algebras in all Grothendieck topoi.

If it helps to clarify this question: in recent work Fiore, Pitts, and Steenkamp 2021 have shown that it is possible to construct QWI types in a wide class of models, including all Grothendieck topoi. I'm hoping for a similar result applied to some form of induction-recursion.

In my (cursory) literature survey, it appears that this question is nearly addressed by Ghani, Malatesta, Nordval Forsberg, and Setzer 2013. They provide a model of their "fibred data types" (which subsume IR) in a split fibration satisfying several conditions regarding presentable objects. They do not, however, make any comment on whether these assumptions are satisfied in a category other than $\mathbf{Set}$, and their assumption of working only with the morphisms defining a splitting makes it difficult to compute whether their assumptions are validated for the (splitting, I suppose) of a the codomain fibration of a Grothendieck topos. It also appears that this question is settled for *small* induction-recursion, which Malatesta, Altenkirch, Ghani, Hancock, and McBride 2013 seem to have reduced to indexed inductive types, which can be modeled in a Grothendieck topos.

(\*) Assuming a suitable large cardinal axiom I'm accepting without comment for the remainder of this question.

Bibliography:

* N. Ghani, L. Malatesta, F. N. Forsberg and A. Setzer, "Fibred Data Types," 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013, pp. 243-252, <https://doi.org/10.1109/LICS.2013.30>.
* Hancock, P., McBride, C., Ghani, N., Malatesta, L., & Altenkirch, T. (2013). Small induction recursion. Typed Lambda Calculus and Applications: 11th International Conference. <https://doi.org/10.1007/978-3-642-38946-7_13>
* Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp. Quotients, inductive types, and quotient inductive types. Available on arxiv <https://arxiv.org/abs/2101.02994>

**Tags:** type-theory, ct.category-theory, denotational-semantics

> **Comments:**
> **username_1**: Please can you include paper titles (and ideally also links) rather than just author names and years when referencing papers?  
> **username_0**: @username_1 I have added more precise references to the question.  

---

## 2 answers

### Answer by username_2 on 2022-01-24. Score: 3

1. Define an **IR system** be a family $U \in \mathrm{Set}$ and a function $\phi \in U \to \mathrm{Set}$.

   IR systems form a domain. The least element is $\bot = (\emptyset, !)$. The order relationship $(U, \phi) \leq (U', \phi')$ holds when $U \subseteq U'$, and for all $c \in U$, we have $\phi(c) = \phi'(c)$. (Limits are computed in the obvious way, by union.)
2. **Pataraia's Theorem**: Suppose $D$ is a domain, and $f : D \to D$ is a monotone
   function on $D$. Then $f$ has a least fixed point.

So for any monotone function on IR systems (i.e., basically any sensible inductive-recursive definition), it has a least fixed point.

Pataraia's theorem is provable in the internal language of any topos, since it is a proof in intuitionistic bounded ZF. (I reproduce the proof below.)

However, the definition of IR system uses a function $\phi : U \to \mathrm{Set}$, so we need a well-behaved universe of small sets to interpret this.

In his 2004 paper, [*Universes in Toposes*](https://www2.mathematik.tu-darmstadt.de/%7Estreicher/NOTES/UniTop.pdf), Thomas Streicher says that not all topoi have such a universe (in particular, the free topos doesn't). but he says that Set, realisability models, and Grothendieck topoi all have universes. (Fair warning: I've read this paper, but haven't tried to reproduce his proofs!)

---

**Proof of Pataraia's theorem**

Define an $f$-inflationary set to be be a set $U \subseteq D$ which
contains $\bot$, is closed under $f$ (i.e., if $x \in U$, then $f(x)
\in S$), and contains joins of directed sets in $U$.

Let $S$ be the intersection of all $f$-inflationary sets (i.e, the
least $f$-inflationary set). Now, note that:

1. $S$ itself a domain, since $\bot \in S$, and it contains directed joins by definition.
2. The restriction $f : S \to S$ is inflationary (i.e., for all
   $x \in S$, $x \leq f(x)$).

Next, let $E(S)$ to be the set of inflationary, monotone maps $S \to S$.

Now, $E(S)$ is a domain. Its least element is the identity function
$\mathit{id}\_S$, and the order and joins are computed pointwise.

$E(S)$ is also a directed set itself. Suppose you have $f$ and $g$ in
$E(S)$. Then, it is clear that $f \circ g \in E(S)$, and because both
$f$ and $g$ are increasing, $f \leq f \circ g$ and $g \leq f \circ g$.

Hence, the lub (call it $m$) of $E(C)$ is itself an element of $E(C)$.
So $m$ is itself an inflationary, monotone map. Since $f$ is an
element of $E(C)$, we know that $f \circ m \in E(C)$, and so $f \circ
m \leq m$. Since $f$ is inflationary, we also have that $m \leq f\circ
m$.

So for every element $s \in S$, we have $f(m(s)) = m(s)$.

So $m(\bot)$ is the least fixed point of $f$.

> **Comments:**
> **username_0**: Hi Neel! Indeed, I was trying to sketch this argument since our discussion but got a bit turned around. Some of this is linguistic (categorical universes aren't exactly like sets internally, so they don't automatically have subset relation assigned to them and the obvious choice of requiring a monic `el(A) >-> el(B)` is sensible, but doesn't make them a partial order, merely a pre-order, etc). Some of my confusion was a bit more foundational though...  
> **username_0**: [sorry, character limit]...  because the literature seems to claim that IR is equivalent to a very large large cardinal axiom (a Mahlo cardinal), but having a universe in a topos is "just" equivalent to a strongly inaccessible cardinal! Is the difference being made up for in the subobject classifier and does this in turn mean that IR is actually quite weak in classical ZFC, for instance?  
> **username_0**: Let me try and drag this out further. Let's say I have a universe in a topos which is big enough to classify the subobject classifier. This is true in $\mathbf{Set}$ if I have just one Grothendieck universe. I then can use IR to build a hierarchy of universes, each containing the subobject classifier. But now I seem to have gone from 1 universe + universe of propositions to a hierarchy + a universe of propositions which shouldn't be possible, should it?  
> **username_3**: Are IR systems actually a domain? Domains need to have joins of _all_ directed sets, but maybe size limitations on the sort of unions a universe is closed under cause it to not quite be a domain? Something along those lines seem like a point where the proof might subtly fail.  
> **username_4**: Hi Neel, I am nearly certain that there must be some mistake somewhere. ZFC+U is consistent with "there does not exist a mahlo cardinal", so if this argument sufficed to show exhibit initial algebras for all IR functors, it would also prove that ZFC is inconsistent with one Grothendieck universe.  
> **username_2**: @DanDoel I think I have just about convinced myself that you are right. For each small set $x$, we can define an IR system $(\{x\}, x \mapsto \mathbb{N})$. Then the code part of the join of all these things will be the non-small set of all small sets, which is not an IR system per my definition. For this to work you have to bound the cardinality of the $U$'s so that their union is itself small.  
> **username_3**: [Here](https://hub.darcs.net/dolio/agda-share/browse/IRDomain.agda) is a formalization of the argument. I was going to also formalize the argument that a system corresponding to the identity partial function is a problem, but I couldn't think of a simple way of formalizing the correspondence (it's not very 'structural').  

---

### Answer by username_5 on 2022-01-25. Score: 0

This is mostly a reaction to the questions posed in the comments to Neel's answer.

Partial maps $A \rightharpoonup B$ between sets $A$ and $B$ form a domain, where we view such maps as single-valued relations. Given a transitive universe of sets $U$ (which is a set) and any $I \in U$, we have $I \subseteq U$. Therefore, maps $I \to U$ where $I \in U$ are just partial maps $U \rightharpoonup U$, so they form a domain.

If we want to use a domain-theoretic argument to establish that a semantic model has inductive-recursive (IR) types, as sketched by Neel, then *the model* has to contain a universe that plays the role of $U$ above. But the type theory being modeled need not have a universe. I believe this is where some of the confusion might be coming from.

A type theory with inductive-recursive types but without a universe carries a lot less punch than one with an additional universe. For instance, consider MLTT (something like $\Pi$, $\Sigma$, $\mathrm{Id}$, $0$, $1$, $+$, $\mathbb{N}$). It is modeled by $V\_\kappa$ where $\kappa$ is strongly inaccessible. If we take $\kappa$ to be the least strongly inaccessible cardinal, then $V\_\kappa$ contains no inaccessibles, so no MLTT universes. By the above arguments such $V\_\kappa$ still models inductive-recursive types. The conclusion is that IR types alone do not beget a universe.

But now consider MLTT with a universe $U\_0$ and IR types. The IR types allow us to define an inductively generated type of codes (a universe) and a decoding function from codes to types, closed under any operations that are already known to exist, and in particular $\Pi$ and $\Sigma$.

So we can construct a universe $U\_1$ which contains $U\_0$ (all universes in this discussion are also closed under $\mathbb{N}$, $\Sigma$ and $\Pi$). And then we can construct $U\_2$ which contains $U\_1$, and so on.

More generally, given any type $A$, we may construct a universe $\mathsf{Univ}(A)$ which contains $A$. Then we may define a family $n : \mathbb{N} \vdash U(n) \; \mathsf{type}$ by $U\_{n+1} = \mathsf{Univ}(U\_n)$. So we have a hierarchy of universes, indexed *internally* by $\mathbb{N}$.

But that's nothing. With a slight improvement, we may construct a universe $\mathsf{Univ}(I, A)$ which contains any type family $i : I \vdash A(i) \, \mathsf{type}$. This allows us to generate a universe above any sequence of universes, so we have uncountably many universes.

But that is nothing. We may construct a universe $\mathcal{U}$ which is closed under $\mathsf{Univ}$, i.e., given any $A : I \to \mathcal{U}$, there will be a universe $\mathsf{Univ}(I, A)$ in $\mathcal{U}$ which exceeds $A$. So not only does $\mathcal{U}$ contain very many universes, they are also unbounded.

I recommend reading Eric Palmgren's [On universes in type theory](http://www2.math.uu.se/%7Epalmgren/universe.pdf) and Anton Setzer's [Extending Martin-Löf Type Theory by one Mahlo-universe](https://doi.org/10.1007/s001530050140).

> **Comments:**
> **username_0**: Hello, this does indeed address some but not all of my confusion, since one can seemingly ask for 2 inaccessible cardinals such that $V \in U$ forms an internal universe. If we have IR for types which are $U$-small through Neel's construction, we can then kick off the universe hierarchy with $V$ and obtain a sequence of universes again. It seems like we must require some additional properties of $U$ for this to be sensible, right?  
> **username_0**: Also, I forgot to write this in my first comment: thank you for the response and references :)  
> **username_4**: This is very interesting, but I do not think it addresses the question at hand. I think a good first step would be for someone to explain why they believe that IR codes in the sense of Dybjer and Setzer are the same things as monotone maps in the domain of IR systems. Once that is explained, I think we will be able to narrow down an answer to this question.  
> **username_3**: I'm also not exactly clear on what sort of I-R definitions are being modeled. Does the domain construction only model "small" I-R, which is no stronger than more plain inductive types? I admittedly usually forget to think about that, because the "large" version is what people are wondering about. The "IR systems" naively look like the "large" version (to me), though. And one of the reasons for inventing the "large" version is that the MLTT universe is just another special case, and a theory can't have such I-R definitions and not have a universe. It can only lack an internal Mahlo universe.  
> **username_3**: Here is something else I don't quite understand. I see how you can think of an I-R system as a partial map. I think the set of all partial maps that are the identity on $I \in U$ is directed. Presumably the join of this directed set is the total identity on $U$. This is fine for the domain of partial maps, but how does the total function decompose into an I-R system? It seems like it would require $U \in U$. So, is it not the case that not all partial maps are given by an I-R system?  
> **username_5**: I am definitely talking about the "large" version, if by that you mean that the "recursive" in "I-R" is allowed to map into types.  
> **username_5**: @JonathanSterling: Do you think one should say more than "observe that an I-R schema defines a monotone map on I-R systems, as defined in Neel's answer"?  
> **username_4**: I think you should say a little more --- there seems to be a pretty big distance between this setting where you have access to the material subset relation and monotone functions, and the logic of a topos where there is no subset relation between arbitrary objects. So while I grant that it may be possible to turn what you and Neel are suggesting into a topos-valid proof, it is currently not type-checking for me.  

---

