Reindexing a displayed category

[maxsnew]

If you have a category E displayed over D and a functor F : C -> D you can pull E back along F to get a category F^*E displayed over C. This is pretty easy to define except for actually proving the displayed category laws:

module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
  (F : Functor C D) (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ') where
  open Functor
  open Categoryᴰ
  module Dᴰ = Categoryᴰ Dᴰ

  reindex : Categoryᴰ C ℓDᴰ ℓDᴰ'
  reindex .ob[_] c = Dᴰ.ob[ F ⟅ c ⟆ ]
  reindex .Hom[_][_,_] f d d' = Dᴰ.Hom[ F ⟪ f ⟫ ][ d , d' ]
  reindex .idᴰ {p = d} = transport (λ i → Dᴰ [ F .F-id (~ i) ][ d , d ]) (Dᴰ.idᴰ {p = d})
  reindex ._⋆ᴰ_ {f = f}{g = g}{xᴰ = xᴰ}{zᴰ = zᴰ} fᴰ gᴰ =
    transport (λ i → Dᴰ [ F .F-seq f g (~ i) ][ xᴰ , zᴰ ]) (fᴰ Dᴰ.⋆ᴰ gᴰ)
  reindex .⋆IdLᴰ fᴰ = {!!}
  reindex .⋆IdRᴰ = {!!}
  reindex .⋆Assocᴰ = {!!}
  reindex .isSetHomᴰ = Dᴰ.isSetHomᴰ

The laws are a bit of nasty cubical stuff, but you can base the proof off of the 1lab: https://1lab.dev/Cat.Displayed.Instances.Pullback.html#pullback-of-a-displayed-category

[maxsnew]

Closing because this was already implemented upstream: https://github.com/agda/cubical/blob/master/Cubical/Categories/Displayed/Properties.agda