Recent searches

No recent searches

Search options

Not available on lingo.lol.
lingo.lol is one of the many independent Mastodon servers you can use to participate in the fediverse.
A place for linguists, philologists, and other lovers of languages.

Administered by:

Server stats:

61
active users

lingo.lol: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.8

#hott

1 post1 participant0 posts today
Dan Christensen

This week the #HoTTEST seminar presents:

Axel Ljungström

A formalisation of the Serre finiteness theorem

The talk is at 11:30am EDT (15:30 UTC) on Thursday, October 23. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See hottest-seminar.github.io/ for the Zoom link and a list of all upcoming talks.

All are welcome!

Abstract:

The central claim of the Serre finiteness theorem is that homotopy groups of spheres are finitely presented. Remarkably, this theorem can be proved constructively in HoTT. A particular consequence of this is that we get a completely synthetic proof of Brown's result that we, at least in theory, can compute (in the computer scientist's sense of the word) any homotopy group of any sphere! The HoTT proof of the Serre finiteness theorem, which is due to Barton and Campion, quickly inspired the launching of a rather extensive formalisation project, with the end-goal of verifying Barton and Campion's proof in Cubical Agda. About a month ago, this formalisation was finally completed.

In this talk, I'll give a rough outline of the Barton and Campion's proof. In my presentation, I will try to follow the timeline of the formalisation project and emphasise whenever the formalisation actually ended up leading to simplifications of the original pen-and-paper proof. I will also take the opportunity to mention some recent work on CW complexes which turned out to play an important role in both the formalisation and the pen-and-paper proof of the theorem.

This is joint work with Reid Barton, Owen Milner, Anders Mörtberg and Loïc Pujet.

#HoTT @carloangiuli @emilyriehl @ljungstrom

hottest-seminar.github.ioHoTTEST
José A. Alonso

Ordinal exponentiation in homotopy type theory. ~ Tom de Jong et als. arxiv.org/abs/2501.14542 #ITP #Agda #HoTT #Math

arXiv logo
arXiv.orgConstructive Ordinal ExponentiationCantor's ordinal numbers, a powerful extension of the natural numbers, are a cornerstone of set theory. They can be used to reason about the termination of processes, prove the consistency of logical systems, and justify some of the core principles of modern programming language theory such as recursion. In classical mathematics, ordinal arithmetic is well-studied; constructively, where ordinals are taken to be transitive, extensional, and wellfounded orders on sets, addition and multiplication are well-known. We present a negative result showing that general constructive ordinal exponentiation is impossible, but we suggest two definitions that come close. The first definition is abstract and solely motivated by the expected equations; this works as long as the base of the exponential is positive. The second definition is based on decreasing lists and can be seen as a constructive version of Sierpiński's definition via functions with finite support; this requires the base to have a trichotomous least element. Whenever it makes sense to ask the question, the two constructions are equivalent, allowing us to prove algebraic laws, cancellation properties, and preservation of decidability of the exponential. The core ideas do not depend on any specific constructive set theory or type theory, but a concrete computer-checked mechanization using the Agda proof assistant is given in homotopy type theory.
José A. Alonso

Ordinal exponentiation in homotopy type theory. ~ Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. arxiv.org/abs/2501.14542 #ITP #Agda #HoTT

arXiv logo
arXiv.orgConstructive Ordinal ExponentiationCantor's ordinal numbers, a powerful extension of the natural numbers, are a cornerstone of set theory. They can be used to reason about the termination of processes, prove the consistency of logical systems, and justify some of the core principles of modern programming language theory such as recursion. In classical mathematics, ordinal arithmetic is well-studied; constructively, where ordinals are taken to be transitive, extensional, and wellfounded orders on sets, addition and multiplication are well-known. We present a negative result showing that general constructive ordinal exponentiation is impossible, but we suggest two definitions that come close. The first definition is abstract and solely motivated by the expected equations; this works as long as the base of the exponential is positive. The second definition is based on decreasing lists and can be seen as a constructive version of Sierpiński's definition via functions with finite support; this requires the base to have a trichotomous least element. Whenever it makes sense to ask the question, the two constructions are equivalent, allowing us to prove algebraic laws, cancellation properties, and preservation of decidability of the exponential. The core ideas do not depend on any specific constructive set theory or type theory, but a concrete computer-checked mechanization using the Agda proof assistant is given in homotopy type theory.
Dan Christensen

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 uwo.ca/math/faculty/kapulkin/s 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 (arxiv.org/abs/2407.09146, 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.
Tom de Jong

I'm pleased to advertise our latest paper titled "Ordinal Exponentiation in Homotopy Type Theory".
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 ordinal-exponentiation-HoTT.gi
In particular, the Paper file links every numbered environment in the paper to its implementation in Agda.

arXiv logo
arXiv.orgConstructive Ordinal ExponentiationCantor's ordinal numbers, a powerful extension of the natural numbers, are a cornerstone of set theory. They can be used to reason about the termination of processes, prove the consistency of logical systems, and justify some of the core principles of modern programming language theory such as recursion. In classical mathematics, ordinal arithmetic is well-studied; constructively, where ordinals are taken to be transitive, extensional, and wellfounded orders on sets, addition and multiplication are well-known. We present a negative result showing that general constructive ordinal exponentiation is impossible, but we suggest two definitions that come close. The first definition is abstract and solely motivated by the expected equations; this works as long as the base of the exponential is positive. The second definition is based on decreasing lists and can be seen as a constructive version of Sierpiński's definition via functions with finite support; this requires the base to have a trichotomous least element. Whenever it makes sense to ask the question, the two constructions are equivalent, allowing us to prove algebraic laws, cancellation properties, and preservation of decidability of the exponential. The core ideas do not depend on any specific constructive set theory or type theory, but a concrete computer-checked mechanization using the Agda proof assistant is given in homotopy type theory.
#logic#TypeTheory#HoTT
Dan Christensen

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

All are welcome!

#HoTT @carloangiuli @emilyriehl

www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Tom de Jong

I'm pleased that my paper with @egbertrijke and @buchholtz on epimorphisms and acyclic types in #HoTT got accepted to The Journal of Symbolic #Logic!

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.

arXiv link: arxiv.org/abs/2401.14106

arXiv.orgEpimorphisms and Acyclic Types in Univalent FoundationsWe characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory as developed in univalent foundations. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with 0-connected, pointed 1-types. Many of our results are formalized as part of the agda-unimath library.
TrendingLive feeds
About