ここ最近、グロタンディーク宇宙の話をしています。 贅沢主義者のグロタンディーク宇宙 (7月20日) 型・インスタンス・宇宙とタルスキ宇宙系列 (7月22日) 贅沢なグロタンディーク宇宙とPropositions-As-Types (7月24日) ZF宇宙、グロタンディーク宇宙、型宇宙…