Effective Kan Fibrations for W-Types in Homotopy Type Theory

Homotopy Type Theory (HoTT) started with the homotopy-theoretic interpretation of Martin-Löf’s dependent type theory and the discovery of the univalence axiom by Voevodsky in the 2000s [11] [12]. Awodey and Warren, and independently Voevodsky, provided this homotopy interpretation. A certain form of Martin-Löf type theory can be modeled in any Quillen model category [1], giving HoTT a semantics with topological intuition. The category of simplicial sets, one of the most significant model categories, models types as Kan complexes and dependent types as Kan fibrations, as proposed by Voevodsky.

Kan fibrations, a key construct in this model, possess a lifting property analogous to the homotopy lifting property in classical homotopy theory. However, the initial Kan fibration model is non-constructive, as closure under pushforward of Kan fibrations is unprovable [2].

To develop constructive models, cubical sets were proposed as an alternative to simplicial sets. Nevertheless, the original Kan fibration concept is still appealing, and there have been endeavors to create a constructive version that maintains Voevodsky’s ideas. Gambino and Sattler proposed a model treating Kan fibrations as structure rather than property [6]. Then, to overcome difficulties in this approach, van den Berg and Faber introduced effective Kan fibrations [2], which is the primary focus of our paper.

Verification of effective Kan fibrations modeling HoTT includes modeling all type formers, such as $\mathrm{\Pi }$-types, and a primary focus of this thesis is W-types, which represent well-founded trees (e.g., natural numbers) introduced by Martin-Löf in [10]. W-types, already modeled by classical HoTT semantics using Kan fibrations [3], are examined here using effective Kan fibrations.

Prior research regarding this concept includes [5] and [7]. The latter defined a special case of effective Kan fibrations, called symmetric effective Kan fibrations. The primary difference between effective Kan fibrations and symmetric effective Kan fibrations lies in the fact that, except for certain exceptions, each horn problem in effective Kan fibrations has two solutions – positive and negative – whereas this distinction does not exist in symmetric effective Kan fibrations. This paper focuses on effective Kan fibrations and employs a slightly modified version of the framework introduced in [7] to incorporate the distinction between positive and negative solutions.

As will be mentioned, constructing W-types categorically involves transfinite induction. To ensure the entire argument is fully constructive, we must deal with this constructively, which is currently an open problem.

The first section introduces preliminary information about simplicial sets, providing essential foundational knowledge for the subsequent sections.

Then, based on the paper [3] on W-types in HoTT in the classical setting, we will extend this study using a constructive approach. We define the categories of effective Kan fibrations and their variants. This categorical framework is crucial for describing W-types and M-types as certain kinds of colimits and limits, respectively.

Next, we explore whether effective Kan fibrations can model W-types and M-types by examining the existence and behavior of filtered colimits and limits in these categories. We then explain how W-types are generated by polynomial functors, and investigate the role of these functors as maps in the categorical structures defined in previous sections.

Finally, we proceed to the main theorem: Effective Kan fibrations can indeed model W-types and their variants, providing a comprehensive conclusion to the theoretical framework developed.

Additionally, for future work, to explore potential applications of W-types in constructive mathematics, we will examine their role in defining quotients and discuss related challenges. Specifically, we address issues involving epimorphisms by introducing additional structures on effective Kan fibrations. A potential goal of this approach is to show that such structures could enable effective Kan complexes and fibrations to model quotient types and quotient maps, respectively, in a constructive framework.

For each $n\ge 0$, there are two important types of morphisms in $\mathrm{\Delta }$. An injection $d_i:[n-1]\to [n]$ that omits the $i$-th element is called the $i$-th face map. A surjection $s_i:[n+1]\to [n]$ that maps two distinct elements to $i$ is called the $i$-th degeneracy map. Specifically,

These maps satisfy the simplicial identities:

$d_j\circ d_k=d_{k+1}\circ d_j$ (if $k\ge j$), and $s_j\circ s_k=s_k\circ s_{j+1}$ (if $j\ge k$).

Given a simplicial set $X$, we write $X_n:=X([n])$, making $X$ a graded set ${\{X_n\}}_{n\in \mathbb{N}}$. Since $X$ is contravariant, the face maps and degeneracy maps induce actions $X(d_i):X_n\to X_{n-1}$ and $X(s_i):X_n\to X_{n+1}$, respectively. For any locally small category $𝒞$ and $C\in \text{ob}(𝒞)$, the Yoneda lemma identifies the natural bijection ${\mathrm{Hom}}_{{\text{Set}}^{{𝒞}^{\text{op}}}}(y_C,F)\cong FC$ for every presheaf $F$ with the representable presheaf $y_C={\mathrm{Hom}}_{𝒞}(-,C)$. Setting $𝒞=\mathrm{\Delta }$, we have:

A face map $d_k\in {\mathrm{Hom}}_{\mathrm{\Delta }}([n-1],[n])$. This corresponds to a face map $d_k:{\mathrm{\Delta }}^{n-1}\to {\mathrm{\Delta }}^n$ in sSet. Similarly, we have degeneracy maps in sSet.

By the density theorem, every presheaf is a colimit of representable presheaves. That is, a horn ${\mathrm{\Lambda }}_m^n$ is a colimit of standard simplices. This is expressed as follows [8]:

Besides this lemma, we will also see another perspective of constructing horns in the next section. The following lemma will be used frequently, so we state it here for reference. The proof follows from the universal property of the coequalizer and coproduct in Lemma 6.

Now, let us see an alternative construction of a horn described in [7].

Notice that except for the edge cases ($m=0$ or $m=n+1$), there are two ways to obtain ${\mathrm{\Lambda }}_m^{n+1}$, since two pairs $(i,ϵ)=(m-1,0)$ and $(m,1)$ satisfy $i+1-ϵ=m$ for . At the edge cases, however, only one pair satisfies the condition: $(i,ϵ)=(0,1)$ when $m=0$ and $(i,ϵ)=(n,0)$ when $m=n+1$. Thus ${\mathrm{\Lambda }}_m^{n+1}$ for is created by $d_{m-1}$ (when $ϵ=0$) or $d_{m+1}$ (when $ϵ=1$) in (1). We call a horn negative if $ϵ=0$ and positive if $ϵ=1$, and denote it by $({\mathrm{\Lambda }}_m^{n+1},\pm )$. Note that at the edges, $({\mathrm{\Lambda }}_0^{n+1},+)$ and $({\mathrm{\Lambda }}_{n+1}^{n+1},-)$ do not exist.

As mentioned in the introduction, this paper uses a framework from [7], which is described below, with a modification to distinguish between positive and negative solutions discussed above.

When $Y=\{\ast \}$, the one-point simplicial set, the lower triangle is trivial and $X$ is called an effective Kan complex.

The $\pm$ distinction is important for bookkeeping since mere existence of a lift is not sufficient anymore in the effective setting. However, for simplicity, we will mostly drop $+$ and $-$ signs from horns throughout the rest of this paper.

By a slight abuse of notation, we sometimes refer to $X$ in the pair $(X,{\mathrm{𝗅𝗂𝖿𝗍}}_X)$ simply as an effective Kan complex, and we say that $X$ is in $\mathrm{𝐄𝐟𝐟𝐊𝐚𝐧𝐂𝐩𝐥𝐱}$. Similarly, the same convention applies in the case of fibrations.

Note that the classical Kan fibrations are maps in $\mathrm{𝐬𝐒𝐞𝐭}$. This $\mathrm{𝐄𝐟𝐟𝐊𝐚𝐧𝐅𝐢𝐛}$ is further endowed with additional structures.

As mentioned in Remark12, we just regard the objects in $\mathrm{𝐄𝐟𝐟𝐊𝐚𝐧𝐂𝐩𝐥𝐱}$ as $(X,{\mathrm{𝗅𝗂𝖿𝗍}}_X)$ instead of $({!}_X,{\mathrm{𝗅𝗂𝖿𝗍}}_{{!}_X})$.

In this section, we will examine filtered colimits and limits in the categories in the previous section, as they play important roles in the construction of W-types and the variants later. Recall that a filtered diagram $F:ℐ\to 𝒞$ satisfies that (1) $ℐ$ has at least one object, (2) for each pair $i,j\in ℐ$, there is $k\in ℐ$ with a pair of morphisms $i\to k$ and $j\to k$ of $ℐ$, (3) for each pair $i,j\in ℐ$ and each pair $a,b:i\to j$, there is a morphism $c:j\to k$ of $ℐ$ such that $F(c\circ a)=F(c\circ b)$ in $𝒞$. And a filtered colimit is the colimit of a filtered diagram. Also, in Set, filtered colimits can be explicitly calculated: For a filtered diagram $F:ℐ\to \text{Set}$, we have ${\mathrm{colim}}_{i\in ℐ}{F}_i=\left({\coprod }_{i\in ℐ}{F}_i\right)/\sim$, where $x_i\sim x_j$ if and only if there exist $k\in ℐ,\phi :i\to k$ and $\psi :j\to k$ such that $F(\phi )(x_i)=F(\psi )(x_j)$, for $i,j\in I$, $x_i\in F_i$ and $x_j\in F_j$.

Applying the above calculation to hom-sets, we can obtain useful facts for sSet. First, more generally, recall that we have ${\mathrm{Hom}}_{\text{sSet}}({\mathrm{\Delta }}^n,X)\cong X_n$ by the Yoneda lemma, and colimits in sSet are computed degree-wise. Thus, every evaluation functor ${\mathrm{Hom}}_{\text{sSet}}({\mathrm{\Delta }}^n,-):\text{sSet}\to \text{Set}$ preserves all small colimits, i.e., for any small diagram $F:ℐ\to \text{sSet}$, we have ${\mathrm{Hom}}_{\text{sSet}}({\mathrm{\Delta }}^n,{\mathrm{colim}}_{i\in ℐ}{F}_i)\cong {\mathrm{colim}}_{i\in ℐ}{\mathrm{Hom}}_{\text{sSet}}({\mathrm{\Delta }}^n,F_i)$. Moreover, suppose $F$ is also filtered. A horn ${\mathrm{\Lambda }}_m^n$ is a finite colimit of standard $n$-simplices, namely finitely presentable, and thus the functor ${\mathrm{Hom}}_{\text{sSet}}({\mathrm{\Lambda }}_m^n,-):\text{sSet}\to \text{Set}$ preserves all filtered colimits. In particular, we have the following.

Let us rewrite the maps of the form $F(f)$ or $F(g)$ in the Lemma 17 as ${\phi }_{ik}$ or ${\phi }_{jk}$, respectively. Also, let us call them mediating maps.

The next proposition is an important tool for our main theorem. Similar results hold for $\mathrm{𝐄𝐟𝐟𝐊𝐚𝐧}/A$ and for $\mathrm{𝐄𝐟𝐟𝐊𝐚𝐧𝐅𝐢𝐛}$ in place of $\mathrm{𝐄𝐟𝐟𝐊𝐚𝐧𝐂𝐩𝐥𝐱}$. While the result for $\mathrm{𝐄𝐟𝐟𝐊𝐚𝐧𝐅𝐢𝐛}$ would immediately imply the results for $\mathrm{𝐄𝐟𝐟𝐊𝐚𝐧𝐂𝐩𝐥𝐱}$ and $\mathrm{𝐄𝐟𝐟𝐊𝐚𝐧}/A$, since the core idea behind the proofs of all three versions is essentially the same, we choose to focus on the simplest case for $\mathrm{𝐄𝐟𝐟𝐊𝐚𝐧𝐂𝐩𝐥𝐱}$.

We summarize the categorical formulation of W-types as described in [3]. For an endofunctor $F:ℰ\to ℰ$, an algebra is a pair $(X,\alpha )$ with $\alpha :FX\to X$, and morphisms $\phi :(X,\alpha )\to (Y,\beta )$ satisfy $\phi \circ \alpha =\beta \circ F\phi$. The initial algebra is the initial object in this category of $F$-algebras, if it exists.

In a locally cartesian closed category $ℰ$, for every $f:A\to B$, the pullback functor $f^{\ast }:ℰ/B\to ℰ/A$ has left and right adjoints, ${\mathrm{\Sigma }}_f$ and ${\mathrm{\Pi }}_f$, forming ${\mathrm{\Sigma }}_f⊣f^{\ast }⊣{\mathrm{\Pi }}_f$. In particular, for the unique morphism $!:A\to 1$, the adjunction ${\mathrm{\Sigma }}_{!}⊣{!}^{\ast }⊣{\mathrm{\Pi }}_{!}$ is written as ${\mathrm{\Sigma }}_A⊣A^{\ast }⊣{\mathrm{\Pi }}_A$. Note that $A^{\ast }$ is also written as $-\times A$.

To describe W-types in sSet, it suffices to describe them in presheaves.

Now let us introduce the first variation. As seen above, a W-type is the initial algebra for a polynomial functor. We can generalize the notion of polynomial functors as follows:

In Set, it behaves as $D_f{(X)}_c={\sum }_{a\in A_c}{\prod }_{b\in B_a}{X}_{h(b)}$. The initial algebra for $D_f$ is a subset of $W(f)$, defined by the condition that an edge labeled by $b\in B$ with source node labeled by $a\in A$ satisfies $g(a)=h(b)$. The concept of rank extends naturally from $W$-types, and this initial algebra generalizes from $\mathrm{𝐒𝐞𝐭}$ to presheaves, in particular sSet.

As a dual to a W-type, an M-type is defined as the final coalgebra of a polynomial functor associated with a morphism $f:B\to A$ in a locally cartesian closed category $ℰ$.

In both Set and sSet, this final coalgebra, denoted $M(f)$, captures both well-founded and non-well-founded trees labeled according to $f$. The construction of $M(f)$ can be understood as the limit of the following chain:

where $P_f$ is the polynomial functor associated with $f$, and $1$ denotes the terminal object. Notably, this sequence stabilizes at the ordinal $\omega$, leading to the isomorphism $M(f)\cong {lim}_{n\in \mathbb{N}}{P}_f^n(1)$. Thus, unlike certain W-types which require transfinite recursion to generate new well-founded trees, M-types do not require it.