Homotopy Type Theory compact connected space > history (Rev #4)

Definition

A compact connected space is a space $S$ such that for subspaces $A \subseteq S$ and $B \subseteq S$ of $S$ with canonical monic mappings $i_{A,S}:A \to S$ and $i_{B,S}:B \to S$ such that the canonical monic mapping $i_{A \cup B,S}:A \cup B \to S$ is an equivalence and the canonical monic mapping $i_{\emptyset,A \cap B}:\emptyset \to A \cap B$ is an equivalence, either $i_{A,S}$ is an equivalence or $i_{B,S}$ is an equivalence.

References

• Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)