Authors: Maria Emilia Maietti, Silvio Valentini
Title: Relative formal topology
Abstract:
The concept of formal topology introduced by P. Martin-Lof
and G. Sambin to deal with topology in a constructive way, that is in
intuitionistic type theory, is based on a binary cover relation and a
positivity predicate.
To deal predicatively with closed subsets of a topological space,
G. Sambin extended formal topology with a binary positivity predicate.
In this talk we consider formal topology with a
binary positivity predicate furtherly extended with an indexed cover,
called "relative formal topology", in order to
represent the topology induced on a closed subset and we connect the
corresponding category with that of topological spaces and that of
formal topologies via categorical adjunctions.