# HG changeset patch # User Shinji KONO # Date 1595153652 -32400 # Node ID 8c3b59f583f278a2775d4e8079d6995dd5b83dea # Parent e75402b1f7d4998ed0769f78cebe7e60f0ae8e46 ... diff -r e75402b1f7d4 -r 8c3b59f583f2 filter.agda --- a/filter.agda Sun Jul 19 16:19:24 2020 +0900 +++ b/filter.agda Sun Jul 19 19:14:12 2020 +0900 @@ -168,26 +168,22 @@ extend : (x : Nat) → (fr : restrict f x ) → restrict g x feq : (x : Nat) → (fr : restrict f x ) → map f x fr ≡ map g x (extend x fr) -record _f∩_ (f g : PFunc) : Set (suc n) where - field - pf : PFunc - f< : f f⊆ pf - g< : g f⊆ pf +open _f⊆_ -full-func : Set n -full-func = Nat → Two - -full→PF : (Nat → Two) → PFunc -full→PF f = record { restrict = λ x → One ; map = λ x _ → f x } +_f∩_ : (f g : PFunc) → PFunc +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) + ; map = λ x p → map f x (proj1 p) } _↑_ : (Nat → Two) → Nat → PFunc f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x } -record gf-filter (f : Nat → Two) (p : PFunc ) : Set (suc n) where +record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where field gn : Nat f