Categories.Object.NaturalNumbers.Parametrized takes a CartesianCategory which can be hard to use, so I've unbundled things.
I also split Categories.Object.NaturalNumbers.Properties.F-Algebras in two, adding Categories.Object.NaturalNumbers.Parametrized.Properties.F-Algebras and removed the anonymous module to move all parameters to the outer module (for ease of use).
Lastly, I've replaced the locally defined functors Maybe and coproductF with the corresponding instances of -+-.
Categories.Object.NaturalNumbers.Parametrizedtakes aCartesianCategorywhich can be hard to use, so I've unbundled things.I also split
Categories.Object.NaturalNumbers.Properties.F-Algebrasin two, addingCategories.Object.NaturalNumbers.Parametrized.Properties.F-Algebrasand removed the anonymous module to move all parameters to the outer module (for ease of use).Lastly, I've replaced the locally defined functors
MaybeandcoproductFwith the corresponding instances of-+-.