open import Cat.Displayed.Cartesian.Weak
open import Cat.Functor.Hom.Displayed
open import Cat.Displayed.Cartesian
open import Cat.Displayed.Total.Op
open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Displayed.Cocartesian.Indexing as Indexing
import Cat.Displayed.Morphism.Duality
import Cat.Displayed.Cocartesian as Cocart
import Cat.Displayed.Cocartesian as Cocart
import Cat.Displayed.Reasoning
import Cat.Displayed.Morphism
import Cat.Reasoning as CR

module Cat.Displayed.Cocartesian.Weak
  {o  o′ ℓ′}
  { : Precategory o }
  ( : Displayed  o′ ℓ′)
  where

Weak Cocartesian Morphisms🔗

We can define a weaker notion of cocartesian morphism much like we can with their cartesian counterparts.

record is-weak-cocartesian
  {a b a′ b′} (f : Hom a b) (f′ : Hom[ f ] a′ b′)
  : Type (o    o′  ℓ′)
  where
  no-eta-equality
  field
    universal :  {x′}  (g′ : Hom[ f ] a′ x′)  Hom[ id ] b′ x′
    commutes  :  {x′}  (g′ : Hom[ f ] a′ x′)  universal g′ ∘′ f′ ≡[ idl _ ] g′
    unique    :  {x′} {g′ : Hom[ f ] a′ x′}
               (h′ : Hom[ id ] b′ x′)
               h′ ∘′ f′ ≡[ idl _ ] g′
               h′  universal g′

Duality🔗

Weak cartesian maps in the total opposite category are equivalent to weak cocartesian maps.

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

weak-cocartesian→weak-co-cartesian
  :  {x y} {f : Hom x y} {x′ y′} {f′ : Hom[ f ] x′ y′}
   is-weak-cocartesian f f′
   is-weak-cartesian ( ^total-op) f f′
These functions just shuffle data around, so we omit their definitions.
weak-co-cartesian→weak-cocartesian wcart .is-weak-cocartesian.universal =
  is-weak-cartesian.universal wcart
weak-co-cartesian→weak-cocartesian wcart .is-weak-cocartesian.commutes =
  is-weak-cartesian.commutes wcart
weak-co-cartesian→weak-cocartesian wcart .is-weak-cocartesian.unique =
  is-weak-cartesian.unique wcart

weak-cocartesian→weak-co-cartesian wcocart .is-weak-cartesian.universal =
  is-weak-cocartesian.universal wcocart
weak-cocartesian→weak-co-cartesian wcocart .is-weak-cartesian.commutes =
  is-weak-cocartesian.commutes wcocart
weak-cocartesian→weak-co-cartesian wcocart .is-weak-cartesian.unique =
  is-weak-cocartesian.unique wcocart

Weak cocartesian maps satisfy the dual properties of weak cartesian maps.

weak-cocartesian-codomain-unique
  :  {x y} {f : Hom x y}
    {x′ y′ y″} {f′ : Hom[ f ] x′ y′} {f″ : Hom[ f ] x′ y″}
   is-weak-cocartesian f f′
   is-weak-cocartesian f f″
   y′ ≅↓ y″

cocartesian→weak-cocartesian
  :  {x y x′ y′} {f : Hom x y} {f′ : Hom[ f ] x′ y′}
   is-cocartesian f f′
   is-weak-cocartesian f f′

weak-cocartesian→cocartesian
  :  {x y x′ y′} {f : Hom x y} {f′ : Hom[ f ] x′ y′}
   Cocartesian-fibration
   is-weak-cocartesian f f′
   is-cocartesian f f′
The proofs consist of tedious applications of duality.
weak-cocartesian-codomain-unique f′-cocart f″-cocart =
  vertical-co-iso→vertical-iso $
  weak-cartesian-domain-unique ( ^total-op)
    (weak-cocartesian→weak-co-cartesian f″-cocart)
    (weak-cocartesian→weak-co-cartesian f′-cocart)

cocartesian→weak-cocartesian cocart =
  weak-co-cartesian→weak-cocartesian $
  cartesian→weak-cartesian ( ^total-op) $
  cocartesian→co-cartesian cocart

weak-cocartesian→cocartesian opfib wcocart =
  co-cartesian→cocartesian $
  weak-cartesian→cartesian ( ^total-op)
    (opfibration→op-fibration opfib)
    (weak-cocartesian→weak-co-cartesian wcocart)

Notably, if E\mathcal{E} is a cartesian fibration, then all weak cocartesian morphisms are cocartesian.

fibration+weak-cocartesian→cocartesian
  :  {x y x′ y′} {f : Hom x y} {f′ : Hom[ f ] x′ y′}
   Cartesian-fibration 
   is-weak-cocartesian f f′
   is-cocartesian f f′
fibration+weak-cocartesian→cocartesian {x} {y} {x′} {y′} {f} {f′} fib weak = cocart
  where
    open Cartesian-fibration fib
    module weak = is-weak-cocartesian weak

To see show this, we need to construct a unique factorization of some morphism h:xmfuh' : x' \to_{mf} u', as depicted in the following diagram

We start by taking the cartesian lift of mm to obtain the map mm^{*}, which we have highlighted in red.

    module Morphisms {u} {u′ : Ob[ u ]} (m : Hom y u) (h′ : Hom[ m  f ] x′ u′) where
      y* : Ob[ y ]
      y* = Cartesian-lift.x′ (has-lift m u′)

      m* : Hom[ m ] y* u′
      m* =  Cartesian-lift.lifting (has-lift m u′)

      module m* = is-cartesian (Cartesian-lift.cartesian (has-lift m u′))

Next, we can construct the morphism hh^{*} (highlighted in red) as the universal factorisation of hh' through mm^{*}.

      h* : Hom[ f ] x′ y*
      h* = m*.universal f h′

Finally, we can construct a vertical morphism h:yyh^{**} : y' \to y^{*}, as ff' is weakly cartesian.

      h** : Hom[ id ] y′ y*
      h** = weak.universal h*

Composing mm^{*} and hh^{**} gives the desired factorisation.

    cocart : is-cocartesian f f′
    cocart .is-cocartesian.universal m h′ =
      hom[ idr _ ] (m* ∘′ h**)
      where open Morphisms m h′

Showing that mh=hm^{*} \cdot h^{**} = h' is best understood diagramatically; both the mh=hm^{*} \cdot h^{*} = h' and hf=hh^{**} \cdot f' = h^{*} cells commute.

    cocart .is-cocartesian.commutes m h′ =
      hom[] (m* ∘′ h**) ∘′ f′   ≡˘⟨ yank _ _ _ ≡˘
      m* ∘′ hom[] (h** ∘′ f′)   ≡⟨ ap (m* ∘′_) (from-pathp (weak.commutes _)) 
      m* ∘′ m*.universal f h′                 ≡⟨ m*.commutes f h′ 
      h′ 
      where open Morphisms m h′

Uniqueness is somewhat more delicate. We need to show that the blue cell in the following diagram commutes.

As a general fact, every morphism in a cartesian fibration factors into a composite of a cartesian and vertical morphism, obtained by taking the universal factorisation of m:ymium' : y' \to{m \cdot i} u'. We shall denote this morphism as idid*.

However, hh^{**} is the unique vertical map that factorises ff' through hh^{*}, so it suffices to show that the cell highlighted in blue commutes.

hh^{*} is the unique vertical map that factorises hh' through mm', and h=mfh' = m' \cdot f' by our hypothesis, so it suffices to show that midf=mfm^{*} \cdot id^{*} \cdot f' = m' \cdot f'. This commutes because mm^{*} is cartesian, thus finishing the proof.

    cocart .is-cocartesian.unique {m = m} {h′ = h′} m′ p =
      m′                ≡⟨ from-pathp⁻ (symP (m*.commutesp (idr _) m′)) 
      hom[] (m* ∘′ id*) ≡⟨ hom[]⟩⟨ ap (m* ∘′_) (weak.unique _ (to-pathp $ m*.unique _ path )) 
      hom[] (m* ∘′ h**) 
      where
        open Morphisms m h′

        id* : Hom[ id ] y′ y*
        id* = m*.universalv m′

        path : m* ∘′ hom[ idl _ ] (id* ∘′ f′)  h′
        path =
          m* ∘′ hom[] (id* ∘′ f′) ≡⟨ whisker-r _ 
          hom[] (m* ∘′ id* ∘′ f′) ≡⟨ cancel _ (ap (m ∘_) (idl _)) (pulll′ (idr _) (m*.commutesv m′)) 
          m′ ∘′ f′                ≡⟨ p 
          h′ 

Weak cocartesian lifts🔗

We can also define the dual to weak cartesian lifts.

record Weak-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′
    weak-cocartesian : is-weak-cocartesian f lifting

  open is-weak-cocartesian weak-cocartesian public

As expected, weak cocartesian lifts are dual to weak cartesian lifts.

weak-co-cartesian-lift→weak-cocartesian-lift
  :  {x y} {f : Hom x y} {x′ : Ob[ x ]}
   Weak-cartesian-lift ( ^total-op) f x′
   Weak-cocartesian-lift f x′

weak-cocartesian-lift→weak-co-cartesian-lift
  :  {x y} {f : Hom x y} {x′ : Ob[ x ]}
   Weak-cocartesian-lift f x′
   Weak-cartesian-lift ( ^total-op) f x′
We omit the proofs, as they are even more applications of duality.
weak-co-cartesian-lift→weak-cocartesian-lift wlift .Weak-cocartesian-lift.y′ =
  Weak-cartesian-lift.x′ wlift
weak-co-cartesian-lift→weak-cocartesian-lift wlift .Weak-cocartesian-lift.lifting =
  Weak-cartesian-lift.lifting wlift
weak-co-cartesian-lift→weak-cocartesian-lift wlift .Weak-cocartesian-lift.weak-cocartesian =
  weak-co-cartesian→weak-cocartesian (Weak-cartesian-lift.weak-cartesian wlift)

weak-cocartesian-lift→weak-co-cartesian-lift wlift .Weak-cartesian-lift.x′ =
  Weak-cocartesian-lift.y′ wlift
weak-cocartesian-lift→weak-co-cartesian-lift wlift .Weak-cartesian-lift.lifting =
  Weak-cocartesian-lift.lifting wlift
weak-cocartesian-lift→weak-co-cartesian-lift wlift .Weak-cartesian-lift.weak-cartesian =
  weak-cocartesian→weak-co-cartesian (Weak-cocartesian-lift.weak-cocartesian wlift)

A displayed category with all weak cocartesian lifts is called a weak cocartesian fibration, though we will often refer to them as weak opfibrations These are also sometimes called preopfibred categories, though we avoid this terminology, as it conflicts with the precategory/category distinction.

record is-weak-cocartesian-fibration : Type (o    o′  ℓ′) where
  no-eta-equality
  field
    weak-lift :  {x y}  (f : Hom x y)  (x′ : Ob[ x ])  Weak-cocartesian-lift f x′

  module weak-lift {x y} (f : Hom x y) (x′ : Ob[ x ]) =
    Weak-cocartesian-lift (weak-lift f x′)
Weak opfibrations are dual to [weak fibrations].
weak-op-fibration→weak-opfibration
  : is-weak-cartesian-fibration ( ^total-op)
   is-weak-cocartesian-fibration

weak-opfibration→weak-op-fibration
  : is-weak-cocartesian-fibration
   is-weak-cartesian-fibration ( ^total-op)
As usual, we omit the duality proofs, as they are quite tedious.
weak-op-fibration→weak-opfibration wlift .is-weak-cocartesian-fibration.weak-lift f x′ =
  weak-co-cartesian-lift→weak-cocartesian-lift $
  is-weak-cartesian-fibration.weak-lift wlift f x′

weak-opfibration→weak-op-fibration wlift .is-weak-cartesian-fibration.weak-lift f y′ =
  weak-cocartesian-lift→weak-co-cartesian-lift $
  is-weak-cocartesian-fibration.weak-lift wlift f y′

Every opfibration is a weak opfibration.

cocartesian-lift→weak-cocartesian-lift
  :  {x y} {f : Hom x y} {x′ : Ob[ x ]}
   Cocartesian-lift f x′
   Weak-cocartesian-lift f x′

opfibration→weak-opfibration
  : Cocartesian-fibration
   is-weak-cocartesian-fibration

A weak opfibration is an opfibration when weak cocartesian morphisms are closed under composition. This follows via duality.

weak-opfibration→opfibration
  : is-weak-cocartesian-fibration
   (∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y}
      {f′ : Hom[ f ] y′ z′} {g′ : Hom[ g ] x′ y′}
      is-weak-cocartesian f f′  is-weak-cocartesian g g′
      is-weak-cocartesian (f  g) (f′ ∘′ g′))
   Cocartesian-fibration
weak-opfibration→opfibration wopfib weak-∘ =
  op-fibration→opfibration $
  weak-fibration→fibration ( ^total-op)
  (weak-opfibration→weak-op-fibration wopfib)
   f g 
    weak-cocartesian→weak-co-cartesian $
    weak-∘
      (weak-co-cartesian→weak-cocartesian g)
      (weak-co-cartesian→weak-cocartesian f))

If E\mathcal{E} is cartesian, we can drop the requirement that weak cocartesian maps are closed under composition, thanks to fibration+weak-cocartesian→cocartesian.

cartesian+weak-opfibration→opfibration
  : Cartesian-fibration 
   is-weak-cocartesian-fibration
   Cocartesian-fibration
cartesian+weak-opfibration→opfibration fib wlifts =
  weak-opfibration→opfibration wlifts λ f-weak g-weak 
    cocartesian→weak-cocartesian $
    cocartesian-∘
      (fibration+weak-cocartesian→cocartesian fib f-weak)
      (fibration+weak-cocartesian→cocartesian fib g-weak)

Weak Opfibrations and Equivalence of Hom Sets🔗

If E\mathcal{E} is a weak opfibration, then the hom sets xfyx' \to_f y' and f(x)idyf^{*}(x') \to_{id} y' are equivalent, where f(x)f^{*}(x') is the codomain of the lift of ff along yy'.

module _ (wopfib : is-weak-cocartesian-fibration) where
  open is-weak-cocartesian-fibration wopfib

  weak-opfibration→universal-is-equiv
    :  {x y y′ x′}
     (u : Hom x y)
     is-equiv (weak-lift.universal u x′ {y′})
  weak-opfibration→universal-is-equiv {x′ = x′} u =
    is-iso→is-equiv $
    iso  u′  hom[ idl u ] (u′ ∘′ weak-lift.lifting u x′))
         u′  sym $ weak-lift.unique u x′ u′ (to-pathp refl))
         u′  cancel _ _ (weak-lift.commutes u x′ u′))

  weak-opfibration→vertical-equiv
    :  {x y x′ y′}
     (u : Hom x y)
     Hom[ u ] x′ y′  Hom[ id ] (weak-lift.y′ u x′) y′
  weak-opfibration→vertical-equiv {x′ = x′} u =
    weak-lift.universal u x′ , weak-opfibration→universal-is-equiv u

Furthermore, this equivalence is natural.

  weak-opfibration→hom-iso-from
    :  {x y x′} (u : Hom x y)
     natural-iso (Hom-over-from  u x′) (Hom-from (Fibre  y) (weak-lift.y′ u x′))
  weak-opfibration→hom-iso-from {y = y} {x′ = x′} u = to-natural-iso mi where
    open make-natural-iso

    u*x′ : Ob[ y ]
    u*x′ = weak-lift.y′ u x′

    mi : make-natural-iso (Hom-over-from  u x′) (Hom-from (Fibre  y) u*x′)
    mi .eta x u′ = weak-lift.universal u x′ u′
    mi .inv x v′ = hom[ idl u ] (v′ ∘′ weak-lift.lifting u x′)
    mi .eta∘inv _ = funext λ v′ 
      sym $ weak-lift.unique u _ _ (to-pathp refl)
    mi .inv∘eta _ = funext λ u′ 
      from-pathp $ weak-lift.commutes u _ _
    mi .natural _ _ v′ = funext λ u′ 
      weak-lift.unique _ _ _ $ to-pathp $
        smashl _ _
       weave _ (ap (_∘ u) (idl id)) _ (pullr′ _ (weak-lift.commutes _ _ _))

As in the weak cartesian case, the converse is also true: if there is a lifting of objects Ob[ x ] → Ob[ y ] for every morphism f:xyf : x \to y in B\mathcal{B}, along with a equivalence of homs as above, then E\mathcal{E} is a weak opfibration.

module _ (_*₀_ :  {x y}  Hom x y  Ob[ x ]  Ob[ y ]) where

  private
    vertical-equiv-iso-natural
      : (∀ {x y x′ y′} {f : Hom x y}  Hom[ f ] x′ y′  Hom[ id ] (f *₀ x′) y′)
       Type _
    vertical-equiv-iso-natural to =
       {x y x′ y′ y″} {g : Hom x y}
       (f′ : Hom[ id ] y′ y″) (g′ : Hom[ g ] x′ y′)
       to (hom[ idl g ] (f′ ∘′ g′)) ≡[ sym (idl id) ] f′ ∘′ to g′

  vertical-equiv→weak-opfibration
    : (to :  {x y x′ y′} {f : Hom x y}  Hom[ f ] x′ y′  Hom[ id ] (f *₀ x′) y′)
     (eqv :  {x y x′ y′} {f : Hom x y}  is-equiv (to {x} {y} {x′} {y′} {f}))
     (natural : vertical-equiv-iso-natural to)
     is-weak-cocartesian-fibration
  vertical-equiv→weak-opfibration to to-eqv natural =
    weak-op-fibration→weak-opfibration $
    vertical-equiv→weak-fibration ( ^total-op) _*₀_ to to-eqv λ f′ g′ 
      to-pathp (reindex _ _  from-pathp (natural g′ f′))