ULC.Domains module ULC.Domains where open import Function using (Inverse; _↔_) public open Inverse {{ ... }} using (to; from) public postulate D∞ : Set postulate instance iso : D∞ ↔ (D∞ → D∞) variable d : D∞