open import Data.Nat --using (ℕ)
open import Agda.Builtin.Equality using (_≡_)
open import Codata.Stream
open import Agda.Builtin.Size
open import Codata.Thunk as Thunk using (Thunk; force)

record Ring : Set₁ where
  constructor RING
  field
    Carrier : Set
    𝟘 𝟙 : Carrier
    _⊕_ _⊗_ : Carrier → Carrier → Carrier

open Ring

record Hom (R S : Ring) : Set where
  constructor HOM
  field
    fun : Carrier R → Carrier S

    𝟘-law : fun (𝟘 R) ≡ 𝟘 S
    𝟙-law : fun (𝟙 R) ≡ 𝟘 S

    ⊕-law : (a b : Carrier R) →
      fun ((_⊕_ R) a b) ≡ (_⊕_ S) (fun a) (fun b)
    ⊗-law : (a b : Carrier R) →
      fun ((_⊗_ R) a b) ≡ (_⊗_ S) (fun a) (fun b)


∞Decimal : Ring
∞Decimal = RING Carrier' 𝟘' 𝟙' _⊕'_ _⊗'_ where
  Carrier' = Stream ℕ ∞
  𝟘' = repeat 0
  𝟙' = 1 ∷ λ where .force → 𝟘'
  _⊕'_ = zipWith _+_
  infixl 10 _⊕'_
  _⊗'_ : Carrier' → Carrier' → Carrier'
  (x ∷ xs) ⊗' (y ∷ ys) = (x * y) ∷ λ where .force → (zipWith _*_ (repeat x) (ys .force)) ⊕' (zipWith _*_ (xs .force) (repeat y)) ⊕' (0 ∷ λ where .force → _⊗'_ (xs .force) (ys .force))


↺Decimal : Ring
↺Decimal = {!!}

⟦_⟧ : Hom ↺Decimal ∞Decimal
⟦_⟧ = {!!}