2:1-2:27. ISBN: 978-3-95977-158-0. DOI: 10.4230/LIPIcs.TYPES.2019.2. URL: https://drops.dagstuhl.de/opus/volltexte/2020/13066.

[18] Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. "The Taming of the Rew: A Type Theory with Computational Assumptions". In: *Proceedings of the ACM on Programming Languages*. POPL 2021 (2021). URL: https://hal.archives-ouvertes.fr/hal-02901011.

[19] Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. "Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi". In: *FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction*. 167. Paris, France, June 2020, 34:1-34:21. DOI: 10.4230/LIPIcs.FSCD.2020.34. URL: https://inria.hal.science/hal-02478907.

[20] Cvetan Dunchev et al. "ELPI: fast, Embeddable, λProlog Interpreter". In: *Proceedings of LPAR*. Suva, Fiji, Nov. 2015. URL: https://inria.hal.science/hal-01176856.

[21] Jana Dunfield and Neel Krishnaswami. "Bidirectional Typing". In: *ACM Computing Surveys*. 54.5 (May 2021). ISSN: 0360-0300. DOI: 10.1145/3450952.

[22] Lucas Escot and Jesper Cockx. "Practical Generic Programming over a Universe of Native Datatypes". In: *Proc. ACM Program. Lang.* 6.ICFP (2022). DOI: 10.1145/3547644. URL: https://doi.org/10.1145/3547644.

[23] Lucas Escot et al. "Read the mode and stay positive". In: *29th International Conference on Types for Proofs and Programs*. 2023.

[24] Gaëtan Gilbert et al. "Definitional Proof-Irrelevance without K". In: *Proceedings of the ACM on Programming Languages*. POPL'19 3.POLP (Jan. 2019), pp. 1-28. DOI: 10.1145/3290316.1145/3290316. URL: https://hal.inria.fr/hal-01859964.

[25] Gaëtan Gilbert et al. *The Rewster: The Coq Proof Assistant with Rewrite Rules*. Presentation at TYPES'23. June 2023. URL: https://media.upv.es/#/portal/video/bf2591f0-34a6-11ee-8485-f133f82f8945.

[26] Martin Hofmann. *Extensional constructs in intensional type theory*. CPHC / BCS distinguished dissertations. Springer, 1997. ISBN: 978-3-540-76121-1.

[27] Cătălin Hrițcu. *Polarities: subtyping for datatypes*. https://github.com/FStarLang/FStar/issues/65. Accessed: 2023-07-04. 2014.

[28] Jasper Hugunin. "Why Not W?" In: *26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy*. Ed. by Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch. Vol. 188. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, 8:1-8:9. ISBN: 978-3-95977-182-5. DOI: 10.4230/LIPIcs.TYPES.2020.8. URL: https://doi.org/10.4230/LIPIcs.TYPES.2020.8.

[29] Bart P. F. Jacobs. *Categorical Logic and Type Theory*. Vol. 141. Studies in logic and the foundations of mathematics. North-Holland, 2001. ISBN: 978-0-444-50853-9. URL: http://www.elsevierdirect.com/product.jsp?isbn=9780444508539.

[30] Jean-Pierre Jouannaud and Pierre-Yves Strub. "Coq without Type Casts: A Complete Proof of Coq Modulo Theory". In: *LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Bo-tswana, May 7-12, 2017*. Ed. by Thomas Eiter and David Sands. Vol. 46. EPiC Series in Computing. EasyChair, 2017, pp. 474-489. DOI: 10.29007/bjpg. URL: https://doi.org/10.29007/bjpg.

[31] András Kovács. "Generalized Universe Hierarchies and First-Class Universe Levels". In: *30th EACSL Annual Conference on Computer Science Logic (CSL 2022)*. Ed. by Florin Manea and Alex Simpson. Vol. 216. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, 28:1-28:17. ISBN: 978-3-95977-218-1. DOI: 10.4230/LIPIcs.CSL.2022.28. URL: https://drops.dagstuhl.de/opus/volltexte/2022/15748.
2:1-2:27. ISBN: 978-3-95977-158-0. DOI: 10.4230/LIPIcs.TYPES.2019.2. URL: https://drops.dagstuhl.de/opus/volltexte/2020/13066.

[18] Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. "The Taming of the Rew: A Type Theory with Computational Assumptions". In: *Proceedings of the ACM on Programming Languages*. POPL 2021 (2021). URL: https://hal.archives-ouvertes.fr/hal-02901011.

[19] Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. "Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi". In: *FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction*. 167. Paris, France, June 2020, 34:1-34:21. DOI: 10.4230/LIPIcs.FSCD.2020.34. URL: https://inria.hal.science/hal-02478907.

[20] Cvetan Dunchev et al. "ELPI: fast, Embeddable, λProlog Interpreter". In: *Proceedings of LPAR*. Suva, Fiji, Nov. 2015. URL: https://inria.hal.science/hal-01176856.

[21] Jana Dunfield and Neel Krishnaswami. "Bidirectional Typing". In: *ACM Computing Surveys*. 54.5 (May 2021). ISSN: 0360-0300. DOI: 10.1145/3450952.

[22] Lucas Escot and Jesper Cockx. "Practical Generic Programming over a Universe of Native Datatypes". In: *Proc. ACM Program. Lang.* 6.ICFP (2022). DOI: 10.1145/3547644. URL: https://doi.org/10.1145/3547644.

[23] Lucas Escot et al. "Read the mode and stay positive". In: *29th International Conference on Types for Proofs and Programs*. 2023.

[24] Gaëtan Gilbert et al. "Definitional Proof-Irrelevance without K". In: *Proceedings of the ACM on Programming Languages*. POPL'19 3.POLP (Jan. 2019), pp. 1-28. DOI: 10.1145/3290316.1145/3290316. URL: https://hal.inria.fr/hal-01859964.

[25] Gaëtan Gilbert et al. *The Rewster: The Coq Proof Assistant with Rewrite Rules*. Presentation at TYPES'23. June 2023. URL: https://media.upv.es/#/portal/video/bf2591f0-34a6-11ee-8485-f133f82f8945.

[26] Martin Hofmann. *Extensional constructs in intensional type theory*. CPHC / BCS distinguished dissertations. Springer, 1997. ISBN: 978-3-540-76121-1.

[27] Cătălin Hrițcu. *Polarities: subtyping for datatypes*. https://github.com/FStarLang/FStar/issues/65. Accessed: 2023-07-04. 2014.

[28] Jasper Hugunin. "Why Not W?" In: *26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy*. Ed. by Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch. Vol. 188. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, 8:1-8:9. ISBN: 978-3-95977-182-5. DOI: 10.4230/LIPIcs.TYPES.2020.8. URL: https://doi.org/10.4230/LIPIcs.TYPES.2020.8.

[29] Bart P. F. Jacobs. *Categorical Logic and Type Theory*. Vol. 141. Studies in logic and the foundations of mathematics. North-Holland, 2001. ISBN: 978-0-444-50853-9. URL: http://www.elsevierdirect.com/product.jsp?isbn=9780444508539.

[30] Jean-Pierre Jouannaud and Pierre-Yves Strub. "Coq without Type Casts: A Complete Proof of Coq Modulo Theory". In: *LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Bo-tswana, May 7-12, 2017*. Ed. by Thomas Eiter and David Sands. Vol. 46. EPiC Series in Computing. EasyChair, 2017, pp. 474-489. DOI: 10.29007/bjpg. URL: https://doi.org/10.29007/bjpg.

[31] András Kovács. "Generalized Universe Hierarchies and First-Class Universe Levels". In: *30th EACSL Annual Conference on Computer Science Logic (CSL 2022)*. Ed. by Florin Manea and Alex Simpson. Vol. 216. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, 28:1-28:17. ISBN: 978-3-95977-218-1. DOI: 10.4230/LIPIcs.CSL.2022.28. URL: https://drops.dagstuhl.de/opus/volltexte/2022/15748.
[32] Meven Lennon-Bertrand. "Bidirectional Typing for the Calculus of Inductive Constructions". PhD thesis. Nantes Université, 2022.

[33] Meven Lennon-Bertrand, Théo Laurent, and Kenji Maillard. *Artifact for Definitional Functionality for Dependent (Sub)Types*. 2024. url: https://zenodo.org/records/10461809.

[34] Meven Lennon-Bertrand, Théo Laurent, and Kenji Maillard. "Definitional Functionality for Dependent (Sub)Types". In: *ESOP 2024 - 33th European Symposium on Programming*. 2024.

[35] Meven Lennon-Bertrand et al. "Gradualizing the Calculus of Inductive Constructions". In: *ACM Transactions on Programming Languages and Systems* 44.2 (Apr. 2022). ISSN: 0164-0925. DOI: 10.1145/3495528.

[36] Miran Lipovača. *Learn You a Haskell for Great Good!* 2010. url: http://learnyouahaskell.com/.

[37] Georgiana Elena Lungu and Zhaohui Luo. "On Subtyping in Type Theories with Canonical Objects". In: *22nd International Conference on Types for Proofs and Programs (TYPES 2016)*. Ed. by Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić. Vol. 97. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. 13:1-13:31. ISBN: 978-3-95977-065-1. DOI: 10.4230/LIPIcs.TYPES.2016.13. URL: http://drops.dagstuhl.de/opus/volltexte/2018/9849.

[38] Zhaohui Luo and Robin Adams. "Structural subtyping for inductive types with functorial equality rules". In: *Mathematical Structures in Computer Science* 18.5 (2008), pp. 931-972. ISSN: 0960-1295. DOI: 10.1017/S0960129508006956.

[39] Zhaohui Luo and Yong Luo. "Transitivity in coercive subtyping". In: *Inf. Comput.* 197.1-2 (2005), pp. 122-144. DOI: 10.1016/j.ic.2004.10.008. URL: https://doi.org/10.1016/j.ic.2004.10.008.

[40] Saunders MacLane. *Categories for the Working Mathematician*. Graduate Texts in Mathematics, Vol. 5. New York: Springer-Verlag, 1971.

[41] Per Martin-Löf and Giovanni Sabin. *Intuitionistic Type Theory*. Studies in Proof Theory 1. Napoli: Bibliopolis, 1984.

[42] Conor McBride. "Grins from my Ripley Cupboard". 2009. URL: http://strictlypositive.org/Ripley.pdf.

[43] Conor McBride. "Types Who Say Ni". 2022. URL: https://github.com/pigworker/TypesWhoSayNi.

[44] Conor McBride and Frederik Nordvall Forsberg. *Functorial Adapters*. 27th International Conference on Types for Proofs and Programs. June 2021.

[45] Leonardo de Moura and Sebastian Ullrich. "The Lean 4 Theorem Prover and Programming Language". In: *Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings*. Ed. by André Platzer and Geoff Sutcliffe. Vol. 12699. Lecture Notes in Computer Science. Springer, 2021, pp. 625-635. ISBN: 978-3-030-79875-8. DOI: 10.1007/978-3-030-79876-5_37. URL: https://doi.org/10.1007/978-3-030-79876-5%5C_37.

[46] Benjamin C. Pierce and David N. Turner. "Local Type Inference". In: *ACM Transactions on Programming Languages and Systems* 22.1 (Jan. 2000), pp. 1-44. ISSN: 0164-0925. DOI: 10.1145/345099.345100.

[47] Loïc Pujet and Nicolas Tabareau. "Impredicative Observational Equality". In: *Proc. ACM Program. Lang.* 7.POL (Jan. 2023). DOI: 10.1145/3571739.

[48] Loïc Pujet and Nicolas Tabareau. "Observational Equality: Now for Good". In: *Proc. ACM Program. Lang.* 6.POL (2022). DOI: 10.1145/3498693. URL: https://doi.org/10.1145/3498693.

[49] Jeremy G. Siek et al. "Refined Criteria for Gradual Typing". In: *1st Summit on Advances in Programming Languages (SNAPL 2015)*. Ed. by Thomas Ball et al. Vol. 32. Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015, pp. 274-293. DOI: 10.4230/LIPIcs.SNAPL.2015.274.
[32] Meven Lennon-Bertrand. "Bidirectional Typing for the Calculus of Inductive Constructions". PhD thesis. Nantes Université, 2022.

[33] Meven Lennon-Bertrand, Théo Laurent, and Kenji Maillard. *Artifact for Definitional Functionality for Dependent (Sub)Types*. 2024. url: https://zenodo.org/records/10461809.

[34] Meven Lennon-Bertrand, Théo Laurent, and Kenji Maillard. "Definitional Functionality for Dependent (Sub)Types". In: *ESOP 2024 - 33th European Symposium on Programming*. 2024.

[35] Meven Lennon-Bertrand et al. "Gradualizing the Calculus of Inductive Constructions". In: *ACM Transactions on Programming Languages and Systems* 44.2 (Apr. 2022). ISSN: 0164-0925. DOI: 10.1145/3495528.

[36] Miran Lipovača. *Learn You a Haskell for Great Good!* 2010. url: http://learnyouahaskell.com/.

[37] Georgiana Elena Lungu and Zhaohui Luo. "On Subtyping in Type Theories with Canonical Objects". In: *22nd International Conference on Types for Proofs and Programs (TYPES 2016)*. Ed. by Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić. Vol. 97. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. 13:1-13:31. ISBN: 978-3-95977-065-1. DOI: 10.4230/LIPIcs.TYPES.2016.13. URL: http://drops.dagstuhl.de/opus/volltexte/2018/9849.

[38] Zhaohui Luo and Robin Adams. "Structural subtyping for inductive types with functorial equality rules". In: *Mathematical Structures in Computer Science* 18.5 (2008), pp. 931-972. ISSN: 0960-1295. DOI: 10.1017/S0960129508006956.

[39] Zhaohui Luo and Yong Luo. "Transitivity in coercive subtyping". In: *Inf. Comput.* 197.1-2 (2005), pp. 122-144. DOI: 10.1016/j.ic.2004.10.008. URL: https://doi.org/10.1016/j.ic.2004.10.008.

[40] Saunders MacLane. *Categories for the Working Mathematician*. Graduate Texts in Mathematics, Vol. 5. New York: Springer-Verlag, 1971.

[41] Per Martin-Löf and Giovanni Sambin. *Intuitionistic Type Theory*. Studies in Proof Theory 1. Napoli: Bibliopolis, 1984.

[42] Conor McBride. "Grins from my Ripley Cupboard". 2009. URL: http://strictlypositive.org/Ripley.pdf.

[43] Conor McBride. "Types Who Say Ni". 2022. URL: https://github.com/pigworker/TypesWhoSayNi.

[44] Conor McBride and Frederik Nordvall Forsberg. *Functorial Adapters*. 27th International Conference on Types for Proofs and Programs. June 2021.

[45] Leonardo de Moura and Sebastian Ullrich. "The Lean 4 Theorem Prover and Programming Language". In: *Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings*. Ed. by André Platzer and Geoff Sutcliffe. Vol. 12699. Lecture Notes in Computer Science. Springer, 2021, pp. 625-635. ISBN: 978-3-030-79875-8. DOI: 10.1007/978-3-030-79876-5_37. URL: https://doi.org/10.1007/978-3-030-79876-5%5C_37.

[46] Benjamin C. Pierce and David N. Turner. "Local Type Inference". In: *ACM Transactions on Programming Languages and Systems* 22.1 (Jan. 2000), pp. 1-44. ISSN: 0164-0925. DOI: 10.1145/345099.345100.

[47] Loïc Pujet and Nicolas Tabareau. "Impredicative Observational Equality". In: *Proc. ACM Program. Lang.* 7.POL (Jan. 2023). DOI: 10.1145/3571739.

[48] Loïc Pujet and Nicolas Tabareau. "Observational Equality: Now for Good". In: *Proc. ACM Program. Lang.* 6.POL (2022). DOI: 10.1145/3498693. URL: https://doi.org/10.1145/3498693.

[49] Jeremy G. Siek et al. "Refined Criteria for Gradual Typing". In: *1st Summit on Advances in Programming Languages (SNAPL 2015)*. Ed. by Thomas Ball et al. Vol. 32. Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015, pp. 274-293. DOI: 10.4230/LIPIcs.SNAPL.2015.274.
[50] Matthieu Sozeau. "Subset Coercions in Coq". In: *Types for Proofs and Programs*. Ed. by Thorsten Altenkirch and Conor McBride. Berlin, Heidelberg: Springer Berlin Heidelberg, 2007, pp. 237–252. ISBN: 978-3-540-74464-1.

[51] Matthieu Sozeau et al. "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq". Preprint. Apr. 2023. URL: https://inria.hal.science/hal-04077552.

[52] Jonathan Sterling. "Algebraic Type Theory and Universe Hierarchies". In: *CoRR abs/1902.08848* (2019). arXiv: 1902.08848.

[53] Pierre-Yves Strub. "Coq Modulo Theory". In: *Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings*. Ed. by Anuj Dawar and Helmut Veith. Vol. 6247. Lecture Notes in Computer Science. Springer, 2010, pp. 529–543. ISBN: 978-3-642-15204-7. DOI: 10.1007/978-3-642-15205-4\_40. URL: https://doi.org/10.1007/978-3-642-15205-4%5C_40.

[54] Nikhil Swamy et al. "Dependent types and multi-monadic effects in F". In: *Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016*. Ed. by Rastislav Bodík and Rupak Majumdar. ACM, 2016, pp. 256–270. ISBN: 978-1-4503-3549-2. DOI: 10.1145/2837614.2837655. URL: https://doi.org/10.1145/2837614.2837655.

[55] Enrico Tassi. "Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect)". working paper or preprint. Jan. 2018. URL: https://inria.hal.science/hal-01637063.

[56] The Coq Development Team. *The Coq Proof Assistant*. Version 8.16. Sept. 2022. DOI: 10.5281/zenodo.7313584. URL: https://doi.org/10.5281/zenodo.7313584.

[57] The Univalent Foundations Program. *Homotopy Type Theory: Univalent Foundations of Mathematics*. Institute for Advanced Study: https://homotopytypetheory.org/book, 2013.

[58] Paweł Wieczorek and Dariusz Biernacki. "A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory". In: *Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs*. CPP 2018. Los Angeles, CA, USA: Association for Computing Machinery, 2018, pp. 266–279. ISBN: 9781450355865. DOI: 10.1145/3167091.

[59] Eric Wieser. *Multiple inheritance hazards in algebraic typeclass hierarchies*. 2023. arXiv: 2306.00617 [cs.LO].

[60] Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau. "Eliminating reflection from type theory". In: *Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019*. Ed. by Assia Mahboubi and Magnus O. Myreen. ACM, 2019, pp. 91–103. ISBN: 978-1-4503-6222-1. DOI: 10.1145/3293880.3294095. URL: https://doi.org/10.1145/3293880.3294095.
[50] Matthieu Sozeau. "Subset Coercions in Coq". In: *Types for Proofs and Programs*. Ed. by Thorsten Altenkirch and Conor McBride. Berlin, Heidelberg: Springer Berlin Heidelberg, 2007, pp. 237–252. ISBN: 978-3-540-74464-1.

[51] Matthieu Sozeau et al. "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq". Preprint. Apr. 2023. URL: https://inria.hal.science/hal-04077552.

[52] Jonathan Sterling. "Algebraic Type Theory and Universe Hierarchies". In: *CoRR abs/1902.08848* (2019). arXiv: 1902.08848.

[53] Pierre-Yves Strub. "Coq Modulo Theory". In: *Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings*. Ed. by Anuj Dawar and Helmut Veith. Vol. 6247. Lecture Notes in Computer Science. Springer, 2010, pp. 529–543. ISBN: 978-3-642-15204-7. DOI: 10.1007/978-3-642-15205-4_40. URL: https://doi.org/10.1007/978-3-642-15205-4%5C_40.

[54] Nikhil Swamy et al. "Dependent types and multi-monadic effects in F". In: *Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016*. Ed. by Rastislav Bodík and Rupak Majumdar. ACM, 2016, pp. 256–270. ISBN: 978-1-4503-3549-2. DOI: 10.1145/2837614.2837655. URL: https://doi.org/10.1145/2837614.2837655.

[55] Enrico Tassi. "Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect)". working paper or preprint. Jan. 2018. URL: https://inria.hal.science/hal-01637063.

[56] The Coq Development Team. *The Coq Proof Assistant*. Version 8.16. Sept. 2022. DOI: 10.5281/zenodo.7313584. URL: https://doi.org/10.5281/zenodo.7313584.

[57] The Univalent Foundations Program. *Homotopy Type Theory: Univalent Foundations of Mathematics*. Institute for Advanced Study: https://homotopytypetheory.org/book, 2013.

[58] Paweł Wieczorek and Dariusz Biernacki. "A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory". In: *Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs*. CPP 2018. Los Angeles, CA, USA: Association for Computing Machinery, 2018, pp. 266–279. ISBN: 9781450355865. DOI: 10.1145/3167091.

[59] Eric Wieser. *Multiple inheritance hazards in algebraic typeclass hierarchies*. 2023. arXiv: 2306.00617 [cs.LO].

[60] Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau. "Eliminating reflection from type theory". In: *Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019*. Ed. by Assia Mahboubi and Magnus O. Myreen. ACM, 2019, pp. 91–103. ISBN: 978-1-4503-6222-1. DOI: 10.1145/3293880.3294095. URL: https://doi.org/10.1145/3293880.3294095.
# A INTERNAL SUBTYPING AND UNDECIDABILITY OF CONVERSION

The goal of the coercive approach is to reflect all the potential ambiguities present in a subtyping derivation. As such, wouldn't it be easier to just internalize the notion of subtype and let type theory deal with it? The following observation shows that there exists a big obstruction to any decidability result for conversion as long as we want to stay equivalent to the subsumptive presentation of subtyping.

**OBSERVATION A.1 (NO-GO OF INTERNAL SUBTYPING).** Suppose that $\mathcal{T}$ is a type theory with a family sub $AB$ for any two types $A$ and $B$, equipped with reflexivity witnesses $refl_A$: sub $AA$ and transitivity witnesses $trans$ $w$ $w'$: sub $AC$ for $w$: sub $AB$ and $w'$: sub $BC$, as well as a coercion function $coe_{A,B}$: sub $AB \to A \to B$, such that $coe_{A,A} refl_A \cong id_A$ and $coe_{B,C} w \circ coe_{A,B} w' \cong coe_{A,C}(trans w_{A,B} w_{B,C})$. Then $\mathcal{T}$ embeds definitional models of the untyped $\lambda$-calculus, and in particular divergent terms.

Indeed, whenever a context provides inhabitants of both sub $AB$ and sub $BA$, $coe_{A,B}$ and $coe_{B,A}$ provide a definitional isomorphism $A \cong B$. In particular any context inhabiting sub $AA \to A$ and sub $A \to AA$, for instance an inconsistent one, provides a definitional retraction of $A \to A$ onto $A$, hence a non-trivial model of the untyped $\lambda$-calculus with a divergent element $\Omega_A: A$. This observation motivates our external approach to subtyping with a specific judgement of subtyping that cannot be abstracted upon.

# B ARTEFACT DESCRIPTION

## B.1 Organization of the Artefact and Other Resources

This section describes in more details the Coq formalisation accompanying this paper, more specifically the content of section 4. To complement it, we also provide the following:

* the REQUIREMENTS.md and INSTALL.md file with installation instructions;

* the README.md file with a quick overview of the development with hyperlinks to the files of interest;

* a DOCKER.md file, with installation and usage instructions for the provided docker image;

* a Readme.v file, which gives a more in-depth overview of the development as a Coq file, using directly the main Coq definitions and theorems, and is roughly similar to the present PDF description;

* a doc/dependency_graph.png file, showing the structure of the development.

We utilize the logical relation proof technique presented in Abel, Öhman, and Vezzosi [2] and build upon its Coq implementation due to Adjedj et al. [3]. This artefact contributes an extension of the formalisation with lists and definitional functor laws for lists. We refer to both articles for further details on the proof technique and the general setup of the formalisation.

## B.2 Syntax

Terms (AutoSubst/Ast). The syntax of terms, along with the other files in the AutoSubst folder, are generated using the AUTO SUBST plugin. The definition of renaming and substitution are also automatically derived from the one of terms, and many boilerplate lemmas on them are too. Of particular interest are the constructors tList, tNil, tCons, tElim and tMap, respectively corresponding to the type constructor for lists, the empty list, list consing, the (dependent) eliminator for lists, and the definitionally functorial map operation.

NormalForms. Weak-head normal forms whnf, neutrals whne and compacted neutrals whne_list are defined as inductive predicate on terms, i.e. as function of type term -> Prop, corresponding to
# A INTERNAL SUBTYPING AND UNDECIDABILITY OF CONVERSION

The goal of the coercive approach is to reflect all the potential ambiguities present in a subtyping derivation. As such, wouldn't it be easier to just internalize the notion of subtype and let type theory deal with it? The following observation shows that there exists a big obstruction to any decidability result for conversion as long as we want to stay equivalent to the subsumptive presentation of subtyping.

**OBSERVATION A.1 (NO-GO OF INTERNAL SUBTYPING).** Suppose that $\mathcal{T}$ is a type theory with a family sub $AB$ for any two types $A$ and $B$, equipped with reflexivity witnesses $refl_A$: sub $AA$ and transitivity witnesses $trans$ $w$ $w'$: sub $AC$ for $w$: sub $AB$ and $w'$: sub $BC$, as well as a coercion function $coe_{A,B}$: sub $AB \to A \to B$, such that $coe_{A,A} refl_A \cong id_A$ and $coe_{B,C} w \circ coe_{A,B} w' \cong coe_{A,C}(trans w_{A,B} w_{B,C})$. Then $\mathcal{T}$ embeds definitional models of the untyped $\lambda$-calculus, and in particular divergent terms.

Indeed, whenever a context provides inhabitants of both sub $AB$ and sub $BA$, $coe_{A,B}$ and $coe_{B,A}$ provide a definitional isomorphism $A \cong B$. In particular any context inhabiting sub $AA \to A$ and sub $A \to AA$, for instance an inconsistent one, provides a definitional retraction of $A \to A$ onto $A$, hence a non-trivial model of the untyped $\lambda$-calculus with a divergent element $\Omega_A: A$. This observation motivates our external approach to subtyping with a specific judgement of subtyping that cannot be abstracted upon.

# B ARTEFACT DESCRIPTION

## B.1 Organization of the Artefact and Other Resources

This section describes in more details the Coq formalisation accompanying this paper, more specifically the content of section 4. To complement it, we also provide the following:

* the REQUIREMENTS.md and INSTALL.md file with installation instructions;

* the README.md file with a quick overview of the development with hyperlinks to the files of interest;

* a DOCKER.md file, with installation and usage instructions for the provided docker image;

* a Readme.v file, which gives a more in-depth overview of the development as a Coq file, using directly the main Coq definitions and theorems, and is roughly similar to the present PDF description;

* a doc/dependency_graph.png file, showing the structure of the development.

We utilize the logical relation proof technique presented in Abel, Öhman, and Vezzosi [2] and build upon its Coq implementation due to Adjedj et al. [3]. This artefact contributes an extension of the formalisation with lists and definitional functor laws for lists. We refer to both articles for further details on the proof technique and the general setup of the formalisation.

## B.2 Syntax

Terms (AutoSubst/Ast). The syntax of terms, along with the other files in the AutoSubst folder, are generated using the AUTO SUBST plugin. The definition of renaming and substitution are also automatically derived from the one of terms, and many boilerplate lemmas on them are too. Of particular interest are the constructors tList, tNil, tCons, tElim and tMap, respectively corresponding to the type constructor for lists, the empty list, list consing, the (dependent) eliminator for lists, and the definitionally functorial map operation.

NormalForms. Weak-head normal forms whnf, neutrals whne and compacted neutrals whne_list are defined as inductive predicate on terms, i.e. as function of type term -> Prop, corresponding to
Fig. 4 and 10 from the paper. In particular, any compacted neutral is a normal form, and compacted neutrals can either consist of a map of a neutral, or simply of a neutral.

**Reduction (UntypedReduction).** Reduction, written `[l ⇒* l']`, is the transitive closure of one-step reduction `[l ⇒ *']`, defined as an inductive relation. In particular, we have the rules of Fig. 9, that is:

mapNil : `forall {A A' B f : term}, [tMap A B f (tNil A') ⇒ tNil B]`
mapCons : `forall {A A' B f a l : term},
[tMap A B f (tCons A' a l) ⇒ tCons B (tApp f a) (tMap A B f l)]`
mapComp : `forall {A B B' C f g l : term},
whe n l -> [tMap B C f (tMap A B' g l) ⇒ tMap A C (comp A f g) l]`

## B.3 Typing and Conversion

**GenericTyping.** Following Abel, Öhman, and Vezzosi [2] and Adjedj et al. [3], the definition of the logical relation is parametrized by a notion of *generic typing*, a common interface to be instantiated with both the declarative and algorithmic notions of typing. This interface features a family of judgments for context well-formation, typing, conversion but also a conversion of neutrals and a (typed) reduction relation. These judgements should satisfy properties, listed for each predicate with a record (*TypingProperties*, *ConvProperties*, etc.), and grouped together in the *GenericTypingProperties* record. We use type-classes to automatically find these properties when needed, and attach generic notations (defined in *Notations*) to these type-classes too.

For lists, generic typing closely resembles declarative typing, as defined in Fig. 2. Generic conversion must contain reduction, which includes typed variants of the rules above. Moreover, we have congruence rules for constructors, for instance we have the following, where ta stands for an arbitrary generic conversion:

`forall (Γ : context) (A A' : term),
[Γ |- [ta] A ≡ A' : U] -> [Γ |- [ta] tList A ≡ tList A' : U]`

Conversion is not constrained to be a congruence for destructors, but it must contain neutral conversion, which is a congruence for `tMap` and `tListElim`, provided its main argument is too. Factor laws are also specified at the level of neutral conversion.

**DeclarativeTyping.** The definition of the declarative judgments, as inductive predicates, corresponds to Fig. 2, 3, and 9 – the latter being restricted to the case of lists. The corresponding instance of generic typing is defined in *DeclarativeTypingInstance*. Neutral comparison is instantiated simply with conversion, i.e. the declarative instance does not distinguish between the two notions. Typed reduction is instantiated as the conjunction of declarative conversion and untyped reduction. All other judgments are directly instantiated with the corresponding declarative one.

**AlgorithmicTyping.** The raw algorithmic typing judgments, akin to Fig. 5 and 6, are again defined as inductive predicates. As we explain at the end of Section 2.3 in relation to Fig. 7, we must impose extra pre-conditions for these judgments to be well-behaved. The corresponding judgments, called *bundled*, are defined in *BundledAlgorithmicTyping*. In *AlgorithmicConvProperties* and *AlgorithmicTypingProperties*, we establish the properties of the conversion and typing judgments, to derive two new instances of generic typing. The first instance uses (bundled) algorithmic conversion, but declarative typing. It depends on consequences of the logical relation instantiated with the fully declarative instance. The second uses only bundled algorithmic judgments, but depends on consequences of the logical relation instantiated with the first, mixed instance.
Fig. 4 and 10 from the paper. In particular, any compacted neutral is a normal form, and compacted neutrals can either consist of a map of a neutral, or simply of a neutral.

**Reduction (UntypedReduction).** Reduction, written `[l ⇒* l']`, is the transitive closure of one-step reduction `[l ⇒ *']`, defined as an inductive relation. In particular, we have the rules of Fig. 9, that is:

mapNil : `forall {A A' B f : term}, [tMap A B f (tNil A') ⇒ tNil B]`
mapCons : `forall {A A' B f a l : term},
[tMap A B f (tCons A' a l) ⇒ tCons B (tApp f a) (tMap A B f l)]`
mapComp : `forall {A B B' C f g l : term},
whe l -> [tMap B C f (tMap A B' g l) ⇒ tMap A C (comp A f g) l]`

## B.3 Typing and Conversion

**GenericTyping.** Following Abel, Öhman, and Vezzosi [2] and Adjedj et al. [3], the definition of the logical relation is parametrized by a notion of *generic typing*, a common interface to be instantiated with both the declarative and algorithmic notions of typing. This interface features a family of judgments for context well-formation, typing, conversion but also a conversion of neutrals and a (typed) reduction relation. These judgements should satisfy properties, listed for each predicate with a record (*TypingProperties*, *ConvProperties*, etc.), and grouped together in the *GenericTypingProperties* record. We use type-classes to automatically find these properties when needed, and attach generic notations (defined in *Notations*) to these type-classes too.

For lists, generic typing closely resembles declarative typing, as defined in Fig. 2. Generic conversion must contain reduction, which includes typed variants of the rules above. Moreover, we have congruence rules for constructors, for instance we have the following, where `ta` stands for an arbitrary generic conversion:

`forall (Γ : context) (A A' : term),
[Γ |- [ta] A ≡ A' : U] -> [Γ |- [ta] tList A ≡ tList A' : U]`

Conversion is not constrained to be a congruence for destructors, but it must contain neutral conversion, which is a congruence for `tMap` and `tListElim`, provided its main argument is too. Factor laws are also specified at the level of neutral conversion.

**DeclarativeTyping.** The definition of the declarative judgments, as inductive predicates, corresponds to Fig. 2, 3, and 9 – the latter being restricted to the case of lists. The corresponding instance of generic typing is defined in *DeclarativeTypingInstance*. Neutral comparison is instantiated simply with conversion, i.e. the declarative instance does not distinguish between the two notions. Typed reduction is instantiated as the conjunction of declarative conversion and untyped reduction. All other judgments are directly instantiated with the corresponding declarative one.

**AlgorithmicTyping.** The raw algorithmic typing judgments, akin to Fig. 5 and 6, are again defined as inductive predicates. As we explain at the end of Section 2.3 in relation to Fig. 7, we must impose extra pre-conditions for these judgments to be well-behaved. The corresponding judgments, called *bundled*, are defined in *BundledAlgorithmicTyping*. In *AlgorithmicConvProperties* and *AlgorithmicTypingProperties*, we establish the properties of the conversion and typing judgments, to derive two new instances of generic typing. The first instance uses (bundled) algorithmic conversion, but declarative typing. It depends on consequences of the logical relation instantiated with the fully declarative instance. The second uses only bundled algorithmic judgments, but depends on consequences of the logical relation instantiated with the first, mixed instance.
## B.4 The Logical Relation

The logical relation is built from two layers, first the reducibility layer attaching witnesses of reducibility to weak-head normal form and second the validity layer that closes reducibility under substitution.

*Definition of reducibility (LogicalRelation).* The reducibility layer describes the types A that are reducible in a given context $\Gamma$ and level $l$, noted $[\Gamma || -<l> A]$ . Informally, a type is reducible when it weak-head reduces to a (weak-head) normal form, and the subterms of this normal form are themselves reducible. This weak-head normal form, when it exists, is unique by determinism of the weak-head reduction strategy. A witness of reducibility $RA : [\Gamma || -<l> A]$ for the type A induce three subsequent predicates:

* reducible conversion of a type B to A, noted $[\Gamma || -<l> A \equiv B | RA]$,

* reducibility of terms t of type A, noted $[\Gamma || -<l> t : A | RA]$,

* reducible conversion of terms t,u of type A, noted $[\Gamma || -<l> t \equiv u : A | RA]$.

These three predicates are packed in a single record LRPack. Reducible types are characterized inductively together with their associated LRPack using an indexed inductive LR. This encoding of a seemingly inductive-recursive definition using the inductively generated graph of the functions is known as small-induction recursion. The actual content of the reducibility relation is defined independently for each type formers as well as the neutrals types. We focus here on the reducibility of lists and refer to [3, 2] for the other type formers.

A type A is reducible as a list if it weak-head reduces to a type of shape tList par where the parameter type par is itself reducible in any weakening of the context $\Gamma$. This Kripke-style quantification on all future (weakened) contexts $\Delta \le \Gamma$ is necessary for specifying reducibility in larger contexts.

Reducible terms of list type are defined inductively in two steps: ListProp holds of canonical forms of type list (nil, cons and neutrals) with reducible arguments; ListRedTm holds of terms that weak-head reduce to a reducible canonical form. The two inductive definitions must be mutual since the tail of a reducible tCons need not to be in weak-head normal form. A neutral term of list type is reducible if it is a well-typed neutral and moreover, if it is of shape $tMap A B f l$ with $l$ necessary neutral itself, then the body $f(\text{wk1 } \Gamma A)(t\text{Rel } 0)$ of $f$ must be reducible in an extended context $\Gamma, A$. In the latter case, the type B of the codomain of $f$ cannot be required to be reducible since that would lead to non-well-founded definition for the logical relation, but it is reducibly convertible to the reducible parameter type par at which reducibility of lists is defined.

Reducible conversion between terms of list type follow a similar pattern. In order to account for the identity functor law, the additional reducibility datum needed to relate two neutral terms also depends on the shape of the terms:

* if both terms are respectively of the shape $tMap A B f l$ and $tMap A' B' f' l'$, then the bodies of $f$ and $f'$ must be reducibly convertible (congruence);

* if only one of the term is of shape $tMap A B f l$, then $f$ must be reducibly convertible to the identity function, i.e. its body must be reducibly convertible to the first variable in context $t\text{Rel } 0$.

*Properties of Reducibility.* In order to reason on reducibility, we derive the induction principle corresponding to the inductive-recursive definition of the logical relation in LogicalRelation/Induction. This induction principle is then employed to derive a variety of properties of reducibility in the LogicalRelation/ subdirectory: an inversion principle, irrelevance with respect to reducible conversion, reflexivity, symmetry and transitivity of reducible conversion, stability by weakening and by anti-reduction.
## B.4 The Logical Relation

The logical relation is built from two layers, first the reducibility layer attaching witnesses of reducibility to weak-head normal form and second the validity layer that closes reducibility under substitution.

*Definition of reducibility (LogicalRelation).* The reducibility layer describes the types A that are reducible in a given context $Γ$ and level $l$, noted $[Γ || -<l> A]$ . Informally, a type is reducible when it weak-head reduces to a (weak-head) normal form, and the subterms of this normal form are themselves reducible. This weak-head normal form, when it exists, is unique by determinism of the weak-head reduction strategy. A witness of reducibility $RA : [Γ || -<l> A]$ for the type A induce three subsequent predicates:

* reducible conversion of a type B to A, noted $[Γ || -<l> A ≡ B | RA]$,

* reducibility of terms t of type A, noted $[Γ || -<l> t : A | RA]$,

* reducible conversion of terms t,u of type A, noted $[Γ || -<l> t ≡ u : A | RA]$.

These three predicates are packed in a single record LRPack. Reducible types are characterized inductively together with their associated LRPack using an indexed inductive LR. This encoding of a seemingly inductive-recursive definition using the inductively generated graph of the functions is known as small-induction recursion. The actual content of the reducibility relation is defined independently for each type formers as well as the neutrals types. We focus here on the reducibility of lists and refer to [3, 2] for the other type formers.

A type A is reducible as a list if it weak-head reduces to a type of shape tList par where the parameter type par is itself reducible in any weakening of the context $Γ$. This Kripke-style quantification on all future (weakened) contexts $Δ ≤ Γ$ is necessary for specifying reducibility in larger contexts.

Reducible terms of list type are defined inductively in two steps: ListProp holds of canonical forms of type list (nil, cons and neutrals) with reducible arguments; ListRedTm holds of terms that weak-head reduce to a reducible canonical form. The two inductive definitions must be mutual since the tail of a reducible tCons need not to be in weak-head normal form. A neutral term of list type is reducible if it is a well-typed neutral and moreover, if it is of shape tMap A B f l with l necessary neutral itself, then the body $f(\text{wk1 } Γ A)(tRel 0)$ of f must be reducible in an extended context $Γ, A$. In the latter case, the type B of the codomain of f cannot be required to be reducible since that would lead to non-well-founded definition for the logical relation, but it is reducibly convertible to the reducible parameter type par at which reducibility of lists is defined.

Reducible conversion between terms of list type follow a similar pattern. In order to account for the identity functor law, the additional reducibility datum needed to relate two neutral terms also depends on the shape of the terms:

* if both terms are respectively of the shape $tMap A B f l$ and $tMap A' B' f' l'$, then the bodies of f and f' must be reducibly convertible (congruence);

* if only one of the term is of shape $tMap A B f l$, then f must be reducibly convertible to the identity function, i.e. its body must be reducibly convertible to the first variable in context $tRel 0$.

*Properties of Reducibility.* In order to reason on reducibility, we derive the induction principle corresponding to the inductive-recursive definition of the logical relation in LogicalRelation/Induction. This induction principle is then employed to derive a variety of properties of reducibility in the LogicalRelation/ subdirectory: an inversion principle, irrelevance with respect to reducible conversion, reflexivity, symmetry and transitivity of reducible conversion, stability by weakening and by anti-reduction.
**Validity and the Fundamental Lemma.** Validity closes reducibility by reducible substitution using another encoding of an inductive-recursive schema. The fundamental lemma then states that all components of a derivable declarative judgement are valid, in particular, terms well-typed for the declarative presentation are valid. The proof of the fundamental lemma proceed by an induction on declarative typing derivations, using that each declarative derivation step is admissible for the validity logical relation. These admissibility results are shown independently for each type former in the *Substitution/Introductions/* subdirectory. Most type and term formers related to lists are in *List*, while the eliminator for lists is in *ListElim*. The proofs follow the description of the logical relation: first, we show that each type, term or conversion equation is reducible using the definition and properties of reducibility, and then that it is valid. To show that the functor laws are valid, we use that composition of functions (e.g. morphisms for list) is definitionally associative and unital.

## B.5 Type-checker (Decidability folder)

**Open Recursion for Partial Functions.** To side-step issues with the complex termination argument of the conversion checker, we define it in an open recursion fashion, relying on a form of free monad. The functions for reduction, conversion and type checking are defined in *Decidability/Functions*. The main change compared to Adjedj et al. [3] is the addition of compaction to weak-head evaluation. Evaluation is implemented using a stack machine, on which elimination forms are pushed as they are encountered. When the machine hits a variable, for Adjedj et al. [3] it means the whole term – the variable against the stack of eliminations – is a neutral. However, this is not the case for us: we want to compute a compacted neutral. Thus, we add an extra compaction pass, implemented by the *compact* function, which merges successive map operations on the stack as we unpile them.

**Correctness of the Functions.** Correctness of the implementations is shown in three steps. First, we show *Soundness*, i.e. that a positive answer of the checker implies the corresponding (algorithmic) judgment. Next, we show *Completeness*, i.e. that whenever an algorithmic judgment holds, then the corresponding checker answers positively. Finally, we show *Termination*, i.e. that the checkers always terminates when run on well-typed inputs. Again, the main innovation has to do with compaction. To reason about it, we need to make explicit the invariant that the stack is always “well-typed”, in a suitable sense, see *typed_stack* in *Completeness*.

## B.6 Main properties

The main properties we obtain from the logical relations and the certified checker are the following. First, every well-typed term and type are (weakly) normalising (proven in *Normalisation*):

Record WN (t : term) := {
    wn_val : term; wn_red : [t ⇒* wn_val ]; wn_whnf : whnf wn_val; }.
Corollary normalisation {Γ A t} : [Γ |-[de] t : A] -> WN t.
Corollary type_normalisation {Γ A} : [Γ |-[de] A] -> WN A.

Conversion and typing are decidable (proven in *Decidability*):

Definition checkoj (Γ : context) (T t t' : term) (hΓ : [Γ] )
(hT : [Γ|-T]) (ht : [Γ|-t : T]) (ht' : [Γ|-t' : T]) :
[Γ|-t ≡ t' : T] + ~[Γ|-t ≡ t' : T].
Definition check_full Γ (T t : term) : [Γ|-t : T] + ~[Γ|-t : T].

Finally, the type system seen as a logic is consistent, and canonicity holds at the type of natural numbers:
**Validity and the Fundamental Lemma.** Validity closes reducibility by reducible substitution using another encoding of an inductive-recursive schema. The fundamental lemma then states that all components of a derivable declarative judgement are valid, in particular, terms well-typed for the declarative presentation are valid. The proof of the fundamental lemma proceed by an induction on declarative typing derivations, using that each declarative derivation step is admissible for the validity logical relation. These admissibility results are shown independently for each type former in the *Substitution/Introductions/* subdirectory. Most type and term formers related to lists are in *List*, while the eliminator for lists is in *ListElim*. The proofs follow the description of the logical relation: first, we show that each type, term or conversion equation is reducible using the definition and properties of reducibility, and then that it is valid. To show that the functor laws are valid, we use that composition of functions (e.g. morphisms for list) is definitionally associative and unital.

## B.5 Type-checker (Decidability folder)

**Open Recursion for Partial Functions.** To side-step issues with the complex termination argument of the conversion checker, we define it in an open recursion fashion, relying on a form of free monad. The functions for reduction, conversion and type checking are defined in *Decidability/Functions*. The main change compared to Adjedj et al. [3] is the addition of compaction to weak-head evaluation. Evaluation is implemented using a stack machine, on which elimination forms are pushed as they are encountered. When the machine hits a variable, for Adjedj et al. [3] it means the whole term – the variable against the stack of eliminations – is a neutral. However, this is not the case for us: we want to compute a compacted neutral. Thus, we add an extra compaction pass, implemented by the *compact* function, which merges successive map operations on the stack as we unpile them.

**Correctness of the Functions.** Correctness of the implementations is shown in three steps. First, we show *Soundness*, i.e. that a positive answer of the checker implies the corresponding (algorithmic) judgment. Next, we show *Completeness*, i.e. that whenever an algorithmic judgment holds, then the corresponding checker answers positively. Finally, we show *Termination*, i.e. that the checkers always terminates when run on well-typed inputs. Again, the main innovation has to do with compaction. To reason about it, we need to make explicit the invariant that the stack is always “well-typed”, in a suitable sense, see *typed_stack* in *Completeness*.

## B.6 Main properties

The main properties we obtain from the logical relations and the certified checker are the following. First, every well-typed term and type are (weakly) normalising (proven in *Normalisation*):

Record WN (t : term) := {
    wn_val : term; wn_red : [t ⇒* wn_val ]; wn_whnf : whnf wn_val; }.

Corollary normalisation {Γ A t} : [Γ |-[de] t : A] -> WN t.

Corollary type_normalisation {Γ A} : [Γ |-[de] A] -> WN A.

Conversion and typing are decidable (proven in *Decidability*):

Definition checkoj (Γ : context) (T t t' : term) (hΓ : [Γ] )
(hT : [Γ|-T]) (ht : [Γ|-t : T]) (ht' : [Γ|-t' : T]) :
[Γ|-t ≡ t' : T] + ~[Γ|-t ≡ t' : T].

Definition check_full Γ (T t : term) : [Γ|-t : T] + ~[Γ|-t : T].

Finally, the type system seen as a logic is consistent, and canonicity holds at the type of natural numbers:
Lemma consistency `{t}` : `[ε | - t : tEmpty]` -> False.

Lemma nat_canonicity `{t}` : `[ε | - t : tNat]` ->
∑ n : nat, [ε | - t ≡ Nat.iter n tSucc tZero : tNat].

# C COMPLETE TYPING RULES

## C.1 Declarative MLTT

### Γ ⊢ Γ Context Γ is well-formed

$$ \vdash . \qquad \frac{\vdash \Gamma \quad \Gamma \vdash A : \mathbf{Type}_i}{\vdash \Gamma, x : A} $$

### Γ ⊢ σ : Δ σ is a well-typed substitution between contexts Γ and Δ

$$ \overline{\Gamma \vdash . : .} \qquad \frac{\Gamma \vdash \sigma : \Delta \quad \Gamma \vdash t : A[\sigma]}{\Gamma \vdash (\sigma, t) : \Delta, x : A} $$

### Γ ⊢ T Type T is well-formed in context Γ

$$ \mathrm{EL} \quad \frac{\Gamma \vdash A : \mathbf{Type}_i}{\Gamma \vdash A} \qquad \mathrm{FUNTY} \quad \frac{\Gamma \vdash A \quad \Gamma, x : A \vdash B}{\Gamma \vdash \Pi x : A.B} \qquad \mathrm{LISTTY} \quad \frac{\Gamma \vdash A}{\Gamma \vdash \mathbf{List} A} $$

$$ \mathrm{SIGTY} \quad \frac{\Gamma \vdash A \quad \Gamma, x : A \vdash B}{\Gamma \vdash \Sigma x : A.B} \qquad \mathrm{TREETY} \quad \frac{\Gamma \vdash A \quad \Gamma, x : A \vdash B}{\Gamma \vdash \mathbf{W} x : A.B} $$

$$ \mathrm{IDTY} \quad \frac{\Gamma \vdash A \quad \Gamma \vdash a : A \quad \Gamma \vdash a' : A}{\Gamma \vdash \mathbf{Id}_A a a'} \qquad \mathrm{SUMTY} \quad \frac{\Gamma \vdash A \quad \Gamma \vdash B}{\Gamma \vdash A + B} $$

### Γ ⊢ t : T Term t has type T under context Γ

$$ \mathrm{CONV} \quad \frac{\Gamma \vdash t : A \quad \Gamma \vdash A \cong B}{\Gamma \vdash t : B} \qquad \mathrm{VAR} \quad \frac{\vdash \Gamma \quad (x : A) \in \Gamma}{\Gamma \vdash x : A} \qquad \mathrm{SORT} \quad \frac{\vdash \Gamma}{\Gamma \vdash \mathbf{Type}_i : \mathbf{Type}_{i+1}} $$

$$ \mathrm{FUNUNI} \quad \frac{\Gamma \vdash A : \mathbf{Type}_i}{\Gamma, x : A \vdash B : \mathbf{Type}_i} \qquad \mathrm{ABS} \quad \frac{\Gamma \vdash A \quad \Gamma, x : A \vdash B}{\Gamma \vdash \lambda x : A.t : \Pi x : A.B} \qquad \mathrm{APP} \quad \frac{\Gamma \vdash t : \Pi x : A.B}{\Gamma \vdash t u : A} $$

$$ \mathrm{LISTUNI} \quad \frac{\Gamma \vdash A : \mathbf{Type}_i}{\Gamma \vdash \mathbf{List} A : \mathbf{Type}_i} \qquad \mathrm{NIL} \quad \frac{\Gamma \vdash A}{\Gamma \vdash \varepsilon_A : \mathbf{List} A} \qquad \mathrm{CONS} \quad \frac{\Gamma \vdash A \quad \Gamma \vdash a : A}{\Gamma \vdash a ::_A l : \mathbf{List} A} $$

$$ \mathrm{LISTIND} \quad \frac{\Gamma, x : \mathbf{List} A \vdash P}{\Gamma \vdash b_{\varepsilon} : P[\varepsilon_A]} \qquad \Gamma \vdash A \quad \Gamma \vdash s : \mathbf{List} A \qquad \Gamma, x : A, y : \mathbf{List} A, z : P[y] \vdash b_{\ddagger} : P[x ::_A y] \\ \qquad \Gamma \vdash \mathrm{ind}_{\mathbf{List} A} (s; z.P; b_{\varepsilon}, x.y.z.b_{\ddagger}) : P[s] $$

$$ \mathrm{EMPTYUNI} \quad \overline{\Gamma \vdash \mathbf{0} : \mathbf{Type}_0} \qquad \mathrm{UNITUNI} \quad \overline{\Gamma \vdash \mathbf{1} : \mathbf{Type}_0} \qquad \mathrm{UNITTM} \quad \overline{\Gamma \vdash () : \mathbf{1}} $$
Lemma consistency {$t$} : [$\varepsilon$ | - t : tEmpty] -> False.

Lemma nat_canonicity {$t$} : [$\varepsilon$ | - t : tNat] ->
$\Sigma n : \text{nat}, [\varepsilon | - t \equiv \text{Nat.iter} n \text{ tSucc tZero} : \text{tNat}]$.

C COMPLETE TYPING RULES

C.1 Declarative MLTT

$\vdash \Gamma$ Context $\Gamma$ is well-formed

$$ \overline{\vdash .} \qquad \frac{\vdash \Gamma \quad \Gamma \vdash A : \mathit{Type}_i}{\vdash \Gamma, x : A} $$

$\Gamma \vdash \sigma : \Delta$ $\sigma$ is a well-typed substitution between contexts $\Gamma$ and $\Delta$

$$ \overline{\Gamma \vdash . : .} \qquad \frac{\Gamma \vdash \sigma : \Delta \quad \Gamma \vdash t : A[\sigma]}{\Gamma \vdash (\sigma, t) : \Delta, x : A} $$

$\Gamma \vdash T$ Type $T$ is well-formed in context $\Gamma$

$$ \mathrm{EL} \quad \frac{\Gamma \vdash A : \mathit{Type}_i}{\Gamma \vdash A} \qquad \mathrm{FUNTY} \quad \frac{\Gamma \vdash A \quad \Gamma, x : A \vdash B}{\Gamma \vdash \Pi x : A.B} \qquad \mathrm{LISTTY} \quad \frac{\Gamma \vdash A}{\Gamma \vdash \mathbf{List} A} $$

$$ \mathrm{SIGTY} \quad \frac{\Gamma \vdash A \quad \Gamma, x : A \vdash B}{\Gamma \vdash \Sigma x : A.B} \qquad \mathrm{TREETY} \quad \frac{\Gamma \vdash A \quad \Gamma, x : A \vdash B}{\Gamma \vdash \mathbf{W} x : A.B} $$

$$ \mathrm{IDTY} \quad \frac{\Gamma \vdash A \quad \Gamma \vdash a : A \quad \Gamma \vdash a' : A}{\Gamma \vdash \mathbf{Id}_A a a'} \qquad \mathrm{SUMTY} \quad \frac{\Gamma \vdash A \quad \Gamma \vdash B}{\Gamma \vdash A + B} $$

$\Gamma \vdash t : T$ Term $t$ has type $T$ under context $\Gamma$

$$ \mathrm{CONV} \quad \frac{\Gamma \vdash t : A \quad \Gamma \vdash A \cong B}{\Gamma \vdash t : B} \qquad \mathrm{VAR} \quad \frac{\vdash \Gamma \quad (x : A) \in \Gamma}{\Gamma \vdash x : A} \qquad \mathrm{SORT} \quad \frac{\vdash \Gamma}{\Gamma \vdash \mathit{Type}_i : \mathit{Type}_{i+1}} $$

$$ \mathrm{FUNUNI} \quad \frac{\Gamma \vdash A : \mathit{Type}_i}{\Gamma, x : A \vdash B : \mathit{Type}_i} \qquad \mathrm{ABS} \quad \frac{\Gamma \vdash A \quad \Gamma, x : A \vdash B}{\Gamma \vdash \lambda x : A.t \vdash \Pi x : A.B} \qquad \mathrm{APP} \quad \frac{\Gamma \vdash t : \Pi x : A.B}{\Gamma \vdash u : A} $$

$$ \mathrm{LISTUNI} \quad \frac{\Gamma \vdash A : \mathit{Type}_i}{\Gamma \vdash \mathbf{List} A : \mathit{Type}_i} \qquad \mathrm{NIL} \quad \frac{\Gamma \vdash A}{\Gamma \vdash \varepsilon_A : \mathbf{List} A} \qquad \mathrm{CONS} \quad \frac{\Gamma \vdash A \quad \Gamma \vdash a : A}{\Gamma \vdash a ::_A l : \mathbf{List} A} $$

$$ \mathrm{LISTIND} \quad \frac{\Gamma, x : \mathbf{List} A \vdash P}{\Gamma \vdash b_{\varepsilon} : P[\varepsilon_A]} \qquad \Gamma \vdash A \qquad \Gamma \vdash s : \mathbf{List} A \qquad \Gamma, x : A, y : \mathbf{List} A, z : P[y] \vdash b_{\equiv} : P[x ::_A y] \\ \qquad \Gamma \vdash \mathrm{ind}_{\mathbf{List} A} (s; z.P; b_{\varepsilon}, x.y.z.b_{\equiv}) : P[s] $$

$$ \mathrm{EMPTYUNI} \quad \overline{\Gamma \vdash \mathbf{0} : \mathit{Type}_0} \qquad \mathrm{UNITUNI} \quad \overline{\Gamma \vdash \mathbf{1} : \mathit{Type}_0} \qquad \mathrm{UNITTM} \quad \overline{\Gamma \vdash () : \mathbf{1}} $$
$$ \text{EMPTYIND} \frac{\Gamma \vdash s : \mathbf{0} \qquad \Gamma \vdash P}{\Gamma \vdash \text{ind}_0(s; P) : P} $$

$$ \text{UNITIND} \frac{\Gamma \vdash s : \mathbf{1} \qquad \Gamma, z : \mathbf{1} \vdash P \qquad \Gamma \vdash b_0 : P(\emptyset)}{\Gamma \vdash \text{ind}_1(s; z.P; b_0) : P[s]} $$

$$ \text{SIGUNI} \frac{\Gamma \vdash A : \text{Type}_i \qquad \Gamma, x : A \vdash B : \text{Type}_i}{\Gamma \vdash \Sigma x : A.B : \text{Type}_i} $$

$$ \text{PAIR} \frac{\Gamma \vdash t : A \qquad \Gamma \vdash u : B[t]}{\Gamma \vdash (t, u)_{x.B} : \Sigma x : A.B} $$

$$ \text{PROJ}_1 \frac{\Gamma \vdash p : \Sigma x : A.B}{\Gamma \vdash \pi_1 p : A} $$

$$ \text{PROJ}_2 \frac{\Gamma \vdash p : \Sigma x : A.B}{\Gamma \vdash \pi_2 p : B[u]} $$

$$ \text{TREEUNI} \frac{\Gamma \vdash A : \text{Type}_i \qquad \Gamma, x : A \vdash B : \text{Type}_i}{\Gamma \vdash \mathbf{W} x : A.B : \text{Type}_i} $$

$$ \text{SUP} \frac{\Gamma \vdash a : A \qquad \Gamma \vdash k : B[a] \rightarrow \mathbf{W} x : A.B}{\Gamma \vdash \sup_{x.B} a k : \mathbf{W} x : A.B} $$

$$ \text{TREEIND} \frac{\Gamma \vdash A \qquad \Gamma, x : A \vdash B \qquad \Gamma \vdash s : \mathbf{W} x : A.B \qquad \Gamma, z : \mathbf{W} x : A.B \vdash P}{\Gamma, x : A, y : B[x] \rightarrow W x : A.B, h : \Pi z : B[x].P[yz] \vdash b : P[\sup_{x.B} x y]} \qquad \Gamma \vdash \text{ind}_{\mathbf{W} x : A.B}(s; z.P; x.y.z.b) : P[s] $$

$$ \text{BOOLUNI} \frac{\Gamma \vdash \mathbf{B} : \text{Type}_0}{\Gamma \vdash \mathbf{B}} $$

$$ \text{TRUE} \frac{\Gamma \vdash \text{tt} : \mathbf{B}}{\Gamma \vdash \text{tt}} $$

$$ \text{FALSE} \frac{\Gamma \vdash \text{ff} : \mathbf{B}}{\Gamma \vdash \text{ff}} $$

$$ \text{BOOLIND} \frac{\Gamma \vdash s : \mathbf{B} \qquad \Gamma, z : \mathbf{B} \vdash P \qquad \Gamma \vdash b_{tt} : P[\text{tt}] \qquad \Gamma \vdash b_{ff} : P[\text{ff}]}{\Gamma \vdash \text{ind}_{\mathbf{B}}(s; z.P; b_{tt}, b_{ff}) : P[s]} $$

$$ \text{SUMUNI} \frac{\Gamma \vdash A : \text{Type}_i \qquad \Gamma \vdash B : \text{Type}_i}{\Gamma \vdash A + B : \text{Type}_i} $$

$$ \text{SUMINJLEFT} \frac{\Gamma \vdash B \qquad \Gamma \vdash a : A}{\Gamma \vdash \text{inj}_B^l a : A + B} $$

$$ \text{SUMINJRIGHT} \frac{\Gamma \vdash A \qquad \Gamma \vdash b : B}{\Gamma \vdash \text{inj}_A^r b : A + B} $$

$$ \text{SUMIND} \frac{\Gamma \vdash s : A + B \qquad \Gamma, z : A + B \vdash P}{\Gamma, x : A \vdash b_l : P[\text{inj}_B^l x] \qquad \Gamma, x : B \vdash b_r : P[\text{inj}_A^r x]} \qquad \Gamma \vdash \text{ind}_+(s; z.P; x.b_l, x.b_r) : P[s] $$

$$ \text{IDTY} \frac{\Gamma \vdash A \qquad \Gamma \vdash a : A \qquad \Gamma \vdash a' : A}{\Gamma \vdash \mathbf{Id}_A a a'} $$

$$ \text{REFLTM} \frac{\Gamma \vdash A \qquad \Gamma \vdash a : A}{\Gamma \vdash \text{refl}_{A,a} : \mathbf{Id}_A a a} $$

$$ \text{IDIND} \frac{\Gamma \vdash s : \mathbf{Id}_A a a' \qquad \Gamma, x : A, y : A, z : \mathbf{Id}_A x y \vdash P \qquad \Gamma, x : A \vdash b : P[\text{id}, x, x, \text{refl}_{A,x}]}{\Gamma \vdash \text{ind}_{\mathbf{Id}_A}(s; x.y.z.P; x.b) : P[a, a', s]} $$
$$ \text{EMPTYIND} \frac{\Gamma \vdash s : \mathbf{0} \qquad \Gamma \vdash P}{\Gamma \vdash \text{ind}_0(s; P) : P} $$

$$ \text{UNITIND} \frac{\Gamma \vdash s : \mathbf{1} \qquad \Gamma, z : \mathbf{1} \vdash P \qquad \Gamma \vdash b_0 : P(\emptyset)}{\Gamma \vdash \text{ind}_1(s; z.P; b_0) : P[s]} $$

$$ \text{SIGUNI} \frac{\Gamma \vdash A : \text{Type}_i \qquad \Gamma, x : A \vdash B : \text{Type}_i}{\Gamma \vdash \Sigma x : A.B : \text{Type}_i} $$

$$ \text{PAIR} \frac{\Gamma \vdash t : A \qquad \Gamma \vdash u : B[t]}{\Gamma \vdash (t, u)_{x.B} : \Sigma x : A.B} $$

$$ \text{PROJ}_1 \frac{\Gamma \vdash p : \Sigma x : A.B}{\Gamma \vdash \pi_1 p : A} $$

$$ \text{PROJ}_2 \frac{\Gamma \vdash p : \Sigma x : A.B}{\Gamma \vdash \pi_2 p : B[u]} $$

$$ \text{TREEUNI} \frac{\Gamma \vdash A : \text{Type}_i \qquad \Gamma, x : A \vdash B : \text{Type}_i}{\Gamma \vdash \mathbf{W} x : A.B : \text{Type}_i} $$

$$ \text{SUP} \frac{\Gamma \vdash a : A \qquad \Gamma \vdash k : B[a] \to \mathbf{W} x : A.B}{\Gamma \vdash \sup_{x.B} a : \mathbf{W} x : A.B} $$

$$ \text{TREEIND} \frac{\Gamma \vdash A \qquad \Gamma, x : A \vdash B \qquad \Gamma \vdash s : \mathbf{W} x : A.B \qquad \Gamma, z : \mathbf{W} x : A.B \vdash P}{\Gamma, x : A, y : B[x] \to W x : A.B, h : \Pi z : B[x].P[yz] \vdash b : P[\sup_{x.B} x y]} \qquad \Gamma \vdash \text{ind}_{\mathbf{W} x : A.B}(s; z.P; x.y.z.b) : P[s] $$

$$ \text{BOOLUNI} \frac{\Gamma \vdash \mathbf{B} : \text{Type}_0}{\Gamma \vdash \mathbf{B}} $$

$$ \text{TRUE} \frac{\Gamma \vdash \text{tt} : \mathbf{B}}{\Gamma \vdash \text{tt}} $$

$$ \text{FALSE} \frac{\Gamma \vdash \text{ff} : \mathbf{B}}{\Gamma \vdash \text{ff}} $$

$$ \text{BOOLIND} \frac{\Gamma \vdash s : \mathbf{B} \qquad \Gamma, z : \mathbf{B} \vdash P \qquad \Gamma \vdash b_{tt} : P[\text{tt}] \qquad \Gamma \vdash b_{ff} : P[\text{ff}]}{\Gamma \vdash \text{ind}_{\mathbf{B}}(s; z.P; b_{tt}, b_{ff}) : P[s]} $$

$$ \text{SUMUNI} \frac{\Gamma \vdash A : \text{Type}_i \qquad \Gamma \vdash B : \text{Type}_i}{\Gamma \vdash A + B : \text{Type}_i} $$

$$ \text{SUMINJLEFT} \frac{\Gamma \vdash B \qquad \Gamma \vdash a : A}{\Gamma \vdash \text{inj}_B^l a : A + B} $$

$$ \text{SUMINJRIGHT} \frac{\Gamma \vdash A \qquad \Gamma \vdash b : B}{\Gamma \vdash \text{inj}_A^r b : A + B} $$

$$ \text{SUMIND} \frac{\Gamma \vdash s : A + B \qquad \Gamma, z : A + B \vdash P}{\Gamma, x : A \vdash b_l : P[\text{inj}_B^l x] \qquad \Gamma, x : B \vdash b_r : P[\text{inj}_A^r x]} \qquad \Gamma \vdash \text{ind}_+(s; z.P; x.b_l, x.b_r) : P[s] $$

$$ \text{IDTY} \frac{\Gamma \vdash A \qquad \Gamma \vdash a : A \qquad \Gamma \vdash a' : A}{\Gamma \vdash \mathbf{Id}_A a a'} $$

$$ \text{REFLTM} \frac{\Gamma \vdash A \qquad \Gamma \vdash a : A}{\Gamma \vdash \text{refl}_{A,a} : \mathbf{Id}_A a a} $$

$$ \text{IDIND} \frac{\Gamma \vdash s : \mathbf{Id}_A a a' \qquad \Gamma, x : A, y : A, z : \mathbf{Id}_A x y \vdash P \qquad \Gamma, x : A \vdash b : P[\text{id}, x, x, \text{refl}_{A,x}]}{\Gamma \vdash \text{ind}_{\mathbf{Id}_A}(s; x.y.z.P; x.b) : P[a, a', s]} $$
$\Gamma \vdash T \cong T'$

Types *T* and *T'* are convertible in context $\Gamma$

$$ \text{REFLTY} \quad \frac{\Gamma \vdash A}{\Gamma \vdash A \cong A} $$

$$ \text{TRANS TY} \quad \frac{\Gamma \vdash A \cong B \qquad \Gamma \vdash B \cong C}{\Gamma \vdash A \cong C} $$

$$ \text{ELC} \quad \frac{\Gamma \vdash A \cong A' : \text{Type}_i}{\Gamma \vdash A \cong A'} $$

$$ \text{FUNTYC} \quad \frac{\Gamma \vdash A \cong A' \qquad \Gamma, x : A \vdash B \cong B'}{\Gamma \vdash \Pi x : A.B \cong \Pi x : A'.B'} $$

$$ \text{LIST TYC} \quad \frac{\Gamma \vdash A \cong A'}{\Gamma \vdash \mathbf{List} A \cong \mathbf{List} A'} $$

$$ \text{SIGTYC} \quad \frac{\Gamma \vdash A \cong A' \qquad \Gamma, x : A \vdash B \cong B'}{\Gamma \vdash \Sigma x : A.B \cong \Sigma x : A'.B'} $$

$$ \text{TREE TYC} \quad \frac{\Gamma \vdash A \cong A' \qquad \Gamma, x : A \vdash B \cong B'}{\Gamma \vdash \mathbf{W} x : A.B \cong \mathbf{W} x : A'.B'} $$

$$ \text{IDTYC} \quad \frac{\Gamma \vdash A \cong A' \qquad \Gamma \vdash t \cong t' : A}{\Gamma \vdash u \cong u' : A \quad t u \cong \mathbf{Id}_{A'} t' u'} $$

$$ \text{SUM TYC} \quad \frac{\Gamma \vdash A \cong A' \qquad \Gamma \vdash B \cong B'}{\Gamma \vdash A + B \cong A' + B'} $$

$\Gamma \vdash t \cong t' : T$

Terms *t* and *t'* are convertible at type *T* in context $\Gamma$

$$ \text{REFL} \quad \frac{\Gamma \vdash t : A}{\Gamma \vdash t \cong t : A} $$

$$ \text{TRANS} \quad \frac{\Gamma \vdash t \cong u : A \qquad \Gamma \vdash u \cong v : A}{\Gamma \vdash t \cong v : A} $$

$$ \text{CONV} \quad \frac{\Gamma \vdash t \cong t' : A}{\Gamma \vdash A \cong B} \quad \frac{\Gamma \vdash t \cong t' : B}{\Gamma \vdash f \cong g : \Pi x : A.B} $$

$$ \text{\betaFUN} \quad \frac{\Gamma \vdash A \qquad \Gamma, x : A \vdash B}{\Gamma \vdash (\lambda x : A.t) u \cong t[u] : B[u]} $$

$$ \text{\etaFUN} \quad \frac{\Gamma, x : A \vdash f x \cong g x : B}{\Gamma \vdash f \cong g : \Pi x : A.B} $$

$$ \text{\betaSIG1} \quad \frac{\Gamma \vdash A \qquad \Gamma, x : A \vdash B}{\Gamma \vdash t : A \qquad \Gamma \vdash u : B[t]} \qquad \Gamma \vdash p : \Sigma x : A.B $$

$$ \text{\betaSIG2} \quad \frac{\Gamma \vdash A \qquad \Gamma, x : A \vdash B}{\Gamma \vdash t : A \qquad \Gamma \vdash u : B[t]} \qquad \Gamma \vdash \pi_2(t, u)_{x.B} \cong u : B[t] $$

$$ \text{\etaSIG} \quad \frac{\Gamma \vdash A \qquad \Gamma, x : A \vdash B}{\Gamma \vdash p \cong (\pi_1 p, \pi_2 p)_{x.B} : \Sigma x : A.B} $$

$$ \text{\betaNIL} \quad \frac{\Gamma \vdash b_{\varepsilon} : P[\varepsilon_A] \qquad \Gamma, x : A, y : \mathbf{List} A, z : P[y] \vdash b_{\varepsilon} : P[x \::_{A} y]}{\Gamma \vdash \mathbf{ind}_{\mathbf{List} A}(\varepsilon_A; z.P; b_{\varepsilon}, x.y.z.b_{\varepsilon}) \cong b_{\varepsilon} : P[\varepsilon_A]} $$

$$ \text{\betaCONS} \quad \frac{\Gamma \vdash A \qquad \Gamma \vdash a : A \qquad \Gamma \vdash l : \mathbf{List} A}{\Gamma \vdash \mathbf{ind}_{\mathbf{List} A}(a \::_{A} l; z.P; b_{\varepsilon}, x.y.z.b_{\varepsilon}) \cong b_{\varepsilon}[a, l, \mathbf{ind}_{\mathbf{List} A}(l; z.P; b_{\varepsilon}, x.y.z.b_{\varepsilon})] : P[a \::_{A} l]}{\Gamma \vdash b_{\varepsilon} : P[\varepsilon_A]} $$

$$ \text{\betaTRUE} \quad \frac{\Gamma \vdash b_{tt} : P[tt] \qquad \Gamma \vdash b_{ff} : P[ff]}{\Gamma \vdash \mathbf{ind}_{\mathbf{B}}(tt; z.P; b_{tt}, b_{ff}) \cong b_{tt} : P[tt]} $$

$$ \text{\betaFALSE} \quad \frac{\Gamma \vdash b_{tt} : P[tt] \qquad \Gamma \vdash b_{ff} : P[ff]}{\Gamma \vdash \mathbf{ind}_{\mathbf{B}}(ff; z.P; b_{tt}, b_{ff}) \cong b_{ff} : P[ff]} $$
$\Gamma \vdash T \cong T'$

Types *T* and *T'* are convertible in context $\Gamma$

$$ \text{REFLTY} \quad \frac{\Gamma \vdash A}{\Gamma \vdash A \cong A} $$

$$ \text{TRANS TY} \quad \frac{\Gamma \vdash A \cong B \qquad \Gamma \vdash B \cong C}{\Gamma \vdash A \cong C} $$

$$ \text{ELC} \quad \frac{\Gamma \vdash A \cong A' : \text{Type}_i}{\Gamma \vdash A \cong A'} $$

$$ \text{FUNTYC} \quad \frac{\Gamma \vdash A \cong A' \qquad \Gamma, x : A \vdash B \cong B'}{\Gamma \vdash \Pi x : A.B \cong \Pi x : A'.B'} $$

$$ \text{LISTTYC} \quad \frac{\Gamma \vdash A \cong A'}{\Gamma \vdash \mathbf{List} A \cong \mathbf{List} A'} $$

$$ \text{SIGTYC} \quad \frac{\Gamma \vdash A \cong A' \qquad \Gamma, x : A \vdash B \cong B'}{\Gamma \vdash \Sigma x : A.B \cong \Sigma x : A'.B'} $$

$$ \text{TREE TYC} \quad \frac{\Gamma \vdash A \cong A' \qquad \Gamma, x : A \vdash B \cong B'}{\Gamma \vdash \mathbf{W} x : A.B \cong \mathbf{W} x : A'.B'} $$

$$ \text{IdTYC} \quad \frac{\Gamma \vdash A \cong A' \qquad \Gamma \vdash t \cong t' : A}{\Gamma \vdash u \cong u' : A \quad t u \cong \mathbf{Id}_{A'} t' u'} $$

$$ \text{SUMTYC} \quad \frac{\Gamma \vdash A \cong A' \qquad \Gamma \vdash B \cong B'}{\Gamma \vdash A + B \cong A' + B'} $$

$\Gamma \vdash t \cong t' : T$

Terms *t* and *t'* are convertible at type *T* in context $\Gamma$

$$ \text{REFL} \quad \frac{\Gamma \vdash t : A}{\Gamma \vdash t \cong t : A} $$

$$ \text{TRANS} \quad \frac{\Gamma \vdash t \cong u : A \qquad \Gamma \vdash u \cong v : A}{\Gamma \vdash t \cong v : A} $$

$$ \text{CONV} \quad \frac{\Gamma \vdash t \cong t' : A}{\Gamma \vdash A \cong B} \quad \frac{\Gamma \vdash t \cong t' : B}{\Gamma \vdash f \cong g : \Pi x : A.B} $$

$$ \text{\betaFUN} \quad \frac{\Gamma \vdash A \qquad \Gamma, x : A \vdash B}{\Gamma \vdash (\lambda x : A.t) u \cong t[u] : B[u]} $$

$$ \text{\etaFUN} \quad \frac{\Gamma, x : A \vdash f x \cong g x : B}{\Gamma \vdash f \cong g : \Pi x : A.B} $$

$$ \text{\betaSIG1} \quad \frac{\Gamma \vdash A \qquad \Gamma, x : A \vdash B}{\Gamma \vdash t : A \qquad \Gamma \vdash u : B[t]} \qquad \Gamma \vdash p : \Sigma x : A.B $$

$$ \text{\betaSIG2} \quad \frac{\Gamma \vdash A \qquad \Gamma, x : A \vdash B}{\Gamma \vdash t : A \qquad \Gamma \vdash u : B[t]} \qquad \Gamma \vdash \pi_2(t, u)_{x.B} \cong u : B[t] $$

$$ \text{\etaSIG} \quad \frac{\Gamma \vdash A \qquad \Gamma, x : A \vdash B}{\Gamma \vdash p \cong (\pi_1 p, \pi_2 p)_{x.B} : \Sigma x : A.B} $$

$$ \text{\betaNIL} \quad \frac{\Gamma \vdash b_{\varepsilon} : P[\varepsilon_A] \qquad \Gamma, x : A, y : \mathbf{List} A, z : P[y] \vdash b_{\varepsilon} : P[x \::_{A} y]}{\Gamma \vdash \mathbf{ind}_{\mathbf{List} A}(\varepsilon_A; z.P; b_{\varepsilon}, x.y.z.b_{\varepsilon}) \cong b_{\varepsilon} : P[\varepsilon_A]} $$

$$ \text{\betaCONS} \quad \frac{\Gamma \vdash A \qquad \Gamma \vdash a : A \qquad \Gamma \vdash l : \mathbf{List} A}{\Gamma \vdash \mathbf{ind}_{\mathbf{List} A}(a \::_{A} l; z.P; b_{\varepsilon}, x.y.z.b_{\varepsilon}) \cong b_{\varepsilon}[a, l, \mathbf{ind}_{\mathbf{List} A}(l; z.P; b_{\varepsilon}, x.y.z.b_{\varepsilon})] : P[a \::_{A} l]}{\Gamma \vdash b_{\varepsilon} : P[\varepsilon_A]} $$

$$ \text{\betaTRUE} \quad \frac{\Gamma \vdash b_{\text{tt}} : P[\text{tt}] \qquad \Gamma \vdash b_{\text{ff}} : P[\text{ff}]}{\Gamma \vdash \mathbf{ind}_{\mathbf{B}}(\text{tt}; z.P; b_{\text{tt}}, b_{\text{ff}}) \cong b_{\text{tt}} : P[\text{tt}]} $$

$$ \text{\betaFALSE} \quad \frac{\Gamma \vdash b_{\text{tt}} : P[\text{tt}] \qquad \Gamma \vdash b_{\text{ff}} : P[\text{ff}]}{\Gamma \vdash \mathbf{ind}_{\mathbf{B}}(\text{ff}; z.P; b_{\text{tt}}, b_{\text{ff}}) \cong b_{\text{ff}} : P[\text{ff}]} $$
$$ \beta\text{INJLEFT} \frac{\Gamma \vdash A+B \qquad \Gamma \vdash a:A \qquad \Gamma, z:A+B \vdash P}{\Gamma, x:A \vdash b_l:P[\text{inj}_B^l x] \qquad \Gamma, x:B \vdash b_r:P[\text{inj}_A^r x]} \qquad \frac{\Gamma \vdash \text{ind}_+(\text{inj}_B^l a; z.P; x.b_l, x.b_r) \cong b_l[a]:P[\text{inj}_B^l a]}{\Gamma \vdash \text{ind}_+(\text{inj}_A^l b; z.P; x.b_l, x.b_r) \cong b_r[b]:P[\text{inj}_A^r b]} $$

$$ \beta\text{INJRIHT} \frac{\Gamma \vdash A+B \qquad \Gamma \vdash b:B \qquad \Gamma, z:A+B \vdash P}{\Gamma, x:A \vdash b_l:P[\text{inj}_B^l x] \qquad \Gamma, x:B \vdash b_r:P[\text{inj}_A^r x]} \qquad \frac{\Gamma \vdash \text{ind}_+(\text{inj}_A^l b; z.P; x.b_l, x.b_r) \cong b_r[b]:P[\text{inj}_A^r b]}{\Gamma \vdash \text{ind}_+(\text{inj}_A^l b; z.P; x.b_l, x.b_r) \cong b_r[b]:P[\text{inj}_A^r b]} $$

$$ \beta\text{TREE} \frac{\Gamma, x:A \vdash B \qquad \Gamma \vdash a:A \qquad \Gamma \vdash k:B[a] \to \mathbf{W}x:A.B \qquad \Gamma, z:\mathbf{W}x:A.B \vdash P}{\Gamma, x:A, y:B[x] \to Wx:A.B, h:\Pi z:B[x].P[yz] \vdash b:P[\sup_{x.B} x y]} \qquad \frac{\Gamma \vdash \text{ind}_{\mathbf{W}x:A.B}(\sup_{x.B} a k; z.P; x.y.z.b) \cong b[a, k, (\lambda z:B[x].\text{ind}_{\mathbf{W}x:A.B}(kz; z.P; x.y.z.b))]:P[\sup_{x.B} a k]}{\Gamma \vdash \text{ind}_{\mathbf{W}x:A.B}(\sup_{x.B} a k; z.P; x.y.z.b) \cong b[a, k, (\lambda z:B[x].\text{ind}_{\mathbf{W}x:A.B}(kz; z.P; x.y.z.b))]:P[\sup_{x.B} a k]} $$

$$ \beta\text{REFL} \frac{\Gamma \vdash a:A \qquad \Gamma, x:A, y:A, z:\mathbf{I}d_A xy \vdash P \qquad \Gamma, x:A \vdash b:P[x, x, \text{refl}_{A,x}]}{\Gamma \vdash \text{ind}_{\mathbf{I}d_A}(\text{refl}_{A,a}; x.y.z.P; x.b) \cong b[a]:P[a, a, \text{refl}_{A,a}]} $$

$$ \text{FUNCONG} \frac{\Gamma \vdash A \cong A' : \text{Type}_i \qquad \Gamma, x:A \vdash B \cong B' : \text{Type}_i}{\Gamma \vdash \Pi x : A.B \cong \Pi x : A'.B' : \text{Type}_i} \qquad \text{other congruences omitted} $$

## C.2 Algorithmic MLTT

$t \rightsquigarrow^1 t'$ Term $t$ weak-head reduces in one step to term $t'$

$$ \beta\text{FUN} \frac{(\lambda x : A.t) u \rightsquigarrow^1 t[u]}{\beta\text{SIG}_1 \frac{\pi_1(t, u)_{x.B} \rightsquigarrow^1 t}{\beta\text{SIG}_2 \frac{\pi_2(t, u)_{x.B} \rightsquigarrow^1 u}{\beta\text{REDNIL}}}} $$

$$ \beta\text{REDNIL} \frac{\text{ind}_{\text{List A}}(\varepsilon_A; x.P; b_\varepsilon, x.y.z.b_\varepsilon) \rightsquigarrow^1 b_\varepsilon}{\beta\text{REDCONS} \frac{\text{ind}_{\text{List A}}(a \circled{=} l; x.P; b_\varepsilon, x.y.z.b_\varepsilon) \rightsquigarrow^1 b_\varepsilon[a, l, \text{ind}_{\text{List A}}(l; x.P; b_\varepsilon, x.y.z.b_\varepsilon)]}{\beta\text{REDCONS}}} $$

$$ \beta\text{TREE} \frac{\text{ind}_{\mathbf{W}x:A.B}(\sup_{x.B} a k; z.P; x.y.z.b) \rightsquigarrow^1 b[a, k, (\lambda z:B[x].\text{ind}_{\mathbf{W}x:A.B}(kz; z.P; x.y.z.b))]}{\beta\text{TRUE} \frac{\text{ind}_{\mathbf{B}}(tt; z.P; b_{tt}, b_{ff}) \rightsquigarrow^1 b_{tt}}{\beta\text{FALSE} \frac{\text{ind}_{\mathbf{B}}(ff; z.P; b_{tt}, b_{ff}) \rightsquigarrow^1 b_{ff}}{\beta\text{REDNIL}}}} $$

$$ \beta\text{TRUE} \frac{\text{ind}_{\mathbf{B}}(tt; z.P; b_{tt}, b_{ff}) \rightsquigarrow^1 b_{tt}}{\beta\text{FALSE} \frac{\text{ind}_{\mathbf{B}}(ff; z.P; b_{tt}, b_{ff}) \rightsquigarrow^1 b_{ff}}{\beta\text{REDNIL}}} $$

$$ \beta\text{INJLEFT} \frac{\text{ind}_+(\text{inj}_A^l a; z.P; x.b_l, x.b_r) \rightsquigarrow^1 b_l[a]}{\beta\text{INJRIGHT} \frac{\text{ind}_+(\text{inj}_A^r b; z.P; x.b_l, x.b_r) \rightsquigarrow^1 b_r[b]}{\beta\text{REFL} \frac{\text{ind}_{\mathbf{I}d_A}(\text{refl}_{A,a}; x.z.P; x.b) \rightsquigarrow^1 b[a]}{\beta\text{INJRIGHT} \frac{\text{ind}_+(\text{inj}_A^l b; z.P; x.b_l, x.b_r) \rightsquigarrow^1 b_l[a]}{\beta\text{TRUE} \frac{\text{ind}_{\mathbf{B}}(tt; z.P; b_{tt}, b_{ff}) \rightsquigarrow^1 b_{tt}}{\beta\text{FALSE} \frac{\text{ind}_{\mathbf{B}}(ff; z.P; b_{tt}, b_{ff}) \rightsquigarrow^1 b_{ff}}{\beta\text{REDNIL}}}}} $$

$$ \beta\text{INJRIGHT} \frac{\text{ind}_+(\text{inj}_A^r b; z.P; x.b_l, x.b_r) \rightsquigarrow^1 b_r[b]}{\beta\text{REFL} \frac{\text{ind}_{\mathbf{I}d_A}(\text{refl}_{A,a}; x.z.P; x.b) \rightsquigarrow^1 b[a]}{\beta\text{INJLEFT} \frac{\text{ind}_+(\text{inj}_A^l a; z.P; x.b_l, x.b_r) \rightsquigarrow^1 b_l[a]}{\beta\text{TRUE} \frac{\text{ind}_{\mathbf{B}}(tt; z.P; b_{tt}, b_{ff}) \rightsquigarrow^1 b_{tt}}{\beta\text{FALSE} \frac{\text{ind}_{\mathbf{B}}(ff; z.P; b_{tt}, b_{ff}) \rightsquigarrow^1 b_{ff}}{\beta\text{REDNIL}}}}} $$

$$ \text{REDAPP} \frac{t \rightsquigarrow^1 t'}{t u \rightsquigarrow^1 t' u} \qquad \text{REDSIG}_1 \frac{t \rightsquigarrow^1 t'}{\pi_1 t \rightsquigarrow^1 \pi_1 t'} \qquad \text{REDSIG}_2 \frac{t \rightsquigarrow^1 t'}{\pi_2 t \rightsquigarrow^1 \pi_2 t'} $$
$$ \text{REDIND} \frac{t \rightsquigarrow^1 t'}{\text{ind}_T(t; P; \vec{b}) \rightsquigarrow^1 \text{ind}_T(t'; P; \vec{b})} $$

### Term $t \rightsquigarrow^* t'$

$$ \text{REDBASE} \xrightarrow{t \rightsquigarrow^* t} \text{REDSTEP} \frac{t \rightsquigarrow^1 t' \quad t' \rightsquigarrow^* t''}{t \rightsquigarrow^* t''} $$

### $nf f$ def
$$ \begin{array}{l} n \mid \text{Type}_i \mid \Pi x : t.t \mid \lambda x : t.t \mid \text{List} t \mid \varepsilon_t \mid t \dot{=} t.t \quad \text{weak-head normal forms} \\ \Sigma x : t.t \mid (t,t) \mid \mathbf{W} x : t.t \mid \text{sup}_t t.t \mid \mathbf{0} \mid \mathbf{1} \mid () \mid \\ \mathbf{B} \mid tt \mid ff \mid \text{Id}_t t.t' \mid \text{refl}_{t,t} \mid t+t \mid \text{inj}_t^l t \mid \text{inj}_t^r t \end{array} $$

### $ne n$ def
$$ x \mid nt \mid \text{ind}_T(n;t;t) \mid \pi_1 n \mid \pi_2 n \quad \text{weak-head neutrals} $$

### $\Gamma \vdash T \triangleleft$ T is a type in $\Gamma$

$$ \text{FUNTy} \frac{\Gamma \vdash A \triangleleft \quad \Gamma, x : A \vdash B \triangleleft}{\Gamma \vdash \Pi x : A.B \triangleleft} \qquad \text{LISTTy} \frac{\Gamma \vdash A \triangleleft}{\Gamma \vdash \text{List } A \triangleleft} $$

$$ \text{SIGTy} \frac{\Gamma \vdash A \triangleleft \quad \Gamma, x : A \vdash B \triangleleft}{\Gamma \vdash \Sigma x : A.B \triangleleft} \qquad \text{TREETy} \frac{\Gamma \vdash A \triangleleft \quad \Gamma, x : A \vdash B \triangleleft}{\Gamma \vdash \mathbf{W} x : A.B \triangleleft} $$

$$ \text{EMPTYTy} \xrightarrow{\Gamma \vdash \mathbf{0} \triangleleft} \text{UNITTy} \xrightarrow{\Gamma \vdash \mathbf{1} \triangleleft} \text{BOOLTy} \xrightarrow{\Gamma \vdash \mathbf{B} \triangleleft} $$

$$ \text{IdTy} \frac{\Gamma \vdash A \triangleleft \quad \Gamma \vdash a \triangleleft A \quad \Gamma \vdash a' \triangleleft A}{\Gamma \vdash \mathbf{Id}_A a a' \triangleleft} $$

$$ \text{SUMTy} \frac{\Gamma \vdash A \triangleleft \quad \Gamma \vdash B \triangleleft}{\Gamma \vdash A+B \triangleleft} \qquad \text{EL} \frac{\Gamma \vdash A \triangleright_h \text{Type}_i \quad A \text{ is not a canonical form}}{\Gamma \vdash A \triangleleft} $$

### $\Gamma \vdash t \triangleright T$ Term $t$ infers type $T$ in context $\Gamma$

$$ \text{SORT} \xrightarrow{\Gamma \vdash \text{Type}_i \triangleright \text{Type}_{i+1}} \text{VAR} \frac{(x:T) \in \Gamma}{\Gamma \vdash x \triangleright T} \qquad \text{FUN} \frac{\Gamma \vdash A \triangleright_h \text{Type}_i \quad \Gamma, x : A \vdash B \triangleleft \text{Type}_i}{\Gamma \vdash \Pi x : A.B \triangleright \text{Type}_i} $$

$$ \text{ABS} \frac{\Gamma \vdash A \triangleleft \quad \Gamma, x : A \vdash t \triangleright B}{\Gamma \vdash \lambda x : A.t \triangleright \Pi x : A.B} \qquad \text{APP} \frac{\Gamma \vdash t \triangleright_h \Pi x : A.B \quad \Gamma \vdash u \triangleleft A}{\Gamma \vdash t u \triangleright B[u]} $$

$$ \text{LIST} \frac{\Gamma \vdash A \triangleright_h \text{Type}_i}{\Gamma \vdash \text{List } A \triangleright \text{Type}_i} \qquad \text{NIL} \frac{\Gamma \vdash A \triangleleft}{\Gamma \vdash \varepsilon_A \triangleright \text{List } A} \qquad \text{CONS} \frac{\Gamma \vdash a \triangleleft A \quad \Gamma \vdash l \triangleleft \text{List } A}{\Gamma \vdash a \dot{=} A_l \triangleright \text{List } A} $$
$$ \text{REDIND} \frac{t \rightsquigarrow^1 t'}{\text{ind}_T(t; P; \vec{b}) \rightsquigarrow^1 \text{ind}_T(t'; P; \vec{b})} $$

### Term $t \rightsquigarrow^* t'$

$$ \text{REDBASE} \xrightarrow{t \rightsquigarrow^* t} \text{REDSTEP} \frac{t \rightsquigarrow^1 t' \quad t' \rightsquigarrow^* t''}{t \rightsquigarrow^* t''} $$

### $nf f$ def
$$ \begin{array}{l} n \mid \text{Type}_i \mid \Pi x : t.t \mid \lambda x : t.t \mid \text{List} t \mid \varepsilon_t \mid t \dot{=} t.t \quad \text{weak-head normal forms} \\ \Sigma x : t.t \mid (t,t) \mid \mathbf{W} x : t.t \mid \text{sup}_t t.t \mid \mathbf{0} \mid \mathbf{1} \mid () \mid \\ \mathbf{B} \mid tt \mid ff \mid \text{Id}_t t.t' \mid \text{refl}_{t,t} \mid t+t \mid \text{inj}_t^l t \mid \text{inj}_t^r t \end{array} $$

### $ne n$ def
$$ x \mid nt \mid \text{ind}_T(n;t;t) \mid \pi_1 n \mid \pi_2 n \quad \text{weak-head neutrals} $$

### $\Gamma \vdash T \triangleleft$ T is a type in $\Gamma$

$$ \text{FUNTy} \frac{\Gamma \vdash A \triangleleft \quad \Gamma, x : A \vdash B \triangleleft}{\Gamma \vdash \Pi x : A.B \triangleleft} \qquad \text{LISTTy} \frac{\Gamma \vdash A \triangleleft}{\Gamma \vdash \text{List } A \triangleleft} $$

$$ \text{SIGTy} \frac{\Gamma \vdash A \triangleleft \quad \Gamma, x : A \vdash B \triangleleft}{\Gamma \vdash \Sigma x : A.B \triangleleft} \qquad \text{TREETy} \frac{\Gamma \vdash A \triangleleft \quad \Gamma, x : A \vdash B \triangleleft}{\Gamma \vdash \mathbf{W} x : A.B \triangleleft} $$

$$ \text{EMPTYTy} \xrightarrow{\Gamma \vdash \mathbf{0} \triangleleft} \text{UNITTy} \xrightarrow{\Gamma \vdash \mathbf{1} \triangleleft} \text{BOOLTy} \xrightarrow{\Gamma \vdash \mathbf{B} \triangleleft} $$

$$ \text{IdTy} \frac{\Gamma \vdash A \triangleleft \quad \Gamma \vdash a \triangleleft A \quad \Gamma \vdash a' \triangleleft A}{\Gamma \vdash \mathbf{Id}_A a a' \triangleleft} $$

$$ \text{SUMTy} \frac{\Gamma \vdash A \triangleleft \quad \Gamma \vdash B \triangleleft}{\Gamma \vdash A + B \triangleleft} \qquad \text{EL} \frac{\Gamma \vdash A \triangleright_h \text{Type}_i \quad A \text{ is not a canonical form}}{\Gamma \vdash A \triangleleft} $$

### $\Gamma \vdash t \triangleright T$ Term $t$ infers type $T$ in context $\Gamma$

$$ \text{SORT} \xrightarrow{\Gamma \vdash \text{Type}_i \triangleright \text{Type}_{i+1}} \text{VAR} \frac{(x : T) \in \Gamma}{\Gamma \vdash x \triangleright T} \qquad \text{FUN} \frac{\Gamma \vdash A \triangleright_h \text{Type}_i \quad \Gamma, x : A \vdash B \triangleleft \text{Type}_i}{\Gamma \vdash \Pi x : A.B \triangleright \text{Type}_i} $$

$$ \text{ABS} \frac{\Gamma \vdash A \triangleleft \quad \Gamma, x : A \vdash t \triangleright B}{\Gamma \vdash \lambda x : A.t \triangleright \Pi x : A.B} \qquad \text{APP} \frac{\Gamma \vdash t \triangleright_h \Pi x : A.B \quad \Gamma \vdash u \triangleleft A}{\Gamma \vdash t u \triangleright B[u]} $$

$$ \text{LIST} \frac{\Gamma \vdash A \triangleright_h \text{Type}_i}{\Gamma \vdash \text{List } A \triangleright \text{Type}_i} \qquad \text{NIL} \frac{\Gamma \vdash A \triangleleft}{\Gamma \vdash \varepsilon_A \triangleright \text{List } A} \qquad \text{CONS} \frac{\Gamma \vdash a \triangleleft A \quad \Gamma \vdash l \triangleleft \text{List } A}{\Gamma \vdash a \dot{=} A \quad l \triangleright \text{List } A} $$
$$ \text{LISTIND} \frac{\Gamma \vdash A \triangleleft \Gamma \vdash s \triangleleft \text{List } A \quad \Gamma, x : \text{List } A \vdash P \triangleleft \Gamma \vdash b_{\varepsilon} \triangleleft P[\varepsilon_A] \quad \Gamma, x : A, y : \text{List } A, z : P[y] \vdash b_{\varepsilon} \triangleleft P[x ::_A y] \quad \Gamma \vdash \text{ind}_{\text{List } A}(s; x.P; b_{\varepsilon}, x.y.z.b_{\varepsilon}) \triangleright P[s]}{\Gamma \vdash \text{ind}_{\text{List } A}(s; P) \triangleright P} $$

$$ \text{EMPTY} \xrightarrow{\Gamma \vdash \mathbf{0} \triangleright \text{Type}_0} \text{EMPTYIND} \xrightarrow{\Gamma \vdash s \triangleleft \mathbf{0} \quad \Gamma \vdash P \triangleleft \Gamma \vdash \text{ind}_0(s; P) \triangleright P} \text{UNITUNI} \xrightarrow{\Gamma \vdash \mathbf{1} \triangleright \text{Type}_0} $$

$$ \text{UNITTM} \xrightarrow{\Gamma \vdash () \triangleright \mathbf{1}} \text{UNITIND} \xrightarrow{\Gamma \vdash s \triangleleft \mathbf{1} \quad \Gamma, z : \mathbf{1} \vdash P \triangleleft \Gamma \vdash b_0() \triangleleft P[]() \quad \Gamma \vdash \text{ind}_1(s; z.P; b_0()) \triangleright P[s]} $$

$$ \text{SIG} \xrightarrow{\Gamma \vdash A \triangleleft_h \text{Type}_i \quad \Gamma, x : A \vdash B \triangleleft \text{Type}_i} \text{PAIR} \xrightarrow{\Gamma \vdash t \triangleright A \quad \Gamma, x : A \vdash B \triangleleft \Gamma \vdash u \triangleleft B[t] \quad \Gamma \vdash (t, u)_{x.B} \triangleright \Sigma x : A.B} \xrightarrow{\Gamma \vdash \Sigma x : A.B \triangleright \text{Type}_i} $$

$$ \text{PROJ}_1 \xrightarrow{\Gamma \vdash p \triangleright_h \Sigma x : A.B \quad \Gamma \vdash \pi_1 p \triangleright A} \text{PROJ}_2 \xrightarrow{\Gamma \vdash p \triangleright \Sigma x : A.B \quad \Gamma \vdash \pi_2 p \triangleright B[\pi_1 p]} $$

$$ \text{TREE} \xrightarrow{\Gamma \vdash A \triangleright_h \text{Type}_i \quad \Gamma, x : A \vdash B \triangleleft \text{Type}_i} \xrightarrow{\Gamma \vdash \mathbf{W} x : A.B \triangleleft \text{Type}_i} $$

$$ \text{SUP} \xrightarrow{\Gamma \vdash a \triangleright A \quad \Gamma, x : A \vdash B \triangleleft \Gamma \vdash k \triangleleft B[a] \rightarrow \mathbf{W} x : A.B} \xrightarrow{\Gamma \vdash \sup_{x.B} ak \triangleright \mathbf{W} x : A.B} $$

$$ \text{TREEIND} \xrightarrow{\Gamma \vdash A \triangleleft \Gamma, x : A \vdash B \triangleleft \Gamma \vdash s \triangleleft \mathbf{W} x : A.B \quad \Gamma, z : \mathbf{W} x : A.B \vdash P \triangleleft \Gamma, x : A, y : B[x] \rightarrow \mathbf{W} x : A.B, h : \Pi z : B[x].P[yz] \vdash b \triangleleft P[\sup_{x.B} xy]} \xrightarrow{\Gamma \vdash \text{ind}_{\mathbf{W} x : A.B}(s; z.P; x.y.z.b) \triangleright P[s]} $$

$$ \text{BOOLUNI} \xrightarrow{\Gamma \vdash \mathbf{B} \triangleright \text{Type}_0} \text{TRUE} \xrightarrow{\Gamma \vdash tt \triangleright \mathbf{B}} \text{FALSE} \xrightarrow{\Gamma \vdash ff \triangleright \mathbf{B}} $$

$$ \text{BOOLIND} \xrightarrow{\Gamma \vdash s \triangleleft \mathbf{B} \quad \Gamma, z : \mathbf{B} \vdash P \triangleleft \Gamma \vdash b_{tt} \triangleleft P[tt] \quad \Gamma \vdash b_{ff} \triangleleft P[ff]} \xrightarrow{\Gamma \vdash \text{ind}_{\mathbf{B}}(s; z.P; b_{tt}, b_{ff}) \triangleright P[s]} $$

$$ \text{SUM} \xrightarrow{\Gamma \vdash A \triangleright_h \text{Type}_i \quad \Gamma \vdash B \triangleleft \text{Type}_i} \text{SUMINJLEFT} \xrightarrow{\Gamma \vdash B \triangleleft \Gamma \vdash a \triangleright A \quad \Gamma \vdash \text{inj}_B^l a \triangleright A + B} \text{SUMINJRIGHT} \xrightarrow{\Gamma \vdash a \triangleright B \triangleleft \Gamma \vdash b \triangleright B} $$

$$ \text{SUMINJRIGHT} \xrightarrow{\Gamma \vdash A \triangleleft \Gamma \vdash b \triangleright B} \xrightarrow{\Gamma \vdash \text{inj}_A^r b \triangleright A + B} $$

$$ \text{SUMIND} \xrightarrow{\Gamma \vdash A \triangleleft \Gamma \vdash B \triangleleft \Gamma \vdash s \triangleleft A + B \quad \Gamma, z : A + B \vdash P \triangleleft \Gamma, x : A \vdash b_l \triangleleft P[\text{inj}_B^l x] \quad \Gamma, x : B \vdash b_r \triangleleft P[\text{inj}_A^r x]} \xrightarrow{\Gamma \vdash \text{ind}_{A+B}(s; z.P; x.b_l, x.b_r) \triangleright P[s]} $$
$$ \text{LISTIND} \frac{\Gamma \vdash A \triangleleft \Gamma \vdash s \triangleleft \text{List A} \quad \Gamma, x : \text{List A} \vdash P \triangleleft \Gamma \vdash b_{\varepsilon} \triangleleft P[\varepsilon_A] \quad \Gamma, x : A, y : \text{List A}, z : P[y] \vdash b_{\varepsilon} \triangleleft P[x ::_A y] \quad \Gamma \vdash \text{ind}_{\text{List A}}(s; x.P; b_{\varepsilon}, x.y.z.b_{\varepsilon}) \triangleright P[s]}{\Gamma \vdash \text{ind}_{\text{List A}}(s; P) \triangleright P} $$

$$ \text{EMPTY} \xrightarrow{\Gamma \vdash \mathbf{0} \triangleright \text{Type}_0} \text{EMPTYIND} \xrightarrow{\Gamma \vdash s \triangleleft \mathbf{0} \quad \Gamma \vdash P \triangleleft \Gamma \vdash \text{ind}_0(s; P) \triangleright P} \text{UNITUNI} \xrightarrow{\Gamma \vdash \mathbf{1} \triangleright \text{Type}_0} $$

$$ \text{UNITTM} \xrightarrow{\Gamma \vdash () \triangleright \mathbf{1}} \text{UNITIND} \xrightarrow{\Gamma \vdash s \triangleleft \mathbf{1} \quad \Gamma, z : \mathbf{1} \vdash P \triangleleft \Gamma \vdash b_0 \triangleleft P[] \quad \Gamma \vdash \text{ind}_1(s; z.P; b_0) \triangleright P[s]} $$

$$ \text{SIG} \frac{\Gamma \vdash A \triangleleft_h \text{Type}_i \quad \Gamma, x : A \vdash B \triangleleft \text{Type}_i}{\Gamma \vdash \Sigma x : A.B \triangleleft \text{Type}_i} \qquad \text{PAIR} \xrightarrow{\Gamma \vdash t \triangleleft A \quad \Gamma, x : A \vdash B \triangleleft \Gamma \vdash u \triangleleft B[t]} \frac{\Gamma \vdash (t, u)_{x.B} \triangleleft \Sigma x : A.B}{\Gamma \vdash (t, u)_{x.B} \triangleleft \Sigma x : A.B} $$

$$ \text{PROJ}_1 \frac{\Gamma \vdash p \triangleleft_h \Sigma x : A.B}{\Gamma \vdash \pi_1 p \triangleleft A} \qquad \text{PROJ}_2 \frac{\Gamma \vdash p \triangleleft \Sigma x : A.B}{\Gamma \vdash \pi_2 p \triangleleft B[\pi_1 p]} $$

$$ \text{TREE} \xrightarrow{\Gamma \vdash A \triangleleft_h \text{Type}_i} \frac{\Gamma, x : A \vdash B \triangleleft \text{Type}_i}{\Gamma \vdash \mathbf{W} x : A.B \triangleleft \text{Type}_i} $$

$$ \text{SUP} \frac{\Gamma \vdash a \triangleleft A \quad \Gamma, x : A \vdash B \triangleleft \Gamma \vdash k \triangleleft B[a] \rightarrow \mathbf{W} x : A.B}{\Gamma \vdash \sup_{x.B} a k \triangleleft \mathbf{W} x : A.B} $$

$$ \text{TREEIND} \xrightarrow{\Gamma \vdash A \triangleleft \Gamma, x : A \vdash B \triangleleft \Gamma \vdash s \triangleleft \mathbf{W} x : A.B \quad \Gamma, z : \mathbf{W} x : A.B \vdash P \triangleleft \Gamma, x : A, y : B[x] \rightarrow \mathbf{W} x : A.B, h : \Pi z : B[x].P[yz] \vdash b \triangleleft P[\sup_{x.B} x y]} \frac{\Gamma \vdash \text{ind}_{\mathbf{W} x : A.B}(s; z.P; x.y.z.b) \triangleright P[s]}{\Gamma \vdash \text{ind}_{\mathbf{W} x : A.B}(s; z.P; x.y.z.b) \triangleright P[s]} $$

$$ \text{BOOLUNI} \xrightarrow{\Gamma \vdash \mathbf{B} \triangleright \text{Type}_0} \text{TRUE} \xrightarrow{\Gamma \vdash tt \triangleleft \mathbf{B}} \text{FALSE} \xrightarrow{\Gamma \vdash ff \triangleleft \mathbf{B}} $$

$$ \text{BOOLIND} \xrightarrow{\Gamma \vdash s \triangleleft \mathbf{B} \quad \Gamma, z : \mathbf{B} \vdash P \triangleleft \Gamma \vdash b_{tt} \triangleleft P[tt]} \frac{\Gamma \vdash b_{ff} \triangleleft P[ff]}{\Gamma \vdash \text{ind}_{\mathbf{B}}(s; z.P; b_{tt}, b_{ff}) \triangleright P[s]} $$

$$ \text{SUM} \frac{\Gamma \vdash A \triangleleft_h \text{Type}_i \quad \Gamma \vdash B \triangleleft \text{Type}_i}{\Gamma \vdash A + B \triangleleft \text{Type}_i} \qquad \text{SUMINJLEFT} \frac{\Gamma \vdash B \triangleleft \Gamma \vdash a \triangleleft A}{\Gamma \vdash \text{inj}_B^l a \triangleleft A + B} $$

$$ \text{SUMINJRIGHT} \frac{\Gamma \vdash A \triangleleft \Gamma \vdash b \triangleleft B}{\Gamma \vdash \text{inj}_A^r b \triangleleft A + B} $$

$$ \text{SUMIND} \xrightarrow{\Gamma \vdash A \triangleleft \Gamma \vdash B \triangleleft \Gamma \vdash s \triangleleft A + B \quad \Gamma, z : A + B \vdash P \triangleleft \Gamma, x : A \vdash b_l \triangleleft P[\text{inj}_B^l x] \quad \Gamma, x : B \vdash b_r \triangleleft P[\text{inj}_A^r x]} \frac{\Gamma \vdash \text{ind}_{A+B}(s; z.P; x.b_l, x.b_r) \triangleright P[s]}{\Gamma \vdash \text{ind}_{A+B}(s; z.P; x.b_l, x.b_r) \triangleright P[s]} $$
$$ \text{ID} \frac{\Gamma \vdash A \triangleright_h \text{Type}_i \quad \Gamma \vdash a \triangleleft A \quad \Gamma \vdash a' \triangleleft A}{\Gamma \vdash \mathbf{Id}_A a a' \triangleright \text{Type}_i} $$

$$ \text{REFLTM} \frac{\Gamma \vdash A \triangleleft \quad \Gamma \vdash a \triangleleft A}{\Gamma \vdash \text{refl}_{A,a} \triangleright \mathbf{Id}_A a a} $$

$$ \text{IDIND} \frac{\Gamma \vdash A \triangleleft \quad \Gamma \vdash s \triangleright_h \mathbf{Id}_{A'} a a' \quad \Gamma, x : A, y : A, z : \mathbf{Id}_A xy \vdash P \triangleleft \quad \Gamma, x : A \vdash b \triangleleft P[x, x, \text{refl}_{A,x}]}{\Gamma \vdash \text{ind}_{\mathbf{Id}_A}(s; x.y.z.P; x.b) \triangleright P[a, a', s]} $$

$\Gamma \vdash t \triangleleft T$ Term $t$ checks against type $T$

$$ \text{CHECK} \frac{\Gamma \vdash t \triangleright T' \quad \Gamma \vdash T' \cong T \triangleleft}{\Gamma \vdash t \triangleleft T} $$

$\Gamma \vdash t \triangleright_h T$ Term $t$ infers the reduced type $T$

$$ \text{INFRED} \frac{\Gamma \vdash t \triangleright T \quad \Gamma \vdash T \rightsquigarrow T'}{\Gamma \vdash t \triangleright_h T'} $$

$\Gamma \vdash T \cong T' \triangleleft$ Types $T$ and $T'$ are convertible

$$ \text{TYRED} \frac{T \rightsquigarrow U \quad T' \rightsquigarrow U' \quad \Gamma \vdash U \cong_h U' \triangleleft}{\Gamma \vdash T \cong T' \triangleleft} $$

$\Gamma \vdash t \cong t' \triangleleft A$ Terms $t$ and $t'$ are convertible at type $T$

$$ \text{TMRED} \frac{t \rightsquigarrow u \quad t' \rightsquigarrow u' \quad T \rightsquigarrow U \quad \Gamma \vdash u \cong_h u' \triangleleft U}{\Gamma \vdash t \cong t' \triangleleft T} $$

$\Gamma \vdash T \cong_h T' \triangleleft$ Reduced types $T$ and $T'$ are convertible

$$ \text{CUUNITY} \frac{\Gamma \vdash \text{Type}_i \cong_h \text{Type}_i \triangleleft}{\Gamma \vdash \text{Type}_i} $$

$$ \text{CPRODTY} \frac{\Gamma \vdash A \cong A' \triangleleft \quad \Gamma, x : A' \vdash B \cong B' \triangleleft}{\Gamma \vdash \Pi x : A.B \cong_h \Pi x : A'.B' \triangleleft} $$

$$ \text{CLISTTY} \frac{\Gamma \vdash A \cong A' \triangleleft}{\Gamma \vdash \mathbf{List} A \cong_h \mathbf{List} A' \triangleleft} $$

$$ \text{CSIGTY} \frac{\Gamma \vdash A \cong A' \triangleleft \quad \Gamma, x : A \vdash B \cong B' \triangleleft}{\Gamma \vdash \Sigma x : A.B \cong_h \Sigma x : A'.B' \triangleleft} $$

$$ \text{CTREETY} \frac{\Gamma \vdash A \cong A' \triangleleft \quad \Gamma, x : A \vdash B \cong B' \triangleleft}{\Gamma \vdash \mathbf{W} x : A.B \cong_h \mathbf{W} x : A'.B' \triangleleft} $$

$$ \text{CIDTY} \frac{\Gamma \vdash A \cong A' \triangleleft \quad \Gamma \vdash t \cong t' \triangleleft A \quad \Gamma \vdash u \cong u' \triangleleft A}{\Gamma \vdash \mathbf{Id}_A t u \cong_h \mathbf{Id}_{A'} t' u' \triangleleft} $$

$$ \text{CSUMTY} \frac{\Gamma \vdash A \cong A' \triangleleft \quad \Gamma \vdash B \cong B' \triangleleft}{\Gamma \vdash A + B \cong A' + B' \triangleleft} $$

$$ \text{CREFLTY} \frac{T \text{ is } \mathbf{0}, \mathbf{1} \text{ or } \mathbf{B}}{\Gamma \vdash T \cong_h T \triangleleft} $$
$$ \text{ID} \frac{\Gamma \vdash A \triangleright_h \text{Type}_i \quad \Gamma \vdash a \triangleleft A \quad \Gamma \vdash a' \triangleleft A}{\Gamma \vdash \mathbf{Id}_A a a' \triangleright \text{Type}_i} $$

$$ \text{REFLTM} \frac{\Gamma \vdash A \triangleleft \quad \Gamma \vdash a \triangleleft A}{\Gamma \vdash \text{refl}_{A,a} \triangleright \mathbf{Id}_A a a} $$

$$ \text{IDIND} \frac{\Gamma \vdash A \triangleleft \quad \Gamma \vdash s \triangleright_h \mathbf{Id}_{A'} a a' \quad \Gamma, x : A, y : A, z : \mathbf{Id}_A xy \vdash P \triangleleft \quad \Gamma, x : A \vdash b \triangleleft P[x, x, \text{refl}_{A,x}]}{\Gamma \vdash \text{ind}_{\mathbf{Id}_A}(s; x.y.z.P; x.b) \triangleright P[a, a', s]} $$

$\Gamma \vdash t \triangleleft T$ Term $t$ checks against type $T$

$$ \text{CHECK} \frac{\Gamma \vdash t \triangleright T' \quad \Gamma \vdash T' \cong T \triangleleft}{\Gamma \vdash t \triangleleft T} $$

$\Gamma \vdash t \triangleright_h T$ Term $t$ infers the reduced type $T$

$$ \text{INFRED} \frac{\Gamma \vdash t \triangleright T \quad \Gamma \vdash T \rightsquigarrow T'}{\Gamma \vdash t \triangleright_h T'} $$

$\Gamma \vdash T \cong T' \triangleleft$ Types $T$ and $T'$ are convertible

$$ \text{TYRED} \frac{T \rightsquigarrow U \quad T' \rightsquigarrow U' \quad \Gamma \vdash U \cong_h U' \triangleleft}{\Gamma \vdash T \cong T' \triangleleft} $$

$\Gamma \vdash t \cong t' \triangleleft A$ Terms $t$ and $t'$ are convertible at type $T$

$$ \text{TMRED} \frac{t \rightsquigarrow u \quad t' \rightsquigarrow u' \quad T \rightsquigarrow U \quad \Gamma \vdash u \cong_h u' \triangleleft U}{\Gamma \vdash t \cong t' \triangleleft T} $$

$\Gamma \vdash T \cong_h T' \triangleleft$ Reduced types $T$ and $T'$ are convertible

$$ \text{CUUNITY} \frac{\Gamma \vdash \text{Type}_i \cong_h \text{Type}_i \triangleleft}{\Gamma \vdash \text{Type}_i \cong_h \text{Type}_i \triangleleft} $$

$$ \text{CPRODTY} \frac{\Gamma \vdash A \cong A' \triangleleft \quad \Gamma, x : A' \vdash B \cong B' \triangleleft}{\Gamma \vdash \Pi x : A.B \cong_h \Pi x : A'.B' \triangleleft} $$

$$ \text{CLISTTY} \frac{\Gamma \vdash A \cong A' \triangleleft}{\Gamma \vdash \mathbf{List} A \cong_h \mathbf{List} A' \triangleleft} $$

$$ \text{CSIGTY} \frac{\Gamma \vdash A \cong A' \triangleleft \quad \Gamma, x : A \vdash B \cong B' \triangleleft}{\Gamma \vdash \Sigma x : A.B \cong_h \Sigma x : A'.B' \triangleleft} $$

$$ \text{CTREETY} \frac{\Gamma \vdash A \cong A' \triangleleft \quad \Gamma, x : A \vdash B \cong B' \triangleleft}{\Gamma \vdash \mathbf{W} x : A.B \cong_h \mathbf{W} x : A'.B' \triangleleft} $$

$$ \text{CIDTY} \frac{\Gamma \vdash A \cong A' \triangleleft \quad \Gamma \vdash t \cong t' \triangleleft A \quad \Gamma \vdash u \cong u' \triangleleft A}{\Gamma \vdash \mathbf{Id}_A t u \cong_h \mathbf{Id}_{A'} t' u' \triangleleft} $$

$$ \text{CSUMTY} \frac{\Gamma \vdash A \cong A' \triangleleft \quad \Gamma \vdash B \cong B' \triangleleft}{\Gamma \vdash A + B \cong A' + B' \triangleleft} $$

$$ \text{CREFLTY} \frac{T \text{ is } \mathbf{0}, \mathbf{1} \text{ or } \mathbf{B}}{\Gamma \vdash T \cong_h T \triangleleft} $$
$$ \text{NEUTY} \frac{\Gamma \vdash n \approx n' \triangleright T}{\Gamma \vdash n \cong_h n' \triangleleft} $$

$$ \Gamma \vdash t \cong_h t' \triangleleft A $$

Reduced terms $t$ and $t'$ are convertible at type $A$

$$ \text{CUNI} \frac{\Gamma \vdash \text{Type}_i \cong_h \text{Type}_j \triangleleft \text{Type}_k}{\Gamma \vdash \text{Type}_i} $$

$$ \text{CFUN} \frac{\Gamma \vdash A \cong A' \triangleleft \text{Type}_i}{\Gamma, x : A' \vdash B \cong B' \triangleleft \text{Type}_i} \qquad \text{CFUNETA} \frac{\Gamma \vdash \Pi x : A.B \cong_h \Pi x : A'.B' \triangleleft \text{Type}_i}{\Gamma \vdash f \cong_h f' \triangleleft \Pi x : A.B} $$

$$ \text{CFUNETA} \frac{\Gamma, x : A \vdash f x \cong f' x \triangleleft B}{\Gamma \vdash f \cong_h f' \triangleleft \Pi x : A.B} $$

$$ \text{CSIG} \frac{\Gamma \vdash A \cong A' \triangleleft \text{Type}_i}{\Gamma \vdash \Sigma x : A.B \cong_h \Sigma x : A'.B' \triangleleft \text{Type}_i} $$

$$ \text{CSIGETA} \frac{\Gamma \vdash \pi_1 p \cong \pi_1 p' \triangleleft A}{\Gamma \vdash \pi_2 p \cong \pi_2 p' \triangleleft B[\pi_1 p]} \qquad \text{CLIST} \frac{\Gamma \vdash A \cong A' \triangleleft \text{Type}_i}{\Gamma \vdash \text{List A} \cong_h \text{List A'} \triangleleft \text{Type}_i} $$

$$ \text{CNIL} \frac{\Gamma \vdash \varepsilon_A \cong_h \varepsilon_{A'} \triangleleft \text{List A''}}{\Gamma \vdash \varepsilon_A \cong_h \varepsilon_{A'} \triangleleft \text{List A''}} $$

$$ \text{CCONS} \frac{\Gamma \vdash a \cong a' \triangleleft A'' \qquad \Gamma \vdash l \cong l' \triangleleft \text{List A''}}{\Gamma \vdash a \coloneqq_A l \cong_h a' \coloneqq_{A'} l' \triangleleft \text{List A''}} $$

$$ \text{CREFLUNI} \frac{T \text{ is } \mathbf{0}, \mathbf{1} \text{ or } \mathbf{B}}{\Gamma \vdash T \cong_h T \triangleleft \text{Type}_0} $$

$$ \text{CUNITK} \frac{\Gamma \vdash () \cong_h () \triangleleft \mathbf{1}}{\Gamma \vdash () \cong_h () \triangleleft \mathbf{1}} $$

$$ \text{CREFLBOOL} \frac{t \text{ is tt or ff}}{\Gamma \vdash t \cong_h t \triangleleft \mathbf{B}} $$

$$ \text{CTREE} \frac{\Gamma \vdash A \cong A' \triangleleft \text{Type}_i}{\Gamma, x : A' \vdash B \cong B' \triangleleft \text{Type}_i} \qquad \text{CTREE} \frac{\Gamma \vdash \mathbf{W} x : A.B \cong_h \mathbf{W} x : A'.B' \triangleleft \text{Type}_i}{\Gamma \vdash \mathbf{W} x : A.B \cong_h \mathbf{W} x : A'.B' \triangleleft \text{Type}_i} $$

$$ \text{CSUP} \frac{\Gamma \vdash a \cong a' \triangleleft A'' \qquad \Gamma \vdash k \cong k' \triangleleft B''[a] \to \mathbf{W} x : A''.B''}{\Gamma \vdash \sup_{x.B} a k \cong_h \sup_{x.B'} a' k' \triangleleft \mathbf{W} x : A''.B''} $$

$$ \text{CSUM} \frac{\Gamma \vdash A \cong A' \triangleleft \text{Type}_i \qquad \Gamma \vdash B \cong B' \triangleleft \text{Type}_i}{\Gamma \vdash A + B \cong A' + B' \triangleleft \text{Type}_i} $$

$$ \text{CINJLEFT} \frac{\Gamma \vdash B \cong B' \triangleleft \Gamma \vdash a \cong a' \triangleleft A}{\Gamma \vdash \text{inj}_B^l a \cong \text{inj}_{B'}^l a' \triangleleft A + B} $$

$$ \text{CINJRIGHT} \frac{\Gamma \vdash A \cong A' \triangleleft \Gamma \vdash b \cong b' \triangleleft B}{\Gamma \vdash \text{inj}_A^r b \cong \text{inj}_{A'}^r b' \triangleleft A + B} $$

$$ \text{REFLREFL} \frac{\Gamma \vdash \text{refl}_{A,a} \cong \text{refl}_{A',a'} \triangleleft \text{Id}_{A''} t u}{\Gamma \vdash \text{refl}_{A,a} \cong \text{refl}_{A',a'} \triangleleft \text{Id}_{A''} t u} $$

$$ \text{NEUNEU} \frac{\Gamma \vdash n \approx n' \triangleright S \qquad \text{ne} M}{\Gamma \vdash n \cong_h n' \triangleleft M} $$

$$ \text{NEUPOS} \frac{\Gamma \vdash n \approx n' \triangleright S \qquad \text{t is Type}_i, \mathbf{0}, \mathbf{1}, \mathbf{B}, \text{List A}, \mathbf{W} x : A.B \text{ or } \text{Id}_A a a'}{\Gamma \vdash n \cong_h n' \triangleleft T} $$
$$ \text{NEUTY} \frac{\Gamma \vdash n \approx n' \triangleright T}{\Gamma \vdash n \cong_h n' \triangleleft} $$

$$ \Gamma \vdash t \cong_h t' \triangleleft A $$

Reduced terms $t$ and $t'$ are convertible at type $A$

$$ \text{CUNI} \frac{\Gamma \vdash \text{Type}_i \cong_h \text{Type}_j \triangleleft \text{Type}_k}{\Gamma \vdash \text{Type}_i} $$

$$ \text{CFUN} \frac{\Gamma \vdash A \cong A' \triangleleft \text{Type}_i}{\Gamma, x : A' \vdash B \cong B' \triangleleft \text{Type}_i} \qquad \text{CFUNETA} \frac{\Gamma \vdash \Pi x : A.B \cong_h \Pi x : A'.B' \triangleleft \text{Type}_i}{\Gamma \vdash f \cong_h f' \triangleleft \Pi x : A.B} $$

$$ \text{CFUNETA} \frac{\Gamma, x : A \vdash f x \cong f' x \triangleleft B}{\Gamma \vdash f \cong_h f' \triangleleft \Pi x : A.B} $$

$$ \text{CSIG} \frac{\Gamma \vdash A \cong A' \triangleleft \text{Type}_i}{\Gamma \vdash \Sigma x : A.B \cong_h \Sigma x : A'.B' \triangleleft \text{Type}_i} $$

$$ \text{CSIGETA} \frac{\Gamma \vdash \pi_1 p \cong \pi_1 p' \triangleleft A}{\Gamma \vdash \pi_2 p \cong \pi_2 p' \triangleleft B[\pi_1 p]} \qquad \text{CLIST} \frac{\Gamma \vdash A \cong A' \triangleleft \text{Type}_i}{\Gamma \vdash \text{List A} \cong_h \text{List A'} \triangleleft \text{Type}_i} $$

$$ \text{CNIL} \frac{\Gamma \vdash \varepsilon_A \cong_h \varepsilon_{A'} \triangleleft \text{List A''}}{\Gamma \vdash \varepsilon_A \cong_h \varepsilon_{A'} \triangleleft \text{List A''}} $$

$$ \text{CCONS} \frac{\Gamma \vdash a \cong a' \triangleleft A'' \qquad \Gamma \vdash l \cong l' \triangleleft \text{List A''}}{\Gamma \vdash a \coloneqq_A l \cong_h a' \coloneqq_{A'} l' \triangleleft \text{List A''}} $$

$$ \text{CREFLUNI} \frac{T \text{ is } 0, 1 \text{ or } B}{\Gamma \vdash T \cong_h T \triangleleft \text{Type}_0} $$

$$ \text{CUNITK} \frac{\Gamma \vdash () \cong_h () \triangleleft \mathbf{1}}{\Gamma \vdash () \cong_h () \triangleleft \mathbf{1}} $$

$$ \text{CREFLBOOL} \frac{t \text{ is tt or ff}}{\Gamma \vdash t \cong_h t \triangleleft \mathbf{B}} $$

$$ \text{CTREE} \frac{\Gamma \vdash A \cong A' \triangleleft \text{Type}_i}{\Gamma, x : A' \vdash B \cong B' \triangleleft \text{Type}_i} \qquad \text{CTREE} \frac{\Gamma \vdash \mathbf{W} x : A.B \cong_h \mathbf{W} x : A'.B' \triangleleft \text{Type}_i}{\Gamma \vdash \mathbf{W} x : A.B \cong_h \mathbf{W} x : A'.B' \triangleleft \text{Type}_i} $$

$$ \text{CSUP} \frac{\Gamma \vdash a \cong a' \triangleleft A'' \qquad \Gamma \vdash k \cong k' \triangleleft B''[a] \to \mathbf{W} x : A''.B''}{\Gamma \vdash \sup_{x.B} a k \cong_h \sup_{x.B'} a' k' \triangleleft \mathbf{W} x : A''.B''} $$

$$ \text{CSUM} \frac{\Gamma \vdash A \cong A' \triangleleft \text{Type}_i \qquad \Gamma \vdash B \cong B' \triangleleft \text{Type}_i}{\Gamma \vdash A + B \cong A' + B' \triangleleft \text{Type}_i} $$

$$ \text{CINJLEFT} \frac{\Gamma \vdash B \cong B' \triangleleft \Gamma \vdash a \cong a' \triangleleft A}{\Gamma \vdash \text{inj}_B^l a \cong \text{inj}_{B'}^l a' \triangleleft A + B} $$

$$ \text{CINJRIGHT} \frac{\Gamma \vdash A \cong A' \triangleleft \Gamma \vdash b \cong b' \triangleleft B}{\Gamma \vdash \text{inj}_A^r b \cong \text{inj}_{A'}^r b' \triangleleft A + B} $$

$$ \text{REFLREFL} \frac{\Gamma \vdash \text{refl}_{A,a} \cong \text{refl}_{A',a'} \triangleleft \text{Id}_{A''} t u}{\Gamma \vdash \text{refl}_{A,a} \cong \text{refl}_{A',a'} \triangleleft \text{Id}_{A''} t u} $$

$$ \text{NEUNEU} \frac{\Gamma \vdash n \approx n' \triangleright S \qquad \text{ne} M}{\Gamma \vdash n \cong_h n' \triangleleft M} $$

$$ \text{NEUPOS} \frac{\Gamma \vdash n \approx n' \triangleright S \qquad T \text{ is Type}_i, 0, 1, B, \text{List A}, \mathbf{W} x : A.B \text{ or } \text{Id}_A a a'}{\Gamma \vdash n \cong_h n' \triangleleft T} $$
$\Gamma \vdash t \approx_h t' \triangleright T$ Neutrals $t$ and $t'$ are comparable, inferring the reduced type $T$

$$ \mathrm{NRED} \frac{\Gamma \vdash n \approx n' \triangleright T \quad T \leadsto^* S}{\Gamma \vdash n \approx_h n' \triangleright S} $$

$\Gamma \vdash t \approx t' \triangleright T$ Neutrals $t$ and $t'$ are comparable, inferring the type $T$

$$ \mathrm{NVAR} \frac{(x : T) \in \Gamma}{\Gamma \vdash x \approx x \triangleright T} \qquad \mathrm{NAPP} \frac{\Gamma \vdash n \approx_h n' \triangleright \Pi x : A.B \quad \Gamma \vdash u \cong u' \triangleleft A}{\Gamma \vdash n u \approx n' u' \triangleright B[u]} $$

$$ \mathrm{NLISTIND} \frac{\Gamma \vdash A \cong A' \triangleleft \Gamma \vdash s \approx s' \triangleright S \quad \Gamma, z : \mathbf{List} A \vdash P \cong P' \triangleleft \Gamma \vdash b_{\epsilon} \cong b'_{\epsilon} \triangleleft P[\epsilon_A] \quad \Gamma, x : A, y : \mathbf{List} A, z : P[y] \vdash b_{\epsilon} \cong b'_{\epsilon} \triangleleft P[x \sim_A y]}{\Gamma \vdash \mathrm{ind}_{\mathbf{List} A}(s; z.P; b_{\epsilon}, x.y.z.b_{\epsilon}) \approx \mathrm{ind}_{\mathbf{List} A'}(s'; z.P'; b'_{\epsilon}, x.y.z.b'_{\epsilon}) \triangleright P[s]} $$

$$ \mathrm{NEMPTYIND} \frac{\Gamma \vdash s \approx_h s' \triangleright \mathbf{0} \quad \Gamma \vdash P \cong P' \triangleleft \Gamma \vdash b \cong b' \triangleleft P(())}{\Gamma \vdash \mathrm{ind}_0(s; P) \approx \mathrm{ind}_0(s'; P') \triangleright P} $$

$$ \mathrm{NUNITIND} \frac{\Gamma \vdash s \approx_h s' \triangleright \mathbf{1} \quad \Gamma, z : \mathbf{1} \vdash P \cong P' \triangleleft \Gamma \vdash b \cong b' \triangleleft P(())}{\Gamma \vdash \mathrm{ind}_1(s; z.P; b) \approx \mathrm{ind}_0(s'; z.P'; b') \triangleright P[s]} $$

$$ \mathrm{NSIG1} \frac{\Gamma \vdash n \approx_h n' \triangleright \Sigma x : A.B}{\Gamma \vdash \pi_1 n \approx \pi_1 n' \triangleright A} \qquad \mathrm{NSIG2} \frac{\Gamma \vdash n \approx_h n' \triangleright \Sigma x : A.B}{\Gamma \vdash \pi_2 n \approx \pi_2 n' \triangleright B[\pi_1 n]} $$

$$ \Gamma \vdash A \cong A' \triangleleft \Gamma \vdash s \approx s' \triangleright S \quad \Gamma, z : \mathbf{W} x : A.B \vdash P \cong P' \triangleleft \Gamma \vdash x : A, y : B[x] \to W x : A.B, h : \Pi z : B[x].P[y z] \vdash b \cong b' \triangleleft P[\sup_{x.B} x y] \\ \mathrm{NTREEIND} \frac{\Gamma \vdash \mathrm{ind}_{\mathbf{W} x:A.B}(s; z.P; x.y.z.b) \approx \mathrm{ind}_{\mathbf{W} x:A.B'}(s'; z.P'; x.y.z.b') \triangleright P[s]}{\Gamma \vdash \mathrm{ind}_{\mathbf{W} x:A.B}(s; z.P; x.y.z.b) \approx \mathrm{ind}_{\mathbf{W} x:A.B'}(s'; z.P'; x.y.z.b') \triangleright P[s]} $$

$$ \mathrm{NBOOLIND} \frac{\Gamma, z : \mathbf{B} \vdash P \cong P' \triangleleft \Gamma \vdash b_{tt} \cong b'_{tt} \triangleleft P[tt] \quad \Gamma \vdash b_{ff} \cong b'_{ff} \triangleleft P[ff]}{\Gamma \vdash \mathrm{ind}_{\mathbf{B}}(s; z.P; b_{tt}, b_{ff}) \approx \mathrm{ind}_{\mathbf{B}}(s'; z.P'; b'_{tt}, b'_{ff}) \triangleright P[s]} $$

$$ \mathrm{NSUMIND} \frac{\Gamma \vdash A \cong A' \triangleleft \Gamma \vdash B \cong B' \triangleleft \Gamma \vdash s \approx_h s' \triangleright S \quad \Gamma, z : A+B \vdash P \cong P' \triangleleft \Gamma \vdash x : A, y : A, z : \mathbf{Id}_A x y \vdash P \cong P' \triangleleft \Gamma, x : A \vdash b \cong b' \triangleleft P[x, x, \mathrm{refl}_{A,x}]}{\Gamma \vdash \mathrm{ind}_{A+B}(s; z.P; x.b_l, x.b_r) \approx \mathrm{ind}_{A'+B'}(s'; z.P'; x.b'_l, x.b'_r) \triangleright P[s]} $$

$$ \mathrm{NIDIND} \frac{\Gamma \vdash A \cong A' \triangleleft \Gamma \vdash s \approx_h s' \triangleright \mathbf{Id}_{A''} a a'}{\Gamma, x : A, y : A, z : \mathbf{Id}_A x y \vdash P \cong P' \triangleleft \Gamma, x : A \vdash b \cong b' \triangleleft P[x, x, \mathrm{refl}_{A,x}]} \quad \Gamma \vdash \mathrm{ind}_{\mathbf{Id}_A}(s; x.y.z.P; x.b) \approx \mathrm{ind}_{\mathbf{Id}_{A'}}(s'; x.y.z.P'; x.b') \triangleright P[a, a', s] $$
$\Gamma \vdash t \approx_h t' \triangleright T$ Neutrals $t$ and $t'$ are comparable, inferring the reduced type $T$

$$ \mathrm{NRED} \frac{\Gamma \vdash n \approx n' \triangleright T \quad T \leadsto^* S}{\Gamma \vdash n \approx_h n' \triangleright S} $$

$\Gamma \vdash t \approx t' \triangleright T$ Neutrals $t$ and $t'$ are comparable, inferring the type $T$

$$ \mathrm{NVAR} \frac{(x : T) \in \Gamma}{\Gamma \vdash x \approx x \triangleright T} $$

$$ \mathrm{NAPP} \frac{\Gamma \vdash n \approx_h n' \triangleright \Pi x : A.B \quad \Gamma \vdash u \cong u' \triangleleft A}{\Gamma \vdash n u \approx n' u' \triangleright B[u]} $$

$$ \mathrm{NLISTIND} \frac{\Gamma \vdash A \cong A' \triangleleft \Gamma \vdash s \approx s' \triangleright S \quad \Gamma, z : \mathbf{List} A \vdash P \cong P' \triangleleft \Gamma \vdash b_{\epsilon} \cong b'_{\epsilon} \triangleleft P[\epsilon_A] \quad \Gamma, x : A, y : \mathbf{List} A, z : P[y] \vdash b_{\epsilon} \cong b'_{\epsilon} \triangleleft P[x \sim_A y]}{\Gamma \vdash \mathrm{ind}_{\mathbf{List} A}(s; z.P; b_{\epsilon}, x.y.z.b_{\epsilon}) \approx \mathrm{ind}_{\mathbf{List} A'}(s'; z.P'; b'_{\epsilon}, x.y.z.b'_{\epsilon}) \triangleright P[s]} $$

$$ \mathrm{NEMPTYIND} \frac{\Gamma \vdash s \approx_h s' \triangleright \mathbf{0} \quad \Gamma \vdash P \cong P' \triangleleft \Gamma \vdash b \cong b' \triangleleft P(())}{\Gamma \vdash \mathrm{ind}_0(s; P) \approx \mathrm{ind}_0(s'; P') \triangleright P} $$

$$ \mathrm{NUNITIND} \frac{\Gamma \vdash s \approx_h s' \triangleright \mathbf{1} \quad \Gamma, z : \mathbf{1} \vdash P \cong P' \triangleleft \Gamma \vdash b \cong b' \triangleleft P(())}{\Gamma \vdash \mathrm{ind}_1(s; z.P; b) \approx \mathrm{ind}_0(s'; z.P'; b') \triangleright P[s]} $$

$$ \mathrm{NSIG1} \frac{\Gamma \vdash n \approx_h n' \triangleright \Sigma x : A.B}{\Gamma \vdash \pi_1 n \approx \pi_1 n' \triangleright A} $$

$$ \mathrm{NSIG2} \frac{\Gamma \vdash n \approx_h n' \triangleright \Sigma x : A.B}{\Gamma \vdash \pi_2 n \approx \pi_2 n' \triangleright B[\pi_1 n]} $$

$$ \Gamma \vdash A \cong A' \triangleleft \Gamma \vdash s \approx s' \triangleright S \quad \Gamma, z : \mathbf{W} x : A.B \vdash P \cong P' \triangleleft \Gamma \vdash x : A, y : B[x] \to W x : A.B, h : \Pi z : B[x].P[y z] \vdash b \cong b' \triangleleft P[\sup_{x.B} x y] \\ \mathrm{NTREEIND} \frac{\Gamma \vdash \mathrm{ind}_{\mathbf{W} x:A.B}(s; z.P; x.y.z.b) \approx \mathrm{ind}_{\mathbf{W} x:A.B'}(s'; z.P'; x.y.z.b') \triangleright P[s]}{\Gamma \vdash \mathrm{ind}_{\mathbf{W} x:A.B}(s; z.P; x.y.z.b) \approx \mathrm{ind}_{\mathbf{W} x:A.B'}(s'; z.P'; x.y.z.b') \triangleright P[s]} $$

$$ \mathrm{NBOOLIND} \frac{\Gamma, z : \mathbf{B} \vdash P \cong P' \triangleleft \Gamma \vdash b_{tt} \cong b'_{tt} \triangleleft P[tt] \quad \Gamma \vdash b_{ff} \cong b'_{ff} \triangleleft P[ff]}{\Gamma \vdash \mathrm{ind}_{\mathbf{B}}(s; z.P; b_{tt}, b_{ff}) \approx \mathrm{ind}_{\mathbf{B}}(s'; z.P'; b'_{tt}, b'_{ff}) \triangleright P[s]} $$

$$ \mathrm{NSUMIND} \frac{\Gamma \vdash A \cong A' \triangleleft \Gamma \vdash B \cong B' \triangleleft \Gamma \vdash s \approx_h s' \triangleright S \quad \Gamma, z : A+B \vdash P \cong P' \triangleleft \Gamma \vdash x : A, y : A, z : \mathbf{Id}_A x y \vdash P \cong P' \triangleleft \Gamma, x : A \vdash b \cong b' \triangleleft P[x, x, \mathrm{refl}_{A,x}]}{\Gamma \vdash \mathrm{ind}_{A+B}(s; z.P; x.b_l, x.b_r) \approx \mathrm{ind}_{A'+B'}(s'; z.P'; x.b'_l, x.b'_r) \triangleright P[s]} $$

$$ \mathrm{NIDIND} \frac{\Gamma \vdash A \cong A' \triangleleft \Gamma \vdash s \approx_h s' \triangleright \mathbf{Id}_{A''} a a'}{\Gamma, x : A, y : A, z : \mathbf{Id}_A x y \vdash P \cong P' \triangleleft \Gamma, x : A \vdash b \cong b' \triangleleft P[x, x, \mathrm{refl}_{A,x}]} \quad \Gamma \vdash \mathrm{ind}_{\mathbf{Id}_A}(s; x.y.z.P; x.b) \approx \mathrm{ind}_{\mathbf{Id}_{A'}}(s'; x.y.z.P'; x.b') \triangleright P[a, a', s] $$
### C.3 Declarative MLTT<sub>map</sub>

Extend the rules of Appendix C.1. In rule MAPCOMP, we rely on conversion at domain and morphism types for a type former F. These are obtained from the judgements of Fig. 7 by replacing every typing judgement by a conversion judgement, and forgetting conversions. For instance, for Π types, we have

$$ 
\begin{align*}
\Delta \vdash_{\text{map}} (A, B) &\cong (A', B') : \text{dom}(\Pi) & \iff & \Delta \vdash_{\text{map}} A &\cong A' \wedge \Delta, x : A \vdash_{\text{map}} B &\cong B' \\
\Delta \vdash_{\text{map}} (f, g) &\cong (f', g') : \text{hom}_{\Pi}((A_1, B_1), (A_2, B_2)) & \iff & \Delta \vdash_{\text{map}} f &\cong f' : A_2 \to A_1 \wedge \\
& & & \Delta, x : A_2 \vdash_{\text{map}} g &\cong g' : B_1[fx] \to B_2
\end{align*}
$$

For each type former F (Π, Σ, List, W, Id, +)

$$ 
\begin{array}{c} 
\text{MAP} \\ 
\Gamma \vdash_{\text{map}} X, Y : \text{dom}(F) \\ 
\Gamma \vdash_{\text{map}} f : \text{hom}_F(X, Y) \\ 
\Gamma \vdash_{\text{map}} \text{map}_F f : FX \to FY 
\end{array} 
\qquad 
\begin{array}{c} 
\text{MAPID} \\ 
\Gamma \vdash_{\text{map}} X : \text{dom}(F) \\ 
\Gamma \vdash_{\text{map}} t : FX \\ 
\Gamma \vdash_{\text{map}} \text{map}_F \text{id}_X^F t \cong t : FX 
\end{array}
$$

$$ 
\begin{array}{c} 
\text{MAPCOMP} \\ 
\Gamma \vdash_{\text{map}} X, Y, Z : \text{dom}(F) \\ 
\Gamma \vdash_{\text{map}} g : \text{hom}_F(X, Y) \\ 
\Gamma \vdash_{\text{map}} f : \text{hom}_F(Y, Z) \\ 
\Gamma \vdash_{\text{map}} t : FX \\ 
\Gamma \vdash_{\text{map}} \text{map}_F f (\text{map}_F gt) \cong \text{map}_F (f \circ g) t : FZ 
\end{array} 
$$

$$ 
\begin{array}{c} 
\Gamma \vdash_{\text{map}} X \cong X' : \text{dom}(F) \\ 
\Gamma \vdash_{\text{map}} Y \cong Y' : \text{dom}(F) \\ 
\Gamma \vdash_{\text{map}} f : \text{hom}_F(X, Y) \\ 
\Gamma \vdash_{\text{map}} f' : \text{hom}_F(X', Y') \\ 
\Gamma \vdash_{\text{map}} f \cong f' : \text{hom}_F(X, Y) \\ 
\Gamma \vdash_{\text{map}} \text{map}_F f \cong \text{map}_F f' : FX \to FY 
\end{array} 
$$

$$ \Gamma \vdash_{\text{map}} t \cong u : A $$

$$ 
\begin{array}{c} 
\text{MAPFUN} \\ 
\Gamma \vdash_{\text{map}} (f, g) : \text{hom}_{\Pi}((A, B), (A', B')) \\ 
\Gamma \vdash_{\text{map}} h : \Pi x : A.B \\ 
\Gamma \vdash_{\text{map}} a' : A' \\ 
\Gamma \vdash_{\text{map}} \text{map}_{\Pi} (f, g) ha' \cong g (ha') : B'[a'] 
\end{array} 
$$

$$ 
\begin{array}{c} 
\text{MAPSIG1} \\ 
\Gamma \vdash_{\text{map}} (f, g) : \text{hom}_{\Sigma}((A, B), (A', B')) \\ 
\Gamma \vdash_{\text{map}} p : \Sigma x : A.B \\ 
\Gamma \vdash_{\text{map}} \pi_1 (\text{map}_{\Sigma} (f, g) p) \cong f (\pi_1 p) : A' 
\end{array} 
$$

$$ 
\begin{array}{c} 
\text{MAPSIG2} \\ 
\Gamma \vdash_{\text{map}} (f, g) : \text{hom}_{\Sigma}((A, B), (A', B')) \\ 
\Gamma \vdash_{\text{map}} p : \Sigma x : A.B \\ 
\Gamma \vdash_{\text{map}} \pi_2 (\text{map}_{\Sigma} (f, g) p) \cong g (\pi_2 p) : B'[f(\pi_1 p)] 
\end{array} 
$$

$$ 
\begin{array}{c} 
\text{MAPLISTNIL} \\ 
\Gamma \vdash_{\text{map}} f : \text{hom}_{\text{List}}(A, A') \\ 
\Gamma \vdash_{\text{map}} \text{map}_{\text{List}} f \varepsilon_A \cong \varepsilon_{A'} : \text{List A'} 
\end{array} 
$$

$$ 
\begin{array}{c} 
\text{MAPLISTCONS} \\ 
\Gamma \vdash_{\text{map}} f : \text{hom}_{\text{List}}(A, A') \\ 
\Gamma \vdash_{\text{map}} hd : A \\ 
\Gamma \vdash_{\text{map}} tl : \text{List A} \\ 
\Gamma \vdash_{\text{map}} \text{map}_{\text{List}} f (hd ::_A tl) \cong (fh ::_{A'} (\text{map}_{\text{List}} f tl)) : \text{List A'} 
\end{array} 
$$

$$ 
\begin{array}{c} 
\text{MAPW} \\ 
\Gamma \vdash_{\text{map}} (f, g) : \text{hom}_{\mathbf{W}}((A, B), (A', B')) \\ 
\Gamma \vdash_{\text{map}} a : A \\ 
\Gamma \vdash_{\text{map}} k : Ba \to \mathbf{W}x : A.B \\ 
\Gamma \vdash_{\text{map}} \text{map}_{\mathbf{W}}(f, g) (\sup_{x.B} ak) \cong \sup_{x.B'} (fa) (\lambda x : B'[fa]. \text{map}_{\mathbf{W}}(f, g) (k(gx))) : \mathbf{W}x : A'.B' 
\end{array} 
$$
$$ \mathbf{MAPID} \quad \frac{\Gamma \vdash_{\text{map}} f : \text{hom}_{\mathbf{Id}}(A, A') \quad \Gamma \vdash_{\text{map}} a : A}{\Gamma \vdash_{\text{map}} \mathbf{map}_{\mathbf{Id}} f \ \text{refl}_{A,a} \cong \text{refl}_{A',fa} : \mathbf{Id} A' (fa) (fa)} $$

$$ \mathbf{MAPSUMLEFT} \quad \frac{\Gamma \vdash_{\text{map}} (f,g) : \text{hom}_+((A,B), (A', B')) \quad \Gamma \vdash_{\text{map}} a : A}{\Gamma \vdash_{\text{map}} \mathbf{map}_+ (f,g) (\text{inj}^l a) \cong \text{inj}^l (fa) : A' + B'} $$

$$ \mathbf{MAPSUMRIGHT} \quad \frac{\Gamma \vdash_{\text{map}} (f,g) : \text{hom}_+((A,B), (A', B')) \quad \Gamma \vdash_{\text{map}} b : B}{\Gamma \vdash_{\text{map}} \mathbf{map}_+ (f,g) (\text{inj}^r b) \cong \text{inj}^r (gb) : A' + B'} $$

### C.4 Algorithmic MLTT<sub>map</sub>

Extends Appendix C.2. Replaces the rules already named with the same name in Appendix C.2.

$$ \Gamma \vdash_{\text{map}} t \cong_h t' \triangleleft T $$

$$ \text{NEUPOSMAP} \quad \frac{\Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft T \quad T \text{ is Type}_i, \text{List } A, \mathbf{W} x : A.B, A+B \text{ or } \mathbf{Id}_A a a'}{\Gamma \vdash_{\text{map}} n \cong_h n' \triangleleft T} $$

$$ \Gamma \vdash_{\text{map}} n \approx n' \triangleright T $$

$$ \text{NLISTIND} \quad \frac{\Gamma \vdash_{\text{map}} A \cong A' \triangleleft \quad \Gamma \vdash_{\text{map}} s \approx_{\text{map}} s' \triangleleft \text{List } A \quad \Gamma, z : \text{List } A \vdash_{\text{map}} P \cong P' \triangleleft \quad \Gamma \vdash_{\text{map}} b_{\varepsilon} \cong b'_{\varepsilon} \triangleleft P[\varepsilon_A] \quad \Gamma, x : A, y : \text{List } A, z : P[y] \vdash_{\text{map}} b_{\varepsilon} \cong b'_{\varepsilon} \triangleleft P[x \ddots_A y]}{\Gamma \vdash_{\text{map}} \text{ind}_{\text{List } A}(s; z.P; b_{\varepsilon}, x.y.z.b_{\varepsilon}) \approx \text{ind}_{\text{List } A'}(s'; z.P'; b'_{\varepsilon}, x.y.z.b'_{\varepsilon}) \triangleright P[s]} $$

$$ \Gamma \vdash_{\text{map}} A \cong A' \triangleleft \quad \Gamma, x : A \vdash_{\text{map}} B \cong B' \triangleleft \quad \Gamma \vdash_{\text{map}} s \approx_{\text{map}} s' \triangleleft \mathbf{W} x : A.B \quad \Gamma, z : \mathbf{W} x : A.B \vdash_{\text{map}} P \cong P' \triangleleft $$

$$ \text{NTREEIND} \quad \frac{\Gamma, x : A, y : B[x] \to Wx : A.B, h : \Pi z : B[x].P[yz] \vdash_{\text{map}} b \cong b' \triangleleft P[\sup_{x.B} xy]}{\Gamma \vdash_{\text{map}} \text{ind}_{W x:A.B}(s; z.P; x.y.z.b) \approx \text{ind}_{W x:A'.B'}(s'; z.P'; x.y.z.b') \triangleright P[s]} $$

$$ \Gamma \vdash_{\text{map}} A \cong A' \triangleleft \quad \Gamma \vdash_{\text{map}} s \approx_{\text{map}} s' \triangleleft A+B \quad \Gamma, z : A+B \vdash_{\text{map}} P \cong P' \triangleleft \quad \Gamma \vdash_{\text{map}} B \cong B' \triangleleft \quad \Gamma \vdash_{\text{map}} s \approx_{\text{map}} s' \triangleleft A+B $$

$$ \text{NSUMIND} \quad \frac{\Gamma, x : A \vdash_{\text{map}} b_l \cong b'_l \triangleleft P[\text{inj}^l x] \quad \Gamma, x : B \vdash_{\text{map}} b_r \cong b'_r \triangleleft P[\text{inj}^r x]}{\Gamma \vdash_{\text{map}} \text{ind}_{A+B}(s; z.P; x.b_l, x.b_r) \approx \text{ind}_{A'+B'}(s'; z.P'; x.b'_l, x.b'_r) \triangleright P[s]} $$

$$ \Gamma \vdash_{\text{map}} A \cong A' \triangleleft \quad \Gamma \vdash_{\text{map}} s \approx_{\text{map}} s' \triangleleft \mathbf{Id}_A \triangleright a, a' \quad \Gamma, x, y : A, z : \mathbf{Id}_A xy \vdash_{\text{map}} P \cong P' \triangleleft \quad \Gamma, x : A \vdash_{\text{map}} b \cong b' \triangleleft P[x, x, \text{refl}_{A,x}] $$

$$ \text{NIDIND} \quad \frac{\Gamma \vdash_{\text{map}} \text{ind}_{\mathbf{Id}_A}(s; x.z.P; b) \approx \text{ind}_{\mathbf{Id}_A'}(s'; x.z.P'; b') \triangleright P[a, a', s]}{\Gamma \vdash_{\text{map}} \text{ind}_{\mathbf{Id}_A}(s; x.z.P; b) \approx \text{ind}_{\mathbf{Id}_A'}(s'; x.z.P'; b') \triangleright P[a, a', s]} $$

unmap, unmapfun, unmapfun<sub>1</sub>, unmapfun<sub>2</sub>

$$ \begin{array}{l@{\quad}l@{\quad}l@{\quad}l@{\quad}l} \text{unmap}(\mathbf{map}_F ft) & \stackrel{\text{def}}{=} & t & \text{unmap}(t) & \stackrel{\text{def}}{=} & t \quad \text{otherwise} \\ \text{unmapfun}(\mathbf{map}_F ft, x) & \stackrel{\text{def}}{=} & fx & \text{unmapfun}(t, x) & \stackrel{\text{def}}{=} & x \quad \text{otherwise} \\ \text{unmapfun}_1(\mathbf{map}_F ft, x) & \stackrel{\text{def}}{=} & \pi_1 fx & \text{unmapfun}_1(t, x) & \stackrel{\text{def}}{=} & x \quad \text{otherwise} \\ \text{unmapfun}_2(\mathbf{map}_F ft, y) & \stackrel{\text{def}}{=} & \pi_2 fy & \text{unmapfun}_2(t, y) & \stackrel{\text{def}}{=} & y \quad \text{otherwise} \end{array} $$
$$ \text{MAPID} \quad \frac{\Gamma \vdash_{\text{map}} f : \text{hom}_{\text{Id}}(A, A') \quad \Gamma \vdash_{\text{map}} a : A}{\Gamma \vdash_{\text{map}} \text{map}_{\text{Id}} f \ \text{refl}_{A,a} \cong \text{refl}_{A',fa} : \text{Id} A' (fa) (fa)} $$

$$ \text{MAPSUMLEFT} \quad \frac{\Gamma \vdash_{\text{map}} (f,g) : \text{hom}_+((A,B), (A', B')) \quad \Gamma \vdash_{\text{map}} a : A}{\Gamma \vdash_{\text{map}} \text{map}_+ (f,g) (\text{inj}^l a) \cong \text{inj}^l (fa) : A' + B'} $$

$$ \text{MAPSUMRIGHT} \quad \frac{\Gamma \vdash_{\text{map}} (f,g) : \text{hom}_+((A,B), (A', B')) \quad \Gamma \vdash_{\text{map}} b : B}{\Gamma \vdash_{\text{map}} \text{map}_+ (f,g) (\text{inj}^r b) \cong \text{inj}^r (gb) : A' + B'} $$

### C.4 Algorithmic MLTT<sub>map</sub>

Extends Appendix C.2. Replaces the rules already named with the same name in Appendix C.2.

$$ \Gamma \vdash_{\text{map}} t \cong_h t' \triangleleft T $$

$$ \text{NEUPOSMAP} \quad \frac{\Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft T \quad T \text{ is Type}_i, \text{List } A, \mathbf{W} x : A.B, A+B \text{ or } \text{Id}_A a a'}{\Gamma \vdash_{\text{map}} n \cong_h n' \triangleleft T} $$

$$ \Gamma \vdash_{\text{map}} n \approx n' \triangleright T $$

$$ \text{NLISTIND} \quad \frac{\Gamma \vdash_{\text{map}} A \cong A' \triangleleft \quad \Gamma \vdash_{\text{map}} s \approx_{\text{map}} s' \triangleleft \text{List } A \quad \Gamma, z : \text{List } A \vdash_{\text{map}} P \cong P' \triangleleft \quad \Gamma \vdash_{\text{map}} b_{\epsilon} \cong b'_{\epsilon} \triangleleft P[\epsilon_A] \quad \Gamma, x : A, y : \text{List } A, z : P[y] \vdash_{\text{map}} b_{\pi} \cong b'_{\pi} \triangleleft P[x \coloneqq_A y]}{\Gamma \vdash_{\text{map}} \text{ind}_{\text{List } A}(s; z.P; b_{\epsilon}, x.y.z.b_{\pi}) \approx \text{ind}_{\text{List } A'}(s'; z.P'; b'_{\epsilon}, x.y.z.b'_{\pi}) \triangleright P[s]} $$

$$ \Gamma \vdash_{\text{map}} A \cong A' \triangleleft \quad \Gamma, x : A \vdash_{\text{map}} B \cong B' \triangleleft \quad \Gamma \vdash_{\text{map}} s \approx_{\text{map}} s' \triangleleft \mathbf{W} x : A.B \quad \Gamma, z : \mathbf{W} x : A.B \vdash_{\text{map}} P \cong P' \triangleleft $$

$$ \text{NTREEIND} \quad \frac{\Gamma, x : A, y : B[x] \rightarrow Wx : A.B, h : \Pi z : B[x].P[yz] \vdash_{\text{map}} b \cong b' \triangleleft P[\sup_{x.B} xy]}{\Gamma \vdash_{\text{map}} \text{ind}_{W x:A.B}(s; z.P; x.y.z.b) \approx \text{ind}_{W x:A'.B'}(s'; z.P'; x.y.z.b') \triangleright P[s]} $$

$$ \text{NSUMIND} \quad \frac{\Gamma \vdash_{\text{map}} A \cong A' \triangleleft \quad \Gamma \vdash_{\text{map}} B \cong B' \triangleleft \quad \Gamma \vdash_{\text{map}} s \approx_{\text{map}} s' \triangleleft A+B \quad \Gamma, z : A+B \vdash_{\text{map}} P \cong P' \triangleleft \quad \Gamma, x : A \vdash_{\text{map}} b_l \cong b'_l \triangleleft P[\text{inj}^l x] \quad \Gamma, x : B \vdash_{\text{map}} b_r \cong b'_r \triangleleft P[\text{inj}^r x]}{\Gamma \vdash_{\text{map}} \text{ind}_{A+B}(s; z.P; x.b_l, x.b_r) \approx \text{ind}_{A'+B'}(s'; z.P'; x.b'_l, x.b'_r) \triangleright P[s]} $$

$$ \text{NIDIND} \quad \frac{\Gamma \vdash_{\text{map}} A \cong A' \triangleleft \quad \Gamma \vdash_{\text{map}} s \approx_{\text{map}} s' \triangleleft \text{Id}_A \triangleright a, a'}{\Gamma, x, y : A, z : \text{Id}_A xy \vdash_{\text{map}} P \cong P' \triangleleft \quad \Gamma, x : A \vdash_{\text{map}} b \cong b' \triangleleft P[x, x, \text{refl}_{A,x}]} \quad \Gamma \vdash_{\text{map}} \text{ind}_{\text{Id}_A}(s; x.z.P; b) \approx \text{ind}_{\text{Id}_A'}(s'; x.z.P'; b') \triangleright P[a, a', s] $$

unmap, unmapfun, unmapfun<sub>1</sub>, unmapfun<sub>2</sub>

$$ \begin{array}{l@{\qquad}l} \text{unmap}(\text{map}_F ft) & \text{unmap}(t) \quad \stackrel{\text{def}}{=} \quad t \quad \text{otherwise} \\ \text{unmapfun}(\text{map}_F ft, x) & \text{unmapfun}(t, x) \quad \stackrel{\text{def}}{=} \quad x \quad \text{otherwise} \\ \text{unmapfun}_1(\text{map}_F ft, x) & \text{unmapfun}_1(t, x) \quad \stackrel{\text{def}}{=} \quad x \quad \text{otherwise} \\ \text{unmapfun}_2(\text{map}_F ft, y) & \text{unmapfun}_2(t, y) \quad \stackrel{\text{def}}{=} \quad y \quad \text{otherwise} \end{array} $$
$$ \Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft T $$

$$ \begin{array}{c} \text{UNMAPLIST} \\ \Gamma, x : A \vdash_{\text{map}} \text{unmapfun}(n, x) \cong \text{unmapfun}(n', x) \triangleleft B \\ \Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft \text{List } B \end{array} $$

$$ \begin{array}{c} \text{UNMAPTREE} \\ \Gamma, x : A, y : B' [\text{unmapfun}_1(n, x)] \vdash_{\text{map}} \text{unmapfun}_2(n, y) \cong \text{unmapfun}_2(n', y) \triangleleft B x \\ \Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft \mathbf{W} x : A' \cdot B' \end{array} $$

$$ \begin{array}{c} \text{UNMAPSUM} \\ \Gamma \vdash_{\text{map}} \text{unmap}(n) \approx_{\text{h}} \text{unmap}(n') \triangleright A + B \\ \Gamma, x : A \vdash_{\text{map}} \text{unmapfun}_1(n, x) \cong \text{unmapfun}_1(n', x) \triangleleft A' \\ \Gamma, x : B \vdash_{\text{map}} \text{unmapfun}_2(n, x) \cong \text{unmapfun}_2(n', x) \triangleleft B' \\ \Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft A' + B' \end{array} $$

$$ \begin{array}{c} \text{UNMAPID} \\ \Gamma \vdash_{\text{map}} \text{unmap}(n) \approx_{\text{h}} \text{unmap}(n') \triangleright \mathbf{Id}_A a a' \\ \Gamma, x : A \vdash_{\text{map}} \text{unmapfun}(n, x) \cong \text{unmapfun}(n', x) \triangleleft A' \\ \Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft \mathbf{Id}_{A'} \triangleright \text{unmapfun}(n, a), \text{unmapfun}(n, a') \end{array} $$

$$ t \rightsquigarrow^1 t' $$

$$ \begin{array}{l@{\qquad}l} \pi_1 (\text{map}_{\Sigma} f p) \rightsquigarrow^1 \pi_1 f (\pi_1 p) & \pi_2 (\text{map}_{\Sigma} f p) \rightsquigarrow^1 \pi_2 f (\pi_2 p) \\ \text{map}_{\Pi} f h t \rightsquigarrow^1 (\pi_2 f) (h ((\pi_1 f) t)) & \text{map}_{\mathbf{Id}} f \text{refl}_{A,a} \rightsquigarrow^1 \text{refl}_{B,fa} \end{array} $$

$$ \text{map}_{\text{List}} f \varepsilon \rightsquigarrow^1 \varepsilon \qquad \text{map}_{\text{List}} f (hd :: tl) \rightsquigarrow^1 f hd :: \text{map}_{\text{List}} f tl $$

$$ \text{map}_{\mathbf{W}}\{T\}\{T'\} f (\sup a k) \rightsquigarrow^1 \sup_{x, \pi_2 T'} (\pi_1 f a) (\lambda x : (\pi_2 T' (\pi_1 f a)). \text{map}_{\mathbf{W}} f (k (\pi_2 g x))) $$

$$ \text{map}_{+} (f, g) (\text{inj}^l a) \rightsquigarrow^1 \text{inj}^l (f a) \qquad \text{map}_{+} (f, g) (\text{inj}^r b) \rightsquigarrow^1 \text{inj}^r (g b) $$

$$ \text{REDMAPCOMP} \frac{\text{ne } n \quad F \in \{\text{List}, \text{Id}, +, \mathbf{W}\}}{\text{map}_F f (\text{map}_F g n) \rightsquigarrow^1 \text{map}_F (f \circ g) n} $$

## C.5 Declarative record types

Extends Appendix C.1.

$$ \text{REC TY} \frac{\mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash A_l}{\Gamma \vdash \{l : A_l\}_{l \in \mathcal{L}}} $$

$$ \text{REC UNI} \frac{\mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash A_l : \text{Type}_i}{\Gamma \vdash \{l : A_l\}_{l \in \mathcal{L}} : \text{Type}_i} $$
$$ \Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft T $$

$$ \begin{array}{c} \text{UNMAPLIST} \\ \Gamma, x : A \vdash_{\text{map}} \text{unmapfun}(n, x) \cong \text{unmapfun}(n', x) \triangleleft B \\ \Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft \text{List } B \end{array} $$

$$ \begin{array}{c} \text{UNMAPTREE} \\ \Gamma, x : A, y : B' [\text{unmapfun}_1(n, x)] \vdash_{\text{map}} \text{unmapfun}_2(n, y) \cong \text{unmapfun}_2(n', y) \triangleleft B x \\ \Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft \mathbf{W} x : A' \cdot B' \end{array} $$

$$ \begin{array}{c} \text{UNMAPSUM} \\ \Gamma \vdash_{\text{map}} \text{unmap}(n) \approx_{\text{h}} \text{unmap}(n') \triangleright A + B \\ \Gamma, x : A \vdash_{\text{map}} \text{unmapfun}_1(n, x) \cong \text{unmapfun}_1(n', x) \triangleleft A' \\ \Gamma, x : B \vdash_{\text{map}} \text{unmapfun}_2(n, x) \cong \text{unmapfun}_2(n', x) \triangleleft B' \\ \Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft A' + B' \end{array} $$

$$ \begin{array}{c} \text{UNMAPID} \\ \Gamma \vdash_{\text{map}} \text{unmap}(n) \approx_{\text{h}} \text{unmap}(n') \triangleright \mathbf{Id}_A a a' \\ \Gamma, x : A \vdash_{\text{map}} \text{unmapfun}(n, x) \cong \text{unmapfun}(n', x) \triangleleft A' \\ \Gamma \vdash_{\text{map}} n \approx_{\text{map}} n' \triangleleft \mathbf{Id}_{A'} \triangleright \text{unmapfun}(n, a), \text{unmapfun}(n, a') \end{array} $$

$$ t \rightsquigarrow^1 t' $$

$$ \begin{array}{l@{\qquad}l} \pi_1 (\text{map}_{\Sigma} f p) \rightsquigarrow^1 \pi_1 f (\pi_1 p) & \pi_2 (\text{map}_{\Sigma} f p) \rightsquigarrow^1 \pi_2 f (\pi_2 p) \\ \text{map}_{\Pi} f h t \rightsquigarrow^1 (\pi_2 f) (h ((\pi_1 f) t)) & \text{map}_{\mathbf{Id}} f \text{refl}_{A,a} \rightsquigarrow^1 \text{refl}_{B,fa} \end{array} $$

$$ \text{map}_{\text{List}} f \varepsilon \rightsquigarrow^1 \varepsilon \qquad \text{map}_{\text{List}} f (hd :: tl) \rightsquigarrow^1 f hd :: \text{map}_{\text{List}} f tl $$

$$ \text{map}_{\mathbf{W}}\{T\}\{T'\} f (\sup a k) \rightsquigarrow^1 \sup_{x, \pi_2 T'} (\pi_1 f a) (\lambda x : (\pi_2 T' (\pi_1 f a)). \text{map}_{\mathbf{W}} f (k (\pi_2 g x))) $$

$$ \text{map}_{+} (f, g) (\text{inj}^l a) \rightsquigarrow^1 \text{inj}^l (f a) \qquad \text{map}_{+} (f, g) (\text{inj}^r b) \rightsquigarrow^1 \text{inj}^r (g b) $$

$$ \text{REDMAPCOMP} \frac{\text{ne } n \quad F \in \{\text{List}, \text{Id}, +, \mathbf{W}\}}{\text{map}_F f (\text{map}_F g n) \rightsquigarrow^1 \text{map}_F (f \circ g) n} $$

## C.5 Declarative record types

Extends Appendix C.1.

$$ \begin{array}{c} \text{REC}\text{TY} \\ \mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash A_l \\ \text{REC}\text{UNI} \\ \mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash A_l : \text{Type}_i \\ \Gamma \vdash \{l : A_l\}_{l \in \mathcal{L}} : \text{Type}_i \end{array} $$
$$ \text{REC}\text{TM} \quad \frac{\mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash u_l : A_l}{\Gamma \vdash \{l := u_l\}_{l \in \mathcal{L}} : \{l : A_l\}_{l \in \mathcal{L}}} $$

$$ \text{REC}\text{PROJ} \quad \frac{\Gamma \vdash r : \{l : A_l\}_{l \in \mathcal{L}}}{\Gamma \vdash r.l : A_l} $$

$$ \beta\text{REC} \quad \frac{\mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash u_l : A_l}{\Gamma \vdash \{l := u_l\}_{l \in \mathcal{L}}. l \cong u_l : A_l} $$

$$ \eta\text{REC} \quad \frac{\Gamma \vdash r : \{l : A_l\}_{l \in \mathcal{L}}}{\Gamma \vdash r \cong \{l := r.l\}_{l \in \mathcal{L}} : \{l : A_l\}_{l \in \mathcal{L}}} $$

## C.6 Algorithmic record types

Extends Appendix C.2. Record construction terms {$l := u_l$}$_{l \in \mathcal{L}}$ are normal forms, and $r.l$ is neutral whenever $r$ is.

$$ \beta\text{REC} \quad \frac{\{l := u_l\}_{l \in \mathcal{L}}. l \rightsquigarrow 1}{u_l} $$

$$ \text{REC}\text{UNI} \quad \frac{\mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash A_l \triangleright_h \text{Type}_i}{\Gamma \vdash \{l : A_l\}_{l \in \mathcal{L}}^i \triangleright \text{Type}_i} $$

$$ \text{REC}\text{TM} \quad \frac{\mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash u_l \triangleright A_l}{\Gamma \vdash \{l := u_l\}_{l \in \mathcal{L}} \triangleright \{l : A_l\}_{l \in \mathcal{L}}} $$

$$ \text{REC}\text{ETA} \quad \frac{\forall l \in \mathcal{L}. \quad \Gamma \vdash r.l \cong r'.l \triangleleft A_l}{\Gamma \vdash r \cong_h r' \triangleleft \{l : A_l\}_{l \in \mathcal{L}}} $$

$$ \text{NREC}\text{PROJ} \quad \frac{\Gamma \vdash n \approx_h n' \triangleright \{l : A_l\}_{l \in \mathcal{L}}}{\Gamma \vdash n.l \approx n'.l \triangleright A_l} $$

## C.7 Algorithmic MLTT<sub>sub</sub>

Extends Appendices C.2 and C.6, with rule `CHECKSUB` replacing `CHECK`.

$$ \Gamma \vdash_{\text{sub}} t \triangleleft T $$

$$ \text{CHECKSUB} \quad \frac{\Gamma \vdash_{\text{sub}} t \triangleright T' \quad \Gamma \vdash_{\text{sub}} T' \preceq T \triangleleft}{\Gamma \vdash_{\text{sub}} t \triangleleft T} $$

$$ \Gamma \vdash_{\text{sub}} T \preceq T' \triangleleft $$

Type $T$ is a subtype of type $T'$

$$ \text{TYRED} \quad \frac{T \rightsquigarrow U \quad T' \rightsquigarrow U'}{\Gamma \vdash_{\text{sub}} T \preceq T' \triangleleft} \quad \Gamma \vdash_{\text{sub}} U \preceq_h U' \triangleleft $$

$$ \Gamma \vdash_{\text{sub}} T \preceq_h T' \triangleleft $$

Reduced type $T$ is a subtype of reduced type $T'$

$$ \text{REC}\text{SUB} \quad \frac{\mathcal{K} \subseteq \mathcal{L} \quad \forall k \in \mathcal{K}. \quad \Gamma \vdash_{\text{sub}} A_k \preceq B_k \triangleleft}{\Gamma \vdash_{\text{sub}} \{l : A_l\}_{l \in \mathcal{L}} \preceq_h \{k : A_k\}_{k \in \mathcal{K}} \triangleleft} $$

$$ \text{PROD}\text{SUB} \quad \frac{\Gamma \vdash_{\text{sub}} A' \preceq A \triangleleft \quad \Gamma, x : A' \vdash_{\text{sub}} B \preceq B' \triangleleft}{\Gamma \vdash_{\text{sub}} \Pi x : A.B \preceq_h \Pi x : A'.B' \triangleleft} $$

$$ \text{LIST}\text{SUB} \quad \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft}{\Gamma \vdash_{\text{sub}} \text{List } A \preceq_h \text{List } A' \triangleleft} $$

$$ \text{SIG}\text{SUB} \quad \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \quad \Gamma, x : A \vdash_{\text{sub}} B \preceq B' \triangleleft}{\Gamma \vdash_{\text{sub}} \Sigma x : A.B \preceq_h \Sigma x : A'.B' \triangleleft} $$
$$ \text{REC}\text{TM} \quad \frac{\mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash u_l : A_l}{\Gamma \vdash \{l := u_l\}_{l \in \mathcal{L}} : \{l : A_l\}_{l \in \mathcal{L}}} $$

$$ \text{REC}\text{PROJ} \quad \frac{\Gamma \vdash r : \{l : A_l\}_{l \in \mathcal{L}}}{\Gamma \vdash r.l : A_l} $$

$$ \beta\text{REC} \quad \frac{\mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash u_l : A_l}{\Gamma \vdash \{l := u_l\}_{l \in \mathcal{L}}. l \cong u_l : A_l} $$

$$ \eta\text{REC} \quad \frac{\Gamma \vdash r : \{l : A_l\}_{l \in \mathcal{L}}}{\Gamma \vdash r \cong \{l := r.l\}_{l \in \mathcal{L}} : \{l : A_l\}_{l \in \mathcal{L}}} $$

## C.6 Algorithmic record types

Extends Appendix C.2. Record construction terms {$l := u_l$}$_{l \in \mathcal{L}}$ are normal forms, and $r.l$ is neutral whenever $r$ is.

$$ \beta\text{REC} \quad \frac{\{l := u_l\}_{l \in \mathcal{L}}. l \rightsquigarrow 1}{u_l} $$

$$ \text{REC}\text{UNI} \quad \frac{\mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash A_l \triangleright_h \text{Type}_i}{\Gamma \vdash \{l : A_l\}_{l \in \mathcal{L}}^i \triangleright \text{Type}_i} $$

$$ \text{REC}\text{TM} \quad \frac{\mathcal{L} \in \mathcal{P}_f(\text{ Label}) \quad \forall l \in \mathcal{L}. \quad \Gamma \vdash u_l \triangleright A_l}{\Gamma \vdash \{l := u_l\}_{l \in \mathcal{L}} \triangleright \{l : A_l\}_{l \in \mathcal{L}}} $$

$$ \text{REC}\text{ETA} \quad \frac{\forall l \in \mathcal{L}. \quad \Gamma \vdash r.l \cong r'.l \triangleleft A_l}{\Gamma \vdash r \cong_h r' \triangleleft \{l : A_l\}_{l \in \mathcal{L}}} $$

$$ \text{NREC}\text{PROJ} \quad \frac{\Gamma \vdash n \approx_h n' \triangleright \{l : A_l\}_{l \in \mathcal{L}}}{\Gamma \vdash n.l \approx n'.l \triangleright A_l} $$

## C.7 Algorithmic MLTT<sub>sub</sub>

Extends Appendices C.2 and C.6, with rule `CHECKSUB` replacing `CHECK`.

$$ \Gamma \vdash_{\text{sub}} t \triangleleft T $$

$$ \text{CHECKSUB} \quad \frac{\Gamma \vdash_{\text{sub}} t \triangleright T' \quad \Gamma \vdash_{\text{sub}} T' \preceq T \triangleleft}{\Gamma \vdash_{\text{sub}} t \triangleleft T} $$

$$ \Gamma \vdash_{\text{sub}} T \preceq T' \triangleleft $$

Type $T$ is a subtype of type $T'$

$$ \text{TYRED} \quad \frac{T \rightsquigarrow U \quad T' \rightsquigarrow U'}{\Gamma \vdash_{\text{sub}} T \preceq T' \triangleleft} \quad \Gamma \vdash_{\text{sub}} U \preceq_h U' \triangleleft $$

$$ \Gamma \vdash_{\text{sub}} T \preceq_h T' \triangleleft $$

Reduced type $T$ is a subtype of reduced type $T'$

$$ \text{REC}\text{SUB} \quad \frac{\mathcal{K} \subseteq \mathcal{L} \quad \forall k \in \mathcal{K}. \quad \Gamma \vdash_{\text{sub}} A_k \preceq B_k \triangleleft}{\Gamma \vdash_{\text{sub}} \{l : A_l\}_{l \in \mathcal{L}} \preceq_h \{k : A_k\}_{k \in \mathcal{K}} \triangleleft} $$

$$ \text{PROD}\text{SUB} \quad \frac{\Gamma \vdash_{\text{sub}} A' \preceq A \triangleleft \quad \Gamma, x : A' \vdash_{\text{sub}} B \preceq B' \triangleleft}{\Gamma \vdash_{\text{sub}} \Pi x : A.B \preceq_h \Pi x : A'.B' \triangleleft} $$

$$ \text{LIST}\text{SUB} \quad \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft}{\Gamma \vdash_{\text{sub}} \text{List } A \preceq_h \text{List } A' \triangleleft} $$

$$ \text{SIG}\text{SUB} \quad \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \quad \Gamma, x : A \vdash_{\text{sub}} B \preceq B' \triangleleft}{\Gamma \vdash_{\text{sub}} \Sigma x : A.B \preceq_h \Sigma x : A'.B' \triangleleft} $$
$$ \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \Gamma, x : A \vdash_{\text{sub}} B' \preceq B \triangleleft \Gamma \vdash_{\text{sub}} \mathbf{W} x : A.B \preceq_h \mathbf{W} x : A'.B' \triangleleft}{\text{TREE SUB}} $$

$$ \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \Gamma \vdash_{\text{sub}} t \cong t' \triangleleft A' \quad \Gamma \vdash_{\text{sub}} u \cong u' \triangleleft A'}{\Gamma \vdash_{\text{sub}} \mathbf{Id}_A \quad t \cong_h \mathbf{Id}_{A'} \quad t' \cong u' \triangleleft} $$

$$ \text{SUBREFL} \quad \frac{\Gamma \vdash_{\text{sub}} T \preceq_h T \triangleleft}{\Gamma \vdash_{\text{sub}} n \cong_h n' \triangleright T} $$

$$ \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \Gamma \vdash_{\text{sub}} B \preceq B' \triangleleft}{\Gamma \vdash_{\text{sub}} A+B \preceq_h A'+B' \triangleleft} $$

$$ \text{NEUSUB} \quad \frac{\Gamma \vdash_{\text{sub}} n \cong_h n' \triangleright T}{\Gamma \vdash_{\text{sub}} n \preceq_h n' \triangleleft} $$

### Admissible rules

$$ \frac{\Gamma \vdash_{\text{sub}} A \cong A' \triangleleft \Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft}{\Gamma \vdash_{\text{sub}}} $$

$$ \text{SUBANTISYM} \quad \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \Gamma \vdash_{\text{sub}} A' \preceq A \triangleleft \Gamma \vdash_{\text{sub}} A \cong A' \triangleleft}{\Gamma \vdash_{\text{sub}}} $$

$$ \text{SUBTRANS} \quad \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \Gamma \vdash_{\text{sub}} A' \preceq A'' \triangleleft \Gamma \vdash_{\text{sub}} A \preceq A'' \triangleleft}{\Gamma \vdash_{\text{sub}}} $$

## C.8 Reduction rules and normal forms for MLTT<sub>coe</sub>

$$ t \rightsquigarrow^1 t' $$

$$ \text{REDCOEFUN} \quad \frac{\text{nff}}{(\text{coe}_{\Pi x : A.B, \Pi x : A'.B'} f) a \rightsquigarrow^1 \text{coe}_{B[\text{coe}_{A',A} a], B'[a]} (f (\text{coe}_{A',A} a))} $$

$$ \text{REDCOESIG1} \quad \frac{\text{nfp}}{\pi_1 (\text{coe}_{\Sigma x : A.B, \Sigma x : A'.B'} p) \rightsquigarrow^1 \text{coe}_{A,A'} (\pi_1 p)} $$

$$ \text{REDCOESIG2} \quad \frac{\text{nfp}}{\pi_2 (\text{coe}_{\Sigma x : A.B, \Sigma x : A'.B'} p) \rightsquigarrow^1 \text{coe}_{B[\pi_1 p], B' [\text{coe}_{A,A'} (\pi_1 p)]} (\pi_2 p)} $$

$$ \text{REDCOEREC} \quad \frac{\text{nfr}}{(\text{coe}_{\{l : A_l\}_{l \in \mathcal{L}}, \{k : A_k\}_{k \in \mathcal{K}}} r).l \rightsquigarrow^1 \text{coe}_{A_t, B_t} r.l} $$

$$ \text{COEREDID} \quad \frac{\text{T is Type}_i, \mathbf{0}, \mathbf{1} \text{ or } \mathbf{B}}{\text{coe}_{T,T} t \rightsquigarrow^1 t} $$

$$ \text{coe}_{A+B,A'+B'} (\text{inj}_B^l a) \rightsquigarrow^1 \text{inj}_{B'}^l (\text{coe}_{A,A'} a) $$

$$ \text{coe}_{A+B,A'+B'} (\text{inj}_A^r b) \rightsquigarrow^1 \text{inj}_{A'}^r (\text{coe}_{B,B'} b) $$

$$ \text{coe}_{\text{List } A, \text{List } A'} \varepsilon \rightsquigarrow^1 \varepsilon_{A'} $$

$$ \text{coe}_{\text{List } A, \text{List } A'} (h :: t) \rightsquigarrow^1 \text{coe}_{A,A'} h ::_{A'} \text{coe}_{\text{List } A, \text{List } A'} t $$

$$ \text{coe}_{\mathbf{W} x : A.B, \mathbf{W} x : A.B'} (\sup a.l) \rightsquigarrow^1 $$

$$ \sup_{x,B'} (\text{coe}_{A,A'} a) (\lambda x : B' [\text{coe}_{A,A'} a] . \text{coe}_{\mathbf{W} x : A.B, \mathbf{W} x : A.B'} (k (\text{coe}_{B' [\text{coe}_{A,A'} a], B[a]} x))) $$

$$ \text{coe}_{\mathbf{Id}_A a, \mathbf{Id}_{A'} a' b'} \text{refl}_{A,a} \rightsquigarrow^1 \text{refl}_{A', (\text{coe}_{A,A'} a)} $$
$$ \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \Gamma, x : A \vdash_{\text{sub}} B' \preceq B \triangleleft \Gamma \vdash_{\text{sub}} \mathbf{W} x : A.B \preceq_h \mathbf{W} x : A'.B' \triangleleft}{\text{TREE SUB}} $$

$$ \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \Gamma \vdash_{\text{sub}} t \cong t' \triangleleft A' \quad \Gamma \vdash_{\text{sub}} u \cong u' \triangleleft A'}{\Gamma \vdash_{\text{sub}} \mathbf{Id}_A \quad t \cong_h \mathbf{Id}_{A'} \quad t' \cong u' \triangleleft} $$

$$ \text{SUBREFL} \quad \frac{\Gamma \vdash_{\text{sub}} T \preceq_h T \triangleleft}{\Gamma \vdash_{\text{sub}} n \cong_h n' \triangleright T} $$

$$ \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \Gamma \vdash_{\text{sub}} B \preceq B' \triangleleft}{\Gamma \vdash_{\text{sub}} A + B \preceq_h A' + B' \triangleleft} $$

$$ \text{NEUSUB} \quad \frac{\Gamma \vdash_{\text{sub}} n \cong_h n' \triangleright T}{\Gamma \vdash_{\text{sub}} n \preceq_h n' \triangleleft} $$

### Admissible rules

$$ \frac{\Gamma \vdash_{\text{sub}} A \cong A' \triangleleft}{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft} $$

$$ \text{SUBANTISYM} \quad \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \Gamma \vdash_{\text{sub}} A' \preceq A \triangleleft}{\Gamma \vdash_{\text{sub}} A \cong A' \triangleleft} $$

$$ \text{SUBTRANS} \quad \frac{\Gamma \vdash_{\text{sub}} A \preceq A' \triangleleft \Gamma \vdash_{\text{sub}} A' \preceq A'' \triangleleft}{\Gamma \vdash_{\text{sub}} A \preceq A'' \triangleleft} $$

## C.8 Reduction rules and normal forms for MLTT<sub>coe</sub>

$t \rightsquigarrow 1 t'$

$$ \text{REDCOEFUN} \quad \frac{\text{nff}}{(\text{coe}_{\Pi x : A.B, \Pi x : A'.B'} f) a \rightsquigarrow 1 \text{ coe}_{B[\text{coe}_{A',A} a], B'[a]} (f (\text{coe}_{A',A} a))} $$

$$ \text{REDCOESIG1} \quad \frac{\text{nfp}}{\pi_1 (\text{coe}_{\Sigma x : A.B, \Sigma x : A'.B'} p) \rightsquigarrow 1 \text{ coe}_{A,A'} (\pi_1 p)} $$

$$ \text{REDCOESIG2} \quad \frac{\text{nfp}}{\pi_2 (\text{coe}_{\Sigma x : A.B, \Sigma x : A'.B'} p) \rightsquigarrow 1 \text{ coe}_{B[\pi_1 p], B' [\text{coe}_{A,A'} (\pi_1 p)]} (\pi_2 p)} $$

$$ \text{REDCOEREC} \quad \frac{\text{nfr}}{(\text{coe}_{\{l : A_l\}_{l \in \mathcal{L}}, \{k : A_k\}_{k \in \mathcal{K}}} r).l \rightsquigarrow 1 \text{ coe}_{A_l, B_l} r.l} $$

$$ \text{COEREDID} \quad \frac{\text{T is Type}_i, \mathbf{0}, \mathbf{1} \text{ or } \mathbf{B}}{\text{coe}_{T,T} t \rightsquigarrow 1 t} $$

$$ \text{coe}_{A+B,A'+B'} (\text{inj}_B^l a) \rightsquigarrow 1 \text{ inj}_{B'}^l (\text{coe}_{A,A'} a) $$

$$ \text{coe}_{A+B,A'+B'} (\text{inj}_A^r b) \rightsquigarrow 1 \text{ inj}_{A'}^r (\text{coe}_{B,B'} b) $$

$$ \text{coe}_{\text{List } A, \text{List } A'} \varepsilon \rightsquigarrow 1 \varepsilon_{A'} $$

$$ \text{coe}_{\text{List } A, \text{List } A'} (h :: t) \rightsquigarrow 1 \text{ coe}_{A,A'} h ::_{A'} \text{coe}_{\text{List } A, \text{List } A'} t $$

$$ \text{coe}_{\mathbf{W} x : A.B, \mathbf{W} x : A.B'} (\sup a l) \rightsquigarrow 1 $$

$$ \sup_{x,B'} (\text{coe}_{A,A'} a) (\lambda x : B' [\text{coe}_{A,A'} a] . \text{coe}_{\mathbf{W} x : A.B, \mathbf{W} x : A.B'} (k (\text{coe}_{B' [\text{coe}_{A,A'} a], B[a]} x))) $$

$$ \text{coe}_{\mathbf{Id}_A a, \mathbf{Id}_{A'} a' b'} \text{ refl}_{A,a} \rightsquigarrow 1 \text{ refl}_{A', (\text{coe}_{A,A'} a)} $$
$$ \text{COEL} \frac{A \rightsquigarrow A'}{\text{coe}_{A,B} t \rightsquigarrow \text{coe}_{A',B} t} $$

$$ \text{COER} \frac{\text{nf}^{\oplus} \text{ or ne } A}{\text{coe}_{A,B} t \rightsquigarrow \text{coe}_{A,B'} t} \rightsquigarrow B $$

$$ \text{COETM} \frac{\text{nf}^{\oplus} \text{ or ne } A, B}{\text{coe}_{A,B} t \rightsquigarrow \text{coe}_{A,B} t'} $$

$$ \text{COECOE} \frac{\text{nf}^{\oplus} \text{ or ne } U, U', T, T'}{\text{coe}_{U,U'} \text{coe}_{T,T'} n \rightsquigarrow \text{coe}_{T,U'} n} $$

nf f

$$ \begin{array}{l} \text{def} \\ \equiv \quad n \mid P \mid N \mid \lambda x : t.t \mid (t,t) \mid \{l := t_l\}_{l \in \mathcal{L}} \\ \phantom{\equiv \quad} \varepsilon_t \mid t \dot{=} t \mid \sup_t t.t \mid () \mid tt \mid ff \mid \text{refl}_{t,t} \mid \text{inj}_t^l t \mid \text{inj}_t^r t \\ \phantom{\equiv \quad} \text{coe}_{N,N} f \end{array} \qquad \text{weak-head normal forms} $$

nf$^{\oplus} N$

$$ \text{def} \quad \Pi x : t.t \mid \Sigma x : t.t \mid \{l : t_l\}_{l \in \mathcal{L}} \qquad \text{negative whnf types} $$

nf$^{\oplus} P$

$$ \text{def} \quad \text{Type}_i \mid \mathbf{0} \mid \mathbf{1} \mid \mathbf{B} \mid \text{List} t \mid \mathbf{W} x : t.t \mid t+t \mid \mathbf{Id}_t t t' \qquad \text{other whnf types} $$

ne n

$$ \text{def} \quad x \mid n t \mid \pi_1 n \mid \pi_2 n \mid n.l \mid \text{ind}_P(n; t; t) \qquad \text{weak-head neutrals} $$

cne c

$$ \text{def} \quad n \mid \text{coe}_{P,P} n \mid \text{coe}_{n,n} n \qquad \text{compacted neutrals} $$

## C.9 Algorithmic MLTT<sub>coe</sub>

Extends Appendix C.2 and Appendix C.6.

$$ \Gamma \vdash_{\text{coe}} t \triangleleft T $$

$$ \text{COE} \frac{\Gamma \vdash_{\text{coe}} A \triangleleft \Gamma \vdash_{\text{coe}} A' \triangleleft \Gamma \vdash_{\text{coe}} t \triangleleft A \quad \Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft}{\Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} t \triangleleft A'} $$

$$ \Gamma \vdash_{\text{coe}} t \approx_{\text{coe}} t' \triangleleft T $$

Compacted neutrals *t* and *t'* are comparable at type *T*

$$ \text{NCOE} \frac{\Gamma \vdash_{\text{coe}} n \approx n' \triangleleft S''}{\Gamma \vdash_{\text{coe}} \text{coe}_{S,T} n \approx_{\text{coe}} \text{coe}_{S',T'} n' \triangleleft T''} $$

$$ \text{NCOEL} \frac{\Gamma \vdash_{\text{coe}} n \approx n' \triangleleft S''}{\Gamma \vdash_{\text{coe}} \text{coe}_{S,T} n \approx_{\text{coe}} n' \triangleleft T''} $$

$$ \text{NCOER} \frac{\Gamma \vdash_{\text{coe}} n \approx n' \triangleleft S''}{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} \text{coe}_{S',T'} n' \triangleleft T''} $$

$$ \text{NNOCOE} \frac{\Gamma \vdash_{\text{coe}} n \approx n' \triangleleft S''}{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft T''} $$

$$ \Gamma \vdash_{\text{coe}} t \cong_{h} t' \triangleleft T $$

$$ \text{NEULIST} \frac{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft \text{List } A}{\Gamma \vdash_{\text{coe}} n \cong_{h} n' \triangleleft \text{List } A} $$

$$ \text{NEUTREE} \frac{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft \mathbf{W} x : A.B}{\Gamma \vdash_{\text{coe}} n \cong_{h} n' \triangleleft \mathbf{W} x : A.B} $$

$$ \text{NEUID} \frac{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft \mathbf{Id}_A a a'}{\Gamma \vdash_{\text{coe}} n \cong_{h} n' \triangleleft \mathbf{Id}_A a a'} $$

$$ \text{NEUSUM} \frac{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft A + B}{\Gamma \vdash_{\text{coe}} n \cong_{h} n' \triangleleft A + B} $$

$$ \text{NEUNEU} \frac{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft M}{\Gamma \vdash_{\text{coe}} n \cong_{h} n' \triangleleft M} \quad \text{ne } M $$
$$ \text{COEL} \frac{A \rightsquigarrow A'}{\text{coe}_{A,B} t \rightsquigarrow \text{coe}_{A',B} t} $$

$$ \text{COER} \frac{\text{nf}^{\oplus} \text{ or ne } A}{\text{coe}_{A,B} t \rightsquigarrow \text{coe}_{A,B'} t} \rightsquigarrow B $$

$$ \text{COETM} \frac{\text{nf}^{\oplus} \text{ or ne } A, B}{\text{coe}_{A,B} t \rightsquigarrow \text{coe}_{A,B} t'} $$

$$ \text{COECOE} \frac{\text{nf}^{\oplus} \text{ or ne } U, U', T, T'}{\text{coe}_{U,U'} \text{coe}_{T,T'} n \rightsquigarrow \text{coe}_{T,U'} n} $$

nf f

$$ \begin{array}{l} \text{def} \\ \equiv \quad n \mid P \mid N \mid \lambda x : t.t \mid (t,t) \mid \{l := t_l\}_{l \in \mathcal{L}} \\ \phantom{\equiv \quad} \varepsilon_t \mid t \dot{=} t \mid \sup_t t.t \mid () \mid tt \mid ff \mid \text{refl}_{t,t} \mid \text{inj}_t^l t \mid \text{inj}_t^r t \\ \phantom{\equiv \quad} \text{coe}_{N,N} f \end{array} \qquad \text{weak-head normal forms} $$

nf$^{\oplus}$ N

$$ \text{def} \quad \Pi x : t.t \mid \Sigma x : t.t \mid \{l : t_l\}_{l \in \mathcal{L}} \qquad \text{negative whnf types} $$

nf$^{\oplus}$ P

$$ \text{def} \quad \text{Type}_i \mid \mathbf{0} \mid \mathbf{1} \mid \mathbf{B} \mid \text{List} t \mid \mathbf{W} x : t.t \mid t+t \mid \mathbf{Id}_t t t' \qquad \text{other whnf types} $$

ne n

$$ \text{def} \quad x \mid n t \mid \pi_1 n \mid \pi_2 n \mid n.l \mid \text{ind}_P(n; t; t) \qquad \text{weak-head neutrals} $$

cne c

$$ \text{def} \quad n \mid \text{coe}_{P,P} n \mid \text{coe}_{n,n} n \qquad \text{compacted neutrals} $$

## C.9 Algorithmic MLTT<sub>coe</sub>

Extends Appendix C.2 and Appendix C.6.

$$ \Gamma \vdash_{\text{coe}} t \triangleleft T $$

$$ \text{COE} \frac{\Gamma \vdash_{\text{coe}} A \triangleleft \Gamma \vdash_{\text{coe}} A' \triangleleft \Gamma \vdash_{\text{coe}} t \triangleleft A \quad \Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft}{\Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} t \triangleleft A'} $$

$$ \Gamma \vdash_{\text{coe}} t \approx_{\text{coe}} t' \triangleleft T $$

Compacted neutrals $t$ and $t'$ are comparable at type $T$

$$ \text{NCOE} \frac{\Gamma \vdash_{\text{coe}} n \approx n' \triangleleft S''}{\Gamma \vdash_{\text{coe}} \text{coe}_{S,T} n \approx_{\text{coe}} \text{coe}_{S',T'} n' \triangleleft T''} $$

$$ \text{NCOEL} \frac{\Gamma \vdash_{\text{coe}} n \approx n' \triangleleft S''}{\Gamma \vdash_{\text{coe}} \text{coe}_{S,T} n \approx_{\text{coe}} n' \triangleleft T''} $$

$$ \text{NCOER} \frac{\Gamma \vdash_{\text{coe}} n \approx n' \triangleleft S''}{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} \text{coe}_{S',T'} n' \triangleleft T''} $$

$$ \text{NNOCOE} \frac{\Gamma \vdash_{\text{coe}} n \approx n' \triangleleft S''}{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft T''} $$

$$ \Gamma \vdash_{\text{coe}} t \cong_{h} t' \triangleleft T $$

$$ \text{NEULIST} \frac{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft \text{List } A}{\Gamma \vdash_{\text{coe}} n \cong_{h} n' \triangleleft \text{List } A} $$

$$ \text{NEUTREE} \frac{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft \mathbf{W} x : A.B}{\Gamma \vdash_{\text{coe}} n \cong_{h} n' \triangleleft \mathbf{W} x : A.B} $$

$$ \text{NEUID} \frac{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft \mathbf{Id}_A a a'}{\Gamma \vdash_{\text{coe}} n \cong_{h} n' \triangleleft \mathbf{Id}_A a a'} $$

$$ \text{NEUSUM} \frac{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft A + B}{\Gamma \vdash_{\text{coe}} n \cong_{h} n' \triangleleft A + B} $$

$$ \text{NEUNEU} \frac{\Gamma \vdash_{\text{coe}} n \approx_{\text{coe}} n' \triangleleft M}{\Gamma \vdash_{\text{coe}} n \cong_{h} n' \triangleleft M} \quad \text{ne } M $$
$$ \Gamma \vdash_{\text{coe}} T \preceq T' \triangleleft $$

$$ \text{TYRED} \quad \frac{T \rightsquigarrow U \quad T' \rightsquigarrow U' \quad \Gamma \vdash_{\text{coe}} U \preceq_h U' \triangleleft}{\Gamma \vdash_{\text{coe}} T \preceq T' \triangleleft} $$

$$ \Gamma \vdash_{\text{coe}} T \preceq_h T' \triangleleft $$

$$ \text{RECSUB} \quad \frac{\mathcal{K} \subseteq \mathcal{L} \quad \forall k \in \mathcal{K}. \ \Gamma \vdash_{\text{coe}} A_k \preceq B_k \triangleleft}{\Gamma \vdash_{\text{coe}} \{l: A_l\}_{l \in \mathcal{L}} \preceq_h \{k: A_k\}_{k \in \mathcal{K}} \triangleleft} $$

$$ \text{PRODSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A' \preceq A \triangleleft \quad \Gamma, x: A' \vdash_{\text{coe}} B[\text{coe}_{A',A}x] \preceq B' \triangleleft}{\Gamma \vdash_{\text{coe}} \Pi x: A.B \preceq_h \Pi x: A'.B' \triangleleft} $$

$$ \text{LISTSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft}{\Gamma \vdash_{\text{coe}} \textbf{List } A \preceq_h \textbf{List } A' \triangleleft} \qquad \Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft \\ \text{SIGSUB} \quad \frac{\Gamma, x: A \vdash_{\text{coe}} B \preceq B' [\text{coe}_{A,A'}x] \triangleleft}{\Gamma \vdash_{\text{coe}} \Sigma x: A.B \preceq_h \Sigma x: A'.B' \triangleleft} $$

$$ \text{TREESUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft \quad \Gamma, x: A \vdash_{\text{coe}} B' [\text{coe}_{A,A'}x] \preceq B \triangleleft}{\Gamma \vdash_{\text{coe}} \mathbf{W} x: A.B \preceq_h \mathbf{W} x: A'.B' \triangleleft} $$

$$ \text{IDSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft \quad \Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} t \cong t' \triangleleft A' \quad \Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} u \cong u' \triangleleft A'}{\Gamma \vdash_{\text{coe}} \mathbf{Id}_A t u \preceq_h \mathbf{Id}_{A'} t' u' \triangleleft} $$

$$ \text{LISTSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft \quad \Gamma \vdash_{\text{coe}} B \preceq B' \triangleleft}{\Gamma \vdash_{\text{coe}} A+B \preceq_h A'+B' \triangleleft} \qquad \text{SUBREFL} \quad \frac{\text{T is Type}_i, \mathbf{0}, \mathbf{1} \text{ or } \mathbf{B}}{\Gamma \vdash_{\text{coe}} T \preceq T \triangleleft} $$

### C.10 Declarative MLTT<sub>coe</sub>

Extends Appendix C.1 and Appendix C.5.

$$ \Gamma \vdash_{\text{coe}} t : T $$

$$ \text{COE} \quad \frac{\Gamma \vdash_{\text{coe}} A \quad \Gamma \vdash_{\text{coe}} A' \quad \Gamma \vdash_{\text{coe}} t: A \quad \Gamma \vdash_{\text{coe}} A \preceq A'}{\Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} t: A'} $$

$$ \Gamma \vdash_{\text{coe}} t \cong t' : T $$

$$ \text{COEID} \quad \frac{\Gamma \vdash_{\text{coe}} t: A}{\Gamma \vdash_{\text{coe}} \text{coe}_{A,A} t \cong t: A} \qquad \text{COETRANS} \quad \frac{\Gamma \vdash_{\text{coe}} t: A \quad \Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma \vdash_{\text{coe}} A' \preceq A''}{\Gamma \vdash_{\text{coe}} \text{coe}_{A',A''} \text{coe}_{A,A'} t \cong \text{coe}_{A,A''} t: A''} $$

$$ \text{COECONG} \quad \frac{\Gamma \vdash_{\text{coe}} t \cong t' : A \quad \Gamma \vdash_{\text{coe}} A \cong A' \quad \Gamma \vdash_{\text{coe}} B \cong B'}{\Gamma \vdash_{\text{coe}} \text{coe}_{A,B} t \cong \text{coe}_{A',B'} t' : B} $$
$$ \Gamma \vdash_{\text{coe}} T \preceq T' \triangleleft $$

$$ \text{TYRED} \quad \frac{T \rightsquigarrow U \quad T' \rightsquigarrow U' \quad \Gamma \vdash_{\text{coe}} U \preceq_h U' \triangleleft}{\Gamma \vdash_{\text{coe}} T \preceq T' \triangleleft} $$

$$ \Gamma \vdash_{\text{coe}} T \preceq_h T' \triangleleft $$

$$ \text{RECSUB} \quad \frac{\mathcal{K} \subseteq \mathcal{L} \quad \forall k \in \mathcal{K}. \ \Gamma \vdash_{\text{coe}} A_k \preceq B_k \triangleleft}{\Gamma \vdash_{\text{coe}} \{l: A_l\}_{l \in \mathcal{L}} \preceq_h \{k: A_k\}_{k \in \mathcal{K}} \triangleleft} $$

$$ \text{PRODSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A' \preceq A \triangleleft \quad \Gamma, x: A' \vdash_{\text{coe}} B[\text{coe}_{A',A}x] \preceq B' \triangleleft}{\Gamma \vdash_{\text{coe}} \Pi x: A.B \preceq_h \Pi x: A'.B' \triangleleft} $$

$$ \text{LISTSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft}{\Gamma \vdash_{\text{coe}} \textbf{List } A \preceq_h \textbf{List } A' \triangleleft} \qquad \Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft \\ \text{SIGSUB} \quad \frac{\Gamma, x: A \vdash_{\text{coe}} B \preceq B' [\text{coe}_{A,A'}x] \triangleleft}{\Gamma \vdash_{\text{coe}} \Sigma x: A.B \preceq_h \Sigma x: A'.B' \triangleleft} $$

$$ \text{TREESUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft \quad \Gamma, x: A \vdash_{\text{coe}} B' [\text{coe}_{A,A'}x] \preceq B \triangleleft}{\Gamma \vdash_{\text{coe}} \mathbf{W} x: A.B \preceq_h \mathbf{W} x: A'.B' \triangleleft} $$

$$ \text{IDSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft \quad \Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} t \cong t' \triangleleft A' \quad \Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} u \cong u' \triangleleft A'}{\Gamma \vdash_{\text{coe}} \mathbf{Id}_A t u \preceq_h \mathbf{Id}_{A'} t' u' \triangleleft} $$

$$ \text{LISTSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \triangleleft \quad \Gamma \vdash_{\text{coe}} B \preceq B' \triangleleft}{\Gamma \vdash_{\text{coe}} A+B \preceq_h A'+B' \triangleleft} \qquad \text{SUBREFL} \quad \frac{\text{T is Type}_i, \mathbf{0}, \mathbf{1} \text{ or } \mathbf{B}}{\Gamma \vdash_{\text{coe}} T \preceq T \triangleleft} $$

### C.10 Declarative MLTT<sub>coe</sub>

Extends Appendix C.1 and Appendix C.5.

$$ \Gamma \vdash_{\text{coe}} t : T $$

$$ \text{COE} \quad \frac{\Gamma \vdash_{\text{coe}} A \quad \Gamma \vdash_{\text{coe}} A' \quad \Gamma \vdash_{\text{coe}} t: A \quad \Gamma \vdash_{\text{coe}} A \preceq A'}{\Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} t: A'} $$

$$ \Gamma \vdash_{\text{coe}} t \cong t' : T $$

$$ \text{COEID} \quad \frac{\Gamma \vdash_{\text{coe}} t: A}{\Gamma \vdash_{\text{coe}} \text{coe}_{A,A} t \cong t: A} \qquad \text{COETRANS} \quad \frac{\Gamma \vdash_{\text{coe}} t: A \quad \Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma \vdash_{\text{coe}} A' \preceq A''}{\Gamma \vdash_{\text{coe}} \text{coe}_{A',A''} \text{coe}_{A,A'} t \cong \text{coe}_{A,A''} t: A''} $$

$$ \text{COECONG} \quad \frac{\Gamma \vdash_{\text{coe}} t \cong t' : A \quad \Gamma \vdash_{\text{coe}} A \cong A' \quad \Gamma \vdash_{\text{coe}} B \cong B'}{\Gamma \vdash_{\text{coe}} \text{coe}_{A,B} t \cong \text{coe}_{A',B'} t' : B} $$
$$ \text{COEFUN} \quad \frac{\Gamma \vdash_{\text{coe}} A' \preceq A \quad \Gamma, x : A' \vdash_{\text{coe}} B [\text{coe}_{A',A} x] \preceq B' \quad \Gamma \vdash_{\text{coe}} f : \Pi x : A.B \quad \Gamma \vdash_{\text{coe}} a : A'}{\Gamma \vdash_{\text{coe}} (\text{coe}_{\Pi x : A.B, \Pi x : A', B'} f) a \cong \text{coe}_{B[\text{coe}_{A',A} a], B'[x]} (f (\text{coe}_{A',A} a)) : \Pi x : A'.B'} $$

$$ \text{COESIG1} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma, x : A \vdash_{\text{coe}} B \preceq B' [\text{coe}_{A,A'} x] \quad \Gamma \vdash_{\text{coe}} p : \Sigma x : A.B}{\Gamma \vdash_{\text{coe}} \pi_1 (\text{coe}_{\Sigma x : A.B, \Sigma x : A'.B'} p) \cong \text{coe}_{A,A'} (\pi_1 p) : A'} $$

$$ \text{COESIG2} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma, x : A \vdash_{\text{coe}} B \preceq B' [\text{coe}_{A,A'} x] \quad \Gamma \vdash_{\text{coe}} p : \Sigma x : A.B}{\Gamma \vdash_{\text{coe}} \pi_2 (\text{coe}_{\Sigma x : A.B, \Sigma x : A'.B} p) \cong \text{coe}_{B[\pi_1 p], B'[\text{coe}_{A,A'} (\pi_1 p)]} (\pi_2 p) : B' [\text{coe}_{A,A'} (\pi_1 p)]} $$

$$ \text{COEREC} \quad \frac{\mathcal{K} \subseteq \mathcal{L} \quad \forall k \in \mathcal{K}. \quad \Gamma \vdash_{\text{coe}} A_k \preceq B_k \quad \Gamma \vdash r \triangleright \{l : A_l\}_{l \in \mathcal{L}}}{\Gamma \vdash_{\text{coe}} (\text{coe}_{\{l : A_l\}_{l \in \mathcal{L}}, \{k : A_k\}_{k \in \mathcal{K}}} r).k \cong \text{coe}_{A_k, B_k} r.k : B_k} $$

$$ \text{COENIL} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A'}{\Gamma \vdash_{\text{coe}} \text{coe}_{\text{List A, List A'}} \varepsilon_A \cong \varepsilon_{A'} : \text{List A'}} $$

$$ \text{COECONS} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma \vdash_{\text{coe}} a : A \quad \Gamma \vdash_{\text{coe}} l : \text{List A}}{\Gamma \vdash_{\text{coe}} \text{coe}_{\text{List A, List A'}} (a ::_A l) \cong (\text{coe}_{A,A'} a) ::_{A'} (\text{coe}_{\text{List A, List A'}} l) : \text{List A'}} $$

$$ \text{COETREE} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma, x : A \vdash_{\text{coe}} B' [\text{coe}_{A,A'} x] \preceq B \quad \Gamma \vdash_{\text{coe}} a : A \quad \Gamma \vdash_{\text{coe}} k : B a \to \mathbf{W} x : A.B}{\Gamma \vdash_{\text{coe}} \text{coe}_{\mathbf{W} x : A.B, \mathbf{W} x : A.B'} (\sup_{x.B} a l) \cong \sup_{x.B'} (\text{coe}_{A,A'} a) (\lambda x : B' [\text{coe}_{A,A'} a] . \text{coe}_{\mathbf{W} x : A.B, \mathbf{W} x : A.B'} (k (\text{coe}_{B' [\text{coe}_{A,A'} a], B[a]} x))) : \mathbf{W} x : A'.B'} $$

$$ \text{COEID} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma \vdash_{\text{coe}} a : A}{\Gamma \vdash_{\text{coe}} \text{coe}_{\mathbf{Id}_A a, \mathbf{Id}_{A'} (\text{coe}_{A,A'} a) a} \text{refl}_{A, a} \cong \text{refl}_{A', (\text{coe}_{A,A'} a)} : \mathbf{Id}_A (\text{coe}_{A,A'} a) (\text{coe}_{A,A'} a)} $$

$$ \text{COESUMLEFT} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma \vdash_{\text{coe}} B \preceq B' \quad \Gamma \vdash_{\text{coe}} a : A}{\Gamma \vdash_{\text{coe}} \text{coe}_{A+B,A'+B'} (\text{inj}^l a) \cong \text{inj}^l (\text{coe}_{A,A'} a) : A' + B'} $$

$$ \text{COESUMRIGHT} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma \vdash_{\text{coe}} B \preceq B' \quad \Gamma \vdash_{\text{coe}} b : B}{\Gamma \vdash_{\text{coe}} \text{coe}_{A+B,A'+B'} (\text{inj}^r b) \cong \text{inj}^r (\text{coe}_{B,B'} b) : A' + B'} $$

$\Gamma \vdash_{\text{coe}} T \preceq T'$ \qquad T$ is a subtype of $T'$ in context $\Gamma$

$$ \text{REC SUB} \quad \frac{\mathcal{K} \subseteq \mathcal{L} \quad \forall k \in \mathcal{K}. \quad \Gamma \vdash_{\text{coe}} A_k \preceq B_k}{\Gamma \vdash_{\text{coe}} \{l : A_l\}_{l \in \mathcal{L}} \preceq \{k : A_k\}_{k \in \mathcal{K}}} $$

$$ \text{PROD SUB} \quad \frac{\Gamma \vdash_{\text{coe}} A' \preceq A \quad \Gamma, x : A' \vdash_{\text{coe}} B [\text{coe}_{A',A} x] \preceq B'}{\Gamma \vdash_{\text{coe}} \Pi x : A.B \preceq \Pi x : A'.B'} $$
$$ \text{COEFUN} \quad \frac{\Gamma \vdash_{\text{coe}} A' \preceq A \quad \Gamma, x : A' \vdash_{\text{coe}} B [\text{coe}_{A',A} x] \preceq B' \quad \Gamma \vdash_{\text{coe}} f : \Pi x : A.B \quad \Gamma \vdash_{\text{coe}} a : A'}{\Gamma \vdash_{\text{coe}} (\text{coe}_{\Pi x : A.B, \Pi x : A', B'} f) a \cong \text{coe}_{B[\text{coe}_{A',A} a], B'[x]} (f (\text{coe}_{A',A} a)) : \Pi x : A'.B'} $$

$$ \text{COESIG1} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma, x : A \vdash_{\text{coe}} B \preceq B' [\text{coe}_{A,A'} x] \quad \Gamma \vdash_{\text{coe}} p : \Sigma x : A.B}{\Gamma \vdash_{\text{coe}} \pi_1 (\text{coe}_{\Sigma x : A.B, \Sigma x : A'.B'} p) \cong \text{coe}_{A,A'} (\pi_1 p) : A'} $$

$$ \text{COESIG2} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma, x : A \vdash_{\text{coe}} B \preceq B' [\text{coe}_{A,A'} x] \quad \Gamma \vdash_{\text{coe}} p : \Sigma x : A.B}{\Gamma \vdash_{\text{coe}} \pi_2 (\text{coe}_{\Sigma x : A.B, \Sigma x : A'.B} p) \cong \text{coe}_{B[\pi_1 p], B'[\text{coe}_{A,A'} (\pi_1 p)]} (\pi_2 p) : B' [\text{coe}_{A,A'} (\pi_1 p)]} $$

$$ \text{COEREC} \quad \frac{\mathcal{K} \subseteq \mathcal{L} \quad \forall k \in \mathcal{K}. \quad \Gamma \vdash_{\text{coe}} A_k \preceq B_k \quad \Gamma \vdash r \triangleright \{l : A_l\}_{l \in \mathcal{L}}}{\Gamma \vdash_{\text{coe}} (\text{coe}_{\{l : A_l\}_{l \in \mathcal{L}}, \{k : A_k\}_{k \in \mathcal{K}}} r).k \cong \text{coe}_{A_k, B_k} r.k : B_k} $$

$$ \text{COENIL} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A'}{\Gamma \vdash_{\text{coe}} \text{coe}_{\text{List A, List A'}} \varepsilon_A \cong \varepsilon_{A'} : \text{List A'}} $$

$$ \text{COECONS} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma \vdash_{\text{coe}} a : A \quad \Gamma \vdash_{\text{coe}} l : \text{List A}}{\Gamma \vdash_{\text{coe}} \text{coe}_{\text{List A, List A'}} (a ::_A l) \cong (\text{coe}_{A,A'} a) ::_{A'} (\text{coe}_{\text{List A, List A'}} l) : \text{List A'}} $$

$$ \text{COETREE} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma, x : A \vdash_{\text{coe}} B' [\text{coe}_{A,A'} x] \preceq B \quad \Gamma \vdash_{\text{coe}} a : A \quad \Gamma \vdash_{\text{coe}} k : B a \to \mathbf{W} x : A.B}{\Gamma \vdash_{\text{coe}} \text{coe}_{\mathbf{W} x : A.B, \mathbf{W} x : A.B'} (\sup_{x.B} a l) \cong \sup_{x.B'} (\text{coe}_{A,A'} a) (\lambda x : B' [\text{coe}_{A,A'} a]. \text{coe}_{\mathbf{W} x : A.B, \mathbf{W} x : A.B'} (k (\text{coe}_{B' [\text{coe}_{A,A'} a], B[a]} x))) : \mathbf{W} x : A'.B'} $$

$$ \text{COEID} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma \vdash_{\text{coe}} a : A}{\Gamma \vdash_{\text{coe}} \text{coe}_{\mathbf{Id}_A a, \mathbf{Id}_{A'} (\text{coe}_{A,A'} a) a} \text{refl}_{A, a} \cong \text{refl}_{A', (\text{coe}_{A,A'} a)} : \mathbf{Id}_A (\text{coe}_{A,A'} a) (\text{coe}_{A,A'} a)} $$

$$ \text{COESUMLEFT} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma \vdash_{\text{coe}} B \preceq B' \quad \Gamma \vdash_{\text{coe}} a : A}{\Gamma \vdash_{\text{coe}} \text{coe}_{A+B,A'+B'} (\text{inj}^l a) \cong \text{inj}^l (\text{coe}_{A,A'} a) : A' + B'} $$

$$ \text{COESUMRIGHT} \quad \frac{\Gamma \vdash_{\text{coe}} A \preceq A' \quad \Gamma \vdash_{\text{coe}} B \preceq B' \quad \Gamma \vdash_{\text{coe}} b : B}{\Gamma \vdash_{\text{coe}} \text{coe}_{A+B,A'+B'} (\text{inj}^r b) \cong \text{inj}^r (\text{coe}_{B,B'} b) : A' + B'} $$

$\Gamma \vdash_{\text{coe}} T \preceq T'$ \qquad T$ is a subtype of $T'$ in context $\Gamma$

$$ \text{REC SUB} \quad \frac{\mathcal{K} \subseteq \mathcal{L} \quad \forall k \in \mathcal{K}. \quad \Gamma \vdash_{\text{coe}} A_k \preceq B_k}{\Gamma \vdash_{\text{coe}} \{l : A_l\}_{l \in \mathcal{L}} \preceq \{k : A_k\}_{k \in \mathcal{K}}} $$

$$ \text{PROD SUB} \quad \frac{\Gamma \vdash_{\text{coe}} A' \preceq A \quad \Gamma, x : A' \vdash_{\text{coe}} B [\text{coe}_{A',A} x] \preceq B'}{\Gamma \vdash_{\text{coe}} \Pi x : A.B \preceq \Pi x : A'.B'} $$
$$ \text{LISTSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A'}{\Gamma \vdash_{\text{coe}} \text{List } A \prec \text{List } A'} \qquad \text{SIGSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A'}{\Gamma \vdash_{\text{coe}} \Sigma x : A.B \prec \Sigma x : A'.B'} $$

$$ \text{TREESUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A' \qquad \Gamma, x : A \vdash_{\text{coe}} B' [\text{coe}_{A,A'} x] \prec B}{\Gamma \vdash_{\text{coe}} \mathbf{W} x : A.B \prec \mathbf{W} x : A'.B'} $$

$$ \text{IDSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A' \qquad \Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} t \cong t' : A' \qquad \Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} u \cong u' : A'}{\Gamma \vdash_{\text{coe}} \mathbf{Id}_A t u \prec \mathbf{Id}_{A'} t' u'} $$

$$ \text{SUMSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A' \qquad \Gamma \vdash_{\text{coe}} B \prec B'}{\Gamma \vdash_{\text{coe}} A+B \prec A'+B'} $$

$$ \text{SUBREFL} \quad \frac{\Gamma \vdash_{\text{coe}} A \cong A'}{\Gamma \vdash_{\text{coe}} A \prec A'} \qquad \text{SUBTRANS} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A' \qquad \Gamma \vdash_{\text{coe}} A' \prec A''}{\Gamma \vdash_{\text{coe}} A \prec A''} $$

# D PROOFS OF LEMMAS

This section contains additional lemmas and proofs omitted from the body of the paper.

## D.1 From Section 3.2

$$ \text{map}_{\Pi}((g, f) : \text{hom}_{\Pi}((A, B), (A', B'))) (h : \Pi(x : A)B) \stackrel{\text{def}}{=} \lambda x : A'.f (h (g x)) $$

$$ \text{map}_{\Sigma}((g, f) : \text{hom}_{\Pi}((A, B), (A', B'))) (p : \Sigma(x : A)B) \stackrel{\text{def}}{=} (g(\pi_1 p), f(\pi_2 p)) $$

**LEMMA D.1.** *map*<sub>Π</sub> and map<sub>Σ</sub> satisfy the functor laws MAPID and MAPCOMP.

*PROOF.* For the preservation of identities, we have:

$$ \text{map}_{\Pi}(\text{id}_A, \lambda\{x : A\}. \text{id}_{Bx}) h \cong \lambda x : A. \text{id}_{Bx} (h (\text{id}_A x)) \cong \lambda x : A. g x \cong g $$

$$ \text{map}_{\Sigma}(\text{id}_A, \lambda\{x : A\}. \text{id}_{Bx}) p \cong (\text{id}_A (\pi_1 p), \text{id}_{B(\pi_1 p)} (\pi_2 p)) \cong (\pi_1 p, \pi_2 p) \cong p $$

For $(g, f) : \text{hom}_{\Pi}((A_2, B_2), (A_3, B_3)), (g', f') : \text{hom}_{\Pi}((A_1, B_1), (A_2, B_2))$ and $h : \Pi x : A_1.B_1 x$ we compute

$$ \begin{align*} \text{map}_{\Pi}(g, f)(\text{map}_{\Pi}(g', f') h) &\cong \lambda x : A.f((\lambda x' : A'.f'(h(g'x')))(g x)) \\ &\cong \lambda x : A, f(f'(h(g'(gx)))) \\ &\cong \lambda x : A, (f \circ f')(h((g' \circ g)x)) \cong \text{map}_{\Pi}((g, f) \circ (g', f'))h \end{align*} $$

Similarly, for $(g, f) : \text{hom}_{\Sigma}((A_2, B_2), (A_3, B_3)), (g', f') : \text{hom}_{\Sigma}((A_1, B_1), (A_2, B_2))$ and $p : \Sigma x : A_1.B_1 x$:

$$ \begin{align*} \text{map}_{\Sigma}(g, f)(\text{map}_{\Sigma}(g', f') p) &\cong (g(\pi_1 \text{map}_{\Sigma}(g', f') p), f(\pi_2 \text{map}_{\Sigma}(g', f') p)) \\ &\cong (g(g'(\pi_1 p)), f(f'(\pi_2 p))) \\ &\cong ((g \circ g')(\pi_1 p)), (f \circ f')(\pi_2 p)) \\ &\cong \text{map}_{\Sigma}((g, f) \circ (g', f')) p \end{align*} $$

□
$$ \text{LISTSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A'}{\Gamma \vdash_{\text{coe}} \text{List } A \prec \text{List } A'} \qquad \text{SIGSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A'}{\Gamma \vdash_{\text{coe}} \Sigma x : A.B \prec \Sigma x : A'.B'} $$

$$ \text{TREESUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A' \qquad \Gamma, x : A \vdash_{\text{coe}} B' [\text{coe}_{A,A'} x] \prec B}{\Gamma \vdash_{\text{coe}} \mathbf{W} x : A.B \prec \mathbf{W} x : A'.B'} $$

$$ \text{IDSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A' \qquad \Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} t \cong t' : A' \qquad \Gamma \vdash_{\text{coe}} \text{coe}_{A,A'} u \cong u' : A'}{\Gamma \vdash_{\text{coe}} \mathbf{Id}_A t u \prec \mathbf{Id}_{A'} t' u'} $$

$$ \text{SUMSUB} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A' \qquad \Gamma \vdash_{\text{coe}} B \prec B'}{\Gamma \vdash_{\text{coe}} A+B \prec A'+B'} $$

$$ \text{SUBREFL} \quad \frac{\Gamma \vdash_{\text{coe}} A \cong A'}{\Gamma \vdash_{\text{coe}} A \prec A'} \qquad \text{SUBTRANS} \quad \frac{\Gamma \vdash_{\text{coe}} A \prec A' \qquad \Gamma \vdash_{\text{coe}} A' \prec A''}{\Gamma \vdash_{\text{coe}} A \prec A''} $$

# D PROOFS OF LEMMAS

This section contains additional lemmas and proofs omitted from the body of the paper.

## D.1 From Section 3.2

$$ \text{map}_{\Pi}((g, f) : \text{hom}_{\Pi}((A, B), (A', B'))) (h : \Pi(x : A)B) \stackrel{\text{def}}{=} \lambda x : A'.f(h(g x)) $$

$$ \text{map}_{\Sigma}((g, f) : \text{hom}_{\Pi}((A, B), (A', B'))) (p : \Sigma(x : A)B) \stackrel{\text{def}}{=} (g(\pi_1 p), f(\pi_2 p)) $$

LEMMA D.1. $\text{map}_{\Pi}$ and $\text{map}_{\Sigma}$ satisfy the functor laws MAPID and MAPCOMP.

PROOF. For the preservation of identities, we have:

$$ \text{map}_{\Pi}(\text{id}_A, \lambda\{x : A\}. \text{id}_{Bx}) h \cong \lambda x : A. \text{id}_{Bx} (h (\text{id}_A x)) \cong \lambda x : A. g x \cong g $$

$$ \text{map}_{\Sigma}(\text{id}_A, \lambda\{x : A\}. \text{id}_{Bx}) p \cong (\text{id}_A (\pi_1 p), \text{id}_{B(\pi_1 p)} (\pi_2 p)) \cong (\pi_1 p, \pi_2 p) \cong p $$

For $(g, f) : \text{hom}_{\Pi}((A_2, B_2), (A_3, B_3))$, $(g', f') : \text{hom}_{\Pi}((A_1, B_1), (A_2, B_2))$ and $h : \Pi x : A_1.B_1 x$ we compute

$$ \begin{align*} \text{map}_{\Pi}(g, f) (\text{map}_{\Pi}(g', f') h) &\cong \lambda x : A. f ((\lambda x' : A'.f' (h (g' x')) (g x)) \\ &\cong \lambda x : A, f (f' (h (g' (g x)))) \\ &\cong \lambda x : A, (f \circ f') (h ((g' \circ g) x)) \cong \text{map}_{\Pi}((g, f) \circ (g', f')) h \end{align*} $$

Similarly, for $(g, f) : \text{hom}_{\Sigma}((A_2, B_2), (A_3, B_3))$, $(g', f') : \text{hom}_{\Sigma}((A_1, B_1), (A_2, B_2))$ and $p : \Sigma x : A_1.B_1 x$:

$$ \begin{align*} \text{map}_{\Sigma}(g, f) (\text{map}_{\Sigma}(g', f') p) &\cong (g(\pi_1 \text{map}_{\Sigma}(g', f') p), f(\pi_2 \text{map}_{\Sigma}(g', f') p)) \\ &\cong (g(g'(\pi_1 p)), f(f'(\pi_2 p))) \\ &\cong ((g \circ g')(\pi_1 p)), (f \circ f')(\pi_2 p)) \\ &\cong \text{map}_{\Sigma}((g, f) \circ (g', f')) p \end{align*} $$

□
## D.2 From Section 5.3

**LEMMA D.2 (CATCH UP, FUNCTION TYPE (LEMMA 5.4)).** If $\Gamma \vdash_{\text{coe}} f a \triangleleft B$ and $|f| = \lambda x : A'. t'$, then there exists $t$ such that $|t| = t'$ and $f a \rightsquigarrow^* t[a]$.

**PROOF.** We must have that $f = (\text{coe}_{T_1, \dots, T_n}(\lambda x : A.t_0))^{15}$ for some $A, t_0$ such that $|A| = A'$ and $|t_0| = t'$. Moreover, by well-typing we know that there exists some $B_0$ such that $\Gamma, x : A \vdash_{\text{coe}} t_0 \triangleright B_0$, $\Gamma \vdash_{\text{coe}} \Pi x : A.B_0 \cong T_1 \prec \dots \prec T_n \triangleleft$. By inversions, we must have $T_i \rightsquigarrow^* \Pi x : A_i.B_i$, with the $A_i$ and $B_i$ again related. But now we can use the reduction rule of coe on product types, and get

$$f a \rightsquigarrow^* \text{coe}_{B'_0, B'_1, \dots, B'_n}((\lambda x : A.t_0) (\text{coe}_{A_n, \dots, A_1, A} a))$$

where the $B'_i$ are obtained by adequately substituting coercions in the $B_i$. Now all the $B'_i$ are well-typed by subject reduction, so they must have weak-head normal forms $B''_i$, and once all of them have been reduced to weak-head normal form by a combination of COEL, COER and COETM, we can finally reduce the inner $\beta$-redex, obtaining

$$f a \rightsquigarrow^* \text{coe}_{B''_0, B''_1, \dots, B''_n}(t_0 [\text{coe}_{A_n, \dots, A_1, A} a])$$

Now we can conclude, as indeed

$$\begin{align*}
|\text{coe}_{B''_0, B''_1, \dots, B''_n}(t_0 [\text{coe}_{A_n, \dots, A_1, A} x])| &= |t_0 [\text{coe}_{A_n, \dots, A_1, A} x]| \\
&= |t_0| [|\text{coe}_{A_n, \dots, A_1, A} x]| \\
&= |t_0| [|x]| = |t_0| = t'
\end{align*}$$

□

**LEMMA D.3 (ERASURE IS A BACKWARD SIMULATION (LEMMA 5.5)).** Assume that $\Gamma \vdash_{\text{coe}} t \triangleleft T$. If $|t| \rightsquigarrow^* u'$, with $u'$ a weak-head normal form, then $t \rightsquigarrow^* u$, with $u$ a weak-head normal form such that $|u| = u'$.

**PROOF.** First, if $|t| \rightsquigarrow^* u'$, then there exists $u$ such that $t \rightsquigarrow^* u$ and $|u| = u'$. Indeed, the previous catch-up lemmas ensure that redexes never get blocked by coercions. On function types, the lemma exactly says that a term erasing to a $\beta$-redex is able to simulate the $\beta$-reduction. On positive types, by the catch-up lemma again, coercions on a constructor reduce away until the constructor is exposed directly to the destructor, and so the reduction can kick in.

Second, if $|u|$ is a weak-head normal form, then there exists a weak-head normal form $v$ such that $u \rightsquigarrow^* v$ and $|v| = |u|$. Indeed, if $|u|$ is a weak-head normal form but $u$ is not, it must be because either $|u|$ is a constructor of a positive type, or a neutral. In the first case, the catch-up lemmas let us conclude. In the second, we can iterate COECOE to fuse coercions until $u$ reduces to a compacted neutral, which is a weak-head normal form. □

**LEMMA D.4 (ELABORATION PRESERVES SUBTYPING (LEMMA 5.6)).** The following implications hold whenever the inputs of the conclusions are well-formed:

(1) if $|\Gamma| \vdash_{\text{sub}} |T| \preceq_h^m |U| \triangleleft$, then $\Gamma \vdash_{\text{coe}} T \preceq_h^m U \triangleleft$;

(2) if $|\Gamma| \vdash_{\text{sub}} |T| \preceq_h^m |U| \triangleleft$, then $\Gamma \vdash_{\text{coe}} T \preceq_h U \triangleleft$;

(3) if $|\Gamma| \vdash_{\text{sub}} |t| \cong_h^l |u| \triangleleft |T|$, then $\Gamma \vdash_{\text{coe}} t \cong_h^l u \triangleleft T$;

(4) if $|\Gamma| \vdash_{\text{sub}} |t| \cong |u| \triangleleft |T|$, then $\Gamma \vdash_{\text{coe}} t \cong u \triangleleft T$;

(5) if $|\Gamma| \vdash_{\text{sub}} |t| \approx |u| \triangleright T$, then $\Gamma \vdash_{\text{coe}} t \approx u \triangleright T$;

(6) if $|\Gamma| \vdash_{\text{sub}} |t| \approx_h^l |u| \triangleright T$, then $\Gamma \vdash_{\text{coe}} t \approx u \triangleright T$.

<footnote>15That is, a string of coercions $\text{coe}_{T_{n-1}, T_n}(\dots \text{coe}_{T_1, T_2}(\lambda x : A.t_0))$.</footnote>
## D.2 From Section 5.3

**LEMMA D.2 (CATCH UP, FUNCTION TYPE (LEMMA 5.4)).** If $\Gamma \vdash_{\text{coe}} f a \triangleleft B$ and $|f| = \lambda x : A'. t'$, then there exists $t$ such that $|t| = t'$ and $f a \rightsquigarrow^* t[a]$.

**PROOF.** We must have that $f = (\text{coe}_{T_1, \dots, T_n}(\lambda x : A.t_0))^{15}$ for some $A, t_0$ such that $|A| = A'$ and $|t_0| = t'$. Moreover, by well-typing we know that there exists some $B_0$ such that $\Gamma, x : A \vdash_{\text{coe}} t_0 \triangleright B_0$, $\Gamma \vdash_{\text{coe}} \Pi x : A.B_0 \cong T_1 \prec \dots \prec T_n \triangleleft$. By inversions, we must have $T_i \rightsquigarrow^* \Pi x : A_i.B_i$, with the $A_i$ and $B_i$ again related. But now we can use the reduction rule of coe on product types, and get

$$f a \rightsquigarrow^* \text{coe}_{B'_0, B'_1, \dots, B'_n}((\lambda x : A.t_0) (\text{coe}_{A_n, \dots, A_1, A} a))$$

where the $B'_i$ are obtained by adequately substituting coercions in the $B_i$. Now all the $B'_i$ are well-typed by subject reduction, so they must have weak-head normal forms $B''_i$, and once all of them have been reduced to weak-head normal form by a combination of COEL, COER and COETM, we can finally reduce the inner $\beta$-redex, obtaining

$$f a \rightsquigarrow^* \text{coe}_{B''_0, B''_1, \dots, B''_n}(t_0 [\text{coe}_{A_n, \dots, A_1, A} a])$$

Now we can conclude, as indeed

$$\begin{align*}
|\text{coe}_{B''_0, B''_1, \dots, B''_n}(t_0 [\text{coe}_{A_n, \dots, A_1, A} x])| &= |t_0 [\text{coe}_{A_n, \dots, A_1, A} x]| \\
&= |t_0| [|\text{coe}_{A_n, \dots, A_1, A} x]| \\
&= |t_0| [|x]| = |t_0| = t'
\end{align*}$$

□

**LEMMA D.3 (ERASURE IS A BACKWARD SIMULATION (LEMMA 5.5)).** Assume that $\Gamma \vdash_{\text{coe}} t \triangleleft T$. If $|t| \rightsquigarrow^* u'$, with $u'$ a weak-head normal form, then $t \rightsquigarrow^* u$, with $u$ a weak-head normal form such that $|u| = u'$.

**PROOF.** First, if $|t| \rightsquigarrow^* u'$, then there exists $u$ such that $t \rightsquigarrow^* u$ and $|u| = u'$. Indeed, the previous catch-up lemmas ensure that redexes never get blocked by coercions. On function types, the lemma exactly says that a term erasing to a $\beta$-redex is able to simulate the $\beta$-reduction. On positive types, by the catch-up lemma again, coercions on a constructor reduce away until the constructor is exposed directly to the destructor, and so the reduction can kick in.

Second, if $|u|$ is a weak-head normal form, then there exists a weak-head normal form $v$ such that $u \rightsquigarrow^* v$ and $|v| = |u|$. Indeed, if $|u|$ is a weak-head normal form but $u$ is not, it must be because either $|u|$ is a constructor of a positive type, or a neutral. In the first case, the catch-up lemmas let us conclude. In the second, we can iterate COECOE to fuse coercions until $u$ reduces to a compacted neutral, which is a weak-head normal form. □

**LEMMA D.4 (ELABORATION PRESERVES SUBTYPING (LEMMA 5.6)).** The following implications hold whenever the inputs of the conclusions are well-formed:

(1) if $|\Gamma| \vdash_{\text{sub}} |T| \preceq_h^m |U| \triangleleft$, then $\Gamma \vdash_{\text{coe}} T \preceq_h^m U \triangleleft$;

(2) if $|\Gamma| \vdash_{\text{sub}} |T| \preceq_h^m |U| \triangleleft$, then $\Gamma \vdash_{\text{coe}} T \preceq_h U \triangleleft$;

(3) if $|\Gamma| \vdash_{\text{sub}} |t| \cong_h^1 |u| \triangleleft |T|$, then $\Gamma \vdash_{\text{coe}} t \cong_h^1 u \triangleleft T$;

(4) if $|\Gamma| \vdash_{\text{sub}} |t| \cong |u| \triangleleft |T|$, then $\Gamma \vdash_{\text{coe}} t \cong u \triangleleft T$;

(5) if $|\Gamma| \vdash_{\text{sub}} |t| \approx |u| \triangleright T$, then $\Gamma \vdash_{\text{coe}} t \approx u \triangleright T$;

(6) if $|\Gamma| \vdash_{\text{sub}} |t| \approx_h^1 |u| \triangleright T$, then $\Gamma \vdash_{\text{coe}} t \approx u \triangleright T$.

<footnote>15That is, a string of coercions $\text{coe}_{T_{n-1}, T_n}(\dots \text{coe}_{T_1, T_2}(\lambda x : A.t_0))$.</footnote>
**PROOF.** Lemma 5.5 ensures we can always match reductions to weak-head normal forms in MLTT<sub>sub</sub> with reductions to weak-head normal forms in MLTT<sub>coe</sub>. As for conversion itself, the key cases are those where the term in MLTT<sub>coe</sub> is a coercion, that gets erased in MLTT<sub>sub</sub>. Given the structure of normal forms from Figure 13, this can happen in three situations. If the coercions are between function types or record types, we do not inspect the terms, and instead eagerly η-expand in a type-directed fashion (which triggers further reduction of the now applied coercions). The third case is compacted neutrals. They can appear exactly in the places where MLTT<sub>coe</sub> uses the comparison of the compacted neutrals, which strips away the possibly present coercions, as expected. □

Finally, the main theorem states that we can elaborate terms using implicit subtyping to explicit coercions, in a type-preserving way.

**THEOREM D.5 (ELABORATION – INDUCTION).** *The following implications hold, whenever inputs to the conclusion are well-formed:*

(1) if $|\Gamma| \vdash_{\text{sub}} t' \triangleright T'$, then there exists $t$ and $T$ such that $t' = |t|$, $T' = |T|$, and $\Gamma \vdash_{\text{coe}} t \triangleright T$;

(2) if $|\Gamma| \vdash_{\text{sub}} t' \triangleright_h T'$, then there exists $t$ and $T$ such that $t' = |t|$, $T' = |T|$, and $\Gamma \vdash_{\text{coe}} t \triangleright_h T$;

(3) if $|\Gamma| \vdash_{\text{sub}} t' \triangleleft |T|$, then there exists $t$ such that $t' = |t|$ and $\Gamma \vdash_{\text{coe}} t \triangleleft T$.

**PROOF.** Once again, by mutual induction. Each rule is mapped to its counterpart, but for CHECK-SUB, where we need to insert a coercion in the elaborated term. This coercion is well-typed by Lemma 5.6. □

### D.3 Translation from MLTT<sub>coe</sub> to MLTT<sub>map</sub>

MLTT<sub>coe</sub> terms contain enough information to entirely capture the subtyping derivations. We exploit this information to define a relation $[[t]] \simeq t'$ between a MLTT<sub>coe</sub> term $t$ and a MLTT<sub>map</sub> term $t'$, that makes explicit the functorial nature of coercions. The definition of $[[t]] \simeq t'$ employs an auxiliary relation $[[A \rightsquigarrow B]] \simeq x$ to translate coercions from $A$ to $B$, where $x$ is either the special value $\star$ or a MLTT<sub>map</sub> term $f$. The value $\star$ arises in the case of an identity coercion that should be erased by the translation. In order to translate records, we assume that we have access to an (effective, decidable) total order on the countable set Lbl of labels, so that we can order in a canonical fashion every finite subsets $\mathcal{L} \subseteq \text{LBL}$ as $\mathcal{L} = \{l_1 < \dots < l_n\}$.

$$ \text{TSLTy} \quad \frac{[[\text{Type}_i]] \simeq \text{Type}_i}{\text{[Type}_i]]} \quad \text{TSLList} \quad \frac{[[A]] \simeq A'}{[[\text{List A}]] \simeq \text{List A'}} \quad \text{TSLPi} \quad \frac{[[A]] \simeq A'}{[[\Pi x : A.B]] \simeq \Pi x : A'.B'} $$

$$ \text{TSLSig} \quad \frac{[[A]] \simeq A' \qquad [[B]] \simeq B'}{[[\Sigma x : A.B]] \simeq \Sigma x : A'.B'} \quad \text{TSLRec} \quad \frac{\forall l \in \mathcal{L}. [[A_l]] \simeq A'_l \qquad \mathcal{L} = \{l_1 < \dots < l_n\}}{[[\{l : A_l\}]_{l \in \mathcal{L}}} \simeq \Sigma x_{l_1} : A'_{l_1} \dots A'_{l_n}} $$

$$ \text{TSLVAR} \quad \frac{[[x]] \simeq x}{[x]} \quad \text{TSLLAM} \quad \frac{[[A]] \simeq A' \qquad [[t]] \simeq t'}{[[\lambda x : A.t]] \simeq \lambda x : A'.t'} \quad \text{TSLAPP} \quad \frac{[[u]] \simeq u' \qquad [[v]] \simeq v'}{[[u v]] \simeq u' v'} $$

$$ \text{TSLPAIR} \quad \frac{[[u]] \simeq u' \qquad [[v]] \simeq v'}{[[ (u, v)]] \simeq (u', v')} \quad \text{TSLFST} \quad \frac{[[p]] \simeq p' \qquad [[\pi_1 p]] \simeq \pi_1 p'}{[\pi_1 p]} \quad \text{TSLSND} \quad \frac{[[p]] \simeq p' \qquad [[\pi_2 p]] \simeq \pi_2 p'}{[\pi_2 p]} $$

$$ \text{TSLRECTM} \quad \frac{\forall l \in \mathcal{L}. [[u_l]] \simeq u'_l \qquad \mathcal{L} = \{l_1 < \dots < l_n\}}{[[\{l := u_l\}]] \simeq (u'_1, \dots, u'_{l_n})} $$
PROOF. Lemma 5.5 ensures we can always match reductions to weak-head normal forms in MLTT<sub>sub</sub> with reductions to weak-head normal forms in MLTT<sub>coe</sub>. As for conversion itself, the key cases are those where the term in MLTT<sub>coe</sub> is a coercion, that gets erased in MLTT<sub>sub</sub>. Given the structure of normal forms from Figure 13, this can happen in three situations. If the coercions are between function types or record types, we do not inspect the terms, and instead eagerly η-expand in a type-directed fashion (which triggers further reduction of the now applied coercions). The third case is compacted neutrals. They can appear exactly in the places where MLTT<sub>coe</sub> uses the comparison of the compacted neutrals, which strips away the possibly present coercions, as expected. □

Finally, the main theorem states that we can elaborate terms using implicit subtyping to explicit
coercions, in a type-preserving way.

THEOREM 5.5 (ELABORATION – INDUCTION). *The following implications hold, whenever inputs to the conclusion are well-formed:*

(1) if $|\Gamma| \vdash_{\text{sub}} t' \succ T'$, then there exists $t$ and $T$ such that $t' = |t|$, $T' = |T|$, and $\Gamma \vdash_{\text{coe}} t \succ T$;

(2) if $|\Gamma| \vdash_{\text{sub}} t' \succ_h T'$, then there exists $t$ and $T$ such that $t' = |t|$, $T' = |T|$, and $\Gamma \vdash_{\text{coe}} t \succ_h T$;

(3) if $|\Gamma| \vdash_{\text{sub}} t' \prec |T|$, then there exists $t$ such that $t' = |t|$ and $\Gamma \vdash_{\text{coe}} t \prec T$.

PROOF. Once again, by mutual induction. Each rule is mapped to its counterpart, but for `CHECK-SUB`, where we need to insert a coercion in the elaborated term. This coercion is well-typed by Lemma 5.6. □

### D.3 Translation from MLTT<sub>coe</sub> to MLTT<sub>map</sub>

MLTT<sub>coe</sub> terms contain enough information to entirely capture the subtyping derivations. We exploit this information to define a relation $[[t]] \approx t'$ between a MLTT<sub>coe</sub> term *t* and a MLTT<sub>map</sub> term *t*', that makes explicit the functorial nature of coercions. The definition of $[[t]] \approx t'$ employs an auxiliary relation $[[A \rightsquigarrow B]] \approx x$ to translate coercions from *A* to *B*, where *x* is either the special value ⋆ or a MLTT<sub>map</sub> term *f*. The value ⋆ arises in the case of an identity coercion that should be erased by the translation. In order to translate records, we assume that we have access to an (effective, decidable) total order on the countable set Lbl of labels, so that we can order in a canonical fashion every finite subsets $\mathcal{L} \subseteq \text{LBL}$ as $\mathcal{L} = \{l_1 < \dots < l_n\}$.

$$ \text{TSLTy} \quad \frac{[[\text{Type}_i]] \approx \text{Type}_i}{[\text{Type}_i]} \qquad \text{TSLList} \quad \frac{[[A]] \approx A'}{[[\text{List A}]] \approx \text{List A'}} \qquad \text{TSLPi} \quad \frac{[[A]] \approx A'}{[\Pi x : A.B]} \frac{[[B]] \approx B'}{\Pi x : A'.B'} $$

$$ \text{TSLSig} \quad \frac{[[A]] \approx A' \qquad [[B]] \approx B'}{[\Sigma x : A.B]} \approx \Sigma x : A'.B' \qquad \text{TSLRec} \quad \frac{\forall l \in \mathcal{L}. [[A_l]] \approx A'_l}{[[\{l : A_l\}_{l \in \mathcal{L}}] \approx \Sigma x_{l_1} : A'_{l_1} \dots A'_{l_n}]} \quad \mathcal{L} = \{l_1 < \dots < l_n\} $$

$$ \text{TSLVAR} \quad \frac{[x] \approx x}{[x]} \qquad \text{TSLLAM} \quad \frac{[[A]] \approx A' \qquad [[t]] \approx t'}{[\lambda x : A.t] \approx \lambda x : A'.t'} \qquad \text{TSLAPP} \quad \frac{[[u]] \approx u' \qquad [[v]] \approx v'}{[[u v]] \approx u' v'} $$

$$ \text{TSLPAIR} \quad \frac{[[u]] \approx u' \qquad [[v]] \approx v'}{[[ (u, v) ]] \approx (u', v')} \qquad \text{TSLFST} \quad \frac{[[p]] \approx p' \qquad [\pi_1 p] \approx \pi_1 p'}{[\pi_2 p]} \qquad \text{TSLSND} \quad \frac{[[p]] \approx p' \qquad [\pi_2 p] \approx \pi_2 p'}{[\pi_1 p]} $$

$$ \text{TSLRECTM} \quad \frac{\forall l \in \mathcal{L}. [[u_l]] \approx u'_l \qquad \mathcal{L} = \{l_1 < \dots < l_n\}}{[[\{l := u_l\}] \approx (u'_1, \dots, u'_{l_n})]} $$
$$ \text{TSLPROJ} \frac{[[p]] \approx p' \quad \Gamma \vdash_{\text{coe}} p\{l : A_l\}_{l \in \mathcal{L}} \quad \mathcal{L} = \{l_1 < \dots < l_n\}}{[[p \cdot l_i]] \approx \pi_1 \circ \pi_2^{i-1}(p')} $$

$$ \text{TSLCOEID} \frac{[[A \rightsquigarrow B]] \approx \star \quad [[t]] \approx t'}{[[\text{coe}_{A,B} t]] \approx t'} $$

$$ \text{TSLCOE} \frac{[[A \rightsquigarrow B]] \approx f \quad [[t]] \approx t'}{[[\text{coe}_{A,B} t]] \approx f t'} $$

$$ \text{TSLCOENF} \frac{A \rightsquigarrow A' \ \text{nf} \quad B \rightsquigarrow B' \ \text{nf} \quad [[A' \rightsquigarrow B')] \approx x \quad A \neq A' \ \text{or} \ B \neq B'}{[[A \rightsquigarrow B]] \approx x} $$

$$ \text{TSLCOEListID} \frac{[[A \rightsquigarrow B]] \approx \star}{[[\text{List } A \rightsquigarrow \text{List } B]] \approx \star} $$

$$ \text{TSLCOEList} \frac{[[A \rightsquigarrow B]] \approx f}{[[\text{List } A \rightsquigarrow \text{List } B]] \approx \text{map}_{\text{List}} f} $$

$$ \text{TSLCOEPIIDBOTH} \frac{[[A_2 \rightsquigarrow A_1]] \approx \star \quad [[B_1 \rightsquigarrow B_2]] \approx \star}{[[\Pi x : A_1.B_1 \rightsquigarrow \Pi x : A_2.B_2]] \approx \star} $$

$$ \text{TSLCOEPIIDDOM} \frac{[[A_2 \rightsquigarrow A_1]] \approx \star \quad [[B_1 \rightsquigarrow B_2]] \approx g \quad [[A_1]] \approx A'_1}{[[\Pi x : A_1.B_1 \rightsquigarrow \Pi x : A_2.B_2]] \approx \text{map}_{\Pi}(\text{id}_{A'_1}, g)} $$

$$ \text{TSLCOEPIIDCOD} \frac{[[A_2 \rightsquigarrow A_1]] \approx f \quad [[B_1 [\text{coe}_{A_2,A_1} x] \rightsquigarrow B_2]] \approx \star \quad [[B_2]] \approx B'_2}{[[\Pi x : A_1.B_1 \rightsquigarrow \Pi x : A_2.B_2]] \approx \text{map}_{\Pi}(f, \text{id}_{B'_2})} $$

$$ \text{TSLCOEPI} \frac{[[A_2 \rightsquigarrow A_1]] \approx f \quad [[B_1 [\text{coe}_{A_2,A_1} x] \rightsquigarrow B_2]] \approx g}{[[\Pi x : A_1.B_1 \rightsquigarrow \Pi x : A_2.B_2]] \approx \text{map}_{\Pi}(f,g)} \quad \text{and similarly for } \Sigma $$

$$ \text{TSLCOEREID} \frac{\mathcal{K} = \mathcal{L} \quad \forall k \in \mathcal{K}. [[A_k \rightsquigarrow B_k]] \approx \star}{[[\{l : A_l\}_{l \in \mathcal{L}} \rightsquigarrow \{k : B_k\}_{k \in \mathcal{K}}]] \approx \star} $$

$$ \text{TSLCOEREC} \frac{\mathcal{K} \subseteq \mathcal{L} \quad \forall k \in \mathcal{K}. [[A_k \rightsquigarrow B_k]] \approx f_k \quad \mathcal{K} = \{k_1 < \dots < k_n\}}{[[\{l : A_l\}_{l \in \mathcal{L}} \rightsquigarrow \{k : B_k\}_{k \in \mathcal{K}}]] \approx \lambda p. (f_{k_1}(\pi_1 p), \dots, f_{k_n}(\pi_2^{n-1} p))} $$

$$ \text{TSLCOETY} \quad [[\text{Type}_i \rightsquigarrow \text{Type}_i]] \approx \star \qquad \text{TSLCOENE} \quad \frac{\text{ne } N}{[[N \rightsquigarrow M]] \approx \star} $$

The translation is extended to contexts pointwise.

$$ \overline{[[\cdot]]} \approx \cdot \qquad \frac{[[\Gamma]] \approx \Gamma' \quad [[A]] \approx A'}{[[\Gamma, x : A]] \approx \Gamma', x : A'} $$

We note $[[t]] \downarrow$ when $t$ is in the domain of the relation and $[[t]]$ for the image of $t$ when it is defined.

**LEMMA D.6 (DETERMINISM OF TRANSLATION).** The translation relation $[[t]] \approx t'$ is a partial function, i.e. it is deterministic: for any $t, t'_1, t'_2$, if $[[t]] \approx t'_1$ and $[[t]] \approx t'_2$ then $t'_1 = t'_2$.

**PROOF.** We show by mutual induction on a derivation that $[[A \rightsquigarrow B]] \approx x$ is a partial function as well from pairs of MLTT<sub>coe</sub> types to either ⋆ or a MLTT<sub>map</sub> term. In the key case TSLCOENF, note that the reduction relation ⋆<sup>⋆</sup> is deterministic as well, so we can conclude by induction hypothesis. All other cases are immediate or simple applications of the inductive hypothesis, using the fact that at each step, at most one rule apply. □
$$ \text{TSLPROJ} \frac{[[p]] \approx p' \quad \Gamma \vdash_{\text{coe}} p\{l : A_l\}_{l \in \mathcal{L}} \quad \mathcal{L} = \{l_1 < \dots < l_n\}}{[[p.l_i]] \approx \pi_1 \circ \pi_2^{i-1}(p')} $$

$$ \text{TSLCOEID} \frac{[[A \rightsquigarrow B]] \approx \star \quad [[t]] \approx t'}{[[\text{coe}_{A,B} t]] \approx t'} $$

$$ \text{TSLCOE} \frac{[[A \rightsquigarrow B]] \approx f \quad [[t]] \approx t'}{[[\text{coe}_{A,B} t]] \approx f t'} $$

$$ \text{TSLCOENF} \frac{A \rightsquigarrow A' \ \text{nf} \quad B \rightsquigarrow B' \ \text{nf} \quad [[A' \rightsquigarrow B'] \approx x \quad A \neq A' \text{ or } B \neq B']}{[[A \rightsquigarrow B] \approx x} $$

$$ \text{TSLCOEListID} \frac{[[A \rightsquigarrow B]] \approx \star}{[[\text{List } A \rightsquigarrow \text{List } B]] \approx \star} $$

$$ \text{TSLCOEList} \frac{[[A \rightsquigarrow B]] \approx f}{[[\text{List } A \rightsquigarrow \text{List } B]] \approx \text{map}_{\text{List}} f} $$

$$ \text{TSLCOEPIIDBOTH} \frac{[[A_2 \rightsquigarrow A_1]] \approx \star \quad [[B_1 \rightsquigarrow B_2]] \approx \star}{[[\Pi x : A_1.B_1 \rightsquigarrow \Pi x : A_2.B_2]] \approx \star} $$

$$ \text{TSLCOEPIIDDOM} \frac{[[A_2 \rightsquigarrow A_1]] \approx \star \quad [[B_1 \rightsquigarrow B_2]] \approx g \quad [[A_1]] \approx A'_1}{[[\Pi x : A_1.B_1 \rightsquigarrow \Pi x : A_2.B_2]] \approx \text{map}_{\Pi}(\text{id}_{A'_1}, g)} $$

$$ \text{TSLCOEPIIDCOD} \frac{[[A_2 \rightsquigarrow A_1]] \approx f \quad [[B_1 [\text{coe}_{A_2,A_1} x] \rightsquigarrow B_2]] \approx \star \quad [[B_2]] \approx B'_2}{[[\Pi x : A_1.B_1 \rightsquigarrow \Pi x : A_2.B_2]] \approx \text{map}_{\Pi}(f, \text{id}_{B'_2})} $$

$$ \text{TSLCOEPI} \frac{[[A_2 \rightsquigarrow A_1]] \approx f \quad [[B_1 [\text{coe}_{A_2,A_1} x] \rightsquigarrow B_2]] \approx g}{[[\Pi x : A_1.B_1 \rightsquigarrow \Pi x : A_2.B_2]] \approx \text{map}_{\Pi}(f,g)} \quad \text{and similarly for } \Sigma $$

$$ \text{TSLCOEREID} \frac{\mathcal{K} = \mathcal{L} \quad \forall k \in \mathcal{K}. [[A_k \rightsquigarrow B_k]] \approx \star}{[[\{l : A_l\}_{l \in \mathcal{L}} \rightsquigarrow \{k : B_k\}_{k \in \mathcal{K}}]] \approx \star} $$

$$ \text{TSLCOEREC} \frac{\mathcal{K} \subseteq \mathcal{L} \quad \forall k \in \mathcal{K}. [[A_k \rightsquigarrow B_k]] \approx f_k \quad \mathcal{K} = \{k_1 < \dots < k_n\}}{[[\{l : A_l\}_{l \in \mathcal{L}} \rightsquigarrow \{k : B_k\}_{k \in \mathcal{K}}]] \approx \lambda p. (f_{k_1}(\pi_1 p), \dots, f_{k_n}(\pi_2^{n-1} p))} $$

$$ \text{TSLCOETY} \quad [[\text{Type}_i \rightsquigarrow \text{Type}_i]] \approx \star \qquad \text{TSLCOENE} \quad \frac{\text{ne } N}{[[N \rightsquigarrow M]] \approx \star} $$

The translation is extended to contexts pointwise.

$$ \overline{[[\cdot]]} \approx \cdot \qquad \frac{[[\Gamma]] \approx \Gamma' \quad [[A]] \approx A'}{[[\Gamma, x : A]] \approx \Gamma', x : A'} $$

We note $[[t]] \downarrow$ when $t$ is in the domain of the relation and $[[t]]$ for the image of $t$ when it is defined.

**LEMMA D.6 (DETERMINISM OF TRANSLATION).** The translation relation $[[t]] \approx t'$ is a partial function, i.e. it is deterministic: for any $t, t'_1, t'_2$, if $[[t]] \approx t'_1$ and $[[t]] \approx t'_2$ then $t'_1 = t'_2$.

**PROOF.** We show by mutual induction on a derivation that $[[A \rightsquigarrow B]] \approx x$ is a partial function as well from pairs of $\text{MLTT}_{\text{coe}}$ types to either $\star$ or a $\text{MLTT}_{\text{map}}$ term. In the key case $\text{TSLCOENF}$, note that the reduction relation $\rightsquigarrow^*$ is deterministic as well, so we can conclude by induction hypothesis. All other cases are immediate or simple applications of the inductive hypothesis, using the fact that at each step, at most one rule apply. $\square$
**LEMMA D.7 (STABILITY OF TRANSLATION BY WEAKENING).** If $\rho$ is a substitution that maps variables to variables then $[[t]][\rho] = [[t[\rho]]]$.

**PROOF.** Immediate by induction on $t$, the only case interesting case being the translation of variables, with a similar lemma for $[[A \rightsquigarrow B]] \simeq x$ using that neutrals are preserved. $\square$

**LEMMA D.8 (WELL-TYPED TERMS TRANSLATE).** If $\Gamma \vdash_{\text{coe}} t : A$ then $[[\Gamma]]\downarrow, [[A]]\downarrow$ and $[[t]]\downarrow$.

**PROOF.** We prove by a straightforward mutual induction on an algorithmic typing derivation that:

* If $\vdash_{\text{coe}} \Gamma$ then $[[\Gamma]]\downarrow$;

* If $\Gamma \vdash_{\text{coe}} A \triangleleft$ and $[[\Gamma]]\downarrow$ then $[[A]]\downarrow$;

* If $\Gamma \vdash_{\text{coe}} t \triangleleft A$ and $[[\Gamma]]\downarrow$ then $[[t]]\downarrow$;

* If $\Gamma \vdash_{\text{coe}} t \triangleright A$ and $[[\Gamma]]\downarrow$ then $[[t]]\downarrow$;

* If $\Gamma \vdash_{\text{coe}} A \preceq B \triangleleft$ or $\Gamma \vdash_{\text{coe}} A \preceq_h B \triangleleft$ then there exists $x$ such that $[[A \rightsquigarrow B]] \simeq x$. $\square$

**LEMMA D.9 (IDENTITY COERCIONS).** If $\Gamma \vdash_{\text{coe}} A \cong B \triangleleft$ or $\Gamma \vdash_{\text{coe}} A \cong_h B \triangleleft$ then $[[A \rightsquigarrow B]] \simeq \star$. $\square$

**PROOF.** Straightforward mutual induction on the bidirectional conversion derivation. $\square$

**LEMMA D.10 (STABILITY OF TRANSLATION BY SUBSTITUTION).** If $\Gamma \vdash_{\text{coe}} t : A$ and $\Delta \vdash_{\text{coe}} \sigma : \Gamma$ then $[[t]][[\sigma]] = [[t[\sigma]]]$ and similarly for typing.

If $\Gamma \vdash_{\text{coe}} A \preceq B \triangleleft$, $\Delta \vdash_{\text{coe}} \sigma : \Gamma$ and

* $[[A \rightsquigarrow B]] \simeq \star$ then $[[A[\sigma] \rightsquigarrow B[\sigma]]] \simeq \star$;

* $[[A \rightsquigarrow B]] \simeq f$ then $[[A[\sigma] \rightsquigarrow B[\sigma]]] \simeq f[\sigma]$.

**PROOF.** Straightforward mutual induction on the bidirectional derivation. $\square$

**Forward simulation.** Following the proof strategy employed for the equivalence between subsumptive and coercive subtyping, the next step would require to prove that the translation is a forward simulate, i.e. if $\Gamma \vdash_{\text{coe}} t : A$ and $t \rightsquigarrow^1 t'$ then $[[t]] \rightsquigarrow^* [[t')]$. As stated, this lemma does not hold. Indeed, the rule COECOE leads to reductions of coercions with type annotations which may be convertible but not reduce correctly. We conjecture that a weaker version of the simulation with respect to conversion in MLTT$_{map}$ should hold, that is if $\Gamma \vdash_{\text{coe}} t : A$ and $t \rightsquigarrow^1 t'$ then $[[\Gamma]] \vdash_{\text{map}} [[t]] \cong [[t')] : [[A]]$. Such statement should be proved mutually with other properties stating that the translation preserves typing, as follows.

**CONJECTURE D.11 (TRANSLATION PRESERVES TYPING).**

(1) If $\vdash_{\text{coe}} \Gamma$ then $\vdash_{\text{map}} [[\Gamma]]$

(2) If $\Gamma \vdash_{\text{coe}} A$ then $\Gamma \vdash_{\text{map}} [[A]]$

(3) If $\Gamma \vdash_{\text{coe}} t : A$ then $\Gamma \vdash_{\text{map}} [[t]] : [[A]]$

(4) If $\Gamma \vdash_{\text{coe}} A \cong B$ then $\Gamma \vdash_{\text{map}} [[A]] \cong [[B]]$

(5) If $\Gamma \vdash_{\text{coe}} t \cong u : A$ then $\Gamma \vdash_{\text{map}} [[t]] \cong [[u]] : [[A]]$

(6) If $\Gamma \vdash_{\text{coe}} A \preceq B$ then either

(a) $[[A \rightsquigarrow B]] \simeq \star$ and $[[\Gamma]] \vdash_{\text{map}} [[A]] \cong [[B]]$

(b) $[[A \rightsquigarrow B]] \simeq f$ and $[[\Gamma]] \vdash_{\text{map}} f : [[A]] \to [[B]]$

Preservation of typing, together with catch up lemmas, and a backward simulation lemma, would then allow to lift bidirectional conversion derivations in MLTT$_{map}$ between the translation of terms from MLTT$_{coe}$. The use of bidirectional conversion is essential here to remain at each step within the translation of MLTT$_{coe}$ terms.