{-# 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