Tom de Jong<p><span class="h-card" translate="no"><a href="https://mathstodon.xyz/@MartinEscardo" class="u-url mention" rel="nofollow noopener" target="_blank">@<span>MartinEscardo</span></a></span> and I have been working on injective <a href="https://mathstodon.xyz/tags/types" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>types</span></a> in <a href="https://mathstodon.xyz/tags/constructive" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>constructive</span></a> <a href="https://mathstodon.xyz/tags/univalent" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>univalent</span></a> mathematics.</p><p>Last week I gave an informal talk in our group's seminar and I wrote a brief blog post with several pointers in case you'd like to know more: <a href="https://fplunchnott.wordpress.com/2024/10/25/injective-types/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">fplunchnott.wordpress.com/2024</span><span class="invisible">/10/25/injective-types/</span></a></p>
eupolicy.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
This Mastodon server is a friendly and respectful discussion space for people working in areas related to EU policy. When you request to create an account, please tell us something about you.
Administered by:
Server stats:
201active users
eupolicy.social: About · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.4.1
#constructive
0 posts · 0 participants · 0 posts today
Susan Larson ♀️🏳️🌈🏳️⚧️🌈<p><a href="https://mastodon.online/tags/VicePresident" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>VicePresident</span></a> <a href="https://mastodon.online/tags/KamalaHarris" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>KamalaHarris</span></a>' <a href="https://mastodon.online/tags/CodeSwitching" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CodeSwitching</span></a> Is <a href="https://mastodon.online/tags/American" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>American</span></a> As <a href="https://mastodon.online/tags/ApplePie" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ApplePie</span></a> </p><p>Code switching is a common practice within the black community. </p><p>Some conservatives have claimed that this <a href="https://mastodon.online/tags/linguisticshift" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>linguisticshift</span></a> was <a href="https://mastodon.online/tags/evidence" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>evidence</span></a> of <a href="https://mastodon.online/tags/inauthenticity" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>inauthenticity</span></a>, essentially <a href="https://mastodon.online/tags/questioning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>questioning</span></a> Harris’ <a href="https://mastodon.online/tags/blackness" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>blackness</span></a>. Their <a href="https://mastodon.online/tags/confusion" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>confusion</span></a> highlights the need for more <a href="https://mastodon.online/tags/constructive" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>constructive</span></a> <a href="https://mastodon.online/tags/conversations" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>conversations</span></a> on <a href="https://mastodon.online/tags/race" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>race</span></a> and <a href="https://mastodon.online/tags/communication" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>communication</span></a>. </p><p><a href="https://www.levelman.com/kamala-harris-code-switching-american-apple-pie/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">levelman.com/kamala-harris-cod</span><span class="invisible">e-switching-american-apple-pie/</span></a></p>
Martin Escardo<p>Index of selected threads on <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/constructive" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>constructive</span></a> <a href="https://mathstodon.xyz/tags/math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>math</span></a></p><p>* 2022/10/31. Proofs by contradiction.<br><a href="https://mathstodon.xyz/@MartinEscardo/109264034964990196" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109264034964990196</span></a></p><p>* 2022/11/12. Synthetic topology of data types and classical spaces.<br><a href="https://mathstodon.xyz/@MartinEscardo/109332986014534390" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109332986014534390</span></a></p><p>* 2022/11/14. Notions of space.<br><a href="https://mathstodon.xyz/@MartinEscardo/109343930842850773" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109343930842850773</span></a></p><p>* 2022/11/16. Trichotomy of ordinals.<br><a href="https://mathstodon.xyz/@MartinEscardo/109355604029879269" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109355604029879269</span></a></p><p>* 2022/11/22. Birthday present by Tom de Jong.<br><a href="https://mathstodon.xyz/@MartinEscardo/109388875794058555" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109388875794058555</span></a></p><p>* 2022/11/23. Concrete example illustrating that constructive mathematics is more general than classical mathematics.<br><a href="https://mathstodon.xyz/@MartinEscardo/109395006766077334" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109395006766077334</span></a></p><p>* 2022/12/01. Combinatorial game theory.<br><a href="https://mathstodon.xyz/@MartinEscardo/109440314312765877" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109440314312765877</span></a></p><p>* 2022/12/08. Universe polymorphic type systems.<br><a href="https://mathstodon.xyz/@MartinEscardo/109480057029596732" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109480057029596732</span></a></p><p>* 2022/12/08. Why cubical type theory, and why cubical Agda?<br><a href="https://mathstodon.xyz/@MartinEscardo/109480455436886869" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109480455436886869</span></a></p><p>* 2022/12/20. The axiom of choice in HoTT/UF.<br><a href="https://mathstodon.xyz/@MartinEscardo/109546988519874380" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109546988519874380</span></a></p><p>* 2022/12/22. A common generalization of the univalence axiom and the K axiom.<br><a href="https://mathstodon.xyz/@MartinEscardo/109558670025171863" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109558670025171863</span></a></p><p>* 2023/02/03. Defining large numbers without using induction.<br><a href="https://mathstodon.xyz/@MartinEscardo/109802885041067972" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109802885041067972</span></a></p><p>* 2023/02/10. Several kinds of categories in HoTT/UF.<br><a href="https://mathstodon.xyz/@MartinEscardo/109842791175514936" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109842791175514936</span></a></p><p>* 2023/03/03. Universes in type theory as mathematical objects interesting in their own right.<br><a href="https://mathstodon.xyz/@MartinEscardo/109961534132268566" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">109961534132268566</span></a></p><p>* 2023/03/22. Playing rationally against irrational players.<br><a href="https://mathstodon.xyz/@MartinEscardo/110068977445045121" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">110068977445045121</span></a></p><p>* 2023/04/11. What are universes for in HoTT/UF?<br><a href="https://mathstodon.xyz/@MartinEscardo/110181596099423100" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">110181596099423100</span></a></p><p>* 2023/06/02. Ayberk's predicative version of the patch locale of a Stone locale.<br><a href="https://mathstodon.xyz/@MartinEscardo/110476555405397697" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">110476555405397697</span></a></p><p>* 2023/06/07. Github project TypeTopology.<br><a href="https://mathstodon.xyz/@MartinEscardo/110504563233350460" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">110504563233350460</span></a></p><p>* 2023/06/15. Constructive notions of disjunction.<br><a href="https://mathstodon.xyz/@MartinEscardo/110549967500023998" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">110549967500023998</span></a></p><p>* 2023/07/09. Trichotomy of the reals constructively.<br><a href="https://mathstodon.xyz/@MartinEscardo/110685074921103237" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">mathstodon.xyz/@MartinEscardo/</span><span class="invisible">110685074921103237</span></a></p><p>1/</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