Reconcile with upstream Displayed Reasoning changes

[hejohns]

wip for #110

[hejohns]

hejohns@agda:~/multi-poly-cats$ git checkout 0762db3cc731df45a83584c28494375047e12d41
...
HEAD is now at 0762db3 Section upstream (#107)
hejohns@agda:~/multi-poly-cats$ (cd ../cubical && git checkout f3d8889726ec5e75ed638679c6ed33546181a20c)
...
HEAD is now at f3d88897 Minor fix: improved definition of whitehead products (#1155)
hejohns@agda:~/multi-poly-cats$ make clean
find . -name "*.agdai" -type f -delete
rm Everything.agda
hejohns@agda:~/multi-poly-cats$ time make
...
real	        8m20.309s
user        8m8.463s
sys	        0m12.858s

hejohns@agda:~/multi-poly-cats$ git checkout 80827f1eab7ad9514a68d357f1197324308a29b4
Previous HEAD position was 0762db3 Section upstream (#107)
HEAD is now at 80827f1 fix line lengths
hejohns@agda:~/multi-poly-cats$ (cd ../cubical && git checkout 581748b01bc43a25295993347bdc8c7cb2166090)
Previous HEAD position was f3d88897 Minor fix: improved definition of whitehead products (#1155)
HEAD is now at 581748b0 Rework displayed category reasoning. (#1153)
hejohns@agda:~/multi-poly-cats$ make clean
...
hejohns@agda:~/multi-poly-cats$ time make
...
real	        8m20.461s
user        8m8.912s
sys	        0m12.624s