José A. Alonso<p>Readings shared March 7, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/07-readings_shared_03-07-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/03/07-readings_shared_03-07-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/Reasoning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Reasoning</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TypeTheory</span></a></p>
Recent searches
No recent searches
Search options
Only available when logged in.
mstdn.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
A general-purpose Mastodon server with a 500 character limit. All languages are welcome.
Administered by:
Server stats:
15Kactive users
mstdn.social: About · Status · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.3.4
#hott
0 posts · 0 participants · 0 posts today
José A. Alonso<p>On the formalization of the simplicial model of HoTT. ~ Kunhong Du. <a href="https://florisvandoorn.com/theses/KunhongDu.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">florisvandoorn.com/theses/Kunh</span><span class="invisible">ongDu.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a></p>
Dan Christensen<p>This week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTTEST</span></a> seminar presents:</p><p>Jonathan Weinberger</p><p>Directed univalence and the Yoneda embedding for synthetic ∞-categories</p><p>The talk is at 11:30am EST (16:30 UTC) on Thursday, March 6. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See <a href="https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">uwo.ca/math/faculty/kapulkin/s</span><span class="invisible">eminars/hottest.html</span></a> for the Zoom link, the abstract, and a list of all upcoming talks.</p><p>All are welcome!</p><p><a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>carloangiuli</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>emilyriehl</span></a></span></p><p>Abstract:</p><p>In this talk, I'll present recent results in synthetic ∞-category theory in an extension of homotopy type theory. An ∞-category is analogous to a 1-category, but with composition defined only up to homotopy. To reason about them in HoTT, Riehl and Shulman proposed simplicial HoTT, an extension by a directed interval, generating the shapes that model arrows and their composition.</p><p>To account for fundamental constructions like the opposite category or the maximal subgroupoid, we add further type formers as modalities using Gratzer-Kavvos-Nuyts-Birkedal's framework of multimodal dependent type theory (MTT).</p><p>I'll present the construction of the universe 𝒮 of small ∞-groupoids in that setting which we can show to be an ∞-category satisfying directed univalence. As an application, we can define various ∞-categories of interest in higher algebra such as ∞-monoids and ∞-groups. Furthermore, I'll show the construction of the fully functorial Yoneda embedding w.r.t. 𝒮 as well as the Yoneda lemma (which is hard to establish in set-theoretic foundations). [truncated due to space considerations]</p><p>The material is joint work with Daniel Gratzer und Ulrik Buchholtz (<a href="https://arxiv.org/abs/2407.09146" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2407.09146</span><span class="invisible"></span></a>, <a href="https://arxiv.org/abs/2501.13229" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2501.13229</span><span class="invisible"></span></a>).</p>
Dan Christensen<p>This week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTTEST</span></a> seminar presents:</p><p>Martín Hötzel Escardó</p><p>Injective types</p><p>The talk is at 11:30am EST (16:30 UTC) on Thursday, February 20. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See <a href="https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">uwo.ca/math/faculty/kapulkin/s</span><span class="invisible">eminars/hottest.html</span></a> for the Zoom link, the abstract, and a list of all upcoming talks.</p><p>All are welcome!</p><p><a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>carloangiuli</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>emilyriehl</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@MartinEscardo" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>MartinEscardo</span></a></span> </p><p>Abstract:</p><p>In previous work, we established results about injective types in HoTT/UF, including characterizations, closure properties, and examples. In recent current work, in collaboration with Tom de Jong, we have developed more examples and counter-examples, as well as a better understanding of the landscape. In this talk I will present these old and new ideas.</p>
Tom de Jong<p>There's still a day left to submit a talk abstract to the Workshop on Homotopy Type Theory and Univalent Foundations!</p><p><a href="https://hott-uf.github.io/2025" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">hott-uf.github.io/2025</span><span class="invisible"></span></a></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/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a></p>
Dan Christensen<p>This week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTTEST</span></a> seminar presents:</p><p>Mario Carneiro</p><p>Lean4Lean: Towards a Verified Typechecker for Lean, in Lean</p><p>The talk is at 11:30am EST (16:30 UTC) on Thursday, February 6. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See <a href="https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">uwo.ca/math/faculty/kapulkin/s</span><span class="invisible">eminars/hottest.html</span></a> for the Zoom link and a list of all upcoming talks.</p><p>All are welcome!</p><p>Abstract:</p><p>This talk will present Lean4Lean, a project to construct a verified checker for the Lean theorem prover in the style of MetaCoq. It consists of a new “external verifier” for Lean, written in Lean. It is the first complete verifier for Lean 4 other than the reference implementation in C++ used by Lean itself, and the new verifier is competitive with the original, running between 20% and 50% slower and usable to verify all of Lean’s mathlib library, forming an additional step in Lean’s aim to self-host the full elaborator and compiler. The second part of the project concerns the type theory itself, and establishing its properties (in spite of several known negative results about the behavior of the type system), with the ultimate goal of being able to show that the verifier is correct to a specification of the type theory, and that the type theory is consistent relative to ZFC with countably many inaccessible cardinals. This work is still ongoing but we plan to use this project to help justify any future changes to the kernel and type theory and ensure unsoundness does not sneak in through either the abstract theory or implementation bugs.</p><p><a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>carloangiuli</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>emilyriehl</span></a></span></p>
Jesper Agdakx 🔸Two postdoc positions on higher observational type theory with Ambrus Kaposi in Budapest: <a href="http://lists.seas.upenn.edu/pipermail/types-announce/2025/011745.html" rel="nofollow noopener noreferrer" target="_blank">lists.seas.upenn.edu/pipermail/types-announce/2025/011745.html</a><br><br>(I am unaffiliated but I think both observational type theory and Ambrus himself are extremely cool, so I can strongly recommend applying!)<br><br><a class="hashtag" href="https://agda.club/tag/typetheory" rel="nofollow noopener noreferrer" target="_blank">#TypeTheory</a> <a class="hashtag" href="https://agda.club/tag/hott" rel="nofollow noopener noreferrer" target="_blank">#HOTT</a> <a class="hashtag" href="https://agda.club/tag/postdoc" rel="nofollow noopener noreferrer" target="_blank">#PostDoc</a>
Tom de Jong<p>I'm pleased to advertise our latest paper titled "Ordinal Exponentiation in Homotopy Type Theory".<br><a href="https://arxiv.org/abs/2501.14542" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2501.14542</span><span class="invisible"></span></a></p><p>This is joint work with <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@fnf" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>fnf</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@Nicolai_Kraus" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>Nicolai_Kraus</span></a></span> and Chuangjie Xu.</p><p>All our results are formalized in Agda, building on <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@MartinEscardo" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>MartinEscardo</span></a></span>'s TypeTopology development, see the HTML version at <a href="https://ordinal-exponentiation-HoTT.github.io/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">ordinal-exponentiation-HoTT.gi</span><span class="invisible">thub.io/</span></a><br>In particular, the Paper file links every numbered environment in the paper to its implementation in Agda.</p><p><a href="https://mathstodon.xyz/tags/logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>logic</span></a> <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/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a></p>
Tom de Jong<p>The slides for my speed talk on our JSL paper about epimorphisms and acyclic <a href="https://mathstodon.xyz/tags/types" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>types</span></a> in <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> at the Yorkshire and Midlands <a href="https://mathstodon.xyz/tags/Category" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Category</span></a> Theory Seminar (<a href="https://conferences.leeds.ac.uk/yamcats/meeting-36/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">conferences.leeds.ac.uk/yamcat</span><span class="invisible">s/meeting-36/</span></a>) are up at <a href="https://tdejong.com/talks/YaMCATS-2025-01-24.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">tdejong.com/talks/YaMCATS-2025</span><span class="invisible">-01-24.pdf</span></a></p>
José A. Alonso<p>Readings shared January 12, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/12-readings_shared_01-12-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/01/12-readings_shared_01-12-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CommonLisp</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Prolog</span></a> <a href="https://mathstodon.xyz/tags/LPTP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LPTP</span></a></p>
José A. Alonso<p>Reconciling impredicative axiom and universe. ~ Stefan Monnier. <a href="https://hal.science/hal-04859508v1/file/jfla2025-final76.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">hal.science/hal-04859508v1/fil</span><span class="invisible">e/jfla2025-final76.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a></p>
José A. Alonso<p>Readings shared January 6, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/06-readings_shared_01-06-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/01/06-readings_shared_01-06-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a></p>
José A. Alonso<p>On planarity of graphs in homotopy type theory. ~ Cubides, Jonathan Steven Prieto; Gylterud, Håkon Robbestad. <a href="https://bora.uib.no/bora-xmlui/handle/11250/3170892" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">bora.uib.no/bora-xmlui/handle/</span><span class="invisible">11250/3170892</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a></p>
HoldMyType<p>The First Real Application of <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <br>-- is this kinda sorta algebraic graph theory?</p><p><a href="https://youtube.com/watch?v=Njx2ed8RGis" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">youtube.com/watch?v=Njx2ed8RGi</span><span class="invisible">s</span></a></p>
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 noreferrer" 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 noreferrer" target="_blank">#<span>univalentfoundations</span></a> <a href="https://akademienl.social/tags/hott" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>hott</span></a> <a href="https://akademienl.social/tags/typetheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>typetheory</span></a> <a href="https://akademienl.social/tags/thesis" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>thesis</span></a></p>
Dan Christensen<p>This week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTTEST</span></a> seminar presents:</p><p>Paige North</p><p>Coinductive control of inductive data types</p><p>The talk is at 11:30am EST (16:30 UTC) on Thursday, December 5. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See <a href="https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">uwo.ca/math/faculty/kapulkin/s</span><span class="invisible">eminars/hottest.html</span></a> for the Zoom link, the abstract, and a list of all upcoming talks.</p><p>All are welcome!</p><p><a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>carloangiuli</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>emilyriehl</span></a></span></p>
Dan Christensen<p>This week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTTEST</span></a> seminar presents:</p><p>Niels van der Weide</p><p>The internal languages of univalent categories</p><p>The talk is at 11:30am EST (16:30 UTC) on Thursday, November 21. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See <a href="https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">uwo.ca/math/faculty/kapulkin/s</span><span class="invisible">eminars/hottest.html</span></a> for the Zoom link, the abstract, and a list of all upcoming talks.</p><p>All are welcome!</p><p><a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>carloangiuli</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>emilyriehl</span></a></span></p>
kat<p><span class="h-card" translate="no"><a href="https://toot.wales/@jwtownshend" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>jwtownshend</span></a></span> I do believe I have constructed a witness via Currying the inputs, with the following type signature</p><p>Cauliflower -> Potato -> Spice-> Edible Things-> TastyFood</p><p>which matches the type signature of Aloo Gobi 😋 </p><p><a href="https://is.burntout.org/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <a href="https://is.burntout.org/tags/math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>math</span></a> <a href="https://is.burntout.org/tags/cooking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>cooking</span></a></p>
Dan Christensen<p>This week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTTEST</span></a> seminar presents:</p><p>Tashi Walde</p><p>An axiomatization of synthetic category theory</p><p>The talk is at 11:30am EST (16:30 UTC) on Thursday, November 7. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See <a href="https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">uwo.ca/math/faculty/kapulkin/s</span><span class="invisible">eminars/hottest.html</span></a> for the Zoom link, the abstract, and a list of all upcoming talks.</p><p>(Note that we are no longer on daylight time, so the local time may have changed for you.)</p><p>All are welcome!</p><p><a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>carloangiuli</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>emilyriehl</span></a></span></p>
Tom de Jong<p>I'm pleased that my paper with <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@egbertrijke" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>egbertrijke</span></a></span> and <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@buchholtz" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>buchholtz</span></a></span> on epimorphisms and acyclic types in <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> got accepted to The Journal of Symbolic <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Logic</span></a>!</p><p>I'm quite proud of this paper as I feel that many of its arguments are rather slick and nicely illustrate the methods of synthetic homotopy theory.</p><p>arXiv link: <a href="https://arxiv.org/abs/2401.14106" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2401.14106</span><span class="invisible"></span></a></p>
ExploreLive 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