Computing spaces in type theory

<p>In this thesis, we develop multiple case studies computing with and in cubical type theory.</p> <p>We begin by setting up a framework to compute with sets in the theorem prover Cubical Agda. Using the example of the powerset, we show how both mathematical <em>definitions&...