Create accountLogin

Recent searches

No recent searches

Search options

Not available on dice.camp.
dice.camp is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon server for RPG folks to hang out and talk. Not owned by a billionaire.

Administered by:

Server stats:

1.7K
active users

dice.camp: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#hott

1 post1 participant0 posts today
Public
Dan Christensen

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 uwo.ca/math/faculty/kapulkin/s 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.
Public
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.
Public *
Dan Christensen

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 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 @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.
Public
Dan Christensen

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 uwo.ca/math/faculty/kapulkin/s 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

www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Public
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.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.
#logic#TypeTheory#HoTT
Public
Programming Languages Delft

Master 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."

repository.tudelft.nl/record/u

repository.tudelft.nlUniversal Algebra, Univalent Foundations and the Untyped λ-Calculus | TU Delft Repository
#univalentfoundations#hott#typetheory
Public
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.
Public
Dan Christensen

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 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.
Public
Dan Christensen

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 uwo.ca/math/faculty/kapulkin/s 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

www.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Public
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.
Public
Dan Christensen

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 uwo.ca/math/faculty/kapulkin/s 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

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

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 uwo.ca/math/faculty/kapulkin/s 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

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

The #HoTTEST seminar begins its fall season with the following talk:

Reid Barton

Directed aspects of condensed type theory

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

www.math.uwo.caHomotopy Type Theory Electronic Seminar TalksWestern University, in vibrant London, Ontario, delivers an academic and student experience second to none.
Public
Patrik Jansson

Come and work with us!

The Logic and types group of the Department of computer science and engineering, Chalmers and Gothenburg University, is recruiting to a 3-year postdoc position to work with dependent type theory extended with univalence and higher inductive types.

For more information about the position and how to apply for it, please follow this link
web103.reachmee.com/ext/I005/1

Deadline for application is 2024-09-17.

Please do not hesitate to contact us if you have any questions.

web103.reachmee.comPostdocThe department of Computer Science and Engineering is strongly international, with approximately 300 employees from
#Agda#HOTT
ExploreLive feeds
About