{-# OPTIONS --guardedness-preserving-type-constructors #-} module TypeConstructorsWhichPreserveGuardedness4 where open import Common.Coinduction data Rec (A : ∞ Set) : Set where fold : ♭ A → Rec A D : Set D = Rec (♯ (D → D)) _·_ : D → D → D fold f · x = f x ω : D ω = fold (λ x → x · x) Ω : D Ω = ω · ω