The exp-log normal form of types: decomposing extensional equality and representing terms compactly