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

The opposite of a fibration🔗


The construction formalised here, defined in terms of an operation which assigns Cartesian lifts, is due to Sterling (2022); there it is introduced as a simplification of a construction to Bénabou as relayed by Streicher (2023). In the univalent setting, the extra generality afforded by Bénabou’s construction would only be relevant in the setting of uncloven fibrations of precategories; we have thus decided to avoid its complexity.

Since the theory of fibrations over behaves like ordinary category theory over we expect to find 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 we want to construct the fibration which classifies1

in other words, the fibration whose fibre categories are the opposites of those of Note that this is still a category over unlike in the case of the total opposite, which results in a category over — which, generally, will not be a fibration. The construction of the fibred opposite proceeds using base change functors. A morphism lying over a map is defined to be a map as indicated (in red) in the diagram below.

At the level of vertical maps, this says that a morphism is determined by a morphism hence by a morphism this correspondence trivially extends to an isomorphism of precategories between and If we have maps and we can obtain a map to stand for their opposite in by calculating

where the map is one of the structural morphisms expressing pseudofunctoriality of

  : ∀ {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 are dependent paths over the corresponding laws in 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 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 in 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 we obtain a vertical map which we call the adjustment induced by The explicit definition below is identical to transporting the identity map along but computes better:

    : ∀ {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 _ _)

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.

    : ∀ {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 with the pseudofunctoriality witnesses of

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

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

    : ∀ {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 γ→
The proofs here are nothing more than calculations at the level of the underlying displayed category. They’re not informative; it’s fine to take the three theorems above as given.
  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''  = π
_^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 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 to 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🔗

Since we defined the displayed morphism spaces directly in terms of base change, it’s not surprising that is itself a fibration. Indeed, if we have and a Cartesian lift of along 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)

  1. Note that, strictly speaking, the construction of opposite categories can not be extended to a pseudofunctor While the opposite of a functor goes in the same direction as the original (i.e.  is taken to the opposite of a natural transformation has reversed direction — the dual of is To capture this, the “opposite category functor” would need to be typed instead, indicating that it reverses 2-cells.

    However, because the domain is locally discrete, all of its 2-cells are isomorphisms. Therefore, the pseudofunctor classified by a given fibration factors through the homwise core of — and the construction of opposite categories restricts to a map ↩︎