Orthogonal factorization in HoTT - Egbert Rijke