What do you mean by "Types are Spaces"? [00D5]

TODO: Look at models, specifically simplicial sets.