Altenkirch, Thorsten
[VerfasserIn];
Kaposi, Ambrus
[VerfasserIn];
Šinkarovs, Artjoms
[VerfasserIn];
Végh, Tamás
[VerfasserIn]
;
Thorsten Altenkirch and Ambrus Kaposi and Artjoms Šinkarovs and Tamás Végh
[MitwirkendeR]
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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.