Tom de Jong<p>I'm happy to report that my expository note (<a href="https://arxiv.org/abs/2408.11501" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2408.11501</span><span class="invisible"></span></a>), which has previously been kindly mentioned on here by <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@ecavallo" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>ecavallo</span></a></span> and <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@jonmsterling" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>jonmsterling</span></a></span>, has been accepted to the TYPES 2024 post-proceedings 🙂</p><p><a href="https://mathstodon.xyz/tags/typetheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>typetheory</span></a> <a href="https://mathstodon.xyz/tags/formalization" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalization</span></a></p>