{-# OPTIONS --safe #-}

module DepthComonads.Prelude where

open import DepthComonads.Level public
open import DepthComonads.Nat using (ℕ; suc; zero) public
open import DepthComonads.Function public
open import DepthComonads.Bool public
open import DepthComonads.Path public
open import DepthComonads.Function.Isomorphism public
open import DepthComonads.Empty public
open import DepthComonads.HLevels public
open import DepthComonads.Sigma public
open import DepthComonads.Path.Reasoning public
open import DepthComonads.Unit public
open import DepthComonads.Dec public
open import DepthComonads.Discrete public
open import DepthComonads.Sum public
open import DepthComonads.WellFounded public
open import DepthComonads.Instance public
open import DepthComonads.List public
open import DepthComonads.Maybe public