From cfe503e318de1e0204f8df19ffb5e27c2339d062 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Sat, 25 Jan 2025 14:50:23 -0300 Subject: [PATCH] def: higher inductive k-finite sets --- src/Data/Finset/Base.lagda.md | 608 ++++++++++++++++++++++++++++++++ src/Data/Finset/Properties.agda | 333 +++++++++++++++++ src/Data/Id/Base.lagda.md | 17 + src/Data/Id/Properties.agda | 13 - 4 files changed, 958 insertions(+), 13 deletions(-) create mode 100644 src/Data/Finset/Base.lagda.md create mode 100644 src/Data/Finset/Properties.agda diff --git a/src/Data/Finset/Base.lagda.md b/src/Data/Finset/Base.lagda.md new file mode 100644 index 000000000..7ed9b8805 --- /dev/null +++ b/src/Data/Finset/Base.lagda.md @@ -0,0 +1,608 @@ + + +```agda +module Data.Finset.Base where +``` + + + +# Finitely indexed subsets + +We define a type of finite(ly indexed) subsets of a type $A$, as a +higher inductive type mirroring the definition of lists, but with +generating equations which allow removing duplicates and reordering +elements. Note that we must also truncate the resulting type to make +sure we end up with something homotopically coherent. + +```agda +infixr 20 _∷_ + +data Finset {ℓ} (A : Type ℓ) : Type ℓ where + [] : Finset A + _∷_ : (x : A) (xs : Finset A) → Finset A + + ∷-dup : ∀ x xs → (x ∷ x ∷ xs) ≡ (x ∷ xs) + ∷-swap : ∀ x y xs → (x ∷ y ∷ xs) ≡ (y ∷ x ∷ xs) + + squash : is-set (Finset A) +``` + +Note that, since these are *equations* (rather than a separate +equivalence relation on lists), we do not need to add path constructors +saying that we can reorder elements deep in the list: + + + +```agda + _ : Path (Finset A) (w ∷ x ∷ y ∷ z ∷ []) (w ∷ x ∷ y ∷ y ∷ z ∷ []) + _ = ap (λ e → w Finset.∷ x Finset.∷ e) (sym (∷-dup y (z ∷ []))) +``` + + + +Of course, since finite sets and lists have the same point constructors, +we can turn any list into a finite set. + +```agda +from-list : List A → Finset A +from-list [] = [] +from-list (x ∷ xs) = x ∷ from-list xs +``` + +Moreover, we can show that this function is surjective; this implies +that the type of finite sets (over a set $A$) is a quotient of the type +of lists of $A$. + +```agda +from-list-is-surjective : is-surjective (from-list {A = A}) +from-list-is-surjective = Finset-elim-prop _ + (inc ([] , refl)) + (λ x → rec! λ xs p → inc (x ∷ xs , ap (x ∷_) p)) +``` + +## Basic operations + +We can replicate the definition of basic list operations on finite sets +essentially as-is, as long as we can prove that they respect the +generating paths --- that is, as long as whatever we choose to "replace +`_∷_`{.Agda} with" is also idempotent and allows swapping on the left. +For a basic example, we can swap conses with conses, to implement +`map`{.Agda}: + +```agda +mapᶠˢ : (A → B) → Finset A → Finset B +mapᶠˢ f [] = [] +mapᶠˢ f (x ∷ xs) = f x ∷ mapᶠˢ f xs +mapᶠˢ f (∷-dup x xs i) = ∷-dup (f x) (mapᶠˢ f xs) i +mapᶠˢ f (∷-swap x y xs i) = ∷-swap (f x) (f y) (mapᶠˢ f xs) i +mapᶠˢ f (squash x y p q i j) = squash (mapᶠˢ f x) (mapᶠˢ f y) (λ i → mapᶠˢ f (p i)) (λ i → mapᶠˢ f (q i)) i j +``` + + + +We can also implement `filter`{.Agda}, since at the end of the day we're +once again replacing conses with conses. + +```agda +cons-if : Dec B → A → Finset A → Finset A +cons-if (yes _) x xs = x ∷ xs +cons-if (no _) x xs = xs + +filter : (P : A → Type ℓ) ⦃ _ : ∀ {x} → Dec (P x) ⦄ → Finset A → Finset A +filter f [] = [] +filter f (x ∷ xs) = cons-if (holds? (f x)) x (filter f xs) +filter f (∷-dup x xs i) with holds? (f x) +... | yes _ = ∷-dup x (filter f xs) i +... | no _ = filter f xs +filter f (∷-swap x y xs i) with holds? (f x) | holds? (f y) +... | yes _ | yes _ = ∷-swap x y (filter f xs) i +... | yes _ | no _ = x ∷ filter f xs +... | no _ | yes _ = y ∷ filter f xs +... | no _ | no _ = filter f xs +filter f (squash x y p q i j) = squash (filter f x) (filter f y) (λ i → filter f (p i)) (λ i → filter f (q i)) i j +``` + +Finally, we can implement an append operation --- called `union` because +of its semantics as a subset --- since we're keeping all the conses and +replacing `[]`{.Agda} with a different finset. + +```agda +union : Finset A → Finset A → Finset A +union [] ys = ys +union (x ∷ xs) ys = x ∷ union xs ys +union (∷-dup x xs i) ys = ∷-dup x (union xs ys) i +union (∷-swap x y xs i) ys = ∷-swap x y (union xs ys) i +union (squash xs ys p q i j) zs = squash (union xs zs) (union ys zs) (λ i → union (p i) zs) (λ i → union (q i) zs) i j +``` + + + +### Properties of union + +One downside of the higher-inductive definition is that if we want to +define operations on finsets which use `union`{.Agda}, we'll have to +prove that it behaves sufficiently like `_∷_`{.Agda}. In particular, we +prove that it's a *semilattice*, which is sufficient (though more than +necessary) to imply it is idempotent and allows swapping on the left. + +All of these proofs are by induction on the leftmost finite set. Since +we're showing a proposition, it suffices to consider the point +constructors, in which case we essentially have the same proofs as for +lists (though written in higher-order style). + +```agda +abstract + union-assoc : (xs ys zs : Finset A) → xs <> (ys <> zs) ≡ (xs <> ys) <> zs + union-assoc = Finset-elim-prop _ + (λ ys zs → refl) + (λ x ih ys zs → ap (x ∷_) (ih ys zs)) + + union-idr : (xs : Finset A) → xs <> [] ≡ xs + union-idr = Finset-elim-prop _ refl λ x p → ap (x ∷_) p + + union-consr : (x : A) (xs ys : Finset A) → xs <> (x ∷ ys) ≡ (x ∷ xs) <> ys + union-consr x = Finset-elim-prop _ (λ ys → refl) + λ y ih ys → ap (y ∷_) (ih ys) ∙ ∷-swap _ _ _ + + union-comm : (xs ys : Finset A) → xs <> ys ≡ ys <> xs + union-comm = Finset-elim-prop _ (λ ys → sym (union-idr ys)) + λ x {xs} ih ys → sym (union-consr x ys xs ∙ ap (x ∷_) (sym (ih ys))) + + union-idem : (xs : Finset A) → xs <> xs ≡ xs + union-idem = Finset-elim-prop _ refl + λ x {xs} ih → ap (x ∷_) (union-consr x xs xs) ·· ∷-dup _ _ ·· ap (x ∷_) ih + + union-dup : (xs ys : Finset A) → xs <> (xs <> ys) ≡ xs <> ys + union-dup xs ys = union-assoc xs xs ys ∙ ap (_<> ys) (union-idem xs) + + union-swap : (xs ys zs : Finset A) → xs <> (ys <> zs) ≡ ys <> (xs <> zs) + union-swap xs ys zs = union-assoc xs ys zs ·· ap (_<> zs) (union-comm xs ys) ·· sym (union-assoc ys xs zs) +``` + +### More basic operations + +With these paths in hand, we can prove that `Finset`{.Agda} is a monad +on sets. First, we show how to flatten a finite set of finite sets, by +applying iterated unions. + +```agda +concat : Finset (Finset A) → Finset A +concat [] = [] +concat (x ∷ xs) = x <> concat xs +concat (∷-dup x xs i) = union-dup x (concat xs) i +concat (∷-swap x y xs i) = union-swap x y (concat xs) i +concat (squash x y p q i j) = squash + (concat x) (concat y) (λ i → concat (p i)) (λ i → concat (q i)) i j +``` + +We can then define a couple more operations familiar to functional +programmers. + +```agda +_<*>ᶠˢ_ : Finset (A → B) → Finset A → Finset B +[] <*>ᶠˢ xs = [] +(f ∷ fs) <*>ᶠˢ xs = mapᶠˢ f xs <> (fs <*>ᶠˢ xs) +∷-dup f fs i <*>ᶠˢ xs = union-dup (map f xs) (fs <*>ᶠˢ xs) i +∷-swap f g fs i <*>ᶠˢ xs = union-swap (map f xs) (map g xs) (fs <*>ᶠˢ xs) i +squash f g p q i j <*>ᶠˢ xs = squash + (f <*>ᶠˢ xs) (g <*>ᶠˢ xs) (λ i → p i <*>ᶠˢ xs) (λ i → q i <*>ᶠˢ xs) i j + +_>>=ᶠˢ_ : Finset A → (A → Finset B) → Finset B +[] >>=ᶠˢ f = [] +(x ∷ xs) >>=ᶠˢ f = f x <> (xs >>=ᶠˢ f) +∷-dup x xs i >>=ᶠˢ f = union-dup (f x) (xs >>=ᶠˢ f) i +∷-swap x y xs i >>=ᶠˢ f = union-swap (f x) (f y) (xs >>=ᶠˢ f) i +squash x y p q i j >>=ᶠˢ f = squash + (x >>=ᶠˢ f) (y >>=ᶠˢ f) (λ i → p i >>=ᶠˢ f) (λ i → q i >>=ᶠˢ f) i j +``` + + + +## Membership + + + +We now show how to define membership for finite sets. Since we have to +map into a set (to handle the `squash`{.Agda} constructor), we have to +make the result a proposition. Therefore, the definition of $x \in (y ∷ +xs)$ has to be truncated. + +```agda + finset-mem : A → Finset A → Prop (level-of A) + finset-mem x [] .∣_∣ = Lift _ ⊥ + finset-mem x (y ∷ xs) .∣_∣ = ∥ (x ≡ᵢ y) ⊎ ⌞ finset-mem x xs ⌟ ∥ + finset-mem x (∷-dup y xs i) .∣_∣ = dup (x ≡ᵢ y) ⌞ finset-mem x xs ⌟ i + finset-mem x (∷-swap y z xs i) .∣_∣ = swap (x ≡ᵢ y) (x ≡ᵢ z) ⌞ finset-mem x xs ⌟ i +``` + + + +We can then define a *case analysis* principle for membership in a +finite set, as long as we're showing a proposition. + +```agda +opaque + unfolding _∈ᶠˢ_ + + ∈ᶠˢ-split + : ∀ {ℓp} {x y : A} {xs} {P : x ∈ᶠˢ (y ∷ xs) → Type ℓp} ⦃ _ : ∀ {x} → H-Level (P x) 1 ⦄ + → ((p : x ≡ᵢ y) → P (hereₛ' p)) + → ((w : x ∈ᶠˢ xs) → P (thereₛ w)) + → (w : x ∈ᶠˢ (y ∷ xs)) → P w + ∈ᶠˢ-split ⦃ h ⦄ l r = ∥-∥-elim (λ x → hlevel 1 ⦃ h ⦄) λ where + (inl a) → l a + (inr b) → r b +``` + + + +Putting this together with induction over finite sets, we can show that +the membership type behaves as though it were an inductive family. + +```agda +∈ᶠˢ-elim + : ∀ {ℓp} {x : A} (P : ∀ xs → x ∈ᶠˢ xs → Type ℓp) ⦃ _ : ∀ {xs p} → H-Level (P xs p) 1 ⦄ + → (∀ {xs} → P (x ∷ xs) hereₛ) + → (∀ {y xs} q → P xs q → P (y ∷ xs) (thereₛ q)) + → ∀ xs w → P xs w +∈ᶠˢ-elim {x = x} P phere pthere xs w = Finset-elim-prop (λ xs → (w : x ∈ᶠˢ xs) → P xs w) + (λ m → absurd (¬mem-[] m)) + (λ y {xs'} ind → ∈ᶠˢ-split {P = P (y ∷ xs')} + (λ { reflᵢ → phere }) + λ w → pthere w (ind w)) + xs w +``` + +### Over discrete types + +We'll show that membership in a finite set is decidable, as long as the +type of elements is [[discrete]]. First, note that we're showing a +propostion, so all the path cases will be automatic. + +```agda +instance + Dec-∈ᶠˢ : ⦃ _ : Discrete A ⦄ {x : A} {xs : Finset A} → Dec (x ∈ xs) + Dec-∈ᶠˢ {A = A} ⦃ eq ⦄ {x = x} {xs} = go xs where + abstract + p : (xs : Finset A) → is-prop (Dec (x ∈ xs)) + p xs = hlevel 1 +``` + +We'll start with our inductive case: if we're looking at a finite set of +the form $y ∷ xs$, we can put together a decision for $x \in (y ∷ xs)$ +out of a decision for whether $x = y$ and a decision for whether $x \in +xs$. + +```agda + cons-mem + : (y : A) (xs : Finset A) + → Dec (x ≡ᵢ y) + → Dec ⌞ x ∈ xs ⌟ + → Dec ⌞ x ∈ (y ∷ xs) ⌟ +``` + +Note that, even though $x$ may also appear in $xs$, if it's at the head +position, we'll always return the "earlier" proof of membership --- this +matters when computing, even though we're dealing with propositions!. + +```agda + cons-mem y xs (yes p) _ = yes (hereₛ' p) + cons-mem y xs (no ¬p) (yes p) = yes (thereₛ p) + cons-mem y xs (no ¬p) (no ¬q) = no (∈ᶠˢ-split ¬p ¬q) +``` + +Finally, the base case is automatic: there are no elements in the empty +finite set. + +```agda + go : (xs : Finset A) → Dec (x ∈ xs) + go [] = no ¬mem-[] + go (y ∷ xs) = cons-mem y xs (x ≡ᵢ? y) (go xs) +``` + +
+It then suffices to remind Agda that all the path cases are +automatic. + +```agda + go (∷-dup y xs i) = is-prop→pathp (λ i → p (∷-dup y xs i)) + (cons-mem y (y ∷ xs) (x ≡ᵢ? y) (cons-mem y xs (x ≡ᵢ? y) (go xs))) + (cons-mem y xs (x ≡ᵢ? y) (go xs)) i + go (∷-swap y z xs i) = is-prop→pathp (λ i → p (∷-swap y z xs i)) + (cons-mem y (z ∷ xs) (x ≡ᵢ? y) (cons-mem z xs (x ≡ᵢ? z) (go xs))) + (cons-mem z (y ∷ xs) (x ≡ᵢ? z) (cons-mem y xs (x ≡ᵢ? y) (go xs))) i + go (squash x y q r i j) = is-prop→squarep (λ i j → p (squash x y q r i j)) (λ i → go x) (λ i → go (q i)) (λ i → go (r i)) (λ i → go y) i j +``` + +
+ +## Cardinality + +To close out this basic module, we show how to count the elements of a +finite set. In a list, you simply count the number of `_∷_`{.Agda} +constructors, but here, we must respect duplicates and swaps. This means +that, at each element, we must only add one to the count if the element +does not appear in the tail of the list. This implies that we can only +count the number of elements in a finite set with discrete carrier; it +also implies that computing the size of a `Finset` is *quadratic* in the +number of equality tests. + +```agda +module _ {A : Type ℓ} ⦃ d : Discrete A ⦄ where + count : Finset A → Nat + + private + has : (x : A) (xs : Finset A) → Dec (x ∈ xs) + has x xs = holds? (x ∈ xs) + + cons : A → Finset A → Nat + cons x xs = Dec-rec (λ _ → count xs) (λ _ → suc (count xs)) (has x xs) + + cons-dup : ∀ x xs → cons x (x ∷ xs) ≡ cons x xs + cons-swap : ∀ x y xs → cons x (y ∷ xs) ≡ cons y (x ∷ xs) + + count [] = 0 + count (x ∷ xs) = cons x xs + count (∷-dup x xs i) = cons-dup x xs i + count (∷-swap x y xs i) = cons-swap x y xs i + count (squash x y p q i j) = hlevel 2 (count x) (count y) (λ i → count (p i)) (λ i → count (q i)) i j +``` + +
+Showing the necessary respect for the generating equations +boils down to a billion case splits. + +```agda + cons-dup x xs with has x xs + cons-dup x xs | yes p with has x (x ∷ xs) + cons-dup x xs | yes p | yes q = refl + cons-dup x xs | yes p | no ¬p = absurd (¬p hereₛ) + cons-dup x xs | no ¬p with has x (x ∷ xs) + cons-dup x xs | no ¬p | yes q = refl + cons-dup x xs | no ¬p | no ¬q = absurd (¬q hereₛ) + + cons-swap x y xs with has x (y ∷ xs) | has y (x ∷ xs) | has x xs | has y xs + ... | yes p | yes q | yes r | yes s = refl + ... | yes p | yes q | no ¬r | no ¬s = refl + ... | yes p | no ¬q | yes r | no ¬s = refl + ... | no ¬p | yes q | no ¬r | yes s = refl + ... | no ¬p | no ¬q | yes r | yes s = refl + ... | no ¬p | no ¬q | no ¬r | no ¬s = refl + ... | yes p | yes q | yes r | no ¬s = ∈ᶠˢ-split (λ { reflᵢ → absurd (¬s r) }) (λ w → absurd (¬s w)) q + ... | yes p | yes q | no ¬r | yes s = ∈ᶠˢ-split (λ { reflᵢ → absurd (¬r s) }) (λ w → absurd (¬r w)) p + ... | yes p | no ¬q | yes r | yes s = absurd (¬q (thereₛ s)) + ... | yes p | no ¬q | no ¬r | yes s = absurd (¬q (thereₛ s)) + ... | yes p | no ¬q | no ¬r | no ¬s = ∈ᶠˢ-split (λ { reflᵢ → absurd (¬q p) }) (λ w → absurd (¬r w)) p + ... | no ¬p | yes q | yes r | yes s = ∈ᶠˢ-split (λ { reflᵢ → absurd (¬p q) }) (λ w → absurd (¬p ((thereₛ r)))) q + ... | no ¬p | yes q | yes r | no ¬s = absurd (¬p (thereₛ r)) + ... | no ¬p | yes q | no ¬r | no ¬s = ∈ᶠˢ-split (λ { reflᵢ → absurd (¬p q) }) (λ w → absurd (¬s w)) q + ... | no ¬p | no ¬q | yes r | no ¬s = absurd (¬p (thereₛ r)) + ... | no ¬p | no ¬q | no ¬r | yes s = absurd (¬q (thereₛ s)) +``` + + + diff --git a/src/Data/Finset/Properties.agda b/src/Data/Finset/Properties.agda new file mode 100644 index 000000000..92ddf604d --- /dev/null +++ b/src/Data/Finset/Properties.agda @@ -0,0 +1,333 @@ +open import 1Lab.Prelude + +open import Data.List.Membership +open import Data.Finset.Base +open import Data.Sum.Base +open import Data.Nat.Base +open import Data.Dec + +import 1Lab.Reflection + +open 1Lab.Reflection using (Idiom-TC ; lit ; nat ; con₀ ; List ; [] ; _∷_) + +module Data.Finset.Properties where + +private variable + ℓ ℓ' ℓ'' : Level + A B C : Type ℓ + +map-∈ᶠˢ : (f : A → B) {x : B} (xs : Finset A) → x ∈ mapᶠˢ f xs → ∃[ (y , _) ∈ fibreᵢ f x ] y ∈ xs +map-∈ᶠˢ f {x} xs w = Finset-elim-prop (λ xs → x ∈ mapᶠˢ f xs → ∃[ (y , _) ∈ fibreᵢ f x ] y ∈ xs) + (λ w → absurd (¬mem-[] w)) + (λ y ind → ∈ᶠˢ-split (λ { p → inc ((y , symᵢ p) , hereₛ) }) λ w → case ind w of λ x p h → inc ((x , p) , thereₛ h)) + xs w + +∈ᶠˢ-map : ∀ (f : A → B) {x} (xs : Finset A) → x ∈ᶠˢ xs → f x ∈ᶠˢ mapᶠˢ f xs +∈ᶠˢ-map f {x} = ∈ᶠˢ-elim (λ xs _ → f x ∈ᶠˢ map f xs) hereₛ (λ q → thereₛ) + +∈ᶠˢ-filter : ∀ {P : A → Type ℓ} ⦃ d : ∀ {x} → Dec (P x) ⦄ {x : A} xs → x ∈ᶠˢ xs → P x → x ∈ᶠˢ filter P xs +∈ᶠˢ-filter {P = P} ⦃ d ⦄ {x} xs mem px = ∈ᶠˢ-elim (λ xs _ → x ∈ᶠˢ filter P xs) + (λ {xs} → case d {x} return (λ p → x ∈ᶠˢ cons-if p x (filter P xs)) of λ { (yes _) → hereₛ ; (no ¬px) → absurd (¬px px)}) + (λ {y} {xs} q ind → case d {y} return (λ p → x ∈ᶠˢ cons-if p y (filter P xs)) of λ { (yes _) → thereₛ ind ; (no ¬px) → ind }) + xs mem + +filter-∈ᶠˢ : ∀ {P : A → Type ℓ} ⦃ d : ∀ {x} → Dec (P x) ⦄ {x : A} xs → x ∈ᶠˢ filter P xs → ∥ P x ∥ +filter-∈ᶠˢ {P = P} ⦃ d = d ⦄ {x = x} = Finset-elim-prop (λ xs → x ∈ filter P xs → ∥ P x ∥) + (λ w → absurd (¬mem-[] w)) + (λ y {xs} ind → case d {y} return (λ p → x ∈ᶠˢ cons-if p y (filter P xs) → ∥ P x ∥) of λ where + (yes py) → ∈ᶠˢ-split (λ p → inc (substᵢ P (symᵢ p) py)) ind + (no ¬py) q → ind q) + +uncons : (x : A) (xs : Finset A) → x ∈ᶠˢ xs → xs ≡ x ∷ xs +uncons x = Finset-elim-prop _ (λ x → absurd (¬mem-[] x)) λ y {xs} ih → ∈ᶠˢ-split + (λ { reflᵢ → sym (∷-dup _ _) }) + (λ w → ap (y ∷_) (ih w) ∙ ∷-swap _ _ _) + +∈ᶠˢ-unionl : (x : A) (xs ys : Finset A) → x ∈ᶠˢ xs → x ∈ᶠˢ (xs <> ys) +∈ᶠˢ-unionl x xs ys p = ∈ᶠˢ-elim (λ xs _ → x ∈ᶠˢ (xs <> ys)) hereₛ (λ q x → thereₛ x) xs p + +∈ᶠˢ-unionr : (x : A) (xs ys : Finset A) → x ∈ᶠˢ ys → x ∈ᶠˢ (xs <> ys) +∈ᶠˢ-unionr x xs ys p = Finset-elim-prop (λ xs → x ∈ᶠˢ (xs <> ys)) p (λ x p → thereₛ p) xs + +∈ᶠˢ-union : (x : A) (xs ys : Finset A) → x ∈ᶠˢ (xs <> ys) → ∥ (x ∈ᶠˢ xs) ⊎ (x ∈ᶠˢ ys) ∥ +∈ᶠˢ-union x = Finset-elim-prop _ (λ ys w → inc (inr w)) λ x {xs} ind ys → + ∈ᶠˢ-split (λ p → inc (inl (hereₛ' p))) + λ w → case ind ys w of λ where + (inl h) → inc (inl (thereₛ h)) + (inr t) → inc (inr t) + +sigma-∈ᶠˢ + : ∀ {ℓ ℓ'} {A : Type ℓ} {P : A → Type ℓ'} {x y} + → ∀ (f : ∀ x → Finset (P x)) xs + → x ∈ᶠˢ xs → y ∈ᶠˢ f x → (x , y) ∈ᶠˢ sigma xs f +sigma-∈ᶠˢ {P = P} {x = x₀} {y = y₀} f xs mx my = ∈ᶠˢ-elim (λ xs _ → (y : P x₀) → y ∈ f x₀ → (x₀ , y) ∈ sigma xs f) + (λ {xs} y ym → ∈ᶠˢ-unionl (x₀ , y) (map (x₀ ,_) (f x₀)) (sigma xs f) (∈ᶠˢ-map (x₀ ,_) (f x₀) ym)) + (λ {y} {xs} q ind py ym → ∈ᶠˢ-unionr (x₀ , py) (map (y ,_) (f y)) (sigma xs f) (ind py ym)) + xs mx y₀ my + +∈ᶠˢ-sigma + : ∀ {ℓ ℓ'} {A : Type ℓ} {P : A → Type ℓ'} {x y} (f : ∀ x → Finset (P x)) xs + → (x , y) ∈ᶠˢ sigma xs f → x ∈ xs × y ∈ f x +∈ᶠˢ-sigma {P = P} {x = x} {y} f = Finset-elim-prop (λ xs → (x , y) ∈ᶠˢ sigma xs f → x ∈ xs × y ∈ f x) + (λ w → absurd (¬mem-[] w)) + (λ x' {xs} ind w → case ∈ᶠˢ-union (x , y) (map (x' ,_) (f x')) (sigma xs f) w of λ where + (inl w) → case map-∈ᶠˢ (x' ,_) (f x') w of λ px' pf mem → + let (p , q) = id-Σ (symᵢ pf) in + Jᵢ (λ x' p → ∀ px' (q : Id-over P p y px') → px' ∈ᶠˢ f x' → (x ∈ᶠˢ (x' ∷ xs)) × (y ∈ᶠˢ f x)) + (λ px'' → Jᵢ (λ px'' _ → px'' ∈ f x → (x ∈ (x ∷ xs)) × (y ∈ f x)) (hereₛ ,_)) + p px' q mem + (inr w) → case ind w of λ h1 h2 → thereₛ h1 , h2) + +intersection-∈ᶠˢ : ⦃ _ : Discrete A ⦄ (x : A) (xs ys : Finset A) → x ∈ xs → x ∈ ys → x ∈ intersection xs ys +intersection-∈ᶠˢ x xs ys mxs mys = ∈ᶠˢ-elim (λ xs _ → x ∈ intersection xs ys) + (λ {xs} → caseᵈ x ∈ ys return (λ p → x ∈ cons-if p x (intersection xs ys)) of λ where + (yes _) → hereₛ + (no ¬mys) → absurd (¬mys mys)) + (λ {y} {xs} w q → there-cons-if (holds? _) y x (intersection xs ys) q) + xs mxs + +∈ᶠˢ-intersection : ⦃ d : Discrete A ⦄ (x : A) (xs ys : Finset A) → x ∈ intersection xs ys → (x ∈ xs) × (x ∈ ys) +∈ᶠˢ-intersection x xs ys w = Finset-elim-prop (λ xs → x ∈ intersection xs ys → x ∈ xs × x ∈ ys) + (λ w → absurd (¬mem-[] w)) + (λ y {tl} ind → caseᵈ (y ∈ ys) return (λ p → x ∈ cons-if p y (intersection tl ys) → x ∈ (y ∷ tl) × x ∈ ys) of λ where + (yes q) → ∈ᶠˢ-split (λ p → substᵢ (λ e → x ∈ᶠˢ (e ∷ tl)) p hereₛ , substᵢ (_∈ᶠˢ ys) (symᵢ p) q) λ w → case ind w of λ a b → thereₛ a , b + (no ¬p) mem → case ind mem of λ a b → thereₛ a , b) + xs w + +from-list-∈ᶠˢ : ∀ {x : A} {xs} → x ∈ᶠˢ from-list xs → ∥ x ∈ₗ xs ∥ +from-list-∈ᶠˢ {xs = []} p = absurd (¬mem-[] p) +from-list-∈ᶠˢ {xs = x ∷ xs} = ∈ᶠˢ-split (λ p → inc (here p)) (λ w → there <$> from-list-∈ᶠˢ w) + +∈ᶠˢ-from-list : ∀ {x : A} {xs} → x ∈ₗ xs → x ∈ᶠˢ from-list xs +∈ᶠˢ-from-list (here p) = hereₛ' p +∈ᶠˢ-from-list (there x) = thereₛ (∈ᶠˢ-from-list x) + +instance + Dec-All + : ∀ {P : A → Type ℓ} ⦃ _ : ∀ {x} → H-Level (P x) 1 ⦄ ⦃ d : ∀ {x} → Dec (P x) ⦄ {xs : Finset A} + → Dec (All P xs) + Dec-All {P = P} {xs} = Finset-elim-prop (λ xs → Dec (All P xs)) (yes all-nil) + (λ { x (yes xs) → caseᵈ P x of λ { (yes x) → yes (all-cons x xs) ; (no ¬x) → no (λ xxs → ¬x (from-all _ xxs hereₛ) )} + ; _ (no ¬xs) → no (λ xxs → ¬xs (to-all _ (λ x w → from-all _ xxs (thereₛ w)))) + }) + xs + +abstract + subset→is-union : (xs ys : Finset A) → xs ⊆ ys → ys ≡ (xs <> ys) + subset→is-union = Finset-elim-prop _ (λ ys p → refl) λ x {xs} ih ys sube → + ys ≡⟨ uncons x ys (sube x hereₛ) ⟩ + x ∷ ys ≡⟨ ap (x ∷_) (ih ys λ x x∈xs → sube x (thereₛ x∈xs)) ⟩ + x ∷ (xs <> ys) ∎ + + finset-ext : {xs ys : Finset A} → xs ⊆ ys → ys ⊆ xs → xs ≡ ys + finset-ext {xs = xs} {ys} p1 p2 = + let + p : xs ≡ (ys <> xs) + p = subset→is-union ys xs p2 + + q : ys ≡ (xs <> ys) + q = subset→is-union xs ys p1 + in p ·· union-comm ys xs ·· sym q + +instance + Discrete-Finset : ⦃ _ : Discrete A ⦄ → Discrete (Finset A) + Discrete-Finset {x = xs} {ys} = case holds? (All (_∈ᶠˢ ys) xs × All (_∈ᶠˢ xs) ys) of λ where + (yes (s1 , s2)) → yes $ finset-ext (λ a → from-all _ s1) (λ a → from-all _ s2) + (no ¬sub) → no λ p → ¬sub (to-all xs (λ a → subst (a ∈_) p) , to-all ys (λ a → subst (a ∈_) (sym p))) + +-- record Finite {ℓ} (A : Type ℓ) : Type ℓ where +-- field +-- univ : Finset A +-- has : (x : A) → x ∈ univ + +-- open Finite + +-- instance +-- H-Level-Finite : ∀ {n} → H-Level (Finite A) (suc n) +-- H-Level-Finite = prop-instance {T = Finite _} λ where +-- x y i .univ → finset-ext (λ a _ → y .has a) (λ a _ → x .has a) i +-- x y i .has a → is-prop→pathp (λ i → hlevel {T = a ∈ᶠˢ finset-ext (λ a _ → y .has a) (λ a _ → x .has a) i} 1) (x .has a) (y .has a) i + +-- open import Data.Fin.Base + +-- test : Finite A → ∃[ n ∈ Nat ] (Fin n ↠ A) +-- test record { univ = xs ; has = h } = do +-- (xs , p) ← from-list-surj xs + +-- let +-- surj : is-surjective (xs !_) +-- surj a = do +-- (ix , p) ← member→lookup <$> from-list-mem {xs = xs} (subst (a ∈ᶠˢ_) (sym p) (h a)) +-- pure (ix , Id≃path.to p) + +-- pure (length xs , (xs !_) , surj) + +-- instance +-- Finite-⊤ : Finite ⊤ +-- Finite-⊤ = record { univ = pure tt ; has = λ x → hereₛ } + +-- Finite-⊥ : Finite ⊥ +-- Finite-⊥ = record { univ = [] ; has = λ () } + +-- Finite-⊎ : ⦃ _ : Finite A ⦄ ⦃ _ : Finite B ⦄ → Finite (A ⊎ B) +-- Finite-⊎ ⦃ a ⦄ ⦃ b ⦄ .univ = map inl (a .univ) <> map inr (b .univ) +-- Finite-⊎ ⦃ a ⦄ ⦃ b ⦄ .has (inl x) = ∈ᶠˢ-unionl (inl x) (map inl (a .univ)) _ (∈ᶠˢ-map inl (a .univ) (a .has x)) +-- Finite-⊎ ⦃ a ⦄ ⦃ b ⦄ .has (inr x) = ∈ᶠˢ-unionr (inr x) (map inl (a .univ)) _ (∈ᶠˢ-map inr (b .univ) (b .has x)) + +-- Finite-Fin : ∀ {n} → Finite (Fin n) +-- Finite-Fin {n} = record { univ = n-univ n ; has = n-has n } where +-- n-univ : ∀ n → Finset (Fin n) +-- n-univ zero = [] +-- n-univ (suc n) = fzero ∷ map fsuc (n-univ n) + +-- n-has : ∀ n (x : Fin n) → x ∈ n-univ n +-- n-has _ f with fin-view f +-- ... | zero = hereₛ +-- ... | suc x = thereₛ (∈ᶠˢ-map fsuc _ (n-has _ x)) + +-- Finite-Σ : {P : A → Type ℓ} ⦃ _ : Finite A ⦄ ⦃ _ : ∀ {x} → Finite (P x) ⦄ → Finite (Σ A P) +-- Finite-Σ ⦃ a ⦄ ⦃ f ⦄ .univ = sigma (a .univ) (λ a → f {a} .univ) +-- Finite-Σ ⦃ a ⦄ ⦃ f ⦄ .has (x , y) = sigma-∈ᶠˢ (λ a → f {a} .univ) (a .univ) (a .has x) (f {x} .has y) + +-- Finite-Lift : ⦃ _ : Finite A ⦄ → Finite (Lift ℓ A) +-- Finite-Lift ⦃ a ⦄ .univ = map lift (a .univ) +-- Finite-Lift ⦃ a ⦄ .has (lift x) = ∈ᶠˢ-map lift _ (a .has x) + +-- -- xs : Finite (Fin 3 × Fin 3 × Fin 3) +-- -- xs = auto + +-- -- _ = {! (λ x → (fst x , fst (snd x))) <$> test xs !} + +-- -- Discrete-⊤ : Discrete ⊤ +-- -- Discrete-⊤ = yes refl + +-- open import Data.List.Membership +-- open import Data.List.Base hiding (count) +-- open import Data.Bool +-- import Data.List.Quantifiers as List + +-- finset→list : ⦃ _ : Discrete A ⦄ (xs : Finset A) → ∃[ l ∈ List A ] ((∀ (x : A) → x ∈ xs → is-contr (x ∈ l)) × ((x : A) → x ∈ l → x ∈ xs)) +-- finset→list {A = A} = go where +-- instance +-- _ : H-Level A 2 +-- _ = basic-instance 2 (Discrete→is-set auto) + +-- enum : (xs : Finset A) → Type _ +-- enum xs = ∃[ l ∈ List A ] ((∀ (x : A) → x ∈ xs → is-contr (x ∈ l)) × ((x : A) → x ∈ l → x ∈ xs)) + +-- enump : (xs : Finset A) → is-prop (enum xs) +-- enump xs = squash + +-- enum-cons : (x : A) (xs : Finset A) → enum xs → enum (x ∷ xs) +-- enum-cons x xs (inc (l , find , dinf)) with holds? (x ∈ xs) +-- ... | yes in-xs = inc (l , find' , dinf') where +-- find' : (y : A) → y ∈ᶠˢ (x ∷ xs) → is-contr (y ∈ₗ l) +-- find' x = ∈ᶠˢ-split (λ p → find x (substᵢ (_∈ xs) (symᵢ p) in-xs)) (find _) + +-- dinf' : (y : A) → y ∈ₗ l → y ∈ᶠˢ (x ∷ xs) +-- dinf' y w = case (x ≡ᵢ? y) of λ { (yes reflᵢ) → hereₛ ; (no ¬x=y) → thereₛ (dinf y w) } +-- ... | no ¬in-xs = inc (x ∷ l , find' , dinf') where +-- find' : (y : A) → y ∈ᶠˢ (x ∷ xs) → is-contr (y ∈ₗ (x ∷ l)) +-- find' y = ∈ᶠˢ-split +-- (λ p → contr (here p) (λ { (here q) → ap here prop! ; (there q) → absurd (¬in-xs (dinf _ (substᵢ (_∈ l) p q))) })) +-- (λ w → let c = find _ w in contr (there (c .centre)) (λ { (here p) → absurd (¬in-xs (dinf x (substᵢ (_∈ l) p (c .centre)))) ; (there q) → ap there (c .paths q)})) + +-- dinf' : (y : A) → y ∈ₗ (x ∷ l) → y ∈ᶠˢ (x ∷ xs) +-- dinf' y (here p) = hereₛ' p +-- dinf' y (there w) = thereₛ (dinf y w) + +-- enum-cons x xs (squash a b i) = squash (enum-cons x xs a) (enum-cons x xs b) i + +-- go : ∀ xs → enum xs +-- go' : (x : A) (xs : Finset A) → enum (x ∷ xs) +-- go' x xs = enum-cons x xs (go xs) + +-- go [] = inc ([] , (λ x m → absurd (¬mem-[] m)) , λ a ()) +-- go (x ∷ xs) = enum-cons x xs (go xs) +-- go (∷-dup x xs i) = is-prop→pathp (λ i → enump (∷-dup x xs i)) (enum-cons x (x ∷ xs) (go' x xs)) (go' x xs) i +-- go (∷-swap x y xs i) = is-prop→pathp (λ i → enump (∷-swap x y xs i)) (enum-cons x _ (go' y xs)) (enum-cons y _ (go' x xs)) i +-- go (squash x y p q i j) = is-prop→squarep (λ i j → enump (squash x y p q i j)) (λ i → go x) (λ i → go (p i)) (λ i → go (q i)) (λ i → go y) i j + +-- -- pi : {P : A → Type ℓ} (xs : Finset A) → (∀ x → Finset (P x)) → Finset ((x : A) → x ∈ xs → P x) +-- -- pi [] p = pure λ _ m → absurd (¬mem-[] m) +-- -- pi (x ∷ xs) p = p x >>= λ a → map (λ f x m → {! ∈ᶠˢ-split m ? ? !}) (pi xs p) +-- -- pi (∷-dup x xs i) p = {! !} +-- -- pi (∷-swap x y xs i) p = {! !} +-- -- pi (squash xs xs₁ x y i i₁) p = {! !} + +-- -- Prod : List A → (P : A → Type ℓ) → Type (level-of A ⊔ ℓ) +-- -- Prod [] P = Lift _ ⊤ +-- -- Prod (x ∷ xs) P = P x × Prod xs P + +-- -- module _ (P : A → Type ℓ) where +-- -- prod→part : (xs : List A) → Prod xs P → (x : A) → x ∈ xs → P x +-- -- prod→part .(_ ∷ _) (pa , pr) a (here q) = subst P (sym q) pa +-- -- prod→part .(_ ∷ _) (pa , pr) a (there w) = prod→part _ pr a w + +-- -- part→prod : (xs : List A) → ((x : A) → x ∈ xs → P x) → Prod xs P +-- -- part→prod [] f = lift tt +-- -- part→prod (x ∷ xs) f = f x (here refl) , part→prod xs (λ a w → f a (there w)) + +-- -- prod→part→prod : (xs : List A) (p : Prod xs P) → part→prod xs (prod→part xs p) ≡ p +-- -- prod→part→prod [] p = refl +-- -- prod→part→prod (x ∷ xs) (px , pr) = transport-refl px ,ₚ prod→part→prod xs pr + +-- -- part→prod→part : (xs : List A) (f : (x : A) → x ∈ xs → P x) (x : A) (w : x ∈ xs) → prod→part xs (part→prod xs f) x w ≡ f x w +-- -- part→prod→part (x ∷ xs) f x' (here p) = J' (λ a b q → (f : (y : A) → y ∈ₗ (b ∷ xs) → P y) → subst P (sym q) (f b (here refl)) ≡ f a (here q)) (λ x f → transport-refl _) p f +-- -- part→prod→part (_ ∷ xs) f x (there w) = part→prod→part xs (λ y w → f y (there w)) x w + +-- -- finite-prod : (xs : List A) → (∀ x → Finite (P x)) → Finite (Prod xs P) +-- -- finite-prod [] f = auto +-- -- finite-prod (x ∷ xs) f = Finite-Σ ⦃ f x ⦄ ⦃ λ {_} → finite-prod xs f ⦄ + +-- -- instance +-- -- Finite-Π : {P : A → Type ℓ} ⦃ _ : Finite A ⦄ ⦃ _ : Discrete A ⦄ ⦃ _ : ∀ {x} → Finite (P x) ⦄ → Finite ((x : A) → P x) +-- -- Finite-Π {A = A} {P = P} ⦃ fa ⦄ ⦃ da ⦄ = done where +-- -- instance +-- -- _ : H-Level A 2 +-- -- _ = basic-instance 2 (Discrete→is-set auto) + +-- -- done : Finite ((x : A) → P x) +-- -- done = ∥-∥-out! do +-- -- (l , find , _) ← finset→list (fa .univ) + +-- -- let +-- -- fin-prod : Finite (Pi l P) +-- -- fin-prod = finite-prod P l (λ _ → auto) + +-- -- to : Prod l P → (x : A) → P x +-- -- to p a = prod→part P l p a (find a (fa .has a) .centre) + +-- -- univ' : Finset ((x : A) → P x) +-- -- univ' = map to (fin-prod .univ) + +-- -- find' : (f : ∀ x → P x) → f ∈ univ' +-- -- find' f = +-- -- let +-- -- ix = fin-prod .has (part→prod P l (λ a _ → f a)) +-- -- ix' = ∈ᶠˢ-map to (fin-prod .univ) ix +-- -- in subst (_∈ᶠˢ univ') (funext λ a → part→prod→part P l (λ a _ → f a) a (find a (fa .has a) .centre)) ix' + +-- -- pure (record { univ = univ' ; has = find' }) + +-- -- module _ {P : A → Type ℓ} ⦃ fa : Finite A ⦄ ⦃ _ : ∀ {x} → Discrete (P x) ⦄ {f g : ∀ x → P x} where +-- -- private +-- -- instance +-- -- _ : ∀ {x} → H-Level (P x) 2 +-- -- _ = basic-instance 2 (Discrete→is-set auto) + +-- -- to : ⌞ finset-all (λ x → f x ≡ g x) (fa .univ) ⌟ → f ≡ g +-- -- to xs = funext λ a → finset-all-ix (λ x → f x ≡ g x) (fa .univ) xs (fa .has a) + +-- -- from : f ≡ g → ⌞ finset-all (λ x → f x ≡ g x) (fa .univ) ⌟ +-- -- from h = to-finset-all (λ x → f x ≡ g x) (fa .univ) λ {x} _ → happly h x + +-- -- dec : Dec ⌞ finset-all (λ x → f x ≡ g x) (fa .univ) ⌟ +-- -- dec = finset-all-dec (λ x → f x ≡ g x) (fa .univ) + +-- -- instance +-- -- Discrete-Π : Dec (f ≡ g) +-- -- Discrete-Π with dec +-- -- ... | yes p = yes (to p) +-- -- ... | no ¬p = no λ h → ¬p (from h) +-- ``` diff --git a/src/Data/Id/Base.lagda.md b/src/Data/Id/Base.lagda.md index 2991e387c..1b98c5ded 100644 --- a/src/Data/Id/Base.lagda.md +++ b/src/Data/Id/Base.lagda.md @@ -232,5 +232,22 @@ fibreᵢ : (f : A → B) (y : B) → Type _ fibreᵢ {A = A} f y = Σ[ x ∈ A ] (f x ≡ᵢ y) infix 7 _≡ᵢ_ + +Σ-id : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y : Σ A B} (p : x .fst ≡ᵢ y .fst) → Id-over B p (x .snd) (y .snd) → x ≡ᵢ y +Σ-id reflᵢ reflᵢ = reflᵢ + +apᵢ-apᵢ + : (f : B → C) (g : A → B) {x y : A} (p : x ≡ᵢ y) + → apᵢ f (apᵢ g p) ≡ᵢ apᵢ (f ∘ g) p +apᵢ-apᵢ f g reflᵢ = reflᵢ + +id-Σ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y : Σ A B} (p : x ≡ᵢ y) → Σ[ p ∈ x .fst ≡ᵢ y .fst ] Id-over B p (x .snd) (y .snd) +id-Σ {B = B} {x} {y} p = apᵢ fst p , substᵢ (λ e → transportᵢ e (x .snd) ≡ᵢ (y .snd)) (symᵢ (apᵢ-apᵢ B fst p)) (apdᵢ snd p) + +happlyᵢ : {f g : ∀ x → P x} → f ≡ᵢ g → (x : A) → f x ≡ᵢ g x +happlyᵢ reflᵢ x = reflᵢ + +funextᵢ : ∀ {A : Type ℓ} {B : A → Type ℓ'} {f g : ∀ x → B x} (h : ∀ x → f x ≡ᵢ g x) → f ≡ᵢ g +funextᵢ h = Id≃path.from (funext (λ a → Id≃path.to (h a))) ``` --> diff --git a/src/Data/Id/Properties.agda b/src/Data/Id/Properties.agda index eb0718a3d..2db423431 100644 --- a/src/Data/Id/Properties.agda +++ b/src/Data/Id/Properties.agda @@ -17,10 +17,6 @@ symᵢ-symᵢ reflᵢ = refl symᵢ-from : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) → symᵢ (Id≃path.from p) ≡ Id≃path.from (sym p) symᵢ-from = J (λ y p → symᵢ (Id≃path.from p) ≡ Id≃path.from (sym p)) (ap symᵢ (transport-refl reflᵢ) ∙ sym (transport-refl reflᵢ)) -apᵢ-apᵢ - : (f : B → C) (g : A → B) {x y : A} (p : x ≡ᵢ y) - → apᵢ f (apᵢ g p) ≡ᵢ apᵢ (f ∘ g) p -apᵢ-apᵢ f g reflᵢ = reflᵢ apᵢ-from : (f : A → B) {x y : A} (p : x ≡ y) → apᵢ f (Id≃path.from p) ≡ Id≃path.from (ap f p) apᵢ-from f = J (λ y p → apᵢ f (Id≃path.from p) ≡ Id≃path.from (ap f p)) (ap (apᵢ f) (transport-refl reflᵢ) ∙ sym (transport-refl reflᵢ)) @@ -28,17 +24,8 @@ apᵢ-from f = J (λ y p → apᵢ f (Id≃path.from p) ≡ Id≃path.from (ap f apᵢ-symᵢ : (f : A → B) (p : x ≡ᵢ y) → apᵢ f (symᵢ p) ≡ᵢ symᵢ (apᵢ f p) apᵢ-symᵢ f reflᵢ = reflᵢ -Σ-id : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y : Σ A B} (p : x .fst ≡ᵢ y .fst) → Id-over B p (x .snd) (y .snd) → x ≡ᵢ y -Σ-id reflᵢ reflᵢ = reflᵢ - symPᵢ : {a b : A} {x : P a} {y : P b} (p : a ≡ᵢ b) → Id-over P p x y → Id-over P (symᵢ p) y x symPᵢ reflᵢ reflᵢ = reflᵢ symPᵢ⁻ : {a b : A} {x : P a} {y : P b} (p : a ≡ᵢ b) → Id-over P (symᵢ p) y x → Id-over P p x y symPᵢ⁻ reflᵢ reflᵢ = reflᵢ - -happlyᵢ : {f g : ∀ x → P x} → f ≡ᵢ g → (x : A) → f x ≡ᵢ g x -happlyᵢ reflᵢ x = reflᵢ - -funextᵢ : ∀ {A : Type ℓ} {B : A → Type ℓ'} {f g : ∀ x → B x} (h : ∀ x → f x ≡ᵢ g x) → f ≡ᵢ g -funextᵢ h = Id≃path.from (funext (λ a → Id≃path.to (h a)))