https://sites.google.com/view/tetsuyasato/
This is an unofficial reimagining of the Archive of Formal Proofs
Quasi-Borel Spacesby Michikazu Hirata, Yasuhiko Minamide and Tetsuya Sato