Programming Languages Delft<p>Master thesis by Arnoud van der Leer: Universal Algebra, Univalent Foundations and the Untyped λ-Calculus</p><p>"This thesis studies and expands upon Martin Hyland’s paper ‘Classical lambda calculus in modern dress’. [...] The thesis translates Hyland’s paper from set theory with classical logic to univalent foundations, and showcases where subtleties arise in such a translation."</p><p><a href="https://repository.tudelft.nl/record/uuid:e6582866-9c0d-4a13-8eda-42c25e0deba4" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">repository.tudelft.nl/record/u</span><span class="invisible">uid:e6582866-9c0d-4a13-8eda-42c25e0deba4</span></a></p><p><a href="https://akademienl.social/tags/univalentfoundations" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>univalentfoundations</span></a> <a href="https://akademienl.social/tags/hott" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>hott</span></a> <a href="https://akademienl.social/tags/typetheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>typetheory</span></a> <a href="https://akademienl.social/tags/thesis" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>thesis</span></a></p>
101010.pl is one of the many independent Mastodon servers you can use to participate in the fediverse.
101010.pl czyli najstarszy polski serwer Mastodon. Posiadamy wpisy do 2048 znaków.
Administered by:
Server stats:
478active users
101010.pl: About · Status · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.5.0-alpha.1
#UnivalentFoundations
0 posts · 0 participants · 0 posts today
Martin Escardo<p>The HoTT book has a proof that if excluded middle holds then all ordinals are trichotomous, meaning that x < y or x = y or x > y. </p><p>Ohad Kammar gave a better proof. </p><p>Today my colleague Paul Blain Levy improved both the proof and at the same time strengthened the statement: An ordinal is trichotomous if and only if its order is decidable. <br>1/</p><p><a href="https://mathstodon.xyz/tags/hott" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>hott</span></a> <a href="https://mathstodon.xyz/tags/univalentFoundations" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>univalentFoundations</span></a> <a href="https://mathstodon.xyz/tags/constructiveMathematics" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>constructiveMathematics</span></a><br><a href="https://mathstodon.xyz/tags/neutralMathematics" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>neutralMathematics</span></a></p>
TrendingLive feeds
Mastodon is the best way to keep up with what's happening.
Follow anyone across the fediverse and see it all in chronological order. No algorithms, ads, or clickbait in sight.
Create accountLoginDrag & drop to upload