1 files changed, 0 insertions, 155 deletions
diff --git a/src/Data/Covec.agda b/src/Data/Covec.agda
deleted file mode 100644
index 529b0e8..0000000
--- a/src/Data/Covec.agda
+++ /dev/null
@@ -1,155 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Coinductive vectors
-------------------------------------------------------------------------
-
-module Data.Covec where
-
-open import Coinduction
-open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Conat as Coℕ using (Coℕ; zero; suc; _+_)
-open import Data.Cofin using (Cofin; zero; suc)
-open import Data.Vec using (Vec; []; _∷_)
-open import Data.Colist as Colist using (Colist; []; _∷_)
-open import Data.Product using (_,_)
-open import Relation.Binary
-
-------------------------------------------------------------------------
--- The type
-
-infixr 5 _∷_
-
-data Covec (A : Set) : Coℕ → Set where
-  []  : Covec A zero
-  _∷_ : ∀ {n} (x : A) (xs : ∞ (Covec A (♭ n))) → Covec A (suc n)
-
-------------------------------------------------------------------------
--- Some operations
-
-map : ∀ {A B n} → (A → B) → Covec A n → Covec B n
-map f []       = []
-map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)
-
-fromVec : ∀ {A n} → Vec A n → Covec A (Coℕ.fromℕ n)
-fromVec []       = []
-fromVec (x ∷ xs) = x ∷ ♯ fromVec xs
-
-fromColist : ∀ {A} (xs : Colist A) → Covec A (Colist.length xs)
-fromColist []       = []
-fromColist (x ∷ xs) = x ∷ ♯ fromColist (♭ xs)
-
-take : ∀ {A} m {n} → Covec A (m + n) → Covec A m
-take zero    xs       = []
-take (suc n) (x ∷ xs) = x ∷ ♯ take (♭ n) (♭ xs)
-
-drop : ∀ {A} m {n} → Covec A (Coℕ.fromℕ m + n) → Covec A n
-drop zero    xs       = xs
-drop (suc n) (x ∷ xs) = drop n (♭ xs)
-
-replicate : ∀ {A} n → A → Covec A n
-replicate zero    x = []
-replicate (suc n) x = x ∷ ♯ replicate (♭ n) x
-
-lookup : ∀ {A n} → Cofin n → Covec A n → A
-lookup zero    (x ∷ xs) = x
-lookup (suc n) (x ∷ xs) = lookup n (♭ xs)
-
-infixr 5 _++_
-
-_++_ : ∀ {A m n} → Covec A m → Covec A n → Covec A (m + n)
-[]       ++ ys = ys
-(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)
-
-[_] : ∀ {A} → A → Covec A (suc (♯ zero))
-[ x ] = x ∷ ♯ []
-
-------------------------------------------------------------------------
--- Equality and other relations
-
--- xs ≈ ys means that xs and ys are equal.
-
-infix 4 _≈_
-
-data _≈_ {A} : ∀ {n} (xs ys : Covec A n) → Set where
-  []  : [] ≈ []
-  _∷_ : ∀ {n} x {xs ys}
-        (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → _≈_ {n = suc n} (x ∷ xs) (x ∷ ys)
-
--- x ∈ xs means that x is a member of xs.
-
-infix 4 _∈_
-
-data _∈_ {A} : ∀ {n} → A → Covec A n → Set where
-  here  : ∀ {n x  } {xs}                   → _∈_ {n = suc n} x (x ∷ xs)
-  there : ∀ {n x y} {xs} (x∈xs : x ∈ ♭ xs) → _∈_ {n = suc n} x (y ∷ xs)
-
--- xs ⊑ ys means that xs is a prefix of ys.
-
-infix 4 _⊑_
-
-data _⊑_ {A} : ∀ {m n} → Covec A m → Covec A n → Set where
-  []  : ∀ {n} {ys : Covec A n} → [] ⊑ ys
-  _∷_ : ∀ {m n} x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) →
-        _⊑_ {m = suc m} {suc n} (x ∷ xs) (x ∷ ys)
-
-------------------------------------------------------------------------
--- Some proofs
-
-setoid : Set → Coℕ → Setoid _ _
-setoid A n = record
-  { Carrier       = Covec A n
-  ; _≈_           = _≈_
-  ; isEquivalence = record
-    { refl  = refl
-    ; sym   = sym
-    ; trans = trans
-    }
-  }
-  where
-  refl : ∀ {A n} → Reflexive (_≈_ {A} {n})
-  refl {x = []}     = []
-  refl {x = x ∷ xs} = x ∷ ♯ refl
-
-  sym : ∀ {A n} → Symmetric (_≈_ {A} {n})
-  sym []        = []
-  sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈)
-
-  trans : ∀ {A n} → Transitive (_≈_ {A} {n})
-  trans []        []         = []
-  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)
-
-poset : Set → Coℕ → Poset _ _ _
-poset A n = record
-  { Carrier        = Covec A n
-  ; _≈_            = _≈_
-  ; _≤_            = _⊑_
-  ; isPartialOrder = record
-    { isPreorder = record
-      { isEquivalence = Setoid.isEquivalence (setoid A n)
-      ; reflexive     = reflexive
-      ; trans         = trans
-      }
-    ; antisym  = antisym
-    }
-  }
-  where
-  reflexive : ∀ {A n} → _≈_ {A} {n} ⇒ _⊑_
-  reflexive []        = []
-  reflexive (x ∷ xs≈) = x ∷ ♯ reflexive (♭ xs≈)
-
-  trans : ∀ {A n} → Transitive (_⊑_ {A} {n})
-  trans []        _          = []
-  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)
-
-  antisym : ∀ {A n} → Antisymmetric (_≈_ {A} {n}) _⊑_
-  antisym []       []        = []
-  antisym (x ∷ p₁) (.x ∷ p₂) = x ∷ ♯ antisym (♭ p₁) (♭ p₂)
-
-map-cong : ∀ {A B n} (f : A → B) → _≈_ {n = n} =[ map f ]⇒ _≈_
-map-cong f []        = []
-map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)
-
-take-⊑ : ∀ {A} m {n} (xs : Covec A (m + n)) → take m xs ⊑ xs
-take-⊑ zero    xs       = []
-take-⊑ (suc n) (x ∷ xs) = x ∷ ♯ take-⊑ (♭ n) (♭ xs)