Hugo Moeneclaey

Post-doc

University of Gothenburg and Chalmers University of Technology

Biography

I am interested in type theory and its homotopical interpretations. At the moment I am mainly working on synthetic homotopy theory and synthetic algebraic geometry.

I started a post-doc at the University of Gothenburg in March 2023.

Download my CV.

I successfully defended my PhD on the 21st of October 2022.

Download my thesis.

Download the slides of the defense.

Contact: hugomo[at]chalmers.se

Publications

Hugo Moeneclaey (2022). Cubical models are cofreely parametric. PhD Thesis.

Hugo Moeneclaey (2021). Parametricity and semi-cubical types. LICS.

Hugo Moeneclaey, Peter Dybjer (2017). Finitary higher inductive types in the groupoid model. MFPS.

Selected Talks

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

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

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

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

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

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

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