Skip to main content
3 of 3
punctuation
Martin Sleziak
  • 4.7k
  • 4
  • 35
  • 40

Models for Higher Inductive Types in Homotopy Type Theory

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?