feat(library/hott) postcomposition from ua lemma is done up to the last gap
chore(library/hott) fix universe issue. note: this should be fixed when contr is not bound to universe level 1 anymore