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