universe-dependent-sum-1.2: Universe instances for types from dependent-sum