Issue558b.agda

module Issue558b where

data Nat : Set where
  Z : Nat
  S : Nat → Nat

data _≡_ {A : Set} (a : A) : A → Set where
  Refl : a ≡ a

plus : Nat → Nat → Nat
plus Z n = n
plus (S n) m = S (plus n m)

data Addable (τ : Set) : Set where
  addable : (τ → τ → τ) → Addable τ

plus' : {τ : Set} → Addable τ → τ → τ → τ
plus' (addable p) = p

record ⊤ : Set where

module AddableM {τ : Set} {a : ⊤} (a : Addable τ) where
  _+_ : τ → τ → τ
  _+_ = plus' a

-- record Addable (τ : Set) : Set where
--  constructor addable
--  field
--   _+_ : τ → τ → τ

open module AddableIFS {t : Set} {a : ⊤} {{r : Addable t}} = AddableM {t} r

data CommAddable (τ : Set) {a : ⊤} : Set where
 commAddable : (addable : Addable τ) → ((a b : τ) → (a + b) ≡ (b + a)) → CommAddable τ

private
  addableCA' : {τ : Set} (ca : CommAddable τ) → Addable τ
  addableCA' (commAddable a _) = a

  comm' : {τ : Set} (ca : CommAddable τ) →
          let a = addableCA' ca in (a b : τ) → (a + b) ≡ (b + a)
  comm' (commAddable _ c) = c

module CommAddableM {τ : Set} {a : ⊤} (ca : CommAddable τ) where
  addableCA : Addable τ
  addableCA = addableCA' ca

  comm : (a b : τ) → (a + b) ≡ (b + a)
  comm = comm' ca

natAdd : Addable Nat
natAdd = addable plus

postulate commPlus : (a b : Nat) → plus a b ≡ plus b a

commNatAdd : CommAddable Nat
commNatAdd = commAddable natAdd commPlus

open CommAddableM {{...}}

test : (Z + Z) ≡ Z
test = comm Z Z

a : {x y : Nat} → (S (S Z) + (x + y)) ≡ ((x + y) + S (S Z))
a {x}{y} = comm (S (S Z)) (x + y)