Set-theoretic paradoxes have made all-inclusive self-referential
Foundational Theories almost a taboo. The few daring attempts
in the literature to break this taboo avoid paradoxes by restricting the
class of formul allowed in Cantor's nave Comprehension Principle. 
A different, more intensional approach was taken by Fitch, reformulated by
Prawitz, by restricting, instead, the shape of deductions, namely allowing
only normal(izable) deductions. The resulting theory is quite powerful,
and consistent by design. However, modus ponens and Scotus ex contradictione
quodlibet principles fail. We discuss Fitch-Prawitz Set Theory (FP) and implement 
it in a Logical Framework with so-called locked types, thereby providing a 
“Computer-assisted Cantor's Paradise": an interactive framework that, unlike the 
familiar Coq and Agda, is closer to the familiar informal way of doing mathematics 
by delaying and consolidating the required normality tests.We prove a Fixed Point 
Theorem, whereby all partial recursive functions are definable in FP. We establish 
an intriguing connection between an extension of FP and the Theory of Hyperuniverses: 
the bisimilarity quotient of the coalgebra of closed terms of FP satisfies the Comprehension Principle for Hyperuniverses.
Keywords: Fitch-Prawitz set theory, logical frameworks, paradoxes, coalgebras, hyperuniverses