# The Frobenius equivalence and Beck–Chevalley condition for Algebraic Weak
Factorisation Systems

Wijnand van Woerkom and Benno van den Berg

###### Abstract.

If a locally cartesian closed category carries a weak factorisation system,
then the left maps are stable under pullback along right maps if and only if
the right maps are closed under pushforward along right maps. We refer to this
statement as the Frobenius equivalence and in this paper we state and prove an
analogical statement for algebraic weak factorisation systems. These algebraic
weak factorisation systems are an explicit variant of the more traditional
weak factorisation systems in that the factorisation and the lifts are part of
the structure of an algebraic weak factorisation system and are not merely
required to exist. Our work has been motivated by the categorical semantics of
type theory, where the Frobenius equivalence provides a useful tool for
constructing dependent function types. We illustrate our ideas using split
fibrations of groupoids, which are the backbone of the groupoid model of
Hofmann and Streicher.

##  1\. Introduction

In this paper we contribute to theory of _algebraic weak factorisation
systems_ (or awfss, for short). The notion of an awfs is due to Garner [7],
building on earlier ideas by Grandis and Tholen [8]. The notion of an awfs is
a refinement of the well-known notion of a weak factorisation system (wfs),
which has become quite important in homotopy theory and category theory. In
particular, Quillen’s influential notion of a model category involves two weak
factorisation systems which interact in a suitable manner [10].

The notion of an algebraic weak factorisation system can be seen as a more
explicit version of the more familiar notion of a wfs. To explain this, let us
recall that a wfs on a category $\mathcal{C}$ consists of two classes of maps
in $\mathcal{C}$, let us denote them by $\mathcal{L}$ and $\mathcal{R}$, which
have the following properties:

  1. (1)

Any map in $\mathcal{C}$ factors as a map in $\mathcal{L}$ followed by a map
in $\mathcal{R}$.

  2. (2)

Any map in $\mathcal{L}$ lifts again any map in $\mathcal{R}$, in the sense
that in any solid commutative square

${\bullet}$${\bullet}$${\bullet}$${\bullet}$$\scriptstyle{\in{\mathcal{L}}}$$\scriptstyle{\in\mathcal{R}}$

in which the map on the left belongs to $\mathcal{L}$ and the map on the right
to $\mathcal{R}$, there exists a dotted arrow (the _lift_) as shown, making
both triangles commute.

  3. (3)

Maps in $\mathcal{L}$ and $\mathcal{R}$ are closed under retracts.

The theory of awfss is more “explicit” in that when we are given an awfs, we
will have explicit witnesses for the truth of axioms (1) and (2): that is, for
an awfs both the factorisation in (1) as well as the lift in (2) can be
obtained in an explicit manner and are not just assumed to exist. However, in
(2) the lift is given as a function which includes explicit witnessing
information for the fact that the map on the left belongs to $\mathcal{L}$ and
the map on the right to $\mathcal{R}$. Indeed, when one is given an awfs, this
involves both a monad $\mathsf{R}=(R,\eta,\mu)$ and a comonad
$\mathsf{L}=(L,\varepsilon,\delta)$ on the category of arrows of
$\mathcal{C}$. The _property_ of being an $\mathcal{L}$-map is then replaced
by the _structure_ of being a coalgebra for the comonad $\mathsf{L}$ and the
_property_ of being an $\mathcal{R}$-map is then replaced by the _structure_
of being an algebra for the monad $\mathsf{R}$; and it is terms of this
structure that the lift in (2) can be constructed.

The theory of algebraic weak factorisation systems has a number of advantages
over the usual theory:

  1. (1)

Due to its explicit nature, it is more constructive than the usual theory.

  2. (2)

In an awfs, the coalgebras are closed under colimits and the algebras under
limits, in an appropriate sense.

  3. (3)

They can be used to describe situations that are not wfss, because algebras
and coalgebras need not be closed under retracts. For example, split
Grothendieck fibrations are the algebras for a monad in an awfs, while not
being closed under retracts.

For the purposes of this paper, points (1) and (3) are the important ones.
Indeed, we feel that point (1) has recently become especially important due to
the influence of _homotopy type theory_ (HoTT) [16]. Here, type theory refers
to formal systems, like the Calculus of Constructions or Martin-Löf’s
intuitionistic type theory, which are both constructive foundations for
mathematics and functional programming languages. Recent developments have
amply demonstrated how ideas from homotopy theory and higher category theory
are highly relevant to type theory. In particular, Voevodsky has shown how one
can exploit the Kan–Quillen model structure on simplicial sets to construct a
model of type theory there which validates principles like his Univalence
Axiom or Higher Inductive Types [13].

This paper focuses on an important aspect of model constructions like those of
Voevodsky which make use of Quillen’s model categories to obtain models of
type theory: how they model $\Pi$-types. $\Pi$-types, or dependent function
types, are arguably the most important type former in type theory and the
argument for why these model categories model them is basically always as
follows. The underlying category is a presheaf category and hence locally
cartesian closed: this means that pullback functors have right adjoints, which
we will call _pushforward functors_. To show that we have a model of
$\Pi$-types, we need that pushforward functors along $\mathcal{R}$-maps
(fibrations) preserve $\mathcal{R}$-maps (fibrations). Using general facts
about adjoints (as well as axiom (3) for a wfs), this is equivalent to the
pullback functors along $\mathcal{R}$-maps preserving $\mathcal{L}$-maps. We
will refer to this equivalence as the _Frobenius equivalence_ and the latter
property as the _Frobenius property_. The Frobenius property is often easier
to check than the original statement; for instance, the Frobenius property
will hold in a model category if it is right proper and the cofibrations are
stable under pullback.

The main contribution of this paper is to find suitable analogues of these
statement for algebraic weak factorisation systems. That is, we will formulate
appropriate forms of the statement that algebras are closed under pushforward
along algebras and the Frobenius property for awfss, and we will prove that
these are equivalent. In order to model type theory, one needs suitably
“stable” versions of both the pushforward and the Frobenius property. This
amounts to requiring an additional property, a version of the well-known
Beck–Chevalley condition, and we will also formulate an appropriate version of
the Beck–Chevalley conditions for awfss.

To prove the various equivalences, the connection between awfss and double
categories will be crucial. The way double categories come in is that as
double categories the algebras and coalgebras in an awfs still determine each
other. To explain this a bit better, recall that the algebras and coalgebras
are not closed under retracts in an awfs as axiom (3) for a wfs would suggest.
However, axiom (3) is equivalent to another axiom. To formulate it, let us say
that $f$ has the right lifting property (RLP) against $g$ and $g$ the left
lifting property (LLP) against $f$, denoted $f\pitchfork g$, if for any solid
commutative square

${\bullet}$${\bullet}$${\bullet}$${\bullet}$$\scriptstyle{g}$$\scriptstyle{f}$

there exists a dotted lift as shown. If $\mathcal{A}$ is some class of maps in
a category $\mathcal{C}$, we will write:

$\displaystyle\mathcal{A}^{\pitchfork}$ $\displaystyle=$
$\displaystyle\\{f\,:\,(\forall g\in\mathcal{A})\,g\pitchfork f\\},$
$\displaystyle{}^{\pitchfork}\mathcal{A}$ $\displaystyle=$
$\displaystyle\\{g\,:\,(\forall f\in\mathcal{A})\,g\pitchfork f\\}.$

In those terms, axiom (3) is equivalent (over axioms (1) and (2)) to:

  1. (3)′

${}^{\pitchfork}\mathcal{R}\subseteq\mathcal{L}$ and
$\mathcal{L}^{\pitchfork}\subseteq\mathcal{R}$.

(So axioms (2) and (3) together are equivalent to
${}^{\pitchfork}\mathcal{R}=\mathcal{L}$ and
$\mathcal{L}^{\pitchfork}=\mathcal{R}$.) The fact that $\mathcal{L}$ and
$\mathcal{R}$ determine each other through lifting properties is very useful
and, indeed, this is what is used in the proof of the Frobenius equivalence.
While we no longer have that algebras and coalgebras are closed under
retracts, we do still have that they determine each other through lifting
properties, but to state these we need the language of double categories.

As it happens, in recent work [2], John Bourke has shown that the notion of an
awfs can be formulated purely in terms of double categories and a double-
categorical lifting property. It is this definition (called a lifting awfs
there) that is especially useful for this paper and we will use that
definition, and not the equivalent one using monads and comonads, to prove the
Frobenius equivalence for awfss.

In this paper we develop this Frobenius equivalence for awfss in a step-by-
step manner as it allows us to gradually introduce the main technical and
conceptual points of this paper. Indeed, it has been our experience that by
conceptualising matters in the right way we can tell a clear story while also
avoiding a lot of messy calculations. For that reason, we start this paper by
going over the Frobenius equivalence for weak factorisation systems in some
detail in Section 2. This material is well-known, but we will develop it in a
particular way, as this allows us to smoothly transition to the more technical
setting of an algebraic weak factorisation system. In particular, we emphasise
that it is more convenient to think of pullback and pushforward as operations
acting on the maps of a slice category (the “arrow view”) rather than the
objects of a slice category (the “object view’). Before developing a Frobenius
equivalence for double categories of maps, we first develop a Frobenius
equivalence for categories of maps in Section 3. After that, we define double
categories and (lifting) awfss in Section 4 and state and prove the Frobenius
equivalence for double categories of maps and awfss in Section 5, building on
the work in Section 3. For obtaining models of type theories with dependent
function types, we need another stability condition for these $\Pi$-types: the
Beck-Chevalley condition. We take a closer look at this condition in Sections
6 and formulate an equivalent condition that should make it easier to verify
in concrete cases. After a digression in Section 7, where we discuss a
strengthening of the Frobenius condition one also encounters in the
literature, we show how our framework can be used to obtain a model of type
theory with dependent function types, as well as other type formers, such as
identity and dependent sum types. We illustrate these ideas using split
fibrations of groupoids, the backbone of the groupoid model of Hofmann and
Streicher [11].

This paper is based on the MSc thesis of the first author, which was
supervised by the second author [20].

##  2\. The Frobenius equivalence for classes of maps

In this section we will go over the Frobenius equivalence for weak
factorisation systems in some detail. We do this, not because this material is
novel (it is not), but because we found that by thinking about this material
in a certain way, the generalisation to settings like that of algebraic weak
factorisation systems becomes much more natural. Therefore we start this
section by recalling the definition of a weak factorisation system and
outlining a perspective on the Frobenius equivalence. We will then go on to
give a detailed proof of the Frobenius equivalence for weak factorisation
systems following this outline.

###  2.1. Weak factorisation systems

In what follows we frequently work in the context of some (small) ambient
category ${\mathcal{C}}$ which is (sufficiently) locally cartesian closed, and
write ${\mathcal{C}}_{1}$ for the set (or class) of morphisms in
${\mathcal{C}}$. Of central importance will be various notions of _lifting_.
Given two morphisms $f,g\in{\mathcal{C}}_{1}$ we say $f$ has the left lifting
property with respect to $g$, and $g$ the right lifting property with respect
to $f$, denoted $f\pitchfork g$, if every commutative square $(u,v):f\to g$
has a diagonal filler $\phi:\operatorname{cod}f\to\operatorname{dom}g$ making
both of the induced triangles commute:

(2.1) ${\bullet}$${\bullet}$${\bullet}$${{\bullet\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{\phi}$

Given a subclass $J\subseteq{\mathcal{C}}_{1}$ of morphisms in ${\mathcal{C}}$
we define

$\displaystyle{{}^{\pitchfork}}J$ $\displaystyle=\\{f\in{\mathcal{C}}_{1}\mid
f\pitchfork g\text{ for all $g\in J$}\\},\text{ and}$ $\displaystyle
J{{}^{\pitchfork}}$ $\displaystyle=\\{f\in{\mathcal{C}}_{1}\mid g\pitchfork
f\text{ for all $g\in J$}\\}.$

######  Definition 1.

A _weak factorisation system_ (wfs) on ${\mathcal{C}}$ is a pair $(L,R)$ of
subclasses $L,R\subseteq{\mathcal{C}}_{1}$ satisfying two axioms:

  1. (1)

_Axiom of lifting_ : $L={{}^{\pitchfork}}R$ and $R=L{{}^{\pitchfork}}$.

  2. (2)

_Axiom of factorisation_ : every morphism $f\in{\mathcal{C}}_{1}$ admits a
factorisation $f=r.l$ with $l\in L$ and $r\in R$.

The set $L$ is referred to as the _left_ class of the wfs, and $R$ as the
_right_ class.

######  Remark 2.

Throughout this work we follow the notational conventions of [3, 2], in using
the letters $J$ and $K$ to denote arbitrary classes of morphisms in a
category, and the letters $L$ and $R$ to denote the classes making up a weak
factorisation system. However, we will often also consider general pairs
$(J,K)$ of subclasses of ${\mathcal{C}}_{1}$, and also then we will speak of
left and right maps to refer to morphisms from $J$ and $K$, respectively.

###  2.2. The Frobenius equivalence in outline

When ${\mathcal{C}}$ is locally cartesian closed every morphism
$f\in{\mathcal{C}}_{1}$ induces an adjunction $f^{*}\dashv f_{*}$ of pullback
and pushforward along $f$, respectively. The two properties of a wfs on such a
category that we will be concerned with in this paper are the following.

######  Definition 3.

A wfs $(L,R)$ on a locally cartesian closed category ${\mathcal{C}}$ satisfies
the _Frobenius property_ if $L$ is closed under pullback along $R$, and the
_pushforward property_ if $R$ is closed under pushforward along $R$.

######  Proposition 4 (Frobenius equivalence for a wfs).

A wfs satisfies the Frobenius property if and only if it satisfies the
pushforward property.

The statement of the Frobenius equivalence of Proposition 4 can be understood
as the result of combining the following two well-known results on wfs.

######  Proposition 5.

Let $F\dashv G:{\mathcal{D}}\to{\mathcal{C}}$ be an adjunction, $(L,R)$ a wfs
on ${\mathcal{C}}$, and $(L^{\prime},R^{\prime})$ one on ${\mathcal{D}}$; then
$F(L)\subseteq L^{\prime}$ if and only if $G(R^{\prime})\subseteq R$.

This statement roughly says that a left adjoint preserves left maps if and
only if its right adjoint preserves right maps. Following the terminology of
[3] we will refer to this and similar results as _change of base_.

######  Proposition 6.

Given a wfs $(L,R)$ on a category ${\mathcal{C}}$ and an object
$A\in{\mathcal{C}}$ there is a wfs $(L/A,R/A)$ on the slice category
${\mathcal{C}}/A$.

The wfs produced by Proposition 6 are often called _slice_ wfs. The left and
right maps of the slice wfs on ${\mathcal{C}}/A$ are those maps in
${\mathcal{C}}/A$ whose underlying morphisms are left or right maps,
respectively.

Proposition 5 now combines with Proposition 6 to yield a slightly more general
version of the Frobenius equivalence.

######  Corollary 7.

Let $f:A\to B$ be a morphism in ${\mathcal{C}}$ and $(L,R)$ a wfs on
${\mathcal{C}}$, then $f^{*}(L/B)\subseteq L/A$ if and only if
$f_{*}(R/A)\subseteq R/B$.

###### Proof.

By Proposition 6 we obtain two slice wfs $(L/A,R/A)$ and $(L/B,R/B)$ on
${\mathcal{C}}/A$ and ${\mathcal{C}}/B$ respectively. We have an adjunction
$f^{*}\dashv f_{*}:{\mathcal{C}}/A\to{\mathcal{C}}/B$ and so Proposition 5
tells us $f^{*}(L/B)\subseteq L/A$ if and only if $f_{*}(R/A)\subseteq R/B$. ∎

######  Remark 8.

While Proposition 4 and Corollary 7 are clearly very similar, there are still
some notable differences between them; for example, Proposition 4 is about
base change along right maps, whereas in Corollary 7 the base change is
performed along an arbitrary morphism. We will get back to these differences
in Section 2.6.

As a matter of fact, the proofs of Propositions 5 and 6 do not rely on the
axiom of factorisation of wfs, but only on the axiom of lifting. They can
therefore be stated for what are called _pre_ -wfs in [2, 4], but which we
will call _closed lifting pairs_ , i.e. pairs $(J,K)$ satisfying
$J={{}^{\pitchfork}}K$ and $K=J{{}^{\pitchfork}}$. We thus see that the
Frobenius equivalence of Corollary 7 consists of the following key components.

  1. (1)

_Lifting_ : A definition of lifting with respect to a subclass
$J\subseteq{\mathcal{C}}_{1}$, giving rise to subclasses of left lifting
${{}^{\pitchfork}}J\subseteq{\mathcal{C}}_{1}$ and right lifting
$J{{}^{\pitchfork}}\subseteq{\mathcal{C}}_{1}$. In turn, this yields the
notion of a closed lifting pair $(J,K)$ satisfying $J={{}^{\pitchfork}}K$ and
$K=J{{}^{\pitchfork}}$.

  2. (2)

_Base change_ : A result relating closed lifting pairs along adjunctions.

  3. (3)

_Slicing_ : An extension of the slice category construction ${\mathcal{C}}/A$
for some object $A\in{\mathcal{C}}$ to a subclass
$J\subseteq{\mathcal{C}}_{1}$, yielding a subclass
$J/A\subseteq({\mathcal{C}}/A)_{1}$. This construction should preserve closed
lifting pairs, meaning that when $(J,K)$ is a closed lifting pair, then so is
$(J/A,K/A)$.

Once these components have been established, definitions of the Frobenius and
pushforward properties, as well as the equivalence between them, follow
readily.

We will now consider components (1)–(3) of lifting, base change, and slicing
in some detail in Sections 2.3, 2.4, and 2.5, respectively. We conclude with
the Frobenius equivalence for weak factorisation systems in Section 2.6.

###  2.3. Lifting

As mentioned in Section 2.1, we write $f\pitchfork g$ for
$f,g\in{\mathcal{C}}_{1}$ when every lifting problem $(u,v):f\to g$ has a
diagonal filler $\phi$ as in (2.1). We extend this notation to subclasses
$J,K\subseteq{\mathcal{C}}_{1}$, by writing $J\pitchfork K$ when $f\pitchfork
g$ for every $f\in J$ and $g\in K$; for singletons we omit brackets. We
define, as before, ${{}^{\pitchfork}}J=\\{f\in{\mathcal{C}}_{1}\mid
f\pitchfork J\\}$ and $J{{}^{\pitchfork}}=\\{f\in{\mathcal{C}}_{1}\mid
J\pitchfork f\\}$. Let $\mathbf{P}({\mathcal{C}}_{1})$ denote the poset
category of subclasses of ${\mathcal{C}}_{1}$ ordered by the inclusion
relation, then ${{}^{\pitchfork}}(-)$ and $(-){{}^{\pitchfork}}$ give a
_Galois connection_ :

(2.2)
${{(\mathbf{P}({\mathcal{C}}_{1}))^{\text{op}}}}$${{\mathbf{P}({\mathcal{C}}_{1})\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{{{}^{\pitchfork}}(-)}$$\scriptstyle{(-){{}^{\pitchfork}}}$$\scriptstyle{\dashv}$

In this notation we have a string of equivalences:

(2.3) $\displaystyle J\subseteq{{}^{\pitchfork}}K$ iff $\displaystyle
J\pitchfork K$ iff $\displaystyle K\subseteq J{{}^{\pitchfork}}.$

We are particularly interested in cases where the inclusions of (2.3) are
equalities.

######  Definition 9.

A pair $(J,K)$ of subclasses $J,K\subseteq{\mathcal{C}}_{1}$ is called a
_lifting pair_ if $J\pitchfork K$. A lifting pair $(J,K)$ is called _closed_
if the induced inclusions of (2.3) hold both ways, so that
$J={{}^{\pitchfork}}K$ and $K=J{{}^{\pitchfork}}$.

######  Remark 10.

In [15, Definition 1.1.3] a lifting pair is defined as what we call a closed
lifting pair in Definition 9. We make this further distinction to align
terminology with [2], cf. Definition 35.

######  Example 11.

We remark, as in [2, Examples 5 & 6], that any subclass
$J\subseteq{\mathcal{C}}_{1}$ induces two canonical lifting pairs
$({{}^{\pitchfork}}J,J)$ and $(J,J{{}^{\pitchfork}})$, because from (2.3) we
get:

$\displaystyle{{}^{\pitchfork}}J$ $\displaystyle\subseteq{{}^{\pitchfork}}J$
iff $\displaystyle{{}^{\pitchfork}}J$ $\displaystyle\pitchfork J$ iff
$\displaystyle J$
$\displaystyle\subseteq({{}^{\pitchfork}}J){{}^{\pitchfork}},\text{ and}$
$\displaystyle J$
$\displaystyle\subseteq{{}^{\pitchfork}}(J{{}^{\pitchfork}})$ iff
$\displaystyle J$ $\displaystyle\pitchfork J{{}^{\pitchfork}}$ iff
$\displaystyle J{{}^{\pitchfork}}$ $\displaystyle\subseteq
J{{}^{\pitchfork}}.$

The inclusions $J\subseteq({{}^{\pitchfork}}J){{}^{\pitchfork}}$ and
$J\subseteq{{}^{\pitchfork}}(J{{}^{\pitchfork}})$ correspond to the unit and
counit of (2.2). The lifting pairs
$({{}^{\pitchfork}}J,({{}^{\pitchfork}}J){{}^{\pitchfork}})$ and
$({{}^{\pitchfork}}(J{{}^{\pitchfork}}),J{{}^{\pitchfork}})$ so obtained are
called _fibrantly generated_ and _cofibrantly generated_ by $J$, respectively.
In fact, since (2.2) is a Galois connection, these fibrantly and cofibrantly
generated pairs are always closed.

###  2.4. Base change

The notion of lifting pair can be generalized relative to adjunctions of
categories. This is because for $J\subseteq{\mathcal{C}}_{1}$ and
$K\subseteq{\mathcal{D}}_{1}$, with an adjunction $F\vdash G$ between two
categories ${\mathcal{C}}$ and ${\mathcal{D}}$, we have the following string
of equivalences:

(2.4) $\displaystyle F(J)\subseteq{{}^{\pitchfork}}K$ iff $\displaystyle
F(J)\pitchfork K$ iff $\displaystyle J\pitchfork G(K)$ iff $\displaystyle
G(K)\subseteq J{{}^{\pitchfork}}.$

######  Proposition 12.

Let $F\dashv G:{\mathcal{D}}\to{\mathcal{C}}$ be an adjunction, and
$J\subseteq{\mathcal{C}}_{1}$, $K\subseteq{\mathcal{D}}_{1}$ classes of maps
in ${\mathcal{C}}$ and ${\mathcal{D}}$ respectively; then
$F(J)\subseteq{{}^{\pitchfork}}K$ if and only if $G(K)\subseteq
J{{}^{\pitchfork}}$.

###### Proof.

We only prove left to right; the other direction is dual. To show $Gk\in
J{{}^{\pitchfork}}$ for $k:A\to B\in K$ we consider $j:C\to D\in J$ and
$(u,v):j\to Gk$ as on the left of:

${C}$${GA}$${FC}$${A}$${D}$${{GB\hbox to0.0pt{ ,\hss}}}$${FD}$${{B\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{Gk}$$\scriptstyle{j}$$\scriptstyle{u}$$\scriptstyle{Fj}$$\scriptstyle{k}$$\scriptstyle{\bar{u}}$$\scriptstyle{\bar{v}}$$\scriptstyle{\phi}$$\scriptstyle{v}$$\scriptstyle{\bar{\phi}}$

Transposing gives a lifting problem $(\bar{u},\bar{v})$ for $Fj$ and $k$ which
has a solution $\phi$ by the assumption $F(J)\subseteq{{}^{\pitchfork}}K$, and
its transpose $\smash{\bar{\phi}}$ is a solution to $(u,v)$. ∎

In the context of closed lifting pairs Proposition 12 tells us that a left
adjoint preserves left maps if and only if its right adjoint preserves right
maps.

######  Corollary 13.

Let $F\dashv G:{\mathcal{D}}\to{\mathcal{C}}$, and $(J,K)$ and $(L,M)$ be
closed lifting pairs on ${\mathcal{C}}$ and ${\mathcal{D}}$ respectively, then
$F(J)\subseteq L$ if and only if $G(M)\subseteq K$.

###  2.5. Slicing

A large part of our work relates to slicing. Recall that if ${\mathcal{C}}$ is
a category and $A$ an object in ${\mathcal{C}}$, then the _slice category_
${\mathcal{C}}/A$ is the category whose objects are maps $a:X\to A$ with
codomain $A$ and whose morphisms $(b:Y\to A)\to(a:X\to A)$ are maps $f:Y\to X$
in ${\mathcal{C}}$ making the triangle below commute:

${Y}$${{X}}$${{A\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{b}$$\scriptstyle{a}$

Note that $f$ (considered as a morphism in ${\mathcal{C}}$) does not uniquely
determine a morphism in ${\mathcal{C}}/A$, as there could be other arrows
besides $a$ in ${\mathcal{C}}(X,A)$. On the other hand, the domain $b$ of $f$
(considered as a morphism in ${\mathcal{C}}/A$) can be inferred from the data
$f$ and $a$. This means an arrow in ${\mathcal{C}}/A$ is equivalently a pair
$(f,a)$ of composable morphisms such that $\operatorname{cod}a=A$, and we will
henceforth refer to them using this notation. In this setting we say $a$ is an
_extension_ of $f$ to $A$. Two morphisms $(f,a)$ and $(g,b)$ in
${\mathcal{C}}/A$ are composable when $a=b.g$, and their composition is given
by $(g.f,b)$.

Next, we extend the slicing operation on categories to one on classes of maps.

######  Definition 14.

Given a subclass $J\subseteq{\mathcal{C}}_{1}$ and an object
$A\in{\mathcal{C}}$ we define the _slice_ subclass
$J/A\subseteq({\mathcal{C}}/A)_{1}$ by
$J/A=\\{(f,a)\in({\mathcal{C}}/A)_{1}\mid f\in J\\}$.

The goal will now be to prove the following proposition, which uses the above
notion of slicing to create new closed lifting pairs from old.

######  Proposition 15.

If $(J,K)$ is a closed lifting pair on ${\mathcal{C}}$, and
$A\in{\mathcal{C}}$ is some object, then $(J/A,K/A)$ is a closed lifting pair
on ${\mathcal{C}}/A$.

We start by considering how lifting works in a slice category. A lifting
problem for morphisms $(f,a)$ and $(g,b)$ in ${\mathcal{C}}/A$ is a square
$((u,c),(v,d)):(f,a)\to(g,b)$, as in:

(2.5) ${{a.f}}$${{b.g}}$${\bullet}$${\bullet}$${a}$${{b\hbox to0.0pt{
,\hss}}}$${\bullet}$${\bullet}$${{A\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{\phi}$$\scriptstyle{a}$$\scriptstyle{b}$$\scriptstyle{(f,a)}$$\scriptstyle{(g,b)}$$\scriptstyle{(u,c)}$$\scriptstyle{(v,d)}$$\scriptstyle{(\phi,e)}$

This boils down to a lifting problem $(u,v):f\to g$ for $f$ and $g$ such that
the induced triangle over the extensions to $A$ commutes, as illustrated on
the right above. Moreover, a lifting solution $(\phi,e)$ to the problem
$((u,c),(v,d))$ is just a solution $\phi$ to the problem $(u,v)$, as $e$
necessarily equals $b.g$. In other words, lifting in ${\mathcal{C}}/A$ is very
similar to lifting in ${\mathcal{C}}$, with the difference being that in
${\mathcal{C}}/A$ a restricted set of lifting problems is considered—namely
those commuting with the extensions to $A$.

######  Lemma 16.

Let $(f,a),(g,b)\in({\mathcal{C}}/A)_{1}$ for $A\in{\mathcal{C}}$, then
$f\pitchfork g$ implies $(f,a)\pitchfork(g,b)$.

###### Proof.

A lifting problem $((u,c),(v,d))$ for $(f,a)$ and $(g,b)$ as on the left of
(2.5) yields a problem $(u,v)$ for $f$ and $g$ as on the right of (2.5), which
has a solution $\phi$ by assumption; now $(\phi,b.g)$ is a solution to
$((u,c),(v,d))$. ∎

######  Lemma 17.

Let $J,K\subseteq{\mathcal{C}}_{1}$ and $A\in{\mathcal{C}}$, then $J\pitchfork
K$ implies $J/A\pitchfork K/A$.

###### Proof.

Let $(f,a)\in J/A,(g,b)\in K/A$, then $f\in J$ and $g\in K$ so $f\pitchfork g$
by assumption, and so $(f,a)\pitchfork(g,b)$ by Lemma 16. ∎

Lemma 17 tells us the slicing operation on subclasses of maps preserves
lifting pairs. To see that it also preserves closed lifting pairs we appeal to
a more general statement about commutativity between slicing and lifting. The
first step towards proving commutativity of lifting is taken by the following
consequence of Lemma 17.

######  Lemma 18.

Let $J\subseteq{\mathcal{C}}_{1}$ and $A\in{\mathcal{C}}$, then
$(J{{}^{\pitchfork}})/A\subseteq(J/A){{}^{\pitchfork}}$ and
$({{}^{\pitchfork}}J)/A\subseteq{{}^{\pitchfork}}(J/A)$.

###### Proof.

By applying Lemma 17 to the canonical lifting pairs $({{}^{\pitchfork}}J,J)$
and $(J,J{{}^{\pitchfork}})$ we get $({{}^{\pitchfork}}J)/A\pitchfork J/A$ and
$J/A\pitchfork(J{{}^{\pitchfork}})/A$, which is equivalent to the desired
inclusions. ∎

Only one of the converse inclusions of Lemma 18 holds in general.

######  Lemma 19.

Let $J\subseteq{\mathcal{C}}_{1}$ and $A\in{\mathcal{C}}$, then
$(J/A){{}^{\pitchfork}}\subseteq(J{{}^{\pitchfork}})/A$.

###### Proof.

Let $(f,a)\in(J/A){{}^{\pitchfork}}$, to show $f\in J{{}^{\pitchfork}}$ we
consider $(u,v):j\to f$ for $j\in J$, as in:

${\bullet}$${\bullet}$${{a.v.j}}$${{a.f}}$${\bullet}$${{\bullet}}$${{a.v}}$${{a\hbox
to0.0pt{ .\hss}}}$${{A\hbox to0.0pt{
,\hss}}}$$\scriptstyle{j}$$\scriptstyle{f}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{\phi}$$\scriptstyle{a.v}$$\scriptstyle{a}$$\scriptstyle{(j,a.v)}$$\scriptstyle{(f,a)}$$\scriptstyle{(u,a.f)}$$\scriptstyle{(v,a)}$$\scriptstyle{(\phi,a.f)}$

Now $(j,a.v)\in J/A$, and we have a commuting square
$((u,a.f),(v,a)):(j,a.v)\to(f,a)$ in ${\mathcal{C}}/A$ which has a solution
$(\phi,a.f)$; and $\phi$ is a solution to the square $(u,v)$. ∎

######  Corollary 20.

Let $J\subseteq C_{1}$, then $(J/A){{}^{\pitchfork}}=(J{{}^{\pitchfork}})/A$.

The trick in the proof of Lemma 19 is to make an extension for $j$ by
precomposing the extension of $f$ with the lower half of the lifting problem.
This does not work when we try to prove the remaining inclusion
${{}^{\pitchfork}}(J/A)\subseteq({{}^{\pitchfork}}J)/A$, which involves a
square $(u,v):f\to j$ in which the positions of $f$ and $j$ are swapped. To
work around this, we place an additional requirement on $J$.

######  Lemma 21.

Let $J\subseteq{\mathcal{C}}_{1}$ be closed under pullbacks and
$A\in{\mathcal{C}}$, then
${{}^{\pitchfork}}(J/A)\subseteq({{}^{\pitchfork}}J)/A$.

###### Proof.

Let $(f,a)\in{{}^{\pitchfork}}(J/A)$, to show $f\in J{{}^{\pitchfork}}$ we
consider $(u,v):f\to j$ for $j\in J$, as in:

${\bullet}$${\bullet}$${\bullet}$${{a.f}}$${{a.v^{*}j}}$${\bullet}$${\bullet}$${{\bullet\hbox
to0.0pt{ ,\hss}}}$${a}$${{a\hbox to0.0pt{ .\hss}}}$${A}$
$\scriptstyle{f}$$\scriptstyle{j}$$\scriptstyle{u}$$\scriptstyle{a}$$\scriptstyle{(f,a)}$$\scriptstyle{(v^{*}j,a)}$$\scriptstyle{(\alpha,a.v^{*}j)}$$\scriptstyle{(1,a)}$$\scriptstyle{(\phi,a.v^{*}j)}$$\scriptstyle{v}$$\scriptstyle{1}$$\scriptstyle{a}$$\scriptstyle{\phi}$$\scriptstyle{\alpha}$$\scriptstyle{\varepsilon_{v}}$$\scriptstyle{v^{*}j}$$\scriptstyle{\lrcorner}$

By assumption $v^{*}j\in J$ and so $(v^{*}j,a)\in J/A$. The morphism
$\alpha:\operatorname{dom}f\to\operatorname{dom}v^{*}j$ induced by $v^{*}j$
gives rise to a lifting problem $((\alpha,a.v^{*}j),(1,a)):(f,a)\to(v^{*}j,a)$
in ${\mathcal{C}}/A$, which has a solution $(\phi,a.v^{*}j)$; and
$\varepsilon_{v}.\phi$ is a solution to $(u,v)$. ∎

This additional assumption on $J$ is satisfied in the case we are interested
in.

######  Lemma 22.

For $J\subseteq{\mathcal{C}}_{1}$ the class $J{{}^{\pitchfork}}$ is closed
under pullbacks.

###### Proof.

Let $f\in J{{}^{\pitchfork}}$ and $(u,v):g\to f$ be a pullback. To show $g\in
J{{}^{\pitchfork}}$ we consider a lifting problem $(w,x):j\to g$ for $j\in J$:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet\hbox to0.0pt{
.\hss}}$$\scriptstyle{j}$$\scriptstyle{g}$$\scriptstyle{f}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{\lrcorner}$$\scriptstyle{w}$$\scriptstyle{x}$$\scriptstyle{\phi}$$\scriptstyle{\alpha}$

By assumption the outer rectangle $(u.w,v.x)$ has a solution $\phi$, by which
the pullback induces a morphism $\alpha$ that solves $(w,x)$. ∎

######  Corollary 23.

Let $J,K\subseteq{\mathcal{C}}_{1}$ with $K=J{{}^{\pitchfork}}$, then
${{}^{\pitchfork}}(K/A)=({{}^{\pitchfork}}K)/A$.

We are now ready to prove that slicing preserves closed lifting pairs.

###### Proof of Proposition 15.

Let $(J,K)$ be a closed lifting pair on ${\mathcal{C}}$; we want to show that
$(J/A,K/A)$ is a closed lifting pair on ${\mathcal{C}}/A$. By Corollaries 20
and 23 we have:

$(J/A){{}^{\pitchfork}}=(J{{}^{\pitchfork}})/A=K/A,\quad\text{and}\quad{{}^{\pitchfork}}(K/A)=({{}^{\pitchfork}}K)/A=J/A.\qed$

###  2.6. Frobenius equivalence

In a locally cartesian closed category ${\mathcal{C}}$, any morphism $f:A\to
B$ induces an adjunction $f^{*}\dashv f_{*}:{\mathcal{C}}/A\to{\mathcal{C}}/B$
of pullback and pushforward along $f$. The action of the pullback functor
$f^{*}$ on an object $g$ in ${\mathcal{C}}/B$ is depicted on the left diagram
below:

(2.6)
${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${A}$${{B\hbox
to0.0pt{ ,\hss}}}$${A}$${{B\hbox to0.0pt{
.\hss}}}$$\scriptstyle{b}$$\scriptstyle{g}$$\scriptstyle{f}$$\scriptstyle{f^{*}b}$$\scriptstyle{f^{*}(b.g)}$$\scriptstyle{f^{*}g}$$\scriptstyle{g}$$\scriptstyle{f^{*}g}$$\scriptstyle{f}$$\scriptstyle{\lrcorner}$

The action of $f^{*}$ on an arrow $(g,b)$ in ${\mathcal{C}}/B$ is depicted on
the right above; it is defined as the morphism induced by the pullback
$f^{*}b$ from the pullback $f^{*}(b.g)$ of the composition $b.g$. In this case
we (abusively) write $f^{*}g$ for the first component of the resulting
morphism in ${\mathcal{C}}/A$, so $f^{*}(g,b)=(f^{*}g,f^{*}b)$.

######  Definition 24.

A morphism $f:A\to B\in{\mathcal{C}}_{1}$ has the _Frobenius property_ with
respect to a pair $(J,K)$ of subclasses $J,K\subseteq{\mathcal{C}}_{1}$ if
$f^{*}(J/B)\subseteq J/A$, and the _pushforward property_ if
$f_{*}(K/A)\subseteq K/B$.

######  Theorem 25.

A morphism $f:A\to B$ in ${\mathcal{C}}$ has the Frobenius property with
respect to a closed lifting pair $(J,K)$ if and only if it has the pushforward
property.

###### Proof.

By Propositions 12 and 15 we have:

$\displaystyle f^{*}(J/B)\subseteq J/A$ $\displaystyle\text{ iff
}f^{*}(J/B)\subseteq{{}^{\pitchfork}}(K/A)$ $\displaystyle\text{ iff
}f_{*}(K/A)\subseteq\smash{(J/B){{}^{\pitchfork}}}$ $\displaystyle\text{ iff
}f_{*}(K/A)\subseteq K/B.\qed$

The definition of the Frobenius property we give in Definition 24 differs from
how it is usually phrased for wfs (Definition 3 above), in two ways. Firstly,
Definition 3 requires the _object_ component of the pullback functor $f^{*}$
to preserve left maps, while in Definition 24 it is the _arrow_ component of
$f^{*}$ which is required to do so. This is illustrated in (2.6)—both versions
of the Frobenius property require that $g\in L$ implies $f^{*}g\in L$, but
Definition 3 is phrased with respect to the left diagram of (2.6) and
Definition 24 with respect to the right diagram. The latter is slightly
stronger.

######  Proposition 26.

Let $(J,K)$ be classes of morphisms in ${\mathcal{C}}$ which are closed under
isomorphisms, and $f$ a map in ${\mathcal{C}}$. If the arrow component of
$f^{*}$ preserves $J$ maps then so does its object component; the same
statement holds for $f_{*}$ w.r.t. $K$ maps.

###### Proof.

To avoid confusion we write $f^{*}$ for the action of the pullback functor
along $f$ on objects, and $f^{\star}$ for its action on arrows. Let $g:C\to B$
be a $J$ map, we want to show that $f^{*}g\in J$. Note that $g$ can be
considered a morphism $(g,1_{A})$ in ${\mathcal{C}}/B$, and so $f^{\star}g\in
J$. Therefore, we have $f^{*}g\in J$ from $(1,f^{*}1):f^{\star}g\cong f^{*}g$:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${A}$${{B\hbox to0.0pt{
.\hss}}}$$\scriptstyle{1}$$\scriptstyle{f^{*}1}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{f^{\star}g}$$\scriptstyle{f^{*}g}$

The argument for the pushforward functor $f_{*}$ is analogous. ∎

The converse implications do not hold in general for an individual morphism
$f$. To obtain something of a converse we should make the statement for a
class of morphisms $K$ which is closed under pullbacks.

######  Proposition 27.

Let $(J,K)$ be closed under isomorphisms, $K$ closed under pullbacks, and $f$
a map in $K$. If the object component of $f^{*}$ preserves $J$ maps then so
does its arrow component. Furthermore, if the object components of all
pushforward functors of $K$ maps preserve $K$ maps, then the arrow component
of $f_{*}$ preserves $K$ maps.

###### Proof.

Let $f:A\to B$ be a $K$ map, and $(g,b)\in{\mathcal{C}}/B$. Writing
$\varepsilon$ for the counit of $f_{!}\dashv f^{*}$, we have that
$\varepsilon_{b}\in K$ by assumption, and so $\varepsilon_{b}^{*}g\cong
f^{*}g\in K$; as on the left of:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${A}$${{B\hbox
to0.0pt{ ,\hss}}}$${A}$${{B\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{b}$$\scriptstyle{g}$$\scriptstyle{f^{*}b}$$\scriptstyle{\varepsilon_{b}}$$\scriptstyle{\varepsilon_{b}^{*}g}$$\scriptstyle{f^{*}g}$$\scriptstyle{a}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{f_{*}a}$$\scriptstyle{f^{*}f_{*}a}$$\scriptstyle{\varepsilon_{f_{*}a}}$$\scriptstyle{\nu_{a}}$$\scriptstyle{\nu_{a}^{*}g}$$\scriptstyle{f_{*}g}$$\scriptstyle{h}$$\scriptstyle{\sim}$$\scriptstyle{\sim}$

Consider $(g,a)\in{\mathcal{C}}/A$, and let $\nu:f^{*}f_{*}\to 1$ denote the
counit of $f^{*}{\,\dashv\,}f_{*}$. As $K$ is closed under pullbacks, we have
that $\nu_{a}^{*}g$ and $\varepsilon_{f_{*}a}$ are both in $K$, and so
$(\varepsilon_{f_{*}a})_{*}\nu_{a}^{*}g=h\in K$. It can be shown that $h$ has
the universal property of $f_{*}g$, and so $h\cong f_{*}g\in K$. ∎

Despite the fact that under the assumptions of Proposition 27 the Frobenius
and pushforward properties for arrows can be reduced to those for objects, we
still regard the ones for arrows as being the most fundamental. Indeed, the
versions for arrows are the ones that can most readily be generalised to the
case of categories and double categories of maps, as we will see in the
subsequent sections.

Proposition 27 brings us to a second difference between Definitions 3 and 24,
which is that in the former both the pullback and pushforward is performed
along a $K$ map, whereas the latter is phrased with respect to an arbitrary
morhpism in the ambient category. There are two reasons why Definition 3 is
phrased this way. Firstly, as Proposition 27 suggests, it is necessary for
obtaining Proposition 4 (as the right class of a wfs is always closed under
pullbacks). The second reason relates to type theory; we want to interpret
dependent types as right maps of a wfs, and the dependent product as
pushforward, so that $R$ should be closed under pushforward. For this reason,
we adapt Definition 24 of the Frobenius property to pairs of classes of maps.

######  Definition 28.

A pair $(J,K)$ of subclasses $J,K\subseteq{\mathcal{C}}_{1}$ satisfies the
_Frobenius property_ if every $f\in K$ does, and likewise the _pushforward
property_ when every $f\in K$ does.

##  3\. The Frobenius equivalence for categories of maps

In this section we move from classes of maps to _categories_ of maps and show
that the results from the previous section can be generalised to this setting.
This generalisation stems from Garner’s paper on understanding the small
object argument [7] and the extension of the Frobenius equivalence to this
setting can be found in [6]. We give a different account of the Frobenius
equivalence here, which shows that it can be derived rather cleanly from the
work of Bourke and Garner in [3], provided we follow the outline we sketched
in Subsection 2.2 and take the “arrow view” instead of the “object view”, as
discussed in Subsection 2.6; moreover, the extension of the Frobenius
equivalence to algebraic weak factorisation systems that we will see in later
sections builds on this particular way of developing the Frobenius equivalence
for categories of maps.

In what follows we will write $\mathbf{Ar}({\mathcal{C}})$ for the _arrow
category_ of a category ${\mathcal{C}}$, that is, the category whose objects
are the arrows of ${\mathcal{C}}$ and whose morphisms are commutative squares
in ${\mathcal{C}}$. Note that $\mathbf{Ar}$ can be considered as a functor
${\bf Cat}\to{\bf Cat}$, and there are natural transformations
$\operatorname{dom},\operatorname{cod}:\mathbf{Ar}\Rightarrow 1_{\bf Cat}$.

We formalise the idea of a category of maps as a functor
$\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$: indeed, we think of $\mathcal{J}$
as consisting of a category of _structured_ morphisms in ${\mathcal{C}}$ and
structure-preserving maps between those. The following examples illustrate
this.

######  Example 29.

Recall that a mono $i$ in a category ${\mathcal{C}}$ is _split_ if it has a
retraction. One option would be to regard the split monos just as a class of
maps, as in the previous section. However, we can also regard the splitting as
additional structure, so that we are interested in pairs $(i,r)$ where $r$ is
a retraction of $i$. Split monos can then be given categorical structure by
defining a morphism between split monomorphisms $(i,r)$,
$(i^{\prime},r^{\prime})$ as a serially commuting square of functors $(u,v)$:

${\bullet}$${\bullet}$${\bullet}$${{\bullet\hbox to0.0pt{
.\hss}}}$$\scriptstyle{i}$$\scriptstyle{i^{\prime}}$$\scriptstyle{r}$$\scriptstyle{r^{\prime}}$$\scriptstyle{u}$$\scriptstyle{v}$

We denote the category of split monos defined in this manner by
$\mathbf{SplMono}$, and we have a (faithful) forgetful functor
$\mathbf{SplMono}\to\mathbf{Ar}({\mathcal{C}})$ sending the pair $(i,r)$ to
$i$.

######  Example 30.

As a special case of the previous example, consider the case where
${\mathcal{C}}={\bf Cat}$ and the split mono $(i,r)$ is a _split reflection_
in that $r\vdash i$ with identity counit (split reflections are better known
as right adjoint right inverses or _rari_ , for short); see [3, Section 4.2].
We can then define $\mathbf{SplRef}$ as a full subcategory of
$\mathbf{SplMono}$ containing the raris in ${\bf Cat}$, and we obtain a
functor $\mathbf{SplRef}\to\mathbf{Ar}({\bf Cat})$. Note that a morphism in
$\mathbf{SplMono}$ between split reflections is guaranteed to commute with the
units of the adjunctions; the reader is referred to [3, Section 4.2] for more
details.

######  Example 31.

A Grothendieck fibration is called split if it comes equipped with an explicit
choice of cartesian lifts which preserves identities and compositions. A
morphism of split fibrations $P$, $Q$ is defined as a commutative square
$(U,V):P\to Q$ in ${\bf Cat}$ that also commutes with the splitting. By this
we mean that if $\underline{f}$ is the chosen lift of $f:b\to Pa$ in
$\operatorname{cod}P$ and $\underline{Vf}$ the chosen lift of $Vf:Vb\to VPa$
in $\operatorname{cod}Q$, then we have
$\smash{U\underline{f}=\underline{Vf}}$. This yields a category
$\mathbf{SplFib}$ together with a (faithful) forgetful functor
$\mathbf{SplFib}\to\mathbf{Ar}({\bf Cat})$. The same definition applies to
split opfibrations, so that we also have a forgetful functor
$\mathbf{SplOpFib}\to\mathbf{Ar}({\bf Cat})$.

Before we proceed, we make some remarks on notation. In this setting, and in
the double categorical setting that follows, we will use the name of the
domain $\mathcal{J}$ of a morphism $\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$
to refer both to the domain and the morphism, rather than naming the morphism
separately. Furthermore, following [3, 2], given such a functor
$\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$ we use bold type to denote an
element $\mathbf{f}\in J$, and italic type for the corresponding image $f$ of
$\mathbf{f}$ under $\mathcal{J}$. Moreover, we use double letters for
morphisms in $\mathcal{J}$: that is, if $\mathbf{f}$ and $\mathbf{g}$ are
objects in $\mathcal{J}$, then a map $\mathbf{f}\to\mathbf{g}$ will usually be
written uv and the image of this map under $\mathcal{J}$ will be $(u,v):f\to
g$.

###  3.1. Lifting

Lifting for categories of maps is defined as a more structured version of
(2.1), demanding a specific and coherent choice of lifts.

######  Definition 32.

Let $\mathcal{J},\mathcal{K}\to\mathbf{Ar}({\mathcal{C}})$; a
$(\mathcal{J},\mathcal{K})$-_lifting operation_ $\phi$ assigns to each
$\mathbf{f}\in\mathcal{J}$, $\mathbf{g}\in\mathcal{K}$, and lifting problem
$(u,v):f\to g$, a solution $\phi_{\mathbf{f},\mathbf{g}}(u,v)$:

(3.1) ${\bullet}$${\bullet}$${\bullet}$${{\bullet\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{\phi_{\mathbf{f},\mathbf{g}}(u,v)}$

This choice is required to respect morphisms of $\mathcal{J}$ and
$\mathcal{K}$, in the sense that if
$\textbf{wx}:\mathbf{f}^{\prime}\to\mathbf{f}$ in $\mathcal{J}$, $(u,v):f\to
g$, and $\textbf{yz}:\mathbf{g}\to\mathbf{g}^{\prime}$ in $\mathcal{K}$, then
$y.\phi_{\mathbf{f},\mathbf{g}}(u,v).x=\phi_{\mathbf{f}^{\prime},\mathbf{g}^{\prime}}(w.u.y,x.v.z)$:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${{=}}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${{\bullet\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{g}$$\scriptstyle{f}$$\scriptstyle{f^{\prime}}$$\scriptstyle{g^{\prime}}$$\scriptstyle{x}$$\scriptstyle{y}$$\scriptstyle{\smash{\phi_{\mathbf{f},\mathbf{g}}}}$$\scriptstyle{w}$$\scriptstyle{z}$$\scriptstyle{f^{\prime}}$$\scriptstyle{g^{\prime}}$$\scriptstyle{y.u.w}$$\scriptstyle{z.v.x}$$\scriptstyle{\smash{\phi_{\mathbf{f}^{\prime},\mathbf{g}^{\prime}}}}$

######  Remark 33.

Note that the lifting operation chooses the lift on the basis of $\mathbf{f}$
and $\mathbf{g}$ rather than $f$ and $g$. This means, for example, that if
$\mathcal{K}$ is the category $\mathbf{SplMono}$ of split monos, as in Example
29, the choice of lift may depend on the retraction.

The assignment
$(\mathcal{J},\mathcal{K})\mapsto\mathbf{Lift}(\mathcal{J},\mathcal{K})$ of
functors $\mathcal{J},\mathcal{K}$ to the class
$\mathbf{Lift}(\mathcal{J},\mathcal{K})$ of
$(\mathcal{J},\mathcal{K})$-lifting operations can be made the object part of
a functor

(3.2) $\mathbf{Lift}:({\bf
Cat}/\mathbf{Ar}({\mathcal{C}}))^{\mathrm{op}}\times({\bf
Cat}/\mathbf{Ar}({\mathcal{C}}))^{\mathrm{op}}\to{\bf Set}.$

A $(\mathcal{J},\mathcal{K})$-lifting operation is to functors
$\mathcal{J},\mathcal{K}\to\mathbf{Ar}({\mathcal{C}})$ what the statement
$J\pitchfork K$ is to subclasses $J,K\subseteq{\mathcal{C}}_{1}$. Further
extending this analogy, we have the following restriction of [3, Proposition
15] to the case of categories of maps.

######  Proposition 34.

$\mathbf{Lift}$ is representable in both arguments, inducing an adjunction:

(3.3) ${{({\bf Cat}/\mathbf{Ar}({\mathcal{C}}))^{\mathrm{op}}}}$${{{\bf
Cat}/\mathbf{Ar}({\mathcal{C}})\hbox to0.0pt{
.\hss}}}$$\scriptstyle{{{}^{\pitchfork}}(-)}$$\scriptstyle{(-){{}^{\pitchfork}}}$$\scriptstyle{\dashv}$

###### Proof.

The representing object of $\mathbf{Lift}(-,\mathcal{J})$ is a category
${{}^{\pitchfork}}\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$ of which the
objects are pairs $(f,\phi_{f-})$ with
$\phi_{f-}\in\mathbf{Lift}(f,\mathcal{J})$ (where we consider $f$ to be a
functor $f:1\to\mathbf{Ar}({\mathcal{C}})$), and in which a morphism
$(f,\phi_{f-})\to(g,\phi_{g-})$ is a square $(u,v):f\to g$ which commutes with
the lifting operations. This means that for $\mathbf{j}\in\mathcal{J}$ and
$(w,x):g\to j$ we have
$\phi_{f,\mathbf{j}}(w.u,x.v)=\phi_{g,\mathbf{j}}(w,x).v$:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${{=}}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${{\bullet\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{j}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{w}$$\scriptstyle{x}$$\scriptstyle{f}$$\scriptstyle{j}$$\scriptstyle{w.u}$$\scriptstyle{x.v}$$\scriptstyle{\smash{\phi_{g,\mathbf{j}}}}$$\scriptstyle{\smash{\phi_{f,\mathbf{j}}}}$

The representing object
$\mathcal{J}{{}^{\pitchfork}}\to\mathbf{Ar}({\mathcal{C}})$ of
$\mathbf{Lift}(\mathcal{J},-)$ is defined analogously. ∎

Birepresentability of (3.2) gives us the following analog of (2.3):

(3.4) ${\bf
Cat}/\mathbf{Ar}(C)(\mathcal{J},{{}^{\pitchfork}}\mathcal{K})\cong\mathbf{Lift}(\mathcal{J},\mathcal{K})\cong{\bf
Cat}/\mathbf{Ar}({\mathcal{C}})(\mathcal{K},\mathcal{J}{{}^{\pitchfork}}).$

In turn, this gives an analog of Definition 9 of (closed) lifting pairs.
However, since this is no longer a property but additional structure—in the
form of a $(\mathcal{J},\mathcal{K})$-lifting operation $\phi$—we will now
speak of _lifting structures_ , following terminology of [2].

######  Definition 35.

A triple $(\mathcal{J},\phi,\mathcal{K})$ of functors
$\mathcal{J},\mathcal{K}\to\mathbf{Ar}({\mathcal{C}})$ and a
$(\mathcal{J},\mathcal{K})$-lifting operation $\phi$ is called a _lifting
structure_. A lifting structure $(\mathcal{J},\phi,\mathcal{K})$ is called
_closed_ when the functors
$\phi_{l}:\mathcal{J}\to{{}^{\pitchfork}}\mathcal{K}$ and
$\phi_{r}:\mathcal{K}\to\mathcal{J}{{}^{\pitchfork}}$ induced by (3.4) are
invertible.

######  Example 36.

Let $\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$; applying (3.4) to the
identities on ${{}^{\pitchfork}}\mathcal{J}$ and
$\mathcal{J}{{}^{\pitchfork}}$ yields lifting operations
$\lambda\in\mathbf{Lift}({{}^{\pitchfork}}\mathcal{J},\mathcal{J})$ and
$\rho\in\mathbf{Lift}(\mathcal{J},\mathcal{J}{{}^{\pitchfork}})$, and so we
get, as we did in Example 11, two canonical lifting structures
$({{}^{\pitchfork}}\mathcal{J},\lambda,\mathcal{J})$ and
$(\mathcal{J},\rho,\mathcal{J}{{}^{\pitchfork}})$. Again, this yields lifting
structures
$({{}^{\pitchfork}}\mathcal{J},\rho,({{}^{\pitchfork}}\mathcal{J}){{}^{\pitchfork}})$
and
$({{}^{\pitchfork}}(\mathcal{J}{{}^{\pitchfork}}),\lambda,\mathcal{J}{{}^{\pitchfork}})$
which are said to be fibrantly generated and cofibrantly generated by
$\mathcal{J}$. Whether these are closed in general seems to be an open
question; see [2, Remark 10].

######  Example 37.

The functors $\mathbf{SplRef}\to\mathbf{Ar}({\bf Cat})$ and
$\mathbf{SplFib}\to\mathbf{Ar}({\bf Cat})$ form part of a lifting structure.
Indeed, suppose

${{\mathcal{C}}}$${{\mathcal{A}}}$${{\mathcal{D}}}$${{\mathcal{B}}}$$\scriptstyle{R}$$\scriptstyle{X}$$\scriptstyle{P}$$\scriptstyle{Y}$$\scriptstyle{\phi}$

is a commutative diagram of categories in which $P$ is a split fibration and
$R$ is a split reflection with left adjoint $L{\,\dashv\,}R$ and unit
$\theta:1\to R.L$. If $d$ is an object in $\mathcal{D}$, then we can consider
the image of the unit $\theta_{d}:d\to RLd$ under $Y$. Since $YRLd=PXLd$ and
$P$ is split fibration, we find a cartesian lift of $P\theta_{d}$ as in

(3.5) ${\phi(d)}$${XLd}$${Yd}$${{YRLd\hbox to0.0pt{
,\hss}}}$$\scriptstyle{P\theta_{d}}$$\scriptstyle{\underline{P\theta_{d}}}$

whose domain we define to be $\phi(d)$. This definition of $\phi$ can be
extended to morphisms $d\to d^{\prime}$ using that
$\underline{P\theta_{d^{\prime}}}$ is cartesian. Then, $P.\phi=Y$ by
construction, while $\phi.R=X$ follows from $\theta_{Rc}=1_{Rc}$ and the fact
that the splitting of $P$ lifts identities to identities. It is readily
verified that this way of constructing the lift $\phi$ respects the morphisms
in both $\mathbf{SplRef}$ and $\mathbf{SplFib}$; for more details, the reader
is referred to [2, Examples 4 (ii)]. Note that this lifting structure is not
closed, as can be seen from the fact that split fibration are not closed under
retracts.

###  3.2. Base change

As with classes of maps, lifting structures can be phrased relative to
adjunctions of categories. Following the approach in [3, Section 6.4], we do
so by extending the adjunction (3.3). Let ${\bf Cat}_{\text{ladj}}$ denote the
category of small categories with fully specified adjunctions between them,
pointing in the direction of the left adjoint; ${\bf Cat}_{\text{radj}}$ is
defined dually, i.e. ${\bf Cat}_{\text{radj}}={\bf
Cat}_{\text{ladj}}^{\mathrm{op}}$. These come with functors ${\bf
Cat}_{\mathrm{ladj}},{\bf Cat}_{\mathrm{radj}}\to{\bf Cat}$ forgetting the
right and left adjoints, respectively. We now define ${\bf
Cat}/\mathbf{Ar}(-_{\mathrm{ladj}})$ by the following pullback:

${{\bf Cat}/\mathbf{Ar}(-_{\mathrm{ladj}})}$${{{\bf
Cat}_{\mathrm{ladj}}}}$${{\mathbf{Ar}({\bf Cat})}}$${{{\bf Cat}\hbox to0.0pt{
.\hss}}}$$\scriptstyle{\operatorname{cod}}$$\scriptstyle{\lrcorner}$

The category ${\bf Cat}/\mathbf{Ar}(-_{\mathrm{radj}})$ is defined similarly,
using ${\bf Cat}_{\mathrm{radj}}\to{\bf Cat}$.

######  Proposition 38.

The adjunction of Proposition 34 extends to:

(3.6) ${{({\bf Cat}/\mathbf{Ar}(-_{\mathrm{ladj}}))^{\mathrm{op}}}}$${{{\bf
Cat}/\mathbf{Ar}(-_{\mathrm{radj}})\hbox to0.0pt{
.\hss}}}$$\scriptstyle{{{}^{\pitchfork}}(-)}$$\scriptstyle{(-){{}^{\pitchfork}}}$$\scriptstyle{\dashv}$

###### Proof.

The functors ${{}^{\pitchfork}}(-)$ and $(-){{}^{\pitchfork}}$ act as before
on objects, and on arrows by the construction in Proposition 12. See [3,
Proposition 21] for further details. ∎

The Frobenius equivalence relies essentially on the fact that (3.6) is an
adjunction, so it is worth stating this property separately; it is the
categorical analog of Proposition 12.

######  Corollary 39.

Let $F\dashv G:{\mathcal{D}}\to{\mathcal{C}}$ be an adjunction, and
$\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$,
$\mathcal{K}\to\mathbf{Ar}({\mathcal{D}})$ be functors; then there is a
bijection between lifts $\mathbf{F}$ and $\mathbf{G}$ as in the diagrams
below:

${\mathcal{J}}$${{{{}^{\pitchfork}}\mathcal{K}}}$${\mathcal{K}}$${{\mathcal{J}{{}^{\pitchfork}}}}$${{\mathbf{Ar}({\mathcal{C}})}}$${{\mathbf{Ar}({\mathcal{D}})\hbox
to0.0pt{
,\hss}}}$${{\mathbf{Ar}({\mathcal{D}})}}$${{\mathbf{Ar}({\mathcal{C}})\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{\mathbf{F}}$$\scriptstyle{\mathbf{Ar}(F)}$$\scriptstyle{\mathbf{G}}$$\scriptstyle{\mathbf{Ar}(G)}$

###  3.3. Slicing

We now proceed to define an analog of slicing for functors
$\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$.

######  Definition 40.

Given a functor $\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$ and an object
$A\in{\mathcal{C}}$ we define the _slice_ functor
$\mathcal{J}/A\to\mathbf{Ar}({\mathcal{C}}/A)$ as the pullback of
$\mathcal{J}$ along
$\mathbf{Ar}(\operatorname{dom}):\mathbf{Ar}({\mathcal{C}}/A)\to\mathbf{Ar}({\mathcal{C}})$:

${{\mathcal{J}/A}}$${\mathcal{J}}$${{\mathbf{Ar}({\mathcal{C}}/A)}}$${{\mathbf{Ar}({\mathcal{C}})\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{\mathbf{Ar}(\operatorname{dom})}$$\scriptstyle{\lrcorner}$

Here we denote by $\operatorname{dom}$ the forgetful functor
${\mathcal{C}}/A\to{\mathcal{C}}:a\mapsto\operatorname{dom}a$.

Spelling out the meaning of Definition 40, we find that an object of
$\mathcal{J}/A$ is equivalently a pair $(\mathbf{f},a)$ with
$\mathbf{f}\in\mathcal{J}$ and $(f,a)$ a morphism in ${\mathcal{C}}/A$. The
associated functor to $\mathbf{Ar}({\mathcal{C}}/A)$ forgets this
$\mathcal{J}$-structure, i.e.
$\mathcal{J}/A\to\mathbf{Ar}({\mathcal{C}}/A):(\mathbf{f},a)\mapsto(f,a)$.

The goal will now be to prove that this slicing operation preserves closed
lifting structures. We begin by adapting the construction of Lemma 16.

######  Proposition 41.

Let $(\mathcal{J},\phi,\mathcal{K})$ be a lifting structure on ${\mathcal{C}}$
and $A\in{\mathcal{C}}$ some object, then there is a lifting structure
$(\mathcal{J}/A,\phi/A,\mathcal{K}/A)$ on ${\mathcal{C}}/A$.

###### Proof.

We define the $(\mathcal{J}/A,\mathcal{K}/A)$-lifting operation $\phi/A$ by:

$\phi/A_{(\mathbf{f},a),(\mathbf{g},b)}((u,c),(v,d))=(\phi_{\mathbf{f},\mathbf{g}}(u,v),b.g).\qed$

######  Proposition 42.

If $(\mathcal{J},\phi,\mathcal{K})$ is a closed lifting structure then so is
$(\mathcal{J}/A,\phi/A,\mathcal{K}/A)$.

To prove Proposition 42, we use the strategy from Section 2.5 in showing that
the operations defined in Proposition 34 commute with the slicing operation,
which is to say that
$(\mathcal{J}{{}^{\pitchfork}})/A\cong(\mathcal{J}/A){{}^{\pitchfork}}$ and
$({{}^{\pitchfork}}\mathcal{J})/A\cong{{}^{\pitchfork}}(\mathcal{J}/A)$ as
functors over $\mathbf{Ar}({\mathcal{C}}/A)$. Again, only the first of these
isomorphisms exists in general. For the second desired isomorphism we do
always obtain a functor
$({{}^{\pitchfork}}\mathcal{J})/A\to{{}^{\pitchfork}}(\mathcal{J}/A)$, but for
its inverse to exist we require that $\mathcal{J}$, in some suitable sense, is
closed under pullbacks.

######  Proposition 43.

Given a functor $\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$ and an object
$A\in{\mathcal{C}}$ there are functors
$(\lambda/A)_{l}:({{}^{\pitchfork}}\mathcal{J})/A\to{{}^{\pitchfork}}(\mathcal{J}/A)$
and
$(\rho/A)_{r}:(\mathcal{J}{{}^{\pitchfork}})/A\to(\mathcal{J}/A){{}^{\pitchfork}}$.

###### Proof.

Apply Proposition 41 to the canonical lifting structures induced by
$\mathcal{J}$. ∎

######  Proposition 44.

The functor $(\rho/A)_{r}$ of Proposition 43 is an isomorphism.

###### Proof.

We make a functor
$(\mathcal{J}/A){{}^{\pitchfork}}\to\mathcal{J}{{}^{\pitchfork}}$ using the
construction in Lemma 19; given $(f,a)$ with a $(\mathcal{J}/A,(f,a))$-lifting
operation $\smash{\phi_{-(f,a)}}$ we define a $(\mathcal{J},f)$-lifting
operation $\theta_{-f}$ by
$\theta_{\mathbf{j},f}(u,v)=\phi_{(\mathbf{j},a.v),(f,a)}((u,a.f),(v,a))$. By
the universal property of $(\mathcal{J}{{}^{\pitchfork}})/A$ this induces the
desired inverse
$(\rho/A)_{r}^{-1}:(\mathcal{J}/A){{}^{\pitchfork}}\to(\mathcal{J}{{}^{\pitchfork}})/A$.
∎

######  Definition 45.

A functor $\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$ is a _comprehension
category_ if $\operatorname{cod}.\mathcal{J}$ is a Grothendieck fibration
making $\mathcal{J}$ into a cartesian functor:

${\mathcal{J}}$${\mathbf{Ar}({\mathcal{C}})}$${{\mathcal{C}}\hbox to0.0pt{
.\hss}}$$\scriptstyle{\mathcal{J}}$$\scriptstyle{\operatorname{cod}.\mathcal{J}}$$\scriptstyle{\operatorname{cod}}$

######  Proposition 46.

Let $\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$; then
$\mathcal{J}{{}^{\pitchfork}}\to\mathbf{Ar}({\mathcal{C}})$ is a comprehension
category.

###### Proof.

Assume we have maps $g:B\to A$ and $y:C\to A$ and $\phi_{-g}$ is a
$(\mathcal{J},g)$-lifting operation. Since $\mathcal{C}$ has pullbacks, there
is a pullback square $(x,y):g^{\prime}\to g$, inducing a
$(\mathcal{J},g^{\prime})$-lifting operation $\psi_{-g^{\prime}}$ for
$g^{\prime}$ by the construction of Lemma 22. Now
$(x,y):(g^{\prime},\psi_{g^{\prime}-})\to(g,\phi_{g-})$ is a cartesian
morphism in $\mathcal{J}{{}^{\pitchfork}}$. ∎

The following is [6, Proposition 5.4].

######  Proposition 47.

Let $\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$ be a comprehension category,
and $A\in{\mathcal{C}}$ be some object; then the functor $(\lambda/A)_{l}$ of
Proposition 43 is an isomorphism.

###### Proof.

Let $((g,a),\phi_{(g,a)-})\in{{}^{\pitchfork}}(\mathcal{J}/A)$ and consider
$\mathbf{f}\in\mathcal{J}$ with $(u,v):g\to f$. By assumption there is a
cartesian morphism $v^{*}\mathbf{f}\to\mathbf{f}\in\mathcal{J}$ over $v$ and a
pullback square $(v^{+},v):v^{*}f\to f$, and so a lift
$\phi_{(g,a),(v^{*}\mathbf{f},a)}(\alpha,1)$ of the induced morphism $\alpha$:

(3.7) ${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${{\bullet\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{g}$$\scriptstyle{f}$$\scriptstyle{1}$$\scriptstyle{v}$$\scriptstyle{v^{+}}$$\scriptstyle{v^{*}f}$$\scriptstyle{\alpha}$$\scriptstyle{\phi}$$\scriptstyle{\lrcorner}$

In other words, following the construction in Lemma 22, we define a
$(g,\mathcal{J})$-lifting operation $\psi_{g-}$ on $(u,v):g\to f$ for
$\mathbf{f}\in\mathcal{J}$ by

(3.8)
$\psi_{g,\mathbf{f}}(u,v)=v^{+}.\phi_{(g,a),(v^{*}\mathbf{f},a)}(\alpha,1).$

This morphism is independent of the choice of cartesian lift
$v^{*}\mathbf{f}\to\mathbf{f}$, by an argument similar to the one which now
follows.

We should check that the lifting function $\psi_{g-}$ defined this way
satisfies the functoriality condition of (3.1). To this end, consider
$\mathbf{w}\mathbf{x}:\mathbf{f}\to\mathbf{f}^{\prime}$ in $\mathcal{J}$ and
$(u,v):g\to f$. We get lifts
$\phi(\alpha)=\phi_{(g,a),(v^{*}\mathbf{f},a)}(\alpha,1)$ and
$\phi(\beta)=\phi_{(g,a),(v^{*}\mathbf{f}^{\prime},1)}(\beta,1)$, as on the
left and middle below, with $y=x.v$, $v^{*}\mathbf{f}\to\mathbf{f}$ cartesian
over $v$, and $v^{*}\mathbf{f}^{\prime}\to\mathbf{f}^{\prime}$ cartesian over
$y$:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${{\bullet}}$${{\bullet\hbox
to0.0pt{ ,\hss}}}$${\bullet}$${\bullet}$${{\bullet\hbox to0.0pt{
,\hss}}}$${\bullet}$${\bullet}$${{\bullet\hbox to0.0pt{
.\hss}}}$$\scriptstyle{g}$$\scriptstyle{v^{*}f}$$\scriptstyle{f}$$\scriptstyle{v}$$\scriptstyle{1}$$\scriptstyle{\alpha}$$\scriptstyle{v^{+}}$$\scriptstyle{\phi(\alpha)}$$\scriptstyle{g}$$\scriptstyle{v^{*}f^{\prime}}$$\scriptstyle{f^{\prime}}$$\scriptstyle{y^{+}}$$\scriptstyle{y}$$\scriptstyle{\beta}$$\scriptstyle{1}$$\scriptstyle{\phi(\beta)}$$\scriptstyle{g}$$\scriptstyle{\alpha}$$\scriptstyle{1}$$\scriptstyle{\gamma}$$\scriptstyle{1}$$\scriptstyle{v^{*}f^{\prime}}$$\scriptstyle{v^{*}f}$$\scriptstyle{\phi(\alpha)}$$\scriptstyle{\phi(\beta)}$$\scriptstyle{f^{\prime}}$$\scriptstyle{w}$$\scriptstyle{x}$

It follows from the universal property of the cartesian lift
$v^{*}\mathbf{f}^{\prime}\to\mathbf{f}^{\prime}$ that there is a
$\mathcal{J}$-morphism $\bm{\gamma}:v^{*}\mathbf{f}\to
v^{*}\mathbf{f}^{\prime}$ over $(\gamma,1)$, as on the right above, and so we
get $\gamma.\phi(\alpha)=\phi(\gamma.\alpha)=\phi(\beta)$; hence
$w.v^{+}.\phi(\alpha)=y^{+}.\gamma.\phi(\alpha)=y^{+}.\phi(\beta)$ as desired.
∎

###  3.4. Frobenius equivalence

It is now straightforward to define and prove a Frobenius equivalence for
categories of maps.

######  Definition 48.

Let $f:A\to B$ be a map in ${\mathcal{C}}$, and $(\mathcal{J},\mathcal{K})$ a
pair of functors over $\mathbf{Ar}({\mathcal{C}})$. A _Frobenius structure_
$\mathbf{f}^{*}$ on $f$ for $(\mathcal{J},\mathcal{K})$ is a filler as on the
left below:

${{\mathcal{J}/B}}$${{\mathcal{J}/A}}$${{\mathcal{K}/A}}$${{\mathcal{K}/B}}$${{\mathbf{Ar}({\mathcal{C}}/B)}}$${{\mathbf{Ar}({\mathcal{C}}/A)\hbox
to0.0pt{
,\hss}}}$${{\mathbf{Ar}({\mathcal{C}}/A)}}$${{\mathbf{Ar}({\mathcal{C}}/B)\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{\mathbf{Ar}(f^{*})}$$\scriptstyle{\mathbf{f}^{*}}$$\scriptstyle{\mathbf{Ar}(f_{*})}$$\scriptstyle{\mathbf{f}_{*}}$

Similarly, a _pushforward structure_ $\mathbf{f}_{*}$ on $f$ is a filler as on
the right above.

######  Theorem 49.

For a map $f:A\to B$ in ${\mathcal{C}}$ and a closed lifting structure
$(\mathcal{J},\phi,\mathcal{K})$ on $C$, there is a bijection between
Frobenius and pushforward structures on $f$ for $(\mathcal{J},\mathcal{K})$.

###### Proof.

The previous results give us the following string of isomorphisms:

$\displaystyle{\bf
Cat}/\mathbf{Ar}(-_{\mathrm{ladj}})(\mathcal{J}/B,\mathcal{J}/A)$
$\displaystyle\cong{\bf
Cat}/\mathbf{Ar}(-_{\mathrm{ladj}})(\mathcal{J}/B,{{}^{\pitchfork}}(\mathcal{K}/A))$
$\displaystyle\cong{\bf
Cat}/\mathbf{Ar}(-_{\mathrm{radj}})(\mathcal{K}/A,(\mathcal{J}/B){{}^{\pitchfork}})$
$\displaystyle\cong{\bf
Cat}/\mathbf{Ar}(-_{\mathrm{radj}})(\mathcal{K}/A,\mathcal{K}/B),$

where we consider morphisms in ${\bf Cat}/\mathbf{Ar}(-_{\mathrm{ladj}})$ and
${\bf Cat}/\mathbf{Ar}(-_{\mathrm{radj}})$ w.r.t. $f^{*}{\,\dashv\,}f_{*}$. ∎

######  Definition 50.

A _Frobenius structure_ for a pair $(\mathcal{J},\mathcal{K})$ of functors
over $\mathbf{Ar}(C)$ is a choice of Frobenius structure $\mathbf{f}^{*}$ for
every $\mathbf{f}\in K$; likewise, a _pushforward structure_ for
$(\mathcal{J},\mathcal{K})$ is a choice of pushforward structure
$\mathbf{f}_{*}$ for every $\mathbf{f}\in K$.

###  3.5. An example of split reflections and split opfibrations

We now give an example of a Frobenius structure in the sense of Definition 50,
building on [5, Proposition 5.3]. Recall from Examples 30 and 31 the functors
$\mathbf{SplRef}\to\mathbf{Ar}({\bf Cat})$ and
$\mathbf{SplOpFib}\to\mathbf{Ar}({\bf Cat})$. Given a split opfibration
$P:{\mathcal{A}}\to{\mathcal{B}}$, an object $a\in{\mathcal{A}}$ and a
morphism $Pa\to b$ in ${\mathcal{B}}$ we write $\smash{\underline{f}:a\to
f_{!}a}$ for the choice of cocartesian lift of $f$ along $a$:

${a}$${{f_{!}a}}$${Pa}$${{b\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{\underline{f}}$

Note that this notation is imprecise, since the lift $\smash{\underline{f}}$
also depends on $a$. Each morphism $f:b\to b^{\prime}\in{\mathcal{B}}$ thus
induces a functor $f_{!}:{\mathcal{A}}(b)\to{\mathcal{A}}(b^{\prime})$, where
${\mathcal{A}}(b)$ denotes the preimage category under $P$, sending an element
$a\in{\mathcal{A}}(b)$ to the codomain of $\smash{\underline{f}}$.

######  Proposition 51.

The pair $(\mathbf{SplRef},\mathbf{SplOpFib})$ admits a Frobenius structure.

###### Proof.

We construct a lift
$\mathbf{P}^{*}:\mathbf{SplRef}/{\mathcal{B}}\to\mathbf{SplRef}/{\mathcal{A}}$
for an opfibration $P:{\mathcal{A}}\to{\mathcal{B}}$:

${{\mathbf{SplRef}/{\mathcal{B}}}}$${{\mathbf{SplRef}/{\mathcal{A}}}}$${{\mathbf{Ar}({\bf
Cat}/{\mathcal{B}})}}$${{\mathbf{Ar}({\bf Cat}/{\mathcal{A}})\hbox to0.0pt{
.\hss}}}$$\scriptstyle{\mathbf{Ar}(P^{*})}$$\scriptstyle{\mathbf{P}^{*}}$

Consider a situation as drawn on the left below, where $L\dashv R$ is a split
reflection with unit $\eta$; the goal is to construct a split reflection
$G\dashv P^{*}R$ as on the left of:

(3.9)
${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{D}}}}$${{\mathcal{D}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{C}}}}$${{\mathcal{C}}}$${{\mathcal{A}}}$${{{\mathcal{B}}\hbox
to0.0pt{
,\hss}}}$$\scriptstyle{P}$$\scriptstyle{U}$$\scriptstyle{R}$$\scriptstyle{P^{*}U}$$\scriptstyle{F}$$\scriptstyle{P^{*}R}$$\scriptstyle{G}$$\scriptstyle{L}$$\scriptstyle{\pi_{\mathcal{C}}}$
${a}$${{(U\eta_{c})_{!}a}}$${Uc}$${{URLc\hbox to0.0pt{
.\hss}}}$$\scriptstyle{U\eta_{c}}$$\scriptstyle{\underline{U\eta_{c}}}$

To achieve this we first define an auxiliary functor
$F:{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{C}}\to{\mathcal{A}}:(a,c)\mapsto(U\eta_{c})_{!}a$,
as illustrated on the right above. The action of $F$ on a morphism
$(a_{1},c_{1})\to(a_{2},c_{2})$ is defined using the universal property of
$\smash{\underline{U\eta_{\smash{c_{1}}}}}$. Now $G$ is defined by
$(a,c)\mapsto(F(a,c),Lc)$, i.e. $G=F\times_{\mathcal{B}}L.\pi_{\mathcal{C}}$.
Lastly, we need a unit $\theta:1\Rightarrow P^{*}R.G$, for which we take

$\theta_{(a,c)}=(\underline{U\eta_{c}},\eta_{c}):(a,c)\to(F(a,c),RLc).$

We have to show that $G$ is a left inverse of $P^{*}R$, and that the triangle
identities $\theta.P^{*}R=1$ and $G.\theta=1$ hold. To start, we note that
because $\eta.R=1$, and the splitting of $P$ preserves units, we have for
$(a,d)\in{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{D}}$ that

(3.10) $\underline{U\eta_{Rd}}=\underline{U1_{Rd}}=\underline{1_{URd}}=1_{a}.$

Therefore, $F(a,Rd)=(U\eta_{Rd})_{!}a=(1_{a})_{!}a=a$, and so

$G(P^{*}R(a,d))=G(a,Rd)=(F(a,Rd),LRd)=(a,d),$

which is to say that $G$ is a left inverse of $P^{*}R$. Similarly, from (3.10)
we get

$\theta_{P^{*}R(a,d)}=\theta_{(a,Rd)}=(\smash{\underline{U\eta_{Rd}}},\eta_{Rd})=(1_{a},1_{Rd}).$

Lastly, we check if $G\theta_{(a,c)}=(1_{F(a,c)},1_{Lc})$. As $L.\eta=1$ by
assumption, this comes down to verifying that
$F(\smash{\underline{U\eta_{c}}},\eta_{c})=1_{F(a,c)}:F(a,c)\to
F(F(a,c),RLc)$. Substituting $Lc$ for $d$ in (3.10) we find that
$\smash{\underline{U\eta_{RLc}}}=1_{F(a,c)}$ and so $F(F(a,c),RLc)=F(a,c)$.
Therefore, the desired result follows from the universal property of the lift
$\smash{\underline{U\eta_{c}}}$.

It remains to check that $\mathbf{P}^{*}$ preserves morphisms of split
reflections; to this end, we consider a morphism of split reflections
$(X,Y):(L^{\prime},R^{\prime})\to(L,R)$ as drawn below:

${{{\mathcal{A}}\times_{\mathcal{B}}\mathcal{F}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{D}}}}$${{\mathcal{F}}}$${{\mathcal{D}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{E}}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{C}}}}$${{\mathcal{E}}}$${{\mathcal{C}}}$${{\mathcal{A}}}$${{{\mathcal{B}}\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{P}$$\scriptstyle{R}$$\scriptstyle{L}$$\scriptstyle{R^{\prime}}$$\scriptstyle{L^{\prime}}$$\scriptstyle{X}$$\scriptstyle{Y}$$\scriptstyle{U}$$\scriptstyle{U^{\prime}}$$\scriptstyle{P^{*}Y}$$\scriptstyle{P^{*}X}$$\scriptstyle{P^{*}R^{\prime}}$$\scriptstyle{G^{\prime}}$$\scriptstyle{G}$$\scriptstyle{P^{*}R}$$\scriptstyle{P^{*}U^{\prime}}$$\scriptstyle{P^{*}U}$

We want that $G.P^{*}Y=P^{*}X.G^{\prime}$, i.e. that
$(F(a,Ye),LYe)=(F^{\prime}(a,e),XL^{\prime}e)$ for
$(a,e)\in{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{E}}$. In fact, both
equalities are simple consequences of the assumption that $L.Y=X.L^{\prime}$
(which implies $\eta\circ Y=Y\circ\eta^{\prime}$). ∎

##  4\. Algebraic Weak Factorisation Systems

An awfs is a significantly more structured object than a wfs, and at first
sight their definitions appear quite distinct, because awfs are usually
defined in terms of an interacting monad-comonad pair, making no explicit
mention of liftings as in diagram (2.1). However, it was recently shown in [2]
that awfs admit an equivalent definition—there called _lifting_ awfs for
distinction—very much akin to Definition 1 of wfs. In this definition of awfs,
the role of the subclasses $L,R\subseteq{\mathcal{C}}_{1}$ in the definition
of a wfs are played by _double functors_
$\mathbb{L},\mathbb{R}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ over the double
category $\mathbb{S}\mathbf{q}({\mathcal{C}})$ of squares in ${\mathcal{C}}$.
To explain what that means, let us first briefly recall what we mean by double
categories.

###  4.1. Double categories

A double category $\mathbb{C}$ can be succinctly defined as an internal
category in ${\bf Cat}$. This amounts to the following data, satisfying the
usual axioms of a category:

${{\mathbb{C}_{0}}}$${{\mathbb{C}_{1}}}$${{\mathbb{C}_{1}\times_{\mathbb{C}_{0}}\mathbb{C}_{1}\hbox
to0.0pt{ .\hss}}}$$\scriptstyle{c}$id$\scriptstyle{s}$$\scriptstyle{t}$

More specifically, a double category $\mathbb{C}$ consists of a category
$\mathbb{C}_{0}$ of objects and a category $\mathbb{C}_{1}$ of arrows, with
operations $\text{id},s,t,c$ for identity arrow assignment, source, target,
and composition operations, respectively. A double category has two types of
morphisms: there are the morphisms of $\mathbb{C}_{0}$, called the
_horizontal_ morphisms of $\mathbb{C}$; and the objects of $\mathbb{C}_{1}$,
called the _vertical_ morphisms of $\mathbb{C}$. The morphisms of
$\mathbb{C}_{1}$ are called _squares_ of $\mathbb{C}$. There is an associated
notion of double functor, which yields the category ${\bf Dbl}$ of double
categories. There is a functor $\mathbb{S}\mathbf{q}:{\bf Cat}\to{\bf Dbl}$
sending a category ${\mathcal{C}}$ to its _double category of squares_
$\mathbb{S}\mathbf{q}({\mathcal{C}})$. The object category of
$\mathbb{S}\mathbf{q}({\mathcal{C}})$ is ${\mathcal{C}}$ itself, and the arrow
category of $\mathbb{S}\mathbf{q}({\mathcal{C}})$ is the arrow category
$\mathbf{Ar}({\mathcal{C}})$.

We saw in Section 3 that a notion of structured morphisms in the ambient
category ${\mathcal{C}}$ can be given as a functor
$\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$. If we wish to impose in addition a
condition saying that the morphisms in $\mathcal{J}$ are closed under
composition, the natural way to capture this is as a double functor over
$\mathbb{S}\mathbf{q}({\mathcal{C}})$, i.e. morphisms
$\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ in ${\bf Dbl}$. Note,
however, that in principle a double functor
$\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ endows ${\mathcal{C}}$ with
more structure than just that on its arrows; for example, it also imposes
structures on its objects through the functor
$\mathbb{J}_{0}\to{\mathcal{C}}$. In many examples of interest, no additional
structure is imposed except that on the arrows. Such double categories are
called concrete in [3].

######  Definition 52.

A double functor $\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ is
_concrete_ if $\mathbb{J}_{0}$ is an isomorphism and $\mathbb{J}_{1}$ is
faithful.

By internalising the definition of natural transformations the category ${\bf
Dbl}$ can be made a 2-category. Spelling this out, a _double_ natural
transformation $\alpha:F\Rightarrow G$ between double functors
$F,G:\mathbb{C}\to\mathbb{D}$ is a functor
$\alpha:\mathbb{C}_{0}\to\mathbb{D}_{1}$ subject to various conditions, such
as $s_{\mathbb{D}}.\alpha=F_{0}$. This means that, by virtue of how we defined
horizontal and vertical morphisms, a double natural transformation would
assign to each object of $\mathbb{C}$ a _vertical_ morphism of $\mathbb{D}$.
However, a second candidate for the 2-cells of ${\bf Dbl}$ is given by first
_transposing_ the double categories and functors involved. This is a type of
duality for double categories in which the sets of vertical and horizontal
arrows are switched. We thus obtain a notion of double natural transformation
which assigns to each object of $\mathbb{C}$ a _horizontal_ morphism of
$\mathbb{D}$, again subject to various conditions. Following [3], we will
consider ${\bf Dbl}$ as a 2-category by taking the latter of these two options
for the 2-cells.

######  Example 53.

Given adjunctions $L\dashv R:{\mathcal{D}}\to{\mathcal{C}}$ and
$L^{\prime}\dashv R^{\prime}:{\mathcal{E}}\to{\mathcal{D}}$ there is a
composite adjunction $L^{\prime}L\dashv
RR^{\prime}:{\mathcal{E}}\to{\mathcal{C}}$, given by pasting the units and
counits:

${{\mathcal{C}}}$${{\mathcal{C}}}$${{\mathcal{C}}}$${{\mathcal{C}}}$${{\mathcal{D}}}$${{\mathcal{E}}}$${{\mathcal{D}}}$${{\mathcal{D}}}$${{\mathcal{C}}}$${{\mathcal{D}}}$${{\mathcal{D}}}$${{\mathcal{E}}}$${{\mathcal{E}}}$${{\mathcal{D}}}$${{{\mathcal{C}}\hbox
to0.0pt{ ,\hss}}}$${{\mathcal{E}}}$${{\mathcal{E}}}$${{{\mathcal{E}}\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{L}$$\scriptstyle{L^{\prime}}$$\scriptstyle{L}$$\scriptstyle{R}$$\scriptstyle{1}$$\scriptstyle{1}$$\scriptstyle{1}$$\scriptstyle{1}$$\scriptstyle{R^{\prime}}$$\scriptstyle{R}$$\scriptstyle{1}$$\scriptstyle{1}$$\scriptstyle{\eta^{\prime}}$$\scriptstyle{\eta}$$\scriptstyle{L}$$\scriptstyle{L^{\prime}}$$\scriptstyle{R}$$\scriptstyle{R^{\prime}}$$\scriptstyle{1}$$\scriptstyle{1}$$\scriptstyle{1}$$\scriptstyle{1}$$\scriptstyle{R^{\prime}}$$\scriptstyle{1}$$\scriptstyle{1}$$\scriptstyle{L^{\prime}}$$\scriptstyle{\varepsilon}$$\scriptstyle{\varepsilon^{\prime}}$

More explicitly, the unit of the composed adjunction is given by
$(R\circ\eta^{\prime}\circ L).\eta$, where $\circ$ denotes horizontal
composition. Split reflections are closed under composition, and so the
functor $\mathbf{SplRef}\to\mathbf{Ar}({\bf Cat})$ forms the arrow part of a
double functor $\mathbb{S}\mathbf{plRef}\to\mathbb{S}\mathbf{q}({\bf Cat})$.

######  Example 54.

Given split opfibrations $P:{\mathcal{A}}\to{\mathcal{B}}$ and
$Q:{\mathcal{B}}\to{\mathcal{D}}$ the composition $Q.P$ is made into a split
opfibration by first lifting along $Q$ and then along $P$. We can thus extend
$\mathbf{SplOpFib}\to\mathbf{Ar}({\bf Cat})$ to a double functor
$\mathbb{S}\mathbf{plOpFib}\to\mathbb{S}\mathbf{q}({\bf Cat})$.

###  4.2. Lifting

A lifting operation for a pair of double functors
$\mathbb{J},\mathbb{K}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ is one for their
underlying functors over $\mathbf{Ar}({\mathcal{C}})$, satisfying a further
coherence condition with respect to composition in $\mathbb{J}$ and
$\mathbb{K}$.

######  Definition 55.

Let $\mathbb{J},\mathbb{K}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$; a
$(\mathbb{J},\mathbb{K})$-_lifting operation_ $\phi$ is a
$(\mathbb{J}_{1},\mathbb{K}_{1})$-lifting operation which respects composition
in $\mathbb{J}$ and $\mathbb{K}$, in the sense that given vertical composable
morphisms $\mathbf{f},\mathbf{f}^{\prime}$ in $\mathbb{J}$, and
$\mathbf{g},\mathbf{g}^{\prime}$ in $\mathbb{K}$, as well as a lifting problem
$(u,v):f.f^{\prime}\to g.g^{\prime}$, we have
$\phi_{\mathbf{f},\mathbf{g}^{\prime}}(\phi_{\mathbf{f}^{\prime},\mathbf{g}.\mathbf{g}^{\prime}}(u,v.f),\phi_{\mathbf{f}.\mathbf{f}^{\prime},\mathbf{g}}(g^{\prime}.u,v))=\phi_{\mathbf{f}.\mathbf{f}^{\prime},\mathbf{g}.\mathbf{g}^{\prime}}(u,v)$:

(4.1)
${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${{=}}$${\bullet}$${\bullet}$${\bullet}$${{\bullet\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{f^{\prime}}$$\scriptstyle{f}$$\scriptstyle{g^{\prime}}$$\scriptstyle{g}$$\scriptstyle{f.f^{\prime}}$$\scriptstyle{g.g^{\prime}}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{\phi_{\mathbf{f}.\mathbf{f}^{\prime},\mathbf{g}.\mathbf{g}^{\prime}}}$$\scriptstyle{\phi_{\mathbf{f},\mathbf{g}^{\prime}}}$

The assignment
$(\mathbb{J},\mathbb{K})\mapsto\mathbf{Lift}(\mathbb{J},\mathbb{K})$ of double
functors $\mathbb{J},\mathbb{K}$ to the class
$\mathbf{Lift}(\mathbb{J},\mathbb{K})$ of $(\mathbb{J},\mathbb{K})$-lifting
operations can again be made the object part of a functor

(4.2) $\mathbf{Lift}:({\bf
Dbl}/\mathbb{S}\mathbf{q}({\mathcal{C}}))^{\mathrm{op}}\times({\bf
Dbl}/\mathbb{S}\mathbf{q}({\mathcal{C}}))^{\mathrm{op}}\to{\bf Set},$

which is again representable in both arguments, as shown in [3, Proposition
18].

######  Proposition 56.

$\mathbf{Lift}$ is representable in both arguments, inducing an adjunction:

(4.3) ${{({\bf
Dbl}/\mathbb{S}\mathbf{q}({\mathcal{C}}))^{\mathrm{op}}}}$${{{\bf
Dbl}/\mathbb{S}\mathbf{q}({\mathcal{C}})\hbox to0.0pt{
.\hss}}}$$\scriptstyle{{{}^{\pitchfork\mskip-9.7mu\pitchfork}}(-)}$$\scriptstyle{(-){{}^{\pitchfork\mskip-9.7mu\pitchfork}}}$$\scriptstyle{\dashv}$

###### Proof.

The representing object of $\mathbf{Lift}(-,\mathbb{J})$ is a double category
${{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$
of which the vertical morphisms are pairs $(f,\phi_{f-})$ with
$\phi_{f-}\in\mathbf{Lift}(f,\mathbb{J})$ (where we consider $f$ to be a
double functor $f:1\to\mathbb{S}\mathbf{q}({\mathcal{C}})$). Vertical
composition in ${{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{J}$ is
performed as in (4.1), and a morphism $(f,\phi_{f-})\to(g,\phi_{g-})$ is a
square $(u,v):f\to g$ which commutes with the lifting operations. The
representing object
$\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$
of $\mathbf{Lift}(\mathbb{J},-)$ is defined analogously. ∎

We obtain the following analog of (3.4):

(4.4) ${\bf
Dbl}/\mathbb{S}\mathbf{q}(C)(\mathbb{J},{{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{K})\cong\mathbf{Lift}(\mathbb{J},\mathbb{K})\cong{\bf
Dbl}/\mathbb{S}\mathbf{q}({\mathcal{C}})(\mathbb{K},\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}}).$

######  Definition 57.

A triple $(\mathbb{J},\phi,\mathbb{K})$ of double functors
$\mathbb{J},\mathbb{K}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ and a
$(\mathbb{J},\mathbb{K})$-lifting operation $\phi$ is called a _lifting
structure_. A lifting structure $(\mathbb{J},\phi,\mathbb{K})$ is called
_closed_ when the functors
$\phi_{l}:\mathbb{J}\to{{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{K}$ and
$\phi_{r}:\mathbb{K}\to\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}}$
induced by (4.4) are invertible.

######  Example 58.

Let $\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$; applying (4.4) to the
identities on ${{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{J}$ and
$\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}}$ yields lifting operations
$\lambda\in\mathbf{Lift}({{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{J},\mathbb{J})$
and
$\rho\in\mathbf{Lift}(\mathbb{J},\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}})$,
and so we get, as we did in Example 11, two canonical lifting structures
$({{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{J},\lambda,\mathbb{J})$ and
$(\mathbb{J},\rho,\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}})$. Again,
this yields lifting structure
$({{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{J},\rho,({{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{J}){{}^{\pitchfork\mskip-9.7mu\pitchfork}})$
and
$({{}^{\pitchfork\mskip-9.7mu\pitchfork}}(\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}}),\lambda,\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}})$
which are said to be fibrantly generated and cofibrantly generated by
$\mathbb{J}$.

The following is [2, Definition 3] of a lifting awfs.

######  Definition 59.

An _algebraic weak factorisation system_ (awfs) on a category ${\mathcal{C}}$
is a closed lifting structure $(\mathbb{J},\phi,\mathbb{K})$ which satisfies
the axiom of factorisation, requiring every morphism $f\in{\mathcal{C}}_{1}$
to admit a bi-universal factorisation $f=h.g$ for vertical morphisms
$\mathbf{g}$ and $\mathbf{h}$ of $\mathbb{L}$ and $\mathbb{R}$ respectively.

######  Example 60.

The double functors $\mathbb{S}\mathbf{plRef}\to\mathbb{S}\mathbf{q}({\bf
Cat})$ and $\mathbb{S}\mathbf{plFib}\to\mathbb{S}\mathbf{q}({\bf Cat})$ form
part of an awfs, when equipped with the lifting structure defined in Example
37. For the proof we refer to [2, Examples 4 (ii)].

In what follows we will never need the axiom of factorisation, so we will
focus on closed lifting structures instead.

##  5\. The Frobenius equivalence for double categories of maps

In this section we will finally establish a Frobenius equivalence for awfss.
For this we follow the outline we sketched in Subsection 2.2 and build on the
work in Section 3. That is, we will establish double-categorical versions of
base change and slicing, from which the Frobenius equivalence will be a direct
corollary.

###  5.1. Base Change

We start with base change. As noted in [3, Proposition 21], the adjunction in
(4.3) can be extended to allow for change of base. This is done by considering
a 2-category ${\bf Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{ladj}})$ which can be
defined as the pullback:

${{\bf Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{ladj}})}$${{{\bf
Cat}_{\mathrm{ladj}}}}$${{\bf Cat}}$${{\mathbf{Ar}({\bf Dbl})}}$${{{\bf
Dbl}\hbox to0.0pt{
.\hss}}}$$\scriptstyle{\operatorname{cod}}$$\scriptstyle{\lrcorner}$$\scriptstyle{\mathbb{S}\mathbf{q}}$

The 2-category ${\bf Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{radj}})$ is defined
dually. We now have an adjunction

(5.1) ${{({\bf
Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{ladj}}))^{\text{coop}}}}$${{{\bf
Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{radj}})\hbox to0.0pt{
.\hss}}}$$\scriptstyle{{{}^{\pitchfork\mskip-9.7mu\pitchfork}}(-)}$$\scriptstyle{(-){{}^{\pitchfork\mskip-9.7mu\pitchfork}}}$$\scriptstyle{\dashv}$

extending that of (4.3), where $(-)^{\text{coop}}$ denotes reversal of both
the 1- and 2-cells.

###  5.2. Slicing

We now define a double categorical analog of the slicing operation that we saw
in Section 3.3. Given a double functor
$\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ and an object
$A\in{\mathcal{C}}$ we define the slice double functor
$\mathbb{J}/A\to\mathbb{S}\mathbf{q}({\mathcal{C}}/A)$ by the following
pullback:

${{\mathbb{J}/A}}$${\mathbb{J}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/A)}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}})\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{\mathbb{S}\mathbf{q}(\operatorname{dom})}$$\scriptstyle{\lrcorner}$

Pullbacks in ${\bf Dbl}$ are taken levelwise, so
$(\mathbb{J}/A)_{1}=\mathbb{J}_{1}/A$. Vertical composition in $\mathbb{J}/A$
is essentially just vertical composition in $\mathbb{J}$; a pair of vertical
morphisms $(\mathbf{g},b)$ and $(\mathbf{f},a)$ in $\mathbb{J}/A$ is
composable if $b=a.f$, and their composition is given by
$(\mathbf{f}.\mathbf{g},a)$.

Like before, we have:

######  Proposition 61.

Let $(\mathbb{J},\phi,\mathbb{K})$ be a lifting structure on ${\mathcal{C}}$
and $A\in{\mathcal{C}}$ some object, then there is a lifting structure
$(\mathbb{J}/A,\phi/A,\mathbb{K}/A)$ on ${\mathcal{C}}/A$.

###### Proof.

Let $\phi/A$ be the lifting operation defined in Proposition 41: it respects
vertical composition whenever $\phi$ does. ∎

We would like to extend this result to:

######  Proposition 62.

If $(\mathbb{J},\phi,\mathbb{K})$ is a closed lifting structure then so is
$(\mathbb{J}/A,\phi/A,\mathbb{K}/A)$.

For this we need an analog of the results of Section 3.3: that for
$\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ there are isomorphisms
$(\mathbb{J}/A)^{\pitchfork\mskip-9.7mu\pitchfork}\cong(\mathbb{J}^{\pitchfork\mskip-9.7mu\pitchfork})/A$
and
$({{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{J})/A\cong{{}^{\pitchfork\mskip-9.7mu\pitchfork}}(\mathbb{J}/A)$.
As before, only the former of these exists in general, for the latter we need
an additional assumption.

######  Proposition 63.

For $\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$, and
$A\in{\mathcal{C}}$, there are double functors

$(\lambda/A)_{l}:({{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{J})/A\to{{}^{\pitchfork\mskip-9.7mu\pitchfork}}(\mathbb{J}/A)\quad\mbox{
and
}\quad(\rho/A)_{r}:(\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}})/A\to(\mathbb{J}/A){{}^{\pitchfork\mskip-9.7mu\pitchfork}},$

with the latter double functor $(\rho/A)_{r}$ being an isomorphism.

###### Proof.

At this point this should be routine. ∎

######  Definition 64.

A double functor $\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ is a
_comprehension double category_ if
$\mathbb{J}_{1}\to\mathbf{Ar}({\mathcal{C}})$ is a comprehension category as
in Definition 45, and, moreover, the squares in $\mathbb{J}$ that are
cartesian with respect to the Grothendieck fibration
$\operatorname{cod}.\mathbb{J}_{1}$ are closed under vertical composition.
That is, if we have two squares in $\mathbb{J}$ that can be composed
vertically as in

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet,}$$\scriptstyle{\mathbf{g}^{\prime}}$$\scriptstyle{\mathbf{u}}$$\scriptstyle{\mathbf{g}}$$\scriptstyle{\mathbf{h}^{\prime}}$$\scriptstyle{\mathbf{v}}$$\scriptstyle{\mathbf{h}}$$\scriptstyle{\mathbf{w}}$

in which the top square is cartesian over $v$ and the bottom square cartesian
over $w$, then the vertically composed square is cartesian over $w$.

######  Proposition 65.

$\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$
is a comprehension double category for any
$\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$.

###### Proof.

This follows from the fact that a square in
$\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}}$ is cartesian precisely
when its image under
$(\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}})_{1}\to\mathbf{Ar}({\mathcal{C}})$
is a pullback. ∎

######  Proposition 66.

Let $\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ be a comprehension
double category, and $A\in{\mathcal{C}}$ be some object; then the double
functor $(\lambda/A)_{l}$ of Proposition 63 is an isomorphism.

###### Proof.

We show that the lifting operation defined in (3.7) satisfies the vertical
condition. To this end we consider a vertical composition
$\mathbf{h}.\mathbf{g}$ in $\mathbb{J}$ and a square $(u,v):f\to h.g$.:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${{\bullet\hbox to0.0pt{
.\hss}}}$$\scriptstyle{g}$$\scriptstyle{h}$$\scriptstyle{f}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{\psi(h)}$$\scriptstyle{\psi(g)}$$\scriptstyle{\psi(h.g)}$

We use the abbreviations $\psi(h)=\psi_{f,\mathbf{h}}(g.u,v)$,
$\psi(g)=\psi_{f,\mathbf{g}}(u,\psi(h))$, and
$\psi(h.g)=\psi_{f,\mathbf{h}.\mathbf{g}}(u,v)$, so we should show
$\psi(h.g)=\psi(g)$. The diagrams below respectively show how these are
computed:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${{\bullet\hbox
to0.0pt{ ,\hss}}}$${\bullet}$${\bullet}$${{\bullet\hbox to0.0pt{
,\hss}}}$${\bullet}$${\bullet}$${{\bullet\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{v^{*}h}$$\scriptstyle{v^{+}}$$\scriptstyle{h}$$\scriptstyle{v}$$\scriptstyle{\alpha}$$\scriptstyle{\phi(h)}$$\scriptstyle{f}$$\scriptstyle{\psi(h)^{*}g}$$\scriptstyle{g}$$\scriptstyle{f}$$\scriptstyle{v^{*}(h.g)}$$\scriptstyle{h.g}$$\scriptstyle{\beta}$$\scriptstyle{\psi(h)^{+}}$$\scriptstyle{\gamma}$$\scriptstyle{v^{++}}$$\scriptstyle{v}$$\scriptstyle{\psi(h)}$$\scriptstyle{\phi(g)}$$\scriptstyle{\phi(h.g)}$

So for instance $\psi(h)=v^{+}.\phi(h)$, where $\phi(h)$ is an abbreviation
for $\phi_{(f,a),(v^{*}\mathbf{h},a)}(\alpha,1)$, which is the lift obtained
from the $\mathbb{J}/A$ lifting operation of $(f,a)$ applied to the
$\mathbb{J}/A$ map $(v^{*}\mathbf{h},a)$.

Our assumption that cartesian square are closed under vertical composition
implies that the cartesian square
$v^{*}(\mathbf{h}.\mathbf{g})\to\mathbf{h}.\mathbf{g}$ can be assumed to be
the vertical composition of two squares

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet,}$$\scriptstyle{v^{*}\mathbf{g}}$$\scriptstyle{\mathbf{v}^{++}}$$\scriptstyle{v^{*}(\mathbf{h}.\mathbf{g})}$$\scriptstyle{\mathbf{g}}$$\scriptstyle{\mathbf{h}.\mathbf{g}}$$\scriptstyle{v^{*}\mathbf{h}}$$\scriptstyle{\mathbf{v}^{+}}$$\scriptstyle{\mathbf{h}}$$\scriptstyle{\mathbf{v}}$

with $\mathbf{v}^{++}\mathbf{v}^{+}:v^{*}\mathbf{g}\to\mathbf{g}$ a cartesian
morphism in $\mathbb{J}$ over $v^{+}$. Since $v^{*}\mathbf{g}$ is a vertical
map in $\mathbb{J}$, we get a lift
$\phi^{\prime}(g)=\phi_{(f,a),(v^{*}\mathbf{g},a.v^{*}h)}(\gamma,\phi(h))$,
and by the vertical condition $\phi(h.g)=\phi^{\prime}(g)$.

Furthermore, because $\mathbf{v}^{++}\mathbf{v}^{+}$ is cartesian, there is a
square $\mathbf{i}\mathbf{j}:\psi(h)^{*}\mathbf{g}\to v^{*}\mathbf{g}$ in
$\mathbb{J}$:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$$\scriptstyle{\psi(h)^{*}{\mathbf{g}}}$$\scriptstyle{v^{*}{\mathbf{g}}}$$\scriptstyle{\mathbf{g}}$$\scriptstyle{\mathbf{i}}$$\scriptstyle{\mathbf{j}}$$\scriptstyle{\mathbf{v}^{++}}$$\scriptstyle{\mathbf{v}^{+}}$

with $j=\phi(h)$. Since $\gamma=i.\beta$ we get that
$\phi(h.g)=\phi^{\prime}(g)=i.\phi(g)$, and so

$\psi(h.g)=v^{++}.\phi(h.g)=v^{++}.i.\phi(g)=\psi(h)^{+}.\phi(g)=\psi(g).\qed$

###  5.3. Frobenius equivalence

The following is now a direct analogue of the results from Subsection 3.4.

######  Definition 67.

Let $f:A\to B$ be a map in ${\mathcal{C}}$, and $(\mathbb{J},\mathbb{K})$ a
pair of double functors over $\mathbb{S}\mathbf{q}({\mathcal{C}})$. A
_Frobenius structure_ $\mathbf{f}^{*}$ on $f$ for $(\mathbb{J},\mathbb{K})$ is
a filler as on the left of:

${{\mathbb{J}/B}}$${{\mathbb{J}/A}}$${{\mathbb{K}/A}}$${{\mathbb{K}/B}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/B)}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/A)\hbox
to0.0pt{
,\hss}}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/A)}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/B)\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{\mathbb{S}\mathbf{q}(f^{*})}$$\scriptstyle{\mathbf{f}^{*}}$$\scriptstyle{\mathbb{S}\mathbf{q}(f_{*})}$$\scriptstyle{\mathbf{f}_{*}}$

Similarly, a _pushforward structure_ $\mathbf{f}_{*}$ on $f$ is a filler as on
the right above.

######  Theorem 68.

For a map $f:A\to B$ in $\mathcal{C}$, and a closed lifting structure
$(\mathbb{J},\phi,\mathbb{K})$, there is a bijection between Frobenius and
pushforward structures on $f$ for $(\mathbb{J},\mathbb{K})$.

###### Proof.

Combining the previous results we get

$\displaystyle{\bf
Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{ladj}})(\mathbb{J}/B,\mathbb{J}/A)$
$\displaystyle\cong{\bf
Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{ladj}})(\mathbb{J}/B,(\mathbb{K}/A)^{\pitchfork\mskip-9.7mu\pitchfork})$
$\displaystyle\cong{\bf
Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{radj}})(\mathbb{K}/A,{{}^{\pitchfork\mskip-9.7mu\pitchfork}}(\mathbb{J}/B))$
$\displaystyle\cong{\bf
Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{radj}})(\mathbb{K}/A,\mathbb{K}/B),$

where we consider morphisms in ${\bf
Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{ladj}})$ and ${\bf
Dbl}/\mathbb{S}\mathbf{q}(-_{\mathrm{radj}})$ w.r.t. $f^{*}\dashv f_{*}$. ∎

######  Definition 69.

A _Frobenius structure_ for a pair $(\mathbb{J},\mathbb{K})$ is an assignment
of a Frobenius structure $\mathbf{f}^{*}$ to every vertical morphism
$\mathbf{f}$ of $\mathbb{K}$.

######  Remark 70.

Let us interpret the meaning of a Frobenius structure on $f:A\to B$ when the
double categories are given by the pair
$(\mathsf{L}\text{-}\mathbb{C}\mathbf{oalg},\mathsf{R}\text{-}\mathbb{A}\mathbf{lg})$
underlying an awfs $(\mathsf{L},\mathsf{R})$. The double category
$\mathsf{\mathsf{L}}\text{-}\mathbb{C}\mathbf{oalg}/A$ is then formed as on
the left below:

${{\mathsf{\mathsf{L}}\text{-}\mathbb{C}\mathbf{oalg}/A}}$${{\mathsf{\mathsf{L}}\text{-}\mathbb{C}\mathbf{oalg}}}$${{\mathsf{\mathsf{L}}\text{-}\mathbb{C}\mathbf{oalg}/B}}$${{\mathsf{\mathsf{L}}\text{-}\mathbb{C}\mathbf{oalg}/A}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/A)}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}})\hbox
to0.0pt{
,\hss}}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/B)}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/A)\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{\mathbb{S}\mathbf{q}(\operatorname{dom})}$$\scriptstyle{\lrcorner}$$\scriptstyle{\mathbb{S}\mathbf{q}(f^{*})}$$\scriptstyle{\mathbf{f}^{*}}$

This situation is discussed more generally in [3, Section 4.5], and it is
shown there that the pullback along $\mathbb{S}\mathbf{q}(\operatorname{dom})$
yields a _slice_ awfs $(\mathsf{L}/A,\mathsf{R}/A)$ on ${\mathcal{C}}/A$ such
that
$(\mathsf{L}/A)\text{-}\mathbb{C}\mathbf{oalg}\cong\mathsf{L}\text{-}\mathbb{C}\mathbf{oalg}/A$.
This means that the square of the Frobenius structure, pictured on the right
above, is in the image of the semantics functor
$\mathsf{(-)}\text{-}\mathbb{C}\mathbf{oalg}$. Therefore, as this functor is
full [3, Proposition 2], a Frobenius structure on $f$ can be understood as
making $f^{*}$ an oplax morphism of slice awfs
$(\mathsf{L}/B,\mathsf{R}/B)\to(\mathsf{L}/A,\mathsf{R}/A)$. Dually, a
pushforward structure $\mathbf{f}_{*}$ on $f$ corresponds to a lax morphism of
slice awfs.

###  5.4. An example of split reflections and split opfibrations

As an example of a pair with a Frobenius structure, we have the following
adaptation of Proposition 51.

######  Proposition 71.

The pair $(\mathbb{S}\mathbf{plRef},\mathbb{S}\mathbf{plOpFib})$ admits a
Frobenius structure.

###### Proof.

We extend the Frobenius structure for a split opfibration
$P:{\mathcal{A}}\to{\mathcal{B}}$ of Proposition 51 to one for this pair by
showing $\mathbf{P}^{*}$ preserves composition of split reflections, yielding:

${{\mathbb{S}\mathbf{plRef}/{\mathcal{B}}}}$${{\mathbb{S}\mathbf{plRef}/{\mathcal{A}}}}$${{\mathbb{S}\mathbf{q}({\bf
Cat}/{\mathcal{B}})}}$${{\mathbb{S}\mathbf{q}({\bf Cat}/{\mathcal{A}})\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{\mathbf{P}^{*}}$$\scriptstyle{\mathbb{S}\mathbf{q}(P^{*})}$

To verify this, we consider the situation sketched below:

${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{E}}}}$${{\mathcal{E}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{E}}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{D}}}}$${{\mathcal{D}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{C}}}}$${{\mathcal{C}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{C}}}}$${{\mathcal{A}}}$${{\mathcal{B}}}$${{{\mathcal{A}}\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{P}$$\scriptstyle{P}$$\scriptstyle{\pi_{\mathcal{C}}}$$\scriptstyle{\pi_{\mathcal{D}}}$$\scriptstyle{\pi_{\mathcal{E}}}$$\scriptstyle{\pi_{\mathcal{E}}}$$\scriptstyle{U}$$\scriptstyle{P^{*}U}$$\scriptstyle{F}$$\scriptstyle{F^{\prime}}$$\scriptstyle{P^{*}U}$$\scriptstyle{F^{\prime\prime}}$$\scriptstyle{P^{*}(R.R^{\prime})}$$\scriptstyle{G^{\prime\prime}}$$\scriptstyle{P^{*}R}$$\scriptstyle{G}$$\scriptstyle{P^{*}R^{\prime}}$$\scriptstyle{G^{\prime}}$$\scriptstyle{R}$$\scriptstyle{\pi_{\mathcal{C}}}$$\scriptstyle{L}$$\scriptstyle{R^{\prime}}$$\scriptstyle{L^{\prime}}$

On the left we have the composition of the pullbacks $G^{\prime}.G\dashv
P^{*}R.P^{*}R^{\prime}$, and on the right the pullback of the composition
$G^{\prime\prime}\dashv P^{*}(R.R^{\prime})$. We should show that
$G^{\prime\prime}=G^{\prime}.G$, and that the unit $\theta^{\prime\prime}$ of
$G^{\prime\prime}\dashv P^{*}(R^{\prime}R)$ is equal to
$(P^{*}R\circ\theta^{\prime}\circ G).\theta$.

These equalities hold precisely because $P$ is split, since this tells us that
for a pair $(a,c)\in{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{C}}$ we have
$\smash{\underline{UR\eta^{\prime}_{Lc}.U\eta_{C}}}=\smash{\underline{UR\eta^{\prime}_{Lc}}}.\underline{U\eta_{c}}$:

(5.2)
${a}$${{(U\eta_{c})_{!}c}}$${{(UR\eta^{\prime}_{Lc})_{!}(U\eta_{c})_{!}a}}$${Uc}$${URLc}$${{URR^{\prime}L^{\prime}Lc\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{U\eta_{c}}$$\scriptstyle{\underline{U\eta_{c}}}$$\scriptstyle{UR\eta^{\prime}_{Lc}}$$\scriptstyle{\underline{UR\eta^{\prime}_{Lc}}}$$\scriptstyle{\underline{UR\eta^{\prime}_{Lc}.U\eta_{C}}}$

To begin we note that $F^{\prime}(a,d)=(UR\eta^{\prime}_{d})_{!}a$, and so:

$\displaystyle F^{\prime\prime}(a,c)$
$\displaystyle=(U((R\circ\eta^{\prime}\circ L).\eta)_{c})_{!}a$
$\displaystyle=(UR\eta^{\prime}_{Lc}.U\eta_{c})_{!}a$
$\displaystyle=(UR\eta^{\prime}_{Lc})_{!}(U\eta_{c})_{!}a$
$\displaystyle=F^{\prime}((U\eta_{c})_{!}a,Lc)$
$\displaystyle=F^{\prime}G(a,c);$

which is to say $F^{\prime}.G=F^{\prime\prime}$. Therefore,

$G^{\prime}.G=(F^{\prime}\times_{\mathcal{B}}L^{\prime}.\pi_{\mathcal{D}}).G=F^{\prime}.G\times_{\mathcal{B}}L^{\prime}.\pi_{\mathcal{D}}.G=F^{\prime\prime}\times_{\mathcal{B}}L^{\prime}.L.\pi_{\mathcal{C}}=G^{\prime\prime}.$

The other equality $\theta^{\prime\prime}=(P^{*}R\circ\theta^{\prime}\circ
G).\theta$ also follows readily from (5.2):

$\displaystyle((P^{*}R\circ\theta^{\prime}\circ G).\theta)_{(a,c)}$
$\displaystyle=P^{*}R(\theta^{\prime}_{G(a,c)}).\theta_{(a,c)}$
$\displaystyle=(\smash{\underline{UR\eta^{\prime}_{Lc}}},R\eta^{\prime}_{Lc}).(\smash{\underline{U\eta_{c}}},\eta_{c})$
$\displaystyle=(\smash{\underline{UR\eta^{\prime}_{Lc}}}.\smash{\underline{U\eta_{c}}},R\eta^{\prime}_{Lc}.\eta_{c})$
$\displaystyle=(\smash{\underline{U((R\circ\eta^{\prime}\circ
L).\eta)_{c}}},((R\circ\eta^{\prime}\circ L).\eta)_{c})$
$\displaystyle=\theta^{\prime\prime}_{(a,c)}.\qed$

##  6\. The Beck–Chevalley condition

Ultimately we are interested in constructing models of type theory using the
right adjoint method for splitting comprehension categories, as used in [5].
In order for this method to work the right maps should satisfy a number of
stability conditions, as outlined in [14, Chapter 2]. The stability condition
for the $\Pi$-types is ensured by a Beck–Chevalley condition (cf. Proposition
88) which we will now phrase.

###  6.1. The categorical case

Consider a closed lifting structure $(\mathcal{J},\phi,\mathcal{K})$ with
$\mathcal{J}$ and $\mathcal{K}$ being categories of maps. For the purpose of
interpreting dependent product types we want this pair to have a pushforward
structure. However, in order for this interpretation to satisfy the coherence
axioms of the theory with respect to substitution, this pushforward structure
should respect morphisms of $\mathcal{K}$ whose underlying square in the
ambient category ${\mathcal{C}}$ is a pullback square.

More specifically, consider $\mathbf{f},\mathbf{g},\mathbf{h}\in\mathcal{K}$
such that $g$ and $h$ are composable, and a morphism
$\mathbf{uv}:\mathbf{f}\to\mathbf{g}$ whose underlying square in
${\mathcal{C}}$ is a pullback square:

(6.1) ${\bullet}$${A}$${C}$${\bullet}$${\bullet}$${B}$${{D\hbox to0.0pt{
,\hss}}}$${{B\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{h}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{\lrcorner}$$\scriptstyle{f_{*}u^{*}h}$$\scriptstyle{v^{*}g_{*}h}$$\scriptstyle{\beta^{-1}_{h}}$

This gives composite parallel adjunctions $u_{!}f^{*}\dashv
f_{*}u^{*},g^{*}v_{!}\dashv v^{*}g_{*}:{\mathcal{C}}/C\to{\mathcal{C}}/B$:

(6.2)
${{{\mathcal{C}}/B}}$${\bot}$${{{\mathcal{C}}/A}}$${\bot}$${{{\mathcal{C}}/C\hbox
to0.0pt{
,\hss}}}$${{{\mathcal{C}}/B}}$${\bot}$${{{\mathcal{C}}/D}}$${\bot}$${{{\mathcal{C}}/C\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{f^{*}}$$\scriptstyle{f_{*}}$$\scriptstyle{u_{!}}$$\scriptstyle{u^{*}}$$\scriptstyle{v_{!}}$$\scriptstyle{v^{*}}$$\scriptstyle{g^{*}}$$\scriptstyle{g_{*}}$

These induce a mateship correspondence between natural transformations with
signatures $u_{!}f^{*}\Rightarrow g^{*}v_{!}$ and $v^{*}g_{*}\Rightarrow
f_{*}u^{*}$. There is a canonical map $\alpha:u_{!}f^{*}\Rightarrow
g^{*}v_{!}$ (itself obtained as a mate of the identity natural transformation
$g_{!}u_{!}=v_{!}f_{!}$) of which the component $\alpha_{w}$ at an object $w$
in ${\mathcal{C}}/B$ is given as follows:

${\bullet}$${\bullet}$${A}$${C}$${\bullet}$${B}$${{D\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{\lrcorner}$$\scriptstyle{w}$$\scriptstyle{f^{*}w}$$\scriptstyle{\lrcorner}$$\scriptstyle{g^{*}v_{!}w}$$\scriptstyle{\alpha_{w}}$

We denote the mate of $\alpha$ with signature $v^{*}g_{*}\Rightarrow
f_{*}u^{*}$ by $\beta$. These transformations $\alpha$ and $\beta$ exist
regardless of whether $(u,v)$ is a pullback, but when it is they are both
isomorphisms; see e.g. [9, Lemma 3.5]. We call $\beta$ the Beck–Chevalley
isomorphism.

In the setup of the left diagram of (6.1), we thus get a triangle pictured as
the right diagram of (6.1). When $(\mathcal{J},\phi,\mathcal{K})$ is a closed
lifting structure, the right class is always closed under pullbacks, and so if
it comes with a Frobenius structure then the morphisms $f_{*}u^{*}h$ and
$v^{*}g_{*}h$ have $\mathcal{K}$ structure. What we need for the
interpretation of dependent products is that $(\beta_{h}^{-1},1)$ underlies a
morphism of $\mathcal{K}$ maps. The goal of this section is to precisely state
this condition, and to show it is equivalent to a condition that is easier to
check in practice. The way we do this is similar to the statement and proof of
[6, Proposition 6.7].

The first step will be to generalize to the case where $h$ is not an object
but an arrow of ${\mathcal{C}}/C$, i.e. we consider
$(\mathbf{h},w)\in\mathcal{K}/C$:

(6.3)
${\bullet}$${\bullet}$${\bullet}$${\bullet}$${A}$${C}$${\bullet}$${\bullet}$${B}$${{D\hbox
to0.0pt{ ,\hss}}}$${{B\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{w}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{\lrcorner}$$\scriptstyle{f_{*}u^{*}w}$$\scriptstyle{v^{*}g_{*}w}$$\scriptstyle{\beta^{-1}_{w}}$$\scriptstyle{h}$$\scriptstyle{f_{*}u^{*}h}$$\scriptstyle{v^{*}g_{*}h}$$\scriptstyle{\beta^{-1}_{w.h}}$

The square $(\beta^{-1}_{w.h},\beta^{-1}_{w})$ on the right above is the
component $\mathbf{Ar}(\beta^{-1})_{(h,w)}$ of the natural transformation
$\mathbf{Ar}(\beta^{-1}):\mathbf{Ar}(f_{*}u^{*})\Rightarrow\mathbf{Ar}(v^{*}g_{*})$.
For a closed lifting structure $(\mathcal{J},\phi,\mathcal{K})$ an isomorphism
in $\mathbf{Ar}({\mathcal{C}})$ underlies a morphism of $\mathcal{J}$ or
$\mathcal{K}$ maps if and only if its inverse does, so we will focus on
$\beta$ instead of $\beta^{-1}$. To state what it means for
$\mathbf{Ar}(\beta)_{(h,w)}$ to underlie a morphism of $\mathcal{K}$ maps we
use the following definition.

######  Definition 72.

Let $\mathbf{F},\mathbf{G}:\mathcal{J}\to\mathcal{K}$ be lifts of
$F,G:{\mathcal{C}}\to{\mathcal{D}}$ for some
$\mathcal{J}\to\mathbf{Ar}({\mathcal{C}})$ and
$\mathcal{K}\to\mathbf{Ar}({\mathcal{D}})$, and $\mu:F\Rightarrow G$ a natural
transformation. We say that $\bm{\mu}:\mathbf{F}\Rightarrow\mathbf{G}$ is a
_lift_ of $\mu$ if
$\mathcal{K}\circ\bm{\mu}=\mathbf{Ar}(\mu)\circ\mathcal{J}$, meaning its
components are over those of $\mu$:

${\mathcal{J}}$${\mathcal{K}}$${{\mathbf{Ar}({\mathcal{C}})}}$${{\mathbf{Ar}({\mathcal{D}})}\hbox
to0.0pt{
.\hss}}$$\scriptstyle{\mathbf{Ar}(F)}$$\scriptstyle{\mathbf{Ar}(G)}$$\scriptstyle{\mathbf{F}}$$\scriptstyle{\mathbf{G}}$$\scriptstyle{\,\mathbf{Ar}(\mu)}$$\scriptstyle{\,\bm{\mu}}$

Note that a composition functor like $u_{!}:{\mathcal{C}}/A\to C/C$ always
lifts to a functor
$\mathbf{u}_{!}:\mathcal{J}/A\to\mathcal{J}/C:(\mathbf{f},a)\mapsto(\mathbf{f},u.a)$.
Since $(\mathcal{J},\mathcal{K})$ has a Frobenius structure, we thus obtain
lifts $\mathbf{u}_{!}\mathbf{f}^{*}$ and $\mathbf{g}^{*}\mathbf{v}_{!}$ as on
the left of:

(6.4)
${{\mathcal{J}/B}}$${{\mathcal{J}/C}}$${{\mathcal{K}/C}}$${{\mathcal{K}/B}}$${{\mathbf{Ar}({\mathcal{C}}/B)}}$${{\mathbf{Ar}({\mathcal{C}}/C)}\hbox
to0.0pt{
,\hss}}$${{\mathbf{Ar}({\mathcal{C}}/C)}}$${{\mathbf{Ar}({\mathcal{C}}/B)}\hbox
to0.0pt{
.\hss}}$$\scriptstyle{\mathbf{u}_{!}\mathbf{f}^{*}}$$\scriptstyle{\mathbf{Ar}(u_{!}f^{*})}$$\scriptstyle{\mathbf{v}^{*}\mathbf{g}_{*}}$$\scriptstyle{\mathbf{Ar}(v^{*}g_{*})}$$\scriptstyle{\mathbf{Ar}(g^{*}v_{!})}$$\scriptstyle{\mathbf{Ar}(f_{*}u^{*})}$$\scriptstyle{\mathbf{f}_{*}\mathbf{u}^{*}}$$\scriptstyle{\mathbf{g}^{*}\mathbf{v}_{!}}$$\scriptstyle{\,\mathbf{Ar}(\alpha)}$$\scriptstyle{\,\bm{\beta}}$$\scriptstyle{\,\mathbf{Ar}(\beta)}$$\scriptstyle{\,\bm{\alpha}}$

Applying the reasoning of Proposition 38 with respect to the adjunctions
(6.2), we obtain corresponding lifts $\mathbf{v}^{*}\mathbf{g}_{*}$ and
$\mathbf{f}_{*}\mathbf{u}^{*}$ as on the right above. The condition that the
square $(\beta_{w.h},\beta_{w})$ is a morphism of $\mathcal{K}$ maps is now
expressed by requiring the existence of a lift $\bm{\beta}$ as depicted on the
right above, due to the requirement that
$(\mathcal{K}/B)\circ\bm{\beta}=\mathbf{Ar}(\beta)\circ(\mathcal{K}/C)$. Note
that—since the lifting structure $(\mathcal{J},\phi,\mathcal{K})$ is
closed—the existence of this lift is not additional structure, but is instead
just a property of $\beta$. In sum, we have the following definition.

######  Definition 73.

A Frobenius structure for a closed structure $(\mathcal{J},\phi,\mathcal{K})$
satisfies the _Beck–Chevalley condition_ when for every
$\mathbf{uv}:\mathbf{f}\to\mathbf{g}$ in $\mathcal{K}$ overlying a pullback
square $(u,v)$, the Beck–Chevalley isomorphism $\beta$ lifts to a
transformation
$\bm{\beta}:\mathbf{v}^{*}\mathbf{g}_{*}\Rightarrow\mathbf{f}_{*}\mathbf{u}^{*}$.

######  Proposition 74.

For a closed lifting structure $(\mathcal{J},\phi,\mathcal{K})$ with a
Frobenius structure, the Beck–Chevalley isomorphism $\beta$ lifts in the sense
of (6.4) iff its mate $\alpha$ does.

###### Proof.

By [6, Proposition 5.8], using that
$\mathcal{J}/C\cong{{}^{\pitchfork}}(\mathcal{K}/C)$ and
$\mathcal{K}/B\cong(\mathcal{J}/B){{}^{\pitchfork}}$. ∎

For future reference we expand on what it means for $\alpha$ to lift in the
sense of Proposition 74. Considering the pullback square $(u,v)$ in (6.3) and
$(w,b)\in\mathbf{Ar}({\mathcal{C}}/B)$, the component
$\mathbf{Ar}(\alpha)_{(w,b)}$ is given by the square
$(\alpha_{b.w},\alpha_{b}):u_{!}f^{*}(w,b)\to g^{*}v_{!}(w,b)$:

(6.5)
${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${B}$${A}$${C}$${D\hbox
to0.0pt{
.\hss}}$$\scriptstyle{f^{*}b}$$\scriptstyle{g^{*}(v.b)}$$\scriptstyle{u}$$\scriptstyle{f^{*}w}$$\scriptstyle{\alpha_{b}}$$\scriptstyle{g^{*}w}$$\scriptstyle{\alpha_{b.w}}$$\scriptstyle{f}$$\scriptstyle{b}$$\scriptstyle{w}$$\scriptstyle{v}$$\scriptstyle{g}$

If in addition $(\mathbf{w},b)\in\mathcal{J}/B$, then $f^{*}w$ and $g^{*}w$
underlie $\mathcal{J}$ maps $\mathbf{f}^{*}\mathbf{w}$ and
$\mathbf{g}^{*}\mathbf{w}$, and $\bm{\alpha}$ should produce a $\mathcal{J}$
morphism
$\bm{\alpha}_{(\mathbf{w},b)}:\mathbf{f}^{*}\mathbf{w}\to\mathbf{g}^{*}\mathbf{w}$
overlying $(\alpha_{b.w},\alpha_{b})$.

###  6.2. The double categorical case

Next, we phrase an analogous version of Definition 73 for a pair of double
categories. More specifically, we consider the case where (6.3) underlies a
square $\mathbf{uv}:\mathbf{f}\to\mathbf{g}$ in $\mathbb{K}$ for some closed
lifting structure $(\mathbb{J},\phi,\mathbb{K})$ with a Frobenius structure.
To start, we define lifts of double natural transformations.

######  Definition 75.

Let $\mathbf{F},\mathbf{G}:\mathbb{J}\to\mathbb{K}$ be lifts of
$F,G:{\mathcal{C}}\to{\mathcal{D}}$ for some
$\mathbb{J}\to\mathbf{Ar}({\mathcal{C}})$ and
$\mathbb{K}\to\mathbf{Ar}({\mathcal{D}})$, and $\mu:F\Rightarrow G$ a natural
transformation. We say that $\bm{\mu}:\mathbf{F}\Rightarrow\mathbf{G}$ is a
_lift_ of $\mu$ if
$\mathbb{K}\circ\bm{\mu}=\mathbb{S}\mathbf{q}(\mu)\circ\mathbb{J}$:

${\mathbb{J}}$${\mathbb{K}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}})}}$${{\mathbb{S}\mathbf{q}({\mathcal{D}})}\hbox
to0.0pt{
.\hss}}$$\scriptstyle{\mathbb{S}\mathbf{q}(F)}$$\scriptstyle{\mathbb{S}\mathbf{q}(G)}$$\scriptstyle{\mathbf{F}}$$\scriptstyle{\mathbf{G}}$$\scriptstyle{\,\mathbb{S}\mathbf{q}(\mu)}$$\scriptstyle{\,\bm{\mu}}$

Note that a composition functor such as
$u_{!}:{\mathcal{C}}/A\to{\mathcal{C}}/C$ in fact lifts to a double functor
$\mathbf{u}_{!}:\mathbb{J}/A\to\mathbb{J}/C$, as the assignment
$(\mathbf{f},a)\mapsto(\mathbf{f},u.a)$ (trivially) preserves vertical
composition. Using the Frobenius structure of $(\mathbb{J},\mathbb{K})$ and
the adjunction (5.1) we thus obtains lifts $\mathbf{u}_{!}\mathbf{f}^{*}$ and
$\mathbf{g}^{*}\mathbf{v}_{!}$ as on the left below:

(6.6)
${{\mathbb{J}/B}}$${{\mathbb{J}/C}}$${{\mathbb{K}/C}}$${{\mathbb{K}/B}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/C)}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/B)\hbox
to0.0pt{
,\hss}}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/C)}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}}/B)\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{\mathbf{g}^{*}\mathbf{v}_{!}}$$\scriptstyle{\mathbf{u}_{!}\mathbf{f}^{*}}$$\scriptstyle{\mathbb{S}\mathbf{q}(u_{!}f^{*})}$$\scriptstyle{\mathbb{S}\mathbf{q}(g^{*}v_{!})}$$\scriptstyle{\mathbf{v}^{*}\mathbf{g}_{*}}$$\scriptstyle{\mathbf{f}_{*}\mathbf{u}^{*}}$$\scriptstyle{\mathbb{S}\mathbf{q}(v^{*}g_{*})}$$\scriptstyle{\mathbb{S}\mathbf{q}(f_{*}u^{*})}$$\scriptstyle{\,\mathbb{S}\mathbf{q}(\beta)}$$\scriptstyle{\,\bm{\beta}}$$\scriptstyle{\,\mathbb{S}\mathbf{q}(\alpha)}$$\scriptstyle{\,\bm{\alpha}}$

As $(\mathbb{J},\mathbb{K})$ is part of a closed lifting structure, the lifts
$\mathbf{u}_{!}\mathbf{f}^{*}$ and $\mathbf{g}^{*}\mathbf{v}_{!}$ can be
transposed to lifts $\mathbf{v}^{*}\mathbf{g}_{*}$ and
$\mathbf{f}_{*}\mathbf{u}^{*}$ using (5.1). Now we can phrase the
Beck–Chevalley condition for double categories completely analogously to that
for categories.

######  Definition 76.

A Frobenius structure for a pair $(\mathbb{J},\mathbb{K})$ of double
categories satisfies the _Beck–Chevalley condition_ when for every
$\mathbf{uv}:\mathbf{f}\to\mathbf{g}$ in $\mathbb{K}$ overlying a pullback
square $(u,v)$, the Beck–Chevalley isomorphism $\beta$ lifts to a
transformation
$\bm{\beta}:\mathbf{v}^{*}\mathbf{g}_{*}\Rightarrow\mathbf{f}_{*}\mathbf{u}^{*}$.

Of course, the definitions of Frobenius structure and Beck–Chevalley condition
directly apply to closed lifting structures underlying awfs.

As before, lifting $\beta$ in this way can be done by lifting $\alpha$, which
is easier in practice.

######  Proposition 77.

For a closed lifting structure $(\mathbb{J},\phi,\mathbb{K})$ with a Frobenius
structure, the Beck–Chevalley isomorphism $\beta$ lifts in the sense of (6.6)
iff its mate $\alpha$ does.

###### Proof.

By the fact that (5.1) is a 2-adjunction [3, Proposition 21], in combination
with the isomorphisms
$\mathbb{J}/C\cong{{}^{\pitchfork\mskip-9.7mu\pitchfork}}(\mathbb{K}/C)$ and
$\mathbb{K}/B\cong(\mathbb{J}/B){{}^{\pitchfork\mskip-9.7mu\pitchfork}}$. ∎

In fact, as we will now show, for concrete double functors Definitions 72 and
75 coincide. This means that checking whether a Frobenius structure for a
closed structure $(\mathbb{J},\phi,\mathbb{K})$ satisfies the Beck–Chevalley
condition comes down to checking whether its Frobenius structure for
$(\mathbb{J}_{1},\mathbb{K}_{1})$, obtained by an application of $(-)_{1}:{\bf
Dbl}\to{\bf Cat}$, satisfies the Beck–Chevalley condition.

######  Lemma 78.

Let $\mathbb{J}\to\mathbb{S}\mathbf{q}({\mathcal{C}})$ and
$\mathbb{K}\to\mathbb{S}\mathbf{q}({\mathcal{D}})$ be concrete double
functors, and $\mathbf{F},\mathbf{G}:\mathbb{J}\to\mathbb{K}$ lifts of
$F,G:{\mathcal{C}}\to{\mathcal{D}}$; then lifts of $\mu:F\to G$ to
$\mathbf{F}\Rightarrow\mathbf{G}$ are in bijection with its lifts to
$\mathbf{F}_{1}\Rightarrow\mathbf{G}_{1}$:

${\mathbb{J}}$${\mathbb{K}}$${{\mathbb{J}_{1}}}$${{\mathbb{K}_{1}}}$${{\mathbb{S}\mathbf{q}({\mathcal{C}})}}$${{\mathbb{S}\mathbf{q}({\mathcal{D}})\hbox
to0.0pt{
,\hss}}}$${{\mathbf{Ar}({\mathcal{C}})}}$${{\mathbf{Ar}({\mathcal{D}})\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{\mathbf{G}}$$\scriptstyle{\mathbf{F}}$$\scriptstyle{\mathbb{S}\mathbf{q}(F)}$$\scriptstyle{\mathbb{S}\mathbf{q}(G)}$$\scriptstyle{\mathbf{F}_{1}}$$\scriptstyle{\mathbf{G}_{1}}$$\scriptstyle{\mathbf{Ar}(F)}$$\scriptstyle{\mathbf{Ar}(G)}$$\scriptstyle{\,\mathbf{Ar}(\mu)}$$\scriptstyle{\,\bm{\mu}}$$\scriptstyle{\,\mathbb{S}\mathbf{q}(\mu)}$$\scriptstyle{\,\bm{\mu}}$

###### Proof.

By spelling out the definitions. ∎

######  Lemma 79.

For a closed lifting structure $(\mathbb{J},\phi,\mathbb{K})$ and
$A\in{\mathcal{C}}$ the double functors $\mathbb{J}/A$ and $\mathbb{K}/A$ are
concrete.

###### Proof.

The double functors $\mathbb{J}{{}^{\pitchfork\mskip-9.7mu\pitchfork}}$ and
${{}^{\pitchfork\mskip-9.7mu\pitchfork}}\mathbb{J}$ are always concrete for
any $\mathbb{J}$, and so because the lifting structure is closed so are
$\mathbb{J}$ and $\mathbb{K}$. Furthermore, slicing preserves concreteness. ∎

######  Corollary 80.

A Frobenius structure for a closed lifting structure
$(\mathbb{J},\phi,\mathbb{K})$ satisfies the Beck–Chevalley condition when its
associated Frobenius structure for $(\mathbb{J}_{1},\mathbb{K}_{1})$ does.

###### Proof.

By Lemmas 78 and 79. ∎

Lastly, we show that our running example satisfies this condition.

######  Proposition 81.

The Frobenius structure for
$(\mathbb{S}\mathbf{plRef},\mathbb{S}\mathbf{plOpFib})$ of Proposition 71
satisfies the Beck–Chevalley condition.

###### Proof.

Consider a pullback square $(X,Y)$ between split opfibrations $P$ and $Q$
which commutes with their splittings. By Corollary 80 it suffices to show that
the induced transformation $\alpha:X_{!}P^{*}\Rightarrow Q^{*}Y_{!}$ has a
lift $\bm{\alpha}$ as depicted on the left below:

${{\mathbf{SplRef}/{\mathcal{B}}}}$${{\mathbf{SplRef}/{\mathcal{C}}}}$${{\mathbf{Ar}({\bf
Cat}/{\mathcal{B}})}}$${{\mathbf{Ar}({\bf Cat}/{\mathcal{C}})}\hbox to0.0pt{
,\hss}}$$\scriptstyle{\mathbf{X}_{!}\mathbf{P}^{*}}$$\scriptstyle{\mathbf{Q}^{*}\mathbf{Y}_{!}}$$\scriptstyle{\mathbf{Ar}(X_{!}P^{*})}$$\scriptstyle{\mathbf{Ar}(Q^{*}Y_{!})}$$\scriptstyle{\,\bm{\alpha}}$$\scriptstyle{\,\mathbf{Ar}(\alpha)}$
${{\mathcal{F}}}$${{{\mathcal{A}}\times_{\mathcal{B}}\mathcal{F}}}$${{{\mathcal{C}}\times_{\mathcal{D}}\mathcal{F}}}$${{\mathcal{E}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{E}}}}$${{{\mathcal{C}}\times_{\mathcal{D}}{\mathcal{E}}}}$${{\mathcal{B}}}$${{\mathcal{A}}}$${{\mathcal{C}}}$${{\mathcal{D}}\hbox
to0.0pt{
.\hss}}$$\scriptstyle{P}$$\scriptstyle{X}$$\scriptstyle{Q}$$\scriptstyle{Y}$$\scriptstyle{U}$$\scriptstyle{L}$$\scriptstyle{R}$$\scriptstyle{F}$$\scriptstyle{P^{*}U}$$\scriptstyle{G}$$\scriptstyle{P^{*}R}$$\scriptstyle{Q^{*}R}$$\scriptstyle{G^{\prime}}$$\scriptstyle{Q^{*}(Y.U)}$$\scriptstyle{F^{\prime}}$$\scriptstyle{\alpha_{U}}$$\scriptstyle{\alpha_{U.R}}$$\scriptstyle{\pi_{\mathcal{F}}}$$\scriptstyle{\pi_{\mathcal{E}}}$

This comes down to showing that the square
$(\alpha_{U.R},\alpha_{U})=(X.\pi_{\mathcal{A}}\times_{\mathcal{D}}\pi_{\mathcal{F}},X.\pi_{\mathcal{A}}\times_{\mathcal{D}}\pi_{\mathcal{E}})$
is a morphism of split reflections, meaning
$(X.\pi_{\mathcal{A}}\times_{\mathcal{D}}\pi_{\mathcal{F}}).G=G^{\prime}.(X.\pi_{\mathcal{A}}\times_{\mathcal{D}}\pi_{\mathcal{E}})$,
as on the right above. Spelling out the definitions involved we see that this
comes down to showing that for any pair
$(a,e)\in{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{E}}$ we have
$X((U\eta_{e})_{!}a)=(YU\eta_{e})_{!}Xa$. Since $(X,Y)$ is a morphism of
opfibrations we have
$\smash{\underline{YU\eta_{e}}}=X\smash{\underline{U\eta_{e}}}$, from which
the desired equality follows immediately. ∎

##  7\. Strong Frobenius structures

We turn to a minor digression concerning strengthened versions of the
Frobenius property sometimes encountered in the literature; see e.g. [14,
Definition B.6.2] and [17, Proposition 5.2]. Recall that Definition 3 of the
Frobenius property for a wfs $(L,R)$ states that $L$ is closed under pullback
along $R$; if, in addition, $L$ comes with a notion of structure preserving
squares of $L$ maps, then the Frobenius property can be strengthened to demand
that the pullback squares of $L$ maps along $R$ maps are structure preserving.
We argue that this strengthened Frobenius property can be understood in terms
of the notion of natural transformation lifting of Definition 72.

Let $(\mathcal{J},\mathcal{K})$ be a pair of functors over an arrow category
$\mathbf{Ar}({\mathcal{C}})$, and $f:A\to B$ a map in ${\mathcal{C}}$. A
Frobenius structure for $f$ is a lift
$\mathbf{f}^{*}:\mathcal{J}/B\to\mathcal{J}/A$. A pair $(\mathbf{g},b)$ in
$\mathcal{J}/B$ now gives rise to a pullback square as depicted below, where
$\varepsilon$ is the counit of $f_{!}{\,\dashv\,}f^{*}$:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${A}$${{B\hbox to0.0pt{
.\hss}}}$$\scriptstyle{f^{*}b}$$\scriptstyle{b}$$\scriptstyle{f}$$\scriptstyle{\varepsilon_{b}}$$\scriptstyle{g}$$\scriptstyle{f^{*}g}$$\scriptstyle{\varepsilon_{b.g}}$$\scriptstyle{\lrcorner}$$\scriptstyle{\lrcorner}$

As mentioned previously, for any such $f$ there is a lift
$\mathbf{f}_{!}:\mathcal{J}/A\to\mathcal{J}/B:(\mathbf{g},a)\mapsto(\mathbf{g},f.a)$,
and so the demand that $(\varepsilon_{b.g},\varepsilon_{b})$ is in the image
of a map $\mathbf{f}^{*}\mathbf{g}\to\mathbf{g}$ in $\mathcal{J}$ can be
phrased as the requirement that $\varepsilon$ has a lift
$\bm{\varepsilon}:\mathbf{f}_{!}\mathbf{f}^{*}\to 1$ in the sense of
Definition 72. What is called the strong Frobenius property in the literature
can then be seen as the special case of this where $b=1_{B}$ and
$f^{*}b=1_{A}$.

Thinking of the strong Frobenius property in this way shows that it has an
evident counterpart, which is the requirement that the unit $\eta$ of
$f_{!}{\,\dashv\,}f^{*}$ lifts to
$\bm{\eta}:1\to\mathbf{f}^{*}\mathbf{f}_{!}$. Together, these lifts could then
be further required to satisfy the triangle identities, so that
$\mathbf{f}_{!}{\,\dashv\,}\mathbf{f}^{*}$. If $(\mathcal{J},\mathcal{K})$ is
part of a closed lifting structure then we can transpose $\mathbf{f}^{*}$ and
$\mathbf{f}_{!}$ to obtain a pushforward structure
$\mathbf{f}_{*}:\mathcal{K}/A\to\mathcal{K}/B$ and (by abuse of notation)
$\mathbf{f}^{*}:\mathcal{K}/B\to\mathcal{K}/A$. These can then be subjected to
similar conditions, asking for a lifted adjunction
$\mathbf{f}^{*}{\,\dashv\,}\mathbf{f}_{*}$. For the sake of discussion we will
call such lifted adjunctions strong Frobenius and strong pushforward
structures.

######  Definition 82.

A _strong Frobenius structure_ $(\mathbf{f}^{*},\bm{\eta},\bm{\varepsilon})$
on a morphism $f:A\to B$ with respect to a closed pair
$(\mathcal{J},\mathcal{K})$ is a Frobenius structure on $f$ togther with lifts
$\bm{\eta}$ and $\bm{\varepsilon}$ of the unit and counit of
$f_{!}{\,\dashv\,}f^{*}$, giving rise to an adjunction
$\mathbf{f}_{!}{\,\dashv\,}\mathbf{f}^{*}$ as on the left of:

${{\mathcal{J}/B}}$${{\mathcal{J}/A}}$${{\mathcal{K}/A}}$${{\mathcal{K}/B}}$${{\mathbf{Ar}({\mathcal{C}}/B)}}$${{\mathbf{Ar}({\mathcal{C}}/A)\hbox
to0.0pt{
,\hss}}}$${{\mathbf{Ar}({\mathcal{C}}/A)}}$${{\mathbf{Ar}({\mathcal{C}}/B)\hbox
to0.0pt{
.\hss}}}$$\scriptstyle{\mathbf{Ar}(f^{*})}$$\scriptstyle{\mathbf{f}^{*}}$$\scriptstyle{\mathbf{Ar}(f_{*})}$$\scriptstyle{\mathbf{f}_{*}}$$\scriptstyle{\mathbf{f}_{!}}$$\scriptstyle{\mathbf{Ar}(f_{!})}$$\scriptstyle{\mathbf{f}^{*}}$$\scriptstyle{\mathbf{Ar}(f^{*})}$$\scriptstyle{\dashv}$$\scriptstyle{\dashv}$$\scriptstyle{\dashv}$$\scriptstyle{\dashv}$

Similarly, a _strong pushforward structure_
$(\mathbf{f}_{*},\bar{\bm{\eta}},\bar{\bm{\varepsilon}})$ on $f$ is a
pushforward structure on $f$ with lifts $\bar{\bm{\eta}}$ and
$\bar{\bm{\varepsilon}}$ of the unit and counit of $f^{*}{\,\dashv\,}f_{*}$,
such that $\mathbf{f}^{*}{\,\dashv\,}\mathbf{f}_{*}$.

######  Proposition 83.

For a map $f:A\to B$ in $\mathcal{C}$, and a closed lifting structure
$(\mathcal{J},\phi,\mathcal{K})$, there is a bijection between strong
Frobenius and pushforward structures on $f$.

###### Proof.

The units and counits of $f_{!}{\,\dashv\,}f^{*}{\,\dashv\,}f_{*}$ are mates
[9, Lemma 3.1], and so—due to how the various lifts of $f_{!}$, $f^{*}$, and
$f_{*}$ are constructed, and that $(\mathcal{J},\phi,\mathcal{K})$ is
closed—their lifts are in bijective correspondence by [6, Proposition 5.8].
The triangle equalities do not add any extra requirement because $\mathcal{J}$
and $\mathcal{K}$ are faithful (as the lifting structure is closed). ∎

Of course, similar definitions and results exist for the double categorical
case, and again our running example exhibits such a structure.

######  Proposition 84.

The pair $(\mathbf{SplRefl},\mathbf{SplOpFib})$ admits a strong Frobenius
structure.

###### Proof.

We expand on the proof of Proposition 51 by showing that the Frobenius
structure $\mathbf{P}^{*}$ of a split opfibration
$P:{\mathcal{A}}\to{\mathcal{B}}$ comes with the required lifts. Since
$\mathbf{SplRefl}$ is faithful, these lifts are not additional structure but
just a property of $\mathbf{P}^{*}$. To show that $\varepsilon:P_{!}P^{*}\to
1$ lifts, we consider the situation as drawn on the left below:

${{{\mathcal{A}}\times{\mathcal{B}}_{\mathcal{D}}}}$${{\mathcal{D}}}$${{\mathcal{D}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{D}}}}$${{\mathcal{D}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{C}}}}$${{\mathcal{C}}}$${{\mathcal{C}}}$${{{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{C}}}}$${{\mathcal{C}}}$${{\mathcal{A}}}$${{{\mathcal{B}}\hbox
to0.0pt{ ,\hss}}}$${{\mathcal{A}}}$${{{\mathcal{B}}\hbox to0.0pt{
.\hss}}}$$\scriptstyle{R}$$\scriptstyle{L}$$\scriptstyle{G}$$\scriptstyle{P^{*}R}$$\scriptstyle{U}$$\scriptstyle{P^{*}P_{!}U}$$\scriptstyle{F}$$\scriptstyle{P}$$\scriptstyle{R}$$\scriptstyle{L}$$\scriptstyle{P_{!}U}$$\scriptstyle{\eta_{U.R}}$$\scriptstyle{\eta_{U}}$$\scriptstyle{U}$$\scriptstyle{R}$$\scriptstyle{L}$$\scriptstyle{F}$$\scriptstyle{P}$$\scriptstyle{P^{*}U}$$\scriptstyle{P^{*}R}$$\scriptstyle{G}$$\scriptstyle{\varepsilon_{U.R}}$$\scriptstyle{\varepsilon_{U}}$

Indeed, $(\varepsilon_{U.R},\varepsilon_{U})=(\pi_{D},\pi_{\mathcal{C}})$ is a
morphism of split reflections because for
$(a,c)\in{\mathcal{A}}\times_{\mathcal{B}}{\mathcal{C}}$ we have
$\pi_{\mathcal{D}}(G(a,c))=\pi_{\mathcal{D}}(F(a,c),Lc)=Lc=L(\pi_{\mathcal{C}}(a,c))$.
For $\eta:1\to P^{*}P_{!}$ we should show that the square
$(\eta_{U.R},\eta_{U})=(U.R\times_{\mathcal{B}}1_{\mathcal{D}},U\times_{{\mathcal{B}}}1_{\mathcal{C}})$,
drawn on the right above, is a morphism of split reflections, too. For
$c\in{\mathcal{C}}$, the equation $G(\eta_{U}(c))=\eta_{U.R}(Lc)$ boils down
to the equality $URLc=(PU\eta_{c})!Uc$. This is an instance of the general
fact that for any $f:a\to b$ in ${\mathcal{A}}$, the cocartesian lift
$\underline{Pf}$ is parallel to $f$ because $P$ is split. Lastly, these lifts
satisfy the triangle identities as $\mathbf{SplRefl}$ is faithful. ∎

##  8\. An algebraic model of type theory from groupoids

Comprehension categories are one of the categorical structures used to model
various forms of type theory. Substitution is modeled using pullbacks, and one
difficulty with this is that pullbacks are usually only associative up to
isomorphism, wheras substitution in type theory is strictly associative. So,
in order to faithfully model type theory, the comprehension category in
question should be split. One way to do this is to use the right adjoint of
the forgetful functor $\mathbf{SplFib}\to\mathbf{Fib}$. In [5, Theorem 2.6],
Gambino and Larrea give a coherence theorem for this method, by identifying
pseudo-stability conditions on a comprehension category that ensure that its
splitting has strict interpretations of the $\Sigma$-, $\Pi$, and
$\mathrm{Id}$-types of Martin-Löf type theory. Any awfs
$(\mathbb{L},\mathbb{R})$ induces a comprehension category
$\mathbb{L}_{1}^{\pitchfork}\to\mathbf{Ar}({\mathcal{C}})$, and conditions are
identified in [5, Theorem 4.11] on $(\mathbb{L},\mathbb{R})$ that ensure that
the coherence theorem can be applied to it. They then revisit the Hofmann and
Streicher groupoid model of [11], by exhibiting an awfs on the category ${\bf
Gpd}$ of groupoids which satisfies these conditions [5, Theorem 5.5].

An awfs $(\mathbb{L},\mathbb{R})$ induces a second (closely related)
comprehension category, namely $\mathbb{R}_{1}\to\mathbf{Ar}({\mathcal{C}})$,
and our goal in this section is to reproduce the aforementioned results in [5]
for this second option—that is, to identify conditions on the awfs
$(\mathbb{L},\mathbb{R})$ that ensure that the coherence theorem can be
applied to $\mathbb{R}_{1}\to\mathbf{Ar}({\mathcal{C}})$. (Note that there is
a functor
$\mathbb{R}_{1}\cong(\mathbb{L}{{}^{\pitchfork\mskip-9.7mu\pitchfork}})_{1}\hookrightarrow\mathbb{L}_{1}^{\pitchfork}$
over $\mathbf{Ar}({\mathcal{C}})$, which is generally not invertible;
$\mathbb{L}_{1}^{\pitchfork}$ corresponds to the retract closure of
$\mathbb{R}_{1}$.) We phrase these conditions, and then show that the same
awfs used by Gambino and Larrea on ${\bf Gpd}$ satisfies our conditions. The
majority of the work needed for this has been done in the preceeding sections,
and what remains is a straightforward adaptation of the approach of [5].
Therefore, we only outline the proofs, and the reader is referred to [5] for
the rest of the details.

###  8.1. Coherence for the comprehension category of right maps

As mentioned, the forgetful functor of the right class of an awfs is always a
comprehension category.

######  Proposition 85.

For an awfs $(\mathbb{L},\mathbb{R})$,
$\mathbb{R}_{1}\to\mathbf{Ar}({\mathcal{C}})$ is a comprehension category.

###### Proof.

This follows from Proposition 65 above. ∎

In fact, no further requirements on the awfs are needed to choose the
$\Sigma$-types.

######  Proposition 86.

The comprehension category $\mathbb{R}_{1}\to\mathbf{Ar}({\mathcal{C}})$
associated with an awfs admits a pseudo-stable choice of $\Sigma$-types.

###### Proof.

The choice of $\Sigma$-types is given simply by the composition operation of
$\mathbb{R}$, which is functorial and preserves pullback squares. The rest of
the choices of structure are made as in [5, Proposition 4.3] (and see [14,
Lemma 2.7.7]). ∎

The $\Pi$-types are interpreted using a pushforward structure on the awfs, and
the Beck–Chevalley condition ensures this choice is pseudo-stable. Following
terminology of [12] we introduce a shorthand for an awfs with this required
structure.

######  Definition 87.

A $\pi$-awfs is an awfs with a Frobenius structure satisfying the
Beck–Chevalley condition as in Definition 76.

######  Proposition 88.

The comprehension category $\mathbb{R}_{1}\to\mathbf{Ar}({\mathcal{C}})$
associated with a $\pi$-awfs admits a pseudo-stable choice of $\Pi$-types.

###### Proof.

Consider composable $\mathbb{R}$ maps $\mathbf{g}$ and $\mathbf{f}$. As the
awfs has a Frobenius structure, $\mathbf{f}$ has a pushforward structure
$\mathbf{f}_{*}$ by Theorem 68, which gives an $\mathbb{R}$ map
$\mathbf{f}_{*}\mathbf{g}$ by the reasoning in Proposition 26; this is the
choice of $\Pi$-type for $\mathbf{g}$ and $\mathbf{f}$. The Beck–Chevalley
condition ensures that the assignment
$\Pi:(\mathbf{g},\mathbf{f})\mapsto\mathbf{f}_{*}\mathbf{g}$ is functorial:

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\smash{\overset{\Pi}{\longmapsto}}}$${\bullet}$${\bullet}$${\bullet}$${{\bullet\hbox
to0.0pt{
,\hss}}}$${\bullet}$${\bullet}$$\scriptstyle{u}$$\scriptstyle{\mathbf{g}}$$\scriptstyle{\lrcorner}$$\scriptstyle{\mathbf{i}}$$\scriptstyle{f_{*}\alpha}$$\scriptstyle{\mathbf{f}_{*}\mathbf{g}}$$\scriptstyle{\beta_{i}}$$\scriptstyle{\mathbf{f}_{*}\mathbf{v}^{*}\mathbf{i}}$$\scriptstyle{w^{+}}$$\scriptstyle{\mathbf{w}^{*}\mathbf{h}_{*}\mathbf{i}}$$\scriptstyle{\mathbf{h}_{*}\mathbf{i}}$$\scriptstyle{v}$$\scriptstyle{\mathbf{f}}$$\scriptstyle{\lrcorner}$$\scriptstyle{\mathbf{h}}$$\scriptstyle{1}$$\scriptstyle{1}$$\scriptstyle{w}$$\scriptstyle{w}$

the outer rectangle on the right above is a pullback, and is a square of
$\mathbb{R}$ because all three of the squares comprising it are. The rest of
the choices of structure are made as in [5, Proposition 4.6] (and see [14,
Lemma 2.7.8]). ∎

The idea for interpreting identity types using wfs originates from [1] and was