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

{-# OPTIONS --without-K --safe #-}

open import Algebra

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

open import Level using (Lift; lift; _⊔_)
open import Category.Functor using (RawFunctor)
open import Category.Monad using (RawMonad)
open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Function
import Function.Identity.Categorical 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.Categorical.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

  open RawMonad monad

  -- Now, let's show that "return" 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).
  returnUnitL : ∀ {x : B} {f : Lift a B → A.Carrier × Lift a B} →
                ((return (lift x)) >>= f) ≈ f (lift x)
  returnUnitL = A.identityˡ _ , refl

  returnUnitR : {x : A.Carrier × Lift a B} → (x >>= return) ≈ x
  returnUnitR = 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