1. Introduction
It is often said that realizability formalizes the BHK interpretation (see, e.g., Bauer, Reference Bauer and Zenil2012). The latter is an informal interpretation, inductively prescribing what counts as evidence for logical formulas (Heyting, Reference Heyting1930; Kolmogorov, Reference Kolmogorov1932; Heyting, Reference Heyting1934, Reference Heyting1956; Heyting, Reference Heyting1934):
-
• Evidence for
$\phi \land \psi$
consists of evidence for
$\phi$
and evidence for
$\psi$
. -
• Evidence for
$\phi \lor \psi$
is an identifier for either
$\phi$
or
$\psi$
together with evidence for the formula identified. -
• Evidence for
$\phi \rightarrow \psi$
is a process (or method, or function) that, when given evidence for
$\phi$
, produces evidence for
$\psi$
. -
• Evidence for
$\exists x\in A.\, \phi (x)$
consists of a representation of some object
$a\in A$
and evidence for
$\phi (a)$
. -
• Evidence for
$\forall x\in A.\, \phi (x)$
is again a process that, when given a representation of any object
$a\in A$
, produces evidence for
$\phi (a)$
.
In a realizability interpretation, formally specified realizers play the role of evidence. Moreover, informal terms like “process” are given a precise, mathematical meaning. For example, in the original realizability interpretation, Kleene’s (Reference Kleene1945) so-called “number realizability” interpretation of Heyting arithmetic, realizers are natural numbers. Processes are also natural numbers. Recall that partial computable functions may be effectively enumerated. Given a natural number
$m$
, the process
$n$
returns the result – if it is defined – of applying the partial computable function encoded by
$n$
to the argument
$m$
(often denoted either by
$\varphi _n(m)$
or by
$\{n\}(m)$
). Insofar as realizers are computational in nature, realizability interpretations unveil computational content of logical or mathematical theories.
A few decades after Kleene’s number realizability, Hyland (Reference Hyland1982) introduced the effective topos
$\mathbf{Eff}$
. This is a universe for computable mathematics: its internal logic extends number realizability. More generally, a realizability topos can be constructed over an arbitrary partial combinatory algebra (PCA);
$\mathbf{Eff}$
is the realizability topos built over the PCA
$\mathscr{K}_1$
(known as “Kleene’s first algebra”) of natural numbers and partial computable functions. The resulting realizability topos is a universe for computable mathematics, where the notion of computation is determined by the PCA.
The realizability topos
$\mathbf{RT}(\mathscr{A})$
over an arbitrary PCA
$\mathscr{A}$
boasts a number of subcategories that model powerful and expressive type theories. Each of these categories has an elementary construction directly over the PCA, independently of the realizability topos. There is the category
$\mathbf{Asm}(\mathscr{A})$
of assemblies, which is regular and locally cartesian closed. The full subcategory
$\mathbf{PAsm}(\mathscr{A}) \subseteq \mathbf{Asm}(\mathscr{A})$
spanned by the partitioned assemblies is weakly locally cartesian closed and therefore a model of type theory without function extensionality. Note that
$\mathbf{RT}(\mathscr{A})$
is exact and can be obtained as the ex/lex completion of
$\mathbf{PAsm}(\mathscr{A})$
or the ex/reg completion of
$\mathbf{Asm}(\mathscr{A})$
(Robinson and Rosolini, Reference Robinson and Rosolini1990).
Both
$\mathbf{Asm}(\mathscr{A})$
and
$\mathbf{PAsm}(\mathscr{A})$
contain an impredicative universe, that is, one closed under large products. The small (closed) types are the modest (partitioned) assemblies.
The realizability categories discussed above model some version of extensional type theory. In number realizability, any natural number realizes a true equation; thus, realizers of equations give no information beyond the fact that the equation holds. The so-called “homotopy interpretation” of type theory understands terms of the identity type
$\textsf{Id}_A(a,b)$
as paths between the points
$a$
and
$b$
in the space
$A$
(The Univalent Foundations Program, 2013). This can be reformulated as a BHK clause:
-
• Evidence for an identification of
$a,b\in A$
is a path between representations of
$a$
and
$b$
in the space representing
$A$
.
The terms “path” and “space” are meant to be understood informally, just like terms such as “process” in the usual BHK clauses. The informal interpretation obtained by adding the above clause to the usual BHK interpretation shall be called the “homotopy BHK interpretation.”
The overarching aim of this paper is to develop realizability models of intensional type theory that formalize the homotopy BHK interpretation just as the realizability models of extensional type theory discussed above formalize the usual BHK interpretation.
To this end, we shall equip Hofmann and Streicher’s (Reference Hofmann, Streicher, Sambin and Smith1998) groupoid model of type theory with a suitable notion of realizability, just as traditional realizability categories do with the set model.
Instead of constructing realizability models over PCAs, we will do so over structured “realizer” categories. This idea can be traced back to Lambek (Reference Lambek1995) and Abramsky (Reference Abramsky1995): over an arbitrary category, the former constructs a category of partial equivalence relations (PERs), while the latter constructs categories of assemblies and modest sets. Both proceed to show that the ensuing realizability categories inherit structure from the initial realizer category and in some cases even improve a weak universal property to a full one, as is a theme in realizability. Later, analyses of realizability using realizer categories were given by Birkedal (Reference Birkedal1999,2000a,b) and Robinson and Rosolini (Reference Robinson and Rosolini2001). The former constructs models of type theory in assemblies and modest sets over weakly closed partial cartesian categories (i.e., categories with a notion of partial map that are weakly cartesian closed in a suitable sense) via a tripos-theoretic approach. The latter studies necessary conditions on a realizer category for the construction of realizability models with certain type-theoretic features. Both consider when a topos may be obtained.
In order to formalize the homotopical BHK interpretation, realizers need carry non-trivial (non-discrete) homotopical structure. In the current approach, the key to attaining this is to take part of the structure of a realizer category
$\mathbf{R}$
to be an interval qua internal cogroupoid
$\mathbb{I}\in \mathbf{R}$
. The interval supplies a notion of homotopy internal to
$\mathbf{R}$
as well as a fundamental groupoid construction
$\Pi :\mathbf{R}\rightarrow \mathbf{Gpd}$
. Objects in a base groupoid
$X$
are realized by points in the fundamental groupoid of some object
$A\in \mathbf{R}$
, and isomorphisms in
$X$
are realized by paths in
$\Pi A$
. In this paper, we concentrate on partitioned groupoidal assemblies, a groupoidal analog of partitioned assemblies.
1.1 Outline
The next ( Section 1.2 ) discusses related work. Following this, Section 2.1 briefly reviews set-based realizability over combinatory algebras (CAs) (2.1.1), TCAs (2.1.2), and categories (2.1.3). Section 2.2 discusses realizer categories for groupoidal realizability. These come equipped with an interval, as described in Section 2.2.1, which facilitaties a notion of homotopy (Section 2.2.2) as well as a fundamental groupoid construction (Section 2.2.3). Untyped realizer categories (required for impredicative universes) are discussed in Section 2.2.5.
Section 3 introduces the main players: partitioned groupoidal assemblies. The category
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
of partitioned groupoidal assemblies over the realizer category
$(\mathbf{R},\mathbb{I})$
is first studied as a (2,1)-category (Section 3.1) and then as a path category (Section 3.2). Dependent products are exhibited in Section 3.2.1. Section 4 is devoted to impredicative universes of modest fibrations. Section 5 summarizes and outlines future work.
1.2 Related work
As far as we understand, the first to consider realizability semantics for intensional type theory were Hofstra and Warren (Reference Hofstra and Warren2013). They equip the syntax of 1-truncated intensional type theory with a notion of realizability allowing them to show that the syntactic groupoid associated with the type theory generated by a graph has the same homotopy type as the free groupoid on this graph.
Further work at the intersection of realizability and intensional type theory was motivated by the search for impredicative and univalent universes of (homotopically) higher types. Uemura (Reference Uemura, Dybjer, Santo and Pinto2018) gave a model with such a universe in the category of “cubical assemblies,” that is, cubical objects internal to the model of extensional type theory in
$\mathbf{Asm}(\mathscr{K}_1)$
. Another type-theoretic principle of interest is propositional resizing, which states that every proposition is equivalent to a “small” one (one living in the lowest universe). Uemura’s model does not satisfy propositional resizing, exhibiting this as a distinct form of impredicativity. Swan and Uemura (Reference Swan and Uemura2021) show that univalence is consistent with Church’s thesis (CT, all functions on the natural numbers are computable): though CT does not hold in the cubical assemblies model, there is a reflective submodel in which it does.
In contrast to cubical assemblies, van den Berg (Reference van den Berg2018
b) exhibits
$\mathbf{Eff}$
as the homotopy category of a path category in which there is an impredicative and univalent universe of propositions that does satisfy propositional resizing. A more complicated path category contains an impredicative and univalent universe of sets satisfying propositional resizing.
Angiuli et al. (Reference Angiuli, Harper, Wilson, Castagna and Gordon2017) introduce computational higher-dimensional type theory, based on a cubical generalization of Martin-Lof’s meaning explanations (Angiuli and Harper, Reference Angiuli and Harper2017). This involves a realizability – in particular, a PER – construction over a cubical programming language, which produces a model of cubical type theory. This approach has been extended to univalent (though not impredicative) universes (Angiuli et al., Reference Angiuli, Hou, Harper, Ghica and Jung2018) and higher inductive types (Cavallo, Reference Cavallo and Harper2019). The realizers here, being expressions in a cubical programming language, do carry non-trivial homotopical structure, making this approach closest in spirit to ours (though vastly different in technical detail).
Almost all of the novel results in this paper first appeared in the author’s DPhil thesis (Speight, Reference Speight2023).
2. From Combinatory Algebras to Realizer Categories
2.1 Set-based realizability
In this section, we briefly review categories of assemblies over: first, (untyped) combinatory algebras; next, typed combinatory algebras; and finally over categories with a terminal object. We show how each of these cases subsumes the previous case. Although the case of (partial) combinatory algebras is best known, it appears that categories are more easily adapted to the groupoidal setting. We put aside the matter of partiality from hereon in.
2.1.1 Combinatory algebras
A CA
$\mathscr{A}$
consists of a set
$\mathscr{A}$
and a binary “application” operation:
\begin{align*} (-)\cdot (?): \mathscr{A}\times \mathscr{A}\rightarrow \mathscr{A} \end{align*}
such that there exist elements (“combinators”)
$\textsf{k},\textsf{s}\in \mathscr{A}$
satisfying
$\textsf{k}\cdot a \cdot b = a$
and
$\textsf{s} \cdot a \cdot b \cdot c = a \cdot c \cdot (b \cdot c)$
. From now on, we adopt the convention of left associativity and may omit the application symbol.
CAs enjoy a property known as “combinatory completeness,” which, roughly speaking, allows them to mimic the
$\lambda$
-calculus (Schönfinkel, Reference Schönfinkel1924; Curry, Reference Curry1930). A polynomial over
$\mathscr{A}$
is a formal expression built from the grammar:
\begin{align*} t ::= x\in \mathscr{V} \;|\; a\in \mathscr{A} \;|\; t \cdot t \end{align*}
where
$\mathscr{V}$
is a countably infinite set of variables. Clearly, we can talk about free variables of a polynomial and substitution
$t[a/x]$
of the element
$a\in \mathscr{A}$
for the free variable
$x\in \mathscr{V}$
in the polynomial
$t$
. Moreover, closed polynomials have an obvious interpretation in
$\mathscr{A}$
. Combinatory completeness says that for every polynomial
$t$
over
$\mathscr{A}$
and every variable
$x$
, there exists a polynomial
$\lambda x.\, t$
such that
$\textsf{FV}(\lambda x.\, t) \subseteq \textsf{FV}(t) - \{x\}$
and for all
$a\in \mathscr{A}$
:
\begin{align*} (\lambda x.\, t) a = t[a/x] \end{align*}
Indeed, an example of a CA is the set of
$\lambda$
-terms up to
$\beta$
-equivalence, where application is
$\lambda$
-application,
$\textsf{k}:= \lambda x y.\, x$
and
$\textsf{s} = \lambda f g x.\, fx(gx)$
. (Kleene’s first algebra
$\mathscr{K}_1$
, mentioned in the previous section, is not a combinatory algebra but a partial combinatory algebra: the application of one element to another may not be defined (Turing machines may not halt).)
The objects of the category
$\mathbf{Asm}(\mathscr{A})$
of assemblies over the CA
$\mathscr{A}$
are pairs
$(X,\Vdash _X)$
consisting of a set
$X$
and a “realizability” relation
$\Vdash _X \subseteq \mathscr{A}\times X$
(written infix) such that
$\forall x\in X. \, \exists a\in \mathscr{A}. \, a \Vdash _X x$
. Assemblies are sometimes thought of as datatypes, whose “values” are implemented (by their realizers) in the programming language given by the CA. A morphism
$f:(X,\Vdash _X) \rightarrow (Y,\Vdash _Y)$
is a set-function
$f:X\rightarrow Y$
such that
$\exists e\in \mathscr{A}.\, \forall x\in X. \, \forall a\in \mathscr{A}. \, a\Vdash _X x \rightarrow ea \Vdash _Y f(x)$
. We say that the function
$f$
is realized by
$e$
and write
$e\Vdash f$
. Identities in
$\mathbf{Asm}(\mathscr{A})$
are identity functions, which are realized by
$\lambda x.\, x$
. Composition is also inherited from
$\mathbf{Set}$
: if
$e\Vdash f: X\rightarrow Y$
and
$e^{\prime}\Vdash g:Y \rightarrow Z$
then
$\lambda x.\, e^{\prime}(ex) \Vdash gf:X \rightarrow Z$
.
An assembly
$X$
is modest when elements are uniquely determined by any of their realizers:
$\forall x,x^{\prime}\in X. \, \forall a\in \mathscr{A}. \, a \Vdash _X x \land a \Vdash _X x^{\prime} \rightarrow x=x^{\prime}$
. An assembly
$X$
is partitioned when the relation
$\Vdash _X$
is actually a function:
\begin{align*} \left \Vert - \right \Vert _X : X \rightarrow \mathscr{A} \end{align*}
(so each element of
$X$
has exactly one realizer). Of course, an assembly
$X$
may be both modest and partitioned, in which case the function
$\left \Vert - \right \Vert _X$
is an injection. Thus, every modest partitioned assembly can be identified with a subset of
$\mathscr{A}$
; this is used in the construction of an impredicative universe of modest partitioned assemblies in
$\mathbf{PAsm}(\mathscr{A})$
.
2.1.2 Typed combinatory algebras
Typed (partial) combinatory algebras were introduced by Longley (Reference Longley1999). A typed combinatory algebra (TCA) is built over a “type system”: a non-empty set
$\mathscr{T}$
of “types” that is closed under the operation
$\rightarrow$
(which associates with the right by convention). (Normally one would also consider products, but for present purposes we need not.) A TCA
$\mathscr{A}$
over the type system
$\mathscr{T}$
is a family
\begin{align*} (\mathscr{A}_A)_{A\in \mathscr{T}} \end{align*}
of non-empty sets indexed by types, together with a family of typed application operations:
\begin{align*} (-) \cdot _{A,B} (?): \mathscr{A}_{A\rightarrow B} \times \mathscr{A}_A \rightarrow \mathscr{A}_B \end{align*}
(again we tend to omit the symbol) such that the following typed combinators are required to exist and satisfy the given equations:
\begin{align*} &\textsf{k}_{A,B} \in \mathscr{A}_{A\rightarrow B \rightarrow A} &\textsf{k}_{A,B} a b = a \\ &\textsf{s}_{A,B,C} \in \mathscr{A}_{(A \rightarrow B \rightarrow C) \rightarrow (A \rightarrow B) \rightarrow A \rightarrow C} &\textsf{s}_{A,B,C} f g a = f a (g a) \end{align*}
TCAs are combinatorially complete in a typed sense (see Bauer (Reference Bauer2022) for details).
If
$\mathscr{A}$
is a TCA, then an object of
$\mathbf{Asm}(\mathscr{A})$
is a triple
$(X,A,\Vdash _X)$
, where
$X\in \mathbf{Set}$
,
$A\in \mathscr{T}$
is the “realizer type” and
$\Vdash _X \subseteq \mathscr{A}_A \times X$
(so realizers of elements of
$X$
all have the same type) is such that
$\forall x\in X. \, \exists a\in \mathscr{A}_A. \, a \Vdash _X x$
. A morphism
$(X,A,\Vdash _X)\rightarrow (Y,B,\Vdash _Y)$
is a function
$f:X\rightarrow Y$
such that
$\exists e\in \mathscr{A}_{A\rightarrow B}.\, \forall x\in X. \, \forall a\in \mathscr{A}. \, a\Vdash _X x \rightarrow ea \Vdash _Y f(x)$
.
Any CA can be regarded as a TCA with a single type
$U=U\rightarrow U$
(in such a way that the ensuing categories of assemblies are isomorphic). Furthermore, any TCA can be equipped with a “unit” type such that the ensuing category of assemblies remains unchanged up to equivalence. That is, given any type system
$\mathscr{T}$
, we consider the augmented type system
$\mathscr{T}^1 := \mathscr{T} \cup \{ 1\}$
, where
$1\rightarrow A := A$
and
$A \rightarrow 1 := 1$
. Then we obtain the augmented TCA
$\mathscr{A}^1$
over
$\mathscr{T}_1$
by setting
$\mathscr{A}^1_1 := 1$
(the terminal set). The augmented application operation is given by:
\begin{align*} &a \cdot _{1\rightarrow A} * := a &* \cdot _{A\rightarrow 1} a := * \end{align*}
For the combinators, it suffices to specify the following (where
$A,A^{\prime}\in \mathscr{T}^1$
):
\begin{align*} &\textsf{k}_{1,A} := * &\textsf{k}_{A,1} := \lambda x.\, x \\ &\textsf{s}_{1,A,A^{\prime}} := \lambda f a.\, fa =: \textsf{s}_{A,1,A^{\prime}} &\textsf{s}_{A,A^{\prime},1} := * \end{align*}
Here, we use typed combinatorial completeness of
$\mathscr{A}$
. Checking the relevant equations is straightforward.
Proposition 1.
Let
$\mathscr{A}$
be a TCA.
$\mathbf{Asm}(\mathscr{A}) \simeq \mathbf{Asm}(\mathscr{A}^1)$
.
Proof.
$\mathbf{Asm}(\mathscr{A})$
is a full subcategory of
$\mathbf{Asm}(\mathscr{A}^1)$
. For any
$X=(X,1,\Vdash _X)\in \mathbf{Asm}(\mathscr{A}^1)$
, we define an isomorphism:
\begin{align*} f: X \rightarrow X^{\prime} := \left (X,A,\left \Vert -\right \Vert _{X^{\prime}}\right ) \end{align*}
where for all
$x\in X$
, we set
\begin{align*} \left \Vert x \right \Vert _{X^{\prime}} := a_0 \end{align*}
for an arbitrarily chosen
$a_0 \in \mathscr{A}_A$
. The function
$f:= \textsf{id}_X$
is realized by
$a_0 \in \mathscr{A}_A = \mathscr{A}_{1\rightarrow A}$
. The inverse
$f^{-1} := \textsf{id}_X$
is realized by
$*\in \mathscr{A}_1 = \mathscr{A}_{A\rightarrow 1}$
.
2.1.3 Categories
A category, like a TCA, gives rise to an a priori typed notion of realizability: the types are the objects of the category. Suppose
$\mathbf{R}$
is a category with a terminal object
$1$
. Then we have the functor:
\begin{align*} \Pi := \mathbf{R}(1,-): \mathbf{R} \rightarrow \mathbf{Set} \end{align*}
The objects of the category
$\mathbf{Asm}(\mathbf{R})$
of assemblies over the “realizer category”
$\mathbf{R}$
are triples
$(X,A,\Vdash _X)$
, where
$X\in \mathbf{Set}$
,
$A\in \mathbf{R}$
(a realizer type is now an object from the realizer category) and
$\Vdash _X \subseteq \Pi A \times X$
is such that
$\forall x\in X. \, \exists a\in \Pi A. \, a \Vdash _X x$
. A morphism
$(X,A,\Vdash _X)\rightarrow (Y,B,\Vdash _Y)$
is a function
$f:X\rightarrow Y$
such that
$\exists e:A\rightarrow B \in \mathbf{R}.\, \forall x\in X. \, \forall a\in \mathscr{A}. \, a\Vdash _X x \rightarrow \Pi (e)(a) = e\circ a \Vdash _Y f(x)$
.
Given a TCA
$\mathscr{A}$
with a unit type
$1$
(
$\mathscr{A}_1 = 1$
), we may build a category
$\mathbf{R}(\mathscr{A})$
with a terminal object. The objects of
$\mathbf{R}(\mathscr{A})$
are the types of
$\mathscr{A}$
. A morphism
$A \rightarrow B$
is a “computable” function
$k: \mathscr{A}_A \rightarrow \mathscr{A}_B$
. The function
$k$
is computable iff there exists
$e\in \mathscr{A}_{A\rightarrow B}$
representing it, that is, for all
$a\in \mathscr{A}_A$
we have
$k(a)=ea$
. Note that computable functions
$\mathscr{A}_1 \rightarrow \mathscr{A}_A$
are in bijective correspondence with elements of
$\mathscr{A}_A$
: a function
$k:\mathscr{A}_1 \rightarrow \mathscr{A}_A$
is represented by
$\lambda x.\, k(*)$
.
Proposition 2.
Let
$\mathscr{A}$
be a TCA with a unit type.
$\mathbf{Asm}(\mathscr{A}) \cong \mathbf{Asm}(\mathbf{R}(\mathscr{A}))$
.
Proof.
Up to the identification of computable functions
$\mathscr{A}_1 \rightarrow \mathscr{A}_A$
with elements of
$\mathscr{A}_A$
, the functors going back and forth between these two categories are identities on both objects and arrows. A function
$f$
realized by
$e$
in
$\mathbf{Asm}(\mathscr{A})$
is realized by the computable function
$e\cdot (-)$
(represented by
$e$
) in
$\mathbf{Asm}(\mathbf{R}(\mathscr{A}))$
; conversely, a function
$g$
realized by the computable function
$k$
in
$\mathbf{Asm}(\mathbf{R}(\mathscr{A}))$
is realized by
$e_k$
in
$\mathbf{Asm}(\mathscr{A})$
, where
$e_k$
represents
$k$
.
2.2 Realizer categories
In this development, the key to obtaining realizers with non-trivial homotopical structure is to take part of the structure of a realizer category to be an interval qua internal cogroupoid. We will assume that realizer categories are cartesian closed; this is a fairly mild assumption and provides a pleasant context in which to work with intervals. Warren (Reference Warren2008) and Warren (Reference Warren2012) are excellent references when it comes to intervals qua cogroupoids. Realizer categories come in typed and untyped varieties.
2.2.1 Intervals
Let
$\mathbf{R}$
be a category with a terminal object. An interval (cogroupoid)
$\mathbb{I}\in \mathbf{R}$
is a diagram of the form
We require that
$\mathbb{I}_0=1$
is terminal.
$\mathbb{I}_0$
and
$\mathbb{I}_1$
are, respectively, known as the “object of coobjects” and the “object of coarrows.” The diagram
is required to be a pushout. Maps
$\mathbb{I}_1 \rightarrow A$
are thought of as paths in
$A$
, and so, the pushout allows us to concatenate two paths
$\alpha, \beta :\mathbb{I}_1 \rightarrow A$
that match nose to tail:
$\beta 0 = \alpha 1$
. The result is
$[\beta, \alpha ]:\mathbb{I}_2 \rightarrow A$
(a path with twice the length of
$\alpha$
and
$\beta$
). Likewise, the following is a pushout.
To round off the definition, the cogroupoid axioms are required to hold. The first set makes sure that the end point (or, respectively, cosource and cotarget) maps
$0,1$
play nicely with cocomposition
$2$
and coidentity
$*$
.
The second set makes sure that the inverse operation
$\sigma$
behaves as expected.
The next two axioms are coidentity and coassociativity, respectively.
Lastly, we have coinverse laws.
Definition 3.
A (typed) realizer category
$(\mathbf{R},\mathbb{I})$
is a cartesian closed category
$\mathbf{R}$
together with an interval
$\mathbb{I}\in \mathbf{R}$
.
Example 4.
$(\mathbf{Gpd},\mathbf{I})$
is a realizer category. The object of coarrows
$\mathbf{I}_1$
is the “walking isomorphism”:
The maps
$0$
and
$1$
pick out the corresponding end points of
$\mathbf{I}_1$
. The map
$\sigma$
sends
$i\mapsto i^{-1}$
.
$\mathbf{I}_2$
has three objects and, again, one arrow in each hom set.
The maps
$i_0$
and
$i_1$
send
$i\in \mathbf{I}_1$
to the synonymous (eponymous, even) morphisms in
$\mathbb{I}_2$
. The map
$2$
picks out the composite
$i_1 i_0$
.
Continuing the trend,
$\mathbf{I}_3$
has four objects and one arrow in each hom set.
The map
$j_0$
sends
$i_0 \mapsto i_0$
and
$i_1 \mapsto i_1$
; the map
$j_1$
sends
$i_0 \mapsto i_1$
and
$i_1 \mapsto i_2$
.
Example 5.
Let
$\mathbf{hTop}$
be the category of spaces and homotopy classes of maps. The full subcategory spanned by the CW complexes is cartesian closed (
$\mathbf{hTop}$
is only weakly cartesian closed). It contains an interval whose object of coarrows is the real unit interval
$[0,1]$
. Note that we must take homotopy classes of maps so that the cogroupoid axioms hold.
2.2.2 Homotopies
The interval
$\mathbb{I}\in \mathbf{R}$
endows the ambient category with the structure of a (2,1)-category (in fact, a strict
$\omega$
-category, see Warren (Reference Warren2012), Theorem 1.12). The higher cells are given by homotopies with respect to
$\mathbb{I}$
.
A homotopy
$H:f\Rightarrow g:A\rightarrow B$
with respect to the interval
$\mathbb{I}$
is a map
$H:A\times \mathbb{I}_1 \rightarrow B$
making the following diagram in
$\mathbf{R}$
commute.
Given a homotopy
$H:A\times \mathbb{I}_1 \rightarrow B$
, we can find its domain and codomain respectively by:
\begin{align*} &\textsf{dom}(H) := H \circ \left \langle A, 0* \right \rangle &\textsf{cod}(H) := H \circ \left \langle A, 1* \right \rangle \end{align*}
As the functor
$(-)\times A$
possesses a right adjoint, the following square is a pushout.
If
$H,H^{\prime}: A \times \mathbb{I}_1 \rightarrow B$
such that
$H^{\prime}(A \times 0) = H (A \times 1)$
, then the morphism
$[H^{\prime},H]:A\times \mathbb{I}_2 \rightarrow B$
is given by:
\begin{align*} \mu \left [ \lambda (H^{\prime} \circ \textsf{swap}), \lambda (H \circ \textsf{swap}) \right ] \circ \textsf{swap} \end{align*}
If
$\textsf{dom}(H^{\prime}) = \textsf{cod}(H)$
, then their vertical composition is defined using this universal morphism:
\begin{equation*} H^{\prime} \circ H := [H^{\prime},H] \circ \left (A\times 2\right ) \end{equation*}
(note the overloading of the composition symbol
$\circ$
).
The horizontal composition
$H^{\prime} \ast H$
of
$H:A\times \mathbb{I}_1\rightarrow B$
and
$H^{\prime}:B\times \mathbb{I}_1\rightarrow C$
is given by the following composite in
$\mathbf{R}$
.
The identity homotopy at
$f:A\rightarrow B$
is given by
$f\pi _1: A\times \mathbb{I}_1 \rightarrow B$
, and the inverse of a homotopy
$H:A\times \mathbb{I}_1 \rightarrow B$
is
$H\circ (A\times \sigma )$
.
2.2.3 Fundamental groupoids
By considering maps out of
$\mathbb{I}$
into a fixed object
$A\in \mathbf{R}$
, we obtain the fundamental groupoid of
$A$
. That is, we have a 2-functor:
\begin{equation*} \Pi = (-)^{\mathbb {I}} : \mathbf {R} \rightarrow \mathbf {Gpd} \end{equation*}
A quick way to see this is because the contravariant hom functor takes colimits (used in the definition of an interval) to limits (used in the definition of a category).
The fundamental groupoid of
$A$
has as objects points in
$A$
, that is, maps
$\mathbb{I}_0\rightarrow A$
. A morphism
$\alpha :a\rightarrow b$
is a path
$\alpha$
in
$A$
making the following diagram commute.
The composition of
$\alpha :a\rightarrow b$
with
$\beta :b\rightarrow c$
is defined by:
\begin{equation*} \beta \circ \alpha := [\beta, \alpha ] \circ 2 \end{equation*}
(
$2$
reparameterizes the double-length path). The identity at
$a$
is
$a*$
and the inverse of
$\alpha$
is
$\alpha \sigma$
.
If
$f:A\rightarrow B \in \mathbf{R}$
, the functor
$\Pi (f):\Pi A \rightarrow \Pi B$
is given by post-composition (in
$\mathbf{R}$
) with
$f$
. The composition law for functors holds because
$f[\beta, \alpha ] = [f\beta, f\alpha ]$
by the universal property of the pushout (1).
A natural isomorphism
$\phi : F\Rightarrow G: \mathbf{C}\rightarrow \mathbf{D}$
between functors (between categories or groupoids) is equivalently given by a functor:
\begin{align*} \phi :\mathbf{C} \times \mathbf{I}_1 \rightarrow \mathbf{D} \end{align*}
such that
$\phi (-,0)=F$
and
$\phi (-,1)=G$
. In this way, a homotopy
$H:f\Rightarrow g:A\rightarrow B\in \mathbf{R}$
gives rise to a natural transformation:
\begin{equation*} \Pi (H) : \Pi A \times \mathbf {I}_1 \rightarrow \Pi B \end{equation*}
by setting:
\begin{align*} &\Pi (H)(a,0) = \Pi (H)(a) := H \circ \langle a,0 \rangle : \mathbb{I}_0\rightarrow B \\ &\Pi (H)(a,1) = \Pi (H)(a) := H \circ \langle a,1 \rangle : \mathbb{I}_0\rightarrow B \\ &\Pi (H)(\alpha, i) = \Pi (H)(\alpha ) := H \circ \langle \alpha, \mathbb{I}_1 \rangle : \mathbb{I}_1\rightarrow B \\ &\Pi (H)(\alpha, i^{-1}) = \Pi (H)(\alpha ) := H \circ \langle \alpha, \sigma \rangle : \mathbb{I}_1\rightarrow B \end{align*}
Given a homotopy
$H:f\Rightarrow g:A\rightarrow B$
and a path
$\alpha :a\rightarrow b\in \Pi A$
, the path
$\Pi (H)(\alpha, i) \in \Pi B$
can be thought of as the diagonal path through a naturality square. Indeed, we have the following.
Lemma 6 (Warren, personal communication). With the above data, the following diagram commutes in
$\Pi B$
.
Proof.
We show that the diagonal is equal to the left-bottom boundary; that these are equal to the top-right boundary is a symmetric argument. Using the definition of composition in
$\Pi B$
, we have to show
\begin{align*} H \circ \langle \alpha, \mathbb{I}_1 \rangle = \left [H \circ \langle \alpha 1 *, \mathbb{I}_1 \rangle, H \circ \langle \alpha, 0 *\rangle \right ] \circ 2 \end{align*}
This simplifies to
\begin{align*} H \circ (\alpha \times \mathbb{I}_1) \circ \left [ \left \langle 1 *, \mathbb{I}_1 \rangle, \langle \mathbb{I}_1, 0 * \right \rangle \right ] \circ 2 \end{align*}
But
\begin{align*} \left [\left \langle 1 *, \mathbb{I}_1 \rangle, \langle \mathbb{I}_1, 0 * \right \rangle \right ] \circ 2 \end{align*}
is a decomposition of the diagonal
$\Delta _{\mathbb{I}_1}$
(see Warren (Reference Warren2012), p. 212).
2.2.4 Squares
Let
$(\mathbf{R},\mathbb{I})$
be a realizer category. Define the (edge-symmetric) double category
$\Box \mathbf{R}(A,B)$
to have
-
• objects: maps
$A\rightarrow B \in \mathbf{R}$
; -
• both horizontal and vertical morphisms: maps
$A\times \mathbb{I}_1 \rightarrow B$
; -
• 2-cells: commutative squares of maps
$A\times \mathbb{I}_1 \rightarrow B$
.
Denote by
$\blacksquare \mathbf{R}(A,B)$
the (edge-symmetric) double category with the same objects and morphisms as
$\Box \mathbf{R}(A,B)$
, but with 2-cells maps
$A\times \mathbb{I}_1 \times \mathbb{I}_1 \rightarrow B$
.
As a consequence of Lemma 6, every 2-cell
$\phi \in \blacksquare \mathbf{R}(A,B)$
determines a 2-cell
$\partial (\phi )\in \Box \mathbf{R}(A,B)$
:
where, for example,
$\phi _{01} := \phi \circ \langle A, 0*, 1* \rangle : A \rightarrow B$
and
$\phi _{\mathbb{I}_1 1} := \phi \circ \langle A\pi _1, \mathbb{I}_1\pi _2, 1*\pi _2 \rangle : A\times \mathbb{I}_1 \rightarrow B$
. This determines a double functor:
\begin{align*} \partial _{\mathbf{R}(A,B)}: \blacksquare \mathbf{R}(A,B) \rightarrow \Box \mathbf{R}(A,B) \end{align*}
for each
$A,B\in \mathbf{R}$
(we sometimes just write
$\partial$
).
Remark 7.
Some of the results to follow rely on the hypothesis that, for all
$A,B\in \mathbf{R}$
,
$\partial _{\mathbf{R}(A,B)}$
is an isomorphism of double categories. As shorthand for this, we will say that
$\partial _{\mathbf{R}}$
is an isomorphism.
This hypothesis holds whenever
$(\mathbf{R},\mathbb{I})$
is finitely complete as a (2,1)-category, for then the cotensor
$\mathbf{I}_1 \pitchfork B$
is necessarily isomorphic to the internal hom
$B^{\mathbb{I}_1}$
(Warren, Reference Warren2008, Lemma 3.25):
\begin{align*} \mathbf{R}\left (A, \mathbf{I}_1 \pitchfork B \right ) \cong \mathbf{Gpd}\left ( \mathbf{I}_1, \mathbf{R}(A,B) \right ) \cong \mathbf{R}\left (A\times \mathbb{I}_1, B \right ) \cong \mathbf{R}\left (A,B^{\mathbb{I}_1}\right ) \end{align*}
2.2.5 Untyped realizer categories
We know from other settings (Birkedal, Reference Birkedal2000a,b; Robinson and Rosolini, Reference Robinson and Rosolini2001; Lietz and Streicher, Reference Lietz and Streicher2002) that impredicativity is intimately related to untypedness at the level of realizers. A “universal object” allows us to turn the a priori typed notion of realizability given by a category into an untyped one. Traditionally, an object in a category is universal iff every object in the category is a retract of it. In the higher setting, we allow for pseudoretracts.
Definition 8.
An object
$U\in \mathbf{R}$
is universal iff for every object
$A\in \mathbf{R}$
, there is a section and retraction
together with a homotopy:
\begin{align*} \rho _A: r_A s_A \Rightarrow \textsf{id}_A \end{align*}
Definition 9.
An untyped realizer category
$(\mathbf{R},\mathbb{I},U)$
is a (typed) realizer category
$(\mathbf{R},\mathbb{I})$
together with a universal object
$U\in \mathbf{R}$
.
In particular, an untyped realizer category provides an up-to-homotopy model of the untyped
$\lambda$
-calculus:
$U^U$
is a pseudoretract of
$U$
.
Example 10.
Domain theory is a rich source of models of the untyped
$\lambda$
-calculus. Scott complete categories, introduced by Adámek (Reference Adámek1997), are categorified Scott domains (Scott, Reference Scott1993). A Scott complete category is a finitely accessible category in which every diagram with a cocone has a colimit. Let
$\kappa$
be an inaccessible cardinal. The category
$\mathbf{SCC}$
of locally
$\kappa$
-small Scott complete categories and continuous functors is cartesian closed (Adámek, Reference Adámek1997), contains the interval
$\mathbf{I}\in \mathbf{Gpd}$
(see Example
4
), and contains a universal object (velebil, Reference Velebil1999). Homotopies with respect to
$\mathbf{I}$
in
$\mathbf{SCC}$
are arbitrary natural isomorphisms.
$\partial _{\mathbf{Gpd}}$
is an isomorphism and thus
$\partial _{\mathbf{SCC}}$
is too.
3. Categories of Partitioned Groupoidal Assemblies
We first define the constituents of the category
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
of partitioned groupoidal assemblies over the realizer category
$(\mathbf{R},\mathbb{I})$
.
Definition 11.
A partitioned groupoidal assembly
$X$
is a triple
$(X,A,{\left \Vert - \right \Vert }_X)$
, where
$X\in \mathbf{Gpd}$
is the underlying groupoid,
$A\in \mathbf{R}$
is the “realizer type,” and
\begin{align*}{\left \Vert - \right \Vert }_X : X \rightarrow \Pi A \end{align*}
is the functor that assigns realizers to objects and isomorphisms of
$X$
. A partitioned groupoidal assembly
$X$
is modest whenever
${\left \Vert -\right \Vert }_X$
is fully faithful.
A morphism
\begin{align*} F: (X,A,{\left \Vert -\right \Vert }_X) \rightarrow (Y,B,{\left \Vert -\right \Vert }_Y) \end{align*}
of partitioned groupoidal assemblies is a functor
$F: X \rightarrow Y$
such that there exists
$e:A\rightarrow B$
and a natural isomorphism
$\epsilon$
as in the following diagram.
This formalizes the homotopy BHK interpretation: a realizer of an object
$x\in X$
is a point
$a\in \Pi A$
(i.e., a map
$a:\mathbb{I}_0 \rightarrow A$
), and a realizer of an identification (isomorphism)
$p:x\rightarrow x^{\prime} \in X$
is a path
$\alpha : a \rightarrow a^{\prime} \in \Pi A$
(i.e., a map
$\alpha :\mathbb{I}_1\rightarrow A$
such that
$\alpha 0=a$
and
$\alpha 1=a^{\prime}$
, where
$a^{\prime}$
realizes
$x^{\prime}$
.
The morphism
$e: A \rightarrow B$
implements the functor
$F$
up to natural isomorphism, as witnessed by
$\epsilon$
. We will often refer to the pair
$(e,\epsilon )$
as a realizer for
$F$
, writing
$(e,\epsilon ) \Vdash F$
.
Identities in
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
are identity functors; each is realized by the relevant pair of an identity morphism and an identity natural isomorphism. Composition is performed by pasting squares such as (2) side by side; explicitly, if
$(e,\epsilon )\Vdash F:X\rightarrow Y$
and
$(e^{\prime},\epsilon ^{\prime})\Vdash G:Y\rightarrow Z$
, then the composite
$GF:X\rightarrow Z$
is realized by:
\begin{align*} \left ( e^{\prime}e, \left (\epsilon ^{\prime} \ast F \right ) \circ \left (\Pi \left (e^{\prime}\right ) \ast \epsilon \right ) \right ) \end{align*}
Observe that
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
is a quotient of the “super-comma” category
$\mathbf{Gpd} \downarrow \Pi$
(to use the terminology of Mac Lane (Reference Mac Lane1971) – though might nowadays be called the underlying 1-category of the 2-comma category); it is a quotient because realizers of are only required to exist, not carried around as extra data. This should be compared to the
$\mathscr{F}$
-construction of Robinson and Rosolini (Reference Robinson and Rosolini2001), which is a set-based, 1-categorical analog.
The above definition of modesty generalizes the traditional notion, for if
$\mathbb{I}$
is a discrete interval and
$X$
a set then, given fullness,
${\left \Vert x \right \Vert }_X ={\left \Vert x^{\prime} \right \Vert }_X$
implies
$X(x,x^{\prime})\neq \emptyset$
and thus
$x=x^{\prime}$
.
Proposition 12.
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
is weakly cartesian closed. Moreover, the weak exponential object
$Y^X$
is modest whenever
$Y$
is.
Proof.
The terminal object is
$(\mathbf{1},\mathbb{I}_0,\Vert \!-\! \Vert _{\mathbf{1}}: *\mapsto \mathbb{I}_0)$
. Let
$(X,A,{\left \Vert -\right \Vert }_X), (Y,B,{\left \Vert -\right \Vert }_Y) \in \mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
. Their product is
\begin{align*} \left ( X\times Y, A\times B,{\left \Vert -\right \Vert }_{X\times Y} \right ) \end{align*}
where
\begin{align*}{\left \Vert -\right \Vert }_{X\times Y} := \left \langle{\left \Vert \pi _1(-) \right \Vert }_X, {\left \Vert \pi _2(-) \right \Vert }_Y \right \rangle \end{align*}
The weak exponential is
\begin{align*} Y^X := \left ( \textsf{Real}\left (Y^X\right ), B^A,{\left \Vert -\right \Vert }_{Y^X} \right ) \end{align*}
where
$\textsf{Real}(Y^X)$
is the groupoid whose objects are triples
\begin{align*} \left ( F: X \rightarrow Y, e \in \Pi \left (B^A\right ),\epsilon \right ) \end{align*}
such that
\begin{align*} \left ( \mu (e) \circ \langle *, A \rangle, \epsilon \right ) \Vdash F \end{align*}
and whose morphisms
$(F,e,\epsilon )\rightarrow (G,e^{\prime},\epsilon ^{\prime})$
are tuples
\begin{align*} \left ( \psi :F\Rightarrow G, f:e\rightarrow e^{\prime}, \zeta \right ) \end{align*}
such that
\begin{align*} \left ( \mu (f)\circ \textsf{swap}, \zeta \right ) \Vdash \psi \end{align*}
and
\begin{align} &\zeta (-,0,-) = \epsilon &\zeta (-,1,-) = \epsilon ^{\prime} \end{align}
Actually, the natural isomorphism
$\zeta$
is uniquely determined: the equations (3) mean that the boundary of
$\zeta$
is fully specified and
$\partial _{\mathbf{Gpd}}$
is an isomorphism.
The evaluation morphism is defined
\begin{align*} &\textsf{ev}: Y^X \times X \rightarrow Y \\ &\textsf{ev}(F,e,\epsilon, x) := Fx \\ &\textsf{ev}(\psi, f,p) := \psi (p,i) \end{align*}
and realized by
$(\textsf{ev},\epsilon ^{\prime})$
, where
$\textsf{ev}$
denotes the evaluation map in
$\mathbf{R}$
, and where
\begin{align*} \epsilon ^{\prime}_{(F,e,\epsilon, x)} := \epsilon _x \end{align*}
The naturality of
$\epsilon ^{\prime}$
is captured the following cube.
For the universal property, suppose we have a morphism
\begin{align*} K: \left ( Z, C,{\left \Vert -\right \Vert }_Z \right ) \times X \rightarrow Y \end{align*}
Pick a realizer
$(e,\epsilon )\Vdash K$
. With this, we define the transpose
$\widetilde{K}: Z \rightarrow Y^X$
of
$K$
. On objects
\begin{align*} \widetilde{K}(z) := \left ( K(z,-), e^z, \epsilon ^z \right ) \end{align*}
where
\begin{align*} &e^z := \lambda \left ( e \circ \left ({\left \Vert z \right \Vert }_Z \times A \right ) \right ) \\ &\epsilon ^z_x :={\epsilon }_{(z,x)} \end{align*}
This works because
\begin{align*} \Pi \left ( \mu \left ( \lambda \left ( e \circ \left ({\left \Vert z \right \Vert }_Z \times A \right ) \right ) \right ) \circ \langle *,A \rangle \right ){\left \Vert x \right \Vert }_X = &\mu \left ( \lambda \left ( e \circ \left ({\left \Vert z \right \Vert }_Z \times A \right ) \right ) \right ) \circ \langle *,A \rangle \circ{\left \Vert x \right \Vert }_X \\ = & e \circ \left ({\left \Vert z \right \Vert }_Z \times A \right ) \langle *, A \rangle \circ{\left \Vert x \right \Vert }_X \\ = & e \circ \left ({\left \Vert z \right \Vert }_Z \times A \right ) \circ \langle \mathbb{I}_0,{\left \Vert x \right \Vert }_X \rangle \\ = & e \circ \left \langle{\left \Vert z \right \Vert }_Z,{\left \Vert x \right \Vert }_X \right \rangle \\ = & \Pi (e){\left \Vert (z,x) \right \Vert }_{Z\times X} \end{align*}
and
\begin{align*} \epsilon _{(z,x)}: \Pi (e){\left \Vert (z,x) \right \Vert }_{Z\times X} \rightarrow{\left \Vert K(z,x) \right \Vert }_Y \end{align*}
On morphisms
\begin{align*} \widetilde{K}(r) := \left ( \psi ^r, f^r \right ) \end{align*}
where
\begin{align*} \psi ^r(p,i) &:= K(r,p) \\ f^r &:= \lambda \left ( e \circ \left ({\left \Vert r \right \Vert }_Z \times A \right ) \right ) \end{align*}
Suppose that
$Y$
is modest and let
$(F,e,\epsilon ),(G,e^{\prime},\epsilon ^{\prime}) \in \textsf{Real}(Y^X)$
. Any
$f:e\rightarrow e^{\prime}$
uniquely determines a morphism
$(\psi, f): (F,e,\epsilon ) \rightarrow (G,e^{\prime},\epsilon ^{\prime})$
due to
${\left \Vert -\right \Vert }_Y$
being fully faithful: the image of the component
$\psi _x$
under
${\left \Vert -\right \Vert }_Y$
is the unique morphism making the following square commute.
3.1 As 2-categories
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
possesses an interval of its own. The object of coarrows is given by:
\begin{align*} &\mathbf{I}_1 := \left ( \mathbf{I}_1, \mathbb{I}_1,{\left \Vert -\right \Vert }_{\mathbf{I}_1} \right ) \\ &{\left \Vert 0 \right \Vert }_{\mathbf{I}_1} := 0 &&{\left \Vert 1 \right \Vert }_{\mathbf{I}_1} := 1 &&&{\left \Vert i \right \Vert }_{\mathbf{I}_1} := \mathbb{I}_1 \end{align*}
The other parts of the cogroupoid diagram are likewise obtained by marrying up the corresponding parts of the cogroupoids in
$\mathbf{Gpd}$
and
$\mathbf{R}$
:
\begin{align*} &\mathbf{I}_2 := \left ( \mathbf{I}_2, \mathbb{I}_2,{\left \Vert -\right \Vert }_{\mathbf{I}_2} \right ) \\ &{\left \Vert 0 \right \Vert }_{\mathbf{I}_2} := i_0 0 &&{\left \Vert 1 \right \Vert }_{\mathbf{I}_2} := i_0 1 = i_1 0 &&&{\left \Vert 2 \right \Vert }_{\mathbf{I}_2} := i_1 1\\ &{\left \Vert i_0 \right \Vert }_{\mathbf{I}_2} := i_0 \quad \quad &&{\left \Vert i_1 \right \Vert }_{\mathbf{I}_2} := i_1 \\ &\mathbf{I}_3 := \left ( \mathbf{I}_3, \mathbb{I}_3,{\left \Vert -\right \Vert }_{\mathbf{I}_3} \right )\\ &{\left \Vert 0 \right \Vert }_{\mathbf{I}_2} := j_0 i_0 0 &&{\left \Vert 1 \right \Vert }_{\mathbf{I}_2} := j_0 i_0 1 = j_0 i_1 0 = j_1 i_0 0 \\ &{\left \Vert 2 \right \Vert }_{\mathbf{I}_2} := j_0 i_1 1 = j_1 i_0 1 = j_1 i_1 0 &&{\left \Vert 3 \right \Vert }_{\mathbf{I}_2} := j_1 i_1 1 \\ &{\left \Vert i_0 \right \Vert }_{\mathbf{I}_2} := j_0 i_0 &&{\left \Vert i_1 \right \Vert }_{\mathbf{I}_2} := j_0 i_1 = j_1 i_0 &&&{\left \Vert i_2 \right \Vert }_{\mathbf{I}_2} := j_1 i_1 \end{align*}
The underlying functors of the morphisms
$i_0,i_1,2,j_0,j_1 \in \mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
are as in Example 4 and are realized by the maps
$i_0,i_1,2,j_0,j_1\in \mathbf{R}$
, respectively.
We will show that
$\mathbf{I}_2$
is the pushout of
$0,1$
; a similar argument works for
$\mathbf{I}_3$
. Suppose that we are in the following situation:
where
$(e,\epsilon )\Vdash F$
. The functor
$[G,F]:\mathbf{I}_2 \rightarrow X$
is the universal morphism in
$\mathbf{Gpd}$
. Define
$d := e0*$
and observe that
\begin{align*} \Pi (d){\left \Vert 0 \right \Vert }_{\mathbf{I}_2} = \Pi (d){\left \Vert 1 \right \Vert }_{\mathbf{I}_2} = \Pi (d){\left \Vert 2 \right \Vert }_{\mathbf{I}_2} = e0 \end{align*}
as well as
\begin{align*} \Pi (d){\left \Vert i_0 \right \Vert }_{\mathbf{I}_2} = \Pi (d){\left \Vert i_1 \right \Vert }_{\mathbf{I}_2} = e0* = \textsf{id}_{e0} \end{align*}
We can realize
$[G,F]$
with
$(d,\delta )$
, where
\begin{align*} \delta _0 &:= \epsilon _0 : e0 \rightarrow{\left \Vert F0 \right \Vert }_X \\ \delta _1 &:= \epsilon _1 e : e0 \rightarrow{\left \Vert F1 \right \Vert }_X \\ \delta _2 &:={\left \Vert G(i) \right \Vert }_X \epsilon _1 e : e0 \rightarrow{\left \Vert G1 \right \Vert }_X \end{align*}
Naturality of
$\epsilon$
guarantees naturality of
$\delta$
.
As
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
is only weakly cartesian closed, we cannot apply ((Warren, Reference Warren2012), Theorem 1.12) (which assumes cartesian closedness) to deduce that it becomes a (2,1)-category when 2-cells are taken to be homotopies. However, we will show by hand that this is the case after all.
Let
$\phi : F \Rightarrow G: X \rightarrow Y$
and
$\psi : G \Rightarrow H: X \rightarrow Y$
be homotopies in
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
. Their vertical composition
$\psi \circ \phi = \psi \phi : F \Rightarrow H: X \rightarrow Y$
is defined as in
$\mathbf{Gpd}$
:
\begin{align*} &\psi \phi : X \times \mathbf{I}_1 \rightarrow Y \\ &\psi \phi (p:x\rightarrow x^{\prime},i) := \psi _{x^{\prime}} \circ \phi _{x^{\prime}} \circ F(p) = H(p) \circ \psi _x \circ \phi _x \end{align*}
Let
$(e^\phi, \epsilon ^\phi ) \Vdash \phi$
and
$(e^\psi, \epsilon ^\psi ) \Vdash \psi$
. We obtain a realizer
$(e^{\psi \phi }, \epsilon ^{\psi \phi }) \Vdash \psi \phi$
as follows. First let
$e^{\psi \phi } := e^\phi$
. Then define
\begin{align*} \epsilon ^{\psi \phi }_{(x,0)} &:= \epsilon ^\phi _{(x,0)} : e^\phi{\left \Vert (x,0) \right \Vert }_{X \times \mathbf{I}_1} \rightarrow{\left \Vert Fx \right \Vert }_Y \\ \epsilon ^{\psi \phi }_{(x,1)} &:={\left \Vert \psi _x \right \Vert }_Y \circ \epsilon ^\phi _{(x,1)} : e^\phi{\left \Vert (x,0) \right \Vert }_{X \times \mathbf{I}_1} \rightarrow{\left \Vert Gx \right \Vert }_Y \rightarrow{\left \Vert Fx \right \Vert }_Y \end{align*}
That this is natural is captured in the following diagram.
Now let
$\phi : F\Rightarrow G: X\rightarrow Y$
and
$\psi : H\Rightarrow K: Y\rightarrow Z$
. Their horizontal composition
$\psi \ast \phi : HF \Rightarrow KG: X \rightarrow Z$
is defined as in
$\mathbf{Gpd}$
:
\begin{align*} &\psi \ast \phi : X \times \mathbf{I}_1 \rightarrow Z \\ &\psi \ast \phi (x,0) := HFx \\ &\psi \ast \phi (x,1) := KGx \\ &\psi \ast \phi (p,i) := \psi _{Gx^{\prime}} \circ H\left (\phi _{x^{\prime}}\right ) \circ H(F(p)) = K(G(p)) \circ \psi _{Gx} \circ H\left (\phi _x\right ) \end{align*}
Let
$(e^\phi, \epsilon ^\phi ) \Vdash \phi$
,
$(e^\psi, \epsilon ^\psi ) \Vdash \psi$
, and
$(e^H, \epsilon ^H) \Vdash H$
. We obtain a realizer
$(e^{\psi \ast \phi }, \epsilon ^{\psi \ast \phi }) \Vdash \psi \ast \phi$
as follows.
\begin{align*} e^{\psi \ast \phi } &:= e^H e^\phi \\ \epsilon ^{\psi \ast \phi }_{(x,0)} &:= \left ( \left (\epsilon ^H \ast \phi \right ) \circ \left (\Pi \left (e^H\right ) \ast \epsilon ^\phi \right ) \right )_{(x,0)} \\ \epsilon ^{\psi \ast \phi }_{(x,1)} &:= \left \Vert \psi _{Gx} \right \Vert _Z \circ \left ( \left (\epsilon ^H \ast \phi \right ) \circ \left (\Pi \left (e^H\right ) \ast \epsilon ^\phi \right ) \right )_{(x,1)} \end{align*}
Naturality is captured in the following diagram.
The identity 2-cell on
$F: X \rightarrow Y$
is given by the identity natural transformation, which is realized by:
\begin{align*} \left ( e^F\pi _1, \left (\epsilon ^F \ast \pi _1 \right ) \circ \left (\Pi \left (e^F\right ) \ast{\left \Vert -\right \Vert }_X \pi _1 \right ) \right ) \end{align*}
where
$(e^F,\epsilon ^F)\Vdash F$
. The inverse of
$\phi : F \Rightarrow G: X \rightarrow Y$
is given by the inverse natural transformation
$\phi ^{-1}: G \Rightarrow F: X \rightarrow Y$
. Assuming
$(e^\phi, \epsilon ^\phi )$
is a realizer for
$\phi$
, then
$\phi ^{-1}$
is realized by
$(e^\phi, \widetilde{\epsilon })$
, where
\begin{align*} &\widetilde{\epsilon }: \Pi (e^\phi ) \circ \Vert \!-\! \Vert _{X \times \mathbf{I}_1} \Rightarrow \Vert \!-\! \Vert _Y \circ \phi ^{-1} \\ &\widetilde{\epsilon }_{(x,0)} := \epsilon ^\phi _{(x,1)} \\ &\widetilde{\epsilon }_{(x,1)} := \epsilon ^\phi _{(x,0)} \end{align*}
The axioms for (2,1)-categories hold in virtue of them holding for
$\mathbf{Gpd}$
.
As a 2-categorical variation on the theme of realizability categories inheriting (or improving) structure from the realizer category, we will now show that
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
is finitely complete as a (2,1)-category whenever
$(\mathbf{R},\mathbb{I})$
is (see Remark 7). With this hypothesis, we may obtain a realizer
$\mathbb{I}_1\times \mathbb{I}_1\rightarrow A$
by providing a commutative square of paths
$\mathbb{I}_1 \rightarrow A$
.
Proposition 13.
If
$\partial _{\mathbf{R}}$
is an isomorphism of double categories, then
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
is finitely complete as a (2,1)-category. In particular, if
$(\mathbf{R},\mathbb{I})$
is finitely complete as a (2,1)-category then so is
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
.
Proof.
A (2,1)-category is finitely complete iff it has a terminal object, pullbacks, and pseudopullbacks ((iso)comma objects) (Street, Reference Street1976). A 2-category
$(\mathbf{C},\mathbb{I})$
arising from an interval has whatever conical (co)limits
$\mathbf{C}$
has in the one-dimensional sense ((Warren, Reference Warren2012), Lemma 2.1). A terminal object was exhibited in Proposition 12.
The pullback
$F^*Y$
of
$G: (Y, B,{\left \Vert -\right \Vert }_Y)\rightarrow (Z,C,{\left \Vert -\right \Vert }_Z)$
along
$F: (X,A,{\left \Vert -\right \Vert }_X) \rightarrow Z$
is given by:
\begin{align*} \left ( F^*Y, A \times B,{\left \Vert -\right \Vert }_{F^* Y} \right ) \end{align*}
where
$F^*Y$
is the pullback in
$\mathbf{Gpd}$
and the realizability functor is defined as:
\begin{align*}{\left \Vert -\right \Vert }_{F^*Y} := \left \langle{\left \Vert \pi _1(-) \right \Vert }_X,{\left \Vert \pi _2(-) \right \Vert }_Y \right \rangle \end{align*}
The projection functors are realized by the respective projections from
$\mathbf{R}$
. If
$S: (W,D,{\left \Vert -\right \Vert }_W) \rightarrow X$
and
$T: W \rightarrow Y$
are such that
$FS = GT$
then we obtain the universal morphism:
\begin{align*} &[S,T] : W \rightarrow F^*Y \\ &[S,T](-) := (S(-),T(-)) \end{align*}
that is realized by:
\begin{align*} \left ( \langle e, e^{\prime} \rangle : D \rightarrow A \times B, \langle \epsilon, \epsilon ^{\prime} \rangle \right ) \end{align*}
where
$(e,\epsilon ) \Vdash S$
and
$(e^{\prime},\epsilon ^{\prime}) \Vdash T$
.
The pseudopullback of
$G: Y \rightarrow Z$
along
$F: X \rightarrow Z$
is given by:
\begin{align*} F\downarrow G := \left ( F\downarrow G, A\times B\times C^{\mathbb{I}_1}, \Vert \!-\! \Vert _{F\downarrow G} \right ) \end{align*}
where
$F\downarrow G$
is the pseudopullback in
$\mathbf{Gpd}$
and the realizability functor is defined as:
\begin{align*}{\left \Vert (x, y, r) \right \Vert }_{F\downarrow G} &:= \left \langle \Vert x \Vert _X, \left \Vert y \right \Vert _Y, \lambda \left \Vert r \right \Vert _Z \right \rangle \\ \left \Vert (p,q) \right \Vert _{F\downarrow G} &:= \left \langle \left \Vert p \right \Vert _X, \left \Vert q \right \Vert _Y, \lambda \left ( \partial ^{-1} \left \Vert (p,q,r,r^{\prime}) \right \Vert _Z \right ) \right \rangle \end{align*}
where
$\Vert (p,q,r,r^{\prime}) \Vert _Z$
denotes the commutative square:
The projection functors are realized by the respective projections from
$\mathbf{R}$
.
If we have morphisms
$S: W \rightarrow X$
and
$T: W \rightarrow Y$
and a 2-cell
$\psi :FS \Rightarrow GT$
, then we obtain the universal morphism:
\begin{align*} & \left [S,T,\psi \right ] : W \rightarrow F\downarrow G \\ &\left [S,T,\psi \right ](w) := \left ( Sw,Tw, \psi (w,i) \right ) \\ &\left [S,T,\psi \right ](v) := \left ( S(v),T(v) \right ) \end{align*}
Finally, we construct a realizer
$(e,\epsilon )\Vdash [S,T,\psi ]$
from realizers
$(e^S,\epsilon ^S) \Vdash S$
,
$(e^T,\epsilon ^T) \Vdash T$
and
$(e^\psi, \epsilon ^\psi ) \Vdash \psi$
. For the first component:
\begin{align*} &e: D \rightarrow A \times B \times C^{\mathbb{I}_1} \\ &e := \big\langle e^S, e^T, \lambda ( e^\psi ) \big\rangle \end{align*}
For the second component:
\begin{align*} \epsilon _w := \left \langle \epsilon ^S_w, \epsilon ^T_w, \lambda \left ( \partial ^{-1} \left ( \epsilon ^\psi _{(w,i)} \right ) \right ) \right \rangle \end{align*}
where
$\epsilon ^\psi _{(w,i)}$
denotes the following (naturality) square of paths in
$\Pi C$
.
Double functoriality of
$\partial ^{-1}$
guarantees the naturality of
$\epsilon$
.
3.2 As path categories
Path categories, introduced by van den Berg and Moerdijk (Reference van den Berg and Moerdijk2018) (see also (van den Berg, Reference van den Berg2018a)), are a slight strengthening of Brown’s (1973) categories of fibrant objects, but nevertheless constitute a relatively minimal setting in which to develop abstract homotopy theory as well as model intensional type theory (in general, path categories model a version of type theory in which the computation rule for identity types holds propositionally). A path category
$\mathbf{C}$
comes equipped with two classes of maps, fibrations and (weak) equivalences, and satisfies the axioms listed below. An acyclic fibration is a map that is both a fibration and an equivalence. Dependent types are modeled by fibrations.
-
PC1 Isomorphisms are fibrations and fibrations are closed under composition.
-
PC2 The pullback of a fibration along any other map exists and is again a fibration.
-
PC3
$\mathbf{C}$
has a terminal object
$1$
and every map
$X \rightarrow 1$
is a fibration. -
PC4 Isomorphisms are equivalences.
-
PC5 Equivalences satisfy the 2-out-of-6 property.
-
PC6 Every object in
$\mathbf{C}$
has a path object. -
PC7 Every acyclic fibration has a section.
-
PC8 The pullback of an acyclic fibration along any other map exists and is again an acyclic fibration.
A path object
$\mathscr{P}X\in \mathbf{C}$
for an object
$X\in \mathbf{C}$
is a factorization of the diagonal by an equivalence
$r$
followed by a fibration
$\langle s, t \rangle$
.
Path objects give rise to a nation of (fiberwise) homotopy between morphisms.
Given an object
$X\in \mathbf{C}$
, let
$\mathbf{C}(X)$
be the full subcategory of the slice
$\mathbf{C}/X$
spanned by the fibrations.
$\mathbf{C}(X)$
is a path category, where a morphism in
$\mathbf{C}(X)$
is a fibration or equivalence iff it is so in
$\mathbf{C}$
. The following result, which is Proposition 2.6 in (van den Berg and Moerdijk, Reference van den Berg and Moerdijk2018) and is proved on p. 428 of (Brown, Reference Brown1973), is used in Section 4.
Lemma 14 (Brown’s lemma). For any map
$f:Y\rightarrow X$
, the pullback functor
\begin{align*} f^*: \mathbf{C}(X) \rightarrow \mathbf{C}(Y) \end{align*}
preserves both fibrations and equivalences.
From hereon in, we assume that
$\partial _{\mathbf{R}}$
is an isomorphism of double categories. To make
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
into a path category, we take fibrations and equivalences to be isofibrations and equivalences, respectively, both internal to
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
considered as a 2-category. Recall (e.g., from ((Lack, Reference Lack, Baez and May2010), Section 7.2) that a morphism
$p:Y\rightarrow Z$
in a 2-category
$\mathbf{C}$
is defined to be an isofibration iff every invertible 2-cell
lifts to an invertible 2-cell
This reduces to the usual notion in the case
$\mathbf{C}=\mathbf{Gpd}$
.
Lemma 15.
A morphism in
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
is a fibration (internal isofibration) if and only if it is an isofibration in
$\mathbf{Gpd}$
.
Proof.
The forward direction is trivial. For the backward direction, suppose we have
$F: (X,A,\left \Vert -\right \Vert _X) \rightarrow (Y,B,\left \Vert -\right \Vert _Y)$
and
$\phi : PF \Rightarrow G: X \rightarrow (Z,C,\left \Vert -\right \Vert _Z) \in \mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
, where
$P: Y \rightarrow Z$
is an isofibration in
$\mathbf{Gpd}$
. Define the functor:
\begin{align*} &\phi ^* F: X \rightarrow Y \\ &\phi ^* F (x) := \left (\phi _x\right )^* Fx \\ &\phi ^* F (p:x\rightarrow x^{\prime}) := \overline{\left (\phi _x\right )}(Fx^{\prime}) \circ F(p) \circ{\overline{\left (\phi _x\right )}(Fx)}^{-1} \end{align*}
where
$\left (\phi _x\right )^* Fx$
is the transport of
$Fx$
along the path
$\phi _x$
. So indeed
$P \circ \phi ^* F = G$
. Moreover, define the natural transformation:
\begin{align*} &\overline{\phi }(F): X \times \mathbf{I}_1 \rightarrow Y \\ &\overline{\phi }(F)(p,i) := \overline{\left (\phi _{x^{\prime}}\right )}(Fx^{\prime}) \circ F(p) \end{align*}
We have
$P \ast \overline{\phi }(F) = \phi$
. We need to realize both
$\phi ^* F$
and
$\overline{\phi }(F)$
.
Suppose that
$(e,\epsilon )\Vdash F$
. We obtain a realizer
$(e, \delta ) \Vdash \phi ^* F$
by setting
\begin{align*} \delta _x :={\left \Vert \overline{\left (\phi _x\right )} (Fx) \right \Vert }_Y \circ \epsilon _x : \Pi (e)\left \Vert x \right \Vert _X \rightarrow{\left \Vert \phi ^* F(x) \right \Vert }_Y \end{align*}
The following diagram encapsulates the naturality of
$\delta$
.
We obtain a realizer
$(e\pi _1: A\times \mathbb{I}_1 \rightarrow B, \gamma ) \Vdash \overline{\phi }(F)$
by setting:
\begin{align*} \gamma _{(x,0)} &:= \epsilon _x: \Pi (e\pi _1) \left \Vert (x,0) \right \Vert _{X\times \mathbf{I}_1} = \Pi (e)\left \Vert x \right \Vert _X \rightarrow \left \Vert Fx \right \Vert _Y \\ \gamma _{(x,1)} &:= \left \Vert \overline{\left ( \phi _x \right )} (Fx) \right \Vert _Y \circ \epsilon : \Pi (e\pi _1) \left \Vert (x,1) \right \Vert _{X\times \mathbf{I}_1} = \Pi (e)\left \Vert x \right \Vert _X \rightarrow \left \Vert \phi ^* F (x) \right \Vert _Y \end{align*}
The diagram above also establishes the naturality of
$\gamma$
, noting that
$\Pi (e\pi _1)\left \Vert - \right \Vert _{X\times \mathbf{I}_1} = \Pi (e)\left \Vert \pi _1(-) \right \Vert _X$
.
This is worth emphasizing: given an isofibration
$F: (X,A,\left \Vert -\right \Vert ) \rightarrow (Y,B,\left \Vert -\right \Vert _Y)$
, the fibers
$X_y$
are partitioned groupoidal assemblies, where
$\left \Vert -\right \Vert _{X_y}$
is just the restriction of
$\left \Vert -\right \Vert _X$
. Given
$q:y \rightarrow y^{\prime} \in Y$
, the transport functor
$q^*: X_y \rightarrow X_{y^{\prime}}$
is realized by
$(\textsf{id}_A, \epsilon )$
, where
$\epsilon _x := \left \Vert \overline{q}(x) \right \Vert _X$
(the
$F$
-lift of
$q$
at
$x$
). This relies on the fact that functors are implemented up to isomorphism.
Using the axiom of choice, every isofibration in
$\mathbf{Gpd}$
is equivalent to a split one. The upshot of the following lemma is that any such equivalence can be upgraded to one in
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
.
Lemma 16.
Let
$X=(X,A,{\left \Vert -\right \Vert }_X) \in \mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
and suppose that we have an equivalence:
\begin{align*} &F: X \rightarrow Y &&G: Y \rightarrow X &&&\phi : \textsf{id}_X \Rightarrow GF &&&&\psi : \textsf{id}_Y \Rightarrow FG \end{align*}
in
$\mathbf{Gpd}$
. Then
$Y$
can be equipped with the structure of a partitioned groupoidal assembly in such a way that the above equivalence is elevated to one in
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
. Moreover, if
$X$
is modest then so is
$Y$
.
Proof.
$Y$
is given the realizer type
$A$
and the realizability functor
\begin{align*}{\left \Vert -\right \Vert }_Y :={\left \Vert -\right \Vert }_X \circ G: Y \rightarrow \Pi A \end{align*}
The functor
$G$
is clearly realized by
$(\textsf{id}, \textsf{id})$
. The functor
$F$
is realized by
$(\textsf{id},{\left \Vert -\right \Vert }_X \ast \phi )$
. The natural transformation
$\phi$
is realized by
$(\pi _1,\epsilon ^\phi )$
, where
\begin{align*} &\epsilon ^\phi _{(x,0)} := \textsf{id}_{{\left \Vert x \right \Vert }_X} &&\epsilon ^\phi _{(x,1)} :={\left \Vert \phi _x \right \Vert }_X \end{align*}
The case for
$\psi$
is completely symmetric.
The functor
$G$
, being an equivalence of groupoids, is fully faithful and essentially surjective. So if
$X$
is modest, then
${\left \Vert -\right \Vert }_Y$
is the composition of two fully faithful functors, and hence fully faithful itself.
Turning to the path category axioms, (PC1)–(PC3) hold due to standard results about isofibrations (of groupoids), and (PC4) and (PC5) hold for equivalences in any 2-category. We check the remaining axioms below.
(PC6): path objects
Given
$X=(X,A,{\left \Vert -\right \Vert }_X)$
, the weak exponential object
$X^{\mathbf{I}_1}$
(see Proposition 12) is a path object
$\mathscr{P}X$
. Thus,
$\mathscr{P}X$
is modest whenever
$X$
is.
The equivalence
$\textsf{r}:X\rightarrow X^{\mathbf{I}_1}$
is given by:
\begin{align*} r(x) &:= \left ( i \mapsto \textsf{id}_x, \lambda{\left \Vert \textsf{id}_x \right \Vert }_X, \textsf{id} \right ) \\ r(p) &:= \left ( (i,i) \mapsto p, \lambda \left ( \partial ^{-1}{\left \Vert p \right \Vert }_X \right ) \right ) \end{align*}
where the argument
${\left \Vert p \right \Vert }_X$
of
$\partial ^{-1}$
denotes the commutative square whose horizontal edges are
${\left \Vert p \right \Vert }_X$
and whose vertical edges are
$\textsf{id}_x$
.
$r$
is realized by
$(\lambda (\pi _1): A \rightarrow A^{\mathbb{I}_1}, \textsf{id})$
.
The fibration
$(s,t)_X: X^{\mathbf{I}_1} \rightarrow X\times X$
is given by:
\begin{align*} (F,e,\epsilon ) &\mapsto (F0,F1) \\ (\psi, f) &\mapsto \left ( \psi (0,i),\psi (1,i) \right ) \end{align*}
realized by
$( \langle \textsf{eval} \circ \langle \textsf{id},0 \rangle, \textsf{eval} \circ \langle \textsf{id},1 \rangle \rangle, \epsilon )$
.
Suppose
$(F,e,\epsilon )$
is in the fiber over
$(x_1,x_2)$
. Then
$F(i): x_1 \rightarrow x_2$
. We define the chosen lift
$(\psi, f): (F,e,\epsilon ) \rightarrow (G,e,\delta )$
of
$p = (p_1,p_2):(x_1,x_2) \rightarrow (x^{\prime}_1,x^{\prime}_2)$
at
$(F,e,\epsilon )$
as follows. First,
\begin{align*} &G(i) := p_2 \circ F(i) \circ p_1^{-1} &&\delta _0 := p_1 \circ \epsilon _0 &&&\delta _1 := p_2 \circ \epsilon _1 \end{align*}
Next,
\begin{align*} \psi (i,i) := p_2 \circ F(i) = G(i) \circ p_1 \end{align*}
Finally,
\begin{align*} f := \lambda \left ( \partial ^{-1} \left (\hat{e}\right ) \right ) : \mathbb{I}_1 \rightarrow A^{\mathbb{I}_1} \end{align*}
where
$\hat{e}$
in the above expression is used to denote the following commutative square of paths in
$\Pi A$
.
(PC7)
Given an acyclic fibration
$F: (X, A,{\left \Vert -\right \Vert }_X ) \rightarrow (Y, B,{\left \Vert -\right \Vert }_Y )$
, a pseudoinverse
$G: Y \rightarrow X$
of
$F$
realized by
$(e,\epsilon )$
and 2-cell
$\psi : GF \Rightarrow \textsf{id}_X$
, we define a section
$S:Y\rightarrow X$
of
$F$
by:
\begin{align*} Sy &:= \left (\psi _y\right )^* Gy \\ S(q:y\rightarrow y^{\prime}) &:= \overline{\left (\psi _{y^{\prime}}\right )}(Gy^{\prime}) \circ G(q) \circ \left ( \overline{\left (\psi _y\right )}(Gy) \right )^{-1} \end{align*}
This is realized by
$(e, \epsilon ^{\prime})$
, where
\begin{align*} \epsilon ^{\prime}_y := \overline{\left (\psi _{y}\right )}(Gy) \circ \epsilon _y \end{align*}
(PC8)
Let
$G: (Y, B, \left \Vert -\right \Vert _Y) \rightarrow (Z, C, \left \Vert -\right \Vert _Z)$
be an acyclic fibration with pseudoinverse
$H: Z \rightarrow Y$
witnessed by natural isomorphisms
$\psi : GH \Rightarrow \textsf{id}_Z$
and
$\phi : \textsf{id}_Y \Rightarrow HG$
. Furthermore, let
$F: (X, A,{\left \Vert -\right \Vert }_X) \rightarrow Z$
be an arbitrary map. We construct a pseudoinverse
$S: X \rightarrow F^*Y$
to the fibration
$F^*(G): F^*Y \rightarrow X$
. Define
$S := [X,T]$
, where
\begin{align*} &T: X \rightarrow Y \\ &Tx := \psi _{Fx}^* HFx \\ &T(p) := \overline{\phi _{Fx^{\prime}}}(HFx^{\prime}) \circ H(F(p)) \circ \left ( \overline{\phi _{Fx}}(HFx) \right ) \end{align*}
Given realizers
$(e^F,\epsilon ^F) \Vdash F$
and
$(e^H,\epsilon ^H) \Vdash H$
, a realizer for
$T$
is
$(e^Fe^H, \epsilon ^T)$
, where
\begin{align*} \epsilon ^T_x := \overline{\psi _{Fx}}(HFx) \circ \epsilon ^H_{Fx} \circ \Pi \left (e^H\right )\left (\epsilon ^F_x\right ) \end{align*}
Clearly, we have
$F^*G \circ S = \textsf{id}_X$
. We now construct a natural isomorphism
$\sigma : \textsf{id}_{F^*Y} \Rightarrow S \circ F^*(G)$
. We have
\begin{align*} S\left (F^*(G)(x,y)\right ) = Sx = \left ( x, \psi ^*_{Fx} HFx \right ) \end{align*}
So we define
\begin{align*} \sigma _{(x,y)} := \left ( \textsf{id}_x, \sigma _y \right ) \end{align*}
where
$\sigma _y$
is the following composite.
This is realized by
$(\pi _1: (A\times B)\times \mathbb{I}_1 \rightarrow A \times B, \epsilon ^\sigma )$
, where
\begin{align*} \epsilon ^\sigma _{(x,y,0)} &:= \left \langle{\left \Vert x \right \Vert }_X,{\left \Vert y \right \Vert }_Y \right \rangle \\ \epsilon ^\sigma _{(x,y,1)} &:= \left \langle{\left \Vert x \right \Vert }_X,{\left \Vert \sigma _y \right \Vert }_Y \right \rangle \end{align*}
3.2.1 Dependent products
The notion of dependent product for path categories studied as (Definition 5.2 van den Berg and Moerdijk (Reference van den Berg and Moerdijk2018)) is as follows. A path category
$\mathbf{C}$
is said to have homotopy
$\Pi$
-types iff for any two fibrations
$f: X \rightarrow J$
and
$\alpha : J \rightarrow I$
, there is an object
$\Pi _\alpha (F): \Pi _\alpha X \rightarrow I$
in
$\mathbf{C}(I)$
together with an “evaluation map”
$\textsf{ev}: \alpha ^* \Pi _\alpha X \rightarrow X$
over
$J$
with the following universal property: if there is a map
$g: Y \rightarrow I$
and a map
$m: \alpha ^* Y \rightarrow X$
over
$J$
, then there exists a unique map
$n: Y \rightarrow \Pi _\alpha X$
such that
$\textsf{ev} \circ \alpha ^* n$
and
$m$
are fiberwise homotopic over
$J$
(type-theoretically, this is the
$\beta$
-law). If the uniqueness criterion on
$n$
is dropped, we are left with weak homotopy
$\Pi$
-types. Type-theoretically, these correspond to dependent functions that do not necessarily satisfy the
$\eta$
-law and thus do not necessarily satisfy function extensionality. If the
$\beta$
-law holds on the nose, then we have (weak)
$\Pi$
-types (see den Besten (Reference den Besten2020)) for a more in-depth study of dependent products in path categories).
Theorem 17.
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
has weak
$\Pi$
-types.
Proof.
Given fibrations
$G: (X, A,{\left \Vert -\right \Vert }_X) \rightarrow (Y, B,{\left \Vert -\right \Vert }_Y)$
and
$F: Y \rightarrow (Z, C,{\left \Vert -\right \Vert }_Z)$
, the objects of the underlying groupoid of
$\Pi _F X$
are tuples
$(z,H,e,\epsilon )$
, where
$z\in Z$
,
$H: F\downarrow z \rightarrow X$
in the slice over
$Y$
(
$F\downarrow z$
is the “homotopy fiber,” constructed as a pseudopullback, see Proposition 13),
$e \in \Pi (A^{B\times C^{\mathbb{I}_1}})$
, and
$\epsilon$
is a natural isomorphism such that
$(\mu (e), \epsilon ) \Vdash H$
.
Observe that any
$r: z \rightarrow z^{\prime}$
induces a morphism
$F\downarrow r: F\downarrow z \rightarrow F\downarrow z^{\prime}$
of partitioned groupoidal assemblies defined by
$(y,u: Fy \rightarrow z) \mapsto (y, ru)$
and identity on morphisms; the morphism is realized by
$(e^r, \epsilon ^r)$
, where
\begin{align*} e^r &:= \textsf{id}_{B\times C^{\mathbb{I}_1}} \\ \epsilon ^r_{(y,u)} &:= \left \langle B, \lambda \left (\partial ^{-1}{\left \Vert (r,u)\right \Vert }_Z\right ) \right \rangle \end{align*}
and where
${\left \Vert (r,u) \right \Vert }_Z$
denotes the following commutative square.
Naturality follows double functoriality of
$\partial ^{-1}$
.
A morphism
$(r, \psi, f, \zeta ): (z,H,e,\epsilon ) \rightarrow (z^{\prime},H^{\prime},e^{\prime},\epsilon ^{\prime})$
in
$\Pi _F X$
consists of a morphism
$r:z\rightarrow z^{\prime}$
, a natural isomorphism
$\psi : H \Rightarrow H^{\prime} \circ (F\downarrow r)$
over
$Y$
and a path
$f:e\rightarrow e^{\prime} \circ e^r = e^{\prime}$
, and a natural isomorphism
$\zeta$
satisfying
\begin{align*} &\zeta (-,0,-) = \epsilon &&\zeta (-,1,-) = \left (\epsilon ^{\prime} \ast (F\downarrow r) \right ) \circ \left (\Pi (e^{\prime}) \ast \epsilon ^r \right ) \end{align*}
as well as
\begin{align*} (\mu (f)\circ \textsf{swap},\zeta )\Vdash \psi \end{align*}
As in the proof of Proposition 12,
$\zeta$
is uniquely determined. The realizer type is
$C \times A^{B\times C^{\mathbb{I}_1}}$
and the realizability functor is given by:
\begin{align*}{\left \Vert -\right \Vert }_{\Pi _F X} := \left \langle{\left \Vert -\right \Vert }_Z \circ \pi _1, \pi _3 \right \rangle \end{align*}
The fibration
$\Pi _F(G): \Pi _F X \rightarrow Z$
is given by the first projection and realized by
$(\pi _1, \textsf{id})$
. The chosen lift of
$r$
at
$(z,H,e,\epsilon )$
is
\begin{align*} (r, \psi, f): (z,H,e,\epsilon ) \rightarrow (z^{\prime},H^{\prime},e,\epsilon ^{\prime}) \end{align*}
where
\begin{align*} H^{\prime} &:= H \circ \left ( F \downarrow r^{-1} \right ) \\ \epsilon ^{\prime} &:= \left (\epsilon \ast F\downarrow r^{-1} \right ) \circ \left ( e \ast \epsilon ^r \right ) \\ \psi &:= \textsf{id}_H \\ f &:= \textsf{id}_e \end{align*}
The third of these definitions makes sense because
$(F\downarrow r^{-1}) \circ (F\downarrow r) = \textsf{id}_{F\downarrow z}$
.
We now define the evaluation map
$\textsf{ev}: F^* \Pi _F X \rightarrow X$
. First, let us compute
$F^*\Pi _F X$
. Objects of the underlying groupoid of
$F^*\Pi _F X$
are tuples
$(y,z,H,e,\epsilon )$
, where
$y\in Y$
,
$z=Fy$
, and
$H$
,
$e$
,
$\epsilon$
are as above. A morphism
$(q, r, \psi, f): (y,z,H,e,\epsilon ) \rightarrow (y^{\prime},z^{\prime},H^{\prime},e^{\prime},\epsilon ^{\prime})$
consists of morphisms
$q: y\rightarrow y^{\prime}$
and
$r=F(q): z \rightarrow z^{\prime}$
, as well as
$\psi$
and
$f$
as described above. The realizer type of
$F^*\Pi _F X$
is
$B \times C \times A^B$
and the realizability functor is given by:
\begin{align*}{\left \Vert -\right \Vert }_{F^*\Pi _F X} := \left \langle{\left \Vert -\right \Vert }_Y \circ \pi _1,{\left \Vert -\right \Vert }_Z \circ \pi _2, \pi _4 \right \rangle \end{align*}
Define the map
$\textsf{ev}$
by:
\begin{align*} \textsf{ev}(y,z,H,e,\epsilon ) &:= H \left ( y, \textsf{id}_z \right ) \\ \textsf{ev}(q,r,\psi, f) &:= H^{\prime}(q) \circ \psi _{\left (y,\textsf{id}_z\right )} \end{align*}
The argument
$q$
of
$H^{\prime}$
is here considered as a morphism
$(y,r) \rightarrow (y^{\prime}, \textsf{id}_{z^{\prime}})$
in
$F\downarrow z^{\prime}$
. The map
$\textsf{ev}$
lives in the slice over
$Y$
thanks to (4). It is realized by
$( \textsf{ev} \circ \langle \pi _3, \pi _1 \rangle, \epsilon ^{\prime} )$
, where we overload notation and use
$\textsf{ev}$
for the evaluation map from
$\mathbf{R}$
, and
$\epsilon ^{\prime}_{(y,z,H,e,\epsilon )} := \epsilon _y$
. This is natural as we know that there is a natural isomorphism
$\zeta$
making the following diagram commute.
For the universal property, assume we have a map
$R: (W, D, \left \Vert -\right \Vert _{W}) \rightarrow Z$
and a map
$S: F^*W \rightarrow X$
over
$Y$
.
We construct a map
$T$
as in the following diagram.
Define
\begin{align*} Tw &:= \left ( Rw, H, e, \epsilon \right ) \\ T(v:w\rightarrow w^{\prime}) &:= \left ( R(v), \psi, f \right ) \end{align*}
where the components
$H$
,
$e$
,
$\epsilon$
,
$\psi$
, and
$f$
are defined below.
First,
\begin{align*} &H: F\downarrow Rw \rightarrow X \\ &H := S \circ \left [ \sigma _1, \sigma _2 \right ] \end{align*}
Here,
\begin{align*} &\sigma _1: F\downarrow Rw \rightarrow Y \\ &\sigma _1(y,r) := r^* y \\ &\sigma _1(q:(y,r)\rightarrow (y^{\prime},r^{\prime})) := \overline{r^{\prime}}(y^{\prime}) \circ q \circ \overline{r}(y)^{-1} \end{align*}
is realized by
$(\pi _1, \delta )$
, where
$\delta _y := \left \Vert \overline{r}(y) \right \Vert _Y$
and
$\sigma _2: F\downarrow Rw \rightarrow W$
is the constantly
$w$
functor, realized by
$( \left \Vert w \right \Vert _W *, \delta ^{\prime})$
, where
$\delta _w := \textsf{id}_{\left \Vert w \right \Vert _W}$
. We can form
$[\sigma _1,\sigma _2]$
because
$F(r^*y) = Rw$
and
\begin{align*} F \left ( \overline{r^{\prime}}(y^{\prime}) \circ q \circ \overline{r}(y)^{-1} \right ) = r^{\prime}qr^{-1} = r^{\prime}qq^{-1}{r^{\prime}}^{-1} = \textsf{id}_{Rw} \end{align*}
Next, pick a realizer
$(e^S, \epsilon ^S) \Vdash S$
and define
$e \in \Pi (A^{B\times C^{\mathbb{I}_1}})$
to be the exponential transpose of
The natural isomorphism
$\epsilon$
is defined by the following pasting diagram.
The
$\Pi$
-types being constructed are weak because we have had to make a choice of realizer
$(e^S,\epsilon ^S)$
for each
$S$
.
As for
$\psi : H \Rightarrow H^{\prime} \circ (F\downarrow R(v))$
, we must have
\begin{align*} &\psi (y,r,0) = H(y,r) = S\left ( r^* y, w \right ) \\ &\psi (y^{\prime},r^{\prime},1) = H^{\prime}(y^{\prime}, R(v)r^{\prime}) = S\left ( (R(v)r^{\prime})^* y^{\prime}, w^{\prime} \right ) \end{align*}
So we define
\begin{align*} \psi (q,i) := S\left ( \overline{R(v)}\left ( (r^{\prime})^*(y^{\prime}) \right ), v \right ) \circ H(q) = H^{\prime}(q) \circ S\left ( \overline{R(v)}\left ( r^*(y) \right ), v \right ) \end{align*}
The argument
$q$
of
$H$
is regarded as a morphism
$(y,r)\rightarrow (y^{\prime},r^{\prime})$
in
$F\downarrow Rw$
, whereas
$q$
qua argument of
$H^{\prime}$
is regarded as a morphism
$(y,R(v)r)\rightarrow (y^{\prime},R(v)r^{\prime})$
in
$F\downarrow Rw^{\prime}$
. Finally, we define
$f:e\rightarrow e^{\prime}$
(recall that
$(e,\epsilon ) \Vdash H$
) to be the exponential transpose of
To complete the proof, we show that
\begin{align*} S = \textsf{ev} \circ F^*T \end{align*}
On objects:
\begin{align*} \textsf{ev}\left ( F^*T (y,w) \right ) &= \textsf{ev}(y,Tw) \\ &= \textsf{ev}(y,Rw,H,e,\epsilon ) \\ &= H\left (y,\textsf{id}_{Rw} \right ) \\ &= S(y, w) \end{align*}
and on morphisms:
\begin{align*} \textsf{ev}\left ( F^*T (q,v) \right ) &= \textsf{ev}(q,T(v)) \\ &= \textsf{ev}(q,R(v),\psi, f) \\ &= H^{\prime}\left (q:(y,R(v)) \rightarrow \left (y^{\prime},\textsf{id}_{Rw^{\prime}}\right )\right ) \circ \psi _{\left ( y, \textsf{id}_{Rw} \right )} \\ &= S\left ( q \circ \left (\overline{R(v)}(y)\right )^{-1}, w^{\prime} \right ) \circ S\left ( \overline{R(v)}(y), v \right ) \\ &= S(q,v) \end{align*}
The fact that that
$S = \textsf{ev} \circ F^*T$
holds on the nose is down to the fact that isofibrations of groupoids are exponentiable.
4. Impredicative Universes of Modest Fibrations
As we have mentioned, we know from other settings (Birkedal, Reference Birkedal2000a,b; Robinson and Rosolini, Reference Robinson and Rosolini2001; Lietz and Streicher, Reference Lietz and Streicher2002) that impredicativity is intimately related to untypedness at the level of realizers. Therefore, in this section, we work over an untyped realizer category
$(\mathbf{R},\mathbb{I},U)$
and in the full subcategory
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I},U) \subseteq \mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
spanned by the partitioned groupoidal assemblies whose realizer type is
$U$
. This subcategory inherits all the categorical structure of
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I})$
discussed so far – including the path category structure – as a consequence of the following.
Proposition 18. The inclusion
\begin{align*} \mathbf{PGAsm}(\mathbf{R},\mathbb{I},U) \hookrightarrow \mathbf{PGAsm}(\mathbf{R},\mathbb{I}) \end{align*}
is an equivalence of 2-categories.
Proof.
It suffices to show essential surjectivity. For any
$X=(X,A,{\left \Vert -\right \Vert }_X)$
, we define an isomorphism
\begin{align*} F:X\rightarrow X^{\prime} := \left (X,U,{\left \Vert -\right \Vert }_{X^{\prime}}\right ) \end{align*}
where
\begin{align*}{\left \Vert -\right \Vert }_{X^{\prime}} := \Pi (s_A){\left \Vert -\right \Vert }_X \end{align*}
The underlying functor of
$F$
is
$\textsf{id}_X$
, which is realized by
$(s_A,\textsf{id})$
. The underlying functor of
$F^{-1}$
is also
$\textsf{id}_X$
, this time realized by
$(r_A,\Pi (\rho _A))$
.
In addition to the above, we also allow the underlying groupoids of partitioned groupoidal assemblies to be locally small (objects of
$\mathbf{GPD}$
). The realizer category is also assumed to be locally small, which means that the fundamental groupoid functor
$\Pi :\mathbf{R}\rightarrow \mathbf{Gpd}$
lands in small groupoids, and further, that the category of presheaves
$\widehat{\Pi A}$
on any fundamental groupoid is locally small (and thus able to be the underlying groupoid of a partitioned groupoidal assembly).
Van den Berg (Reference van den Berg2018
Reference van den Bergb) defines a notion of representation for a subclass
$\mathscr{S}$
of fibrations (called “small” fibrations) that contains all isomorphisms and is closed under composition and homotopy pullbacks along arbitrary maps. A representation models a type-theoretic universe where small types are interpreted as small fibrations. The universe is impredicative iff the (weak) dependent product
$\Pi _\alpha (f) \in \mathscr{S}$
whenever
$\alpha$
is a fibration and
$f\in \mathscr{S}$
. We will now show that
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I},U)$
has an impredicative universe of 1-types, where the small types are modest fibrations.
Definition 19.
A modest fibration is a fibration
$M:Y\rightarrow X$
such that for all
$x:\mathbf{1}\rightarrow X$
the pullback
is modest in the sense of Definition 11 , that is, the realizability functor
\begin{align*}{\left \Vert -\right \Vert }_{Y_x} :={\left \Vert -\right \Vert }_Y \circ \pi _2 : Y_x \rightarrow \Pi U \end{align*}
for each of the fibers
$Y_x$
is fully faithful.
Remark 20.
Suppose that
$M:Y \rightarrow X$
is a modest fibration. Is the splitting
of
$M$
again a modest fibration? By Brown’s lemma it is: Take any
$x:\mathbf{1} \rightarrow X$
. Then, by Brown’s lemma,
\begin{align*} x^* S : \widetilde{Y}_x \rightarrow Y_y \end{align*}
is an equivalence between the fibers. The realizability functor of
$\widetilde{Y}_x$
is given by:
\begin{align*}{\left \Vert -\right \Vert }_{\widetilde{Y}_x} &:={\left \Vert -\right \Vert }_Y \circ S \circ i_{\widetilde{Y}_x} \\ &={\left \Vert -\right \Vert }_Y \circ i_{Y_x} \circ x^* S \\ &={\left \Vert -\right \Vert }_{Y_x} \circ x^* S \end{align*}
(where
$i$
’s denote inclusions of fibers into total groupoids), which is, as the composition of two fully faithful functors, itself fully faithful.
It is clear that isomorphisms are modest fibrations. By the pullback lemma, modest fibrations are closed under pullback.
Proposition 21. Modest fibrations are closed under composition.
Proof.
Let
$F: X \rightarrow Y$
and
$G: Y \rightarrow Z$
be modest fibrations. We want to show that the fiber
$X^{GF}_z$
of
$GF$
over
$z$
is modest for any
$z\in Z$
.
For faithfulness, take
$x,x^{\prime}\in X^{GF}_z$
and
$\alpha : \left \Vert x \right \Vert _X \rightarrow \left \Vert x^{\prime} \right \Vert _X \in \Pi U$
. We want a morphism
$p:x \rightarrow x^{\prime} \in X^{GF}_z$
such that
$\left \Vert p \right \Vert _X = \alpha$
. Suppose that
$(e,\epsilon ) \Vdash F$
. Then we have a path
We know that
$Fx. Fx^{\prime}\in Y^G_z$
are both in the fiber of
$G$
over
$z$
, so by fullness of
$\left \Vert -\right \Vert _{Y_z}$
we get a morphism
$q: Fx \rightarrow Fx^{\prime} \in Y^G_z$
. Now, the transport
$q^* x$
and
$x^{\prime}$
are both in the fiber
$X^F_{Fx^{\prime}}$
, and we have a path
$\alpha \circ \left \Vert \overline{g}(x)^{-1} \right \Vert _X : \left \Vert g^* x \right \Vert _X \rightarrow \left \Vert x^{\prime} \right \Vert _X$
. So by fullness of
$\left \Vert -\right \Vert _{X_{Fx^{\prime}}}$
, we get a morphism
$r: g^* x \rightarrow x^{\prime} \in X^F_{Fx^{\prime}}$
. So we take
$p := r \circ \overline{q}(x)$
. Clearly,
\begin{align*} \left \Vert p \right \Vert _X = \left \Vert r \right \Vert _X \circ \left \Vert \overline{q}(x) \right \Vert _X = \alpha \circ \left \Vert \overline{q}(x)^{-1} \right \Vert _X \circ \left \Vert \overline{q}(x) \right \Vert _X = \alpha \end{align*}
and
\begin{align*} G(F(p)) = G \left (F\left (r\circ \overline{q}(x) \right ) \right ) = G(q) = z \end{align*}
For faithfulness, suppose
$p,q: x \rightarrow x^{\prime} \in X^{GF}_z$
such that
$\left \Vert p \right \Vert _{X} = \left \Vert q \right \Vert _{X}$
. We want to show that
$p=q$
. We know that
$F(p), F(q)\in Y^G_z$
. So we know that
$\left \Vert F(p) \right \Vert _Y = \left \Vert F(q) \right \Vert _Y$
.
By faithfulness of
$\left \Vert -\right \Vert _{Y_z}$
we infer that
$F(p)=F(q)=: r$
. Then
$r^* x, x^{\prime} \in X^F_{Fx^{\prime}}$
and we have maps
\begin{align*} &p \circ{\overline{r}(x)}^{-1} &&q \circ{\overline{r}(x)}^{-1} \end{align*}
such that
\begin{align*} \left \Vert p \circ{\overline{r}(x)}^{-1} \right \Vert _X = \left \Vert q \circ{\overline{r}(x)}^{-1} \right \Vert _X \end{align*}
By faithfulness, we deduce
$p \circ{\overline{r}(x)}^{-1} = q \circ{\overline{r}(x)}^{-1}$
and thus
$p=q$
.
We will now explain what a representation for modest fibrations amounts to. A representation
$\theta$
for modest fibrations is a modest fibration
$\theta :\Theta \rightarrow \Lambda$
such that for every modest fibration
$M:Y \rightarrow X$
there is a map
$M_*: Y \rightarrow \Theta$
such that
$\theta \circ M_* = \nu _M \circ M$
and such that the induced map
$\left [ M_*, M \right ] : Y \rightarrow P$
is an equivalence
$M \simeq (\nu _M)^*\theta$
in
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I},U)$
.
Theorem 22.
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I},U)$
has a representation for modest fibrations.
Before giving the proof, we first define the “chaotic” inclusion
\begin{align*} \nabla :\mathbf{GPD} \rightarrow \mathbf{PGAsm}(\mathbf{R},\mathbb{I},U) \end{align*}
of groupoids into partitioned groupoidal assemblies. Choose an arbitrary
$a_0\in \Pi U$
and set
\begin{align*} \nabla X &:= \left ( X,{\left \Vert -\right \Vert }_{\nabla X} : p \mapsto a_0 \right ) \\ \nabla (F) &:= F \end{align*}
where
$\nabla (F)$
—in fact any functor into an object in the image of
$\nabla$
– is realized by
$(a_0*,\textsf{id})$
(i.e.,
$\nabla$
is right adjoint to the underlying groupoid functor).
Proof of Theorem 22. Define
\begin{align*} \Lambda := \nabla \widehat{\Pi U} \end{align*}
where
$\widehat{\Pi U}$
is the groupoid of
$\mathbf{Bij}$
-valued presheaves on
$\Pi U$
.
The underlying groupoid of
$\Theta$
has as objects pairs
$(F, a)$
, where
$F\in \widehat{\Pi U}$
and
$a\in \Pi U$
is such that
$Fa\neq \emptyset$
. A morphism
$(\psi, \alpha ): (F,a)\rightarrow (G,b)$
consists of a natural isomorphism
$\psi :F\Rightarrow G$
and a path
$\alpha : a\rightarrow b$
. The realizability functor
${\left \Vert -\right \Vert }_\Theta$
is given by the second projection. The modest fibration
$\theta :=\pi _1:\Theta \rightarrow \Lambda$
is given by the first projection. Fix
$(F,a)$
and
$(F,b)$
in the fiber over
$F\in \Lambda$
. Every
$\alpha :a\rightarrow b$
in
$\Pi U$
uniquely determines a morphism
$(\textsf{id}_F,\alpha )$
in the fiber over
$F$
. The chosen lift of
$\psi :F\rightarrow G$
at
$(F,a)$
is
$(\psi, \textsf{id}_a):(F,a) \rightarrow (G,a)$
.
Let
$M:Y\rightarrow X$
be a modest fibration. By Remark 20, we can (using AC) take
$M$
to be split. Define the object part of its characteristic map
$\nu _M:X \rightarrow \Lambda$
of
$M$
as follows. First,
\begin{align*} \nu _M(x)(a) := \left \{ \alpha :a\rightarrow a^{\prime} \mid \exists y\in Y. \, My=x \land \Vert y \Vert _Y = a^{\prime} \right \}\diagup{\sim } \end{align*}
where the relation
$\sim$
is isomorphism in the coslice above
$a$
. Then
\begin{align*} &\nu _M(x)(\beta :a\rightarrow b)[\alpha ] := [\alpha \circ \beta ^{-1}] \end{align*}
To define
$\nu _M(p:x\rightarrow x^{\prime})(\beta, i)[\alpha ]$
, we pick a representative
$\alpha :a\rightarrow c$
from
$[\alpha ]$
. Further, we pick
$y_x^{c}\in Y$
such that
$M(y_x^{c})=x$
and
$\left \Vert y_x^{c} \right \Vert _Y = c$
. Using the fact that
$M$
is an isofibration, we define
\begin{align*} \nu _M(p:x\rightarrow x^{\prime})(\beta, i)[\alpha ] := \left [{\left \Vert \overline{p}\left ( y_x^{c} \right ) \right \Vert }_Y \circ \alpha \circ \beta ^{-1} \right ] \end{align*}
The following diagram helps visualize this definition.
This definition is independent of the choices made. Let
$\alpha ^{\prime}:a\rightarrow d$
be a element of
$[\alpha ]$
isomorphic to
$\alpha$
in the coslice above
$a$
, and let
$y^d_x \in Y$
be a choice of element such that
$M(y_x^{d})=x$
and
${\left \Vert y_x^{d} \right \Vert }_Y = d$
. Then by modesty of
$M$
, we have an isomorphism
$y_x^{c} \rightarrow y_x^{d}$
. Transporting this isomorphism along
$p$
and applying
${\left \Vert -\right \Vert }_Y$
yields an isomorphism
\begin{align*} \left \Vert \overline{p}\left ( y_x^{c} \right ) \right \Vert _Y \circ \alpha \circ \beta ^{-1} \rightarrow \left \Vert \overline{p}\left ( y_x^{d} \right ) \right \Vert _Y \circ \alpha \circ \beta ^{-1} \end{align*}
in the coslice above
$b$
.
To show that
$\nu _M(x)$
is functorial, first note that
$\nu _M(\textsf{id}_x)(\beta, i)[\alpha ] = [\alpha \circ \beta ^{-1}]$
. For composition, we exhibit an isomorphism between
\begin{align*} \left \Vert \overline{qp}\left ( y_x^{c} \right ) \right \Vert _Y \circ \alpha \circ \beta ^{-1} \end{align*}
and
\begin{align*} \left \Vert \overline{p}\left ( y_{x^{\prime}}^{\left \Vert p^* y^c_x \right \Vert _Y} \right ) \right \Vert _Y \circ \left \Vert \overline{p}\left ( y_x^{c} \right ) \right \Vert _Y \circ \alpha \circ \beta ^{-1} \end{align*}
in the slice over
$b$
, where
$y_{x^{\prime}}^{\left \Vert p^* y^c_x \right \Vert _Y}$
is a chosen element such that:
\begin{align*} M\left (y_{x^{\prime}}^{\left \Vert p^* y^c_x \right \Vert _Y}\right ) &= x^{\prime} \\ \left \Vert y_{x^{\prime}}^{\left \Vert p^* y^c_x \right \Vert _Y} \right \Vert _Y &= \left \Vert p^* y^c_x \right \Vert _Y \end{align*}
Given that
$p^* y^c_{x^{\prime}}$
and
$y_{x^{\prime}}^{\left \Vert p^* y^c_x \right \Vert _Y}$
are both in the fiber over
$x^{\prime}$
and the image of each under
${\left \Vert -\right \Vert }_Y$
is
$\left \Vert p^* y^c_x \right \Vert _Y$
, by the fullness of
${\left \Vert -\right \Vert }_Y$
we obtain an isomorphism:
\begin{align*} \left \Vert p^* y^c_x \right \Vert ^{-1}_Y : p^* y^c_{x^{\prime}} \rightarrow y_{x^{\prime}}^{\left \Vert p^* y^c_x \right \Vert _Y} \end{align*}
Transporting this isomorphism along
$q$
and then applying
${\left \Vert -\right \Vert }_Y$
gives the desired isomorphism.
The pullback
$P := X \times _\Lambda \Theta$
has objects of the form
$(x,a)$
(we omit the component
$\nu _M(x)$
that is determined by (
$x$
) and morphisms of the form
$(p,\alpha )$
. To show that
$M$
is equivalent to
$(\nu _M)^*\theta$
, we first construct
$M_*:Y\rightarrow \Theta$
:
\begin{align*} M_*(y) &:= \left ( \nu _M(My), \left \Vert y \right \Vert _Y \right ) \\ M_*(q) &:= \left ( \nu _M(M(q)), \left \Vert q \right \Vert _Y \right ) \end{align*}
This is realized by
$(\textsf{id},\textsf{id})$
and indeed satisfies
$\nu _M \circ M = \theta \circ M_*$
. So we get the universal map
$[M_*,M]$
.
Now we define a pseudoinverse
$M^*:P\rightarrow Y$
to
$[M_*,M]$
. Given
$(x,a)\in P$
, we choose an element
$[\gamma _{x,a}] \in \nu _M(x)(a)$
and a representative
$\gamma _{x,a}: a \rightarrow c_{x,a}$
from
$[\gamma _{x,a}]$
(we know
$\nu _M(x)(a)$
is non-empty). Moreover,
$\upsilon (\gamma _{x,a}) \in Y$
is a chosen element such that
$M(\upsilon (\gamma _{x,a})) = x$
and
$\left \Vert \upsilon (\gamma _{x,a}) \right \Vert _Y = c_{x,a}$
.
With this, on objects we define
\begin{align*} M^*\left (x,a\right ) := \upsilon \left (\gamma _{x,a}\right ) \end{align*}
Now take a morphism
$\left (p,\alpha \right ): \left (x,a\right )\rightarrow \left (x^{\prime},b\right ) \in P$
. We would like to define its image under
$M^*$
to be
\begin{align} \overline{p}\left ( \upsilon \left (\gamma _{x,a}\right ) \right ): \upsilon \left (\gamma _{x,a}\right ) \rightarrow p^* \upsilon \left (\gamma _{x,a} \right ) \end{align}
but it is not necessarily the case that
\begin{align} p^* \upsilon \left (\gamma _{x,a} \right ) = \upsilon \left (\gamma _{x^{\prime},b}\right ) \end{align}
that is, the codomain may not align. Here, we utilize modesty. Consider the following commutative diagram in
$\Pi U$
.
We know that
\begin{align*} p^* \upsilon (\gamma _{x,a}), \upsilon (\gamma _{x^{\prime},b}) \in Y_{x^{\prime}} \end{align*}
and we have the morphism:
\begin{align*} \delta _{p,\alpha }: \left \Vert p^* \upsilon \left (\gamma _{x,a} \right ) \right \Vert _Y \rightarrow c_{x^{\prime},b} = \left \Vert \upsilon \left (\gamma _{x^{\prime},b}\right ) \right \Vert _Y \end{align*}
Thus, using fullness, we obtain a morphism:
\begin{align*} \left \Vert \delta _{p,\alpha } \right \Vert ^{-1}_Y : p^* \upsilon \left (\gamma _{x,a} \right ) \rightarrow \upsilon \left (\gamma _{x^{\prime},b}\right ) \end{align*}
in the fiber
$Y_{x^{\prime}}$
. Therefore, we can define
\begin{align*} M^*\left (p,\alpha \right ) :={\left \Vert \delta _{p,\alpha } \right \Vert }^{-1}_Y \circ \overline{p}\left ( \upsilon \left (\gamma _{x,a}\right ) \right ) \end{align*}
which reduces to (5) in case (6) holds. Faithfulness ensures this is functorial.
$M^*$
is realized by
$(\pi _2 \circ r_{U\times U}, \epsilon )$
, where
$\epsilon _{(x,a)} := \gamma _{x,a} \circ \rho _a$
.
There is a natural isomorphism
$\sigma : \textsf{id}_Y \Rightarrow M^* [M_*,M]$
, defined
\begin{align*} \sigma (q,i) := \left \Vert \gamma _{My^{\prime},\left \Vert y^{\prime} \right \Vert _Y} \right \Vert ^{-1}_Y \circ q \end{align*}
and realized by
$( \pi _1 r_{U\times U}, \epsilon )$
, where
\begin{align*} \epsilon _{(y,0)} &:= \left ( \left \langle{\left \Vert -\right \Vert }_Y, {\left \Vert -\right \Vert }_{\mathbf{I}_1} \right \rangle \ast \Pi \left ( \rho _{U\times U} \right ) \ast \Pi (\pi _1) \right )_{(y,0)} \\ \epsilon _{(y,1)} &:= \gamma _{My,{\left \Vert y \right \Vert }_Y} \circ \epsilon _{(y,0)} \end{align*}
Conversely, there is a natural isomorphism
$\tau : \textsf{id}_P \Rightarrow [M_*,M] M^*$
, defined
\begin{align*} \tau \left (\left (p, \alpha \right ), i\right ) := \left ( p, \gamma _{x^{\prime},b} \circ \alpha \right ) \end{align*}
and realized by
$( \pi _1 r_{U\times U}, \epsilon ^{\prime})$
, where
\begin{align*} \epsilon ^{\prime}_{\left ( \left (x, a \right ), 0 \right )} &:= \left ( \left \langle{\left \Vert -\right \Vert }_P, {\left \Vert -\right \Vert }_{\mathbf{I}_1} \right \rangle \ast \Pi \left ( \rho _{U\times U} \right ) \ast \Pi (\pi _1) \right )_{\left ( \left (x, a \right ), 0 \right )} \\ \epsilon ^{\prime}_{\left ( \left (x, a \right ), 1 \right )} &:= \left ( \textsf{id}_x, \textsf{id}_{\nu _M(x)}, \gamma _{x^{\prime},b} \right ) \circ \epsilon ^{\prime}_{\left ( \left (x, a \right ), 0 \right )} \end{align*}
To round off the impredicative universe, we have
Theorem 23.
Let
$F: Y \rightarrow Z$
be a fibration and
$G: X \rightarrow Y$
be a modest fibration. Then the dependent product
$\Pi _F(G): \Pi _F X \rightarrow Z$
is a modest fibration.
Proof.
The argument is similar to that at the end of the proof of Proposition 12. Given
$(z,H,e,\epsilon ), (z,H^{\prime},e^{\prime},\epsilon ^{\prime}) \in (\Pi _F X)_z$
and
$(y,u)\in F\downarrow z$
, we know that
$H(y,u)$
and
$H^{\prime}(y,u)$
are both in the fiber
$X^G_y$
by the commutativity of (4). Then any
$f:e \rightarrow e^{\prime}$
uniquely determines a morphism
$(\textsf{id}_z, \psi, f) \in (\Pi _F X)_z$
because
${\left \Vert -\right \Vert }_{X_y}$
is fully faithful: the image of the component
$\psi _y$
under
${\left \Vert -\right \Vert }_{X_y}$
is the unique morphism making the following square commute.
5. Outlook
We have exhibited a model of 1-truncated intensional type theory with an impredicative universe of 1-types in the category
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I},U)$
of partitioned groupoidal assemblies over the untyped realizer category
$(\mathbf{R},\mathbb{I},U)$
. This generalizes set-based partitioned assemblies over a cartesian closed category. More broadly, we have opened the door to a categorical treatment of higher-dimensional realizability—where realizers themselves carry higher-dimensional structure. One could consider alternative classes of fibrations in
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I},U)$
. For instance, one might take fibrations to be given by the homotopy lifting property, which would be tantamount to the lifting operation being realized.
Ultimately, we would like to investigate groupoidal analog of assemblies (not necessarily partitioned) and realizability topoi (as well as modest sets and PERs). These could be studied directly or as free completions of partitioned groupoidal assemblies. Shulman (Reference Shulman2021) has studied two-dimensional regular and exact completions. One can take the regular or exact completion of any finitely complete 2-category.
-
• Is the exact completion of
$\mathbf{PGAsm}(\mathbf{R},\mathbb{I},U)$
an elementary (non-Grothendieck) (2,1)-topos?
To be sure, we do not seek a 1-topos but a (2,1)-topos; it is two-dimensional regular and exact completions that are relevant. A result due to Lumsdaine (Reference Lumsdaine2011) states that in any coherent 1-category, any cocategory is a co-equivalence relation, that is, it is a cogroupoid whose end point maps are jointly epimorphic—in terms of fundamental groupoids, this means that any two parallel paths are equal. We escape this limitation in the higher setting: for example, the (2,1)-category
$\mathbf{Gpd}$
is a (2,1)-topos but contains a cogroupoid that is not a co-equivalence relation (Example 4). On the other hand, van den Berg and Moerdijk (Reference van den Berg and Moerdijk2018) study the “homotopy exact completion”
$\mathbf{Hex}(\mathbf{C})$
of a path category
$\mathbf{C}$
, which turns out to be equivalent to the ex/lex completion
${\mathbf{Ho}(\mathbf{C})}_{\textsf{ex/lex}}$
of the homotopy category
$\mathbf{Ho}(\mathbf{C})$
of
$\mathbf{C}$
(their Proposition 3.18).
We would like to know what principles are valid in these putative models.
-
• Do they contain impredicative and univalent universes?
-
• What about propositional resizing?
-
• Church’s thesis?
A model with an impredicative universe and function extensionality contains refined encodings of (higher) inductive types that satisfy their full universal property (Awodey et al., Reference Awodey, Frey and Speight2018).
Beyond this, we would like to find more examples of untyped realizer categories or else generalize untyped realizer categories to admit more examples. In particular, we would like to do groupoidal realizability over:
-
• higher-dimensional untyped
$\lambda$
-calculi, such as a cubical untyped
$\lambda$
-calculus (roughly, an untyped version of a much stripped back version of cubical type theory Cohen et al. (Reference Cohen, Coquand, Huber and Mörtberg2015)); -
• two-dimensional models of the untyped
$\lambda$
-calculus, that is, cartesian closed bicategories with a pseudoreflexive object (these include generalized species of structures (Fiore et al., Reference Fiore, Gambino, Hyland and Winskel2008), a profunctorial Scott semantics (Galal, Reference Galal and Ariola2020), and categorified relational (distributors-induced) (Olimpieri, Reference Olimpieri2021) and graph models (Kerinec et al., Reference Kerinec, Manzonetto and Olimpieri2023)); -
• partial computable functors over finite sets (beefed-up natural numbers).
Finally, we would eventually like to investigate weak
$\infty$
-groupoidal realizability. This should use a weaker notion of interval compared with that used here, in that the cogroupoid axioms should be allowed to hold up to homotopy; it should accomodate
$[0,1] \in \mathbf{Top}$
—with no quotienting by homotopy. For further discussion of future work, see Speight (Reference Speight2023).
Acknowledgments
The authors thank Samson Abramsky, Carlo Angiuli, Steve Awodey, Robert Harper, Andrzej Murawski, Michael Shulman, Benno van den Berg, and Michael Warren for helpful discussions.
The research presented here was carried out during the author’s DPhil at the University of Oxford, under the supervision of Samson Abramsky. For some of that time, the author was supported by an EPSRC Doctoral Training Partnership Studentship. The author’s affiliation changed to University of Birmingham before preparation of the paper.
Open access
