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 $\mathcal{E}\mathcal{A}\times \mathcal{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

1. For every $A:\mathcal{A}\text{,}$ $B:\mathcal{B}\text{,}$ the type ${\mathcal{E}}_{A,B}$ is a set.

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

2. For every $u:\mathcal{A}(A_1,A_2)$ and $Y:{\mathcal{E}}_{A_2,B}\text{,}$ there exists a unique pair $u^{\ast },{\pi }_{u,Y}$ that fits into the diagram below.

This condition provides us with a source of cartesian lifts, and ensures that the pullback of $\mathcal{E}$ along the functor $(-,B):\mathcal{A}\to \mathcal{A}\times \mathcal{B}$ is a discrete fibration for every $B:\mathcal{B}\text{.}$ In more intuitive terms, this means that $\mathcal{E}$ is a sort of “presheaf in $\mathcal{A}$”, as we can contravariantly reindex along morphisms in $\mathcal{A}\text{!}$

    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

3. For every $v:\mathcal{B}(B_1,B_2)$ and $X:{\mathcal{E}}_{A,B_1}\text{,}$ there exists a unique pair $v_{!}(X),{\iota }_{v,X}$ that fit into the following diagram.

This gives us a source of cocartesian lifts, and ensures that the pullback of $\mathcal{E}$ along the functor $(A,-):\mathcal{B}\to \mathcal{A}\times \mathcal{B}$ is a discrete opfibration.

    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

4. For every $f:{\mathcal{E}}_{u,v}(X,Y)\text{,}$ there exists a vertical map ${\alpha }_f:{\mathcal{E}}_{\mathrm{id},\mathrm{id}}(v_{!}(X),u^{\ast }(Y))$ that causes the following diagram to commute.

This condition is a bit opaque, and is best understood from the indexed point of view. From this perspective, our previous 2 conditions ensure that $\mathcal{E}$ is separately functorial in ${\mathcal{A}}^{\mathrm{op}}$ and $\mathcal{B}\text{;}$ there is no way to commute the two reindexing functors! To get something that is jointly functorial, we need to assert the existence of some extra lifts that allow us more room to manuever.

    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)

In particular, the existence of such vertical lifts ensure that the for every $f:{\mathcal{E}}_{u,v}(X,Y)\text{,}$ the lifts $u^{\ast }(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 ${\mathcal{E}}_{\mathrm{id},\mathrm{id}}(v_{!}(X),u^{\ast }(Y))\text{,}$ as the space of lifts of $u^{\ast }(Y)$ along $\mathrm{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:{\mathcal{E}}_{u,v}(X,Y)$ be a pair of morphisms. Both maps factor as ${\pi }_{u,Y}\circ {\alpha }_f\circ {\iota }_{v,X}$ and ${\pi }_{u,Y}\circ {\alpha }_g\circ {\iota }_{v,X}\text{,}$ so it suffices to show that ${\alpha }_f={\alpha }_g\text{.}$

    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),{\alpha }_f)=(v_{!}(X),{\alpha }_g)\text{,}$ 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 ${\mathcal{E}}_{u,v}(X,Y)$ are equivalent to proofs that $u^{\ast }(Y)=v_{!}(X)\text{.}$

    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 $(-{)}^{\ast }$ is functorial on the fibres of $E$ that are vertical over $B\text{,}$ 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 $A\text{.}$

    ^!-∘
      : ∀ {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:{\mathcal{E}}_{u,v}(X,Y)$ be a map displayed over a pair of invertible maps $u:\mathcal{A}(A_1,A_2),v:\mathcal{B}(B_1,B_2)\text{.}$

    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

Since each of our $\mathrm{Hom}\text{-sets}$ is a proposition, to construct an inverse it suffices to build a map ${\mathcal{E}}_{u^{-1},v^{-1}}(Y,X)\text{.}$ This, in turn, reduces to showing $(u^{-1}{)}^{\ast }(X)=(v^{-1}{)}_{!}(X)\text{,}$ 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 $\mathcal{B}\text{-vertical}$ is cartesian; and, dually, every map that is $\mathcal{A}\text{-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 _ _

    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\text{-vertical}$ map is cocartesian, and every $B\text{-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-beck-chevalley _ _ _ _ = vertical-cartesian _
    E-fib .cocart-beck-chevalley _ _ _ _ = vertical-cocartesian _