Displayed Category of Displayed Functors

[maxsnew]

It would be useful for getting a better definition of displayed universal properties in terms of presheaves to have a displayed category of displayed functors over the category of functors. So C^d : DisplayedCat C and D^d : DisplayedCat D we would construct FUNCTOR^D C^d D^d : DisplayedCat (FUNCTOR C D).

[hejohns]

Working on this.

FUNCTORᴰ : Categoryᴰ (FUNCTOR C D)  _ _
FUNCTORᴰ .ob[_] F = Functorᴰ F Cᴰ Dᴰ
FUNCTORᴰ .Hom[_][_,_] {x = F} {y = G} α Fᴰ Gᴰ = NatTransᴰ α Fᴰ Gᴰ
FUNCTORᴰ .idᴰ {x = F} {p = Fᴰ} = idTransᴰ F Fᴰ
FUNCTORᴰ ._⋆ᴰ_ {x = F} {y = G} {z = H} {f = α} {g = β} {xᴰ = Fᴰ} {yᴰ = Gᴰ} {zᴰ = Hᴰ} αᴰ βᴰ = seqTransᴰ αᴰ βᴰ

were routine, I think, but I'm stuck on

FUNCTORᴰ .⋆IdLᴰ

which requires some version of makeNatTransPathᴰ, which I'm stuck on so I've asked on zulip about it.

[hejohns]

69 should close this