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 Martin-Löf type theory?
$\begingroup$
$\endgroup$
2
asked Jul 18, 2022 at 23:33
-
$\begingroup$ This question is asked and (briefly) answered in part 1, 1h21'35" $\endgroup$– L. GardeCommented Jul 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 work-in-progress on stackexchange. You'd probably have gotten a faster and better answer by just emailing me (or Thorsten or Ambrus) directly. $\endgroup$– Mike ShulmanCommented Jul 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.
answered Jul 30, 2022 at 2:28