diff options
author | Sean Whitton <spwhitton@spwhitton.name> | 2018-11-23 17:29:18 -0700 |
---|---|---|
committer | Sean Whitton <spwhitton@spwhitton.name> | 2018-11-23 17:29:18 -0700 |
commit | a19b25a865b2000bbd3acd909f5951a5407c1eec (patch) | |
tree | e283a809447d00f63289a918e6fd0f73ee0b8ece /src/Codata/Covec/Properties.agda | |
parent | 0b3946998d82e1be6c50e2872e7474db69b5a0dc (diff) |
New upstream version 0.17
Diffstat (limited to 'src/Codata/Covec/Properties.agda')
-rw-r--r-- | src/Codata/Covec/Properties.agda | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/Codata/Covec/Properties.agda b/src/Codata/Covec/Properties.agda new file mode 100644 index 0000000..c86975c --- /dev/null +++ b/src/Codata/Covec/Properties.agda @@ -0,0 +1,30 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of operations on the Covec type +------------------------------------------------------------------------ + +module Codata.Covec.Properties where + +open import Size +open import Codata.Thunk using (Thunk; force) +open import Codata.Conat +open import Codata.Covec +open import Codata.Covec.Bisimilarity +open import Function +open import Relation.Binary.PropositionalEquality as Eq + +-- Functor laws + +module _ {a} {A : Set a} where + + map-identity : ∀ {m} (as : Covec A ∞ m) {i} → i , m ⊢ map id as ≈ as + map-identity [] = [] + map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force) + +module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where + + map-map-fusion : ∀ (f : A → B) (g : B → C) {m} as {i} → i , m ⊢ map g (map f as) ≈ map (g ∘ f) as + map-map-fusion f g [] = [] + map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force) + |