Note for the Budapest Seminar on Two Sortification
This note contains the outline of what I expect to talk about in the Budapest Type Theory Seminar on two sortification. The collapsible sections with (Memo) in the title give a quick remainder of a classical concept.
Two Sortification
Two-sortification consists in transforming a GAT to a GAT with only 2 sorts \((U : \mathbf{Set}, El : U \to \mathbf{Set})\). For example, the GAT of transitive graphs:
V : Set E : V → V → Set T : (x y z : V) → E x y → E y z → E x z
is translated to
U : Set El : U → Set V : U E : El V → El V → U T : (x y z : El V) → El (E x y) → El (E y z) → El (E x z)
Motivational Examples
Two-sortification is a technique that already appears in the litterature:
- Altenkirch and Scoccola use it to give an HIT definition of integers
- Altenkirch, Kaposi and Xie use it to formalize intrinsic dependent type theory in cubical agda.
HIT Definition of Integers
Integers can be generated using a base point 0 and an equivalence \(s : \mathbb{Z} \cong \mathbb{Z}\). In this presentation, \(s^{-1}\) is the predecessor. This can be expressed using an HIT as follows.
data ℤ : Set where zero : ℤ loop : ℤ = ℤ
However, this is not a valid HIT as loop mentions Z which is not yet
defined. Two-sortification can be used to eliminate sort equations.
data U : Set data El : U → Set data U where ℤ : U loop : ℤ = ℤ data El where zero : El ℤ
Intrinsic Syntax of Dependent Type Theory
Cannot define a CwF in Cubical Agda as the equations in Ty refer to the constructors of
Sub, but the constructors of Sub refer to the constructors of Ty.
data Con : Set data Ty : Con → Set data Sub : Con → Con → Set data Con where ◇ : Con _▷_ : (Γ : Con) → Ty Γ → Con data Ty where _[_] : Ty Γ → Sub Δ Γ → Ty Δ []-id : A [ id ] = A []-funct : A [ γ ] [ δ ] = A [ γ ⚬ δ ] ... data Sub where id : Sub Γ Γ _⚬_ : Sub Δ Γ → Sub Ξ Δ → Sub Ξ Γ _,_ : (γ : Sub Δ Γ) → Tm Δ (A [ γ ]) → Sub Δ (Γ ▷ A) ...
Two-sortification can be used to eliminate interleaving.
data U : Set data El : U → Set data U where Con : U Ty : El Con → U Sub : El Con → El Con → Set data El where ◇ : El Con _▷_ : (Γ : El Con) → El (Ty Γ) → El Con _[_] : El (Ty Γ) → El (Sub Δ Γ) → El (Ty Δ) _,_ : (γ : Sub Δ Γ) → Tm Δ (A [ γ ]) → Sub Δ (Γ ▷ A) id : El (Sub Γ Γ) []-id : A [ id ] = A _⚬_ : El (Sub Δ Γ) → El (Sub Ξ Δ) → El (Sub Ξ Γ) []-funct : A [ γ ] [ δ ] = A [ γ ⚬ δ ] ...
GATs
Justify this trick, i.e., show that if the two-sortified GAT has an initial model (a QIIT), then the original GAT is also equipped with an initial model (a QIIT).
What is a GAT?
The category FinGat of finite generalized algebraic theories is the category of contexts and substitutions of the type theory generated by a universe of types, extensional equality types and dependent products over types.
Our universe of types is Set. It has dependent products and extensional equality.
Dependent Products in Set (Memo)
Given a family \(A : I \to \mathbf{Set}\), the dependent product is defined as: \[ \Pi I A := \{ u : I \to \bigcup_{i \in I} A_i \mid \forall i \in I.\ u i \in A_i \} \]
Dependent Sum in Set (Memo)
Given a family \(A : I \to \mathbf{Set}\), the dependent sum is defined as: \[ \Sigma I A := \{ (i, a) \mid i \in I, a \in A_i \} \]
What is a Model of a GAT?
We use Uemura's characterisation of GATs:
The category FinGat is bi-initial in the category CartExp of finitely complete categories with a chosen dependent product .
Finitely Complete Category (Memo)
A category is said finitely complete if it has all limits. Equivalently, it is finitely complete if it has all pullbacks and a terminal object. We will only use the second characterisation in this talk.
For any category \(C\) in CartExp, there exists a CartExp-morphism between FinGat and \(C\). Moreover, any pair of such functors are naturally (uniquely) isomorphic.
Questions raised by this theorem and this definition:
- What does it mean for a category to have a dependent product?
- What is the dependent product in FinGat?
- What are the morphisms of CartExp?
Dependent product
We need an abstract way of defining dependent products such that, in Set, it corresponds to the concrete definition we gave previously.
Let \(C\) be a finitely complete category and \(f : Y \to X\). The pullback functor \(f^* : C/X \to C/Y\) (where \(C/X\) is the slice category \(C\) over \(X\)) that sends \(g : Z \to X\) to the first projection of the pullback between \(f\) and \(g\):
The action on morphism is defined by the universal property of pullbacks.
Slice Category (Memo)
Let \(C\) be a category and \(X : C\). The slice category \(C/X\) has:
- morphisms \(f : Y \to X\) as objects, and
- given \(f : Y \to X\) and \(g : Z \to X\), commuting triangles as morphisms:
A slice category \(C/X\) has pullbacks whenever \(C\) has pullbacks. They are computed as the pullbacks in the underlying category. The identity function is the terminal object of a slice category.
Let \(C\) be a finitely complete category and \(f : Y \to X\). The dependent product \(\Pi_f : C/Y \to C/X\) of \(f\) is the right adjoint of \(f^*\) (if it exists).
The dependent product of \(f\) is also called the pushforward of \(f\).
But why is this a dependent product?
From a category-theoretic perspective. One can think of the pullback functor \(f^*\) as the binary product in \(C/X\) of \(f\) together with the input morphism \(g : C/X\). Indeed, the binary products in a slice category are exactly the pullbacks in the underlying category. Then, the right adjoint of the pullback functor can be seen as the right adjoint to the binary product functor, which is the exponential object, i.e., a function that is indexed due to the slice.
Let \(C\) be a finitely complete category and \(f : Y \to X\). \(f\) is said to be exponentiable if the pullback functor \(f^*\) has a right adjoint.
From a type theoretic perspective. We can view adjoints as "approximations" of categories. A right adjoint is a "conservative approximation", whereas a left adjoint is a "liberal approximation". For instance, let us look at the embedding functor \(\iota : \mathbb{N} \to \mathbb{R}\). We have: \[ \lceil \cdot \rceil \dashv \iota \dashv \lfloor \cdot \rfloor \] Here, the left adjoint overestimates (is "liberal") while the right adjoint underestimates (is "conservative") the integer unless it is already an integer. We will see that the usual dependent product in type theory is the "conservative approximation" of a well-chosen morphism.
Consider the following semantics of type theory: let \(C\) be the category of contexts and substitutions. We define \(\textsf{Ty}\ \Gamma := C/\Gamma\), i.e., a type is a morphism between contexts. We have \(A : \textsf{Ty}\ \Gamma\) if \(A : \Gamma \triangleright A \to \Gamma\). In this sense, if \(A : \textsf{Ty}\ \Gamma\) and \(\sigma : \Delta \to \Gamma\), we can define \(A[\sigma] : \textsf{Ty}\ \Delta\) by the following pullback:
The usual dependent product in type theory is the "conservative approximation" of the weakening substitution \(p : \Gamma \triangleright A \to \Gamma\). Indeed, the "conservative approximation" asks that, in order to make a type over \(\Gamma\) from a type over \(B\) over \(\Gamma \triangleright A\), we must be able to produce a term of type \(B[\langle a \rangle]\) (where \(\langle a \rangle : \Gamma \to \Gamma \triangleright A\)) from each term \(a\) of type \(A\). Conversely, the usual dependent sum is the "liberal approximation" of \(p\). Indeed, in this case, the left adjoint simply asks that there is at least one term \(a\) of type \(A\) for which we can produce a term of type \(B[\langle a \rangle]\).
Another way to see this (this was remarked by Niels during the talk) is that:
- the unit of the adjunction \(f^* \dashv \Pi_f\) defines the λ-abstraction, and
- the counit of the adjunction defines the application.
Checking the Definition in Set
We can verify that the dependent product and the dependent sum defined as left and right adjoints of the weakening substitution yield the same sets as those aforementioned.
Let us consider a displayed family \(\varphi : B \to \Gamma \triangleright A\). By definition, we have \(B_{\gamma,a} := \{ b \in B \mid \varphi(b) = \gamma , a\}\). The set \((\Sigma_p B)_\gamma\) is then, again by definition, \(\{ b \in B \mid p(\varphi(b)) = \gamma\}\). In fact, if \(p(\varphi(b)) = \gamma\), then there must exist an \(a \in A_\gamma\) such that \(\varphi(b) = \gamma , a\). Hence: \[ (\Sigma_p B)_\gamma := \{ b \in B \mid \exists (a : A_\gamma).\ \varphi(b) = \gamma , a \} \cong \{ (a, b) \mid a \in A_\gamma, b \in B_{\gamma, a}\} \]
Moreover, in this case, we can directly show that the following expected dependent product: \[ (\Pi_p B)_\gamma := \{ u : A_\gamma \to \bigcup_{a \in A_\gamma} B_{\gamma,a} \mid \forall a \in A_\gamma.\ u a \in B_{\gamma,a} \} \] is a right adjoint to \(p^*\). Indeed, given \(\varphi : B \to \Gamma\), \(p^* B = \{ (\gamma, a, b) \mid \varphi(b) = \gamma\}\), i.e., \[ p^* B = \{ (\gamma, a, b) \mid \gamma \in \Gamma, a \in A_\gamma, b \in B_{\gamma,a}\}. \] Then, giving the bijection between \(p^* B \to C\) and \(B \to \Pi_p C\) (where \(\psi : C \to \Gamma \triangleright A\)) is easy:
- Let \(h : p^* B \to C\), then given \(\gamma : \Gamma\) and \(b : B_\gamma\), we have to give a function \(u : A_\gamma \to \bigcup_{a \in A_\gamma} C_{\gamma, a}\). Let \(a : A_\gamma\), then \((\gamma, a, b)\) is an element of \(p^* B\) and yields an element \(c : C\) such that \(\psi(c) = \gamma, a\). But then, \(c \in \bigcup_{a \in A_\gamma} C_{\gamma, a}\) and so \(u := \lambda a.\ h(\gamma, a, b)\).
- Let \(h : B \to \Pi_p C\), then given \((\gamma, a, b)\) in \(p^* B\), we have to give a \(c : C\) such that \(c \in C_{\gamma, a}\). As \(b \in B_\gamma\), \(h(b)\) is a function from \(A_\gamma\) to \(\bigcup_{a \in A_\gamma} C_{\gamma, a}\) s.t. \(h(b)(a) \in C_{\gamma, a}\).
By definition, this is indeed an isomorphism between \(p^* B \to C\) and \(B \to \Pi_p C\).
Chosen Exponentiable Arrow in FinGat
The "universal" exponentiable arrow in FinGat (the one that makes FinGat a bi-initial object of CartExp) is the weakening \(p : 1/\textbf{Set} \to \textbf{Set}\), which sends \((A : \textbf{Set}, a : A)\) to \(A : \textbf{Set}\).
Note that it is not always convenient to work in slice categories. Consequently, instead of considering the pullback functor, we may consider polynomial functors instead:
- \(Q_f : C \to C/X\), right adjoint to \(dom \circ f^* : C/X \to C\) or even
- \(P_f : C \to C\), right adjoint to \(dom \circ f^* \circ \Delta : C \to C\) where \(\Delta\) sends \(X\) to the first projection \(X \times X \to X\).
It suffices that one of these functor has a right adjoint for all of them to have one. We will mostly work with the small polynomial functor, allowing us to forget one side of the slice.
Then, one can check that \(Q_p : \textbf{FinGat}/\textbf{Set} \to \textbf{FinGat}\) has a right adjoint sending \(G : \textbf{FinGat}\) to \(\mathrm{Fam}(G)\) together with the family fibration.
Fam(C) and FamilyFibration (Memo)
The category \(\mathrm{Fam}(C)\) has:
- \((U : \textbf{Set}, \mathrm{El} : U \to C)\) as objects, and
- \((f : U \to V, g : \forall (u : U).\ \mathrm{El}\ u \to \mathrm{El'}\ f(u))\) as morphisms.
We usually write \(\mathrm{Fam}\) for \(\mathrm{Fam}(\textbf{Set})\). The family fibration of \(\mathrm{Fam}(C)\) is the functor sending \((U : \textbf{Set}, \mathrm{El} : U \to C)\) to \(U : \textbf{Set}\).
Morphisms of CartExp
What is the right notion of morphisms for CartExp? The objects of the category are finitely complete categories with a chosen exponentiable arrows. The natural notion of morphism would be a functor that preserves finite limits and the exponentiable morphism. However, this is not quite enough, as our primary focus is on the dependent products, not really on the exponentiable arrows themselves. Hence, a CartExp morphism between two CartExp \(C\) and \(D\) is a functor \(F : C \to D\) such that:
- \(F\) preserves finite limits,
- \(F\) preserves the exponentiable arrow, i.e., \(Fp_C \cong p_D\), and
- \(F\) commutes with the polynomial functor, i.e., \(P_{p_D}F \cong FP_{p_C}\).
Note that the isomorphism of Point (2) is in the arrow category.
Arrow Category (Memo)
Let \(C\) be a category. The arrow category \(C^{\to}\) has:
- morphisms \(f : X \to Y\) as objects, and
- given \(f : X \to Y\) and \(g : X' \to Y'\), commuting squares as morphisms:
A CartExp-functor \(F : C \to D\) is strict if \(Fp_C \cong p_D\) is the identity. Given any CartExp \(C\) with exponentiable arrow \(p_C : Y \to X\), if \(Y \neq X\) then any CartExp morphism from \(C\) is naturally isomorphic to a strict one. In particular, there exists a strict morphism from FinGat to any CartExp category.
Proof.
Let \(F : C \to D\). We construct the strictified CartExp-morphism as follows:
- \(F'(c) = \begin{cases} X_D & \text{if } c = X_C \\ Y_D & \text{if } c = Y_C \\ F(c) & \text{otherwise}\end{cases}\)
- \(F'(f : Y \to X) = \begin{cases} p_D & \text{if } f = p_C \\ i \circ Ff & \text{if } X = X_C \\ Ff \circ i & \text{if } Y = Y_C \\ Ff & \text{otherwise}\end{cases}\)
Note that this proof is only suitable for small categories. We can lift this proof to a more generic setting by using the Theorem 2 of Joyal and Street.
Model of a GAT
The category of categories Cat is in CartExp. Indeed, the weakening functor \(p : 1/\textbf{Set} \to \textbf{Set}\) is exponentiable in Cat (with the same right adjoint as the one in FinGat).
The model functor \([\![-]\!] : \textbf{FinGat} \to \textbf{Cat}\) is the strict initial functor between FinGat and Cat in CartExp.
Two-Sortification
We use strict bi-initiality to define the two-sortification functor. We need to:
- Find a category whose objects are "family GATs", i.e., GATs with only two sorts \(U : \mathbf{Set}, \mathrm{El} : U \to \mathbf{Set}\),
- Equip this category with a CartExp structure.
Family GATs
Family GATs can be defined as the least set containing Fam and closed under certain pullbacks and equalizers. However, we leave the definition vague, and characterise them as follows.
The category FamGat is the full subcategory of FinGat/Fam spanned by family GATs.
Full Subcategory (Memo)
\(D\) is a full subcategory of \(C\) when:
- if \(X : D\), then \(X : C\), and
- \(f : D(X, Y)\) iff \(f : C(X, Y)\).
In other words, a full subcategory has a subset of objects of the base category and all the morphisms between the objects.
The goal of this characterisation is to be able to work in FinGat/Fam instead of FamGat.
The CartExp Structure of FamGat
We start by equiping FinGat/Fam with a CartExp structure. Then we show that FamGat inherits this structure.
FinGat/Fam
As FinGat is finitely complete, FinGat/Fam is also finitely complete. This is a general property of slice categories. The terminal object is \(\mathrm{id} : \mathbf{Fam} \to \mathbf{Fam}\).
We now choose an exponentiable arrow for FinGat/Fam. This choice is driven by what we expect two-sortification to do. Recall that the chosen exponentiable morphism of FinGat is \(p : 1/\mathbf{Set} \to \mathbf{Set}\). Its two-sortification will be: \[ p' : (U : \mathbf{Set}, \mathrm{El} : U \to \mathbf{Set}, A : U, a : \mathrm{El}\ A) \mapsto (U : \mathbf{Set}, \mathrm{El} : U \to \mathbf{Set}, A : U) \]
We can recover this structure by pure categorical means as follows:
We can see that elements of Set are \((U : \mathbf{Set}, \mathrm{El} : U \to \mathbf{Set}, A : U)\). Then, we select the following arrow for Set → Set: \[ \varepsilon : (U : \mathbf{Set}, \mathrm{El} : U \to \mathbf{Set}, A : U) \to (\mathrm{El}\ A : \mathbf{Set}) \]
The arrow between 1/Set and Set yields exactly \(p'\). It is easy to show that an exponentiable arrow is stable under pullback, and as \(p'\) comes from a pullback with \(p\) (that is exponentiable), \(p'\) is also exponentiable in FinGat.
Moreover, we can see \(p'\) as a morphism in FinGat/Fam with the following projections to Fam:
- \(\pi_1 :\) Set → Fam
- \(p' ; \pi_1 :\) 1/Set → Fam.
Then, \(p'^* : \mathbf{FinGat/Fam}/\pi_1 \to \mathbf{FinGat/Fam}/(p';\pi_1)\), but \((C/Z)/g\) for \(g : X \to Z\) is actually \(C/X\). By applying this property, we get that: \[ p'^* : \mathbf{FinGat/\underline{Set}} \to \mathbf{FinGat/\underline{1/Set}} \] which is exactly the pullback functor of \(p'\) in FinGat, which has a right adjoint. Hence, \(p'\) is indeed exponentiable in FinGat/Fam.
This process can be generalized to any CartExp category using the same steps, remarking that \(\mathrm{Fam}\) is \(P_p\ \mathbf{Set}\) and \(\varepsilon\) is the counit of the adjunction \(p^* \dashv p_*\). As we use only generic properties of slice categories, the proof can be adapted straightforwardly.
FamGat
We now have to check whether all of this process works for FamGat. First, the terminal object is indeed in FamGat as Fam is an object of FamGat, which is a full subcategory of FinGat/Fam.
FamGat has all pullbacks: for \(G_0, G_1, G_2\) family GATs, we get the following pullback in FinGat/Fam:
As \(G_0\) and \(G_2\) have the same family (thanks to the slice structure), the pullback will also have the same family. As the family has all the sorts of \(G_0\) and \(G_2\), it also has all the sorts of the pullback. Hence, the pullback is indeed in FamGat.
Finally, \((U : \mathbf{Set}, \mathrm{El} : U \to \mathbf{Set}, A : U, a : \mathrm{El}\ A)\) and \((U : \mathbf{Set}, \mathrm{El} : U \to \mathbf{Set}, A : U)\) are both objects of FamGat and so \(p'\) is a morphism of FamGat. The polynomial functor is also a functor in FamGat as it yields the input GAT with a new point, and so it is still a right adjoint for \(p'\) in FamGat.
The Two-Sortification Functor
The two-sortification functor \(T : \textbf{FinGat} \to \textbf{FamGat}\) is the strict initial functor between FinGat and FamGat in CartExp.
The embedding \(\mathbf{FamGat} \hookrightarrow \mathbf{FinGat/Fam}\) is a CartExp-morphism. Hence, the composition of \(T\) and the embedding is naturally isomorphic to the strict initial functor between FinGat and FinGat/Fam. In the following, we consider that \(T : \mathbf{FinGat} \to \mathbf{FinGat/Fam}\).
The two-sortification of the GAT \((A : \mathbf{Set})\) yields the following two-sorted GAT: \[ (\{*\} : \mathbf{Set}, El(*) = A : \{*\} \to \mathbf{Set}, * : \{*\}). \]
Semantic Justification to Two-Sortification
We can now restate the goal formally.
For every GAT Γ, there is a FinGat morphism \(\alpha_\Gamma : T\Gamma \to \Gamma\) such that the functor \([\![\alpha_\Gamma]\!] : [\![T\Gamma]\!] \to [\![\Gamma]\!]\) preserves the initial object.
In this case, if \(T\Gamma\) has a QIIT, then so has \(\Gamma\). In the paper, we also show that \(T\Gamma\) always has a QIIT.
Instead of building a single morphism, we build a natural transformation as we wish to use a lemma (stated subsequently) that ensures unicity of natural transformations. By this property, we can give two natural transformations: one from \([\![-]\!] \circ T\) to \([\![-]\!]\) and another one from \(T\) to \(Id\), and show that the whiskering of the second one by the model functor is equal to the first one.
Natural Transformation Preserving the Initial Object
We start by building a natural transformation between \([\![-]\!] \circ T\) and \([\![-]\!]\). This makes it possible to work with the expected models of \([\![-]\!] \circ T\) instead of the abstract definition: we can define a category that is equivalent to \([\![T\Gamma]\!]\) for every GAT \(\Gamma\).
Goals:
- Define a category which gives the models of a GAT equipped with a projection to the family of its two-sortification.
- For every GAT \(\Gamma\), recover a suitable object of this category \([\![\Gamma]\!] \to \mathrm{Fam}\).
- Define a suitable category (equivalent to \([\![T\Gamma]\!]\)).
- Define an initial-object preserving natural transformation between this category and \([\![\Gamma]\!]\).
\(\mathbf{Cat//Fam}\)
We want to describe the category of models of \(T\Gamma\). The idea is to have (i) the model of the original with (ii) a projection to its family computed by \(T\).
Here, Cat/Fam is a tempting candidate as it is the direct "interpretation" of FinGat/Fam. But this category is not adapted: the terminal object of Cat/Fam is the identity functor on Fam. Here, we wish instead to have a category whose terminal object is the functor 1 → Fam: the model of the empty GAT is the terminal category 1, and the two-sortification of the empty GAT gives the empty family.
Such a terminal object can be recovered from a category similar to Cat/Fam, but with relaxed requirements: the colax slice category Cat//Fam.
This category has:
- morphisms C → Fam as objects
- for every object \(F\) : C → Fam, \(G\) : D → Fam, a morphism is a pair \((H, \alpha)\) where \(H\) is a functor from C to D and \(\alpha\) is the following natural transformation:
One can indeed verify that 1 → Fam is the terminal object in this category. We now need to recover a characterisation for every GAT \(\Gamma\).
Recovering \([\![\Gamma]\!] \to \mathrm{Fam}\)
To get a mapping \([\![\Gamma]\!] \to \mathrm{Fam}\), it suffices to (i) show that Cat//Fam is in CartExp, and (ii) show that the strict initial functor sends a GAT to its model in Cat//Fam.
Cat//Fam is in CartExp.
First, we need to show that Cat//Fam has finite limits; we show that it has a terminal object and all pullbacks.
It is easy to verify that 1 → Fam (where the trivial object is mapped to the empty family) is terminal. The pullbacks can be computed by the underlying pullbacks in Cat. The projection to Fam is given by the pushout of the given natural transformation.
Second, we can show that the following arrow is exponentiable in Cat//Fam:
where \(\delta\) maps \((X : \mathbf{Set})\) to \((\{*\}, El(*) = X)\).
The right adjoint maps an object \(G\) : D → Fam in Cat//Fam to an object
\[ (F' : P\mathbf{D} \to \mathbf{Fam}, U' : P\mathbf{D} \to \mathbf{Set}, \gamma' : \delta \circ U' \Rightarrow F'), \] where \(P\) is the polynomial functor of Cat (with chosen arrow \(p : \mathbf{1/Set} \to \mathbf{Set}\)).
As Cat//Fam is in CartExp, there is a strict initial CartExp morphism \(F : \mathbf{FinGat} \to \mathbf{Cat//Fam}\).
The domain functor Cat//Fam → Cat is a CartExp morphism.
Proof.
- The terminal object of Cat//Fam is 1 → Fam and gets mapped to 1.
- The pullbacks of Cat//Fam are computed as the pullbacks of Cat. Hence, forgetting the slice structure yields pullbacks in Cat.
- The exponentiable arrow in Cat//Fam is mapped (strictly) to the exponentiable arrow in Cat.
- One can show that the pushforwards are also preserved.
The strict bi-initial functor between FinGat and Cat//Fam maps a theory \(\Gamma\) to its family functor \(F_\Gamma : [\![\Gamma]\!] \to \mathrm{Fam}\).
By uniqueness of the strict initial morphism, the composition FinGat → Cat//Fam → Cat is isomorphic to the model functor. As Cat//Fam → Cat is an isofibration, we can refine \(F\) so that it coincides with the model functor when composed with the projection to Cat.
From \(F_\Gamma\) to a Category
The natural way of transforming a functor to a category is by taking the comma category \(F_\Gamma / \mathrm{Fam}\). Explicitely:
- objects are morphisms \(\alpha : F_\Gamma M \to (U, El)\) for \(M : [\![\Gamma]\!]\) and \((U, El) : \mathrm{Fam}\),
- morphisms between \(\alpha : F_\Gamma M \to (U, El)\) and \(\beta : F_\Gamma N \to (U', El')\) are pairs \((f : M \to N, g : (U, El) \to (U', El'))\) such that the following square commutes:
\([\![T\Gamma]\!]\) is isomorphic to \(F_\Gamma / \mathrm{Fam}\).
We want to use the bi-initiality of the mappings to conclude. But the functor mapping Cat//Fam to Cat given by \(F : C \to \mathrm{Fam} \mapsto F / \mathrm{Fam}\) cannot be upgraded to a CartExp morphism.
Instead, the following mapping can be extended: \[ F : C \to \mathrm{Fam} \mapsto F / \mathrm{Fam} \to \mathrm{Fam} \] to a functor between Cat//Fam and Cat/Fam. In fact, it is the right adjoint \(R\) of the embedding \(L :\) Cat/Fam → Cat//Fam. It can also be upgraded into a CartExp morphism.
Hence, the composite \(F \circ R : \mathbf{FinGat} \to \mathbf{Cat/Fam}\) that maps \(\Gamma\) to \(F_\Gamma / \mathrm{Fam} \to \mathrm{Fam}\) is a CartExp morphism.
Likewise, the mapping from FinGat to Cat/Fam defined on objects as \(\Gamma \mapsto [\![T\Gamma]\!] \to \mathrm{Fam}\) can also be extended to a CartExp morphism as the composition \([\![-]\!]/\mathrm{Fam} \circ T\), where the functor \(-/\mathrm{Fam}\) is a particular instance of the functor \(-/PX\) which, given a CartExp morphism \(F : (C, p_C) \to (D, p_D)\) returns a CartExp morphism \(F/PX : (C/P_{p_C} X_C, \underline{p_C} : \underline{Y_C} \to \underline{X_C}) \to (C/P_{p_D} X_D, \underline{p_D} : \underline{Y_D} \to \underline{X_D})\).
By bi-initiality, \(F \circ R \cong [\![-]\!]/\mathrm{Fam} \circ T\). As this is an isomorphism in the slice category, we have that for every GAT \(\Gamma\), the domain of \(F(R(\Gamma))\) and of \([\![T\Gamma]\!]/\mathrm{Fam}\) are isomorphic, i.e., \[ F_\Gamma / \mathrm{Fam} \cong [\![T\Gamma]\!]. \]
The Natural Transformation
We define the natural transformation \(\alpha : F_- / \mathrm{Fam} \Rightarrow [\![-]\!]\) by mapping each morphism \(F_\Gamma M \to (U, El)\) where \(M : [\![\Gamma]\!]\) to \(M\). Naturality follows immediately.
\(\alpha\) preserves initial objects.
Let \(\Gamma\) be a GAT and \(0_F : F_\Gamma M \to (U, El)\). Then \(M\) is initial in \([\![\Gamma]\!]\).
Let \(N : [\![\Gamma]\!]\). We have that \(id : F_\Gamma N \to F_\Gamma N\) is an object of \(F_\Gamma / \mathrm{Fam}\). Hence, by initiality of \(0_F\), there is a unique morphism \((f : M \to N, g : (U, El) \to F_\Gamma N)\). If \(f' : M \to N\), then \((F_\Gamma f', F_\Gamma f')\) is a morphism in \(F_\Gamma / \mathrm{Fam}\), and by initiality, the following diagram commutes:
Actually, \((id, !) : (F_\Gamma M \to (U, El)) \to (F_\Gamma M \to F_\Gamma M)\) and so the mapping \(! : F_\Gamma M \to F_\Gamma M\) is the identity by definition. Hence, \(f \circ id = f = f'\).
There is a natural transformation \([\![T -]\!] \Rightarrow [\![-]\!]\) that preserves the initial object.
Recovering the Original GAT
For the proof to be complete, we define a natural transformation \(\beta : T \Rightarrow Id\) that behaves as expected. We use the following lemma.
Let \(C\) be in CartExp with chosen exponentiable arrow \(p\). Let \(F : \mathbf{FinGat} \to C\) be a functor preserving pullbacks and \(G : \mathbf{FinGat} \to C\) be a CartExp morphism. Given a pullback square:
there exists a unique natural transformation \(\alpha_{(x,y)}\) between \(F\) and \(G\) such that the given pullback is the naturality square for \(\alpha_{(x,y)}\) at \(p\).
By applying this lemma, we get a natural transformation \(\beta\). Moreover, instantiating \(C\) with FinGat, \(F\) with \(dom \circ T\) and \(G\) with \(Id\), we get that the naturality square at \(p\) is the following one:
Recall that the action of ε is to map \((U : \mathbf{Set}, El : U \to \mathbf{Set}, A : U)\) to \(El(A)\). Now, starting from \(\Gamma = (A : \mathbf{Set})\), recall that the two-sortification of Γ yields the following two-sorted GAT: \[ (\{*\} : \mathbf{Set}, El(*) = A : \{*\} \to \mathbf{Set}, * : \{*\}). \] Furthermore, applying \(\varepsilon\) gives back the original GAT, as \(A : U\) is \(* : \{*\}\) here, and \(El(A)\) is \(El(*) = A\).
Moreover, \([\![\beta_\Gamma]\!] : [\![T\Gamma]\!] \to [\![\Gamma]\!]\), which means that we have two parallel natural transformations:
By strict initiality, \([\![\beta_\Gamma]\!]\) for \(\Gamma = (A : \mathbf{Set})\) is the pullback square defined similarly as the one above of FinGat. Moreover, the pullback square of \(\alpha\) at \(p_\mathbf{Cat}\) is given by the underlying pullback in Cat, i.e., it is also the pullback given above. Consequently, the previous lemma's hypotheses are fulfilled and so \(\alpha = [\![\beta]\!]\).
\(\beta : T \Rightarrow Id\) is a natural transformation such that for every GAT Γ, \([\![\beta_\Gamma]\!] : [\![T\Gamma]\!] \to [\![\Gamma]\!]\) preserves the initial object.
Conclusion
We have shown that two-sortification is justified at the level of the models of GATs, i.e., that if a two-sortified GAT has an initial model then so has the original GAT.
We have illustrated everything with finite GATs (i.e., categories with finite limits), but this also works for infinite GATs (categories with all limits).
In the paper, we have also shown that the two-sortification functor is fully faithful.
If you look at the paper, it actually introduces cartesianness for Cat//Fam and \(F_\Gamma / \mathrm{Fam}\), which is needed in the details of the proofs.