Type theory and mathematical logic explorations. Is there a type theory for 𝕠𝕡? HoTT III: Sets and Logic HoTT II: The essentials HoTT I: The type theory An inquiry into the Foundations of Mathematics ZFC and propositional logic