Loïc Pujet

I am a postdoc in the department of mathematics of the University of Stockholm, funded by the Sverker-Lerheden foundation. My research interests lie mainly in type theory, proof assistants, homotopy theory and constructive mathematics. Here is a picture of me.

You can contact me at .l?o+i8ch@^pdurrj*egt2.zf6r! .

News
28/02/2025 – I uploaded a preprint about strictifying categories with families, written in collaboration with Ambrus Kaposi.
21/02/2025 – I uploaded the slides of a presentation I gave at SCALP 2024 and the SU/Gothenburg joint meeting, on strictification of categories with families (joint work with Ambrus Kaposi).
24/01/2025 – I uploaded a preprint about CW complexes and cellular methods in HoTT, written in collaboration with Axel Ljungström
25/07/2024 – I uploaded a preprint about constructing setoid models that validate weak forms of choice. Update: I took down the preprint on the 03/09/2024 for revisions.
23/06/2024 – I uploaded the slides for my talk on the cellular approximation theorem at TYPES 2024.
16/03/2024 – I uploaded the slides for my talk on choice principles in OTT, that I originally prepared for the Stockholm-Gothenburg joint seminar, and subsequently presented at several other seminars.
15/01/2024 – Our paper "Observational Equality meets CIC" with Nicolas Tabareau was accepted to ESOP 2024.

Research

Publications and Preprints

Type Theory in Type Teory Using a Strictified Syntax Preprint

Ambrus Kaposi, Loïc Pujet

Preprint

Cellular Methods in Homotopy Type Theory Preprint

Axel Ljungström, Loïc Pujet

Preprint

Martin-Löf à la Coq HAL Formalisation

Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet

CPP 2024 (distinguished paper)

Observational Equality: Now For Good HAL slides Formalisation

Loïc Pujet, Nicolas Tabareau

POPL 2022 (distinguished paper)

Cubical Synthetic Homotopy Theory HAL slides

Anders Mörtberg, Loïc Pujet

CPP 2020

PhD thesis

Computing with Extensionality Principles in Type Theory Github slides

PhD thesis, Nantes University, 2022

The version on Github is the finished product, I am waiting for the university to put it on a more official-looking platform...

Talks

Strictifying Categories with Families slides

On joint work with Ambrus Kaposi

SCALP 2024

A Constructive Cellular Approximation Theorem slides abstract

On joint work with Axel Ljungström

TYPES 2024

Choice Principles in Observational Type Theory slides

Stockholm-Gothenburg joint seminar (2023)

Engineering Logical Relations for MLTT in Coq abstract

Talk by Kenji Maillard on j.w.w Arthur Adjedj, Meven Lennon-Bertrand and Kenji Maillard

TYPES 2023

Mechanising Reducibility Proofs in Coq slides

Invited talk

Europroofnet Working Group 6, 24 April 2023

Observational Type Theory meets CIC slides video

Joint work with Nicolas Tabareau

HoTTEST Seminar, 23 February 2023

Extensionality in Intensional Type Theory slides

Joint work with Nicolas Tabareau

Rencontres Chocola, 10 March 2022

Computing with Univalence in Coq using Intensional Presheaves abstract slides

Joint work with Maxime Lucas, Pierre-Marie Pédrot, and Nicolas Tabareau

ICMS 2020

Synthetic homotopy theory in cubical type theory and the Hopf fibration

CMU HoTT seminar, 28 February 2019

Beyond the probability of coprimality slides

UTokyo, JFLI Internship Day, 20 July 2017

Notes and drafts

A semantic account of the presheaf translation PDF

Last update: 02/12/2020