{-# 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 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 _[_]

Source

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:

private
: β {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
: β {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

: β {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 with the pseudofunctoriality witnesses of

  adjust-idr
: β {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' .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 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π

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 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 β©οΈ