Two-sided cartesian fibrations of synthetic $(\infty ,1)$-categories

Abstract

Within the framework of Riehl–Shulman’s synthetic $(\infty ,1)$-category theory, we present a theory of two-sided cartesian fibrations. Central results are several characterizations of the two-sidedness condition à la Chevalley, Gray, Street, and Riehl–Verity, a two-sided Yoneda Lemma, as well as the proof of several closure properties. Along the way, we also define and investigate a notion of fibered or sliced fibration which is used later to develop the two-sided case in a modular fashion. We also briefly discuss discrete two-sided cartesian fibrations in this setting, corresponding to $(\infty ,1)$-distributors. The systematics of our definitions and results closely follows Riehl–Verity’s $\infty$-cosmos theory, but formulated internally to Riehl–Shulman’s simplicial extension of homotopy type theory. All the constructions and proofs in this framework are by design invariant under homotopy equivalence. Semantically, the synthetic $(\infty ,1)$-categories correspond to internal $(\infty ,1)$-categories implemented as Rezk objects in an arbitrary given $(\infty ,1)$-topos.

Appendices

Fibered equivalences

We state some expected and useful closure properties of fibered equivalences.

Lemma A.1

(Right properness) Pullbacks of weak equivalences are weak equivalences again, i.e. , given a pullback diagram

then, as indicated if the right vertical map is a weak equivalence, then so is the left hand one.

Proof

Denote by $P: A \rightarrow \mathcal {U}$ the straightening of $k:B \rightarrow A$, so that $B \simeq \sum _{a:A} P\,a$, and $D \simeq \sum _{c:C} P(j\,c)$. The map $k:B \rightarrow A$ (identified with its projection equivalence) is a weak equivalence if and only if $\prod _{a:A} {{\,\textrm{isContr}\,}}(P\,a)$. This implies $\prod _{c:C} P(j\,c)$ which is equivalent to $k' = j^*k$ being a weak equivalence, as desired. $\square$

Proposition A.1

(Homotopy invariance of homotopy pullbacks) Given a map between cospans of types

where the vertical arrows are weak euivalences the induced map

$$\begin{aligned} B \times _A C \rightarrow B' \times _{A'} C' \end{aligned}$$

is an equivalence as well.

Proof

By right properness and 2-out-of-3 the mediating map is an equivalence as can be seen from the diagram:

This gives the following cube

and by the Pullback Lemma we know that the back face is a pullback, too. Then again, by right properness

$$\begin{aligned} B \times _A C \rightarrow B' \times _{A'} C' \end{aligned}$$

is an equivalence. $\square$

Proposition A.2

Given a fibered equivalence as below

and a map $k:A \rightarrow B$ the fibered equivalence $\varphi$ pulls back as shown below:

Proof

By projection equivalence, we can consider families $R:B \rightarrow \mathcal {U}$, $P: F \equiv \widetilde{R} \rightarrow \mathcal {U}$, $Q : E \equiv \widetilde{P} \rightarrow \mathcal {U}$, with $F \equiv \widetilde{Q}$. The fibered equivalence $\varphi$ is given by a family of equivalences

$$\begin{aligned} \varphi : \prod _{\begin{array}{c} b:B \\ x:R\,b \end{array}} \big ( \sum _{e:P\,b\,x} Q \, b \, x \, e \big ) {\mathop {\longrightarrow }\limits ^{\simeq }} P\,b\,x. \end{aligned}$$

The induced family

also constitutes a fibered equivalence. Commutation of all the diagrams is clear since, after projection equivalence, all the vertical maps are given by projections. $\square$

Lemma A.2

(Closedness of fibered equivalences under dependent products) Let I be a type. Suppose given a family $B:I\rightarrow \mathcal {U}$ and indexed families $P,Q:\prod _{i:I} B_i \rightarrow \mathcal {U}$ together with a fiberwise equivalence $\varphi : \prod _{i:I} \prod _{b:B} P_i\,b {\mathop {\longrightarrow }\limits ^{\simeq }} Q_i\,b$. Then the map

$$\begin{aligned} \prod _{i:I} \varphi _i: \big (\prod _{i:I} \widetilde{P_i} \big ) \longrightarrow _{\prod _{i:I} B_i} \big (\prod _{i:I} \widetilde{Q_i} \big ) \end{aligned}$$

induced by taking the dependent product over I is a fiberwise equivalence, too.

Proof

For i : I, we fibrantly replace the given fiberwise equivalence $\varphi _i$ by projections, giving rise to (strictly) commutative diagrams:

Now, $\varphi$ being a fiberwise equivalence is equivalent to

$$\begin{aligned} \prod _{i:I} {{\,\textrm{isEquiv}\,}}(\varphi _i)&\simeq \prod _{i:I} \prod _{\begin{array}{c} b:B_i \\ x:Q_i(b) \end{array}} {{\,\textrm{isContr}\,}}(P_i(b,x)) \\&\simeq \prod _{\beta :\prod _{i:I} B_i} \prod _{\sigma :\prod _{i:I} \beta ^* P_i} \prod _{i:I} {{\,\textrm{isContr}\,}}\left( P_i(\beta (i), \sigma (i))\right) . \end{aligned}$$

By (weak) function extensionality,³⁰ this implies

$$\begin{aligned}&\prod _{\beta :\prod _{i:I} B_i} \prod _{\sigma :\prod _{i:I} \beta ^*Q_i} {{\,\textrm{isContr}\,}}\left( \prod _{i:I} \langle {\beta },{\sigma }\rangle ^* P_i\right) \\&\quad \simeq {{\,\textrm{isEquiv}\,}}\left( \prod _{i:I} \varphi _i \right) \end{aligned}$$

wich yields the desired statement. Note, that the latter equivalence follows by projection equivalence of the diagram obtained by applying $\prod _{i:I}(-)$:

$\square$

Lemma A.3

(Closedness of fibered equivalences under sliced products) Given indexed families $P,Q:I \rightarrow B \rightarrow \mathcal {U}$ and a family of fibered equivalences $\prod _{i:I} \prod _{b:B} P_i \,b {\mathop {\longrightarrow }\limits ^{\simeq }} Q_i \,b$. Then the induced fibered functor

$$\begin{aligned} \times _{i:I}^B \varphi _i: \prod _{i:I} \prod _{b:B} \times _{i:I}^B P_i \,b \longrightarrow \times _{i:I}^B Q_i\,b \end{aligned}$$

between the sliced products over B is also a fibered equivalence.

Proof

As usual, denote for i :  by and the unstraightenings of the given fibered families, giving rise to a (strict) diagram:

Since weak equivalences are closed under taking dependent products, the induced fibered map $\prod _{i:I} \varphi _i: \prod _{i:I} E_i \rightarrow _{I \rightarrow B} \prod _{i:I} F_i$ is also a weak equivalence, and by right properness Lemma A.1 the desired mediating map is as well:

$\square$

Proposition A.3

For an indexing type I and a base Rezk type B, families of fibered equivalences between Rezk types over B are closed under taking sliced products, i.e. : Given a family of isoinner fibrations over B together with a fibered equivalence as below left, the induced maps on the right make up a fibered equivalence as well:

Proof

This is a consequence of Lemmas A.2 and A.3, considering the following diagram:

$\square$

Fibered (LARI) adjunctions

Building on previous work [67, Section 11] and [17, Appendix B] we provide a characterization of fibered LARI adjunctions along similar lines.

Theorem B.1

(Characterizations of fibered adjunctions, cf. [67, Theorem 11.23], [17, Theorem B.1.4]) Let B be a Rezk type. For $P,Q:B \rightarrow \mathcal {U}$ isoinner families we write and . Given a fibered functor $\varphi : E \rightarrow _B F$ such that (strictly)

the following are equivalent propositions:

• 1. The type of fibered left adjoints of $\varphi$, i.e. , fibered functors $\psi$ which are ordinary (transposing) left adjoints of $\varphi$ whose unit, moreover, is vertical.

• 2. The type of fibered functors $\psi :F \rightarrow _B E$ together with a vertical 2-cell $\eta : {{\,\textrm{id}\,}}_F \Rightarrow _B \varphi \psi$ s.t.

  

  is a fiberwise equivalence.

• 3. The type of sliced (or fiberwise) left adjoints (over B) to $\varphi$, i.e. , fibered functors $\psi :F \rightarrow _B E$ together with a fibered equivalence

  $$\begin{aligned} \psi \mathbin {\downarrow }_{B} E \simeq _{F \times _B E} F \mathbin {\downarrow }_{B} \varphi . \end{aligned}$$

• 4. The type of bi-diagrammatic fibered (or fiberwise) left adjoints, i.e. , fibered functors $\psi$ together with:

  • a vertical natural transformation $\eta : {{\,\textrm{id}\,}}_F \Rightarrow _B \varphi \psi$

  • two vertical natural transformations $\varepsilon , \varepsilon ': \psi \varphi \Rightarrow _B {{\,\textrm{id}\,}}_E$

  • homotopies³¹$\alpha : \varphi \varepsilon \circ \eta \varphi =_{E \rightarrow F} {{\,\textrm{id}\,}}_\varphi , ~\beta : \varepsilon ' \psi \circ \psi \eta =_{F \rightarrow E} {{\,\textrm{id}\,}}_\psi$

• 5. The type of fibered functors $\psi$ together with:

  • a vertical natural transformation $\eta : {{\,\textrm{id}\,}}_F \Rightarrow _B \varphi \psi$

  • two natural transformations $\varepsilon , \varepsilon ': \psi \varphi \Rightarrow {{\,\textrm{id}\,}}_E$

  • homotopies $\alpha : \varphi \varepsilon \circ \eta \varphi =_{E \rightarrow F} {{\,\textrm{id}\,}}_\varphi , ~\beta : \varepsilon ' \psi \circ \psi \eta =_{F \rightarrow E} {{\,\textrm{id}\,}}_\psi$

Proof

At first, we prove that, given a fixed and fibered functor $\psi :F \rightarrow _B E$ the respective witnessing data are propositions.³²

1 $\iff$ 5:

This follows from the equivalence between transposing left adjoint and bi-diagrammatic left adjoint data, cf. [67, Theorem 11.23].

4 $\implies$ 5:

This is clear since the latter is a weakening of the former.

5 $\implies$ 4:

Denoting the base component of $\varepsilon$ by $v:\varDelta ^1 \rightarrow (B \rightarrow B) \simeq B \rightarrow (\varDelta ^1 \rightarrow B)$, projecting down from $\alpha$ via $\xi$ we obtain the identity $\xi \alpha : v \circ {{\,\textrm{id}\,}}_B = {{\,\textrm{id}\,}}_B$. Thus $\varepsilon$ is vertical, and similarly one argues for $\varepsilon '$.

3 $\iff$ 4:

Given the fibered functor $\psi$, both lists of data witness that for every b : B the components $\psi _b \dashv \varphi _b: P\,b \rightarrow Q\,b$ define an adjunction between the fibers, again by [67, Theorem 11.23].

2 $\implies$ 3:

The latter is an instance of the former.

4 $\implies$ 2:

Using naturality and the triangle identities, we show that the fiberwise conditions (vertical case) can be lifted to the case of arbitrary arrows in the base.³³ Consider the transposing maps:

The first roundtrip yields:

The result yields back k using a triangle identity in the triangle on the left, and naturality of $\varepsilon$ in the square on the right:

In addition, we have also used naturality of $\varepsilon$ for $\psi _a \varepsilon _d \equiv \varepsilon _{\psi _a\,d}$. An analogous argument proves the other roundtrip.

We have proven, that relative to a fixed fibered functor $\psi : F \rightarrow _B E$ the different kinds of witnesses that this is a fibered left adjoint to $\varphi$ are equivalent propositions, giving rise to a predicate ${\textrm{isFibLAdj}}_\varphi : (F \rightarrow _B E) \rightarrow {\textrm{Prop}}$. What about the $\varSigma$-type as a whole? E.g. using the data from Item 3 (after conversion via [67, Theorem 11.23]), said type is equivalent to

$$\begin{aligned} {\textrm{FibLAdj}}_\varphi (\psi )&\simeq \sum _{\psi :\prod _{b:B} P\,b \rightarrow Q\,b} \sum _{\eta :\prod _{b:B} \prod _{d:Q\,b} \hom _{Q\,b}(d,(\varphi \,\psi )_b\,d)} \prod _{\begin{array}{c} b:B \\ d:Q\,b \\ e:P\,b \end{array}} {{\,\textrm{isEquiv}\,}}\big ( \lambda k.\varphi _b(k) \circ \eta _d\big ) \\&\simeq \prod _{\begin{array}{c} b:B \\ d:Q\,b \end{array}} \sum _{\psi _b:P\,b} \sum _{\eta _d:d \rightarrow _{Q\,b} \varphi _b(\psi _b d)} \prod _{e:P\,b} {{\,\textrm{isEquiv}\,}}(\lambda k.\varphi _b(k) \circ \eta _d). \end{aligned}$$

Finally, one shows that this is indeed a proposition, completely analogously to the argument given in the proof of [67, Theorem 11.23] for the non-dependent case. $\square$

Definition B.1

(Fibered (LARI) adjunction) Let B be a Rezk type and $\pi : E \twoheadrightarrow B$, $\xi :F \twoheadrightarrow B$ be isoinner fibrations, with and . Given a fibered functor $\varphi : E \rightarrow _B F$, the data of a fibered left adjoint right inverse (LARI) adjunction is given by

• a fibered functor $\psi : F \rightarrow _B E$,

• and an equivalence $\varPhi : \psi \mathbin {\downarrow }_{B} E \simeq _{F \times _B E} F \mathbin {\downarrow }_{B} \varphi$ s.t. the fibered unit

  

  is a componentwise homotopy.

Together, this defines the data of a fibered LARI adjunction. Diagrammatically, we represent this by:

In fact, as established in the previous works of [67, Section 11] the unit of a coherent adjunction is determined uniquely up to homotopy. Hence, using the characterizations of a (coherent) LARI adjunction, the type of fibered LARI adjunctions in the above sense is equivalent to the type of LARI adjunctions which are also fibered adjunctions. This implies the validity of the familiar closure properties for this restricted class as well.

Sliced commas and products

We record here explicitly some closure properties involving sliced commas and products that are often used, especially in the treatise of two-sided fibrations and related notions.

Proposition C.1

(Dependent products of sliced commas) For a type I and i : I, given fibered cospans

$$\begin{aligned} \psi _i: F_i \rightarrow _{B_i} G_i \leftarrow _{B_i} E_i: \varphi _i \end{aligned}$$

of Rezk types, taking the dependent product fiberwisely commutes with forming sliced comma types:

Proof

We denote by $P_i, Q_i, R_i: B_i \rightarrow \mathcal {U}$ the straightenings of the given maps $E_i \twoheadrightarrow B_i$, $F_i \twoheadrightarrow B_i$, and $G_i \twoheadrightarrow B_i$, resp. Using projection equivalence, the sliced commas are computed as

$$\begin{aligned} \psi _i \mathbin {\downarrow }_{B_i} \varphi _i \simeq \sum _{b:B_i} \sum _{\begin{array}{c} e:P_i(b) \\ d:Q_i(b) \end{array}} \big (\psi _i\big )_b(d) \longrightarrow _{R_i(b)} \big (\varphi _i\big )_b(e). \end{aligned}$$

(C.1)

From this and the type-theoretic axiom of choice, we obtain as projection equivalence for

$$\begin{aligned} \prod _{i:I} (\psi _i \downarrow _{B_i} \varphi _i) \twoheadrightarrow \prod _{i:I} B_i \end{aligned}$$

the type

$$\begin{aligned} \prod _{i:I} (\psi _i \downarrow _{B_i} \varphi _i)&{\mathop {\simeq }\limits ^{\text {(C.1)} }} \prod _{i:I} \sum _{b:B_i} \sum _{\begin{array}{c} e:P_i(b) \\ d:Q_i(b) \end{array}} \big (\psi _i\big )_b(d) \longrightarrow _{R_i(b)} \big (\varphi _i\big )_b(e) \\&{\mathop {\simeq }\limits ^{\text {(AC)}}} \sum _{\beta :\prod _{i:I} B_i} \prod _{i:I} \sum _{\begin{array}{c} e:P_i(\beta (i)) \\ d:Q_i(\beta (i)) \end{array}} \big (\psi _i\big )_{\beta (i)}(d) \longrightarrow _{R_i(\beta (i))} \big (\varphi _i\big )_{\beta (i)}(e) \\&{\mathop {\simeq }\limits ^{\text {(C.1)}}} \sum _{\beta :\prod _{i:I} B_i} \sum _{\begin{array}{c} \sigma :\prod _{i:I} P_i(\beta (i)) \\ \tau :\prod _{i:I} Q_i(\beta (i)) \end{array}} \big ( \prod _{i:I} \psi (\tau ) \big ) \rightarrow _{ \big ( \prod _{i:I} R_i(\beta (i))\big ) } \big ( \prod _{i:I} \varphi _i(\sigma )\big ) \\&{\mathop {\simeq }\limits ^{\text {(AC)}}} \left( \prod _{i:I} \psi _i \right) \downarrow _{\left( \prod _{i:I} B_i \right) } \left( \prod _{i:I} \varphi _i \right) \end{aligned}$$

This yields the desired fibered equivalence. $\square$

Corollary C.1

(Products of commas in a slice) Fix a base Rezk type B be and an indexing type I. Given for i : I an isoinner fibration $\pi _i:E_i \twoheadrightarrow B$ consider a cospan of isoinner fibrations $\psi _i: F_i \rightarrow E_i \leftarrow G_i: \varphi$. Then we have a fibered equivalence:

Proposition C.2

(Fibered (LARI) adjunctions are preserved by sliced products) For an indexing type I and a base Rezk type B, families of fibered (LARI) adjunctions between Rezk types over B are closed under taking sliced products, i.e. : Given a family of isoinner fibrations over B together with a fibered (LARI) adjunction as below left, the induced maps on the right make up a fibered (LARI) adjunction as well:

Proof

Given a family of fibered adjunctions as indicated amounts to a family of fibered equivalences, themselves fibered over B, for i : I:

Taking the dependent product over i : I produces a fibered equivalence, itself fibered over $B^I$. Pullback along $\textrm{cst}: B \rightarrow B^I$ yields the sliced products and again preserves the fibered equivalence:

Since sliced products canonically commute with both sliced commas and fiber products, this gives a fibered equivalence

which exactly yields the desired fibered adjunction of the sliced products. $\square$