implementing (co)datatype

Stream: general

[Asei Inoue]

Have you read this paper?
see: https://lean-forward.github.io/pubs/keizer_msc_thesis.pdf
title: Implementing a definitional (co)datatype package in Lean 4, based on quotients of polynomial functors

I have not read the whole of this, but this seems to be really good. I think we should have this data command in Mathlib, maybe...?

[Henrik Böving]

It exists here as a library https://github.com/alexkeizer/QpfTypes

[Asei Inoue]

ok I know this library, but I wanted to say this is worth to be known widely...
I'm Sorry

[Vasilii Nesterov]

Just curious, what do you need it for?

[Asei Inoue]

to implement histomorphism