Added some properties of transporting along identity types.
Added equational reasoning combinators.
Renamed _=⟨_⟩_ to _≡⟨_⟩_.
Proved some properties of ap.
Showed that using the wrong definition of propositional truncation, one can show that the "truncation" of the unit type is equivalent to the circle.