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 #-}