Code related to the paper "Erased Postulates, Identity Types and Quotients"

Résumé fourni par la source

This formalisation is related to the paper Erased Postulates, Identity Types and Quotients by Nils Anders Danielsson. It builds on a formalisation due to Andreas Abel, Nils Anders Danielsson, Oskar Eriksson, Naïm Camille Favier, Eve Geng, Gaëtan Gilbert, Ondřej Kubánek, Wojciech Nawrocki, Joakim Öhman and Andrea Vezzosi.