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

comparison filter.agda @ 375:8cade5f660bd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 20 Jul 2020 16:22:44 +0900
parents b265042be254
children 7b6592f0851a
comparison
equal deleted inserted replaced
374:b265042be254 375:8cade5f660bd
171 extend : (x : Nat) → (fr : restrict f x ) → restrict g x 171 extend : (x : Nat) → (fr : restrict f x ) → restrict g x
172 feq : (x : Nat) → (fr : restrict f x ) → map f x fr ≡ map g x (extend x fr) 172 feq : (x : Nat) → (fr : restrict f x ) → map f x fr ≡ map g x (extend x fr)
173 173
174 open _f⊆_ 174 open _f⊆_
175 175
176 _f∩_ : (f g : PFunc) → PFunc
177 f f∩ g = record { restrict = λ x → (restrict f x ) ∧ (restrict g x ) ∧ ((fr : restrict f x ) → (gr : restrict g x ) → map f x fr ≡ map g x gr)
178 ; map = λ x p → map f x (proj1 p) }
179
180 _↑_ : (Nat → Two) → Nat → PFunc
181 f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
182
183 record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where
184 field
185 gn : Nat
186 f<n : (f ↑ gn) f⊆ p
187
188 open Gf
189
190 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 176 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
191 field 177 field
192 filter : L → Set n 178 filter : L → Set n
193 f⊆P : PL filter 179 f⊆P : PL filter
194 filter1 : { p q : L } → PL (λ x → q ⊆ x ) → filter p → p ⊆ q → filter q 180 filter1 : { p q : L } → PL (λ x → q ⊆ x ) → filter p → p ⊆ q → filter q
203 } 189 }
204 190
205 min = Data.Nat._⊓_ 191 min = Data.Nat._⊓_
206 -- m≤m⊔n = Data.Nat._⊔_ 192 -- m≤m⊔n = Data.Nat._⊔_
207 open import Data.Nat.Properties 193 open import Data.Nat.Properties
194
195 _f∩_ : (f g : PFunc) → PFunc
196 f f∩ g = record { restrict = λ x → (restrict f x ) ∧ (restrict g x ) ∧ ((fr : restrict f x ) → (gr : restrict g x ) → map f x fr ≡ map g x gr)
197 ; map = λ x p → map f x (proj1 p) }
198
199 _↑_ : (Nat → Two) → Nat → PFunc
200 f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
201
202 record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where
203 field
204 gn : Nat
205 f<n : (f ↑ gn) f⊆ p
206
207 open Gf
208 208
209 GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_ 209 GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_
210 GF f = record { 210 GF f = record {
211 filter = λ p → Gf f p 211 filter = λ p → Gf f p
212 ; f⊆P = lift OneObj 212 ; f⊆P = lift OneObj