Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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
- β¦_β§ = {!!}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement