blob: 138641c09c6f00819c4a639143d1f1b277666027 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- "Finite" sets indexed on coinductive "natural" numbers
------------------------------------------------------------------------
module Codata.Musical.Cofin where
open import Codata.Musical.Notation
open import Codata.Musical.Conat as Conat using (Coℕ; suc; ∞ℕ)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Fin using (Fin; zero; suc)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Function
------------------------------------------------------------------------
-- The type
-- Note that Cofin ∞ℕ is /not/ finite. Note also that this is not a
-- coinductive type, but it is indexed on a coinductive type.
data Cofin : Coℕ → Set where
zero : ∀ {n} → Cofin (suc n)
suc : ∀ {n} (i : Cofin (♭ n)) → Cofin (suc n)
suc-injective : ∀ {m} {p q : Cofin (♭ m)} → (Cofin (suc m) ∋ suc p) ≡ suc q → p ≡ q
suc-injective refl = refl
------------------------------------------------------------------------
-- Some operations
fromℕ : ℕ → Cofin ∞ℕ
fromℕ zero = zero
fromℕ (suc n) = suc (fromℕ n)
toℕ : ∀ {n} → Cofin n → ℕ
toℕ zero = zero
toℕ (suc i) = suc (toℕ i)
fromFin : ∀ {n} → Fin n → Cofin (Conat.fromℕ n)
fromFin zero = zero
fromFin (suc i) = suc (fromFin i)
toFin : ∀ n → Cofin (Conat.fromℕ n) → Fin n
toFin zero ()
toFin (suc n) zero = zero
toFin (suc n) (suc i) = suc (toFin n i)
|
