Artifact Description - Definitional Functoriality for Dependent (Sub)Types

Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard

PDF DOI 10.1007/978-3-031-57262-3_14 dblp BibTeX

Abstract

Abstract This document describes the Coq formalisation accompanying the paper Definitional Functoriality for Dependent (Sub)Types, more specifically the content of section 4.

Artifact Description - Definitional Functoriality for Dependent (Sub)Types

Abstract

Related papers