Mathstodon

0 posts0 participants0 posts today

Dan ChristensenThis week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="tag">#HoTTEST</a> seminar presents:Mitchell RileyTiny types and cubical type theoryThe talk is at 11:30am EDT (15:30 UTC) on Thursday, April 17. 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" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html</a> for the Zoom link and a list of all upcoming talks.All are welcome!<a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> <a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention">@carloangiuli</a> <a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention">@emilyriehl</a>Abstract:I will present an extension of Martin-Löf Type Theory that contains a tiny object; a type for which there is an "amazing" right adjoint to the formation of function types as well as the expected left adjoint. A primary aim of the theory is to be simple enough to be used both by hand and in a (hypothetical) proof assistant. I will sketch a normalisation algorithm and discuss a few potential applications, in particular, to implementations of Cubical Type Theory.

José A. AlonsoReadings shared March 7, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/07-readings_shared_03-07-25" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2025/03/07-readings_shared_03-07-25</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="tag">#Agda</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="tag">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#Coq</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="tag">#Programming</a> <a href="https://mathstodon.xyz/tags/Reasoning" class="mention hashtag" rel="tag">#Reasoning</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="tag">#Rocq</a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="tag">#TypeTheory</a>

José A. AlonsoOn the formalization of the simplicial model of HoTT. ~ Kunhong Du. <a href="https://florisvandoorn.com/theses/KunhongDu.pdf" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://florisvandoorn.com/theses/KunhongDu.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="tag">#Agda</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a>

Dan ChristensenThis week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="tag">#HoTTEST</a> seminar presents:Jonathan WeinbergerDirected univalence and the Yoneda embedding for synthetic ∞-categoriesThe 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" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html</a> for the Zoom link, the abstract, and a list of all upcoming talks.All are welcome!<a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> <a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention">@carloangiuli</a> <a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention">@emilyriehl</a>Abstract: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.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).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]The material is joint work with Daniel Gratzer und Ulrik Buchholtz (<a href="https://arxiv.org/abs/2407.09146" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://arxiv.org/abs/2407.09146</a>, <a href="https://arxiv.org/abs/2501.13229" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://arxiv.org/abs/2501.13229</a>).

Dan ChristensenThis week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="tag">#HoTTEST</a> seminar presents:Martín Hötzel EscardóInjective typesThe 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" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html</a> for the Zoom link, the abstract, and a list of all upcoming talks.All are welcome!<a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> <a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention">@carloangiuli</a> <a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention">@emilyriehl</a> <a href="https://mathstodon.xyz/@MartinEscardo" class="u-url mention">@MartinEscardo</a> Abstract: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.

Tom de JongThere's still a day left to submit a talk abstract to the Workshop on Homotopy Type Theory and Univalent Foundations!<a href="https://hott-uf.github.io/2025" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://hott-uf.github.io/2025</a><a href="https://mathstodon.xyz/tags/typetheory" class="mention hashtag" rel="tag">#typetheory</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a>

Dan ChristensenThis week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="tag">#HoTTEST</a> seminar presents:Mario CarneiroLean4Lean: Towards a Verified Typechecker for Lean, in LeanThe 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" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html</a> for the Zoom link and a list of all upcoming talks.All are welcome!Abstract: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.<a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> <a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention">@carloangiuli</a> <a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention">@emilyriehl</a>

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> (I am unaffiliated but I think both observational type theory and Ambrus himself are extremely cool, so I can strongly recommend applying!) <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 JongI'm pleased to advertise our latest paper titled "Ordinal Exponentiation in Homotopy Type Theory". <a href="https://arxiv.org/abs/2501.14542" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://arxiv.org/abs/2501.14542</a>This is joint work with <a href="https://mathstodon.xyz/@fnf" class="u-url mention">@fnf</a> <a href="https://mathstodon.xyz/@Nicolai_Kraus" class="u-url mention">@Nicolai_Kraus</a> and Chuangjie Xu.All our results are formalized in Agda, building on <a href="https://mathstodon.xyz/@MartinEscardo" class="u-url mention">@MartinEscardo</a>'s TypeTopology development, see the HTML version at <a href="https://ordinal-exponentiation-HoTT.github.io/" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://ordinal-exponentiation-HoTT.github.io/</a> In particular, the Paper file links every numbered environment in the paper to its implementation in Agda.<a href="https://mathstodon.xyz/tags/logic" class="mention hashtag" rel="tag">#logic</a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="tag">#TypeTheory</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="tag">#Agda</a>

Tom de JongThe slides for my speed talk on our JSL paper about epimorphisms and acyclic <a href="https://mathstodon.xyz/tags/types" class="mention hashtag" rel="tag">#types</a> in <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> at the Yorkshire and Midlands <a href="https://mathstodon.xyz/tags/Category" class="mention hashtag" rel="tag">#Category</a> Theory Seminar (<a href="https://conferences.leeds.ac.uk/yamcats/meeting-36/" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://conferences.leeds.ac.uk/yamcats/meeting-36/</a>) are up at <a href="https://tdejong.com/talks/YaMCATS-2025-01-24.pdf" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://tdejong.com/talks/YaMCATS-2025-01-24.pdf</a>

Freek WiedijkNote that I didn't mention <a href="https://bsky.app/search?q=%23HoTT" rel="nofollow noopener noreferrer" target="_blank">#HoTT</a> 😁

José A. AlonsoReadings shared January 12, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/12-readings_shared_01-12-25" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2025/01/12-readings_shared_01-12-25</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#Coq</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="tag">#Rocq</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="tag">#CommonLisp</a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="tag">#LogicProgramming</a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="tag">#Prolog</a> <a href="https://mathstodon.xyz/tags/LPTP" class="mention hashtag" rel="tag">#LPTP</a>

José A. AlonsoReconciling impredicative axiom and universe. ~ Stefan Monnier. <a href="https://hal.science/hal-04859508v1/file/jfla2025-final76.pdf" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://hal.science/hal-04859508v1/file/jfla2025-final76.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#Coq</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="tag">#Rocq</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a>

José A. AlonsoReadings shared January 6, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/06-readings_shared_01-06-25" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://jaalonso.github.io/vestigium/posts/2025/01/06-readings_shared_01-06-25</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#Lean4</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="tag">#Agda</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#Coq</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="tag">#Rocq</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#Math</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#AI</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#LLMs</a>

José A. AlonsoOn 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" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://bora.uib.no/bora-xmlui/handle/11250/3170892</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#ITP</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="tag">#Agda</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a>

HoldMyTypeThe First Real Application of <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="tag">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> -- is this kinda sorta algebraic graph theory?<a href="https://youtube.com/watch?v=Njx2ed8RGis" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://youtube.com/watch?v=Njx2ed8RGis</a>

LaneI thought that it might be interesting to diary some thoughts tangential to my research from time to time here. I picked up Homotopy Type Theory (<a href="https://social.praxis.nyc/tags/hott" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#hott</a>) and <a href="https://social.praxis.nyc/tags/categorytheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#categorytheory</a> more or less from scratch, albeit with the help of many wonderful guides and tutors from online seminars (<a href="https://social.praxis.nyc/tags/HoTTest" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#HoTTest</a> Summer School crew and Topos Institute, I'm looking at you). Therefore I've been more or less undisturbed in forming my intuition on these subjects, often drawn to philosophical considerations and themes. 🧵

Programming Languages DelftMaster thesis by Arnoud van der Leer: Universal Algebra, Univalent Foundations and the Untyped λ-Calculus"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."<a href="https://repository.tudelft.nl/record/uuid:e6582866-9c0d-4a13-8eda-42c25e0deba4" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://repository.tudelft.nl/record/uuid:e6582866-9c0d-4a13-8eda-42c25e0deba4</a><a href="https://akademienl.social/tags/univalentfoundations" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#univalentfoundations</a> <a href="https://akademienl.social/tags/hott" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#hott</a> <a href="https://akademienl.social/tags/typetheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#typetheory</a> <a href="https://akademienl.social/tags/thesis" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#thesis</a>

Dan ChristensenThis week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="tag">#HoTTEST</a> seminar presents:Paige NorthCoinductive control of inductive data typesThe 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" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html</a> for the Zoom link, the abstract, and a list of all upcoming talks.All are welcome!<a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> <a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention">@carloangiuli</a> <a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention">@emilyriehl</a>

Dan ChristensenThis week the <a href="https://mathstodon.xyz/tags/HoTTEST" class="mention hashtag" rel="tag">#HoTTEST</a> seminar presents:Niels van der WeideThe internal languages of univalent categoriesThe 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" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html</a> for the Zoom link, the abstract, and a list of all upcoming talks.All are welcome!<a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="tag">#HoTT</a> <a href="https://mathstodon.xyz/@carloangiuli" class="u-url mention">@carloangiuli</a> <a href="https://mathstodon.xyz/@emilyriehl" class="u-url mention">@emilyriehl</a>

Recent searches

Search options

Administered by:

Server stats:

#hott