open import Data.Nat
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
⟦_⟧ = {!!}