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 25 _β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 30 _[_]

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
$B$
behaves like ordinary category theory over
$Sets,$
we expect to find
$B-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
$EB;$
we want to construct the fibration which classifies^{1}

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

At the level of vertical maps, this says that a morphism $xβ_{op}y$ is determined by a morphism $id_{β}yβx,$ hence by a morphism $yβx;$ this correspondence trivially extends to an isomorphism of precategories between $E_{β}(x)_{op}$ and $E_{op}(x).$ If we have maps $h:f_{β}zβy$ and $h_{β²}:g_{β}yβx,$ we can obtain a map $fg_{β}zβx$ to stand for their opposite in $E_{op}$ by calculating

$fg_{β}zΞ³βg_{β}f_{β}zf_{β}hβg_{β}yh_{β²}βx,$where the map $Ξ³$ is one of the structural morphisms expressing pseudofunctoriality of $E_{β}(β).$

_β,_ : β {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
$EB$
are *dependent paths* over the corresponding laws in
$B.$
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_{β}yβx$ and the composite

$(fid)_{β}yΞ³βid_{β}f_{β}yid_{β}hβid_{β}xΟβx,$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
$fid=f$
in
$B,$
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_{β²},$
we obtain a vertical map
$f_{β²β}xβf_{β}x,$
which we call the `adjust`

ment induced by
$p.$
The explicit definition below is identical to transporting the identity
map
$f_{β}xβf_{β}x$
along
$p,$
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 `adjust`

ment induced by the
algebraic laws of
$B$
with the pseudofunctoriality witnesses of
$E.$

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 Ξ³β

## 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' .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
$E.$
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
$E$
to
$E_{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
$Eβs$
base change, itβs not surprising that
$E_{op}$
is itself a fibration.
Indeed, if we have
$f:aβb$
and
$yb,$
a Cartesian lift of
$y$
along
$f,$
*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) } }

Note that, strictly speaking, the construction of opposite categories can not be extended to a pseudofunctor $CatβCat:$ While the opposite of a functor goes in the same direction as the original (i.e.Β $F:CβD$ is taken to $F_{op}:C_{op}βD_{op}),$ the opposite of a

*natural transformation*has reversed direction β the dual of $Ξ·:FβG$ is $Ξ·_{op}:G_{op}βF_{op}.$ To capture this, the βopposite category functorβ would need to be typed $CatβCat_{co}$ instead, indicating that it reverses 2-cells.However, because the domain $B_{op}$ is locally discrete, all of its 2-cells are isomorphisms. Therefore, the pseudofunctor classified by a given fibration factors through the

*homwise core*of $Cat$ β and the construction of opposite categories restricts to a map $Cat_{core}βCat_{core}.$β©οΈ

## References

- Sterling, Jonathan, and Carlo Angiuli. 2022. βFoundations of Relative Category Theory.β https://www.jonmsterling.com/frct-003I.xml.
- Streicher, Thomas. 2023. βFibered Categories Γ La Jean BΓ©nabou.β https://arxiv.org/abs/1801.02927.