Indexed Polynomial Functor

An indexed polynomial functor is an extra-dependent version of a Polynomial Functor. We can think of these as "multivariate" polynomial functors.

These polynomials can be defined in any category as a sort of span

I←Bβ†’Aβ†’J←𝐼𝐡→𝐴→𝐽\par I\leftarrow B\rightarrow A\rightarrow J

But we typically want to view the series of maps B β†’ A β†’ J β†’ 𝐡 𝐴 β†’ 𝐽 B\to A\to J as a tower of Bundles. If we specialize to Category of Sets, we get the following definition.

record IxPoly (I J : Type) : Type₁ where
  no-eta-equality
  field
    Shape : J β†’ Type
    Pos : βˆ€ {j} β†’ Shape j β†’ Type
    ix : βˆ€ {j} {s : Shape j} β†’ Pos s β†’ I

We also recall the definition of a Morphism of Indexed Polynomial Functors:

record IxPoly-hom {I J I' J'} (u : I β†’ I') (v : J β†’ J') (P : IxPoly I J) (Q : IxPoly I' J') : Type₁ where
  field
    shape : βˆ€ {j} β†’ P .Shape j β†’ Q .Shape (v j)
    pos   : βˆ€ {j} (s : P .shape j) β†’ Q .Pos (shape s) β†’ P .Pos s
    index : βˆ€ {j} (s : Shape j) (q# : Q .Pos (shape s)) β†’ u (P .ix (pos s q#)) ≑ Q .ix q#

As Fibrations

With a bit of massaging, we see that the Shape field comes from the Family Fibration, and Pos comes from the Fibrewise Opposite of the Family Fibration on a Total Category; EG: the start of a Dialectica Category Fam ⁒ ( Sets ) ∘ Fam ⁒ ( ∫ Fam ⁒ ( Sets ) ) op Fam Sets Fam superscript Fam Sets op \mathrm{Fam}(\mathrm{Sets})\circ\mathrm{Fam}(\int\mathrm{Fam}(\mathrm{Sets}))^% {\mathrm{op}} .

However, ix is rather odd; it looks like some sort of "cofamily fibration?"

We do have the start of a construction:

Graded : βˆ€ {ΞΊ} β†’ Displayed (B Γ—αΆœ Sets ΞΊ) {!!} {!!}
Graded .Ob[_] (X , S) = E.Ob[ X ] β†’ ⌞ S ⌟
Graded .Hom[_] (h , f) s t = βˆ€ {y'} β†’ f (s (h E.^* y')) ≑ t y'
Graded .Hom[_]-set = {!!}
Graded .id' {X , S} {s} = ap s ?
Graded ._∘'_ = {!!}
Graded .idr' = {!!}
Graded .idl' = {!!}
Graded .assoc' = {!!}

However, this requires that the underlying fibration is Split.

There is a more general construction of the form:

Graded : Displayed B (oe βŠ” β„“e) (oe βŠ” β„“e)
Graded .Ob[_] X = Functor (Fibre E X) (Fibre F X)
Graded .Hom[_] f P Q = P F∘ E.base-change f => F.base-change f F∘ Q

However, this is not quite the same; we could try and use a discrete category here, but this doesn't really capture what is going on. Moreover, note that these graditions will totally trash our morphisms in β„° β„° \mathcal{E} .

I think a more useful perspective is to curry the function ix to get ix : Ξ£ (j : J) (s : Shape j) (Pos p) β†’ I; this is a bundle map in the category of sets. Moreover, one typically talks about indexed polynomials in a Locally Cartesian Closed Category; both of these settings are Comprehension Categories.

This feels much more plausible:

Gradings : Displayed (∫ E Γ—αΆœ B) β„“b β„“b
Gradings .Ob[_] ((Ξ“ , Ξ±) , X) = B.Hom (Ξ“ E.β¨Ύ Ξ±) X
Gradings .Hom[_] (total-hom v f , u) s t = u B.∘ s ≑ t B.∘ (v E.β¨ΎΛ’ f)
Gradings .Hom[_]-set _ _ _ = hlevel 2
Gradings .id' = B.idl _ βˆ™ B.intror E.sub-id
Gradings ._∘'_ p q =
  B.pullr q
  βˆ™ B.extendl p
  βˆ™ apβ‚‚ B._∘_ refl (sym (E.sub-∘))
Gradings .idr' _ = prop!
Gradings .idl' _ = prop!
Gradings .assoc' _ _ _ = prop!

This is exactly a Comma Category for the identity functor and the total space functor obtained from a comprehension category! Note that this goes in the opposite direction of Artin Gluing, which forms a comma category π’ž ↓ Ο• ↓ π’ž italic-Ο• \mathcal{C}\downarrow\phi .

However, this doesn't quite line up with how indexed polynomial morphisms work; this doesn't give us the required "twist": instead, we want to have our morphisms be something like u B.∘ s B.∘ (B.id E.β¨ΎΛ’ f) ≑ t B.∘ (v E.β¨ΎΛ’ E.Ο€* v Ξ²). This can be done neatly by having ourselves be displayed over the total category of the Fibrewise Opposite.

Random Junk

Gradings : Displayed (∫ E^op Γ—αΆœ B) β„“b β„“b
Gradings .Ob[_] ((Ξ“ , Ξ±) , X) = B.Hom (Ξ“ E.β¨Ύ Ξ±) X
Gradings .Hom[_] {(Ξ“ , Ξ±) , X} {(Ξ” , Ξ²) , Y} (total-hom v f , u) s t =
  u B.∘ s B.∘ (B.id E.β¨ΎΛ’ f) ≑ t B.∘ (v E.β¨ΎΛ’ E.Ο€* v Ξ²)
Gradings .Hom[_]-set _ _ _ = hlevel 2
Gradings .id' {(Ξ“ , Ξ±) , X} {s} =
  B.id B.∘ s B.∘ (B.id E.β¨ΎΛ’ E.Ο€* B.id Ξ±) β‰‘βŸ¨ B.idl _ ⟩
  s B.∘ (B.id E.β¨ΎΛ’ E.Ο€* B.id Ξ±) ∎
Gradings ._∘'_ {(Ξ“ , Ξ±) , X} {(Ξ” , Ξ²) , Y} {(Θ , Ξ³) , Z} {r} {s} {t} {total-hom v f , u} {total-hom w g , x} p q =
  (u B.∘ x) B.∘ r B.∘ ⌜ B.id  E.β¨ΎΛ’ E.hom[] (g E.∘' E.hom[] (E.Ο€*.universal' _ (f E.∘' E.Ο€* w (v E.^* Ξ³)) E.∘' _)) ⌝
    β‰‘βŸ¨ ap! (apβ‚‚ E._β¨ΎΛ’_ (sym (B.idl _)) (E.unwrap (B.idl _))) ⟩
  (u B.∘ x) B.∘ r B.∘ ⌜ (B.id B.∘ B.id) E.β¨ΎΛ’ (g E.∘' E.hom[] (E.Ο€*.universal' B.id-comm (f E.∘' E.Ο€* w (v E.^* Ξ³)) E.∘' _)) ⌝
    β‰‘βŸ¨ ap! E.sub-∘ ⟩
  (u B.∘ x) B.∘ r B.∘ (B.id E.⨾˒ g) B.∘ (B.id E.⨾˒ E.hom[] _)
    β‰‘βŸ¨ B.pullr (B.pulll3 q) ⟩
  u B.∘ (s B.∘ (w E.β¨ΎΛ’ E.Ο€* w Ξ²)) B.∘ (B.id E.β¨ΎΛ’ E.hom[] (E.Ο€*.universal' B.id-comm (f E.∘' E.Ο€* w (v E.^* Ξ³)) E.∘' _))
    β‰‘βŸ¨ ap (u B.∘_) (B.pullr (sym (E.sub-∘))) ⟩
  u B.∘ s B.∘ (w B.∘ B.id E.β¨ΎΛ’ E.Ο€* w Ξ² E.∘' E.hom[] (E.Ο€*.universal' B.id-comm (f E.∘' E.Ο€* w (v E.^* Ξ³)) E.∘' _))
    β‰‘βŸ¨ apβ‚‚ (Ξ» Ο• ψ β†’ u B.∘ s B.∘ (Ο• E.β¨ΎΛ’ ψ)) B.id-comm (E.cast[] \( E.unwrapr _ E.βˆ™[] E.pulll[] B.id-comm (E.Ο€*.commutesp B.id-comm _) E.βˆ™[] E.pullr[] (B.idr _) (E.Ο€*.commutesp (B.idr _) (E.Ο€*.universal w (E.Ο€* (v B.∘ w) Ξ³)))) ⟩
  u B.∘ s B.∘ ⌜ B.id B.∘ w E.β¨ΎΛ’ f E.∘' E.Ο€*.universal w (E.Ο€* (v B.∘ w) Ξ³) ⌝
    β‰‘βŸ¨ ap (Ξ» Ο• β†’ u B.∘ s B.∘ Ο•) (E.sub-∘) ⟩
  u B.∘ s B.∘ (B.id E.β¨ΎΛ’ f) B.∘ (w E.β¨ΎΛ’ E.Ο€*.universal w (E.Ο€* (v B.∘ w) Ξ³))
    β‰‘βŸ¨ B.pulll3 p ⟩
  (t B.∘ (v E.β¨ΎΛ’ E.Ο€* v Ξ³)) B.∘ (w E.β¨ΎΛ’ E.Ο€*.universal w (E.Ο€* (v B.∘ w) Ξ³))
    β‰‘βŸ¨ B.pullr (sym E.sub-∘ βˆ™ ap (v B.∘ w E.β¨ΎΛ’_) (E.Ο€*.commutes w (E.Ο€* (v B.∘ w) Ξ³))) ⟩
  t B.∘ (v B.∘ w E.β¨ΎΛ’ E.Ο€* (v B.∘ w) Ξ³)
    ∎
Gradings .idr' _ = prop!
Gradings .idl' _ = prop!
Gradings .assoc' _ _ _ = prop!

References