180KiB, 826x575, FoxitReader_6xQyJCAfim.png View SameGoogleiqdbSauceNAO Anonymous Wed 15 Sep 15:40:27 2021 No.13643842 ViewReplyOriginalReport Quoted By: How would you formalize this homotopy equivalence in something like Lean?