TY  - RPRT
TI  - Definitional Functoriality for Dependent (Sub)Types -- Extended version
AU  - Théo Laurent
AU  - Meven Lennon-Bertrand
AU  - Kenji Maillard
PY  - 2024
UR  - https://arxiv.org/abs/2310.14929
ID  - 2310.14929
ER  -