TY  - RPRT
TI  - Builtin Types viewed as Inductive Families
AU  - Guillaume Allais
PY  - 2023
UR  - https://arxiv.org/abs/2301.02194
ID  - 2301.02194
ER  -