Redo definition of category of polynomial signatures

[Vtec234]

The current definition of the category of polynomial signatures bundles a choice of pullback object as part of the data of a hom:

Poly/Poly/UvPoly/Basic.lean

Line 197 in 914d9b7

structure Hom {F D : C} (P : UvPoly E B) (Q : UvPoly F D) where

We (@Jlh18) think this will not support a definition of a 1-category: assoc (possibly also id_comp) will not be provable for composition because the choice of pullback will differ in general between the two ways to reassociate.

A potential better approach is to give the data of (pseudocode below)

structure Hom {F D : C} (P : UvPoly E B) (Q : UvPoly F D) where
  δ : B ⟶ D
  ρ : forall (Pb : Pullback Q.p δ), Pb ⟶ E
  ρ_coherence : forall (Pb1 Pb2), pbIso Pb1 Pb2 >> ρ Pb1 =  ρ Pb2

Thanks to @FernandoChu for the suggestion.