Proved stuff about creating a new type out of a retraction that is isomorphic to the one we are retracting into.
Proved minor thing about retractions and isomorphisms.
Rearranged file.
Finished part on non-isomorphic views.