Eine topologische Lesart von induktiven und koinduktiven Definitionen in der abhängigen Typentheorie

Im Kontext der abhängigen Typentheorie zeigen wir, dass koinduktive Prädikate einen äquivalenten topologischen Gegenpart in Form von koinduktiv erzeugten Positivitätsrelationen haben, die von G. Sambin eingeführt wurden, um geschlossene Teilmengen in der punktfreien Topologie darzustellen. Unsere Arbeit ergänzt eine vorherige mit M.E. Maietti, in der wir zeigten, dass das bekannte Konzept der wohlgeordneten Bäume in der abhängigen Typentheorie einen topologischen äquivalenten Gegenpart in Form von beweisrelevanten induktiv erzeugten formalen Überdeckungen hat, die verwendet werden, um eine prädikative und konstruktive Darstellung vollständiger Supplattice zu bieten. Alle Beweise in Martin-Löf's Typentheorie sind im Agda-Beweisassistenten formalisiert.