diff options
Diffstat (limited to 'Generic.agda')
| -rw-r--r-- | Generic.agda | 31 |
1 files changed, 28 insertions, 3 deletions
diff --git a/Generic.agda b/Generic.agda index 4e55c21..f543256 100644 --- a/Generic.agda +++ b/Generic.agda @@ -3,14 +3,17 @@ 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 (_∘_ ; id) -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.Indexed using (_at_) renaming (Setoid to ISetoid) +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 (_>>=_) @@ -36,6 +39,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 + sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n) sequenceV = mapMV id @@ -64,3 +75,17 @@ 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 + +vecIsISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀ +vecIsISetoid S = record + { Carrier = Vec (Setoid.Carrier S) + ; _≈_ = λ x → S VecEq.≈ x + ; isEquivalence = record + { refl = VecEq.refl S _ + ; sym = VecEq.sym S + ; trans = VecEq.trans S } + } + + +vecIsSetoid : Setoid ℓ₀ ℓ₀ → ℕ → Setoid ℓ₀ ℓ₀ +vecIsSetoid S n = (vecIsISetoid S) at n |