------------------------------------------------------------------------ -- The delay monad quotiented by weak bisimilarity ------------------------------------------------------------------------ {-# OPTIONS --without-K #-} module Partiality-monad.Coinductive where open import Equality.Propositional open import H-level.Truncation.Propositional open import Prelude hiding (⊥) open import Quotient.HIT open import H-level equality-with-J open import Delay-monad open import Delay-monad.Weak-bisimilarity -- The partiality monad, defined as the delay monad quotiented by -- (propositionally truncated) weak bisimilarity. _⊥ : ∀ {a} → Set a → Set a A ⊥ = Delay A ∞ / λ x y → ∥ x ≈ y ∥ , truncation-is-proposition -- The partiality monad is a set. ⊥-is-set : ∀ {a} {A : Set a} → Is-set (A ⊥) ⊥-is-set = /-is-set