2
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ This question is asked and (briefly) answered in part 1, 1h21'35" $\endgroup$
    – L. Garde
    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$ Jul 30, 2022 at 4:23

1 Answer 1

2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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