1. open import Data.Nat
2. open import Agda.Builtin.Equality using (_≡_)
3. open import Codata.Stream
4. open import Agda.Builtin.Size
5. open import Codata.Thunk as Thunk using (Thunk; force)
6.  
7. record Ring : Set₁ where
8.   constructor RING
9.   field
10.     Carrier : Set
11.     ? ? : Carrier
12.     _⊕_ _⊗_ : Carrier → Carrier → Carrier
13.  
14. open Ring
15.  
16. record Hom (R S : Ring) : Set where
17.   constructor HOM
18.   field
19.     fun : Carrier R → Carrier S
20.  
21.     ?-law : fun (? R) ≡ ? S
22.     ?-law : fun (? R) ≡ ? S
23.  
24.     ⊕-law : (a b : Carrier R) →
25.       fun ((_⊕_ R) a b) ≡ (_⊕_ S) (fun a) (fun b)
26.     ⊗-law : (a b : Carrier R) →
27.       fun ((_⊗_ R) a b) ≡ (_⊗_ S) (fun a) (fun b)
28.      
29.  
30. ∞Decimal : Ring
31. ∞Decimal = RING Carrier' ?' ?' _⊕'_ _⊗'_ where
32.   Carrier' = Stream ℕ ∞
33.   ?' = repeat 0
34.   ?' = 1 ∷ λ where .force → ?'
35.   _⊕'_ = zipWith _+_
36.   infixl 10 _⊕'_
37.   _⊗'_ : Carrier' → Carrier' → Carrier'
38.   (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))
39.  
40.  
41. ↺Decimal : Ring
42. ↺Decimal = {!!}
43.  
44. ⟦_⟧ : Hom ↺Decimal ∞Decimal
45. ⟦_⟧ = {!!}
46.