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.