open import Cat.Displayed.Cocartesian
open import Cat.Displayed.Cartesian
open import Cat.Displayed.TwoSided
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.Discrete where

Discrete two-sided fibrations🔗

Much like how discrete fibrations are presheaves, a discrete two-sided fibration is a displayed presentation of a profunctor.

A displayed category $E A \times B$ is a discrete two-sided fibration if:

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
    module A×B = Cat.Reasoning (A ×ᶜ B)
    open Cat.Displayed.Reasoning E
    open Cat.Displayed.Morphism E
    open Displayed E

  record is-discrete-two-sided-fibration : Type (oa ⊔ ℓa ⊔ ob ⊔ ℓb ⊔ oe ⊔ ℓe) where

For every $A : A,$ $B : B,$ $E_{A, B}$ is a set.

    field
      fibre-set : ∀ a b → is-set (Ob[ a , b ])

For every $u : A (A_{1}, A_{2})$ and $Y : E_{A_{2}, B},$ there exists a unique pair $u^{*} (Y) : E_{A_{1}, B}, π_{u, Y} : E_{u, id} (u^{*} (Y), Y) .$

    field
      cart-lift
        : ∀ {a₁ a₂ : A.Ob} {b : B.Ob}
        → (f : A.Hom a₁ a₂)
        → (y' : Ob[ a₂ , b ])
        → is-contr (Σ[ x' ∈ Ob[ a₁ , b ] ] Hom[ f , B.id ] x' y')

    _^*_ : ∀ {a₁ a₂ : A.Ob} {b : B.Ob} → A.Hom a₁ a₂ → Ob[ a₂ , b ] → Ob[ a₁ , b ]
    u ^* y' = cart-lift u y' .centre .fst

    π*
      : ∀ {a₁ a₂ : A.Ob} {b : B.Ob}
      → (u : A.Hom a₁ a₂)
      → (y' : Ob[ a₂ , b ])
      → Hom[ u , B.id ] (u ^* y') y'
    π* u y' = cart-lift u y' .centre .snd

For every $v : B (B_{1}, B_{2})$ and $X : E_{A, B_{1}},$ there exists a unique pair $v_{!} (X) : E_{B, B_{2}}, ι_{v, X} : E_{id, v} (X, v_{!} (X)) .$

    field
      cocart-lift
        : ∀ {a : A.Ob} {b₁ b₂ : B.Ob}
        → (f : B.Hom b₁ b₂)
        → (x' : Ob[ a , b₁ ])
        → is-contr (Σ[ y' ∈ Ob[ a , b₂ ] ] Hom[ A.id , f ] x' y')
    _^!_ : ∀ {a : A.Ob} {b₁ b₂ : B.Ob} → B.Hom b₁ b₂ → Ob[ a , b₁ ] → Ob[ a , b₂ ]
    v ^! x' = cocart-lift v x' .centre .fst

    ι!
      : ∀ {a : A.Ob} {b₁ b₂ : B.Ob}
      → (v : B.Hom b₁ b₂)
      → (x' : Ob[ a , b₁ ])
      → Hom[ A.id , v ] x' (v ^! x')
    ι! v x' = cocart-lift v x' .centre .snd

For every $f : E_{u, v} (X, Y),$ there exists a vertical map $α_{f} : E_{id, id} (v_{!} (X), u^{*} (Y))$ such that $π_{u, Y} \circ α_{f} \circ ι_{v, X} = f .$

    field
      vert-lift
        : ∀ {a₁ a₂ b₁ b₂ x y}
        → {u : A.Hom a₁ a₂} {v : B.Hom b₁ b₂}
        → (f : Hom[ u , v ] x y)
        → Hom[ A.id , B.id ] (v ^! x) (u ^* y)
      factors
        : ∀ {a₁ a₂ b₁ b₂ x y}
        → {u : A.Hom a₁ a₂} {v : B.Hom b₁ b₂}
        → (f : Hom[ u , v ] x y)
        → f ≡[ A.intror (A.idl _) ,ₚ B.insertl (B.idl _) ] (π* u y ∘' vert-lift f ∘' ι! v x)

This final condition implies that for every $f : E_{u, v} (X, Y),$ the lifts $u^{*} (Y)$ and $v_{!} (X)$ coincide.

    same-lift
      : ∀ {a₁ a₂ b₁ b₂ x' y'} {u : A.Hom a₁ a₂} {v : B.Hom b₁ b₂}
      → (f : Hom[ u , v ] x' y')
      → u ^* y' ≡ v ^! x'

First, note that it suffices to construct a map $E_{id, id} (v_{!} (X), u^{*} (Y)),$ as the space of lifts of $u^{*} (Y)$ along $id$ is contractible. The above axiom ensures that this map exists!

    same-lift {x' = x'} {y' = y'} {u = u} {v = v} f =
       ap fst $ is-contr→is-prop (cart-lift A.id (u ^* y'))
         (u ^* y' , id')
         (v ^! x' , vert-lift f)

Moreover, the factorisation condition ensures that every hom set forms a proposition.

    Hom[]-is-prop
      : ∀ {a₁ a₂ b₁ b₂ x' y'} {u : A.Hom a₁ a₂} {v : B.Hom b₁ b₂}
      → is-prop (Hom[ u , v ] x' y')

Let $f, g : E_{u, v} (X, Y)$ be a pair of morphisms. Both maps factor as $π_{u, Y} \circ α_{f} \circ ι_{v, X}$ and $π_{u, Y} \circ α_{g} \circ ι_{v, X},$ so it suffices to show that $α_{f} = α_{g} .$

    Hom[]-is-prop {x' = x'} {y' = y'} {u = u} {v = v} f' g' =
      cast[] $
        f'                                     ≡[]⟨ factors f' ⟩
        π* u y' ∘' ⌜ vert-lift f' ⌝ ∘' ι! v x' ≡[]⟨ ap! vert-lift-eq ⟩
        π* u y' ∘' vert-lift g' ∘' ι! v x'     ≡[]˘⟨ factors g' ⟩
        g'                                     ∎

The type of objects is a set, so it further suffices to prove that $(v_{!} (X), α_{f}) = (v_{!} (X), α_{g}),$ which follows immediately from uniqueness of lifts.

      where
        vert-lift-eq : vert-lift f' ≡ vert-lift g'
        vert-lift-eq =
          Σ-inj-set (fibre-set _ _) $
          is-contr→is-prop (cart-lift A.id (u ^* y'))
            (v ^! x' , vert-lift f')
            (v ^! x' , vert-lift g')

An alternative view is that these final conditions ensure that morphisms $E_{u, v} (X, Y)$ are equivalent to proofs that $u^{*} (Y) = v_{!} (X) .$

    opaque
      discrete-two-sided-hom
        : ∀ {a₁ a₂ b₁ b₂ x' y'}
        → (u : A.Hom a₁ a₂) (v : B.Hom b₁ b₂)
        → (u ^* y') ≡ (v ^! x')
        → Hom[ u , v ] x' y'
      discrete-two-sided-hom {x' = x'} {y' = y'} u v p =
        hom[ A.elimr (A.idr _) ,ₚ B.cancell (B.idl _) ] $
          π* u y' ∘' subst (λ v!x → Hom[ A.id , B.id ] v!x (u ^* y')) p id' ∘' ι! v x'

    discrete-two-sided-hom-is-equiv
      : ∀ {a₁ a₂ b₁ b₂ x' y'}
      → (u : A.Hom a₁ a₂) (v : B.Hom b₁ b₂)
      → is-equiv (discrete-two-sided-hom {x' = x'} {y' = y'} u v)
    discrete-two-sided-hom-is-equiv u v =
      is-iso→is-equiv $
      iso same-lift
        (λ _ → Hom[]-is-prop _ _)
        (λ _ → fibre-set _ _ _ _ _ _)

Functoriality🔗

Note that the action $(-)^{*}$ is functorial on the fibres of $E$ that are vertical over $B,$ as lifts are unique.

    ^*-∘
      : ∀ {a₁ a₂ a₃ : A.Ob} {b : B.Ob}
      → (u : A.Hom a₂ a₃) (v : A.Hom a₁ a₂)
      → (y' : Ob[ a₃ , b ])
      → (u A.∘ v) ^* y' ≡ (v ^* (u ^* y'))
    ^*-∘ u v y' =
      ap fst $ cart-lift (u A.∘ v) y' .paths $
        v ^* (u ^* y') ,
        hom[ refl ,ₚ B.idl _ ] (π* u y' ∘' π* v (u ^* y'))

    ^*-id
      : ∀ {a b} {x' : Ob[ a , b ]}
      → A.id ^* x' ≡ x'
    ^*-id {x' = x'} =
      ap fst $ cart-lift A.id x' .paths (x' , id')

Dually, the action $(-)_{!}$ is functorial on the fibres of $E$ that are vertical over $B .$

    ^!-∘
      : ∀ {a : A.Ob} {b₁ b₂ b₃ : B.Ob}
      → (u : B.Hom b₂ b₃) (v : B.Hom b₁ b₂)
      → (x' : Ob[ a , b₁ ])
      → (u B.∘ v) ^! x' ≡ (u ^! (v ^! x'))
    ^!-∘ u v x' =
      ap fst $ cocart-lift (u B.∘ v) x' .paths $
        u ^! (v ^! x') , hom[ A.idr _ ,ₚ refl ] (ι! u (v ^! x') ∘' ι! v x')

    ^!-id
      : ∀ {a b} {x' : Ob[ a , b ]}
      → B.id ^! x' ≡ x'
    ^!-id {x' = x'} =
      ap fst $ cocart-lift B.id x' .paths (x' , id')

Moreover, we also have an interchange law that lets us relate the contravariant and covariant actions on fibres.

    ^*-^!-comm
      : ∀ {a₁ a₂ : A.Ob} {b₁ b₂ : B.Ob}
      → (u : A.Hom a₁ a₂) (v : B.Hom b₁ b₂)
      → (x' : Ob[ a₂ , b₁ ])
      → (u ^* (v ^! x')) ≡ (v ^! (u ^* x'))
    ^*-^!-comm u v x' =
      same-lift (hom[ A.idl u ,ₚ B.idr v ] (ι! v x' ∘' π* u x'))

Invertible maps🔗

Every morphism in a discrete two-sided fibration living over an invertible pair of morphisms is itself invertible.

    all-invertible[]
      : ∀ {a₁ a₂ b₁ b₂ x' y'} {u : A.Hom a₁ a₂} {v : B.Hom b₁ b₂}
      → (f : Hom[ u , v ] x' y')
      → (uv⁻¹ : A×B.is-invertible (u , v))
      → is-invertible[ uv⁻¹ ] f

Let $f : E_{u, v} (X, Y)$ be a map displayed over a pair of invertible maps $u : A (A_{1}, A_{2}), v : B (B_{1}, B_{2}) .$

    all-invertible[] {a₁} {a₂} {b₁} {b₂} {x'} {y'} {u} {v} f uv⁻¹ = f⁻¹ where
      module uv⁻¹ = A×B.is-invertible uv⁻¹
      open is-invertible[_]

      u⁻¹ : A.Hom _ _
      u⁻¹ = uv⁻¹.inv .fst

      v⁻¹ : B.Hom _ _
      v⁻¹ = uv⁻¹.inv .snd

All of our Hom sets are propositional, so constructing an inverse only requires us to build a map $E_{u^{- 1}, v^{- 1}} (Y, X) .$ Moreover, it suffices to prove that $(u^{- 1})^{*} (X) = (v^{- 1})_{!} (X),$ which follows from some tedious functoriality algebra.

      f⁻¹ : is-invertible[ uv⁻¹ ] f
      f⁻¹ .inv' =
        discrete-two-sided-hom u⁻¹ v⁻¹ $
          u⁻¹ ^* x'                    ≡˘⟨ ap (u⁻¹ ^*_) ^!-id ⟩
          u⁻¹ ^* (⌜ B.id ⌝ ^! x')      ≡⟨ ap! (sym (ap snd $ uv⁻¹.invr)) ⟩
          u⁻¹ ^* ((v⁻¹ B.∘ v) ^! x')   ≡⟨ ap (u⁻¹ ^*_) (^!-∘ v⁻¹ v x') ⟩
          u⁻¹ ^* (v⁻¹ ^! ⌜ v ^! x' ⌝)  ≡⟨ ap! (sym (same-lift f)) ⟩
          u⁻¹ ^* (v⁻¹ ^! (u ^* y'))    ≡˘⟨ ap (u⁻¹ ^*_) (^*-^!-comm u v⁻¹ y') ⟩
          u⁻¹ ^* (u ^* (v⁻¹ ^! y'))    ≡˘⟨ ^*-∘ u u⁻¹ (v⁻¹ ^! y') ⟩
          ⌜ u A.∘ u⁻¹ ⌝ ^* (v⁻¹ ^! y') ≡⟨ ap! (ap fst $ uv⁻¹.invl) ⟩
          A.id ^* (v⁻¹ ^! y')          ≡⟨ ^*-id ⟩
          v⁻¹ ^! y' ∎
      f⁻¹ .inverses' .Inverses[_].invl' =
        is-prop→pathp (λ _ → Hom[]-is-prop) _ _
      f⁻¹ .inverses' .Inverses[_].invr' =
        is-prop→pathp (λ _ → Hom[]-is-prop) _ _

Cartesian and cocartesian maps🔗

Every map that is $B -vertical$ is cartesian and every map that is $A -vertical$ is cocartesian.

    vertical-cartesian
      : ∀ {a₁ a₂ b x' y'} {u : A.Hom a₁ a₂}
      → (f : Hom[ u , B.id {b} ] x' y')
      → is-cartesian E (u , B.id) f

    vertical-cocartesian
      : ∀ {a b₁ b₂ x' y'} {v : B.Hom b₁ b₂}
      → (f : Hom[ A.id {a} , v ] x' y')
      → is-cocartesian E (A.id , v) f

The proof is a bit more functoriality algebra.

    vertical-cartesian {x' = x'} {y'} {u} f .is-cartesian.universal {_} {a'} (v , w) h =
      discrete-two-sided-hom v w $
        v ^* x'            ≡˘⟨ ap (v ^*_) ^!-id ⟩
        v ^* (B.id ^! x')  ≡˘⟨ ap (v ^*_) (same-lift f) ⟩
        v ^* (u ^* y')     ≡˘⟨ ^*-∘ u v y' ⟩
        (u A.∘ v) ^* y'    ≡⟨ same-lift h ⟩
        (B.id B.∘ w) ^! a' ≡⟨ ap (_^! a') (B.idl w) ⟩
        w ^! a'            ∎
    vertical-cartesian {x' = x'} {y'} {u} f .is-cartesian.commutes _ _ =
      Hom[]-is-prop _ _
    vertical-cartesian {x' = x'} {y'} {u} f .is-cartesian.unique _ _ =
      Hom[]-is-prop _ _

The cocartesian case is formally dual, so we omit the details.

    vertical-cocartesian {x' = x'} {y'} {v} f .is-cocartesian.universal {_} {a'} (u , w) h =
      discrete-two-sided-hom u w $
        u ^* a'            ≡˘⟨ ap (_^* a') (A.idr _) ⟩
        (u A.∘ A.id) ^* a' ≡⟨ same-lift h ⟩
        (w B.∘ v) ^! x'    ≡⟨ ^!-∘ w v x' ⟩
        w ^! (v ^! x')     ≡˘⟨ ap (w ^!_) (same-lift f) ⟩
        w ^! (A.id ^* y')  ≡⟨ ap (w ^!_) ^*-id ⟩
        w ^! y'            ∎
    vertical-cocartesian {x' = x'} {y'} {v} f .is-cocartesian.commutes _ _ =
      Hom[]-is-prop _ _
    vertical-cocartesian {x' = x'} {y'} {v} f .is-cocartesian.unique _ _ =
      Hom[]-is-prop _ _

Discrete two-sided fibrations are two-sided fibrations🔗

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

Every discrete two-sided fibration is a two-sided fibration.

  discrete-two-sided-fibration→two-sided-fibration
    : is-discrete-two-sided-fibration E
    → Two-sided-fibration E

This is essentially a triviality at this point: every $A -vertical$ map is cocartesian, and every $B -vertical$ map is cartesian, and all requisite lifts exit.

  discrete-two-sided-fibration→two-sided-fibration E-dfib = E-fib where
    open is-discrete-two-sided-fibration E-dfib
    open Two-sided-fibration
    open Cocartesian-lift
    open Cartesian-lift

    E-fib : Two-sided-fibration E
    E-fib .cart-lift u y' .x' = u ^* y'
    E-fib .cart-lift u y' .lifting = π* u y'
    E-fib .cart-lift u y' .cartesian = vertical-cartesian (π* u y')
    E-fib .cocart-lift v x' .y' = v ^! x'
    E-fib .cocart-lift v x' .lifting = ι! v x'
    E-fib .cocart-lift v x' .cocartesian = vertical-cocartesian (ι! v x')
    E-fib .cart-cocart-commute p f-cocart g-cart ._↔_.to _ =
      vertical-cocartesian _
    E-fib .cart-cocart-commute p f-cocart g-cart ._↔_.from _ =
      vertical-cartesian _