Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison partfunc.agda @ 423:9984cdd88da3
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 01 Aug 2020 18:05:23 +0900 |
parents | 55f44ec2a0c6 |
children |
comparison
equal
deleted
inserted
replaced
422:44a484f17f26 | 423:9984cdd88da3 |
---|---|
17 | 17 |
18 open _∧_ | 18 open _∧_ |
19 open _∨_ | 19 open _∨_ |
20 open Bool | 20 open Bool |
21 | 21 |
22 ---- | |
23 -- | |
24 -- Partial Function without ZF | |
25 -- | |
22 | 26 |
23 record PFunc (Dom : Set n) (Cod : Set n) : Set (suc n) where | 27 record PFunc (Dom : Set n) (Cod : Set n) : Set (suc n) where |
24 field | 28 field |
25 dom : Dom → Set n | 29 dom : Dom → Set n |
26 pmap : (x : Dom ) → dom x → Cod | 30 pmap : (x : Dom ) → dom x → Cod |
27 meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q | 31 meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q |
28 | 32 |
33 ---- | |
34 -- | |
35 -- PFunc (Lift n Nat) Cod is equivalent to List (Maybe Cod) | |
36 -- | |
29 | 37 |
30 data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where | 38 data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where |
31 v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero | 39 v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero |
32 vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) | 40 vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) |
33 | 41 |
46 List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod | 54 List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod |
47 List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x)) | 55 List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x)) |
48 ; pmap = λ x y → find fp (lower x) (lower y) | 56 ; pmap = λ x y → find fp (lower x) (lower y) |
49 ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} | 57 ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} |
50 } | 58 } |
59 ---- | |
60 -- | |
61 -- to List (Maybe Two) is a Latice | |
62 -- | |
51 | 63 |
52 _3⊆b_ : (f g : List (Maybe Two)) → Bool | 64 _3⊆b_ : (f g : List (Maybe Two)) → Bool |
53 [] 3⊆b [] = true | 65 [] 3⊆b [] = true |
54 [] 3⊆b (nothing ∷ g) = [] 3⊆b g | 66 [] 3⊆b (nothing ∷ g) = [] 3⊆b g |
55 [] 3⊆b (_ ∷ g) = true | 67 [] 3⊆b (_ ∷ g) = true |