Belangrijkste concepten
Die Arbeit zeigt, dass koinduktive Prädikate ein topologisches Äquivalent in Form von koinduktiv erzeugten Positivitätsrelationen haben, die von G. Sambin eingeführt wurden, um abgeschlossene Teilmengen in punktfreier Topologie darzustellen.
Samenvatting
Die Arbeit besteht aus folgenden Hauptteilen:
- Einführung in (Ko)Induktion in der Minimalistischen Grundlegung:
- Formalisierung von (Ko)Induktiven Prädikaten als kleinste geschlossene bzw. größte konsistente Prädikate bezüglich gewisser Ableitungs- und Widerlegungsoperatoren.
- Äquivalenz dieser (Ko)Induktiven Prädikate mit (Ko)Induktiv erzeugten Topologien (Basisüberdeckungen und Positivitätsrelationen).
- Übertragung der Ergebnisse in die Typentheorie von Martin-Löf:
- Darstellung von (Ko)Induktiven Prädikaten als spezielle W-Typen bzw. M-Typen.
- Kategorientheoretische Interpretation der Konstruktoren als initiale Algebren abhängiger polynomialer Endofunktoren.
Die Arbeit zeigt somit eine topologische Sichtweise auf (Ko)Induktion in abhängigen Typentheorien auf und verbindet diese mit etablierten Konzepten wie W-Typen und M-Typen.
Statistieken
(∀x ∈A)(x ε V ∨(∃y ∈I(x))(∀z ε C(x, y))P(z) ⇒P(x)) true
(∀x ∈A)(P(x) ⇒x ε V ∧(∀y ∈I(x))(∃z ε C(x, y))P(z)) true
Citaten
"In the context of dependent type theory, we show that coinductive predicates have an equivalent topological counterpart in terms of coinductively generated positivity relations, introduced by G. Sambin to represent closed subsets in point-free topology."
"Our work is complementary to a previous one with M.E. Maietti, where we showed that, in dependent type theory, the well-known concept of wellfounded trees has a topological equivalent counterpart in terms of proof-relevant inductively generated formal covers used to provide a predicative and constructive representation of complete suplattices."