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