module Universal where

open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open Relation.Binary.PropositionalEquality.≡-Reasoning
open import Agda.Primitive
open import Data.Nat hiding (_⊔_)
open import Data.Unit hiding (setoid)
open import Data.Bool
open import Data.Nat.Properties
open import Data.Product hiding (map)
open import Data.Vec hiding (drop; map)
open import Data.Fin hiding (_+_)
open import Data.List hiding (zipWith)

data HVec {a} : (n : ℕ) → List (Set a) → Set a where
  hnil : HVec 0 []
  hcons : {A : Set a} → {n : ℕ} → {l : List (Set a)} →
          (x : A) → HVec n l → HVec (suc n) (A ∷ l)


hLookup : {a : Level} → ∀ {len l} → HVec {a} len l → (n : Fin (length l)) → (lookup n (fromList l))
hLookup hnil ()
hLookup (hcons x xs) zero = x
hLookup (hcons x xs) (suc n) = hLookup xs n

opSignature : ∀ {a} → Set a → ℕ → Set a
opSignature A zero = A
opSignature A (suc n) = A → (opSignature A n)

apply : ∀ {a} → {A : Set a} → (n : ℕ) → (f : opSignature A n) →
                (v : Vec A n) → A
apply zero f [] = f
apply (suc n) f (x ∷ l) = apply n (f x) l

data WellDefined {a b} {A : Set a} (_==_ : A → A → Set b) (n : ℕ) (f : opSignature A n) : Set (a ⊔ b) where
  wd : ((vx vy : Vec A n) →
       (p : let t = toList (zipWith _==_ vx vy) in HVec (length t) t) →
       (apply n f vx == apply n f vy)) →
       WellDefined _==_ n f

respect : ∀ {a b} → {A : Set a} → (_==_ : A → A → Set b) →
          (ns : List ℕ) → HVec (length ns) (map (opSignature A) ns) →
          List (Set (a ⊔ b))
respect _ [] _ = []
respect _==_ (n ∷ ns) (hcons f hfs) = (WellDefined _==_ n f) ∷ (respect _==_ ns hfs)

open Agda.Primitive

record Universal {a b} (S : Setoid a b) (Signature : List ℕ) : Set (lsuc (a ⊔ b)) where
  open Setoid S

  n = length Signature

  opTypes = map (opSignature Carrier) Signature

  field
    Operators : HVec n opTypes

  wdTypes = respect _≈_  Signature Operators

  field
    WellDef : HVec n wdTypes

record Monoid {a b} (S : Setoid a b) : Set (lsuc (a ⊔ b)) where
  open Setoid S

  field
    {{Uni}} : Universal S (2 ∷ 0 ∷ [])

  open Universal Uni

  _●_ = hLookup Operators zero
  ε = hLookup Operators (suc zero)

  field
    assoc : (x y z : Carrier) → (x ● (y ● z)) ≈ ((x ● y) ● z)
    lunit : (x : Carrier) → (ε ● x) ≈ x
    runit : (x : Carrier) → (x ● ε) ≈ x

plusAssoc : (x y z : ℕ) → x + (y + z) ≡ (x + y) + z
plusAssoc zero y z = refl
plusAssoc (suc x) y z = cong suc (plusAssoc x y z)

plusZero : (x : ℕ) → x + 0 ≡ x
plusZero zero = refl
plusZero (suc n) = cong suc (plusZero n)

plusWellDef : WellDefined _≡_ 2 _+_
plusWellDef = wd f where
              f : (vx vy : Vec ℕ 2) →
                  let t = toList (zipWith _≡_ vx vy) in HVec (length t) t →
                  apply 2 _+_ vx ≡ apply 2 _+_ vy
              f (a ∷ b ∷ []) (c ∷ d ∷ []) (hcons pac (hcons pbd hnil)) =
                begin
                  a + b
                ≡⟨ cong (λ x → x + b) pac ⟩
                  c + b
                ≡⟨ cong (λ x → c + x) pbd ⟩
                  c + d
                ∎

zeroWellDef : WellDefined _≡_ 0 0
zeroWellDef = wd f where
              f : (vx vy : Vec ℕ 0) →
                  let t = toList (zipWith _≡_ vx vy) in HVec (length t) t →
                  apply 0 0 vx ≡ apply 0 0 vy
              f [] [] _ = refl

instance
  natPlus : Monoid (setoid ℕ)
  natPlus = record
            {
              Uni = record
                    {
                      Operators = hcons _+_ (hcons 0 hnil);
                      WellDef = hcons plusWellDef (hcons zeroWellDef hnil)
                    };
              assoc = plusAssoc;
              lunit = λ x → refl;
              runit = plusZero
            }