유니버스는 의존 타입 이론의 핵심이며, 정확하면서도 사용하기 쉬운 방식으로 다루기가 매우 어렵습니다. 우리는 다형적인 누적 유니버스에 대한 새로운 'fuss-free' 일반 대수적 표현을 제안합니다. 이는 복잡한 코히런트 유니버스 강제 변환(coherent universe coercions) 이론 대신 더 간단한 공식화를 사용하며, 우리는 이 둘이 동등함을 전자의 정규화 정리(normalisation theorem)를 통해 증명합니다. fuss-free 공식화의 유용성에 대한 증거는 (1) 양방향 상세화 알고리즘(bidirectional elaboration algorithm)에 대한 추상적인 명세와 (2) Haskell을 사용한 구체적인 구현 형태로 제공됩니다. 또한 우리는 fuss-free 유니버스 계층 구조를 데이터 타입 설명에 대한 판단적 개념(judgemental notion of datatype description)으로 확장하고 이를 구현하며, 이로부터 이전의 누적 귀납 타입(cumulative inductive type) 개념을 도출할 수 있습니다.