Ordinary inductive types is initial algebras for free monads. However, HITs are not initial algebras for endofunctors but presented monads.

From nLab, initial algebra of a presentable (infinity,1)-monad and blog comment, Peter and Mike constructed models for HITs in their paper.

Where is the reference or link for this paper?


https://arxiv.org/abs/1705.07088 . I've updated the nLab page.

There are also some slides available at my web page.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.