* homotopy/BlakersMassey.agda: Added file
Fixed assumptions to BM.