Intersections of compactly many open sets are open - Martín Hötzel Escardó (2020)