Algebras for pointed endofunctors and Kelly's transfinite construction (

UniMath#1928)

This is my first contribution to UniMath so feedback is appreciated.

It consists contains the construction of a free algebra for a
well-pointed endofunctor and some relationships between well-pointed
endofunctors and reflective subcategories.

I did my best to reuse existing definitions, however I haven't used
PointedFunctors.v, and instead just have my own `pointed_endofunctor`
definition, since I had issues with `F : category_Ptd C` not coercing to
a `functor C C`. Using `ptd_obj C` works, but this naming is obscure in
my opinion - I would not guess that it's a functor.

I followed `UniMath/CategoryTheory/Monads/MonadAlgebras.v` to implement
the definition of the category of algebras for a pointed endofunctor.
Everything is much the same, except we have only 1 algebra law, not 2.
I'm not sure if I should also be capitalising like `MonadAlg`? Also
worth noting is I've called them `pointed_algebras`, which may imply the
algebra X has a point (1 --> X) rather than the endofunctor F, but I
don't there's a better alternative.

The relationship to reflective subcategories hasn't been made concrete.
I use the term `reflective` in comments and the final theorem, but I'm
essentially just using a fully-faithful right adjoint in the code.

UniMath/CONTENTS.md

@@ -490,6 +490,7 @@ The packages and files are listed here in logical order: each file depends only
    - [Inductives/LambdaCalculus.v](CategoryTheory/Inductives/LambdaCalculus.v)
    - [Inductives/PropositionalLogic.v](CategoryTheory/Inductives/PropositionalLogic.v)
    - [CategoricalRecursionSchemes.v](CategoryTheory/CategoricalRecursionSchemes.v)
+   - [PointedFunctorAlgebras.v](CategoryTheory/PointedFunctorAlgebras.v)
    - [DisplayedCats/Equivalences.v](CategoryTheory/DisplayedCats/Equivalences.v)
    - [DisplayedCats/EquivalenceOverId.v](CategoryTheory/DisplayedCats/EquivalenceOverId.v)
    - [DisplayedCats/DisplayedCatEq.v](CategoryTheory/DisplayedCats/DisplayedCatEq.v)

UniMath/CategoryTheory/.package/files

@@ -311,6 +311,7 @@ Inductives/Trees.v
 Inductives/LambdaCalculus.v
 Inductives/PropositionalLogic.v
 CategoricalRecursionSchemes.v
+PointedFunctorAlgebras.v
 
 DisplayedCats/Equivalences.v
 DisplayedCats/EquivalenceOverId.v