sassa_nf

Yes. The difference is that we don't attempt to make everything church-encoded. Like, hylo takes a co-algebra for f, but church-encoded fixed point of f does not have f. So Tr needs to be introduced. This is not the same as "if your type is a functor, hylo will work". It really is "create a polynomial functor for your church-encoded type, and then hylo will work".