2026-07-24T02:23:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18453 2024-03-06T11:01:52Z ddc:004 open_access

The Münchhausen Method in Type Theory Altenkirch, Thorsten Kaposi, Ambrus Šinkarovs, Artjoms Végh, Tamás type theory proof assistants very dependent types 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thorsten Altenkirch and Ambrus Kaposi and Artjoms Šinkarovs and Tamás Végh 2023 Is Part Of LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2022.10 urn:nbn:de:0030-drops-184534 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.10 eng https://creativecommons.org/licenses/by/4.0/legalcode