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 BopCat\mathcal{B}^{op} \to \mathfrak{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 aba \to b in B\mathcal{B}, objects aa' and bb' displayed over aa and bb resp., and a map f:afbf' : a' \to_f b' over ff. We say that ff' 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:Bu : \mathcal{B} and uu' be displayed over uu. Furthermore, suppose we have a map m:bum : b \to u (highlighted in violet below), along with a map h:amfuh' : a' \to_{mf} u' displayed over mfm \cdot f (highlighted in red). For ff' to be cocartesian, every such situation must give rise to a unique universal factorisation of hh' through a map bmub' \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′

Duality🔗

As noted before, cocartesian maps are dual to cartesian maps. We can make this correspondence precise by showing that cartesian maps in the total opposite of E\mathcal{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)

Cocartesian Lifts🔗

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

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