Since we have different representations of free structures and proofs of their freeness we can use them to develop some applications! Some ideas:
Representation independence: take two different representations and convert back and forth between them using the universal property
Normalization: show that every representation has a normal form, by defining an nf function using the universal property and NbE, and then showing it has good properties (esp. interesting for free commutative monoids or bags or multisets) (related: Frex project, see Nathan's thesis)
Monads and algebras: for each free structure, define the monad structure and categories of algebras for the monad etc. using the Free interface
Combinatorics of free commutative monoids: there are many such things in my paper, some of them partially formalised, but this requires much more than just freeness
Since we have different representations of free structures and proofs of their freeness we can use them to develop some applications! Some ideas:
nffunction using the universal property and NbE, and then showing it has good properties (esp. interesting for free commutative monoids or bags or multisets) (related: Frex project, see Nathan's thesis)