Meeting 27

Thursday May 12, 2022

Hosted by the University of Leeds
Supported by the London Mathematical Society

Schedule:

13:00-13:45: Andrew Slattery (University of Leeds)
13:45-14:30: Florrie Verity (Australian National University)
14:30-15:00: Coffee break
15:00-15:45: Alex Rice (University of Cambridge)
15:45-16:30: Tom de Jong (University of Birmingham)

Location:

All talks are in the Roger Stevens Building, Lecture Theatre 12 (Room 10M.12). It is located on Level 10, across the bridge from the School of Mathematics.

Further information on travel to Leeds and the campus itself is available here:

Titles and Abstracts:

Speaker: Andrew Slattery
Title: Property-like Structures and Relative Pseudomonads
Abstract: Idempotent monads—monads for which T : C -> C is idempotent as a functor in the relevant category-theoretic sense, which is to say that mu : TT -> T is an isomorphism—characterise monads whose algebras describe objects with only properties and not structure. Equivalently, the forgetful functor T-Alg -> C is fully faithful; every object of C has at most one algebra structure.
Kock and Zöberlein independently developed the analogous notion in 2 dimensions (called KZ or lax-idempotent pseudomonads), which describe so-called “property-like structures” which are not quite unique but *are* unique up to unique isomorphism (as discussed by Kelly and Lack). For example, the pesudomonad whose algebras are categories with finite products (“having finite products” being an example of a property-like structure) is lax-idempotent. One characterisation of lax-idempotency is that any algebra structure a : TA -> A is left adjoint to the unit i : A -> TA.
In my talk I extend this characterisation to the relative setting, articulating analogues of two characterisations of lax-idempotency for relative pseudomonads and proving that they are equivalent.

Slides: here

Speaker: Florrie Verity
Title: Hyperdoctrine semantics for higher-order modal logic
Abstract: Lawvere hyperdoctrines give categorical semantics for intuitionistic predicate logic [1]; they are flexible enough to be applied to other logics and can be extended to higher-order systems as higher-order hyperdoctrines (aka triposes). In this talk, I’ll present a straightforward extension in both directions: sound and complete hyperdoctrine semantics for higher-order non-normal modal logics. By focusing on non-normal modal logics, this work is intended to complement the other categorical semantics that have been developed for modal predicate logic: namely, Ghilardi’s first-order hyperdoctrine semantics for quantified normal modal logics [2]; and Awodey, Kishida and Kotzsch’s topos semantics for higher-order intuitionistic S4 modal logic [3]. This is joint work with Yoshihiro Maruyama.

[1] F. William Lawvere (1969): Adjointness in Foundations. Dialectica 23, pp. 281–296.
[2] Torben Brauner & Silvio Ghilardi (2007): First-order modal logic. Studies in Logic and Practical Reasoning 3, pp. 549–620.
[3] Steve Awodey, Kohei Kishida & Hans-Christoph Kotzsch (2014): Topos Semantics for Higher-Order Modal Logic. Logique et Analyse 57(228), pp. 591–636.

Slides: here

Speaker: Alex Rice
Title: Type theoretic approaches to semistrict higher categories
Abstract: Describing and constructing different operations in non-strict infinity category is notoriously difficult. Recently, there have been various type theoretic approaches to describing these operations, which can come equipped with a decidable type checker and a syntax that allows terms to be written in the style of a programming language. In this talk I will describe the type theory CaTT, for which the models are fully weak globular infinity categories.

It is known that not all weak infinity categories are equivalent to a strict infinity category, but it is believed that there are semistrict definitions of infinity categories where some operations are strictified, but still have the full expressivity of the fully weak setting. Searching for such semistrict definitions is an active research field. CaTT is an unusual type theory, in that it has no definitional equality. I will give an overview on our approaches to giving new semistrict definitions of infinity categories by adding definitional equality into CaTT.

Slides: here

Speaker: Tom de Jong
Title: Domain theory in constructive and predicative HoTT/UF
Abstract: Homotopy Type Theory, also known as Univalent Foundations (HoTT/UF), is a modern foundation for mathematics that is constructive and predicative by default. By constructive and predicative we respectively mean that excluded middle (and choice) and propositional resizing axioms are not assumed. We explain how to develop domain theory within this context, focusing on the Scott model of the programming language PCF and the lifting monad in particular.