6
$\begingroup$

I'm new to HoTT. I've started reading the current version of the HoTT book.

On page 12, it mentions as an open problem whether HoTT + univalence has the “homotopy canonicity” property, i.e., every closed term of natural number type is propositionally equal to a canonical form (as opposed to canonicity, which requires a definitional equality).

I found the page homotopy canonicity on the nLab which mentions an unpublished proof by Kapulkin and Sattler that HoTT + univalence does enjoy homotopy canonicity. However, the talk is from 2019 and I did not find a publication of this proof since then.

What is the state of this conjecture?

Improve this question
$\endgroup$
2
  • $\begingroup$ Thanks! I guess you could post that as an answer so I can accept it. (The paper is way over my head right now, so I'll just trust the result.) $\endgroup$
    – Jean Abou Samra
    Commented Nov 20 at 17:36
  • 2
    $\begingroup$ I've updated the nLab page now. $\endgroup$
    – Naïm Favier
    Commented Nov 20 at 17:53

1 Answer 1

Reset to default
7
$\begingroup$

I believe the state of the art in November 2024 is Rafaël Bocquet, 2023, Strict Rezk completions of models of HoTT and homotopy canonicity.

Improve this answer
$\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.