{-# OPTIONS --without-K --safe #-}
module Data.Sum.Categorical.Examples where
open import Level
open import Data.Sum.Base
import Data.Sum.Categorical.Left as Sumₗ
open import Category.Functor
open import Category.Monad
private
module Examplesₗ {a b} {A : Set a} {B : Set b} where
open import Agda.Builtin.Equality
open import Function
module Sₗ = Sumₗ A b
open RawFunctor Sₗ.functor
fmapId : (x : A ⊎ (Lift a B)) → (id <$> x) ≡ x
fmapId (inj₁ x) = refl
fmapId (inj₂ y) = refl
open RawMonad Sₗ.monad
returnUnitL : ∀ {x : B} {f : Lift a B → A ⊎ (Lift a B)}
→ ((return (lift x)) >>= f) ≡ f (lift x)
returnUnitL = refl
returnUnitR : (x : A ⊎ (Lift a B)) → (x >>= return) ≡ x
returnUnitR (inj₁ _) = refl
returnUnitR (inj₂ _) = refl
bindCompose : ∀ {f g : Lift a B → A ⊎ (Lift a B)}
→ (x : A ⊎ (Lift a B))
→ ((x >>= f) >>= g) ≡ (x >>= (λ y → (f y >>= g)))
bindCompose (inj₁ x) = refl
bindCompose (inj₂ y) = refl