diff options
Diffstat (limited to 'Generic.agda')
| -rw-r--r-- | Generic.agda | 28 |
1 files changed, 25 insertions, 3 deletions
diff --git a/Generic.agda b/Generic.agda index 11b9594..33cd1ac 100644 --- a/Generic.agda +++ b/Generic.agda @@ -3,14 +3,16 @@ module Generic where import Category.Functor import Category.Monad open import Data.List using (List ; length ; replicate) renaming ([] to []L ; _∷_ to _∷L_) -open import Data.Maybe using (Maybe ; just ; nothing) +open import Data.Maybe using (Maybe ; just ; nothing) renaming (setoid to MaybeEq) open import Data.Nat using (ℕ ; zero ; suc) open import Data.Product using (_×_ ; _,_) open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_) +open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Function using (_∘_) -import Level +open import Level using () renaming (zero to ℓ₀) +open import Relation.Binary using (Setoid ; module Setoid) open import Relation.Binary.Core using (_≡_ ; refl) -open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans) +open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans) renaming (setoid to PropEq) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) @@ -46,6 +48,14 @@ mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → map mapMV-purity f []V = refl mapMV-purity f (x ∷V xs) rewrite mapMV-purity f xs = refl +maybeEq-from-≡ : {A : Set} {a b : Maybe A} → Setoid._≈_ (PropEq (Maybe A)) a b → Setoid._≈_ (MaybeEq (PropEq A)) a b +maybeEq-from-≡ {a = just x} {b = .(just x)} refl = just refl +maybeEq-from-≡ {a = nothing} {b = .nothing} refl = nothing + +maybeEq-to-≡ : {A : Set} {a b : Maybe A} → Setoid._≈_ (MaybeEq (PropEq A)) a b → Setoid._≈_ (PropEq (Maybe A)) a b +maybeEq-to-≡ (just refl) = refl +maybeEq-to-≡ nothing = refl + subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) → f ∘ subst T p ≗ subst T (cong g p) ∘ f subst-cong T f refl _ = refl @@ -65,3 +75,15 @@ toList-fromList (x ∷L xs) = cong (_∷L_ x) (toList-fromList xs) toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) → toList (subst (Vec A) p v) ≡ toList v toList-subst v refl = refl + +vecIsSetoid : Setoid ℓ₀ ℓ₀ → ℕ → Setoid ℓ₀ ℓ₀ +vecIsSetoid S n = record + { Carrier = Vec S.Carrier n + ; _≈_ = λ x y → VecEq._≈_ S {n} x {n} y + ; isEquivalence = record + { refl = VecEq.refl S _ + ; sym = VecEq.sym S + ; trans = VecEq.trans S } + } + where + module S = Setoid S |