Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 373:b4a247f9d940
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 19 Jul 2020 19:57:59 +0900 |
| parents | 8c3b59f583f2 |
| children | b265042be254 |
| files | filter.agda |
| diffstat | 1 files changed, 4 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/filter.agda Sun Jul 19 19:14:12 2020 +0900 +++ b/filter.agda Sun Jul 19 19:57:59 2020 +0900 @@ -196,12 +196,12 @@ filter = λ p → Gf f p ; f⊆P = OneObj ; filter1 = λ {p} {q} fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q } - ; filter2 = λ {p} {q} fp fq → record { gn = {!!} ; f<n = {!!} } + ; filter2 = λ {p} {q} fp fq → record { gn = gn fp ; f<n = f2 fp fq } } where f1 : {p q : PFunc } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → q f⊆ (f ↑ gn fp) - f1 {p} {q} fp p⊆q = record { extend = λ x fr → extend (f<n fp) x {!!} ; feq = λ x fr → {!!} } where - f2 : (x : Nat) → x ≤ gn fp - f2 x = ? -- extend (f<n fp) x ? + f1 {p} {q} fp p⊆q = record { extend = λ x fq → {!!} ; feq = λ x fr → {!!} } where + f2 : {p q : PFunc } → (fp : Gf f p ) → (fq : Gf f q ) → (p f∩ q) f⊆ (f ↑ gn fp) + f2 {p} {q} fp fq = record { extend = λ x y → extend (f<n fp) x (proj1 y) ; feq = λ x fr → {!!} } where ODSuc : (y : HOD) → infinite ∋ y → HOD ODSuc y lt = Union (y , (y , y))