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 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 in objects and displayed over and resp., and a map over We say that 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 and be displayed over Furthermore, suppose we have a map (highlighted in violet below), along with a map displayed over (highlighted in red). For to be cocartesian, every such situation must give rise to a unique universal factorisation of through a map (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 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, is cocartesian if and only if the function 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 over together with a cartesian arrow a cocartesian lift of

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')
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')