{-# OPTIONS --safe #-}
module HLevels where
open import Cubical.Foundations.HLevels using
(isSetΠ; isProp→; isSet×; isPropΠ; isPropΣ; isSetΣ; isOfHLevel→isOfHLevelDep; isProp×; isOfHLevel)
public
open import Cubical.Foundations.Prelude using
(isProp; isSet; isProp→isSet)
public