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