Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison filter.agda @ 380:0a116938a564

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Jul 2020 02:39:09 +0900
parents 7b6592f0851a
children d2cb5278e46d
comparison
equal deleted inserted replaced
379:7b6592f0851a 380:0a116938a564
217 findp n x = Findp n x 217 findp n x = Findp n x
218 find : (n : List Three ) → (x : Nat) → Findp n x → Two 218 find : (n : List Three ) → (x : Nat) → Findp n x → Two
219 find (j0 ∷ _) 0 v0 = i0 219 find (j0 ∷ _) 0 v0 = i0
220 find (j1 ∷ _) 0 v1 = i1 220 find (j1 ∷ _) 0 v1 = i1
221 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p 221 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p
222 lemma : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p)
223 lemma j0 n {x} {p} = refl
224 lemma j1 n {x} {p} = refl
225 lemma j2 n {x} {p} = refl
222 feq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q 226 feq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q
223 feq n {0} {v0} {v0} = refl 227 feq n {0} {v0} {v0} = refl
224 feq n {0} {v1} {v1} = refl 228 feq n {0} {v1} {v1} = refl
225 feq [] {Suc x} {()} 229 feq [] {Suc x} {()}
226 feq (_ ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) {!!} {!!} (feq n {x} {p} {q}) 230 feq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (lemma h n) (lemma h n) (feq n {x} {p} {q})
227 231
228 record _f⊆_ (f g : PFunc) : Set (suc n) where 232 record _f⊆_ (f g : PFunc) : Set (suc n) where
229 field 233 field
230 extend : {x : Nat} → (fr : dom f x ) → dom g x 234 extend : {x : Nat} → (fr : dom f x ) → dom g x
231 feq : {x : Nat} → {fr : dom f x } → map f x fr ≡ map g x (extend fr) 235 feq : {x : Nat} → {fr : dom f x } → map f x fr ≡ map g x (extend fr)