3 files changed, 113 insertions, 0 deletions
diff --git a/src/Codata/Covec/Bisimilarity.agda b/src/Codata/Covec/Bisimilarity.agda
new file mode 100644
index 0000000..65c49b7
--- /dev/null
+++ b/src/Codata/Covec/Bisimilarity.agda
@@ -0,0 +1,61 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bisimilarity for Covecs
+------------------------------------------------------------------------
+
+module Codata.Covec.Bisimilarity where
+
+open import Level using (_⊔_)
+open import Size
+open import Codata.Thunk
+open import Codata.Conat hiding (_⊔_)
+open import Codata.Covec
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+
+data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) :
+           ∀ m n (xs : Covec A ∞ m) (ys : Covec B ∞ n) → Set (r ⊔ a ⊔ b) where
+  []  : Bisim R i zero zero [] []
+  _∷_ : ∀ {x y m n xs ys} → R x y → Thunk^R (λ i → Bisim R i (m .force) (n .force)) i xs ys →
+        Bisim R i (suc m) (suc n) (x ∷ xs) (y ∷ ys)
+
+
+module _ {a r} {A : Set a} {R : A → A → Set r} where
+
+ reflexive : Reflexive R → ∀ {i m} → Reflexive (Bisim R i m m)
+ reflexive refl^R {i} {m} {[]}     = []
+ reflexive refl^R {i} {m} {r ∷ rs} = refl^R ∷ λ where .force → reflexive refl^R
+
+module _ {a b} {A : Set a} {B : Set b}
+         {r} {P : A → B → Set r} {Q : B → A → Set r} where
+
+ symmetric : Sym P Q → ∀ {i m n} → Sym (Bisim P i m n) (Bisim Q i n m)
+ symmetric sym^PQ []       = []
+ symmetric sym^PQ (p ∷ ps) = sym^PQ p ∷ λ where .force → symmetric sym^PQ (ps .force)
+
+module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
+         {r} {P : A → B → Set r} {Q : B → C → Set r} {R : A → C → Set r} where
+
+ transitive : Trans P Q R → ∀ {i m n p} → Trans (Bisim P i m n) (Bisim Q i n p) (Bisim R i m p)
+ transitive trans^PQR []       []       = []
+ transitive trans^PQR (p ∷ ps) (q ∷ qs) =
+   trans^PQR p q ∷ λ where .force → transitive trans^PQR (ps .force) (qs .force)
+
+-- Pointwise Equality as a Bisimilarity
+------------------------------------------------------------------------
+
+module _ {ℓ} {A : Set ℓ} where
+
+ infix 1 _,_⊢_≈_
+ _,_⊢_≈_ : ∀ i m → Covec A ∞ m → Covec A ∞ m → Set ℓ
+ _,_⊢_≈_ i m = Bisim _≡_ i m m
+
+ refl : ∀ {i m} → Reflexive (i , m ⊢_≈_)
+ refl = reflexive Eq.refl
+
+ sym : ∀ {i m} → Symmetric (i , m ⊢_≈_)
+ sym = symmetric Eq.sym
+
+ trans : ∀ {i m} → Transitive (i , m ⊢_≈_)
+ trans = transitive Eq.trans
diff --git a/src/Codata/Covec/Categorical.agda b/src/Codata/Covec/Categorical.agda
new file mode 100644
index 0000000..8e99de4
--- /dev/null
+++ b/src/Codata/Covec/Categorical.agda
@@ -0,0 +1,22 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A categorical view of Covec
+------------------------------------------------------------------------
+
+module Codata.Covec.Categorical where
+
+open import Codata.Conat
+open import Codata.Covec
+
+open import Category.Functor
+open import Category.Applicative
+
+functor : ∀ {ℓ i n} → RawFunctor {ℓ} (λ A → Covec A n i)
+functor = record { _<$>_ = map }
+
+applicative : ∀ {ℓ i n} → RawApplicative {ℓ} (λ A → Covec A n i)
+applicative = record
+  { pure = replicate _
+  ; _⊛_  = ap
+  }
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)
+