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

comparison src/partfunc.agda @ 1096:55ab5de1ae02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recovery
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2022 12:54:05 +0900
parents 5f22af3562b7
children 7d2bae0ff36b
comparison
equal deleted inserted replaced
1095:08b6aa6870d9 1096:55ab5de1ae02
200 finite3cov : (p : List (Maybe Two) ) → List (Maybe Two) 200 finite3cov : (p : List (Maybe Two) ) → List (Maybe Two)
201 finite3cov [] = [] 201 finite3cov [] = []
202 finite3cov (just y ∷ x) = just y ∷ finite3cov x 202 finite3cov (just y ∷ x) = just y ∷ finite3cov x
203 finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x 203 finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x
204 204
205 record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where
206 field
207 filter : L → Set n
208 f⊆P : PL filter
209 filter1 : { p q : L } → PL (λ x → q ⊆ x ) → filter p → p ⊆ q → filter q
210 filter2 : { p q : L } → filter p → filter q → filter (p ∩ q)
211
212 record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where
213 field
214 dense : L → Set n
215 d⊆P : PL dense
216 dense-f : L → L
217 dense-d : { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p )
218 dense-p : { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p)
219
220
205 Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_ 221 Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_
206 Dense-3 = record { 222 Dense-3 = record {
207 dense = λ x → Finite3b x ≡ true 223 dense = λ x → Finite3b x ≡ true
208 ; d⊆P = OneObj 224 ; d⊆P = OneObj
209 ; dense-f = λ x → finite3cov x 225 ; dense-f = λ x → finite3cov x