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.

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).

Today was one of these days I left home at 7am and got back home from work at 8pm.

Luckily the commute is nice by bike in the canal, and short too, only <20 minutes (4 miles) each way.

Also at least I wasn't doing bureaucracy, but teaching preparation, followed by teaching, followed by a teaching meeting with staff and TA's, followed by more teaching preparation for tomorrow.

I love teaching, but I really need to find time to prepare my Thursday #HoTTEST talk, preferably not on Thursday, and preferably not in the evening.

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.

#Hottest #January on record mystifies #Climate #Scientists | #ClimateCrisis | The Guardian

Just as the planet’s biggest polluter has abandoned any pretence of tackling #GreenhouseGas #Emissions.

https://www.theguardian.com/environment/2025/feb/06/hottest-january-on-record-climate-scientists-global-temperatures-high

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.

#HoTT @carloangiuli @emilyriehl

This week the #HoTTEST seminar presents:

Paige North

Coinductive control of inductive data types

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 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

This week the #HoTTEST seminar presents:

Niels van der Weide

The internal languages of univalent categories

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 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

This week the #HoTTEST seminar presents:

Tashi Walde

An axiomatization of synthetic category theory

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 https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link, the abstract, and a list of all upcoming talks.

(Note that we are no longer on daylight time, so the local time may have changed for you.)

All are welcome!

#HoTT @carloangiuli @emilyriehl

This week the #HoTTEST seminar presents:

Max Zeuner

Univalent foundations of constructive algebraic geometry

The talk is at 11:30am EDT (15:30 UTC) on Thursday, October 24. 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@twtr.plus @carloangiuli@birdsite.wilde.cloud @emilyriehl

This week the #HoTTEST seminar presents:

Floris van Doorn

Formalizing a proof of Carleson's theorem

The talk is at 11:30am EDT (15:30 UTC) on Thursday, October 10. 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@twtr.plus @carloangiuli@birdsite.wilde.cloud @emilyriehl

Summer 2024 sweltered to Earth’s #hottest on record, making it even more likely that this year will end up as the warmest humanity has measured, European climate service Copernicus reported Friday.

And if this sounds familiar, that’s because the records the globe shattered were set just last year as human-caused climate change, with a temporary boost from an El Nino, keeps dialing up temperatures and extreme weather, scientists said.

The northern meteorological summer — June, July and August — averaged 16.8 degrees Celsius (62.24 degrees Fahrenheit), according to Copernicus.

That’s 0.03 degrees Celsius (0.05 degrees Fahrenheit) warmer than the old record in 2023.

Copernicus records go back to 1940, but American, British and Japanese records, which start in the mid-19th century, show the last decade has been the hottest since regular measurements were taken and likely in about 120,000 years, according to some scientists

https://apnews.com/article/heat-climate-change-record-broiling-hot-699026b8e57cc8404bc73d20e223500e

Finally got round to watching @dwarn's #HoTTEST talk [1]. I highly recommend it! We make good use of David's results in our work on acyclic maps [2], but what I particularly liked about this talk were the informal explanations which I found very helpful.

[1] https://www.youtube.com/watch?v=Fn_n72tuCSk
[2] https://tdejong.com/talks/TYPES-2023.pdf

@MartinEscardo I also really enjoyed it! For those who missed it, links to slides and the YouTube video are on the #HoTTEST web page.

Sorry, but I can't fulfill that request.

https://tinyurl.com/ylm4m9f4

September 2023 shatters #climate records - warmest September on record by far - "Global #temperatures soared to a new record in #September by a huge margin, stunning scientists and leading one to describe it as “absolutely gobsmackingly bananas”.

The #hottest September on record follows the hottest #August and hottest #July, with the latter being the hottest month ever recorded. The high temperatures have driven #heatwaves and #wildfires across the world.

September 2023 beat the previous record for that month by 0.5C, the largest jump in temperature ever seen. September was about 1.8C warmer than pre-industrial levels. Datasets from #European and #Japanese scientists confirm the leap."

https://www.theguardian.com/environment/2023/oct/05/gobsmackingly-bananas-scientists-stunned-by-planets-record-september-heat

Whee! #nuclear #catastrophe risks, #hottest month ever recorded on Earth, #AIpocalypse! What fun!!! (/sarcasm) https://www.axios.com/2023/08/01/climate-change-artificial-intelligence-nuclear-war-existential?utm_medium=mastodon&utm_campaign=mastodon&utm_source=mastodon

‘Era of #global #boiling has arrived,’ says #UN chief as July set to be #hottest month on #record

https://www.theguardian.com/science/2023/jul/27/scientists-july-world-hottest-month-record-climate-temperatures?CMP=Share_AndroidApp_Other
#ClimateChange #Climate