[Agda] Simple monoid instance based on monoid instance of underlying type

[James ‘Twey’ Kay]

In Agda you also have to lift the laws into your new type.  Unless 
you're willing to go into HoTT, as far as I can tell you need to lift it 
manually:


```

module Identity where

open import Relation.Binary.PropositionalEquality
   using (_≡_; cong; cong₂; isEquivalence)
open import Algebra using (Monoid)
open import Level using (zero; suc)
open import Algebra.Structures using (IsSemigroup; IsMonoid)
open import Algebra.FunctionProperties using (Op₂; Associative)
open import Data.Product using (_,_; proj₁; proj₂)
open import Function using (_∘_)

record Id {ℓ} (A : Set ℓ) : Set (suc ℓ) where
   constructor I
   field
     unI : A

lift-Op₂ : ∀ {ℓ} {A : Set ℓ} → Op₂ A → Op₂ (Id A)
lift-Op₂ _∙_ a b = I (Id.unI a ∙ Id.unI b)

lift-Associative : ∀ {ℓ} {A : Set ℓ} {∙ : Op₂ A}
   → Associative _≡_ ∙ → Associative _≡_ (lift-Op₂ ∙)
lift-Associative a∙ =
   λ x y z → cong I (a∙ (Id.unI x) (Id.unI y) (Id.unI z))

lift-IsSemigroup : ∀ {ℓ} {A : Set ℓ} {∙ : Op₂ A}
   → IsSemigroup _≡_ ∙ → IsSemigroup _≡_ (lift-Op₂ ∙)
lift-IsSemigroup {∙ = _∙_} a =
   record { isEquivalence = isEquivalence;
            assoc = lift-Associative {∙ = _∙_} (IsSemigroup.assoc a) ;
            ∙-cong = cong₂ (lift-Op₂ _∙_) }

lift-IsMonoid : ∀ {ℓ} {A : Set ℓ} {∙ : Op₂ A} {ε : A}
   → IsMonoid _≡_ ∙ ε → IsMonoid _≡_ (lift-Op₂ ∙) (I ε)
lift-IsMonoid a =
   record { isSemigroup = lift-IsSemigroup (IsMonoid.isSemigroup a);
            identity = cong I ∘ proj₁ (IsMonoid.identity a) ∘ Id.unI ,
                       cong I ∘ proj₂ (IsMonoid.identity a) ∘ Id.unI }

lift-Monoid : ∀ {ℓ} {A : Set ℓ} {∙ : Op₂ A} {ε : A}
   → IsMonoid _≡_ ∙ ε → Monoid (suc ℓ) (suc ℓ)
lift-Monoid {_} {A} {∙} {ε} a =
   record {
     Carrier = Id A;
     _≈_ = _≡_;
     _∙_ = lift-Op₂ ∙;
     ε = I ε;
     isMonoid = lift-IsMonoid a }

```

   HoTT gives you the univalence axiom, letting you generalize this 
process when you can prove isomorphism between the types (and also 
abstract over the relation).

   HTH,
     — Twey


On 2014-01-12 09:39, Mateusz Kowalczyk wrote:
> Hi all,
> 
> I'm struggling with something that seemed like an easy task. Consider:
> 
> ```
> open import Algebra
> 
> record Input (τ : Set) : Set where
>   constructor I
>   field
>     unI : τ
> ```
> 
> I now want to give a monoid instance to this type, as long as τ can
> give me one. That is, in Haskell I could say
> 
> ```
> import Data.Monoid
> 
> newtype I t = I t
> 
> instance Monoid t => Monoid (I t) where
>   mempty = I mempty
>   I x `mappend` I y = I $ x `mappend` y
> ```
> 
> In fact, I could use the GHC extension to derive this for me. I
> thought writing an instance like this in Agda should not be a problem
> at all but I seem to be struggling. In the snippet below is my failed
> attempt to replicate what the Haskell code does. I had hoped that I
> can simply pass the Monoid (or should I be using RawMonoid?) instance
> of the underlying type and use that. My problem with this is that I
> don't seem to be able to get out anything meaningful out of the passed
> in Monoid. For example, opening the ‘m’ and trying to use ε in my
> ‘binOp’ function quickly shoots me down with the message that ‘Carrier
> ≠ τ’. I'm unsure how to tell Agda that I only want to pass in the
> Monoid instances with τ as a Carrier or how to get the value out once
> I do: the Monoid type doesn't seem to be parametrised by anything but
> Level. I struggle to find any examples in standard lib or elsewhere of
> how to use passed in instances of Monoid from Data.Algebra: all I can
> find are either usages of monoids from other libraries or short
> documents which show off Agda by rolling their own.
> 
> Here's the snippet. I imagine that the ‘monoid’ type needs fixing up
> so that I can actually use ‘m’ somehow.
> 
> I'd appreciate if someone can point me in the right direction.
> 
> ```
> module InputMonoid where
>   open import Level using (zero)
>   open import Relation.Binary.PropositionalEquality
> 
>   monoid : (τ : Set) → (m : Monoid {!!} {!!}) → Monoid zero zero
>   monoid τ m = record
>     { Carrier = Input τ
>     ; _≈_      = _≡_
>     ; _∙_      = binOp
>     ; ε        = {!!}
>     ; isMonoid = record
>       { isSemigroup = record
>         { isEquivalence = {!!}
>         ; assoc         = {!!}
>         ; ∙-cong        = {!!}
>         }
>       ; identity = {!!}
>       }
>     }
>     where
>       open Monoid m
> 
>       binOp : ∀ {τ} → Input τ → Input τ → Input τ
>       binOp (I unI) (I unI₁) = {!!}
> ```
> 
> --
> Mateusz K.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda