Closed MatthiasHu closed 8 months ago
(with Max Zeuner)
Superseded by https://github.com/agda/cubical/pull/1082.
(with Max Zeuner)