open import Cat.Displayed.Cartesian
open import Cat.Displayed.Total.Op
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Morphism.Duality
import Cat.Displayed.Reasoning as DR
import Cat.Displayed.Morphism
import Cat.Reasoning

module Cat.Displayed.Cocartesian
  {o ℓ o' ℓ'} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o' ℓ') where

open Cat.Reasoning ℬ
open Displayed ℰ
open Cat.Displayed.Morphism ℰ
open Cat.Displayed.Morphism.Duality ℰ
open DR ℰ

Cocartesian morphisms and opfibrations🔗

Cartesian fibrations provide a way of describing pseudofunctorial families of categories $B^{o p} \to Cat$ purely in terms of displayed structure. It’s then natural to ask: what about covariant pseudofunctorial families of categories? Such pseudofunctors can be encoded by dualising cartesian fibrations.

To do this, we must first dualise the notion of a cartesian map to a cocartesian map. Fix a map $a \to b$ in $B,$ objects $a^{'}$ and $b^{'}$ displayed over $a$ and $b$ resp., and a map $f^{'} : a^{'} \to_{f} b^{'}$ over $f .$ We say that $f^{'}$ is cocartesian if it has the shape of a “pushout diagram”, in contrast to the “pullback diagrams” shape associated with cartesian maps.

record is-cocartesian
  {a b a' b'} (f : Hom a b) (f' : Hom[ f ] a' b')
  : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ')
  where
  no-eta-equality

Concretely, let $u : B$ and $u^{'}$ be displayed over $u .$ Furthermore, suppose we have a map $m : b \to u$ (highlighted in violet below), along with a map $h^{'} : a^{'} \to_{m f} u^{'}$ displayed over $m \cdot f$ (highlighted in red). For $f^{'}$ to be cocartesian, every such situation must give rise to a unique universal factorisation of $h^{'}$ through a map $b^{'} \to_{m} u^{'}$ (highlighted in green).

  field
    universal
      : ∀ {u u'} (m : Hom b u) (h' : Hom[ m ∘ f ] a' u')
      → Hom[ m ] b' u'
    commutes
      : ∀ {u u'} (m : Hom b u) (h' : Hom[ m ∘ f ] a' u')
      → universal m h' ∘' f' ≡ h'
    unique
      : ∀ {u u'} {m : Hom b u} {h' : Hom[ m ∘ f ] a' u'}
      → (m' : Hom[ m ] b' u') → m' ∘' f' ≡ h'
      → m' ≡ universal m h'

  universal' : ∀ {u u'} {m : Hom b u} {k : Hom a u}
             → (p : m ∘ f ≡ k) (h' : Hom[ k ] a' u')
             → Hom[ m ] b' u'
  universal' {u' = u'} p h' = universal _ (coe1→0 (λ i → Hom[ p i ] a' u') h')

  commutesp : ∀ {u u'} {m : Hom b u} {k : Hom a u}
            → (p : m ∘ f ≡ k) (h' : Hom[ k ] a' u')
            → universal' p h' ∘' f' ≡[ p ] h'
  commutesp {u' = u'} p h' =
    to-pathp⁻ (commutes _ (coe1→0 (λ i → Hom[ p i ] a' u') h'))

  universalp : ∀ {u u'} {m₁ m₂ : Hom b u} {k : Hom a u}
             → (p : m₁ ∘ f ≡ k) (q : m₁ ≡ m₂) (r : m₂ ∘ f ≡ k)
             → (h' : Hom[ k ] a' u')
             → universal' p h' ≡[ q ] universal' r h'
  universalp {u = u} p q r h' i =
    universal' (is-set→squarep (λ _ _ → Hom-set a u) (ap (_∘ f) q) p r refl i) h'

  uniquep : ∀ {u u'} {m₁ m₂ : Hom b u} {k : Hom a u}
          → (p : m₁ ∘ f ≡ k) (q : m₁ ≡ m₂) (r : m₂ ∘ f ≡ k)
          → {h' : Hom[ k ] a' u'}
          → (m' : Hom[ m₁ ] b' u')
          → m' ∘' f' ≡[ p ] h' → m' ≡[ q ] universal' r h'
  uniquep p q r {h' = h'} m' s  =
    to-pathp⁻ (unique m' (from-pathp⁻ s) ∙ from-pathp⁻ (universalp p q r h'))

  uniquep₂ : ∀ {u u'} {m₁ m₂ : Hom b u} {k : Hom a u}
          → (p : m₁ ∘ f ≡ k) (q : m₁ ≡ m₂) (r : m₂ ∘ f ≡ k)
          → {h' : Hom[ k ] a' u'}
          → (m₁' : Hom[ m₁ ] b' u')
          → (m₂' : Hom[ m₂ ] b' u')
          → m₁' ∘' f' ≡[ p ] h'
          → m₂' ∘' f' ≡[ r ] h'
          → m₁' ≡[ q ] m₂'
  uniquep₂ p q r {h' = h'} m₁' m₂' α β = to-pathp⁻ $
       unique m₁' (from-pathp⁻ α)
    ·· from-pathp⁻ (universalp p q r _)
    ·· ap hom[] (sym (unique m₂' (from-pathp⁻ β)))

  universalv : ∀ {b''} (f'' : Hom[ f ] a' b'') → Hom[ id ] b' b''
  universalv f'' = universal' (idl _) f''

  commutesv
    : ∀ {x'} (g' : Hom[ f ] a' x')
    → universalv g' ∘' f' ≡[ idl _ ] g'
  commutesv = commutesp (idl _)

  uniquev
    : ∀ {x'} {g' : Hom[ f ] a' x'}
    → (h' : Hom[ id ] b' x')
    → h' ∘' f' ≡[ idl _ ] g'
    → h' ≡ universalv g'
  uniquev h' p = uniquep (idl _) refl (idl _) h' p

  uniquev₂
    : ∀ {x'} {g' : Hom[ f ] a' x'}
    → (h' h'' : Hom[ id ] b' x')
    → h' ∘' f' ≡[ idl _ ] g'
    → h'' ∘' f' ≡[ idl _ ] g'
    → h' ≡ h''
  uniquev₂ h' h'' p q = uniquep₂ (idl _) refl (idl _) h' h'' p q

record Cocartesian-morphism
  {x y : Ob} (f : Hom x y) (x' : Ob[ x ]) (y' : Ob[ y ])
  : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
  no-eta-equality
  field
    hom' : Hom[ f ] x' y'
    cocartesian : is-cocartesian f hom'

  open is-cocartesian cocartesian public

Duality🔗

As noted before, cocartesian maps the are duals to cartesian maps. We can make this correspondence precise by showing that cartesian maps in the total opposite of $E$ are cocartesian maps, and vice versa.

co-cartesian→cocartesian
  : ∀ {x y} {f : Hom x y} {x' y'} {f' : Hom[ f ] x' y'}
  → is-cartesian (ℰ ^total-op) f f'
  → is-cocartesian f f'

cocartesian→co-cartesian
  : ∀ {x y} {f : Hom x y} {x' y'} {f' : Hom[ f ] x' y'}
  → is-cocartesian f f'
  → is-cartesian (ℰ ^total-op) f f'

These functions just unpack and repack data, they are not particularly interesting.

co-cartesian→cocartesian cart^op .is-cocartesian.universal m h' =
  is-cartesian.universal cart^op m h'
co-cartesian→cocartesian cart^op .is-cocartesian.commutes m h' =
  is-cartesian.commutes cart^op m h'
co-cartesian→cocartesian cart^op .is-cocartesian.unique m' p =
  is-cartesian.unique cart^op m' p

cocartesian→co-cartesian cocart .is-cartesian.universal m h' =
  is-cocartesian.universal cocart m h'
cocartesian→co-cartesian cocart .is-cartesian.commutes m h' =
  is-cocartesian.commutes cocart m h'
cocartesian→co-cartesian cocart .is-cartesian.unique m' p =
  is-cocartesian.unique cocart m' p

Furthermore, these 2 functions form an equivalence, which we can extend to a path via univalence.

co-cartesian→cocartesian-is-equiv
  : ∀ {x y} {f : Hom x y} {x' y'} {f' : Hom[ f ] x' y'}
  → is-equiv (co-cartesian→cocartesian {f' = f'})
co-cartesian→cocartesian-is-equiv {f' = f'} =
  is-iso→is-equiv $ iso cocartesian→co-cartesian cocart-invl cocart-invr
  where
    cocart-invl
      : ∀ f
      → co-cartesian→cocartesian {f' = f'} (cocartesian→co-cartesian f) ≡ f
    cocart-invl f i .is-cocartesian.universal m h' = is-cocartesian.universal f m h'
    cocart-invl f i .is-cocartesian.commutes m h' = is-cocartesian.commutes f m h'
    cocart-invl f i .is-cocartesian.unique m' p = is-cocartesian.unique f m' p

    cocart-invr
      : ∀ f
      → cocartesian→co-cartesian {f' = f'} (co-cartesian→cocartesian f) ≡ f
    cocart-invr f i .is-cartesian.universal m h' = is-cartesian.universal f m h'
    cocart-invr f i .is-cartesian.commutes m h' = is-cartesian.commutes f m h'
    cocart-invr f i .is-cartesian.unique m' p = is-cartesian.unique f m' p

co-cartesian≡cocartesian
  : ∀ {x y} {f : Hom x y} {x' y'} {f' : Hom[ f ] x' y'}
  → is-cartesian (ℰ ^total-op) f f' ≡ is-cocartesian f f'
co-cartesian≡cocartesian =
  ua (co-cartesian→cocartesian , co-cartesian→cocartesian-is-equiv)

Properties of cocartesian morphisms🔗

We shall now prove the following properties of cocartesian morphisms.

cocartesian-∘
  : ∀ {x y z} {f : Hom y z} {g : Hom x y}
  → ∀ {x' y' z'} {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'}
  → is-cocartesian f f' → is-cocartesian g g'
  → is-cocartesian (f ∘ g) (f' ∘' g')

cocartesian-id : ∀ {x x'} → is-cocartesian id (id' {x} {x'})

invertible→cocartesian
  : ∀ {x y} {f : Hom x y} {x' y'} {f' : Hom[ f ] x' y'}
  → (f-inv : is-invertible f)
  → is-invertible[ f-inv ] f'
  → is-cocartesian f f'

cocartesian→weak-epic
  : ∀ {x y} {f : Hom x y}
  → ∀ {x' y'} {f' : Hom[ f ] x' y'}
  → is-cocartesian f f'
  → is-weak-epic f'

cocartesian-codomain-unique
  : ∀ {x y} {f : Hom x y}
  → ∀ {x' y' y''} {f' : Hom[ f ] x' y'} {f'' : Hom[ f ] x' y''}
  → is-cocartesian f f'
  → is-cocartesian f f''
  → y' ≅↓ y''

cocartesian-vertical-section-stable
  : ∀ {x y} {f : Hom x y}
  → ∀ {x' y' y''} {f' : Hom[ f ] x' y'} {f'' : Hom[ f ] x' y''} {ϕ : Hom[ id ] y'' y'}
  → is-cocartesian f f'
  → has-retract↓ ϕ
  → ϕ ∘' f'' ≡[ idl _ ] f'
  → is-cocartesian f f''

cocartesian-pasting
  : ∀ {x y z} {f : Hom y z} {g : Hom x y}
  → ∀ {x' y' z'} {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'}
  → is-cocartesian g g'
  → is-cocartesian (f ∘ g) (f' ∘' g')
  → is-cocartesian f f'

vertical+cocartesian→invertible
  : ∀ {x} {x' x'' : Ob[ x ]} {f' : Hom[ id ] x' x''}
  → is-cocartesian id f'
  → is-invertible↓ f'

The proofs are all applications of duality, as we have already done the hard work of proving these properties for cartesian morphisms.

cocartesian-∘ f-cocart g-cocart =
  co-cartesian→cocartesian $
  cartesian-∘ _
    (cocartesian→co-cartesian g-cocart)
    (cocartesian→co-cartesian f-cocart)

cocartesian-id = co-cartesian→cocartesian (cartesian-id _)

invertible→cocartesian f-inv f'-inv =
  co-cartesian→cocartesian $
  invertible→cartesian _ _ (invertible[]→co-invertible[] f'-inv)

cocartesian→weak-epic cocart =

  cartesian→weak-monic (ℰ ^total-op) (cocartesian→co-cartesian cocart)

cocartesian-codomain-unique f'-cocart f''-cocart =
  vertical-co-iso→vertical-iso $
  cartesian-domain-unique (ℰ ^total-op)
    (cocartesian→co-cartesian f''-cocart)
    (cocartesian→co-cartesian f'-cocart)

cocartesian-vertical-section-stable cocart ret factor =
  co-cartesian→cocartesian $
  cartesian-vertical-retraction-stable (ℰ ^total-op)
    (cocartesian→co-cartesian cocart)
    (vertical-retract→vertical-co-section ret)
    factor

cocartesian-pasting g-cocart fg-cocart =
  co-cartesian→cocartesian $
  cartesian-pasting (ℰ ^total-op)
    (cocartesian→co-cartesian g-cocart)
    (cocartesian→co-cartesian fg-cocart)

vertical+cocartesian→invertible cocart =
  vertical-co-invertible→vertical-invertible $
  vertical+cartesian→invertible (ℰ ^total-op)
    (cocartesian→co-cartesian cocart)

Furthermore, $f^{'} : x^{'} \to_{f} y^{'}$ is cocartesian if and only if the function $- \cdot^{'} f$ is an equivalence.

precompose-equiv→cocartesian
  : ∀ {x y x' y'} {f : Hom x y}
  → (f' : Hom[ f ] x' y')
  → (∀ {z z'} {g : Hom y z} → is-equiv {A = Hom[ g ] y' z'} (_∘' f'))
  → is-cocartesian f f'
precompose-equiv→cocartesian f' cocart =
  co-cartesian→cocartesian $
  postcompose-equiv→cartesian (ℰ ^total-op) f' cocart

cocartesian→precompose-equiv
  : ∀ {x y z x' y' z'} {g : Hom y z} {f : Hom x y} {f' : Hom[ f ] x' y'}
  → is-cocartesian f f'
  → is-equiv {A = Hom[ g ] y' z'} (_∘' f')
cocartesian→precompose-equiv cocart =
  cartesian→postcompose-equiv (ℰ ^total-op) $
  cocartesian→co-cartesian cocart

Cocartesian lifts🔗

We call an object $b^{'}$ over $b$ together with a cartesian arrow $f^{'} : a \to_{f} b^{'}$ a cocartesian lift of $f .$

record Cocartesian-lift {x y} (f : Hom x y) (x' : Ob[ x ]) : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ')
  where
  no-eta-equality
  field
    {y'} : Ob[ y ]
    lifting : Hom[ f ] x' y'
    cocartesian : is-cocartesian f lifting
  open is-cocartesian cocartesian public

We also can apply duality to cocartesian lifts.

co-cartesian-lift→cocartesian-lift
  : ∀ {x y} {f : Hom x y} {x' : Ob[ x ]}
  → Cartesian-lift (ℰ ^total-op) f x'
  → Cocartesian-lift f x'

cocartesian-lift→co-cartesian-lift
  : ∀ {x y} {f : Hom x y} {x' : Ob[ x ]}
  → Cocartesian-lift f x'
  → Cartesian-lift (ℰ ^total-op) f x'

The proofs are simply applying duality, so they are not particularly interesting.

co-cartesian-lift→cocartesian-lift cart .Cocartesian-lift.y' =
  Cartesian-lift.x' cart
co-cartesian-lift→cocartesian-lift cart .Cocartesian-lift.lifting =
  Cartesian-lift.lifting cart
co-cartesian-lift→cocartesian-lift cart .Cocartesian-lift.cocartesian =
  co-cartesian→cocartesian (Cartesian-lift.cartesian cart)

cocartesian-lift→co-cartesian-lift cocart .Cartesian-lift.x' =
  Cocartesian-lift.y' cocart
cocartesian-lift→co-cartesian-lift cocart .Cartesian-lift.lifting =
  Cocartesian-lift.lifting cocart
cocartesian-lift→co-cartesian-lift cocart .Cartesian-lift.cartesian =
  cocartesian→co-cartesian (Cocartesian-lift.cocartesian cocart)

We can use this notion to define cocartesian fibrations (sometimes referred to as opfibrations).

record Cocartesian-fibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
  no-eta-equality
  field
    has-lift : ∀ {x y} (f : Hom x y) (x' : Ob[ x ]) → Cocartesian-lift f x'

  module has-lift {x y} (f : Hom x y) (x' : Ob[ x ]) =
    Cocartesian-lift (has-lift f x')

  rebase : ∀ {x y x' x''} → (f : Hom x y)
           → Hom[ id ] x' x''
           → Hom[ id ] (has-lift.y' f x') (has-lift.y' f x'')
  rebase f vert =
    has-lift.universalv f _ (hom[ idr _ ] (has-lift.lifting f _ ∘' vert))

As expected, opfibrations are dual to fibrations.

op-fibration→opfibration : Cartesian-fibration (ℰ ^total-op) → Cocartesian-fibration

opfibration→op-fibration : Cocartesian-fibration → Cartesian-fibration (ℰ ^total-op)

The proofs here are just further applications of duality, so we omit them.

op-fibration→opfibration fib .Cocartesian-fibration.has-lift f x' =
  co-cartesian-lift→cocartesian-lift (Cartesian-fibration.has-lift fib f x')

opfibration→op-fibration opfib .Cartesian-fibration.has-lift f y' =
  cocartesian-lift→co-cartesian-lift (Cocartesian-fibration.has-lift opfib f y')