Rearrange dependencies

Now function.isomorphism.properties can depend on function.fibration.
Simplify proof of iso≡
Abstract out proof of family iso via display map