Extending Categories.Object.NaturalNumbers.Properties.F-Algebras with the algebras corresponding to PNNOs
Adding Categories.Object.NaturalNumbers.Properties.Parametrized (not sure about the naming) to show that in CCCs NNO yields a ParametrizedNNO
Furthermore I needed two lemmas that I added to Categories.Category.BinaryProducts, Categories.Object.Exponential and Categories.Category.CartesianClosed, these are:
∘swap-inj : f ∘ swap ≈ g ∘ swap → f ≈ g (plus swap∘-inj)
λ-inj : λg f ≈ λg g → f ≈ g
I thought they are convenient to have so I added them to the respective files, but I can also remove them and use them locally.
I added parametrized natural numbers objects (definition 2.2 https://ncatlab.org/nlab/show/natural+numbers+object#withparams).
This entails:
Categories.Object.NaturalNumbers.ParametrizedCategories.Object.NaturalNumbers.Properties.F-Algebraswith the algebras corresponding to PNNOsCategories.Object.NaturalNumbers.Properties.Parametrized(not sure about the naming) to show that in CCCsNNOyields aParametrizedNNOFurthermore I needed two lemmas that I added to
Categories.Category.BinaryProducts,Categories.Object.ExponentialandCategories.Category.CartesianClosed, these are:∘swap-inj : f ∘ swap ≈ g ∘ swap → f ≈ g(plusswap∘-inj)λ-inj : λg f ≈ λg g → f ≈ gI thought they are convenient to have so I added them to the respective files, but I can also remove them and use them locally.