Mike Shulman gave the following set of talks on higher observational type theory earlier this year (part 1, part 2, part 3). However, while he talked about how the identity types are defined and behave in higher observational type theory and how univalence is a theorem in higher observational type theory, he never talked about higher inductive types. So, how are higher inductive types defined in higher observational type theory, and do they behave differently from higher inductive types in MartinLöf type theory?
$\begingroup$
$\endgroup$
2

$\begingroup$ This question is asked and (briefly) answered in part 1, 1h21'35" $\endgroup$– L. GardeJul 23, 2022 at 16:42

4$\begingroup$ Also, FWIW, I don't think it works very well to ask questions about other people's unpublished workinprogress on stackexchange. You'd probably have gotten a faster and better answer by just emailing me (or Thorsten or Ambrus) directly. $\endgroup$– Mike ShulmanJul 30, 2022 at 4:23
Add a comment

1 Answer
$\begingroup$
$\endgroup$
This is work in progress. There are issues with defining ap on the eliminator in the absence of diagonals that will probably make HITs less ergonomic than in cubical type theory, but I have hope that they can be made no less convenient than in Book HoTT.