{-# OPTIONS --cubical --safe --postfix-projections #-}

module DepthComonads.Function.Isomorphism where

open import Cubical.Foundations.Isomorphism using (Iso; section; retract; isoToPath; iso; isoToEquiv) public
open import DepthComonads.Level
open import DepthComonads.Path

open Iso public

infix 4 _⇔_
_⇔_ = Iso