5
$\begingroup$

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?

$\endgroup$

1 Answer 1

6
$\begingroup$

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

There are also some slides available at my web page.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .