Abstract: The Hahn-Banach Theorem in Type Theory
Jan Cederquist, Thierry Coquand, Sara Negri
We give the basic definitions for pointfree functional analysis and
present constructive proofs of the Alaoglu and Hahn-Banach theorems
in the setting of formal topology.
Back to Sara's homepage.