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

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?

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

A displayed category $\mathcal{E}\mathcal{A}\times \mathcal{B}$ is a two-sided fibration when it satisfies the following 3 conditions:

1. We are given an operation assigning cartesian lifts ${\pi }_{u,Y}:{\mathcal{E}}_{u,\mathrm{id}}(u^{\ast }(Y),Y)$ to each $u:\mathcal{A}(A_1,A_2)\text{,}$ $B:\mathcal{B}\text{,}$ and $Y:{\mathcal{E}}_{A_2,B}\text{.}$

2. Similarly, to each $A:\mathcal{A},v:\mathcal{B}(B_1,B_2)$ and $X:{\mathcal{E}}_{A,B_1}\text{,}$ we are equipped with a cocartesian lift ${\iota }_{v,X}:{\mathcal{E}}_{\mathrm{id},v}(X,v_{!}(X))\text{.}$

3. For every diagram of the form below with $f$ cocartesian and $g$ cartesian, $h$ is cartesian if and only if $k$ is cocartesian.

  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}\text{:}$ the first acts contravariantly in $\mathcal{A}\text{,}$ the second covariantly in $\mathcal{B}\text{.}$ These are analogs to the actions $P(-,\mathrm{id})$ and $P(\mathrm{id},-)$ of a profunctor $P:\mathcal{A}\times \mathcal{B}\to \mathbf{Sets}\text{.}$ The final condition serves to ensure that the base change and cobase change functors $u^{\ast }:{\mathcal{E}}_{A_2,B}\to {\mathcal{E}}_{A_1,B}$ and $v_{!}:{\mathcal{E}}_{A,B_1}\to {\mathcal{E}}_{A,B_2}$ preserve cocartesian and cartesian morphisms, resp.