open import Cat.Instances.Functor
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning as Dr

module
  Cat.Displayed.Instances.Pullback
    {o β„“ oβ€² β„“β€² oβ€²β€² β„“β€²β€²}
    {X : Precategory o β„“} {B : Precategory oβ€² β„“β€²}
    (F : Functor X B)
    (E : Displayed B oβ€²β€² β„“β€²β€²)
  where

Pullback of a displayed categoryπŸ”—

If we have a category EE displayed over BB, then a functor F:Xβ†’BF : X \to B defines a (contravariant) β€œchange-of-base” action, reasulting in a category Fβˆ—(E)F^*(E) displayed over XX.

The reason for this contravariance is the following: A category displayed over XX must have a XX-indexed space of objects; But our category EE has a BB-indexed space of objects. Fortunately, FF gives us a map x↦F0(x)x \mapsto F_0(x) which allows us to convert our XX-indices to BB-indices. The same goes for indexing the displayed Hom\hom-sets.

Change-of-base : Displayed X oβ€²β€² β„“β€²β€²
Change-of-base .Ob[_] x      = E.Ob[ Fβ‚€ x ]
Change-of-base .Hom[_] f x y = E.Hom[ F₁ f ] x y
Change-of-base .Hom[_]-set f = E.Hom[ F₁ f ]-set
Change-of-base .idβ€²          = hom[ sym F-id ] E.idβ€²
Change-of-base ._βˆ˜β€²_ fβ€² gβ€²   = hom[ sym (F-∘ _ _) ] (fβ€² E.βˆ˜β€² gβ€²)

Proving that the pullback Fβˆ—(E)F^*(E) is indeed a displayed category is a bit trickier than it might seem β€” we must adjust the identity and composites in EE by the paths witnessing functoriality of FF, and this really throws a spanner in the works β€” but the handy displayed category reasoning combinators are here to help.

Change-of-base .idrβ€² {f = f} fβ€² = to-pathp $
  hom[ ap F₁ (X.idr f) ] (hom[ F-∘ _ _ ]⁻ (fβ€² E.βˆ˜β€² hom[ F-id ]⁻ _)) β‰‘βŸ¨ hom[]⟩⟨ smashr _ _ βŸ©β‰‘
  hom[ ap F₁ (X.idr f) ] (hom[] (fβ€² E.βˆ˜β€² E.idβ€²))                    β‰‘βŸ¨ hom[]-βˆ™ _ _ βŸ©β‰‘
  hom[] (fβ€² E.βˆ˜β€² E.idβ€²)                                             β‰‘βŸ¨ cancel _ _ (E.idrβ€² fβ€²) βŸ©β‰‘
  fβ€²                                                                ∎

Change-of-base .idlβ€² fβ€² = to-pathp $
  hom[ ap F₁ (X.idl _) ] (hom[ F-∘ _ _ ]⁻ (hom[ F-id ]⁻ _ E.βˆ˜β€² fβ€²)) β‰‘βŸ¨ hom[]⟩⟨ smashl _ _ βŸ©β‰‘
  hom[ ap F₁ (X.idl _) ] (hom[] (E.idβ€² E.βˆ˜β€² fβ€²))                    β‰‘βŸ¨ hom[]-βˆ™ _ _ βŸ©β‰‘
  hom[] (E.idβ€² E.βˆ˜β€² fβ€²)                                             β‰‘βŸ¨ cancel _ _ (E.idlβ€² fβ€²) βŸ©β‰‘
  fβ€²                                                                ∎

Change-of-base .assocβ€² fβ€² gβ€² hβ€² = to-pathp $
  hom[ ap F₁ _ ] (hom[ F-∘ _ _ ]⁻ (fβ€² E.βˆ˜β€² hom[ F-∘ _ _ ]⁻ (gβ€² E.βˆ˜β€² hβ€²)))   β‰‘βŸ¨ hom[]⟩⟨ smashr _ _ βŸ©β‰‘
  hom[] (hom[] (fβ€² E.βˆ˜β€² gβ€² E.βˆ˜β€² hβ€²))                                        β‰‘βŸ¨ hom[]-βˆ™ _ _ βŸ©β‰‘
  hom[ (ap (_ B.∘_) _ βˆ™ sym (F-∘ _ _)) βˆ™ ap F₁ _ ] (fβ€² E.βˆ˜β€² gβ€² E.βˆ˜β€² hβ€²)     β‰‘βŸ¨ weave _ _ _ (E.assocβ€² fβ€² gβ€² hβ€²) βŸ©β‰‘
  hom[ ap (B._∘ _) (sym (F-∘ _ _)) βˆ™ sym (F-∘ _ _) ] ((fβ€² E.βˆ˜β€² gβ€²) E.βˆ˜β€² hβ€²) β‰‘Λ˜βŸ¨ smashl _ _ βŸ©β‰‘Λ˜
  hom[ sym (F-∘ _ _) ] (hom[ sym (F-∘ _ _) ] (fβ€² E.βˆ˜β€² gβ€²) E.βˆ˜β€² hβ€²)          ∎