Ali, many thanks for your comments which are very instructive. Actually I
am trying to understand anything in the Floris van Doorn's thesis,
particularly the formalization in HoTT for the
Atiyah-Hirzebruch spectral sequence and the Leray-Serre spectral sequence.