Examples of generating universe polymorphic code?

[gmalecha]

Are there any examples of people using the template monad to generate universe polymorphic code? I was having difficulty generating polymorphic lenses in the lens library: https://github.com/gmalecha/coq-lens/blob/master/theories/Lens.v

[mattam82]

I didn't try, but maybe others did. It could be that we lack some support somewhere, did you have an example of something you want to quote/unquote?