blob: 9a0a4aaf932877f5090adcd051399ec5bb936388 (
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
{-# OPTIONS --without-K --safe #-}
module Cfe.Fin.Base where
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; Fin′; zero; suc; inject₁)
data Fin< : ∀ {n} → Fin n → Set where
zero : ∀ {n i} → Fin< {suc n} (suc i)
suc : ∀ {n i} → Fin< {n} i → Fin< (suc i)
data Fin<′ : ∀ {n i} → Fin< {n} i → Set where
zero : ∀ {n i j} → Fin<′ {suc n} {suc i} (suc j)
suc : ∀ {n i j} → Fin<′ {n} {i} j → Fin<′ (suc j)
-- Fin> {n} zero ≡ Fin n
-- Fin> (suc i) ≡ Fin> i
data Fin> : ∀ {n} → Fin n → Set where
zero : ∀ {n} → Fin> {suc n} zero
suc : ∀ {n} → Fin> {suc n} zero → Fin> {suc (suc n)} zero
inj : ∀ {n i} → Fin> {n} i → Fin> (suc i)
data Fin>′ : ∀ {n i} → Fin> {n} i → Set where
zero : ∀ {n j} → Fin>′ {suc (suc n)} {zero} (suc j)
suc : ∀ {n j} → Fin>′ {suc n} {zero} j → Fin>′ (suc j)
inj : ∀ {n i j} → Fin>′ {n} {i} j → Fin>′ (inj j)
toℕ< : ∀ {n i} → Fin< {n} i → ℕ
toℕ< zero = 0
toℕ< (suc j) = suc (toℕ< j)
toℕ> : ∀ {n i} → Fin> {n} i → ℕ
toℕ> zero = 0
toℕ> (suc j) = suc (toℕ> j)
toℕ> (inj j) = suc (toℕ> j)
strengthen< : ∀ {n} → (i : Fin n) → Fin< (suc i)
strengthen< zero = zero
strengthen< (suc i) = suc (strengthen< i)
inject<! : ∀ {n i} → Fin< {suc n} i → Fin n
inject<! {suc _} zero = zero
inject<! {suc _} (suc j) = suc (inject<! j)
cast<-inject₁ : ∀ {n i} → Fin< {n} i → Fin< (inject₁ i)
cast<-inject₁ zero = zero
cast<-inject₁ (suc j) = suc (cast<-inject₁ j)
inject<!′ : ∀ {n i j} → Fin<′ {suc n} {suc i} j → Fin< i
inject<!′ {suc _} {suc _} zero = zero
inject<!′ {suc _} {suc _} (suc k) = suc (inject<!′ k)
inject<′ : ∀ {n i j} → Fin<′ {n} {i} j → Fin< i
inject<′ zero = zero
inject<′ (suc k) = suc (inject<′ k)
inject<!′-inject! : ∀ {n i j} → Fin<′ {suc n} {i} j → Fin< (inject<! j)
inject<!′-inject! {suc n} {_} {suc j} zero = zero
inject<!′-inject! {suc n} {_} {suc j} (suc k) = suc (inject<!′-inject! k)
raise> : ∀ {n i} → Fin> {n} i → Fin n
raise> {suc _} zero = zero
raise> {suc _} (suc j) = suc (raise> j)
raise> {suc _} (inj j) = suc (raise> j)
suc> : ∀ {n i} → Fin> {n} i → Fin> (inject₁ i)
suc> zero = suc zero
suc> (suc j) = suc (suc> j)
suc> (inj j) = inj (suc> j)
inject>!′ : ∀ {n i j} → Fin>′ {suc n} {inject₁ i} j → Fin> {n} i
inject>!′ {suc _} {zero} zero = zero
inject>!′ {suc (suc _)} {zero} {suc _} (suc k) = suc (inject>!′ k)
inject>!′ {suc _} {suc i} (inj k) = inj (inject>!′ k)
inject>′ : ∀ {n i j} → Fin>′ {n} {i} j → Fin> {n} i
inject>′ zero = zero
inject>′ (suc k) = suc (inject>′ k)
inject>′ (inj k) = inj (inject>′ k)
cast>-inject<! : ∀ {n i} (j : Fin< (suc i)) → Fin> {suc n} i → Fin> (inject<! j)
cast>-inject<! zero zero = zero
cast>-inject<! zero (suc k) = suc (cast>-inject<! zero k)
cast>-inject<! {suc n} zero (inj k) = suc (cast>-inject<! zero k)
cast>-inject<! {suc n} (suc j) (inj k) = inj (cast>-inject<! j k)
reflect :
∀ {n i} → (j : Fin< {suc (suc n)} (suc i)) → (k : Fin<′ (suc j)) → Fin> (inject<! (inject<!′ k))
reflect zero zero = zero
reflect {suc n} {suc i} (suc j) zero = suc (reflect j zero)
reflect {suc n} {suc i} (suc j) (suc k) = inj (reflect j k)
|
