Tom de Jong<p>TYPES talk done! Time to enjoy the rest of the conference 😄 I talked about injective types in univalent mathematics which is joint work with <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>. You can find my slides here <a href="https://tdejong.com/talks/TYPES-2025.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">tdejong.com/talks/TYPES-2025.p</span><span class="invisible">df</span></a>.</p><p><a href="https://mathstodon.xyz/tags/TYPES2025" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TYPES2025</span></a> <a href="https://mathstodon.xyz/tags/typetheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>typetheory</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HoTT</span></a></p>
#hott
0 posts0 participants0 posts today
HoTTLean: Formalizing the meta-theory of HoTT in Lean. ~ Joseph Hua et als. https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper25.pdf #ITP #LeanProver #HoTT
The University of Gothenburg is looking to hire a postdoc for work on
compilation of cubical type theory:
web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=37550
Application deadline: June 12.
#TypeTheory #Cubical #HoTT #Agda #PostDoc #Gothenburg
compilation of cubical type theory:
web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=37550
Application deadline: June 12.
#TypeTheory #Cubical #HoTT #Agda #PostDoc #Gothenburg
web103.reachmee.comPostdoc in Type theory and programming languagesThe department of Computer Science and Engineering is strongly international, with approximately 300 employees from
Ordinal exponentiation in homotopy type theory. ~ Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. https://arxiv.org/abs/2501.14542 #ITP #Agda #HoTT
arXiv.orgOrdinal Exponentiation in Homotopy Type TheoryWhile ordinals have traditionally been studied mostly in classical frameworks, constructive ordinal theory has seen significant progress in recent years. However, a general constructive treatment of ordinal exponentiation has thus far been missing. We present two seemingly different definitions of constructive ordinal exponentiation in the setting of homotopy type theory. The first is abstract, uses suprema of ordinals, and is solely motivated by the expected equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version of a classical construction by Sierpiński based on functions with finite support. We show that our two approaches are equivalent (whenever it makes sense to ask the question), and use this equivalence to prove algebraic laws and decidability properties of the exponential. All our results are formalized in the proof assistant Agda.
This week the #HoTTEST seminar presents:
Mitchell Riley
Tiny types and cubical type theory
The 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 https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link and a list of all upcoming talks.
All are welcome!
#HoTT @carloangiuli @emilyriehl
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.
www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Readings shared March 7, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/07-readings_shared_03-07-25 #Agda #CategoryTheory #Coq #HoTT #ITP #LLMs #LeanProver #Math #Programming #Reasoning #Rocq #TypeTheory
Vestigium · Readings shared February 7, 2025The readings shared in Bluesky on 7 March 2025 are
A formalisation of addition chains. ~ Laurent Théry. #ITP #Coq #Rocq
QED in context (An observation study of proof assistant users). ~ Jessica Shi,
On the formalization of the simplicial model of HoTT. ~ Kunhong Du. https://florisvandoorn.com/theses/KunhongDu.pdf #ITP #Agda #HoTT
This week the #HoTTEST seminar presents:
Jonathan Weinberger
Directed univalence and the Yoneda embedding for synthetic ∞-categories
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 https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link, the abstract, and a list of all upcoming talks.
All are welcome!
#HoTT @carloangiuli @emilyriehl
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 (https://arxiv.org/abs/2407.09146, https://arxiv.org/abs/2501.13229).
www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
This week the #HoTTEST seminar presents:
Martín Hötzel Escardó
Injective types
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 https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link, the abstract, and a list of all upcoming talks.
All are welcome!
#HoTT @carloangiuli @emilyriehl @MartinEscardo
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.
www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Continued thread
There's still a day left to submit a talk abstract to the Workshop on Homotopy Type Theory and Univalent Foundations!
hott-uf.github.ioHoTT/UF 2025
This week the #HoTTEST seminar presents:
Mario Carneiro
Lean4Lean: Towards a Verified Typechecker for Lean, in Lean
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 https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html 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.
www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Two postdoc positions on higher observational type theory with Ambrus Kaposi in Budapest: lists.seas.upenn.edu/pipermail/types-announce/2025/011745.html
(I am unaffiliated but I think both observational type theory and Ambrus himself are extremely cool, so I can strongly recommend applying!)
#TypeTheory #HOTT #PostDoc
(I am unaffiliated but I think both observational type theory and Ambrus himself are extremely cool, so I can strongly recommend applying!)
#TypeTheory #HOTT #PostDoc
lists.seas.upenn.edu[TYPES/announce] Postdoc positions in type theory (start: May 2025; location: Budapest, Hungary)
I'm pleased to advertise our latest paper titled "Ordinal Exponentiation in Homotopy Type Theory".
https://arxiv.org/abs/2501.14542
This is joint work with @fnf @Nicolai_Kraus and Chuangjie Xu.
All our results are formalized in Agda, building on @MartinEscardo's TypeTopology development, see the HTML version at https://ordinal-exponentiation-HoTT.github.io/
In particular, the Paper file links every numbered environment in the paper to its implementation in Agda.
arXiv.orgOrdinal Exponentiation in Homotopy Type TheoryWhile ordinals have traditionally been studied mostly in classical frameworks, constructive ordinal theory has seen significant progress in recent years. However, a general constructive treatment of ordinal exponentiation has thus far been missing. We present two seemingly different definitions of constructive ordinal exponentiation in the setting of homotopy type theory. The first is abstract, uses suprema of ordinals, and is solely motivated by the expected equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version of a classical construction by Sierpiński based on functions with finite support. We show that our two approaches are equivalent (whenever it makes sense to ask the question), and use this equivalence to prove algebraic laws and decidability properties of the exponential. All our results are formalized in the proof assistant Agda.
The slides for my speed talk on our JSL paper about epimorphisms and acyclic #types in #HoTT at the Yorkshire and Midlands #Category Theory Seminar (https://conferences.leeds.ac.uk/yamcats/meeting-36/) are up at https://tdejong.com/talks/YaMCATS-2025-01-24.pdf
conferences.leeds.ac.ukMeeting 36 | Yorkshire and Midlands Category Theory Seminar
Readings shared January 12, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/12-readings_shared_01-12-25 #ITP #Coq #Rocq #Math #HoTT #CommonLisp #LogicProgramming #Prolog #LPTP
Vestigium · Readings shared January 12, 2025The readings shared in Bluesky on 12 January 2025 are
Readings shared January 11, 2025. #ITP #LeanProver #Coq #Rocq #Agda #FunctionalProgramming #Haskell #Python #Math #CategoryTheory #ComputerSci #
Reconciling impredicative axiom and universe. ~ Stefan Monnier. https://hal.science/hal-04859508v1/file/jfla2025-final76.pdf #ITP #Coq #Rocq #HoTT
Readings shared January 6, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/06-readings_shared_01-06-25 #ITP #IsabelleHOL #LeanProver #Lean4 #Agda #Coq #Rocq #HoTT #Math #AI #LLMs
Vestigium · Readings shared January 6, 2025The readings shared in Bluesky on 6 January 2025 are
Readings shared January 4, 2025. #ITP #IsabelleHOL #LeanProver #HOLLight #Mizar #Math #Logic #Haskell #Python
Computing huge Fibonacci numbers, by
On planarity of graphs in homotopy type theory. ~ Cubides, Jonathan Steven Prieto; Gylterud, Håkon Robbestad. https://bora.uib.no/bora-xmlui/handle/11250/3170892 #ITP #Agda #HoTT
bora.uib.noBergen Open Research Archive: On planarity of graphs in homotopy type theory