```------------------------------------------------------------------------
-- The Agda standard library
--
-- Universe-sensitive functor and monad instances for the Product type.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra

module Data.Product.Effectful.Examples
{a e b} {A : Monoid a e} {B : Set b} where

open import Level using (Lift; lift; _⊔_)
open import Effect.Functor using (RawFunctor)
open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Function
import Function.Identity.Effectful as Id
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

------------------------------------------------------------------------
-- Examples

-- Note that these examples are simple unit tests, because the type
-- checker verifies them.

private

module A = Monoid A

open import Data.Product.Effectful.Left A.rawMonoid b

_≈_ : Rel (A.Carrier × Lift a B) (e ⊔ a ⊔ b)
_≈_ = Pointwise A._≈_ _≡_

open RawFunctor functor

-- This type to the right of × needs to be a "lifted" version of (B : Set b)
-- that lives in the universe (Set (a ⊔ b)).
fmapIdₗ : (x : A.Carrier × Lift a B) → (id <\$> x) ≈ x
fmapIdₗ x = A.refl , refl

-- Now, let's show that "pure" is a unit for >>=. We use Lift in exactly
-- the same way as above. The data (x : B) then needs to be "lifted" to
-- this new type (Lift B).
pureUnitL : ∀ {x : B} {f : Lift a B → A.Carrier × Lift a B} →
(pure (lift x) >>= f) ≈ f (lift x)
pureUnitL = A.identityˡ _ , refl

pureUnitR : {x : A.Carrier × Lift a B} → (x >>= pure) ≈ x
pureUnitR = A.identityʳ _ , refl

-- And another (limited version of a) monad law...
bindCompose : ∀ {f g : Lift a B → A.Carrier × Lift a B} →
{x : A.Carrier × Lift a B} →
((x >>= f) >>= g) ≈ (x >>= (λ y → (f y >>= g)))
bindCompose = A.assoc _ _ _ , refl
```