open import Cat.Functor.Equivalence.Path
open import Cat.Functor.Equivalence
open import Cat.Displayed.Fibre
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning as DR

module Cat.Displayed.Total.Op where

open Functor
open Total-hom


# Total oppositesπ

Opposites of displayed categories are somewhat subtle, as there are multiple constructions that one could reasonably call the βoppositeβ. The most obvious construction is to construct a new displayed category over we call this category the total opposite of

module _ {o β o' β'} {β¬ : Precategory o β} (β° : Displayed β¬ o' β') where
open Precategory β¬
open Displayed β°

_^total-op : Displayed (β¬ ^op) o' β'
_^total-op .Displayed.Ob[_] x = Ob[ x ]
_^total-op .Displayed.Hom[_] f x y = Hom[ f ] y x
_^total-op .Displayed.Hom[_]-set f x y = Hom[ f ]-set y x
_^total-op .Displayed.id' = id'
_^total-op .Displayed._β'_ f' g' = g' β' f'
_^total-op .Displayed.idr' f' = idl' f'
_^total-op .Displayed.idl' f' = idr' f'
_^total-op .Displayed.assoc' f' g' h' = symP $assoc' h' g' f'  Much like the opposite of categories, the total opposite is an involution on displayed categories. total-op-involution : β {o β o' β'} {β¬ : Precategory o β} {β° : Displayed β¬ o' β'} β (β° ^total-op) ^total-op β‘ β° total-op-involution {β° = β°} = path where open Displayed path : (β° ^total-op) ^total-op β‘ β° path i .Ob[_] = β° .Ob[_] path i .Hom[_] = β° .Hom[_] path i .Hom[_]-set = β° .Hom[_]-set path i .id' = β° .id' path i ._β'_ = β° ._β'_ path i .idr' = β° .idr' path i .idl' = β° .idl' path i .assoc' = β° .assoc'  {-# REWRITE total-op-involution #-}  ## The total opposites and total categoriesπ The reason we refer to this construction as the total opposite is that its total is equal to the opposite of the total category! To show this, we first need to prove some lemmas relating the morphisms of the total category of the total opposite to those in the opposite of the total category. These functions are essentially the identity function, but we canβt convince Agda that this is the case due to definitional equality reasons. total-opβtotal-hom : β {o β o' β'} {β¬ : Precategory o β} {β° : Displayed β¬ o' β'} β β {x y} β Total-hom (β° ^total-op) x y β Total-hom β° y x total-opβtotal-hom f = total-hom (f .hom) (f .preserves) total-homβtotal-op : β {o β o' β'} {β¬ : Precategory o β} {β° : Displayed β¬ o' β'} β β {x y} β Total-hom β° y x β Total-hom (β° ^total-op) x y total-homβtotal-op f = total-hom (f .hom) (f .preserves)  Furthermore, these two maps constitute an equivalence, and thus yield an equality of types via univalence. total-opβtotal-hom-is-equiv : β {o β o' β'} {β¬ : Precategory o β} {β° : Displayed β¬ o' β'} β β {x y} β is-equiv (total-opβtotal-hom {β° = β°} {x = x} {y = y}) total-opβtotal-hom-is-equiv = is-isoβis-equiv$ iso total-homβtotal-op (Ξ» _ β refl) (Ξ» _ β refl)

total-opβ‘total-hom
: β {o β o' β'} {β¬ : Precategory o β} {β° : Displayed β¬ o' β'}
β β {x y} β Total-hom (β° ^total-op) x y β‘ Total-hom β° y x
total-opβ‘total-hom = ua \$ total-opβtotal-hom , total-opβtotal-hom-is-equiv


We can use the fact that total-opβtotal-hom is an equivalence to construct an isomorphism of precategories.

β«total-opββ«^op
: β {o β o' β'} {β¬ : Precategory o β} (β° : Displayed β¬ o' β')
β Functor (β« (β° ^total-op)) ((β« β°) ^op)
β«total-opββ«^op _ .Fβ x = x
β«total-opββ«^op _ .Fβ f = total-opβtotal-hom f
β«total-opββ«^op _ .F-id = refl
β«total-opββ«^op _ .F-β _ _ = refl

β«total-opββ«^op
: β {o β o' β'} {β¬ : Precategory o β} (β° : Displayed β¬ o' β')
β is-precat-iso (β«total-opββ«^op β°)
β«total-opββ«^op β° .is-precat-iso.has-is-ff = total-opβtotal-hom-is-equiv
β«total-opββ«^op β° .is-precat-iso.has-is-iso = id-equiv


Finally, we show that this extends to an equality of categories.

β«total-opβ‘β«^op
: β {o β o' β'} {β¬ : Precategory o β} (β° : Displayed β¬ o' β')
β β« (β° ^total-op) β‘ (β« β°) ^op
β«total-opβ‘β«^op β° =
Precategory-path
(β«total-opββ«^op β°)
(β«total-opββ«^op β°)


# Functors between fibresπ

If there is a functor between the fibres of a displayed category then we also obtain a functor between the fibres of the total opposite of

fibre-functor-total-op
: β {o β o' β'} {β¬ : Precategory o β} {β° : Displayed β¬ o' β'} {x y}
β Functor (Fibre β° x) (Fibre β° y)
β Functor (Fibre (β° ^total-op) x) (Fibre (β° ^total-op) y)
fibre-functor-total-op F .Fβ = F .Fβ
fibre-functor-total-op F .Fβ = F .Fβ
fibre-functor-total-op F .F-id = F .F-id
fibre-functor-total-op {β° = β°} F .F-β f g =
ap (F .Fβ) (DR.reindex β° _ _ ) Β·Β· F .F-β g f Β·Β· DR.reindex β° _ _

fibre-functor-total-op-total-op
: β {o β o' β'} {β¬ : Precategory o β} {β° : Displayed β¬ o' β'} {x y}
β {F : Functor (Fibre β° x) (Fibre β° y)}
β fibre-functor-total-op (fibre-functor-total-op F) β‘ F
fibre-functor-total-op-total-op {F = F} i .Fβ = F .Fβ
fibre-functor-total-op-total-op {F = F} i .Fβ = F .Fβ
fibre-functor-total-op-total-op  {F = F} i .F-id = F .F-id
fibre-functor-total-op-total-op {β° = β°} {y = y} {F = F} i .F-β f g =
is-propβpathp (Ξ» i β Hom-set  _ _ _ (F .Fβ f β F .Fβ g))
((fibre-functor-total-op (fibre-functor-total-op F)) .F-β f g)
(F .F-β f g)
i
where open Precategory (Fibre β° y)

{-# REWRITE fibre-functor-total-op-total-op #-}