Talks

---

ASSUME

The Γ-Cube: Polarities and Modalities

— at the February 2024 meeting of ASSUME, 01 February 2024, Birmingham, UK

I discuss the interrelationships of eight standard models of dependent type theory, which are defined in a uniform way from eight categories of structures: sets, setoids, (univalent) groupoids, posets, preorders, and (univalent) categories. In particular, I highlight the 'negation' and 'core' modalities which exist on the latter four models, arising from their relationship to the former four. I also describe how this system of polarity sets the stage for semantics of directed type theory. Joint work with Thorsten Altenkirch.

HoTT 2023

Presheaf Models of Polarized Higher-Order Abstract Syntax

— at the Second International Conference on Homotopy Type Theory, 24 May 2023, Pittsburgh, USA

The Gamma Cube

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi non lectus volutpat, posuere mauris quis, tristique elit. Morbi faucibus ipsum urna, eget sollicitudin ipsum sagittis eu. Integer gravida mauris ac purus facilisis, vitae dapibus ex mattis. Nulla eget interdum ipsum. Donec tempor augue luctus nisi consectetur sodales. Aliquam semper rutrum nisi eget congue. Mauris ac tellus id turpis tempus euismod et eget velit.

Party Like It's 1999

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi non lectus volutpat, posuere mauris quis, tristique elit. Morbi faucibus ipsum urna, eget sollicitudin ipsum sagittis eu. Integer gravida mauris ac purus facilisis, vitae dapibus ex mattis. Nulla eget interdum ipsum. Donec tempor augue luctus nisi consectetur sodales. Aliquam semper rutrum nisi eget congue. Mauris ac tellus id turpis tempus euismod et eget velit.

Directed HOAS and Beyond

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi non lectus volutpat, posuere mauris quis, tristique elit. Morbi faucibus ipsum urna, eget sollicitudin ipsum sagittis eu. Integer gravida mauris ac purus facilisis, vitae dapibus ex mattis. Nulla eget interdum ipsum. Donec tempor augue luctus nisi consectetur sodales. Aliquam semper rutrum nisi eget congue. Mauris ac tellus id turpis tempus euismod et eget velit.

HoTT/UF 2023

The Category Interpretation of (Polarized and Directed) Type Theory

— at the Workshop on Homotopy Type Theory/Univalent Foundations, 23 April 2023, Vienna, Austria

Ontological Scandal!

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi non lectus volutpat, posuere mauris quis, tristique elit. Morbi faucibus ipsum urna, eget sollicitudin ipsum sagittis eu. Integer gravida mauris ac purus facilisis, vitae dapibus ex mattis. Nulla eget interdum ipsum. Donec tempor augue luctus nisi consectetur sodales. Aliquam semper rutrum nisi eget congue. Mauris ac tellus id turpis tempus euismod et eget velit.

Replace Groupoids with Categories

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi non lectus volutpat, posuere mauris quis, tristique elit. Morbi faucibus ipsum urna, eget sollicitudin ipsum sagittis eu. Integer gravida mauris ac purus facilisis, vitae dapibus ex mattis. Nulla eget interdum ipsum. Donec tempor augue luctus nisi consectetur sodales. Aliquam semper rutrum nisi eget congue. Mauris ac tellus id turpis tempus euismod et eget velit.

A Vision of Directed J

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi non lectus volutpat, posuere mauris quis, tristique elit. Morbi faucibus ipsum urna, eget sollicitudin ipsum sagittis eu. Integer gravida mauris ac purus facilisis, vitae dapibus ex mattis. Nulla eget interdum ipsum. Donec tempor augue luctus nisi consectetur sodales. Aliquam semper rutrum nisi eget congue. Mauris ac tellus id turpis tempus euismod et eget velit.

HoTT/UF 2022

Towards Directed Higher Observational Type Theory

— at the Workshop on Homotopy Type Theory/Univalent Foundations, 01 August 2022, Haifa, Israel

The Category Interpretation of Type Theory

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi non lectus volutpat, posuere mauris quis, tristique elit. Morbi faucibus ipsum urna, eget sollicitudin ipsum sagittis eu. Integer gravida mauris ac purus facilisis, vitae dapibus ex mattis. Nulla eget interdum ipsum. Donec tempor augue luctus nisi consectetur sodales. Aliquam semper rutrum nisi eget congue. Mauris ac tellus id turpis tempus euismod et eget velit.

A Dream of Directed HOTT

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Morbi non lectus volutpat, posuere mauris quis, tristique elit. Morbi faucibus ipsum urna, eget sollicitudin ipsum sagittis eu. Integer gravida mauris ac purus facilisis, vitae dapibus ex mattis. Nulla eget interdum ipsum. Donec tempor augue luctus nisi consectetur sodales. Aliquam semper rutrum nisi eget congue. Mauris ac tellus id turpis tempus euismod et eget velit.