The Münchhausen Method in Type Theory

Altenkirch, Thorsten; Kaposi, Ambrus; Šinkarovs, Artjoms; Végh, Tamás

Abstract

In one of his long tales, after falling into a swamp, Baron Münchhausen salvaged himself and the horse by lifting them both up by his hair. Inspired by this, the paper presents a technique to justify very dependent types. Such types reference the term that they classify, e.g. x : F x. While in most type theories this is not allowed, we propose a technique on salvaging the meaning of both the term and the type. The proposed technique does not refer to preterms or typing relations and works in a completely algebraic setting, e.g categories with families. With a series of examples we demonstrate our technique. We use Agda to demonstrate that our examples are implementable within a proof assistant.

Citation

Altenkirch, T., Kaposi, A., Šinkarovs, A., & Végh, T. (2023). The Münchhausen Method in Type Theory. LIPIcs, 269, https://doi.org/10.4230/LIPIcs.TYPES.2022.10

• Journal Article Type: Article
• Conference Name: th International Conference on Types for Proofs and Programs (TYPES 2022)
• Acceptance Date: May 22, 2023
• Online Publication Date: Jul 28, 2023
• Publication Date: 2023
• Deposit Date: Jun 8, 2023
• Publicly Available Date: Jul 28, 2023
• Journal: LIPIcs
• Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
• Peer Reviewed: Peer Reviewed
• Volume: 269
• ISBN: 9783959772853
• DOI: https://doi.org/10.4230/LIPIcs.TYPES.2022.10
• Public URL: https://nottingham-repository.worktribe.com/output/21641275
• Publisher URL: https://drops.dagstuhl.de/opus/volltexte/2023/18453/