Mobiles as a Quotient-Inductive Type via Plump Ordinals

Abstract

This note describes a construction of infinitary mobiles as a quotient-inductive type. The construction proceeds in two stages. First, we give a setoid-based description in terms of a transfinite diagram indexed by a plump tree ordinal $(T_I,\le )$. Second, we show that the same construction can be carried out directly in the category Set, assuming the availability of non-recursive quotients or colimit higher inductive types.

The key property of the index order $T_I$ is that it possesses a definable supremum: every family of elements indexed by $I$ has a canonical upper bound. This avoids the need for WISC (the Weakly Initial Set of Covers), which is typically required to ensure that polynomial functors preserve colimits in exact completions. Our construction is an instance where these general-purpose axioms are unnecessary.

Raw infinitary trees and plumpness

Fix a set $I$. Define the W Type of infinitary $I$-branching trees:

$\mathsf{leaf}:T_I,\mathsf{node}:(I\to T_I)\to T_I.$

Define the strict plump order $<$ on $T_I$ inductively:

$u<\mathsf{node}(f)\text{if}u\le f(i)\text{ for some }i.$

Here $\le$ is the reflexive closure of $<$. Plumpness ensures that for any $f:I\to T_I$, the tree $t^{\ast }:=\mathsf{node}(f)$ is an upper bound for all $f(i)$:

$f(i)<t^{\ast }\forall i.$

Setoid construction of mobiles

Stage sets

For each $t:T_I$, define

$S(t):=\{u:T_I\mid u<t\}.$

Define an equivalence relation $\approx$ on $S(t)$ by the following generators:

• $\mathsf{leaf}\approx \mathsf{leaf}$
• if $\forall i,f(i)\approx g(i)$ then $\mathsf{node}(f)\approx \mathsf{node}(g)$
• for any bijection $\pi :I\cong I$, if $\forall i,f(i)\approx g(\pi (i))$ then both $\mathsf{node}(f)\approx \mathsf{node}(g)$ and $\mathsf{node}(g)\approx \mathsf{node}(f)$

Let $P(t)$ be the setoid whose carrier is $S(t)$ and whose relation is $\approx$.

The diagram $P$

If $p:t\le u$, then $S(t)\subseteq S(u)$, so we obtain a setoid morphism $P(p):P(t)\to P(u)$ by inclusion. This yields a diagram

$P:(T_I,\le )⟶\mathrm{Setoid}.$

The setoid colimit

Define $\mathrm{colim}P$ as the quotient of the disjoint union ${\sum }_{t:T_I}|P(t)|$ by the equivalence generated by:

$(t,x)\sim (u,P(p)(x))\text{for all }p:t\le u.$

This gives a setoid $(|\mathrm{colim}P|,\sim )$ with injections

${\iota }_t:P(t)⟶\mathrm{colim}P.$

The quotient-polynomial functor

Define an endofunctor on setoids:

${\tilde{F}}_I(X,{\approx }_X):=(1+(I\to X))/{\approx }_F,$

where ${\approx }_F$ is the smallest equivalence relation generated by:

$\mathsf{Leaf}{\approx }_F\mathsf{Leaf},$

$\mathsf{Node}(f){\approx }_F\mathsf{Node}(g)\text{if}\forall i,f(i){\approx }_{X}g(i),$

$\mathsf{Node}(f){\approx }_F\mathsf{Node}(g)\text{if}\exists \pi :I\cong I,\forall i,f(i){\approx }_{X}g(\pi (i)).$

Cocontinuity

A crucial lemma is that for any $g:I\to \mathrm{colim}P$, if $g(i)$ is represented by $(t_i,x_i)$ then the definable supremum

$t^{\ast }:=\mathsf{node}(i\mapsto t_i)$

satisfies $t_i\le t^{\ast }$, hence

$g={\iota }_{t^{\ast }}\circ h$

for the unique $h:I\to P(t^{\ast })$ defined by $h(i):=P(t_i\le t^{\ast })(x_i)$. This supplies the factorisation needed to prove that ${\tilde{F}}_I$ preserves this colimit.

Constructing Mobiles Directly in Set

In this section we reinterpret the construction internally in Set, using a colimit higher inductive type. No use of WISC is required because the index order $(T_I,\le )$ has a definable supremum.

Explicit colimit constructors

Define the colimit as a Higher Inductive Type $M_I$ with constructors:

Points:

$\mathsf{inc}(t,x):M_I(t:T_I,x:P(t)).$

Paths:

$\mathsf{glue}(p,x):\mathsf{inc}(t,x)=\mathsf{inc}(u,P(p)(x))(p:t\le u).$

No further constructors are required.

The functor ${\tilde{F}}_I$ on Set

Define

${\tilde{F}}_I(X):=\left(1+(I\to X)\right)/\approx ,$

where $\approx$ is the same permutation-generated relation as in the setoid case.

Cocontinuity in Set

Given $g:I\to M_I$, write $g(i)=\mathsf{inc}(t_i,x_i)$. Define $t^{\ast }:=\mathsf{node}(i\mapsto t_i)$ and

$h(i):=P(t_i\le t^{\ast })(x_i).$

Then

$g(i)=\mathsf{inc}(t^{\ast },h(i))$

up to paths generated by $\mathsf{glue}$. This provides the factor needed for the $\psi$ map of the cocontinuity equivalence.

The initial algebra

Cocontinuity yields an isomorphism

${\tilde{F}}_I(M_I)\cong \mathrm{Colim}({\tilde{F}}_I\circ P),$

from which we obtain a structure map

${\mathsf{mob}}_I:{\tilde{F}}_I(M_I)\to M_I.$

By transfinite induction along $T_I$ and the colimit universal property, one obtains a unique algebra morphism into any other ${\tilde{F}}_I$-algebra. Hence:

Theorem. $M_I$ is the Initial Algebra for ${\tilde{F}}_I$.

Remarks on WISC

In general, proving that a polynomial or quotient-polynomial functor preserves colimits in a quotient completion requires a principle such as WISC to factor arbitrary maps through a small family of covers. In this specific case, the definable supremum provided by the plump order $(T_I,\le )$ replaces the need for any choice principle.