{-# OPTIONS --lossy-unification #-}
open import Cat.Displayed.Cartesian
open import Cat.Functor.Naturality
open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Cartesian.Indexing as Ix
import Cat.Displayed.Fibre.Reasoning as Fib
import Cat.Displayed.Reasoning as Disp
import Cat.Functor.Reasoning as Fr
import Cat.Reasoning as Cat

module Cat.Displayed.Instances.Opposite
  {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ')
  (cart : Cartesian-fibration E)
  where

The opposite of a fibration🔗

open Cartesian-fibration cart
open Displayed E
open Ix E cart
open Cat B
open _=>_

private
  module rebase {x} {y} {f : Hom x y} = Fr (base-change f)
  module D = Displayed
  module E = Disp E
  module F = Fib E
  open F renaming (_∘_ to infixr  _∘v_) using ()

  _^*_ : ∀ {a b} (f : Hom a b) → Ob[ b ] → Ob[ a ]
  f ^* x = has-lift.x' f x

  π : ∀ {a b} {f : Hom a b} {x : Ob[ b ]} → Hom[ f ] (f ^* x) x
  π = has-lift.lifting _ _

  γ← = ^*-comp-from
  γ→ = ^*-comp-to
  ι← = ^*-id-from
  ι→ = ^*-id-to
  _[_] = rebase
  infix  _[_]

Since the theory of fibrations over $\mathcal{B}$ behaves like ordinary category theory over $\mathbf{Sets}\text{,}$ we expect to find $\mathcal{B}\text{-indexed}$ analogues of basic constructions such as functor categories, product categories, and, what concerns us here, opposite categories. Working at the level of displayed categories, fix a fibration $\mathcal{E}\mathcal{B}\text{;}$ we want to construct the fibration which classifies¹

in other words, the fibration whose fibre categories are the opposites of those of $\mathcal{E}\text{.}$ Note that this is still a category over $\mathcal{B}\text{,}$ unlike in the case of the total opposite, which results in a category over ${\mathcal{B}}^{\mathrm{op}}$ — which, generally, will not be a fibration. The construction of the fibred opposite proceeds using $\mathcal{E}\text{’s}$ base change functors. A morphism $h:y{\to }_f^{\mathrm{op}}x\text{,}$ lying over a map $f:a\to b\text{,}$ is defined to be a map $f^{\ast }y{\to }_{\mathrm{id}}x\text{,}$ as indicated (in red) in the diagram below.

At the level of vertical maps, this says that a morphism $x{\to }^{\mathrm{op}}y$ is determined by a morphism ${\mathrm{id}}^{\ast }y\to x\text{,}$ hence by a morphism $y\to x\text{;}$ this correspondence trivially extends to an isomorphism of precategories between ${\mathcal{E}}^{\ast }(x{)}^{\mathrm{op}}$ and ${\mathcal{E}}_{\mathrm{op}}^{\ast }(x)\text{.}$ If we have maps $h:f^{\ast }z\to y$ and $h^{\prime }:g^{\ast }y\to x\text{,}$ we can obtain a map $f{g}^{\ast }z\to x$ to stand for their opposite in ${\mathcal{E}}^{\mathrm{op}}$ by calculating

where the map $\gamma$ is one of the structural morphisms expressing pseudofunctoriality of ${\mathcal{E}}^{\ast }(-)\text{.}$

_∘,_
  : ∀ {a b c} {x y z} {f : Hom b c} {g : Hom a b}
  → (f' : Hom[ id ] (f ^* z) y) (g' : Hom[ id ] (g ^* y) x)
  → Hom[ id {x = a} ] ((f ∘ g) ^* z) x
_∘,_ {g = g} f' g' = g' ∘v g [ f' ] ∘v γ→

The coherence problem🔗

Having done the mathematics behind the fibred opposite, we turn to teaching Agda about the construction. Recall that the algebraic laws (associativity, unitality) of a displayed category $\mathcal{E}\mathcal{B}$ are dependent paths over the corresponding laws in $\mathcal{B}\text{.}$ Ordinarily, this dependence is strictly at the level of morphisms depending on morphisms, with the domain and codomain staying fixed — and we have an extensive toolkit of combinators for dealing with this indexing.

However, the fibred opposite mixes levels in a complicated way. For concreteness, let’s focus on the right identity law. We want to construct a path between some $h:f^{\ast }y\to x$ and the composite

but note that, while these are both vertical maps, they have different domains! While the path we’re trying to construct is allowed to depend on the witness that $f\mathrm{id}=f$ in $\mathcal{B}\text{,}$ introducing this dependency on the domain object actually complicates things even further. Our toolkit does not include very many tools for working with dependent identifications between maps whose source and target vary.

The solution is to reify the dependency of the identifications into a morphism, which we can then calculate with at the level of fibre categories. Given a path $p:f=f^{\prime }\text{,}$ we obtain a vertical map $f^{\prime \ast }x\to f^{\ast }x\text{,}$ which we call the adjustment induced by $p\text{.}$ The explicit definition below is identical to transporting the identity map $f^{\ast }x\to f^{\ast }x$ along $p\text{,}$ but computes better:

private
  adjust
    : ∀ {a b} {f f' : Hom a b} {x : Ob[ b ]}
    → (p : f ≡ f')
    → Hom[ id ] (f' ^* x) (f ^* x)
  adjust p = has-lift.universal' _ _ (idr _ ∙ p) (has-lift.lifting _ _)

private abstract
  π-adjust
    : ∀ {a b} {f f' : Hom a b} {x : Ob[ b ]} (p : f ≡ f')
    → π {a} {b} {f} {x} ∘' adjust p ≡[ refl ∙ idr f ∙ p ] π
  π-adjust p = has-lift.commutes _ _ _ _ ∙[] to-pathp⁻ refl

  adjust-refl
    : ∀ {a b} {f : Hom a b} {x : Ob[ b ]}
    → adjust {x = x} (λ i → f) ≡ id'
  adjust-refl = has-lift.uniquep₂ _ _ (idr _) refl (idr _) (adjust refl) id'
    (to-pathp (ap E.hom[] (has-lift.commutes _ _ _ _) ·· E.hom[]-∙ _ _ ·· E.liberate _))
    (idr' _)

The point of introducing adjust is the following theorem, which connects transport in the domain of a vertical morphism with postcomposition along adjust. The proof is by path induction: it suffices to cover the case where the domain varies trivially, which leads to a correspondingly trivial adjustment.

  transp-lift
    : ∀ {a b} {f f' : Hom a b} {x : Ob[ b ]} {y : Ob[ a ]} {h : Hom[ id ] (f ^* x) y}
    → (p : f ≡ f')
    → transport (λ i → Hom[ id ] (p i ^* x) y) h ≡ h ∘v adjust p
  transp-lift {f = f} {x = x} {y} {h} =
    J (λ f' p → transport (λ i → Hom[ id ] (p i ^* x) y) h ≡ E.hom[ idl id ] (h ∘' adjust p))
      ( transport-refl _
      ∙ sym (ap E.hom[] (ap₂ _∘'_ refl adjust-refl)
      ∙ ap E.hom[] (from-pathp⁻ (idr' h)) ∙ E.hom[]-∙ _ _ ∙ E.liberate _))

To finish, we’ll need to connect the adjustment induced by the algebraic laws of $\mathcal{B}$ with the pseudofunctoriality witnesses of $\mathcal{E}\text{.}$

  adjust-idr
    : ∀ {a b} {f : Hom a b} {x : Ob[ b ]}
    → adjust {x = x} (idr f) ≡ γ← ∘v ι←

  adjust-idl
    : ∀ {a b} {f : Hom a b} {x : Ob[ b ]}
    → adjust {x = x} (idl f) ≡ γ← ∘v f [ ι← ]

  adjust-assoc
    : ∀ {a b c d} {f : Hom c d} {g : Hom b c} {h : Hom a b} {x : Ob[ d ]}
    → adjust {x = x} (assoc f g h) ≡ γ← ∘v γ← ∘v h [ γ→ ] ∘v γ→

  adjust-idr {f = f} {x} = has-lift.uniquep₂ _ _ _ _ _ _ _ (π-adjust (idr f))
    (   F.pulllf (has-lift.commutesv (f ∘ id) x (π ∘' π))
    ∙[] E.pullr[] (idr id) (has-lift.commutesp id (f ^* x) (idr id) id')
    ∙[] idr' π)

  adjust-idl {f = f} {x} = has-lift.uniquep₂ _ _ _ _ _ _ _ (π-adjust (idl f))
    (   F.pulllf (has-lift.commutesv (id ∘ f) x (π ∘' π))
    ∙[] E.pullr[] _ (has-lift.commutesp f (id ^* x) id-comm (ι← ∘' π))
    ∙[] E.pulll[] _ (has-lift.commutesp id x (idr id) id') ∙[] idl' π)

  adjust-assoc {f = f} {g} {h} = has-lift.uniquep₂ _ _ _ _ _ _ _ (π-adjust (assoc f g h))
    (F.pulllf (has-lift.commutesv (f ∘ g ∘ h) _ _) ∙[] E.pullr[] _ (F.pulllf (has-lift.commutesp (g ∘ h) _ (idr (g ∘ h)) _))
    ∙[] (E.refl⟩∘'⟨ E.pullr[] (id-comm ∙ sym (idr (id ∘ h))) (F.pulllf (has-lift.commutesp _ _ _ _)))
    ∙[] (E.refl⟩∘'⟨ E.pulll[] _ (E.pulll[] (idr g) (has-lift.commutesp _ _ _ _)))
    ∙[] E.pulll[] _ (E.pulll[] _ (has-lift.commutes _ _ _ _))
    ∙[] E.pullr[] (idr h) (has-lift.commutesp _ _ _ _)
    ∙[] has-lift.commutes _ _ _ _)

The construction🔗

Using adjust, and the three theorems above, we can tackle each of the three laws in turn. Having boiled the proofs down to reasoning about coherence morphisms in a pseudofunctor, the proofs are… no more than reasoning about coherence morphisms in a pseudofunctor — which is to say, boring algebra. Let us make concrete note of the data of the fibrewise opposite before tackling the properties:

_^op' : Displayed B o' ℓ'
_^op' .D.Ob[_] = Ob[_]
_^op' .D.Hom[_]     f x y = Hom[ id ] (f ^* y) x
_^op' .D.Hom[_]-set f x y = Hom[_]-set _ _ _
_^op' .D.id'  = π
_^op' .D._∘'_ = _∘,_

We can look at the case of left identity as a representative example. Note that, after applying the generic transp-lift and the specific lemma — in this case, adjust-idl — we’re reasoning entirely in the fibres of $\mathcal{E}\text{.}$ This lets us side-step most of the indexed nonsense that otherwise haunts working with fibrations.

_^op' .D.idl' {x = x} {y} {f = f} f' = to-pathp $
  transport (λ i → Hom[ id ] (idl f i ^* y) x) _  ≡⟨ transp-lift _ ∙ ap₂ _∘v_ refl adjust-idl ⟩
  (f' ∘v f [ π ] ∘v γ→) ∘v γ← ∘v f [ ι← ]         ≡⟨ F.pullr (F.pullr refl) ⟩
  f' ∘v f [ π ] ∘v γ→ ∘v (γ← ∘v f [ ι← ])         ≡⟨ ap₂ _∘v_ refl (ap₂ _∘v_ refl (F.cancell (^*-comp .F.invl))) ⟩
  f' ∘v f [ π ] ∘v f [ ι← ]                       ≡⟨ F.elimr (rebase.annihilate (E.cancel _ _ (has-lift.commutesv _ _ _))) ⟩
  f'                                              ∎

The next two cases are very similar, so we’ll present them without further comment.

_^op' .D.idr' {x = x} {y} {f} f' = to-pathp $
  transport (λ i → Hom[ id ] (idr f i ^* y) x) _  ≡⟨ transp-lift _ ∙ ap₂ _∘v_ refl adjust-idr ⟩
  (π ∘v id [ f' ] ∘v γ→) ∘v γ← ∘v ι←              ≡⟨ F.pullr (F.pullr (F.cancell (^*-comp .F.invl))) ⟩
  π ∘v id [ f' ] ∘v ι←                            ≡⟨ ap (π ∘v_) (sym (base-change-id .Isoⁿ.from .is-natural _ _ _)) ⟩
  π ∘v ι← ∘v f'                                   ≡⟨ F.cancell (base-change-id .Isoⁿ.invl ηₚ _) ⟩
  f'                                              ∎

_^op' .D.assoc' {x = x} {y} {z} {f} {g} {h} f' g' h' = to-pathp $
  transport (λ i → Hom[ id ] (assoc f g h i ^* _) _) (f' ∘, (g' ∘, h'))           ≡⟨ transp-lift _ ∙ ap₂ _∘v_ refl adjust-assoc ⟩
  ((h' ∘v h [ g' ] ∘v γ→) ∘v (g ∘ h) [ f' ] ∘v γ→) ∘v γ← ∘v γ← ∘v h [ γ→ ] ∘v γ→  ≡⟨ sym (F.assoc _ _ _) ∙ F.pullr (F.pullr (ap (γ→ ∘v_) (F.pullr refl))) ⟩
  h' ∘v h [ g' ] ∘v γ→ ∘v (g ∘ h) [ f' ] ∘v ⌜ γ→ ∘v γ← ∘v γ← ∘v h [ γ→ ] ∘v γ→ ⌝  ≡⟨ ap (λ e → h' ∘v h [ g' ] ∘v γ→ ∘v (g ∘ h) [ f' ] ∘v e) (F.cancell (^*-comp .F.invl))  ⟩
  h' ∘v h [ g' ] ∘v ⌜ γ→ ∘v (g ∘ h) [ f' ] ∘v γ← ∘v h [ γ→ ] ∘v γ→ ⌝              ≡⟨ ap (λ e → h' ∘v h [ g' ] ∘v e) (F.extendl (sym (^*-comp-to-natural _))) ⟩
  h' ∘v h [ g' ] ∘v h [ g [ f' ] ] ∘v γ→ ∘v γ← ∘v h [ γ→ ] ∘v γ→                  ≡⟨ ap₂ _∘v_ refl (F.pulll (sym (rebase.F-∘ _ _)) ∙ ap₂ _∘v_ refl (F.cancell (^*-comp .F.invl))) ⟩
  h' ∘v h [ g' ∘v g [ f' ] ] ∘v h [ γ→ ] ∘v γ→                                    ≡⟨ ap (h' ∘v_) (rebase.pulll (F.pullr refl)) ⟩
  h' ∘v h [ g' ∘v g [ f' ] ∘v γ→ ] ∘v γ→                                          ∎

Having defined the fibration, we can prove the comparison theorem mentioned in the introductory paragraph, showing that passing from $\mathcal{E}$ to ${\mathcal{E}}^{\mathrm{op}}$ inverts each fibre.

opposite-map : ∀ {a} {x y : Ob[ a ]} → Fib.Hom E y x ≃ Fib.Hom _^op' x y
opposite-map .fst f = f ∘v π
opposite-map .snd = is-iso→is-equiv $ iso
  (λ f → f ∘v has-lift.universalv id _ id')
  (λ x → F.cancelr (base-change-id .Isoⁿ.invr ηₚ _))
  (λ x → F.cancelr (base-change-id .Isoⁿ.invl ηₚ _))

Cartesian lifts🔗

abstract
  ∘,-idl
    : ∀ {a b c} {x y} {f : Hom b c} {g : Hom a b} (f' : Hom[ id ] (g ^* (f ^* x)) y)
    → id' ∘, f' ≡ f' ∘v γ→
  ∘,-idl {f = f} {g} f' =
    f' ∘v g [ id' ] ∘v γ→ ≡⟨ ap (f' ∘v_) (F.eliml (base-change g .Functor.F-id)) ⟩
    f' ∘v γ→              ∎

private module Cf = Cartesian-fibration

Since we defined the displayed morphism spaces directly in terms of $\mathcal{E}\text{’s}$ base change, it’s not surprising that ${\mathcal{E}}_{\mathrm{op}}$ is itself a fibration. Indeed, if we have $f:a\to b$ and $yb\text{,}$ a Cartesian lift of $y$ along $f\text{,}$ in the opposite, boils down to asking for something to fit into the question mark in the diagram

It’s no coincidence that the boundary of the question mark is precisely that of the identity morphism. A mercifully short calculation establishes that this choice does furnish a Cartesian lift.

Opposite-cartesian : Cartesian-fibration _^op'
Opposite-cartesian .Cf.has-lift f y' = record
  { lifting   = id'
  ; cartesian = record
    { universal = λ m h → h ∘v γ←
    ; commutes  = λ m h → ∘,-idl (h ∘v γ←) ∙ F.cancelr (^*-comp .F.invr)
    ; unique    = λ m h → sym (F.cancelr (^*-comp .F.invl)) ∙ ap (_∘v γ←) (sym (∘,-idl m) ∙ h)
    }
  }