Home
Publications
Talks
Contact
Light
Dark
Automatic
Recent & Upcoming Talks
2024
Differential geometry in synthetic algebraic geometry
We present a few proofs in synthetic algebraic geometry, related to smoothness for affine schemes.
Apr 3, 2024
HoTT-UF
PDF
Slides
2022
Cubical models are cofreely parametric
We give a solid theoretical grounding to the observation that cubical structures arise naturally when working with parametricity. More precisely, we claim that cubical models are cofreely parametric.
Jun 20, 2022
TYPES
Slides
Video
2021
Parametricity and cubes
We report on our investigations linking parametricity and cubical structures. Our slogan is that cubical models of type theory are cofreely parametric.
Oct 21, 2021
HoTTEST
Slides
Video
Parametricity and semi-cubical types
We construct a model of type theory enjoying parametricity from an arbitrary one. A type in the new model is a semi-cubical type in the old one, illustrating the correspondence between parametricity and cubes.
Jun 29, 2021
LICS
Slides
2019
Toward a cubical type theory univalent by definition
We report on our progress in the construction of a variant of cubical type theory where univalence holds by definition.
Jun 16, 2019
HoTT
PDF
Slides
Monoids up to coherent homotopy in two-level type theory
We formalize monoids up to coherent homotopy in Agda, using two level type theory.
Apr 11, 2019
Deducteam seminar
PDF
Code
Slides
2018
Finitary higher inductive types in the groupoid model
We present a schema for finitary higher inductive types with constructors for paths and surfaces only. This schema is supported by the groupoid model.
Dec 11, 2018
Göteborg–Stockholm seminar
Slides
Cite
×