{-# OPTIONS --cubical --safe #-}

module DepthComonads.HLevels where

open import DepthComonads.Path
open import Cubical.Foundations.Everything
  using (isProp
        ;isSet
        ;isContr
        ;isPropIsContr
        ;isProp→isSet
        ;isOfHLevel→isOfHLevelDep
        ;hProp
        ;isSetHProp
        ;isPropIsProp
        ;hSet
        ;isProp×
        )
  public

open import DepthComonads.Empty
open import DepthComonads.Level

isProp¬ : isProp (A → ⊥)
isProp¬ x y = funExt λ p → ⊥-elim (x p)