Finite Decidable Setoids

module FDS where

record FinDecEq {a} (n : ℕ) : Set (lsuc a) where

  field

    _ω_ : Rel (Fin n) a

    isDecEq : IsDecEquivalence _ω_

  std : DecSetoid _ _

  std = record { Carrier = (Fin n) ;

                _≈_ = _ω_ ;

                isDecEquivalence = isDecEq }

  open DecSetoid std

    renaming (_≟_ to _ω?_ ;

              refl to ω-refl ;

              sym to ω-sym ;

              trans to ω-transitive ;

              Carrier to F)

    public

  [_]ω : F → Subset n

  [ o ]ω = Vec.tabulate (does ∘ (_ω? o))

open import Level

open import Data.Nat.Base

open import FDS using (FinDecEq)

module FDS.Properties {a : Level} {n : ℕ} {FDS : FinDecEq {a} n} where

open import FDS.Fin.Subset.Lemmas

open import FDS.List.AllPairs.Lemmas

open FinDecEq FDS

import Data.List.Membership.Propositional

module MP = Data.List.Membership.Propositional {A = F}

open MP renaming (_∈_ to _∈ℓ_)

open import Data.List.Membership.Propositional.Properties

lmap = List.map

syntax lmap (λ x → B) L = ⟦ B ∣ x 𝕚𝕟 L ⟧

Fˡ = List.allFin n

ω⇒∈ : ∀ {x y} → x ω y → x ∈ [ y ]ω

ω⇒∈ {x} {y} xωy = let lkp = begin 

                              Vec.lookup [ y ]ω x ≡⟨ lookup∘tabulate _ x ⟩

                              does (x ω? y) ≡⟨ dec-true (x ω? y) xωy ⟩

                              true ∎

                  in lookup⇒[]= x [ y ]ω lkp

o∈[o]ω : ∀ { o : F } → o ∈ [ o ]ω

o∈[o]ω = ω⇒∈ ω-refl

∈⇒ω : ∀ {x y} → x ∈ [ y ]ω → x ω y

∈⇒ω {x} {y} x∈[y] = 

  let w = begin

            isYes (x ω? y) ≡⟨ isYes≗does _ ⟩ 

            does (x ω? y)  ≡˘⟨ lookup∘tabulate _ x ⟩

            Vec.lookup [ y ]ω x ≡⟨ []=⇒lookup x∈[y] ⟩

            true ∎

      ≡→T : ∀ {b : Bool} → b ≡ true → T b

      ≡→T = λ { refl → tt }

      r : True (x ω? y)

      r = ≡→T w

  in toWitness r

ω⇒⊆ : ∀ {x y} → x ω y → [ x ]ω ⊆ [ y ]ω

ω⇒⊆ {x} {y} xωy s∈[x] = ω⇒∈ (ω-transitive (∈⇒ω s∈[x]) xωy )

ω⇒≡ : ∀ {x y} → x ω y → [ x ]ω ≡ [ y ]ω

ω⇒≡ {x} {y} xωy = ⊆-antisym (ω⇒⊆ xωy) (ω⇒⊆ (ω-sym xωy))

cc : F → F

cc f = index {n} [ f ]ω ( f , o∈[o]ω )

ccx∈[x] : ∀ (x : F) → (cc x) ∈ [ x ]ω

ccx∈[x] x = proj₁ (proj₂ (index* [ x ]ω ( x , o∈[o]ω )))

xωccx : ∀ (x : F) → x ω (cc x)

xωccx x = ω-sym (∈⇒ω (ccx∈[x] x))

c⇒ω : ∀ {x y} → cc x ≡ cc y → x ω y

c⇒ω {x} {y} ccx≡ccy = let P = λ q → q ∈ [ y ]ω

                          w : (cc x) ∈ [ y ]ω

                          w = subst P (sym ccx≡ccy) (ccx∈[x] y)

                    in ω-transitive (xωccx x) (∈⇒ω w)

ω⇒c : ∀ {x y} → x ω y → cc x ≡ cc y

ω⇒c {x} {y} xωy = index-unique _ _ _ _ (ω⇒≡ xωy)

cc-idempt : (x : F) → cc (cc x) ≡ cc x

cc-idempt x = ω⇒c {cc x} {x} (ω-sym (xωccx x))

cr : (i : F) → Set

cr i = i ≡ (cc i)

cr? : Decidable cr

cr? = λ i → i ≟ (cc i)

Transversal : List F

Transversal = (List.filter cr? Fˡ)

Covering : ∀ (x : F) → Any (x ∈_) ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧

Covering x = let

               cover : ∀ (x : F) → (∃ λ k → cr k × x ω k)

               cover t = (cc t) , sym (cc-idempt t) , xωccx t

               (k , crk , xωk) = cover x

               k∈ℓFˡ : k ∈ℓ Fˡ

               k∈ℓFˡ = ∈-allFin {n} k

               k∈ℓTr : k ∈ℓ Transversal

               k∈ℓTr = ∈-filter⁺ cr? k∈ℓFˡ crk

               a : Any (x ω_) Transversal

               a = lose k∈ℓTr xωk

               b : Any ((x ∈_) ∘ [_]ω) Transversal

               b = Any.map ω⇒∈ a

            -- AnyProps.map⁺ : Any (P ∘ f) xs → Any P (List.map f xs)

            in AnyProps.map⁺ b

Disjointness : AllPairs Disj ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧

Disjointness = 

  let ap₁ : AllPairs _≢_ Fˡ

      ap₁ = AllPairsProps.tabulate⁺ id

      cr-injective : ∀ {x y} → (cr x) → (cr y) → x ≢ y → ¬ x ω y

      cr-injective {x} {y} crx cry x≢y xωy = x≢y (begin x ≡⟨ crx ⟩

                                                     cc x ≡⟨ ω⇒c xωy ⟩

                                                     cc y ≡˘⟨ cry ⟩

                                                     y ∎)

      ω-disj : ∀ {x y} → ¬ (x ω y) → Empty ([ x ]ω ∩ [ y ]ω)

      ω-disj {x} {y} ¬xωy f∈∩ = let f , [x]∩[y] = f∈∩

                                    l , r = x∈p∩q⁻ _ _ [x]∩[y]

                                    xωf = ω-sym (∈⇒ω l)

                                    fωy = ∈⇒ω r

                                    in ¬xωy (ω-transitive xωf fωy)

      ω-Disj : ∀ {x y} → ¬ x ω y → Disj [ x ]ω [ y ]ω

      ω-Disj ¬xωy = disj⇒Disj (ω-disj ¬xωy)

      ap₂ : AllPairs (λ x y → ¬ x ω y) Transversal

      ap₂ = filter⁺₃ cr? cr-injective ap₁

      ap₃ = AllPairs.map ω-Disj ap₂ 

      in AllPairsProps.map⁺ ap₃

Cover : ⊤ ≡ ⋃ ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧ 

Cover = cover-⊤ ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧ Covering

Cardinality : n ≡ List.sum ⟦ ∣ [ x ]ω ∣ ∣ x 𝕚𝕟 Transversal ⟧

Cardinality = 

  let c = ∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧ Disjointness

      d = map-compose {g = ∣_∣} {f = [_]ω} Transversal

      sum = List.sum

      in begin 

          n ≡˘⟨ ∣⊤∣≡n n ⟩

          ∣ ⊤ {n} ∣ ≡⟨ cong ∣_∣ Cover ⟩

          ∣ ⋃ ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧ ∣ ≡⟨ c ⟩ 

          sum (List.map ∣_∣ ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧) ≡˘⟨ cong sum d ⟩

          sum ⟦ ∣ [ x ]ω ∣ ∣ x 𝕚𝕟 Transversal ⟧ ∎

module FDS.Characterisation where

open import FDS

open import FDS.Fin.Subset.Lemmas

open import FDS.List.AllPairs.Lemmas

import FDS.Properties

record Partition (n : ℕ) : Set (sucℓ 0ℓ) where

  field

    parts : List (Subset n)

    disjoint : AllPairs disj parts

    cover : ∀ (x : Fin n) → Any (x ∈_) parts

  _ωP_ : Rel (Fin n) 0ℓ

  x ωP y = Any (λ s → x ∈ s × y ∈ s) parts

FDS⇒Partition : ∀ {ℓ n} → FinDecEq {ℓ} n → Partition n

FDS⇒Partition FDS = 

  record { parts = ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧ ;

           disjoint = AllPairs.map Disj⇒disj Disjointness ;

           cover = Covering } where

  open FinDecEq FDS

  open FDS.Properties {FDS = FDS}

Partition⇒FDS : ∀ {n} → Partition n → FinDecEq n

Partition⇒FDS {n} P = 

  record { _ω_ = _ωP_ ;

           isDecEq = isDecEq }

  where

    open Partition P

    ωRefl : Reflexive _ωP_

    ωRefl {x} = Any.map {P = λ s → x ∈ s} (λ z → z , z) (cover x)

    ωSym : Symmetric _ωP_

    ωSym xωPy = Any.map (λ (a , b) → b , a) xωPy

    ωTrans : Transitive _ωP_

    ωTrans {x} {y} {z} xωPy yωPz = 

      let

        s , s∈ℓparts , x∈s , y∈s = Membership.find xωPy

        t , t∈ℓparts , y∈t , z∈t = Membership.find yωPz

        y∈s∩t : y ∈ s ∩ t

        y∈s∩t = x∈p∩q⁺ ( y∈s , y∈t )

        i = Any.index s∈ℓparts

        j = Any.index t∈ℓparts

        ¬d : ¬ (disj s t)

        ¬d e = e ( y , y∈s∩t ) 

        disj-sym : Symmetric disj

        disj-sym {x} {y} disjxy = subst Empty (∩-comm x y) disjxy

        helper : i ≡ j → x ωP z

        helper i≡j = 

          let s≡t : s ≡ t

              s≡t = begin 

                s ≡⟨ helper₁ s∈ℓparts ⟩ 

                Any.lookup s∈ℓparts ≡⟨ cong (List.lookup parts) i≡j ⟩

                Any.lookup t∈ℓparts ≡˘⟨ helper₁ t∈ℓparts ⟩ 

                t ∎

              x∈t : x ∈ t

              x∈t = subst₂ _∈_ refl s≡t x∈s

          in Membership.lose t∈ℓparts ( x∈t , z∈t )

        in case i ≟ j of λ {

          (yes i≡j) → helper i≡j ;

          (no i≢j) → ⊥-elim (¬d (elim-sym disj-sym disjoint s∈ℓparts t∈ℓparts i≢j))

        } where

            helper₁ : ∀ {A : Set} {x : A} {l : List A} → 

                      (ξ : x ∈ℓ l) → x ≡ Any.lookup ξ

            helper₁ (here px) = px

            helper₁ (there χ) = helper₁ χ

    isEq : IsEquivalence _ωP_

    isEq = record {

            refl = ωRefl ;

            sym = ωSym ; 

            trans = ωTrans }

    -- decidability

    ≟P : Decidable ( _ωP_ )

    ≟P = λ x y → Any.any (λ t → dec-× (x ∈? t) (y ∈? t)) parts

    isDecEq : IsDecEquivalence _ωP_

    isDecEq = record { isEquivalence = isEq ; _≟_ = ≟P }                         

module FDS.Fin.Subset.Lemmas where

open import FDS.Subset.Helpers

Disj : ∀ {n} → Subset n → Subset n → Set

Disj S T = S ∩ T ≡ ⊥

disj : ∀ {n} → Subset n → Subset n → Set

disj S T = Empty (S ∩ T)

Disj-sym : ∀ {n} → Symmetric (Disj {n = n})

Disj-sym {n} {S} {T} S∩T≡⊥ = begin T ∩ S ≡⟨ ∩-comm T S ⟩ S ∩ T ≡⟨ S∩T≡⊥ ⟩ ⊥ ∎

Empty⊥ : ∀ {n} → Empty { n } ⊥

Empty⊥ (i , n) = let

                    x : Vec.lookup ⊥ i ≡ outside

                    x = lookup-replicate i outside

                    y : Vec.lookup ⊥ i ≡ inside

                    y = []=⇒lookup n

                    z = trans (sym x) y

                  in contradiction z (not-¬ refl)

disj⇒Disj : ∀ {n} → ∀ {s t : Subset n} → disj s t → Disj s t

disj⇒Disj d = Empty-unique d

Disj⇒disj : ∀ {n} → ∀ {s t : Subset n} → Disj s t → disj s t

Disj⇒disj D = subst Empty (sym D) (Empty⊥)

⋃-remove : ∀ {n} {L : List (Subset n)} → ∀ s → (s∈L : s ∈ℓ L) →

           ⋃ L ≡ s ∪ ⋃ (L Any.─ s∈L)

⋃-remove {n} {List.[]} _ = λ ()

⋃-remove {n} {x ∷ xs} s (here px) =

  begin

    ⋃ (x ∷ xs) ≡⟨ refl ⟩

    x ∪ (⋃ xs) ≡˘⟨ cong (_∪ _) px ⟩

    s ∪ (⋃ xs) ≡⟨ cong (_ ∪_) refl ⟩

    s ∪ ⋃ ((x ∷ xs) Any.─ (here {P = P} px)) ∎

    where

    P : Pred (Subset n) Level.zero

    P = s ≡_

⋃-remove {n} {x ∷ xs} s (there s∈L) =

  begin

    x ∪ (⋃ xs) ≡⟨ cong (x ∪_) (⋃-remove {L = xs} s s∈L) ⟩

    x ∪ (s ∪ ⋃ (xs Any.─ s∈L)) ≡˘⟨ ∪-assoc _ _ _ ⟩ -- TODO: -- use solver

    (x ∪ s) ∪ ⋃ (xs Any.─ s∈L) ≡⟨ cong (_∪ _) (∪-comm x s) ⟩

    (s ∪ x) ∪ ⋃ (xs Any.─ s∈L) ≡⟨ ∪-assoc _ _ _ ⟩

    s ∪ (x ∪ ⋃ (xs Any.─ s∈L)) ≡⟨ refl ⟩

    s ∪ ⋃ ((x ∷ xs) Any.─ (there s∈L)) ∎

cover-⊤ : ∀ {n} → (L : List (Subset n)) →

          (∀ (x : Fin n) → Any (x ∈_) L ) →

          ⊤ {n} ≡ ⋃ L

cover-⊤ {n} L ∃lx∈l = ⊆-antisym ⊤⊆⋃L (⊆-max (⋃ L)) where

  ⊤⊆⋃L : ⊤ ⊆ (⋃ L)

  ⊤⊆⋃L {x} _ = let

                  (l , l∈ℓL , x∈l) = find {P = x ∈_} (∃lx∈l x)

                  l⊆l∪* = p⊆p∪q {p = l} (⋃ (L Any.─ l∈ℓL))

                  x∈l∪* = l⊆l∪* {x} x∈l

                in subst₂ _∈_ refl (sym (⋃-remove l l∈ℓL)) x∈l∪*

∣p⊍q∣≡∣p∣+∣q∣ : ∀ {n} → ∀ (p q : Subset n) → 

                Disj p q → ∣ p ∪ q ∣ ≡ ∣ p ∣ + ∣ q ∣

∣p⊍q∣≡∣p∣+∣q∣ {zero} [] [] d = refl

∣p⊍q∣≡∣p∣+∣q∣ {suc n} (outside ∷ p) (outside ∷ q) d = 

  begin

    ∣ p ∪ q ∣ ≡⟨ ∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {outside} {outside} d) ⟩

    ∣ (outside ∷ p) ∣ + ∣ (outside ∷ q) ∣ ∎

∣p⊍q∣≡∣p∣+∣q∣ {suc n} (inside ∷ p) (outside ∷ q) d = 

  begin

    ∣ (inside ∷ p) ∪ (outside ∷ q) ∣ ≡⟨ refl ⟩

    suc ∣ p ∪ q ∣ 

      ≡⟨ cong suc (∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {inside} {outside} d)) ⟩

    suc (∣ p ∣ + ∣ q ∣) ≡⟨⟩

    (suc ∣ p ∣) + ∣ q ∣ ≡⟨⟩

    ∣ (inside ∷ p) ∣ + ∣ (outside ∷ q) ∣ ∎

∣p⊍q∣≡∣p∣+∣q∣ {suc n} (outside ∷ p) (inside ∷ q) d = 

  begin

    ∣ (outside ∷ p) ∪ (inside ∷ q) ∣ ≡⟨ refl ⟩

    suc ∣ p ∪ q ∣ 

      ≡⟨ cong suc (∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {outside} {inside} d)) ⟩

    suc (∣ p ∣ + ∣ q ∣) ≡⟨ cong suc (+-comm ∣ p ∣ ∣ q ∣) ⟩

    suc (∣ q ∣ + ∣ p ∣) ≡⟨ refl ⟩

    (suc ∣ q ∣) + ∣ p ∣ ≡⟨⟩

    ∣ (inside ∷ q) ∣ + ∣ (outside ∷ p) ∣ 

      ≡⟨ +-comm ∣ (inside ∷ q) ∣ ∣ (outside ∷ p) ∣  ⟩

    ∣ (outside ∷ p) ∣ + ∣ (inside ∷ q) ∣ ∎            

∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ : ∀ {n} → (C : List (Subset n)) → AllPairs Disj C →

                ∣ ⋃ C ∣ ≡ List.sum (List.map ∣_∣ C)

∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} List.[] Δℓ =

  begin

    ∣ ⋃ {n} List.[] ∣ ≡⟨⟩

    ∣ ⊥ {n} ∣ ≡⟨ ∣⊥∣≡0 n ⟩

    0 ≡⟨⟩

    List.foldr _+_ 0 List.[] ∎

∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} (s ∷ C) (h ∷ t) = 

  begin

    ∣ ⋃ (s ∷ C) ∣ ≡⟨⟩

    ∣ s ∪ (⋃ C) ∣ ≡⟨ ∣p⊍q∣≡∣p∣+∣q∣ s (⋃ C) (Disj-sym DisjUCs) ⟩

    ∣ s ∣ + ∣ ⋃ C ∣ ≡⟨ cong (∣ s ∣ +_) (∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} C t ) ⟩

    ∣ s ∣ + (List.sum (List.map ∣_∣ C)) ≡⟨⟩

    List.sum (List.map ∣_∣ (s ∷ C)) ∎

    where

    a : All (λ x → x ⊆ ∁ s) C

    a = All.map (disj⇒⊆∁ ∘ Disj-sym) h

    c : ⋃ C ⊆ ∁ s

    c = pᵢ⊆q⇒⋃pᵢ⊆q (∁ s) C a

    DisjUCs : Disj (⋃ C) s

    DisjUCs = ⊆∁⇒disj c

fsuc∈ : ∀ {n} → {p : Subset n} → {x : Fin n} → {s : Side} → 

        (x ∈ p) → (fsuc x) ∈ (s ∷ p)

fsuc∈ here = there here

fsuc∈ (there x∈p) = there (fsuc∈ x∈p)

index* : ∀ {n} → (s : Subset n) → Nonempty s →

         ∃ (λ x → ( x ∈ s × (∀ {y} → (y ∈ s) → x ≤ y )))

index* {suc n} (inside ∷ rest) _ = (fzero , here , λ _ → z≤n )

index* {suc n} (outside ∷ rest) ne with (∃-toSum ne)

... | inj₂ b = let w = drop-there (proj₂ b)

                   z = (proj₁ b , w)

                   ( a , bb , c ) = (index* rest z)

               in (fsuc a , fsuc∈ bb , λ { (there y∈s) → s≤s (c y∈s) } )

index : ∀ {n} → (s : Subset n) → Nonempty s → Fin n

index s ne = proj₁ (index* s ne)

index-unique : ∀ {n} → ∀ (s t : Subset n) → (ns : Nonempty s) →

             (nt : Nonempty t) →

             s ≡ t → (index s ns) ≡ (index t nt)

index-unique s t ns nt s≡t = let fs , fs∈s , fs≤ = index* s ns

                                 ft , ft∈t , ft≤ = index* t nt

                                 ft∈s : ft ∈ s

                                 ft∈s = subst _ (sym s≡t) ft∈t

                                 fs∈t : fs ∈ t

                                 fs∈t = subst _ s≡t fs∈s

                              in ≤-antisym (fs≤ ft∈s) (ft≤ fs∈t)

module FDS.List.AllPairs.Lemmas where

module _ {a ℓ} {A : Set a} {R : Rel A ℓ } where

  elim : ∀ {xs x y} → AllPairs R xs → 

           (x∈ : x ∈ xs) → (y∈ : y ∈ xs) →

           (Any.index x∈) <f (Any.index y∈) → R x y

  elim {xs} {x} {y} ap x∈ y∈ i<j =

    let  i = (Any.index x∈) 

         j = (Any.index y∈)

         xs' = drop (toℕ i) xs

         ¬∅ : xs' ≡ x ∷ _

         ¬∅ = drop∷ xs x∈

         d : AllPairs R xs'

         d = drop⁺ (toℕ i) ap

         d' = subst (AllPairs R) ¬∅ d

         h = AllPairs.head d'

    in All.lookup h (drop-suc xs x∈ y∈ i<j)

module _ {a ℓ} {A : Set a} {R : Rel A ℓ } (S : Symmetric R) where

  elim-sym : ∀ {xs x y} → AllPairs R xs → 

          (x∈ : x ∈ xs) → (y∈ : y ∈ xs) → 

          (Any.index x∈) ≢ (Any.index y∈) → R x y

  elim-sym ap x∈ y∈ i≢j with <-cmp (Any.index x∈) (Any.index y∈)

  ...| tri< i<j _ _ = elim ap x∈ y∈ i<j

  ...| tri> _ _ j<i = S (elim ap y∈ x∈ j<i)

  ...| tri≈ _ i≈j _ = ⊥-elim (i≢j i≈j)

module _ {a ℓ ℓ₁ ℓ₂} {A : Set a}

         {R : Rel A ℓ₁} {S : Rel A ℓ₂}

         {P : Pred A ℓ} (P? : Decidable P) where

  filter⁺₃ : ∀ {xs} → (∀ {x y} → P x → P y → R x y → S x y) →

            AllPairs R xs → AllPairs S (filter P? xs)

  filter⁺₃ {[]} _ _ = []

  filter⁺₃ {x ∷ xs} Δ (h ∷ t) with (P? x)

  ... | no  ¬p = filter⁺₃ {xs} Δ t

  ... | yes p = let

                  hf : All (R x) (filter P? xs)

                  hf = filter⁺ P? h

                  ap : All P (filter P? xs)

                  ap = all-filter P? xs

                  w : All (P ∩ R x) (filter P? xs)

                  w = All.zip ( ap , hf )

                  y : P ∩ R x ⊆ S x

                  y = λ z → Δ p (proj₁ z) (proj₂ z)

                  z : All (S x) (filter P? xs)

                  z =  All.map y w

                in z ∷ filter⁺₃ {xs} Δ t

module FDS.Subset.Helpers where

∩-⊆-stable : ∀ {n} → ∀ {p q} → (r : Subset n) → p ⊆ q → (p ∩ r) ⊆ (q ∩ r)

∩-⊆-stable {_} {p} {q} r p⊆q x∈p∩r = 

  let

    x∈p = proj₁ (x∈p∩q⁻ p r x∈p∩r)

    x∈r = proj₂ (x∈p∩q⁻ p r x∈p∩r)

  in x∈p∩q⁺ ( p⊆q x∈p , x∈r )

idʳ⇒⊆ : ∀ {n} → (S T : Subset n) → (S ∪ T) ≡ T → S ⊆ T

idʳ⇒⊆ {n} S T sut≡t = subst₂ _⊆_ refl sut≡t (p⊆p∪q T)

p∩∁p≡⊥ : ∀ {n} → (p : Subset n) → p ∩ ∁ p ≡ ⊥