(Picture from Andrej Bauer's collection)
All times are BST (British Summer Time, UTC+1).
Peter Dybjer: Indexed Categories with Families
Categories with families (cwfs) constitute a notion of model of dependent type theory. Its main feature is that cwfs are models of a generalized algebraic theory closely related to Martin-Löf’s substitution calculus for dependent types and thus have a syntactic flavour. Cwfs where the set of types does not depend on the context are called simply typed (scwfs) and ones with only one type are called unityped (ucwfs). With these three notions one can develop a uniform metatheory of dependently typed, simply typed, and untyped lambda calculi, see Castellan, Clairambault, and Dybjer 2021. In this talk I will discuss various notions of indexed cwfs that turn out to capture several other well-known logical systems, including predicate logic, logic-enriched type theories, and type theory with universe-level judgments. The aim is to provide a further step in the quest for a uniform cwf-based metatheory of logical system.
Thierry Coquand (online): Paradoxes and Definitions
The first part of this talk will consist of some remarks on Reynolds/Hurkens’ paradox, following a talk given by Thorsten last August on paradoxes. The notion of definitional equality is essential to represent and analyse such a paradox in a convenient way and the second part will present some questions about this notion.
Wouter Swierstra: Correct by Construction Conversion to Combinators
I will present a translation in Agda, mapping well typed lambda terms to combinatory logic. By construction, this translation guarantees the types and semantics of each lambda term is preserved.
Jeremy Gibbons: When is a Function a Fold or an Unfold?
This is a story about a time when Thorsten clarified a problem Graham Hutton and I were working on, leading us to a clearer picture, a neater result, and a better paper. The problem is my talk title: when is a function a fold (or dually, an unfold)? A sufficient condition is for the function to be invertible. But that's clearly not a necessary condition - consider sum - so what is necessary? Come along and find out!
Fredrik Nordvall Forsberg: Counting on Thorsten: Representing Ordinals in Homotopy Type Theory
How can ordinals be represented in a constructive system such as homotopy type theory? Compromise will always be required, since for example it is not possible to simultaneously be able to decide equality of ordinals and compute limits of sequences. I will discuss different representations of ordinals and their trade offs, developed in joint work with Nicolai Kraus and Chuangjie Xu, and also a coinductive construction of ordinals suggested by Thorsten.
Anton Setzer (online): The Extended Predicative Mahlo Universe in Type Theory (jww Peter Dybjer)
Kahle and Setzer extended Feferman's system of explicit mathematics with an extended predicative Mahlo universe. Their aim was to formulate a notion that is predicative in the extended sense of Martin-Löf type theory and provide an alternative to Jäger and Strahm's original axiomatic Mahlo universe in explicit mathematics. We introduce an external version of their extended predicative Mahlo universe.
To substantiate that the extended predicative Mahlo universe is indeed predicative, we build a model of the external version n Martin-Löf type theory extended with certain inductive-recursive definitions.
Although these new definitions go beyond the class of inductive-recursive definitions defined in previous work by the authors, we argue that they are constructive and predicative in Martin-Löf's sense. The model construction has been implemented in the proof assistant Agda.
Conor McBride: A Little Irrelevance
Abstract TBA
Ondřej Rypáček: A little Algebra of Colours
Abstract TBA
Paul Levy: Derivational Families: a Form of Induction-Recursion
We look at two "Derivational Family" principles that can be seen as forms of induction-recursion. Given a "rubric", or collection of rules, they generate a family in which each item is indexed by its derivation. The so-called "Wide" principle is derivable just from W-types, whereas the so-called "Broad" principle relies on the universe being Mahlo.
Ambrus Kaposi (online): Type Theory in Type Theory using Quotient-Inductive-Inductive-Recursive Types
In 2006, Nils Anders Danielsson formalised type theory in Agda using inductive-inductive-recursive types (IIRTs) before those types were understood. In 2009, James Chapman formalised type theory in Agda using inductive-inductive types (IITs) before the term "induction-induction" was coined. In 2016, Thorsten and I formalised type theory in Agda using quotient inductive-inductive types (QIITs) before a formal definition of QIITs was given. Cubical Agda now supports quotient inductive-inductive-recursive types (QIIRTs). We don't yet understand QIIRTs, so it is time to formalise the syntax of type theory using them! This is work in progress.
Martín Hötzel Escardó: Totally Separated Types
We answer a question by Thorsten and his collaborators.
Bernhard Reus: Monadic Presentations of Lambda Terms using Generalized Inductive Types
Abstract TBA
Nicola Gambino: How Constructive is the Simplicial Model of Univalent Foundations?
I will review the current status of the attempts to obtain a constructive version of the simplicial model of Univalent Foundations, and indicate some directions for future work. This will be based on joint papers with S. Henry, C. Sattler and K. Szumilo.
Steve Awodey (online): Containing type theory
We have recently proposed an algebraic approach to the syntax of (dependent) type theory based on polynomial functors, aka containers. One question that arises - namely whether the monad laws must hold - is answered in a univalent setting.
Tarmo Uustalu: Skewness Everywhere
As we (re)discovered relative monads with Thorsten, we also discovered skew monoidal categories. Very soon thereafter, they were independently isolated as a concept by Szlachányi and then caught the attention of the Australians. Now we know quite a bit about them and I run into instances of this surprisingly robust concept everywhere.
We will hold the event in room C49, Dearing Building (Google Maps) on Jubilee Campus at the University of Nottingham (UK postcode NG8 1BB).
On the campus map, the Dearing Building has number 6 in square D2. The room is on the second floor ("C floor"), which is also the top floor.
Zoom streaming will start around 9:05 (BST). Here are the meeting details:
Meeting ID: 650 6459 2551
Passcode: T60
Join by SIP
65064592551@109.105.112.236
65064592551@109.105.112.235
Join by H.323
109.105.112.236
109.105.112.235
Meeting ID: 650 6459 2551
Passcode: 582313
The closest hotels seem to be booked out now (1 October). A good choice would be to stay in one of the many hotels in the city centre, which is well-connected to the campus by bus (lines 28 and 30, see local travel below).
Another option is to stay in the Castle Marina area, e.g. the Premier Inn at Castle Marina Park, Castle Bridge Road, Nottingham NG7 1GX.
Nottingham is centrally located in the UK and reachable by all forms of transport. The university's directions for getting to Jubilee Campus can be found here.
International travel: If you want to come by plane, closest to Nottingham is East Midlands Airport, but it is so small that you need to be lucky to find a flight arriving there. A very good destination airport is Birmingham, followed by Manchester and London Luton. All of these are within reasonable distance from Nottingham and well-connected by train, with none or very few changes.
Other London airports such as Stansted, Heathrow, and Gatwick are also options, but a bit more of a trek if you want to travel onwards by train; however, connections by bus can be very convenient (see national travel below).
If you want to avoid a flight, the Eurostar is fantastic.
National travel: National Rail is one of the sites that let you find train connections. If you want to try to save costs, there are a couple of websites that let you split the journey into smaller parts (search for "UK train split ticket"), using that the triangular inequality does not hold for UK train fares. However, be aware that your tickets will be less flexible.
National Express offers cheap and often very convenient bus journeys and is an interesting option when the train connection is not direct. A similar website is Megabus.
Local travel: Jubilee Campus (Google Maps) has the address Wollaton Road, NG8 1BB. The campus is quite a bit away from Nottingham Train Station. Taxis are waiting at Station Street. Another possibility is to walk to Victoria Centre and take bus 28 or 30 (or Two, another operator) to the stop Jubilee Campus. Contactless payment is possible on the bus. (Caveat: Contactless payment will not produce a physical ticket or receipt).
Travel by car: It is possible to park on Jubilee Campus or nearby. An all-day parking permit is £10.
For all enquiries, please contact Tarmo Uustalu, Conor McBride, Nicolai Kraus, and Artem Shinkarov.