Combinatorics of Finite Sets

Cubical/Data/Empty/Properties.agda

@@ -18,6 +18,10 @@ isContr⊥→A : ∀ {ℓ} {A : Type ℓ} → isContr (⊥ → A)
 fst isContr⊥→A ()
 snd isContr⊥→A f i ()
 
+isContrΠ⊥ : ∀ {ℓ} {A : ⊥ → Type ℓ} → isContr ((x : ⊥) → A x)
+fst isContrΠ⊥ ()
+snd isContrΠ⊥ f i ()
+
 uninhabEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
   → (A → ⊥) → (B → ⊥) → A ≃ B
 uninhabEquiv ¬a ¬b = isoToEquiv isom

Cubical/Data/FinSet.agda

@@ -1,105 +1,6 @@
-{-
-
-Definition of finite sets
-
-A set is finite if it is merely equivalent to `Fin n` for some `n`. We
-can translate this to code in two ways: a truncated sigma of a nat and
-an equivalence, or a sigma of a nat and a truncated equivalence. We
-prove that both formulations are equivalent.
-
--}
-
 {-# OPTIONS --safe #-}
 
 module Cubical.Data.FinSet where
 
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Function
-open import Cubical.Foundations.Structure
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Univalence
-open import Cubical.Foundations.Equiv
-open import Cubical.HITs.PropositionalTruncation
-open import Cubical.Data.Unit
-open import Cubical.Data.Nat
-open import Cubical.Data.Fin
-open import Cubical.Data.Sigma
-
-private
-  variable
-    ℓ : Level
-    A : Type ℓ
-
-isFinSet : Type ℓ → Type ℓ
-isFinSet A = ∃[ n ∈ ℕ ] A ≃ Fin n
-
-isProp-isFinSet : isProp (isFinSet A)
-isProp-isFinSet = isPropPropTrunc
-
-FinSet : Type (ℓ-suc ℓ)
-FinSet = TypeWithStr _ isFinSet
-
-isFinSetFin : ∀ {n} → isFinSet (Fin n)
-isFinSetFin = ∣ _ , pathToEquiv refl ∣
-
-isFinSetUnit : isFinSet Unit
-isFinSetUnit = ∣ 1 , Unit≃Fin1 ∣
-
-isFinSetΣ : Type ℓ → Type ℓ
-isFinSetΣ A = Σ[ n ∈ ℕ ] ∥ A ≃ Fin n ∥
-
-FinSetΣ : Type (ℓ-suc ℓ)
-FinSetΣ = TypeWithStr _ isFinSetΣ
-
-isProp-isFinSetΣ : isProp (isFinSetΣ A)
-isProp-isFinSetΣ {A = A} (n , equivn) (m , equivm) =
-  Σ≡Prop (λ _ → isPropPropTrunc) n≡m
-  where
-    Fin-n≃Fin-m : ∥ Fin n ≃ Fin m ∥
-    Fin-n≃Fin-m = rec
-      isPropPropTrunc
-      (rec
-        (isPropΠ λ _ → isPropPropTrunc)
-        (λ hm hn → ∣ Fin n ≃⟨ invEquiv hn ⟩ A ≃⟨ hm ⟩ Fin m ■ ∣)
-        equivm
-      )
-      equivn
-
-    Fin-n≡Fin-m : ∥ Fin n ≡ Fin m ∥
-    Fin-n≡Fin-m = rec isPropPropTrunc (∣_∣ ∘ ua) Fin-n≃Fin-m
-
-    ∥n≡m∥ : ∥ n ≡ m ∥
-    ∥n≡m∥ = rec isPropPropTrunc (∣_∣ ∘ Fin-inj n m) Fin-n≡Fin-m
-
-    n≡m : n ≡ m
-    n≡m = rec (isSetℕ n m) (λ p → p) ∥n≡m∥
-
-isFinSet≡isFinSetΣ : isFinSet A ≡ isFinSetΣ A
-isFinSet≡isFinSetΣ {A = A} = hPropExt isProp-isFinSet isProp-isFinSetΣ to from
-  where
-    to : isFinSet A → isFinSetΣ A
-    to ∣ n , equiv ∣ = n , ∣ equiv ∣
-    to (squash p q i) = isProp-isFinSetΣ (to p) (to q) i
-
-    from : isFinSetΣ A → isFinSet A
-    from (n , ∣ isFinSet-A ∣) = ∣ n , isFinSet-A ∣
-    from (n , squash p q i) = isProp-isFinSet (from (n , p)) (from (n , q)) i
-
-FinSet≡FinSetΣ : FinSet {ℓ} ≡ FinSetΣ
-FinSet≡FinSetΣ = ua (isoToEquiv (iso to from to-from from-to))
-  where
-    to : FinSet → FinSetΣ
-    to (A , isFinSetA) = A , transport isFinSet≡isFinSetΣ isFinSetA
-
-    from : FinSetΣ → FinSet
-    from (A , isFinSetΣA) = A , transport (sym isFinSet≡isFinSetΣ) isFinSetΣA
-
-    to-from : ∀ A → to (from A) ≡ A
-    to-from A = Σ≡Prop (λ _ → isProp-isFinSetΣ) refl
-
-    from-to : ∀ A → from (to A) ≡ A
-    from-to A = Σ≡Prop (λ _ → isProp-isFinSet) refl
-
-card : FinSet {ℓ} → ℕ
-card = fst ∘ snd ∘ transport FinSet≡FinSetΣ
+open import Cubical.Data.FinSet.Base public
+open import Cubical.Data.FinSet.Properties public

Cubical/Data/FinSet/Base.agda

@@ -0,0 +1,34 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.FinSet.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Equiv
+
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Fin
+open import Cubical.Data.Sigma
+
+private
+  variable
+    ℓ : Level
+    A : Type ℓ
+
+isFinSet : Type ℓ → Type ℓ
+isFinSet A = ∃[ n ∈ ℕ ] A ≃ Fin n
+
+-- finite sets are sets
+isFinSet→isSet : isFinSet A → isSet A
+isFinSet→isSet = rec isPropIsSet (λ (_ , p) → isOfHLevelRespectEquiv 2 (invEquiv p) isSetFin)
+
+isPropIsFinSet : isProp (isFinSet A)
+isPropIsFinSet = isPropPropTrunc
+
+-- the type of finite sets
+
+FinSet : (ℓ : Level) → Type (ℓ-suc ℓ)
+FinSet ℓ = TypeWithStr _ isFinSet

Cubical/Data/FinSet/Constructors.agda

@@ -0,0 +1,196 @@
+{-
+
+Closure properties of FinSet under several type constructors.
+
+-}
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.FinSet.Constructors where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+
+open import Cubical.HITs.PropositionalTruncation renaming (rec to TruncRec)
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Unit
+open import Cubical.Data.Empty renaming (rec to EmptyRec)
+open import Cubical.Data.Sum
+open import Cubical.Data.Sigma
+
+open import Cubical.Data.Fin
+open import Cubical.Data.SumFin renaming (Fin to SumFin) hiding (discreteFin)
+open import Cubical.Data.FinSet.Base
+open import Cubical.Data.FinSet.Properties
+open import Cubical.Data.FinSet.FiniteChoice
+
+open import Cubical.Relation.Nullary
+
+open import Cubical.Functions.Embedding
+open import Cubical.Functions.Surjection
+
+private
+  variable
+    ℓ ℓ' ℓ'' ℓ''' : Level
+
+module _
+  (X : Type ℓ)(p : ≃Fin X) where
+
+  ≃Fin∥∥ : ≃Fin ∥ X ∥
+  ≃Fin∥∥ = ≃SumFin→Fin (_ , compEquiv (propTrunc≃ (≃Fin→SumFin p .snd)) (SumFin∥∥≃ _))
+
+module _
+  (X : Type ℓ )(p : ≃Fin X)
+  (Y : Type ℓ')(q : ≃Fin Y) where
+
+  ≃Fin⊎ : ≃Fin (X ⊎ Y)
+  ≃Fin⊎ = ≃SumFin→Fin (_ , compEquiv (⊎-equiv (≃Fin→SumFin p .snd) (≃Fin→SumFin q .snd)) (SumFin⊎≃ _ _))
+
+  ≃Fin× : ≃Fin (X × Y)
+  ≃Fin× = ≃SumFin→Fin (_ , compEquiv (Σ-cong-equiv (≃Fin→SumFin p .snd) (λ _ → ≃Fin→SumFin q .snd)) (SumFin×≃ _ _))
+
+module _
+  (X : Type ℓ )(p : ≃Fin X)
+  (Y : X → Type ℓ')(q : (x : X) → ≃Fin (Y x)) where
+
+  private
+    p' = ≃Fin→SumFin p
+
+    m = p' .fst
+    e = p' .snd
+
+    q' : (x : X) → ≃SumFin (Y x)
+    q' x = ≃Fin→SumFin (q x)
+
+    f : (x : X) → ℕ
+    f x = q' x .fst
+
+  ≃SumFinΣ : ≃SumFin (Σ X Y)
+  ≃SumFinΣ = _ ,
+      Σ-cong-equiv {B' = λ x → Y (invEq (p' .snd) x)} (p' .snd) (transpFamily p')
+    ⋆ Σ-cong-equiv-snd (λ x → q' (invEq e x) .snd)
+    ⋆ SumFinΣ≃ _ _
+
+  ≃SumFinΠ : ≃SumFin ((x : X) → Y x)
+  ≃SumFinΠ = _ ,
+      equivΠ {B' = λ x → Y (invEq (p' .snd) x)} (p' .snd) (transpFamily p')
+    ⋆ equivΠCod (λ x → q' (invEq e x) .snd)
+    ⋆ SumFinΠ≃ _ _
+
+  ≃FinΣ : ≃Fin (Σ X Y)
+  ≃FinΣ = ≃SumFin→Fin ≃SumFinΣ
+
+  ≃FinΠ : ≃Fin ((x : X) → Y x)
+  ≃FinΠ = ≃SumFin→Fin ≃SumFinΠ
+
+module _
+  (X : FinSet ℓ)
+  (Y : X .fst → FinSet ℓ') where
+
+  isFinSetΣ : isFinSet (Σ (X .fst) (λ x → Y x .fst))
+  isFinSetΣ =
+    elim2 (λ _ _ → isPropIsFinSet {A = Σ (X .fst) (λ x → Y x .fst)})
+          (λ p q → ∣ ≃FinΣ (X .fst) p (λ x → Y x .fst) q ∣)
+          (X .snd) (choice X (λ x → ≃Fin (Y x .fst)) (λ x → Y x .snd))
+
+  isFinSetΠ : isFinSet ((x : X .fst) → Y x .fst)
+  isFinSetΠ =
+    elim2 (λ _ _ → isPropIsFinSet {A = ((x : X .fst) → Y x .fst)})
+          (λ p q → ∣ ≃FinΠ (X .fst) p (λ x → Y x .fst) q ∣)
+          (X .snd) (choice X (λ x → ≃Fin (Y x .fst)) (λ x → Y x .snd))
+
+module _
+  (X : FinSet ℓ)
+  (Y : X .fst → FinSet ℓ')
+  (Z : (x : X .fst) → Y x .fst → FinSet ℓ'') where
+
+  isFinSetΠ2 : isFinSet ((x : X .fst) → (y : Y x .fst) → Z x y .fst)
+  isFinSetΠ2 = isFinSetΠ X (λ x → _ , isFinSetΠ (Y x) (Z x))
+
+module _
+  (X : FinSet ℓ)
+  (Y : X .fst → FinSet ℓ')
+  (Z : (x : X .fst) → Y x .fst → FinSet ℓ'')
+  (W : (x : X .fst) → (y : Y x .fst) → Z x y .fst → FinSet ℓ''') where
+
+  isFinSetΠ3 : isFinSet ((x : X .fst) → (y : Y x .fst) → (z : Z x y .fst) → W x y z .fst)
+  isFinSetΠ3 = isFinSetΠ X (λ x → _ , isFinSetΠ2 (Y x) (Z x) (W x))
+
+module _
+  (X : FinSet ℓ) where
+
+  isFinSet≡ : (a b : X .fst) → isFinSet (a ≡ b)
+  isFinSet≡ a b = isDecProp→isFinSet (isFinSet→isSet (X .snd) a b) (isFinSet→Discrete (X .snd) a b)
+
+  isFinSetIsContr : isFinSet (isContr (X .fst))
+  isFinSetIsContr = isFinSetΣ X (λ x → _ , (isFinSetΠ X (λ y → _ , isFinSet≡ x y)))
+
+  isFinSet∥∥ : isFinSet ∥ X .fst ∥
+  isFinSet∥∥ = TruncRec isPropIsFinSet (λ p → ∣ ≃Fin∥∥ (X .fst) p ∣) (X .snd)
+
+module _
+  (X : FinSet ℓ )
+  (Y : FinSet ℓ')
+  (f : X .fst → Y .fst) where
+
+  isFinSetFiber : (y : Y .fst) → isFinSet (fiber f y)
+  isFinSetFiber y = isFinSetΣ X (λ x → _ , isFinSet≡ Y (f x) y)
+
+  isFinSetIsEquiv : isFinSet (isEquiv f)
+  isFinSetIsEquiv =
+    EquivPresIsFinSet
+      (invEquiv (isEquiv≃isEquiv' f))
+      (isFinSetΠ Y (λ y → _ , isFinSetIsContr (_ , isFinSetFiber y)))
+
+module _
+  (X : FinSet ℓ )
+  (Y : FinSet ℓ') where
+
+  isFinSet⊎ : isFinSet (X .fst ⊎ Y .fst)
+  isFinSet⊎ = elim2 (λ _ _ → isPropIsFinSet) (λ p q → ∣ ≃Fin⊎ (X .fst) p (Y .fst) q ∣) (X .snd) (Y .snd)
+
+  isFinSet× : isFinSet (X .fst × Y .fst)
+  isFinSet× = elim2 (λ _ _ → isPropIsFinSet) (λ p q → ∣ ≃Fin× (X .fst) p (Y .fst) q ∣) (X .snd) (Y .snd)
+
+  isFinSet→ : isFinSet (X .fst → Y .fst)
+  isFinSet→ = isFinSetΠ X (λ _ → Y)
+
+  isFinSet≃ : isFinSet (X .fst ≃ Y .fst)
+  isFinSet≃ = isFinSetΣ (_ , isFinSet→) (λ f → _ , isFinSetIsEquiv X Y f)
+
+module _
+  (X : FinSet ℓ) where
+
+  isFinSet¬ : isFinSet (¬ (X .fst))
+  isFinSet¬ = isFinSet→ X (⊥ , ∣ 0 , uninhabEquiv (λ x → x) ¬Fin0 ∣)
+
+module _
+  (X : FinSet ℓ) where
+
+  isFinSetNonEmpty : isFinSet (NonEmpty (X .fst))
+  isFinSetNonEmpty = isFinSet¬ (_ , isFinSet¬ X)
+
+module _
+  (X : FinSet ℓ )
+  (Y : FinSet ℓ')
+  (f : X .fst → Y .fst) where
+
+  isFinSetIsEmbedding : isFinSet (isEmbedding f)
+  isFinSetIsEmbedding =
+    isFinSetΠ2 X (λ _ → X)
+      (λ a b → _ , isFinSetIsEquiv (_ , isFinSet≡ X a b) (_ , isFinSet≡ Y (f a) (f b)) (cong f))
+
+  isFinSetIsSurjection : isFinSet (isSurjection f)
+  isFinSetIsSurjection =
+    isFinSetΠ Y (λ y → _ , isFinSet∥∥ (_ , isFinSetFiber X Y f y))
+
+module _
+  (X : FinSet ℓ )
+  (Y : FinSet ℓ') where
+
+  isFinSet↪ : isFinSet (X .fst ↪ Y .fst)
+  isFinSet↪ = isFinSetΣ (_ , isFinSet→ X Y) (λ f → _ , isFinSetIsEmbedding X Y f)
+
+  isFinSet↠ : isFinSet (X .fst ↠ Y .fst)
+  isFinSet↠ = isFinSetΣ (_ , isFinSet→ X Y) (λ f → _ , isFinSetIsSurjection X Y f)