Categorical models of subtyping
Coraglia]Greta Coraglia
Emmenegger]Jacopo Emmenegger

Most categorical models for dependent types have traditionally been heavily set based: contexts form a category, and for each we have a set of types in said context – and for each type a set of terms of said type. This is the case for categories with families, categories with attributes, and natural models; in particular, all of them can be traced back to certain discrete Grothendieck fibrations. We extend this intuition to the case of general, non necessarily discrete, fibrations, so that over a given context one has not only a set but a category of types.

We argue that the added structure can be attributed to a notion of subtyping that shares many features with that of coercive subtyping, in the sense that it is the product of thinking about subtyping as an abbreviation mechanism: we say that a given type $A'$ is a subtype of $A$ if there is a unique coercion from $A'$ to $A$. Whenever we need a term of type $A$, then, it suffices to have a term of type $A'$, which we can `plug-in' into $A$.

For this version of subtyping we provide rules, coherences, and explicit models, and we compare and contrast it to coercive subtyping as introduced by Z. Luo and others. We conclude by suggesting how the tools we present can be employed in finding appropriate rules relating subtyping and certain type constructors.

The notion of subtyping is often quite tricky because of its double nature: on one hand, it is meant to represent a relation so simple that one would like to not be bothered to look too much into it but, at the same time, programming languages do not do well with things that are left unsaid. In <cit.>, subtyping $A\leq B$ is defined as a relation between two types $A$ and $B$ such that, if a term of type $A$ is provided, than it can be `safely' used in a context where $B$ is expected, and the program should not falter if this happens. This is often called the principle of safe substitution, and is encoded via a new typing rule that goes by the name of subsumption.

\[
(Sub)\frac{\Gamma\vdash a:A\quad\Gamma \vdash A\leq B}{\Gamma \vdash a:B}
\]

The problem with subsumption is that it threatens to break certain structures and properties such as canonicity or induction principles. Many variants of subtyping have been proposed, and one in particular has proved itself to be well-behaved with respect to such issues, and that is coercive subtyping [21].

In the present work we tackle the problem of subtyping from the point of view of its categorical semantics: we extend a known model to naturally include a notion of subtyping (<ref>), and show how this turns out to be in fact quite closely related to coercive subtyping (<ref>). We then study some examples and applications (<ref>), and conclude by observing some properties that that this new notion intrinsically shows (<ref>).

§ CATEGORICAL MODELS OF DEPENDENT TYPES

The relation between type theory and category theory is one which has been widely studied, and has in the years produced a large variety of models and structures. The interest of the present work is in those that strongly employ objects and techniques coming from the theory of Grothendieck fibrations.

§.§ Grothendieck fibrations

Fibrations were introduced by A. Grothendieck [9] for purposes pertaining algebraic geometry, but were soon found extremely useful to describe certain phenomena in logic [14]. We will recall key results and definitions when needed, but we refer to <cit.> for a detailed introduction.

Let $p\colon\ee\to\bb$ a functor and  a morphism in $\ee$. We say that $s$ is $p$-cartesian or cartesian over $\sigma\colon \Theta\to\Gamma$ if $p(s)=\sigma$ and for any other $r\colon C\to A$ and $\tau$ such that $p(r)=\sigma\circ \tau$ there is a unique $t\colon C\to B$ in $\ee$ such that $p(t)=\tau$ and $s\circ t =r $.

\begin{equation}\label{cartesian}
\begin{tikzcd}[ampersand replacement=\&]
C \\
\& B \& A \&\& \ee \\
\Xi \\
\& \Theta \& \Gamma \&\& \bb
\arrow["s"', from=2-2, to=2-3]
\arrow["r", curve={height=-6pt}, from=1-1, to=2-3]
\arrow["\sigma"', from=4-2, to=4-3]
\arrow["\sigma\circ\tau", curve={height=-6pt}, from=3-1, to=4-3]
\arrow["\tau"', from=3-1, to=4-2]
\arrow["p", from=2-5, to=4-5]
\arrow[dashed, from=1-1, to=2-2]
\end{tikzcd}
\end{equation}

We say that $s$ is a ($p$-)cartesian lifting of $\sigma$, and it is often denoted $s_{A,\sigma}\colon\sigma^*A\to A$.

A functor $p\colon\ee\to\bb$ is a fibration if for all $A$ in $\ee$, each $\sigma:\Theta \to pA$ has a cartesian lifting. We also say that $\ee$ is fibered over $\bb$ or that $\ee$ is over $\bb$. Oftentimes $\bb$ is called the base category and $\ee$ the total category of $p$.

From the point of view of the logic, we can consider $\bb$ to be a category of contexts and substitutions/terms, and $\ee$ to be a category of formulae/types, so that each formula is sent to its corresponding context. Asking that for each term and formula there exist a lifting, then, amounts to asking that substitution can be computed and that it indeed produces a formula in then new context. A classical example is that of the Lindenbaum-Tarski algebra for a given first-order theory (<ref>).

A particular feature of fibrations is that they induce a factorization system on their total category, because for any given $r\colon C\to A$, we can always instantiate the diagram in (<ref>) as follows,

\[\begin{tikzcd}[ampersand replacement=\&]
C \\
{\sigma^*A} \& A \&\& \ee \\
\Theta \\
\Theta \& \Gamma \&\& \bb
\arrow["{s_{A,\sigma}}"', from=2-1, to=2-2]
\arrow["r", curve={height=-6pt}, from=1-1, to=2-2]
\arrow["\sigma"', from=4-1, to=4-2]
\arrow["\sigma", curve={height=-6pt}, from=3-1, to=4-2]
\arrow["\id"', from=3-1, to=4-1]
\arrow["p", from=2-4, to=4-4]
\arrow[from=1-1, to=2-1]
\end{tikzcd}\]

producing a factorization of $r$. Maps in the left class of such factorization system, meaning maps that are sent to identities, are called vertical.

Consider $p\colon\ee\to\bb$ a fibration. The classes of vertical and cartesian morphisms form a orthogonal factorization system on $\ee$. It additionally has the following properties:

* if $g$ and $gf$ are vertical, then so is $f$;

* pullbacks of vertical maps along cartesian ones exist and are vertical.

If cartesian maps can be thought of as substitutions, vertical maps relate formulae/types in the same context precisely in a way that `does nothing' to the underlying terms.

Not only are vertical maps part of a factorization system, but they can be shown to form a category: more precisely, for each context $\Gamma$ in $\bb$, one can define a category $\ee_\Gamma$ having for objects those in $\ee$ that are sent to $\Gamma$, and for morphisms those in $\ee$ that are vertical over $\id_\Gamma$. This intuition is part of one of the most meaningful results of the theory, again due to Grothendieck.

There exists a 2-equivalence

\[
\Fib(\bb)\cong \Psd[\bb\opp,\Cat]
\]

between the 2-category of fibrations (with base $\bb$), functors preserving cartesian maps, and natural transformations, and that of contravariant pseudofunctors (from $\bb$), pseudonatural transformations, and modifications.

From left to right, a fibration is sent to a (pseudo)functor that computes for each $\Gamma$ its fiber $\ee_\Gamma$. From right to left, it performs what is called the Grothendieck construction of a (pseudo)functor, which to an $F\colon\bb\opp\rightsquigarrow\Cat$, maps the fibration $p\colon\int F\to\bb$, where objects of $\int F$ are pairs $(\Gamma,A)$ with $\Gamma$ in $\bb$ and $A$ in $F(\Gamma)$.

Relevant classes of fibrations are those that correspond to functors, which are called split, those whose fibers are preorders, which are called faithful, and those whose fibers are sets, which are called discrete.

§.§ Categories with families

A category with families (cwf) is the data of

* a small category $\bb$ with terminal object $\top$;

* a functor $\Ty\colon\bb\opp\to\Set$;

* a functor $\Tm\colon\int\Ty\opp\to\Set$

* for each $\Gamma$ in $\bb$ and $A$ in $\Ty(\Gamma)$ an object $\Gamma.A$ in $\bb$, together with two projections $\mathsf{p}_A\colon\Gamma.A\to\Gamma$ and $\mathsf{v}_A\in\Tm(\Gamma.A,\Ty\,\mathsf{p}_A (A) )$ such that for each $\sigma\colon\Theta\to\Gamma$ and $a\in\Tm(\Ty\sigma (A))$ there exists a unique morphism $\Theta\to\Gamma.A$ making the obvious triangles commute.

In particular,

$\Ty(\Gamma)$ is a set, the set of types in context $\Gamma$, and $\Tm(\Gamma,A)$ is again a set, the set of terms of type $A$ in context $\Gamma$. The terminal object is meant to model the empty context, while the last condition is what provides context extension – since we are about to give a simpler, equivalent form of it, we do not dwell on it any longer.

Following <ref>, we can turn <ref> upside down. What we get is the (equivalent, see <cit.>) notion of natural model.

A natural model is the data of

* a small category $\bb$ (with terminal object $\top$);

* a discrete fibration $u\colon\uu\to\bb$;

* a discrete fibration $\du\colon\duu\to\bb$;

* a fibration morphism $\Sigma\colon\du\to u$ with a right adjoint functor.

In this case $u$ collects types and $\du$ collects terms, as both are fibered on contexts.

$\Gamma \vdash A\ty$     $\Gamma \vdash a: A$

$u(A)=\Gamma$     $\du(a)=\Gamma,\Sigma (a) =A$

$u\;\text{in }\Fib^{disc}(\ctx)$     $\du\;\text{in }\Fib^{disc}(\ctx)$

The fibration morphism (a functor making the diagram below commute) $\Sigma$ maps to each term its type, while $\Delta$ computes for each $A$ what in <ref> is called $\mathsf{v}_A$, meaning a variable in $A$ `transported' to the context $\Gamma.A$.

\begin{gather}\label{rules-gcwf}
\begin{tikzcd}[ampersand replacement=\&]
\duu \&\& \uu \\
\& \bb
\arrow["u", from=1-3, to=2-2]
\arrow["\du"', from=1-1, to=2-2]
\arrow[""{name=0, anchor=center, inner sep=0}, "\Sigma"', curve={height=6pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "\Delta"', curve={height=6pt}, from=1-3, to=1-1]
\arrow["\dashv"{anchor=center, rotate=90}, draw=none, from=0, to=1]
\end{tikzcd}
\qquad
(\Sigma)\frac{\Gamma\vdash a:A}{\Gamma\vdash A\ty}
\quad
(\Delta)\frac{\Gamma\vdash A\ty}{\Gamma.A\vdash \mathsf{v}_A:A}
\end{gather}

§.§ Generalized categories with families

Our intuition, now, is that we want to use the theory of fibrations to generalize categories with families (or natural models) to the case where fibers over a given context are no longer a set, but a (small)  category. If we manage to do this swiftly, we will have found a model for dependent types that introduces and additional relation between types in the same context, so that this relation does imply absolutely no substitution. This leads us to the following definition.

A generalized category with families (gcwf) is the data of

* a small category $\bb$ (with terminal object $\top$);

* a fibration $u\colon\uu\to\bb$;

* a fibration $\du\colon\duu\to\bb$;

* a fibration morphism $\Sigma\colon\du\to u$ with a right adjoint functor, and unit and counit with cartesian components.

Notice that the adjoint pair in <ref> is not fibered, as $\Delta$ does not make the desired triangle commute and unit and counit have cartesian components.

Of course a gcwf with discrete $u,\du$ is a regular cwf, so that a gcwf is simply a generalization of a well-known model. We choose the name as to remark that this new structure falls into a long tradition of models, which categories with families is perhaps one of the most prominent exponents of, but these could be very easily called `generalized natural models', or something entirely different (cf. [4]). We conclude this section with one last result relating gcwfs to other notable structures, namely comprehension categories [11], as to show that our path did not stray much away from known territory.

There is a biequivalence between (the 2-category of) gcwfs and (the 2-category of) comprehension categories.

A generalized category with families, then, is precisely as good a model as a comprehension category. The purpose of introducing the new structure, though, lies in the clarity of its use, and we hope that the rest of the present work will be a witness to that.

In our exposition we put aside two elements in the discussion on categorical models for dependent types. The first is of course the issue of coherence: since fibrations involve pseudofunctors, equations for identities and, especially, associativity only hold up to vertical isomorphism, while it is usually preferable to have substitution `on the nose'. If one so wishes, the reader is invited to only use split fibrations, meaning those that correspond to strict functors, and morphisms that preserve the splitting. A thorough discussion on the topic can be found in  <cit.>.

Another sensitive topic is that of definitional equality. For the moment, having other purposes in mind, we settle for interpreting it as identity of objects (in the category over each context) and, therefore, rarely make explicit coherence rules involving it, as they are all trivial from our definitions.

§ VERTICAL MAPS INDUCE A NOTION OF SUBTYPING

The idea that vertical maps could nicely relate types in the same context is of course not new. The most closely related precedent to this is perhaps [23], followed by the notes in [27], where, quite radically, functors were interpreted to be type refinement systems. Our work is similar in spirit – though one should really be careful of the difference between “type refinement” and “subtyping” <cit.> – but of course based on fibrations instead on functors, hence with a special focus on substitution.

§.§ Two new judgements

Now that we are all set, let us describe what it is that we can say in a gcwf, that was not already available in the discrete case. To the two judgements pertaining types and terms, we add two new ones involving subtyping.

$\Gamma \vdash A\ty$     $\Gamma \vdash a: A$     $\Gamma \vdash A'\leq_f A$     $\Gamma \vdash a:_g A$

$u(A)=\Gamma$     $\du(a)=\Gamma,\Sigma (a) =A$     $f\colon A'\to A$, $u(f)=\id_\Gamma$     $g\colon \Sigma a\to A$, $u(g)=\id_\Gamma$

In particular, when a notion of subtyping is introduced, it automatically entails a notion of “sub-typing” for terms as well. We read the new judgements, respectively, as $A'$ is a subtype of $A$, as witnessed by $f$ and $a$ is a term of type a subtype of $A$, as witnessed by $g$. Recall that vertical maps enjoy some nice properties (<ref>), and their combination provides us with structural rules for the new judgements.

The following rules are satisfied by a gcwf.

\begin{equation*}
\AxiomC{$\Gamma\vdash a:_g A'$}\AxiomC{$\Gamma\vdash A'\leq_f A$\LeftLabel{(Sbsm)}}\BinaryInfC{$\Gamma\vdash a:_{fg} A$}
\DisplayProof
\qquad
\AxiomC{$\Gamma\vdash A' \leq_f A$}\AxiomC{$\Gamma\vdash A''\leq_g A'$}\LeftLabel{(Trans)}\BinaryInfC{$\Gamma\vdash A'' \leq_{fg} A$}
\DisplayProof
\end{equation*}

\begin{equation*}
\AxiomC{$\Gamma.A\vdash B' \leq_f B$}\AxiomC{$\Gamma\vdash a:_g A$}\LeftLabel{(Sbst)}\BinaryInfC{$\Gamma\vdash B'[a] \leq_{\du(\Delta g \eta_a)^* f} B[a]$}
\DisplayProof
\qquad
\AxiomC{$\Gamma\vdash A' \leq_f A$}\AxiomC{$\Gamma\vdash B\ty$}\LeftLabel{(Wkn)}\BinaryInfC{$\Gamma.B\vdash A' \leq_{(u\epsilon_B)^* f} A$}
\DisplayProof
\end{equation*}

Intuitively, Subsumption and Transitivity are both due to the fact that vertical maps compose to vertical maps, while Substitution and Weakening make use of the substitution structure due to the fibration part of the system. We refer to the appendix for further details.

§.§ Comparison with coercive subtyping

As we said in the introduction, it turns out that the calculus resulting in this generalization comes close to coercive subtyping. We hope to convince the reader that, despite all the technical differences, they actually entertain the same spirit.

The basic idea of coercive subtyping is that subtyping is modelled as an abbreviation mechanism: $A$ is a subtype of $B$, if there is a unique coercion $c$ from $A$ to $B$, written as $A<_c B$. Then, if a hole in a context requires an object of type $B$, it is legal to supply an object $a$ of type $A$ – it is equivalent to supplying the object $c(a)$. [20]

A coercion $c$ from $A$ to $B$ is technically a term of the function type $A\to B$, hence computing $c(a)$ amounts to function application. Coercions are added `manually' to a given type theory, as they are a priori not part of the calculus, and the resulting system is shown both to be a conservative extension of the original one and to act well with respect to canonicity.

Let us now collect in a table the main similarities and differences between coercive subtyping and subtyping via vertical maps. We then will consider each point in detail.

coercive subtyping     categorical subtyping

$\Gamma \vdash f: A'\to A$     $f\colon A'\to A$ vertical over $\Gamma$

judgements added to the calculus     judgements `added' the the classical model

no witnesses for typing judgements     witnesses for typing judgements

$f$ is unique     $f$ is not necessarily unique

(Sbsm) via substitution     (Sbsm) via composition

satisfies (Trans)     satisfies (Trans)

satisfies (Sbst)     satisfies (Sbst)

satisfies (Wkn)     satisfies (Wkn)

satisfies congruence     satisfies congruence

The main technical difference is of course what coercions are, as on one side they are function terms, on the other they are (particular) morphisms in the total category. In some sense this difference is unavoidable: if one starts from the traditional syntax of a type theory, syntactic objects are all that is available, while if one looks at a very general model as if it was a syntax (and one would have some merit in doing so, see <ref>), then they have more objects at hand. In both cases, though, subtyping is a notion that is somehow independent of the calculus, because in one case it is added by selecting a choice of witnesses (and adding one new judgement for each), while on the other it is literally orthogonal to the rest of the structure.

While we will deal with the matter of uniqueness of coercions in <ref>, a difference that is unbridgeable is that of dealing with typing judgements: in coercive subtyping, a term can indeed have more than one type, so that a typing judgments is in some sense ambiguous, while in subtyping with vertical maps one can always unambiguously know by which means a term is of a certain type, but for this it pays the price of having a whole new set of annotated judgements.

Finally, validity with respect to rules appearing in the table above is common to both systems – by `congruence', in particular, we mean congruence of the subtyping relation with respect to definitional equality, see <ref>. It should be remarked that rules appearing on the `coercive subtyping' side are not all rules required, for example, in [20], but they are in a sense the structural ones, as the others aim to discipline either how coercions (as function types) interact with the system, while in our case that is granted.

§.§ On uniqueness of coercions

As we suggested in presenting this new perspective on subtyping, uniqueness of coercions is not really an issue. In particular, we have a whole theory of fibrations whose fibers are preorders, we actually call them faithful fibrations (cf. <ref>).

Not only that, but we can show that, given a gcwf, if its type fibration is faithful, then so is its term fibration.

Let $(u,\du,\Sigma \dashv \Delta)$ a gwcf. Then $\Sigma$ is a faithful functor.

In this sense, faithfulness, hence uniqueness of coercions, can indeed be modeled by simply looking at faithful fibrations, and such a burden is in fact not laid on the choice of the fibration collecting terms.

Though a key feature of coercive subtyping, avoiding uniqueness might have its merits. Consider for example the case of sum types: it seems like one should have two different witnesses for the judgement $\Gamma\vdash A\leq A+A$, one per coproduct injection.

§.§ Comparison with related variants of type theory

Directed type theory.
Extending the paradigm connecting types, $\omega$-groupoids, and homotopy theory, to the directed case – meaning involving $\omega$-categories and directed homotopy theory, one encounters the notion of directed type theory. The underlying intuition wishes to add, for each pair of terms of the same type (and substitutions), a new asymmetric `identity' type of transformations from one to the other, possibly stopping at some given height/iteration [16]. Though vertical in some sense, this notion of directed-ness is considered only for terms, while in our case the main focus is for types (though one could regard types as terms of a given universe, in DTT transformations are introduced for all pairs of terms). Being based on ($\omega$-)categories, they share some properties of morphisms, such as composition and identity, but our vertical maps are a lot simpler, and in no way higher-dimensional – though the monad in <ref> suggests possible extensions in this direction.

Observational type theory.
Observational type theory was introduced to combine the nice computational features of intensional type theory, such as termination of reductions, and propositional equality of extensional type theory, so that two functions are equal if they are equal point-wise, or “if all observations about them agree”  <cit.>. The fact that conversion rules allow to pass implicitly between definitionally equal types is extended to a mechanism that allows to pass implicitly between provably equal types. This process is explicit and its agents are called coercions. Coercions for a OTT work in a way that is much similar to our vertical maps, but their being originated by proofs of equality of types ensures that for a given coercion, one can always one associated to it and going in the opposite direction.

Practical subtyping.
Another relevant syntactic approach is that of `practical subtyping' as introduced in [18]. There, the new subtyping judgements are ternary relations as $t\in A\subset B$, which are encoded as sorts of implications: “if $t$ is a term of type $A$, then it is a term of type $B$”. In particular, this notion of subtyping most notably (and `practically') describes subtyping from the perspective of terms, and not types, as in our case. In particular, subtyping between types, meaning intrinsic judgements such as $A\subseteq B$, are encoded by means of choices operators, such as Hilbert's $\epsilon$ <cit.>.

§ EXAMPLES AND APPLICATIONS

§.§ Gcwfs from Lindenbaum-Tarski

Consider the Lindenbaum-Tarski algebra of a given first-order theory $\mathcal{T}$ in a language $\mathcal{L}$. We take $\catof{ctx}$ to be the category where

* objects are lists of distinct variables $x=(x_1,\dots,x_n)$,

* arrows are lists of substitution for variables, meaning $[t_1/y_1,\dots,t_m/y_m]=[t/y]\colon x\to y$, with $t_j$'s being $\mathcal{L}$-terms that are built on variables $x_1,\dots,x_n$,

and composition is defined by simultaneous substitution. The product of two lists $x$ and $y$ is a list $w$ with length the sum of the lengths of $x$ and $y$, and projections on $x$ and $y$ are substitutions with, respectively, the first $n$ and the last $m$ variables in $w$. Categorically and in the sense of [14], this is the free Lawvere theory on the language $\mathcal{L}$.

One can define the functor $LT_{\mathcal{T}}\colon\catof{ctx}\opp\to\catof{InfSL}$ so that to each list $x$, the category $LT_{\mathcal{T}}(x)$ has for objects equivalence classes of well-formed formulae in $\mathcal{L}$ with free variables at most those that are in $x$, and with respect to the equivalence relation induced by reciprocal deducibility in $\mathcal{T}$, $\phi \dashv \vdash_{\mathcal{T}} \phi'$. Notice that this makes our treatment proof-irrelevant. Maps in $LT_{\mathcal{T}}(x)$ are provable consequences in $\mathcal{T}$. Composition is given by the cut rule of the calculus, and identities are tautologies. Since substitution preserves provability, $LT_{\mathcal{T}}$ can be suitably extended to a functor, and its correspondent under the Grothendieck construction <ref> is a faithful fibration $p\colon \int LT_{\mathcal{T}}\to\catof{ctx}$.

Such a construction was first introduced with the name of (hyper)doctrine in [15] and is thoroughly explained in [13] and [22]. We here show that it underlies the structure of a gcwf where terms are entailments.

Call $\ee$ the category of $p$-vertical maps and commutative squares, which is again fibered over $\catof{ctx}$ – call $e$ this fibration, $\mathsf{Cod}\colon\ee\to\int LT_{\mathcal{T}}$ the codomain functor, $\mathsf{Diag}$ the functor mapping each formula to its identity. The triple $(p,e,\mathsf{Cod}\dashv\mathsf{Diag})$ is a gcwf.

This gcwf is in fact not a cwf. Here, types are formulae and terms are (unique) witnesses to entailment, meaning triples $x;\phi\vdash\psi$ where $\phi$ and $\psi$ are both formulae in the fiber over $x$. The underlying notion of subtyping actually coincides with terms.

This is an example of a more general instance, which will thoroughly discussed in <ref>.

§.§ Gcwfs from topos theory

Let $\ee$ an elementary topos and $\top\colon\one\to\Omega$ its subobject classifier, then consider

\[\begin{tikzcd}[ampersand replacement=\&]
\ee_{/\one} \&\& \ee_{/\Omega} \\
\& \ee
\arrow["\dom", from=1-3, to=2-2]
\arrow["\sim"', from=1-1, to=2-2]
\arrow[""{name=0, anchor=center, inner sep=0}, "\Sigma_\top"', curve={height=6pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "\Delta_\top"', curve={height=6pt}, from=1-3, to=1-1]
%\arrow["\dashv"{anchor=center, rotate=90}, draw=none, from=0, to=1]
\end{tikzcd}\]

with $\Sigma_\top=\top\circ\text{-}$ and $\Delta_\top(\phi\colon X\to \Omega)=(\text{canonical p.b. of }\phi\text{ along }\top)$ .

The triple $(\sim,\dom,\Sigma_\top\dashv\Delta_\top)$ is a gcwf.

Compatibly with the Mitchell-Bénabou interpretation, types are (proof irrelevant) propositions, $\Delta_\top$ computes the comprehension $\{x\,|\,\phi(x)\}$, and so on – we refer to <cit.>, <cit.> for an extensive treatment of the topic, and to [17] for a quick overview. In this case, the fibrations involved are discrete, hence this is really is a cwf, and there is no subtyping.

A topos is quite a general structure, so let us break down a couple of examples for it. The prototypical example of an elementary topos is $\catof{Set}$, the categories of sets and functions, with subobject classifier $\top\colon\one\to\mathsf{2}$, $\ast\mapsto 1$, which classifies subsets via their characteristic function.

\[\begin{tikzcd}[ampersand replacement=\&]
{A_\phi} \& \one \\
A \& {\mathsf{2}}
\arrow["\top", from=1-2, to=2-2]
\arrow["\phi"', from=2-1, to=2-2]
\arrow["{i_\phi}"', hook', from=1-1, to=2-1]
\arrow[from=1-1, to=1-2]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
\end{tikzcd}\]

In this case terms are sets, types are functions $\phi\colon A\to \mathsf{2}$, which are equivalently subsets of $A$ – and the reason why we usually call them propositions. The context for each proposition $\phi$ is its domain set $A$. Let us now break down rules as in (<ref>),

\begin{gather}
(\Sigma_\top)\frac{A\vdash A}{A\vdash i_{\id_A}\ty}
\quad
(\Delta_\top)\frac{A\vdash \phi\ty}{A_\phi\vdash A_\phi}
\end{gather}

where we use the fact that $\Delta_\top(\phi)=\dom i_\phi=\{a\,|\,\phi(a)\}\subseteq A$ by definition. Notice how, again, $\Delta$ does not make the triangle commute, as, in principle, $A\neq A_\phi$.

Let us now look at a more complicated case, namely that of $\catof{Eff}$, the effective topos [10, 25], whose objects are sets $A$ with an $\nn$-valued equality predicate $=_A\in\mathcal{P}(\nn)^{A\times A}$, and whose morphisms are $\mathcal{P}(\nn)$-valued functional relations: we think of each subset of $\nn$ as the realizers (in the sense of Kleene) for a given proposition. One can show that $\catof{Eff}$ is a topos with subobject classifier $\top\colon (\{\ast\},\nn)\to(\mathcal{P}(\nn), \leftrightarrow)$, where $A\leftrightarrow B:= (A\to B)\land(B\to A)$ is a pair of recursive functions mimicking bi-implication <cit.>, and $\top(\ast,A)=[A\leftrightarrow \nn]$. In this case, terms are sets with an $\nn$-valued equality predicate, and types are subobjects of them, which can be shown to be sort of subsets with a compatible equality predicates and an additional `membership' unary predicate compatible with it.

§.§ Gcwfs from pullbacks

For $\ctg{C}$ with pullbacks we can define $\ctg{C}\due$ the category of arrows in $\ctg{C}$ and $\catof{Sec}(\ctg{C})$ of sections of arrows in $\ctg{C}$, meaning of pairs $(s,f)$ with $f,s\in\ctg{C}\due$ and $f\circ s =\id$. Therefore a type in context $A$ is a map $f\colon B\to A$ and a term of type $f$ is one of its sections, $s$. For a given type $f$ (map) context extension can be performed using what is usually called its `kernel pair' construction, meaning computing the following pullback,

\[\begin{tikzcd}[ampersand replacement=\&]
B \\
\& {K_f} \& B \\
\& B \& A
\arrow["f"', from=3-2, to=3-3]
\arrow["f", from=2-3, to=3-3]
\arrow["{f^+}", from=2-2, to=3-2]
\arrow[from=2-2, to=2-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3]
\arrow["\id"', curve={height=6pt}, from=1-1, to=3-2]
\arrow["\id", curve={height=-6pt}, from=1-1, to=2-3]
\arrow["{!\, d(f)}"{description}, dashed, from=1-1, to=2-2]
\end{tikzcd}\]

which we can interpret as the universal $f$-induced congruence on $B$. One can always compute the section $B\to K_f$, which can be extended to a functor $K\colon\ctg{C}\due\to\catof{Sec}(\ctg{C})$.

Call $U\colon\catof{Sec}(\ctg{C})\to\ctg{C}\due$ the functor mapping each pair $(s,f)$, with $s$ section of $f$, to $f$. The triple $(\cod,\cod U,U\dashv K)$ is a gcwf.

Actually, by <ref>, the same can be said for any $\ctg{D}$ subcategory of $\ctg{C}\due$ closed for pullbacks, for example we can consider monomorphisms, and their sections. Notice that this is not a cwf, as vertical maps are commutative triangles.

Let us give a couple of examples of this case, as well. We look at $\Set$ again, for a function $f\colon B\to A$, we find that $K_f$ is the set of pairs of elements of $B$ with the same image through $f$, and $B\to K_f$ is the diagonal. We again try to break down rules as in (<ref>), and get the following.

\begin{gather}
(U)\frac{A\vdash f\colon B \leftrightarrows A \colon s}{A\vdash f\colon B\to A\ty}
\quad
(K)\frac{A\vdash f\colon B\to A\ty}{B\vdash f^+\colon K_f \leftrightarrows B \colon d(f)}
\end{gather}

Again, it is important that the right adjoint $K$, the one performing context extension, does not make the triangle commute, as $B$ is not (necessarily) equal to $A$. Let us now look at subtyping judgements: morphisms in $\ctg{C}\due$ are commutative squares, vertical ones are squares such that the codomain is the identity, hence commutative triangles. The whole set of structural judgements available in this model (cf. <ref>) is then the following.

$A \vdash f\ty$     $A \vdash s:f$     $A \vdash f'\leq_h f$     $A \vdash s:_k f$

[ampersand replacement=&]

["f", from=1-1, to=2-1]
[ampersand replacement=&]

["f", curve=height=-6pt, from=1-1, to=2-1]
["s", curve=height=-6pt, from=2-1, to=1-1]
[ampersand replacement=&]
f' && f

& A
["f'"', from=1-1, to=2-2]
["f", from=1-3, to=2-2]
["h", from=1-1, to=1-3]
[ampersand replacement=&]
f' && f

& A
["f'", curve=height=-6pt, from=1-1, to=2-2]
["f", from=1-3, to=2-2]
["k", from=1-1, to=1-3]
["s", curve=height=-6pt, from=2-2, to=1-1]

Of course one could consider a great multitude of other categories, such as $\catof{Pos},\catof{Top}$, $\catof{Vect}_K, \catof{Grp}$, all topoi, and many others.

§.§ On type constructors

We consider here only function types of the form $\funty(A,B)$,
where $A$ and $B$ are in the same context
(in particular, $B$ does not depend on $A$).
In this case, given a subtype $A'$ of $A$ and a subtype $B$ of $B'$
(note the different order),
one would like to conclude that $\funty(A,B)$ is a subtype of $\funty(A',B')$.
In our proposed framework, this can be expressed by requiring an action of $\funty$ on vertical arrows, which is contravariant in the first component.

In the case of a discrete gcwf
(that is, in the fibrational formulation of a natural model/cwf)
the existence of function types can be expressed by requiring the existence of functors $\funty$ and $\absty$ making the right-hand square below a pullback [2]

\[\begin{tikzcd}
\uu {}_{\du\Delta}\!\!\times_{\du} \duu	\ar[d,"{\id \times \Sigma}"']
&	\mathrm{W}^*(\uu {}_{\du\Delta}\!\!\times_{\du} \duu)
\ar[d] \ar[r,"\absty"] \ar[l]
&	\duu	\ar[d,"{\Sigma}"]
\\
\uu {}_{\du\Delta}\!\!\times_u \uu
&	\uu {}_u\!\!\times_u \uu
\ar[l,"\mathrm{W}"'] \ar[r,"\funty"]
&	\uu
\end{tikzcd}\]

where the left-hand square is a pullback.
The lower functor $\funty$ simply takes two types $A$ and $B$ in the same context $\Gamma$ to the type $\funty(A,B)$.
The functor $\mathrm{W}$ is weakening of the second type with the first one:
it takes a pair $(A,B)$ of two types $A$ and $B$ in the same context $\Gamma$ to the pair $(A,(u\epsilon_A)^*B)$
where $(u\epsilon_A)^*B$ is the type $B$ weakened to the context $\Gamma.A$.
As the left-hand square is a pullback,
the domain of the functor $\absty$ consists of pairs $(A,b)$ of a type $A$ in context $\Gamma$ and a term $b$ of the weakened type $(u\epsilon_A)^*B$ in context $\Gamma.A$.
The functor $\absty$ simply maps such a pair to the term $\absty(A,b)$.

Commutativity of the square ensures that the type of $\absty(A,b)$ is $\funty(A,B)$.
As it is not relevant for our discussion,
we refer to [2] for details on how the pullback property of the right-hand square validates both the elimination rule and the $\eta$-rule.

To extend this setting to include subtyping in the form of vertical arrows,
we need to take into account that the action of $\funty$ (and $\absty$) should be contravariant only on the vertical arrows of the first component.

Contravariant actions of functors on some category $\ctg{B}$ are rendered by considering functors on the opposite category $\ctg{B}\opp$,
but here we want to take the opposite only of vertical arrows,
otherwise substitution, the action of $\funty$ on cartesian arrows, would go in the wrong direction.
So we cannot just replace $u$ with $u\opp \colon \uu\opp \to \ctx\opp$.
Instead, we want to construct a fibration
$u\vopp \colon \uu\vopp \to \ctx$
that has the same cartesian arrows of $u$, and vertical arrows going in the opposite direction

This can be done passing through the associated pseudo-functor:
write $\mathrm{P} \colon \Fib(\ctx) \to \Psd[\ctx\opp,\Cat]$
and $\mathrm{F} \colon \Psd[\ctx\opp,\Cat] \to \Fib(\ctx)$
for the two 2-functors realising the 2-equivalence in <ref>.
Then the fibration $u\vopp$ is the image under $\mathrm{F}$

of the pseudo-functor $\mathrm{P}(u)^{\text{o}} \colon \ctx^{\text{op}} \to \Cat$ defined by $\mathrm{P}(u)^{\text{o}}(X):=(\mathrm{P}(u)(X))^{\text{op}}$.
Equivalently, $u\vopp:= \mathrm{F}((-)\opp \circ \mathrm{P}(u))$.
It follows from the last equation that $(-)\vopp$ is 2-functorial.

Let $(u,\du,\Sigma,\Delta)$ be a gcwf equipped with two functors $\funty$ and $\absty$ making the square below a pullback.

\[\begin{tikzcd}
\uu\vopp {}_{\du\vopp\Delta\vopp}\!\!\times_{\du} \duu
\ar[d,"{\id \times \Sigma}"']
&	\mathrm{W}^*(\uu\vopp {}_{\du\vopp\Delta\vopp}\!\!\times_{\du} \duu)
\ar[d] \ar[r,"\absty"] \ar[l]
&	\duu	\ar[d,"{\Sigma}"]
\\
\uu\vopp {}_{\du\vopp\Delta\vopp}\!\!\times_u \uu
&	\uu\vopp {}_{u\vopp}\!\!\times_u \uu
\ar[l,"\mathrm{W}"'] \ar[r,"\funty"]
&	\uu
\end{tikzcd}\]

Then, in addition to the usual formation, introduction, elimination and computation rules for function types, the following rules are satisfied.

\[
\AxiomC{$\Gamma\vdash A' \leq_f A$}
\AxiomC{$\Gamma\vdash B\leq_g B'$}
\BinaryInfC{$\Gamma\vdash \funty(A,B) \leq_{\funty(f,g)} \funty(A',B')$}
\DisplayProof
\hspace{3em}
\AxiomC{$\Gamma.A \vdash b :_f B$}
\UnaryInfC{$\Gamma \vdash \absty(A,b) :_{\funty(\id_A,f)} \funty(A,B)$}
\DisplayProof
\]

§ THE `SUBTYPING' MONAD

We now deepen our intuition for both the properties and the features of this new construction. In particular, the process of taking into consideration vertical maps turns out to amount to the result of the action of a particular monad. Grothendieck fibrations are known to be strongly linked to certain (co)monads, to the point of them being classified as pseudo-algebras of a given one (cf. [8] for a recent review and extension). We here present a simple monad that has the nice feature of collecting vertical maps, and show that it actually produces gcwfs out of gcwfs.

We start from the endofunctor $(\Id_{-}/\Id_{-})\colon\Fib(\bb)\to\Fib(\bb)$ computing for each fibration $p\colon\ee\to\bb$ the comma object $(\Id_p/\Id_p)$, meaning the following (very boring) 2-limit below.

\[\begin{tikzcd}[ampersand replacement=\&]
{(\Id_p/\Id_p)} \& p \\
p \& p
\arrow["\Id_p"', from=2-1, to=2-2]
\arrow["\Id_p", from=1-2, to=2-2]
\arrow[from=1-1, to=2-1]
\arrow[from=1-1, to=1-2]
\arrow[shorten <=3pt, shorten >=3pt, Rightarrow, from=1-2, to=2-1]
\end{tikzcd}\]

To make the reding a bit smoother, we denote $(\Id_p/\Id_p)$ by $(p/p)$. Unpacking this categorical construction, one finds that the new fibration $(p/p)\colon\vcomma{\ee}{\ee}\to\bb$ has in the domain triples $(f,A',A)$ such that $f\colon A'\to A$ is a $p$-vertical map, while morphisms in $\vcomma{\ee}{\ee}$ are simply commutative squares.

There is a monad on $\Fib(\bb)$ with endofunctor $(\Id_{-}/\Id_{-})$.

Its associated unit has components $\eta\colon p \to Tp$ sending each object to its identity, while the multiplication $\mu_p\colon TTp\to Tp$ is fiber-wise composition – as objects in the total category of $TTp$ are squares of vertical maps, and vertical maps compose.

This simple construction we can actually extend to a gcwf, meaning we can use it to build out of a gcwf with type fibration $u$, a new gcwf with type fibration $Tu$.

Let $(u,\du,\Sigma \dashv\Delta)$ a gcwf. Then there are adjoint functors $\overline{\Sigma}\dashv\overline{\Delta}$ such that $(u/u,\Sigma/u,\overline{\Sigma}\dashv\overline{\Delta})$ is a gcwf.

If we look at the basic judgments this second gcwf is describing, we will find precisely the two introduced in <ref>, so that we can reformulate our old perspective:

$\Gamma \vdash A\ty$     $\Gamma \vdash a: A$

$u(A)=\Gamma$     $\du(a)=\Gamma,\Sigma (a) =A$

$\Gamma \vdash A'\leq_f A$     $\Gamma \vdash a:_g A$

$f\colon A'\to A$, $u(f)=\id_\Gamma$     $g\colon \Sigma a\to A$, $u(g)=\id_\Gamma$

into the newer following notation.

$\Gamma \vdash A\ty$     $\Gamma \vdash a: A$

$u(A)=\Gamma$     $\du(a)=\Gamma,\Sigma (a) =A$

$\Gamma \vdash A'\leq_f A$     $\Gamma \vdash a:_g A$

$(u/u)(f,A',A)=\Gamma$     $(\Sigma/u)(g,a,A)=\Gamma$, $p_2\circ\overline{\Sigma}(g,a,A)=A$

Notice now the symmetry of the first and the second two judgments: the two new ones can be regarded as `classifiers' for new types and terms themselves, in a way such that it is always possible to recover the original theory – one simply has to look at those vertical maps that, in particular, are identities.

A gcwf morphism $(u,\du,\Sigma\dashv\Delta)\to(v,\dv,\Sigma'\dashv\Delta')$ is the data of a pair $(H,\dot{H})$, with $H\colon u\to v$, $\dot{H}\colon \du\to\dv$ fibration morphisms such that $H\Sigma =\Sigma'\dot{H}$. We denote $\gcwf$ the category of gcwfs and gcwf morphisms, and $\gcwf(\bb)$ its subcategory with fixed context category $\bb$.

Again, it should be noted that gcwfs can be equipped with more interesting (and higher dimensional) structure <cit.>, but for the purposes of the present paper we are not interested in that.

The monad in <ref> can be lifted to a monad over $\gcwf(\bb)$.

If a monad is an object for abstract computation, this one in particular computes `subtyping judgements'. An interesting question is now to check what objects does iterating this computation produce: the first iteration collects vertical maps, and morphisms are squares; in particular, vertical morphisms are those squares having vertical (with respect to the original type fibration) components, therefore the second iteration produced the fibration of said `all vertical' squares; here morphisms are cubes, and the vertical ones are those where all `connecting' maps are vertical (again, with respect to the original type fibration), and so on.

§ FUTURE WORK

Of course the applications to constructors can be taken much further than what is done in <ref>, and considering more complex ones can lead to a new extension of the present theory. Our intention was to introduce the `vertical maps' perspective, so that whoever gets interested in categorical models for type theory is motivated to consider the benefit of including non-discrete fibrations – usually, all in all, at little additional cost.

We conclude this exposition with a take that was suggested to the first author by F. Dagnino, and which we believe might be of some interest: as a fibration can be regarded as an internal category in the category of discrete fibrations, it seems like the process of going from a theory without a notion of subtyping to a theory with subtyping is close to that of considering a category internal to another one. In this sense, our work is perhaps not best interpreted as a generalization of some known models, but as a structure internal to them.

[1]
Thorsten Altenkirch and Conor McBride.
Towards observational type theory.

[2]
Steve Awodey.
Natural models of homotopy type theory.
Mathematical Structures in Computer Science, 28(2):241–286,

[3]
Francis Borceux.
Handbook of Categorical Algebra, volume 2 of Encyclopedia
of Mathematics and its Applications.
Cambridge University Press, 1994.

[4]
Greta Coraglia and Ivan Di Liberti.
Context, judgement, deduction.
ArXiv e-prints, 2022.

[5]
Greta Coraglia and Jacopo Emmenegger.
A 2-dimensional analysis of categorical comprehensions.

[6]
Greta Coraglia.
Categorical structures for deduction.
PhD thesis, Università degli Studi di Genova, 2023.

[7]
Peter Dybjer.
Internal type theory.
In Stefano Berardi and Mario Coppo, editors, Types for Proofs
and Programs, pages 120–134, Berlin, Heidelberg, 1996. Springer Berlin

[8]
Jacopo Emmenegger, Luca Mesiti, Giuseppe Rosolini, and Thomas Streicher.
A comonad for grothendieck fibrations, 2023.

[9]
Alexander Grothendieck.
Categoriés fibrées et descente (Exposé VI).
Revêtements étales et groupe fondamental - SGA1, 1960-61.

[10]
J. Martin E. Hyland.
The effective topos.
In A.S. Troelstra and D. van Dalen, editors, The L. E. J.
Brouwer Centenary Symposium, volume 110 of Studies in Logic and the
Foundations of Mathematics, pages 165–216. Elsevier, 1982.

[11]
Bart Jacobs.
Comprehension categories and the semantics of type dependency.
Theoretical Computer Science, 107(2):169–207, 1993.

[12]
Peter T. Johnstone.
Sketches of an Elephant: A Topos Theory Compendium: 1 Volume
Oxford University Press UK, 2002.

[13]
Anders Kock and Gonzalo E. Reyes.
Doctrines in categorical logic.
In Studies in Logic and the Foundations of Mathematics,
volume 90, pages 283–313. Elsevier, 1977.

[14]
F. William Lawvere.
Functorial Semantics of Algebraic Theories: And, Some Algebraic
Problems in the Context of Functorial Semantics of Algebraic Theories.
Mount Allison University, 1963.

[15]
F. William Lawvere.
Equality in hyperdoctrines and comprehension schema as an adjoint
Proceedings of the American Mathematical Society, pages 1–14,

[16]
Daniel R. Licata and Robert Harper.
2-dimensional directed type theory.
Electronic Notes in Theoretical Computer Science, 276:263–289,
Twenty-seventh Conference on the Mathematical Foundations of
Programming Semantics (MFPS XXVII).

[17]
Zhen Lin Low.
Logic in a topos, 2013.

[18]
Rodolphe Lepigre and Christophe Raffalli.
Practical subtyping for curry-style languages.
ACM Trans. Program. Lang. Syst., 41(1):5:1–5:58, 2019.

[19]
Joachim Lambek and Philip J. Scott.
Introduction to higher-order categorical logic, volume 7.
Cambridge University Press, 1988.

[20]
Zhaohui Luo, Sergei Soloviev, and Tao Xue.
Coercive subtyping: Theory and implementation.
Information and Computation, 223:18–42, 2013.

[21]
Zhaohui Luo.
Coercive subtyping.
Journal of Logic and Computation, 9(1):105–130, 02 1999.

[22]
Maria E. Maietti and Giuseppe Rosolini.
Quotient completion for the foundation of constructive mathematics.
Logica Universalis, 7(3):371–402, 2013.

[23]
Paul-André Melliès and Noam Zeilberger.
Functors are type refinement systems.
SIGPLAN Not., 50(1):3–16, jan 2015.

[24]
Benjamin C. Pierce.
Types and Programming Languages.
MIT Press, 1 edition, February 2002.

[25]
Edmund Robinson and Giuseppe Rosolini.
Colimit completions and the effective topos.
The Journal of Symbolic Logic, 55(2):678–699, 1990.

[26]
Thomas Streicher.
Fibred categories à la Jean Bénabou.
arXiv preprint arXiv:1801.02927, 2022.

[27]
Noam Zeilberger.
Principles of type refinement (OPLSS 2016), 2016.

§ PROOFS

The first two rules, Subsumption (Sbsm) and Transitivity (Trans), simply follow from composition of vertical arrows. Substitution (Sbst) and Weakening (Wkn) are a bit trickier and make use of, precisely, the substitutional part of the structure, namely it being a fibration. We begin with Weakening, as it is a bit easier: consider that the premise of the rule is given by maps and objects as below.

\[\begin{tikzcd}[ampersand replacement=\&]
\& {A'} \\
\& A \& \uu \\
{\Gamma.B} \& \Gamma \& \bb
\arrow["{u\epsilon_B}", from=3-1, to=3-2]
\arrow["u", from=2-3, to=3-3]
\arrow["f", from=1-2, to=2-2]
\end{tikzcd}\]

Since $B$ is a type in context $\Gamma$, we can compute the counit $\epsilon\colon\Sigma\Delta B\to B$, which we know by (<ref>) that acts as weakening, in particular producing the context extension $u\epsilon_B\colon\Gamma.B\to\Gamma$. In the fiber over $\Gamma$, not only do we have $B$, but we also have a vertical map $f\colon A'\to A$. Applying the reindexing $(u\epsilon_B)^*$ to the three of them yields a new vertical map over $\Gamma.B$, hence the judgement $\Gamma.B\vdash (u\epsilon_B)^*A'\leq_{(u\epsilon_B)^*f} (u\epsilon_B)^*A$. In <ref> we have actually written $A$ for $(u\epsilon_B)^*A$, at it is customary for weakening rules – and as, in fact, it appears in (<ref>). All in all, the Weakening rule only tells us that subtyping is preserved through weakening.

Now let us get to Substitution. In order to prove it, we first need to recall how $B[a]$ is computed in a traditional natural model (cf. <cit.>): for given $\Gamma\vdash a:A$ and $\Gamma.A\vdash B$, $B[a]$ is the result of the reindexing $B$ along the (image of the) unit $\eta_a$. (This is not precisely how the original paper presents it, though it is equivalent to that: see <cit.> for a detailed discussion on the matter.) In our setting, the premises of (Sbst) start from the following.

\[\begin{tikzcd}[ampersand replacement=\&]
{\Sigma a} \& {\Sigma\Delta\Sigma a} \&\& {\Sigma a} \\
A \&\& {\Sigma\Delta A} \& A \& \uu \\
\Gamma \& {\Gamma.\Sigma a} \& {\Gamma.A} \& \Gamma \& \bb
\arrow["{\du\Delta g}", from=3-2, to=3-3]
\arrow["u", from=2-5, to=3-5]
\arrow["{\du\eta_a}", from=3-1, to=3-2]
\arrow["{u\epsilon_{\Sigma a}}", from=3-3, to=3-4]
\arrow["g", from=1-4, to=2-4]
\arrow[from=1-2, to=1-4]
\arrow[from=2-3, to=2-4]
\arrow[from=1-2, to=2-3]
\arrow[dashed, from=2-1, to=2-3]
\arrow[from=1-1, to=2-1]
\arrow[from=1-1, to=1-2]
\end{tikzcd}\]

Notice that, since $g$ is vertical, and the top horizontal compositions in the top diagram is an identity due to triangle identities of $\Sigma\dashv\Delta$, by cartesianness of the counit $\epsilon_A\colon\Sigma\Delta A\to A$ there is a unique map making the top diagram commute. Now, each `external' side in the top diagram is mapped to the identity through $u$, meaning we can repeat Awodey's argument, and the required vertical arrow is the result of reindexing along the (image of the) unit – post-composed with $\du\Delta g$. Notice that $a$ is only `allowed' to interact with $B,B'$ through $g$, which in turn does nothing to contexts, so that we are in our right to write, as customary, $B[a]$ for $(\du(\Delta g\circ\eta_a))^*B$.

It might not seem like it, but this last proof makes heavy use of the universal property of the comma object $(u/u)$, and it could be in fact entirely proved using that profusely. We point the interested reader to <cit.> for the corresponding alternative proof.

Each component of the unit in a gcwf is a monic arrow.
Indeed, let $f,g \colon a \to b$ in $\duu$ be such that $\eta_b f = \eta_b g$.
It follows that

\[
\du f = (u\epsilon_{\Sigma b})(\du \eta_b)(\du f)
= (u\epsilon_{\Sigma b})(\du \eta_b)(\du g) = \du g
\]

and, in turn, that $f = g$ since $\eta_b$ is cartesian. The left adjoint $\Sigma$ is then faithful.

In fact, it is easy to see that $\Sigma$ induces a bijection

\begin{equation}\label{jdtt-leftfaith-iso}
\begin{tikzcd}[column sep=4em]
\duu(a,b)	\ar[r,"\sim"]
&	\{ f \in \uu(\Sigma a, \Sigma b) \mid (\Sigma\eta_b)f = (\Sigma\Delta f)(\Sigma\eta_a) \}.
\end{tikzcd}
\end{equation}

Since $\eta_b$ is cartesian,
the counter-image of $f$ is the only arrow $g$ in $\duu(a,b)$ over $uf$
such that $\eta_b g = (\Delta f) \eta_a$.

This is straightforward, by reading the action of $\funty$ on vertical arrows
and unfolding the definitions of the judgements involved as in <ref>.

We begin by describing what the fibration of terms $(\Sigma/u)$ does: it simply collects pairs $(g,a,A)$ such that $g\colon\Sigma a\to A$ is a $u$-vertical map, and sends them to their underlying context. Its vertical maps are pairs of vertical maps (respectively $\du$- and $u$-vertical) fitting in appropriate squares, and its cartesian maps are pairs of cartesian maps (again, respectively, with reference to $\du$ and $u$).

The required typing functor, then, is simply $\overline{\Sigma}$ sending each triple $(g,a,A)$ to $(g,\Sigma a,A)$, which is cartesian because $\Sigma$ is. Describing its right adjoint requires a little more effort: for a triple $(f,A',A)$ in $(u/u)$ one considers its image through $\Delta$, then its vertical-cartesian factorization system (cf. <ref>), then the image of the vertical portion of it through $\Sigma$ to get back to $\uu$.

\[\begin{tikzcd}[ampersand replacement=\&]
{A'} \&\& {\Delta A'} \&\&\& {\Sigma\Delta A'} \&\& {A'} \\
A \&\& {a_f} \& {\Delta A} \&\& {\Sigma a_f} \& {\Sigma\Delta A} \& A
\arrow["f", from=1-1, to=2-1]
\arrow["{(\Delta f)^v}"', from=1-3, to=2-3]
\arrow["{(\Delta f)_c}"', from=2-3, to=2-4]
\arrow["{\Delta f}", from=1-3, to=2-4]
\arrow["{\epsilon_{A'}}", from=1-6, to=1-8]
\arrow["{\epsilon_A}"', from=2-7, to=2-8]
\arrow["f", from=1-8, to=2-8]
\arrow["{\Sigma\Delta f}", from=1-6, to=2-7]
\arrow["{\overline{\Delta}f=\Sigma(\Delta f)^v}"', from=1-6, to=2-6]
\arrow["{\Sigma(\Delta f)_c}"', from=2-6, to=2-7]
\end{tikzcd}\]

Cartesianness of $(\Delta f)_c$ can be used to provide functoriality. Let us now show how the two functors form an adjoint pair by means of the universal property of its counit, which is actually depicted on the right square above. For any triple $(g,b,B)$ in $(\Sigma/u)$ and morphism $(h,k)\colon \overline{\Sigma}(g,b,B)\to (f,A',A)$ we must show that there is a unique pair $(m,n)$ such that $\overline{\Sigma}(m,n)\colon \overline{\Sigma}(g,b,B)\to \overline{\Sigma}\overline{\Delta}(f,A',A)$ makes the obvious triangle commute. The universal property of the counit $\epsilon_A'$ yields a unique $m\colon b\to \Delta A'$ so that $h=\epsilon_{A'}\circ m$,

\[\begin{tikzcd}[ampersand replacement=\&]
{\Sigma b} \\
B \&\& {\Sigma\Delta A'} \&\& {A'} \\
\&\& {\Sigma a_f} \& {\Sigma\Delta A} \& A \\
\Theta \\
\&\& {\Gamma.A'} \& {\Gamma.A} \& \Gamma
\arrow["{\epsilon_{A'}}", from=2-3, to=2-5]
\arrow["{\epsilon_A}"', from=3-4, to=3-5]
\arrow["f", from=2-5, to=3-5]
\arrow["{\Sigma\Delta f}", from=2-3, to=3-4]
\arrow["{\overline{\Delta}f=\Sigma(\Delta f)^v}"', from=2-3, to=3-3]
\arrow["{\Sigma(\Delta f)_c}"', from=3-3, to=3-4]
\arrow["g"', from=1-1, to=2-1]
\arrow["h"{pos=0.1}, curve={height=-6pt}, from=1-1, to=2-5]
\arrow["k"'{pos=0.1}, curve={height=-6pt}, from=2-1, to=3-5]
\arrow["{\Sigma(!)}"', dashed, from=1-1, to=2-3]
\arrow[from=5-4, to=5-5]
\arrow[curve={height=-6pt}, from=4-1, to=5-5]
\arrow[from=5-3, to=5-4]
\arrow["{u\Sigma(!)}"', from=4-1, to=5-3]
\end{tikzcd}\]

hence a map filling the bottom diagram to a commuting triangle. By cartesianness of $\epsilon_A\circ\Sigma(\Delta f)_c$ there is a unique map $n\colon B\to\Sigma a_f$ making the `other' triangle commute as well.

Let us denote $(T,\eta,\mu)$ the desired monad. On objects it of course acts as $T(u,\du,\Sigma\vdash\Delta)=((u/u), (\Sigma/u), \overline{\Sigma}\dashv\overline{\Delta})$ as in <ref>. The image of a morphism $(H,\dot{H})$ is actually simply the action of $H$, and it provides a commutative square because $H\Sigma=\Sigma'\dot{H}$. Unit is again induced by identity, and multiplication by composition.


]Cluster Algebras and Scattering Diagrams

Part I

Basics in Cluster Algebras
This is the final manuscript of
Part I of the monograph “Cluster Algebras and Scattering Diagrams”,
MSJ Mem. 41 (2023) by the author.

]Tomoki Nakanishi

Graduate School of Mathematics, Nagoya University

This  is a first step guide to
the theory of cluster algebras.
We especially focus  on
basic notions, techniques, and results concerning seeds,
cluster patterns, and cluster algebras.


††thanks: Corresponding authors††thanks: Corresponding authors

# Breakup dynamics in primary jet atomization using mesh- and interface-
refined Cahn-Hilliard Navier-Stokes

Makrand A. Khanwale  Center for Turbulence Research, Stanford University,
Stanford, CA 94305, USA  Kumar Saurabh  Department of Mechanical Engineering,
Iowa State University, Ames, IA 50010, USA  Masado Ishii  School of Computing,
The University of Utah, Salt Lake City, UT 84112, USA  Hari Sundar  School of
Computing, The University of Utah, Salt Lake City, UT 84112, USA  Baskar
Ganapathysubramanian  Department of Mechanical Engineering, Iowa State
University, Ames, IA 50010, USA

###### Abstract

We present a technique to perform interface-resolved simulations of complex
breakup dynamics in two-phase flows using the Cahn-Hilliard Navier-Stokes
equations. The method dynamically decreases the interface thickness parameter
in relevant regions and simultaneously increases local mesh resolution,
preventing numerical artifacts. We perform a detailed numerical simulation of
pulsed jet atomization that shows a complex cascade of break-up mechanisms
involving sheet rupture and filament formation. To understand the effect of
refinement on the breakup, we analyze the droplet size distribution. The
proposed approach opens up resolved simulations for various multiphase flow
phenomena.

††preprint: APS/123-QED

##  I Introduction

A fluid jet injected into a lighter-density fluid (like air) exhibits a rich
tapestry of flow physics, including the rupture of fluid films into filaments,
the breakup of filaments into droplets, and a cascade of droplet breakup and
coalescence. Understanding this jet atomization process can transform how we
interact with, design, and control a wide array of natural and engineered
systems, for example, combustion, printing, coating, and spraying operations.

---

Figure 1: Consider a droplet in swirling flow. The swirling flow gradually
stretches out the droplet into a spiraling and thinning filament. Fig (a) is a
simulation with constant interface thickness, $\epsilon$, and shows spurious
breakup into droplets when the filament thickness becomes comparable to
$\epsilon$. In contrast, Fig (b) is a simulation where $\epsilon$ is always
smaller than the local filament thickness. See animations for the evolution in
both cases in the supplementary video

Jet atomization – the dynamics of generation of micro-droplets from a compact
fluid core via the breakup of unstable liquid sheets and filaments [1, 2] –
has proved notoriously challenging to understand, primarily due to the
presence of a wide range of spatial scales [3]. For instance, if we consider
the liquid jet diameter $D_{i}$, atomization produces fluid sheets that break
up into filaments. These thin sheets and long filaments have one (sheets) or
two (filaments) of their characteristic dimensions $100\times$ smaller than
$D_{i}$. The subsequent breakup of the filaments produces droplets as much as
$1000\times$ smaller than $D_{i}$. The ensuing 3D structures span nine orders
of magnitude in volume and must be resolved accurately to capture the droplet
distribution dynamics. Computationally resolving the spatio-temporal dynamics
of these multi-scale structures calls for approaches that accurately track the
fluid-air interface.

In diffuse interface simulations of multi-phase flow, the atomically thin
fluid-air interface is replaced with an interface having a much larger and
constant thickness, $\epsilon$, for computational efficacy. As long as the
relevant length scales are larger than $\epsilon$, such approaches work [4].
However, in phenomena like jet atomization, thin filaments and droplets have
characteristic dimensions that become comparable to $\epsilon$; thus, the
standard approach produces spurious artifacts like mass loss and nonphysical
breakup (see Fig. 1, and supplementary video of Fig. 1). While one could
choose a very small $\epsilon$, the associated computational cost makes this
infeasible. In this paper, our first modeling advance is to replace a constant
interface thickness model with a locally adaptive interface thickness. This
ensures that the (local) interface thickness, $\epsilon$, is always smaller
than the local length scales of interest (see Fig. 1), thus allowing interface
tracking approaches to reliably capture multi-scale features in a
computationally efficient manner. Note that automatically identifying the
local regions of interest where $\epsilon$ has to be adapted is itself non-
trivial. We leverage concepts from image processing (see Fig. 2) to build an
efficient approach to do so, which constitutes our second modeling advance.
While the first modeling advance is specific to diffuse interface approaches,
the second modeling advance applies to all interface capturing methods,
including sharp interface approaches. We briefly discuss the current
challenges of both sharp and diffuse interface approaches next and how the
current work (as illustrated in Fig. 1) resolves these challenges.

Figure 2: Flow chart describing the algorithm for detecting thin/small
interface features. (a) Start with the continuous field $\phi$; (b) Threshold
to produce a binary image; (c) An illustration of one step of erosion, the top
image shows a sample binary with white cells equal to 1, black cells equal to
the value of 0. Gray dots in the middle picture shows cells identified (with
at least one neighbor of 0) to be converted to 0. The bottom picture shows
binary after cells with Gray dots turned to 0; (d) Binary after 15 steps of
erosion on $\phi_{b}$; (e) An illustration of one step of dilation, the top
image shows a sample eroded binary. Gray dots in the middle picture shows
cells identified (with at least one neighbor 1) to be converted to 1. The
bottom picture shows binary after cells with Gray dots turned to 1; (f) Binary
after 20 steps of dilation on $\phi_{b,d}$;(g) Binary after original
$\phi_{b}$ is subtracted from $\phi_{b,d}$ which shows the identified small
filament region.

Sharp interface approaches have been very successful for high-fidelity
simulations of turbulent multiphase flows, including atomization [5, 6, 7, 8,
9, 10]. However – as in the case of the diffuse interface approaches – when
the interfacial features (droplets/filaments) are comparable to the grid size,
the numerical breakup is observed as the method tries to conserve volume; this
effect is also known as numerical surface tension [3]. Active research
continues towards methods – for example, interface reconstruction [11, 12],
moment-of-fluid [13], manifold death [14] – that resolve this issue. These
methods, however, remain computationally complex because the interface quality
is determined purely by the mesh resolution.

Diffuse interface approaches consider a computationally smeared out fluid-
fluid interface with thickness $\epsilon$. By keeping $\epsilon$ relatively
large, comparable results can be produced under coarser mesh resolutions.
These methods also avoid any interface reconstruction process, provide a
thermodynamically consistent way to handle surface tension [15], and are
endowed with desirable numerical properties like smoothness and energy
stability. However, when interfacial features have a comparable length scale
to $\epsilon$, diffuse interface methods also suffer from artificial breakup
and mass loss. We leverage that diffuse interface approaches allow us to
disentangle the interface thickness, $\epsilon$, from the mesh resolution.
When the interfacial feature length scales, $r$ become comparable to the
numerical interface thickness ($\epsilon/r\sim\mathcal{O}(1)$), we locally
reduce $\epsilon$. Subsequently, a more refined mesh resolution is needed only
locally to accurately capture this interface with lower $\epsilon$. This is
especially appealing over current approaches of decreasing $\epsilon/r$
everywhere, which are prohibitively expensive even with adaptive mesh
refinement.

Note that the ability to efficiently identify regions of interest for
subsequent local refinement is readily applicable to both sharp and diffuse
interface approaches, potentially improving a large array of interface-
capturing methods. This technique – implemented into our massively parallel,
adaptive mesh refined, multi-phase flow framework and described in detail in a
companion methods paper [16] (see also SI)– allows us to perform one of the
most detailed simulations of primary jet atomization at $64\times$ the
previous best possible resolution [10]. Specifically, we use a
thermodynamically consistent diffuse interface method that uses Cahn-Hilliard
Navier-Stokes (CHNS) as detailed in [17].

##  II Identification of regions of interest

We describe the algorithm (see Fig. 2) for identifying regions such as
filaments and small droplets where $\epsilon/r$ can become
$\sim\mathcal{O}(1)$. Consider a two-fluid system. The two fluid phases are
described by a phase field variable $\phi$, which varies continuously in
$[-1,1]$, with -1 and 1 corresponding to the pure phases; see panel (a) of
Fig. 2. The central thin part in the figure is a region of interest. We
perform a sequence of efficient image processing steps to identify this
region. We first threshold the continuous field, $\phi$ into a binary field,
$\phi_{b}$ 111$\phi\geq 0.8=1$ and $\phi\leq 0.8=0$ with each cell being
either 1 or 0 (see panel (b) in Fig. 2). We then perform a predetermined
number of morphological erosion steps (see panel (c) Fig. 2) on the binary
image 222One erosion step converts cells with a value of 1 to 0 if at least
one of the neighbors of the cell its neighbor is 0 to get $\phi_{b,e}$ (see
panel (d) Fig. 2).

We could subtract $\phi_{b,e}$ from the original binary $\phi_{b}$ to find the
filament region, but the erosion steps also remove parts of the bigger
structure. To recover the part of the bigger structure without recovering the
small feature, we perform a predetermined number of morphological dilation
steps 333The dilatation step involves converting the cell value from 0 to 1 if
at least one of its neighbors is 1. on the eroded binary $\phi_{b,e}$ to get
the dilated binary $\phi_{b,d}$ (panel (e) in Fig. 2). We perform slightly
more dilation steps than erosion steps to completely recover the larger
structure (see panel (f) Fig. 2). Finally, we subtract $\phi_{b}$ from
$\phi_{b,d}$ to get a binary field with non-zero values in the regions
representing the small features of interest (see panel (g) of Fig. 2).

We choose such a computational graphics-based approach for several reasons:
(a) computational complexity: all steps detailed above can be performed using
algorithms exhibiting $\mathcal{O}(N)$ complexity, where $N$ is the total
number of cells in the mesh, (b) parallel scalability: these algorithms can be
implemented to scale efficiently on a large number of processors. We refer
readers to the companion method papers [16] for a detailed discussion of
parallel deployment on octree meshes, (c) algorithmic alignment: these
algorithms (re)use the data structures and communication constructs present in
our existing, optimized codebase [18, 17]. We note that other approaches, for
instance, connected component analysis, can also be applied. But these come at
a higher computational cost, specifically in a distributed setting, and our
experiments indicated that they could not identify all features of interest
(like long thin filaments attached to larger structures).

To demonstrate the capability of the identification algorithm, we choose a
popular problem of a drop in swirling flow, which is often used to test
interface methods, especially under resolution constraints [19, 20, 21]. A
circle with radius 0.15, centered at $(0.5,0.75)$ is placed inside a unit box
(origin at bottom left corner) and undergoes advection in a swirling velocity
field given by the stream function $\varphi(x,y,t)=\frac{1}{\pi}\sin^{2}(\pi
x)\sin^{2}(\pi y)$. We set $\epsilon$ to 0.0025. The circle advects and
deforms to form concentric thin filaments. With increasing time, the thickness
of the filament becomes comparable to the interface thickness, and we see
breakup and coarsening for CHNS, Fig. 1. In sharp interface methods like VOF,
as the filament grows thinner, they break into droplets under limited mesh
resolution, thus showing a ”numerical” surface tension (see Fig. 5.21 in
[21]). Therefore, we see a breakup for both sharp and diffuse interface
methods due to limiting mesh resolution. Our approach detects thin filaments’
regions as they develop. We adaptively reduce the interface thickness
$\epsilon$ in those regions (to 0.001) and locally use a higher mesh
resolution. Consequently, the numerical breakup is prevented. Figure 1 shows
the comparison between the case of constant $\epsilon$ (panel (a)) compared to
the case where we dynamically decrease $\epsilon$ (panel (b)). We provide
videos of simulations for significantly longer times (up to $t=8$) in the
supplementary files, which illustrates the utility of this approach.

Figure 3:  A snapshot of the mesh overlay on the zoomed-in 2D plane view of
the diffuse interface at the mid-z plane.

##  III Primary jet atomization

We deploy this approach on the challenging problem of pulsed primary jet
atomization from Pairetti  _et al._ [10] with high Reynolds numbers
($Re_{gas}=25000$, $Re_{liquid}=5800$)
444$Re_{liquid}=\rho_{liquid}U_{i}D_{i}/\mu_{liquid}$,
$Re_{gas}=\rho_{gas}U_{i}D_{i}/\mu_{gas}$,
$We_{gas}=\rho_{gas}U^{2}_{i}D_{i}/\sigma=430$, and
$We_{gas}=\rho_{liquid}U^{2}_{i}D_{i}/\sigma=11600$. A liquid jet with the
properties of diesel is pulsed into a large box filled with air. The max inlet
velocity, $U_{i}$ is 100 $\mathrm{m}\mathrm{/}\mathrm{s}$ with the diameter of
the injection $D_{i}=$100\text{\,}\mathrm{\SIUnitSymbolMicro m}$$. All
simulation parameters and boundary conditions are identical to those in [10]
and are detailed in the supplementary material. Analysis by Pairetti  _et al._
[10] revealed that mesh resolution significantly affects breakup statistics.
They showed that even using the finest mesh refinement level of 13 –
corresponding to the cell size of $30D_{i}/2^{13}$=
$0.36\text{\,}\mathrm{\SIUnitSymbolMicro m}$ – still produces structures of
the same order as the mesh.

Here, our approach allows us to reach a mesh refinement of 15, corresponding
to a finest cell size of $30D_{i}/2^{15}$ =
$0.0915\text{\,}\mathrm{\SIUnitSymbolMicro m}$. We believe this to be one of
the finest resolution simulations of primary jet atomization. Our simulation
spanned 120000 timesteps reaching 6.3 $\mathrm{\SIUnitSymbolMicro s}$, and
required over $200,000$ node hours on the supercomputer, TACC Frontera 555We
estimate that without dynamic $\epsilon$, using level 15 everywhere on the
interface would result in a $20\times$ more expensive simulation[16].

The dynamics are characterized by two length scales, Kolmogorov and Hinze. The
Kolmogorov length scales represent the size of the smallest turbulent
structures (in both liquid $\eta_{l}$ and air $\eta_{g}$), and the Hinze scale
($\xi$) represent the size of the biggest drop that does not suffer breakup by
turbulent fluctuations 666$\eta_{l}=D_{i}/Re_{l}^{3/4}$,
$\eta_{g}=D_{i}/Re_{g}^{3/4}$, $\epsilon=\nu_{gas}^{3}/\eta_{gas}^{4}$,
$\xi=0.75\left(\sigma/\rho_{gas}\right)^{3/5}\left(\epsilon/\rho_{gas}\right)^{-2/5}$.
Here, $\eta_{l}=$0.131\text{\,}\mathrm{\SIUnitSymbolMicro m}$$,
$\eta_{g}=$0.078\text{\,}\mathrm{\SIUnitSymbolMicro m}$$, and
$\xi=$9.71\text{\,}\mathrm{\SIUnitSymbolMicro m}$$. To achieve DNS resolution,
the mesh size $h\leq 2\min(\eta_{l},\eta_{g})$. We achieve DNS resolution near
the dynamically refined interface. The fine resolution near the interface
resolves the fine-scale shear instabilities near the interface, which impact
breakup mechanisms.

We start with a non-dimensional interface thickness $\epsilon_{1}=0.001$.
Using the algorithm in Fig. 2, we locally decrease the interface thickness to
$\epsilon_{2}=0.00075$. The refinement in these regions changes from level 13
to level 15. Figure 3 shows the mesh overlaid on the diffuse interface on a
zoomed-in view of a mid-z slice near the top of the jet. Notice that our
algorithm detects small droplets and sheets and imposes a smaller $\epsilon$
in these thin regions, with a finer resolution (level 15) only in these
regions. Such a selected decrease in $\epsilon$ allows us to prevent numerical
breakup and Ostwald ripening. As seen in Figure 3, we impose an extended
region of refinement near the interface 777either level 13 if $\epsilon$ =
0.001 or level 15 if the $\epsilon$ = 0.00075.. Thus, any droplet formed with
a length scale less than the Hinze length does not break up further through
turbulent fluctuations.

This strategy allows tracking both droplets as well as thin sheets and
filaments. We discovered that (see Figure 4 and accompanying video) sheets are
formed as early as $1.68\text{\,}\mathrm{\SIUnitSymbolMicro s}$. This is in
contrast to lower resolution studies that report sheet formation around
$5\text{\,}\mathrm{\SIUnitSymbolMicro s}$ [10]. As the jet evolves, we notice
a cascade of sheet ruptures near the jet’s tip, forming filaments (see Fig.
4). This destabilization and rupture is typically via the Kelvin-Helmholtz
instability. This rupture can be seen in the blue bounding boxes in Figure
4(right). To our best knowledge, this is the first time that such rupture
dynamics have been computationally captured. The filaments then fragment to
form droplets through the Rayleigh-Plateau instability. Representative
filament fragmentation events are indicated with red bounding boxes in Figure
4(bottom). Capturing this cascade of breakup phenomena is necessary for
correctly computing the breakup statistics.

Figure 4: Isocontour of diffuse interface parameter showing the liquid-air
interface at $6.2\text{\,}\mathrm{\SIUnitSymbolMicro s}$. We present two
zoomed-in views of the jet, one focusing on sheet rupture on the right and the
second focusing on filament breakup below. Examples of sheet ruptures are
marked with blue rectangles, and examples of filament breakup are marked with
red ellipses. Please see supplementary information for a full animation of the
evolution of the jet.
$10^{0}$$10^{1}$$10^{0}$$10^{1}$$10^{2}$$10^{3}$$10^{-0.5}$$10^{0.5}$$d\left($\text{\,}\mathrm{\SIUnitSymbolMicro
m}$\right)$$\text{N}_{\text{Drops}}$ Figure 5:  Droplet statistics in jet
atomization at $6.21\text{\,}\mathrm{\SIUnitSymbolMicro s}$:  A histogram of
the number of droplets for a range of logarithms of the length scales (in
$\text{\,}\mathrm{\SIUnitSymbolMicro m}$) representing the droplets. We fit
the Log-normal PDF with a mean of $10^{0.3}$ and a standard variation of
$10^{0.28}$ shown with the red curve. The black vertical line shows the
thinnest interface thickness used $\epsilon_{2}=4h$, where $h$ is the size of
the smallest mesh element. The blue vertical line represents the Hinze scale
$\xi$, and the black vertical line represents the diffuse interface thickness
$\epsilon_{2}$.

We construct breakup statistics by computing the ensuing structures’
representative length scale ($d$). We compute the volume ($V_{d}$) of each
connected components, and then calculate $d=\left(6V_{d}/\pi\right)^{1/3}$.
Breakup statistics are constructed at the final time of our simulation,
$6.3\text{\,}\mathrm{\SIUnitSymbolMicro s}$. Figure 5 shows this size
distribution of droplets, along with a best-fit log-normal distribution. We
point out several observations:

  * •

The mean value of the histogram is much larger than the interface thickness
(indicated by the black vertical line). Additionally, most of the histogram is
smaller than the Hinze scale $\xi$; therefore, the bulk of the distribution
consists of droplets that will not further break up due to turbulence. The
log-normal fit to droplet distribution has also been observed in other jet
atomization simulations (see [7, 10]). The distribution suggests that all the
features in the distribution are well resolved.

  * •

The histogram is to the right of the interface thickness. This indicates that
all the resolved drops are larger than the interface thickness. Furthermore,
drops smaller than the interface thickness are not resolved by the method and
do not pollute the statistics. In the accompanying movie, we observe that
droplets with sizes around the order of the interface thickness get absorbed
into nearby larger structures due to the coarsening nature of the Cahn-
Hilliard equation, which is why we do not see tails in the droplet size
distribution near the interface thickness. One could resolve these smaller
droplets by deploying a multi-level interface thickness refinement. That is,
the interface thickness can be recursively refined to capture smaller and
smaller droplets.

  * •

We notice no pile-up of droplets with a length scale smaller than the
interface thickness. This indicates that no artificial droplets result from
numerical breakup due to low mesh resolution, unlike other state-of-the-art
volume-of-fluid simulations.

The source code and associated datasets of the simulation are publicly
available. We anticipate this to produce lively discussions and analysis of
the data. We continue to analyze the hydrodynamical conditions of sheet
rupture and plan to deploy another level of interface refinement to capture
smaller droplets. A follow-up paper will present an additional analysis of the
hydrodynamic conditions of different breakup events and the turbulent
statistics of the flow. While the computational approach has been used to
model an important canonical multi-flow physics problem, this approach has
wide applicability to other fluid mechanics phenomena, like low Reynolds
number ligament breakup.

###### Acknowledgements.

Acknowledgments: We acknowledge fruitful conversations with Prof. Ali Mani and
Prof. Marcus Herrmann. We thank Greg Foss and Dave Semeraro for the detailed
and insightful visualizations. We thank TACC Frontera and XSEDE program for
computational resources.

## References

  * Villermaux [2007] E. Villermaux, Annual Review of Fluid Mechanics 39, 419 (2007).
  * Majumdar and Tirumkudulu [2018] N. Majumdar and M. S. Tirumkudulu, Physical Review Letters 120, 164501 (2018).
  * Gorokhovski and Herrmann [2008] M. Gorokhovski and M. Herrmann, Annu. Rev. Fluid Mech. 40, 343 (2008).
  * Yue  _et al._ [2007] P. Yue, C. Zhou, and J. J. Feng, Journal of Computational Physics 223, 1 (2007).
  * Fuster  _et al._ [2009] D. Fuster, A. Bagué, T. Boeck, L. Le Moyne, A. Leboissetier, S. Popinet, P. Ray, R. Scardovelli, and S. Zaleski, International Journal of Multiphase Flow 35, 550 (2009).
  * Tomar  _et al._ [2010] G. Tomar, D. Fuster, S. Zaleski, and S. Popinet, Computers & Fluids 39, 1864 (2010).
  * Herrmann [2010] M. Herrmann, Journal of Engineering for Gas Turbines and Power 132, 061506 (2010).
  * Shinjo and Umemura [2011] J. Shinjo and A. Umemura, International Journal of Multiphase Flow 37, 1294 (2011).
  * Hasslberger  _et al._ [2019] J. Hasslberger, S. Ketterl, M. Klein, and N. Chakraborty, Journal of Fluid Mechanics 859, 819 (2019).
  * Pairetti  _et al._ [2020] C. I. Pairetti, S. M. Damián, N. M. Nigro, S. Popinet, and S. Zaleski, Atomization and Sprays 30, 913 (2020).
  * Lu and Tryggvason [2018] J. Lu and G. Tryggvason, Physical Review Fluids 3, 084401 (2018).
  * Chiodi [2020] R. M. Chiodi,  _Advancement of numerical methods for simulating primary atomization_ (Cornell University, 2020).
  * Jemison  _et al._ [2015] M. Jemison, M. Sussman, and M. Shashkov, Journal of Computational Physics 285, 149 (2015).
  * Chirco  _et al._ [2022] L. Chirco, J. Maarek, S. Popinet, and S. Zaleski, Journal of Computational Physics 467, 111468 (2022).
  * Anderson  _et al._ [1998] D. M. Anderson, G. B. McFadden, and A. A. Wheeler, Annual Review of Fluid Mechanics 30, 139 (1998).
  * Saurabh  _et al._ [2022] K. Saurabh, M. Ishii, M. A. Khanwale, H. Sundar, and B. Ganapathysubramanian, arXiv preprint arXiv:2209.12130 (2022).
  * Khanwale  _et al._ [2021] M. A. Khanwale, K. Saurabh, M. Ishii, H. Sundar, J. A. Rossmanith, and B. Ganapathysubramanian, arXiv preprint arXiv:2107.05123 (2021).
  * Saurabh  _et al._ [2021] K. Saurabh, M. Ishii, M. Fernando, B. Gao, K. Tan, M.-C. Hsu, A. Krishnamurthy, H. Sundar, and B. Ganapathysubramanian, in  _Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis_ (2021) pp. 1–15.
  * Bell  _et al._ [1989] J. B. Bell, P. Colella, and H. M. Glaz, Journal of computational physics 85, 257 (1989).
  * Rider and Kothe [1998] W. J. Rider and D. B. Kothe, Journal of computational physics 141, 112 (1998).
  * Tryggvason  _et al._ [2011] G. Tryggvason, R. Scardovelli, and S. Zaleski,  _Direct numerical simulations of gas–liquid multiphase flows_ (Cambridge university press, 2011).