Two-sided fibrations (the1lab#456)

# Description

This PR defines two-sided fibrations and two-sided discrete fibrations,
and proves that the comma category is a two-sided discrete fibration
when regarded as a displayed category.

## Checklist

Before submitting a merge request, please check the items below:

- [x] I've read [the contributing
guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md).
- [x] The imports of new modules have been sorted with
`support/sort-imports.hs` (or `nix run --experimental-features
nix-command -f . sort-imports`).
- [x] All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content,
and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title
with `chore:`.

---------

Co-authored-by: Amélia <[email protected]>

Author: TOTBWF

src/Cat/Displayed/Cartesian/Discrete.lagda.md

@@ -29,7 +29,7 @@ open is-cartesian
 ```
 -->
 
-# Discrete fibrations
+# Discrete fibrations {defines="discrete-fibration"}
 
 A **discrete fibration** is a [[displayed category]] whose [[fibre
 categories]] are all _discrete categories_: thin, univalent groupoids.
@@ -203,7 +203,7 @@ that every vertical morphism in a discrete fibration is invertible.
       x''≡x' = ap fst (discrete→vertical-id disc (x' , f'))
 ```
 
-## Discrete fibrations are presheaves
+## Discrete fibrations are presheaves {defines="discrete-fibrations-are-presheaves"}
 
 As noted earlier, a discrete fibration over $\cB$ encodes the same
 data as a presheaf on $\cB$. First, let us show that we can construct

src/Cat/Displayed/Cocartesian.lagda.md

@@ -384,7 +384,7 @@ cocartesian→precompose-equiv cocart =
 ```
 
 
-## Cocartesian lifts
+## Cocartesian lifts {defines="cocartesian-lift"}
 
 We call an object $b'$ over $b$ together with a cartesian arrow
 $f' : a \to_{f} b'$ a **cocartesian lift** of $f$.

src/Cat/Displayed/Instances/Comma.lagda.md

@@ -0,0 +1,190 @@
+---
+description: |
+  Comma categories as two-sided displayed categories.
+---
+<!--
+```agda
+open import Cat.Displayed.TwoSided.Discrete
+open import Cat.Displayed.Cocartesian
+open import Cat.Displayed.Cartesian
+open import Cat.Instances.Product
+open import Cat.Displayed.Base
+open import Cat.Prelude
+
+import Cat.Functor.Reasoning
+import Cat.Reasoning
+```
+-->
+```agda
+module Cat.Displayed.Instances.Comma where
+```
+
+# Comma categories as displayed categories
+
+We can neatly present [[comma categories]] as categories displayed over
+product categories.
+
+<!--
+```agda
+module _
+  {oa ℓa ob ℓb oc ℓc}
+  {A : Precategory oa ℓa}
+  {B : Precategory ob ℓb}
+  {C : Precategory oc ℓc}
+  (F : Functor A C)
+  (G : Functor B C)
+  where
+  private
+    module A = Cat.Reasoning A
+    module B = Cat.Reasoning B
+    module C = Cat.Reasoning C
+    module F = Cat.Functor.Reasoning F
+    module G = Cat.Functor.Reasoning G
+
+  open Displayed
+```
+-->
+
+```agda
+  Comma : Displayed (A ×ᶜ B) ℓc ℓc
+  Comma .Ob[_] (a , b) = C.Hom (F.₀ a) (G.₀ b)
+  Comma .Hom[_] (u , v) f g = G.₁ v C.∘ f ≡ g C.∘ F.₁ u
+  Comma .Hom[_]-set _ _ _ = hlevel 2
+  Comma .id' = C.eliml G.F-id ∙ C.intror F.F-id
+  Comma ._∘'_ α β = G.popr β ∙ sym (F.shufflel (sym α))
+  Comma .idr' _ = prop!
+  Comma .idl' _ = prop!
+  Comma .assoc' _ _ _ = prop!
+```
+
+## Comma categories are discrete two-sided fibrations
+
+<!--
+```agda
+module _
+  {oa ℓa ob ℓb oc ℓc}
+  {A : Precategory oa ℓa}
+  {B : Precategory ob ℓb}
+  {C : Precategory oc ℓc}
+  {F : Functor A C}
+  {G : Functor B C}
+  where
+  private
+    module A = Cat.Reasoning A
+    module B = Cat.Reasoning B
+    module C = Cat.Reasoning C
+    module F = Cat.Functor.Reasoning F
+    module G = Cat.Functor.Reasoning G
+
+  open is-discrete-two-sided-fibration
+  open Displayed
+```
+-->
+
+Comma categories are [[discrete two-sided fibrations]].
+
+```agda
+  Comma-is-discrete-two-sided-fibration
+    : is-discrete-two-sided-fibration (Comma F G)
+  Comma-is-discrete-two-sided-fibration .fibre-set _ _ = hlevel 2
+  Comma-is-discrete-two-sided-fibration .cart-lift f g .centre =
+    g C.∘ F.₁ f , C.eliml G.F-id
+  Comma-is-discrete-two-sided-fibration .cart-lift f g .paths (h , p) =
+    Σ-prop-path! (sym p ∙ C.eliml G.F-id)
+  Comma-is-discrete-two-sided-fibration .cocart-lift f g .centre =
+    G.₁ f C.∘ g , C.intror F.F-id
+  Comma-is-discrete-two-sided-fibration .cocart-lift f g .paths (h , p) =
+    Σ-prop-path! (p ∙ C.elimr F.F-id)
+  Comma-is-discrete-two-sided-fibration .vert-lift {x = f} {y = g} {u = h} {v = k} p =
+    G.F₁ B.id C.∘ G.F₁ k C.∘ f   ≡⟨ C.eliml G.F-id ⟩
+    G.F₁ k C.∘ f                 ≡⟨ p ⟩
+    g C.∘ F.₁ h                  ≡⟨ C.intror F.F-id ⟩
+    (g C.∘ F.F₁ h) C.∘ F.F₁ A.id ∎
+  Comma-is-discrete-two-sided-fibration .factors _ = prop!
+```
+
+Every *$B$-vertical* morphism in a discrete two-sided fibration is [[cartesian|cartesian morphism]],
+but this is not neccesarily true of *every* morphism. In our setting,
+the cartesian maps are given by squares that satisfy the following
+pasting property: for every (potentially non-commutative) square of the below
+form, if the overall rectangle commutes, then the upper square commutes.
+
+~~~{.quiver}
+\begin{tikzcd}
+  F(A) && G(Y) \\
+  \\
+  F(W) && G(Y) \\
+  \\
+  F(X) && G(Z)
+  \arrow["h", from=1-1, to=1-3]
+  \arrow["F(j)"', from=1-1, to=3-1]
+  \arrow["G(k)", from=1-3, to=3-3]
+  \arrow["f", from=3-1, to=3-3]
+  \arrow["F(u)"', from=3-1, to=5-1]
+  \arrow["G(v)", from=3-3, to=5-3]
+  \arrow["g"', from=5-1, to=5-3]
+\end{tikzcd}
+~~~
+
+```agda
+  pasting→comma-cartesian
+    : ∀ {w x y z} {u : A.Hom w x} {v : B.Hom y z} {f : C.Hom (F.₀ w) (G.₀ y)} {g : C.Hom (F.₀ x) (G.₀ z)}
+    → (p : G.₁ v C.∘ f ≡ g C.∘ F.₁ u)
+    → (∀ {a b} {h : C.Hom (F.₀ a) (G.₀ b)} {j : A.Hom a w} {k : B.Hom b y}
+       → G.₁ v C.∘ G.₁ k C.∘ h ≡ g C.∘ F.₁ u C.∘ F.₁ j
+       → G.₁ k C.∘ h ≡ f C.∘ F.₁ j)
+    → is-cartesian (Comma F G) (u , v) p
+  pasting→comma-cartesian p paste .is-cartesian.universal _ outer =
+    paste (C.pulll (sym $ G.F-∘ _ _) ·· outer ·· ap₂ C._∘_ refl (F.F-∘ _ _))
+  pasting→comma-cartesian p paste .is-cartesian.commutes _ _ = prop!
+  pasting→comma-cartesian p paste .is-cartesian.unique _ _ = prop!
+
+  comma-cartesian→pasting
+    : ∀ {w x y z} {u : A.Hom w x} {v : B.Hom y z} {f : C.Hom (F.₀ w) (G.₀ y)} {g : C.Hom (F.₀ x) (G.₀ z)}
+    → (p : G.₁ v C.∘ f ≡ g C.∘ F.₁ u)
+    → is-cartesian (Comma F G) (u , v) p
+    → ∀ {a b} {h : C.Hom (F.₀ a) (G.₀ b)} {j : A.Hom a w} {k : B.Hom b y}
+       → G.₁ v C.∘ G.₁ k C.∘ h ≡ g C.∘ F.₁ u C.∘ F.₁ j
+       → G.₁ k C.∘ h ≡ f C.∘ F.₁ j
+  comma-cartesian→pasting p p-cart outer =
+    is-cartesian.universal p-cart _ $
+      C.pushl (G.F-∘ _ _) ·· outer ·· ap₂ C._∘_ refl (sym $ F.F-∘ _ _)
+```
+
+Moreover, a square is [[cocartesian|cocartesian-morphism]] when it satisfies
+the dual pasting lemma.
+
+```agda
+  pasting→comma-cocartesian
+    : ∀ {w x y z} {u : A.Hom w x} {v : B.Hom y z} {f : C.Hom (F.₀ w) (G.₀ y)} {g : C.Hom (F.₀ x) (G.₀ z)}
+    → (p : G.₁ v C.∘ f ≡ g C.∘ F.₁ u)
+    → (∀ {a b} {h : C.Hom (F.₀ a) (G.₀ b)} {j : A.Hom x a} {k : B.Hom z b}
+        → G.₁ k C.∘ G.₁ v C.∘ f ≡ h C.∘ F.₁ j C.∘ F.₁ u
+        → G.₁ k C.∘ g ≡ h C.∘ F.₁ j)
+    → is-cocartesian (Comma F G) (u , v) p
+
+  comma-cocartesian→pasting
+    : ∀ {w x y z} {u : A.Hom w x} {v : B.Hom y z} {f : C.Hom (F.₀ w) (G.₀ y)} {g : C.Hom (F.₀ x) (G.₀ z)}
+    → (p : G.₁ v C.∘ f ≡ g C.∘ F.₁ u)
+    → is-cocartesian (Comma F G) (u , v) p
+    → ∀ {a b} {h : C.Hom (F.₀ a) (G.₀ b)} {j : A.Hom x a} {k : B.Hom z b}
+        → G.₁ k C.∘ G.₁ v C.∘ f ≡ h C.∘ F.₁ j C.∘ F.₁ u
+        → G.₁ k C.∘ g ≡ h C.∘ F.₁ j
+
+```
+
+<details>
+<summary>The proofs are formally dual, so we omit them.
+</summary>
+
+```agda
+  pasting→comma-cocartesian p paste .is-cocartesian.universal _ outer =
+    paste (C.pulll (sym $ G.F-∘ _ _) ·· outer ·· ap₂ C._∘_ refl (F.F-∘ _ _))
+  pasting→comma-cocartesian p paste .is-cocartesian.commutes _ _ = prop!
+  pasting→comma-cocartesian p paste .is-cocartesian.unique _ _ = prop!
+
+  comma-cocartesian→pasting p p-cocart outer =
+    is-cocartesian.universal p-cocart _ $
+      C.pushl (G.F-∘ _ _) ·· outer ·· ap₂ C._∘_ refl (sym $ F.F-∘ _ _)
+```
+</details>

src/Cat/Displayed/TwoSided.lagda.md

@@ -0,0 +1,116 @@
+---
+description: |
+  Two-sided fibrations.
+---
+<!--
+```agda
+open import Cat.Displayed.BeckChevalley
+open import Cat.Displayed.Cocartesian
+open import Cat.Displayed.Cartesian
+open import Cat.Instances.Product
+open import Cat.Displayed.Base
+open import Cat.Prelude
+
+import Cat.Displayed.Reasoning
+import Cat.Displayed.Morphism
+import Cat.Reasoning
+```
+-->
+```agda
+module Cat.Displayed.TwoSided where
+```
+
+# Two-sided fibrations
+
+One useful perspective on [[cartesian fibrations]] and [[cocartesian fibrations]]
+is that they are (co)presheaves of categories. This raises a natural question: what
+is the appropriate generalization of profunctors?
+
+<!--
+```agda
+module _
+  {oa ℓa ob ℓb oe ℓe}
+  {A : Precategory oa ℓa} {B : Precategory ob ℓb}
+  (E : Displayed (A ×ᶜ B) oe ℓe)
+  where
+  private
+    module A = Cat.Reasoning A
+    module B = Cat.Reasoning B
+    open Cat.Displayed.Reasoning E
+    open Cat.Displayed.Morphism E
+    open Displayed E
+```
+-->
+
+:::{.definition #two-sided-fibration}
+A displayed category $\cE \liesover \cA \times \cB$ is a **two-sided fibration**
+when it satisfies the following 3 conditions:
+
+1. We are given an operation assigning [[cartesian lifts]]
+$\pi_{u, Y} : \cE_{u, \id}(u^{*}(Y), Y)$ to each $u : \cA(A_1, A_2)$, $B : \cB$, and $Y : \cE_{A_2, B}$.
+
+2. Similarly, to each $A : \cA, v : \cB(B_1, B_2)$ and $X : \cE_{A, B_1}$,
+we are equipped with a [[cocartesian lift]] $\iota_{v, X} : \cE_{\id, v}(X, v_{!}(X))$.
+
+3. For every diagram of the form below with $f$ cocartesian and $g$ cartesian,
+$h$ is cartesian if and only if $k$ is cocartesian.
+
+~~~{.quiver}
+\begin{tikzcd}
+  W && X \\
+  & Y && Z \\
+  {(A_1, B_1)} && {(A_2, B_1)} \\
+  & {(A_1, B_2)} && {(A_2, B_2)}
+  \arrow["g", from=1-1, to=1-3]
+  \arrow["k", from=1-1, to=2-2]
+  \arrow[from=1-1, to=3-1]
+  \arrow["f", from=1-3, to=2-4]
+  \arrow[from=1-3, to=3-3]
+  \arrow["h"{pos=0.3}, from=2-2, to=2-4]
+  \arrow[from=2-2, to=4-2]
+  \arrow[from=2-4, to=4-4]
+  \arrow["{(u,\id)}"{pos=0.7}, from=3-1, to=3-3]
+  \arrow["{(\id, v)}"', from=3-1, to=4-2]
+  \arrow["{(\id, v)}", from=3-3, to=4-4]
+  \arrow["{(u,\id)}"', from=4-2, to=4-4]
+\end{tikzcd}
+~~~
+:::
+
+
+```agda
+  record Two-sided-fibration : Type (oa ⊔ ℓa ⊔ ob ⊔ ℓb ⊔ oe ⊔ ℓe) where
+    no-eta-equality
+    field
+      cart-lift
+        : ∀ {a₁ a₂ : A.Ob} {b : B.Ob}
+        → (u : A.Hom a₁ a₂)
+        → (y' : Ob[ a₂ , b ])
+        → Cartesian-lift E (u , B.id) y'
+      cocart-lift
+        : ∀ {a : A.Ob} {b₁ b₂ : B.Ob}
+        → (v : B.Hom b₁ b₂)
+        → (x' : Ob[ a , b₁ ])
+        → Cocartesian-lift E (A.id , v) x'
+      cart-beck-chevalley
+        : ∀ {a₁ a₂ : A.Ob} {b₁ b₂ : B.Ob}
+        → {u : A.Hom a₁ a₂} {v : B.Hom b₁ b₂}
+        → right-beck-chevalley E
+            (A.id , v) (u , B.id) (u , B.id) (A.id , v)
+            (sym A.id-comm ,ₚ B.id-comm)
+      cocart-beck-chevalley
+        : ∀ {a₁ a₂ : A.Ob} {b₁ b₂ : B.Ob}
+        → {u : A.Hom a₁ a₂} {v : B.Hom b₁ b₂}
+        → left-beck-chevalley E
+            (A.id , v) (u , B.id) (u , B.id) (A.id , v)
+            (sym A.id-comm ,ₚ B.id-comm)
+```
+
+This definition is rather opaque, so let's break it down. The first two
+conditions ensure that we have 2 functorial actions on each of the [[fibre categories]]
+$E_{a, b}$: the first acts contravariantly in $\cA$, the second covariantly
+in $\cB$. These are analogs to the actions $P(-, \id)$ and $P(\id, -)$ of
+a profunctor $P : \cA \times \cB \to \Sets$. The final condition serves to
+ensure that the [[base change]] and [[cobase change]] functors
+$u^{*} : \cE_{A_2, B} \to \cE_{A_1, B}$ and $v_{!} : \cE_{A, B_1} \to \cE_{A, B_2}$
+preserve cocartesian and cartesian morphisms, resp.