diff --git a/Cubical/Algebra/CommAlgebra/Localisation.agda b/Cubical/Algebra/CommAlgebra/Localisation.agda index b6bc3f5525..eaa98ef1c7 100644 --- a/Cubical/Algebra/CommAlgebra/Localisation.agda +++ b/Cubical/Algebra/CommAlgebra/Localisation.agda @@ -10,7 +10,7 @@ open import Cubical.Foundations.Equiv.HalfAdjoint open import Cubical.Foundations.Powerset open import Cubical.Data.Sigma -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm) open import Cubical.Data.FinData diff --git a/Cubical/Algebra/CommRing/BinomialThm.agda b/Cubical/Algebra/CommRing/BinomialThm.agda index f8e49041d9..3ed7696a91 100644 --- a/Cubical/Algebra/CommRing/BinomialThm.agda +++ b/Cubical/Algebra/CommRing/BinomialThm.agda @@ -4,7 +4,7 @@ module Cubical.Algebra.CommRing.BinomialThm where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-comm to +ℕ-comm ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm ; _choose_ to _ℕchoose_ ; snotz to ℕsnotz) diff --git a/Cubical/Algebra/CommRing/FGIdeal.agda b/Cubical/Algebra/CommRing/FGIdeal.agda index 649e66c04a..0ac9b8d8e9 100644 --- a/Cubical/Algebra/CommRing/FGIdeal.agda +++ b/Cubical/Algebra/CommRing/FGIdeal.agda @@ -16,7 +16,7 @@ open import Cubical.Data.Sigma open import Cubical.Data.Sum hiding (map ; elim ; rec) open import Cubical.Data.FinData hiding (elim ; rec) open import Cubical.Data.Nat renaming ( zero to ℕzero ; suc to ℕsuc - ; _+_ to _+ℕ_ ; _·_ to _·ℕ_ + ; _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-assoc to +ℕ-assoc ; +-comm to +ℕ-comm ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm) hiding (elim ; _choose_) diff --git a/Cubical/Algebra/CommRing/Localisation/Base.agda b/Cubical/Algebra/CommRing/Localisation/Base.agda index 1582d947a0..bc25fd054f 100644 --- a/Cubical/Algebra/CommRing/Localisation/Base.agda +++ b/Cubical/Algebra/CommRing/Localisation/Base.agda @@ -17,7 +17,7 @@ open import Cubical.Functions.FunExtEquiv import Cubical.Data.Empty as ⊥ open import Cubical.Data.Bool -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm) open import Cubical.Data.Vec diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda index 4c5b81e192..d3c7c32995 100644 --- a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda +++ b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda @@ -21,7 +21,7 @@ open import Cubical.Functions.FunExtEquiv import Cubical.Data.Empty as ⊥ open import Cubical.Data.Bool -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm) open import Cubical.Data.Nat.Order diff --git a/Cubical/Algebra/CommRing/Localisation/PullbackSquare.agda b/Cubical/Algebra/CommRing/Localisation/PullbackSquare.agda index 1dfdd64816..0a1342ae0b 100644 --- a/Cubical/Algebra/CommRing/Localisation/PullbackSquare.agda +++ b/Cubical/Algebra/CommRing/Localisation/PullbackSquare.agda @@ -34,7 +34,7 @@ open import Cubical.Functions.FunExtEquiv import Cubical.Data.Empty as ⊥ open import Cubical.Data.Bool -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm) open import Cubical.Data.Nat.Order diff --git a/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda b/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda index 273d61720d..b0424fafbd 100644 --- a/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda +++ b/Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda @@ -21,7 +21,7 @@ open import Cubical.Functions.Embedding import Cubical.Data.Empty as ⊥ open import Cubical.Data.Bool -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm) open import Cubical.Data.Vec diff --git a/Cubical/Algebra/CommRing/Properties.agda b/Cubical/Algebra/CommRing/Properties.agda index 5dc51a0150..847cb45f36 100644 --- a/Cubical/Algebra/CommRing/Properties.agda +++ b/Cubical/Algebra/CommRing/Properties.agda @@ -15,7 +15,7 @@ open import Cubical.Foundations.Powerset open import Cubical.Foundations.Path open import Cubical.Data.Sigma -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm) open import Cubical.Structures.Axioms diff --git a/Cubical/Algebra/CommRing/RadicalIdeal.agda b/Cubical/Algebra/CommRing/RadicalIdeal.agda index 6d4740cd3b..fc44baba07 100644 --- a/Cubical/Algebra/CommRing/RadicalIdeal.agda +++ b/Cubical/Algebra/CommRing/RadicalIdeal.agda @@ -10,7 +10,7 @@ open import Cubical.Foundations.HLevels open import Cubical.Data.Sigma open import Cubical.Data.Sum hiding (map) open import Cubical.Data.FinData hiding (elim) -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-comm to +ℕ-comm ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm ; _choose_ to _ℕchoose_ ; snotz to ℕsnotz) diff --git a/Cubical/Algebra/ZariskiLattice/Base.agda b/Cubical/Algebra/ZariskiLattice/Base.agda index 6600125ad6..fd78ec0894 100644 --- a/Cubical/Algebra/ZariskiLattice/Base.agda +++ b/Cubical/Algebra/ZariskiLattice/Base.agda @@ -12,7 +12,7 @@ open import Cubical.Foundations.Transport import Cubical.Data.Empty as ⊥ open import Cubical.Data.Bool -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm ; ·-identityʳ to ·ℕ-rid) diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda index b1d19c0da3..da97f57a59 100644 --- a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda +++ b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda @@ -23,7 +23,7 @@ open import Cubical.Foundations.Powerset using (ℙ ; ⊆-refl-consequence) import Cubical.Data.Empty as ⊥ open import Cubical.Data.Bool -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm ; ·-identityʳ to ·ℕ-rid) diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda index 0a2e813e47..3aabf29e0f 100644 --- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda +++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda @@ -13,7 +13,7 @@ open import Cubical.Foundations.Powerset using (ℙ ; ⊆-refl-consequence) import Cubical.Data.Empty as ⊥ open import Cubical.Data.Bool -open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ +open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_ ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm ; ·-identityʳ to ·ℕ-rid) diff --git a/Cubical/Data/Bool/Properties.agda b/Cubical/Data/Bool/Properties.agda index c899f997d7..a8f2b8feb7 100644 --- a/Cubical/Data/Bool/Properties.agda +++ b/Cubical/Data/Bool/Properties.agda @@ -12,8 +12,10 @@ open import Cubical.Foundations.Transport open import Cubical.Foundations.Univalence open import Cubical.Foundations.Pointed +open import Cubical.Data.Unit renaming (tt to tt') +open import Cubical.Data.Sum open import Cubical.Data.Bool.Base -open import Cubical.Data.Empty +open import Cubical.Data.Empty as Empty open import Cubical.Data.Sigma open import Cubical.Relation.Nullary @@ -68,10 +70,10 @@ false≢true p = subst (λ b → if b then ⊥ else Bool) p true ¬true→false : (x : Bool) → ¬ x ≡ true → x ≡ false ¬true→false false _ = refl -¬true→false true p = rec (p refl) +¬true→false true p = Empty.rec (p refl) ¬false→true : (x : Bool) → ¬ x ≡ false → x ≡ true -¬false→true false p = rec (p refl) +¬false→true false p = Empty.rec (p refl) ¬false→true true _ = refl not≢const : ∀ x → ¬ not x ≡ x @@ -189,9 +191,9 @@ module BoolReflection where categorize P | inspect true false p q = subst (λ b → transport P ≡ transport (⊕-Path b)) (sym p) (notLemma P p q) categorize P | inspect false false p q - = rec (¬transportNot P false (q ∙ sym p)) + = Empty.rec (¬transportNot P false (q ∙ sym p)) categorize P | inspect true true p q - = rec (¬transportNot P false (q ∙ sym p)) + = Empty.rec (¬transportNot P false (q ∙ sym p)) ⊕-complete : ∀ P → P ≡ ⊕-Path (transport P false) ⊕-complete P = isInjectiveTransport (categorize P) @@ -219,3 +221,15 @@ Iso.rightInv IsoBool→∙ a = refl Iso.leftInv IsoBool→∙ (f , p) = ΣPathP ((funExt (λ { false → refl ; true → sym p})) , λ i j → p (~ i ∨ j)) + +open Iso + +Iso-⊤⊎⊤-Bool : Iso (Unit ⊎ Unit) Bool +Iso-⊤⊎⊤-Bool .fun (inl tt') = true +Iso-⊤⊎⊤-Bool .fun (inr tt') = false +Iso-⊤⊎⊤-Bool .inv true = inl tt' +Iso-⊤⊎⊤-Bool .inv false = inr tt' +Iso-⊤⊎⊤-Bool .leftInv (inl tt') = refl +Iso-⊤⊎⊤-Bool .leftInv (inr tt') = refl +Iso-⊤⊎⊤-Bool .rightInv true = refl +Iso-⊤⊎⊤-Bool .rightInv false = refl diff --git a/Cubical/Data/Empty/Base.agda b/Cubical/Data/Empty/Base.agda index efba43446b..b126a028f1 100644 --- a/Cubical/Data/Empty/Base.agda +++ b/Cubical/Data/Empty/Base.agda @@ -5,7 +5,7 @@ open import Cubical.Foundations.Prelude private variable - ℓ : Level + ℓ ℓ' : Level data ⊥ : Type₀ where @@ -15,5 +15,8 @@ data ⊥ : Type₀ where rec : {A : Type ℓ} → ⊥ → A rec () +rec* : {A : Type ℓ} → ⊥* {ℓ = ℓ'} → A +rec* () + elim : {A : ⊥ → Type ℓ} → (x : ⊥) → A x elim () diff --git a/Cubical/Data/Empty/Properties.agda b/Cubical/Data/Empty/Properties.agda index f0cc830651..51f873ea4a 100644 --- a/Cubical/Data/Empty/Properties.agda +++ b/Cubical/Data/Empty/Properties.agda @@ -22,6 +22,10 @@ isContrΠ⊥ : ∀ {ℓ} {A : ⊥ → Type ℓ} → isContr ((x : ⊥) → A x) fst isContrΠ⊥ () snd isContrΠ⊥ 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 diff --git a/Cubical/Data/Fin/Base.agda b/Cubical/Data/Fin/Base.agda index 3e14db2588..4b91796369 100644 --- a/Cubical/Data/Fin/Base.agda +++ b/Cubical/Data/Fin/Base.agda @@ -7,7 +7,7 @@ open import Cubical.Foundations.Function open import Cubical.Foundations.HLevels import Cubical.Data.Empty as ⊥ -open import Cubical.Data.Nat using (ℕ; zero; suc; _+_) +open import Cubical.Data.Nat using (ℕ ; zero ; suc ; _+_ ; znots) open import Cubical.Data.Nat.Order open import Cubical.Data.Nat.Order.Recursive using () renaming (_≤_ to _≤′_) open import Cubical.Data.Sigma @@ -33,6 +33,12 @@ private fzero : Fin (suc k) fzero = (0 , suc-≤-suc zero-≤) +fone : Fin (suc (suc k)) +fone = (1 , suc-≤-suc (suc-≤-suc zero-≤)) + +fzero≠fone : ¬ fzero {k = suc k} ≡ fone +fzero≠fone p = znots (cong fst p) + -- It is easy, using this representation, to take the successor of a -- number as a number in the next largest finite type. fsuc : Fin k → Fin (suc k) diff --git a/Cubical/Data/Fin/Properties.agda b/Cubical/Data/Fin/Properties.agda index 007ee0b264..b712e61b7a 100644 --- a/Cubical/Data/Fin/Properties.agda +++ b/Cubical/Data/Fin/Properties.agda @@ -14,6 +14,8 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.Univalence open import Cubical.Foundations.Transport +open import Cubical.HITs.PropositionalTruncation renaming (rec to ∥∥rec) + open import Cubical.Data.Fin.Base as Fin open import Cubical.Data.Nat open import Cubical.Data.Nat.Order @@ -634,3 +636,48 @@ FinData≃Fin N = isoToEquiv (FinDataIsoFin N) FinData≡Fin : (N : ℕ) → FinData N ≡ Fin N FinData≡Fin N = ua (FinData≃Fin N) + +-- decidability of Fin + +DecFin : (n : ℕ) → Dec (Fin n) +DecFin 0 = no ¬Fin0 +DecFin (suc n) = yes fzero + +-- propositional truncation of Fin + +Dec∥Fin∥ : (n : ℕ) → Dec ∥ Fin n ∥ +Dec∥Fin∥ n = Dec∥∥ (DecFin n) + +-- some properties about cardinality + +Fin>0→isInhab : (n : ℕ) → 0 < n → Fin n +Fin>0→isInhab 0 p = Empty.rec (¬-<-zero p) +Fin>0→isInhab (suc n) p = fzero + +Fin>1→hasNonEqualTerm : (n : ℕ) → 1 < n → Σ[ i ∈ Fin n ] Σ[ j ∈ Fin n ] ¬ i ≡ j +Fin>1→hasNonEqualTerm 0 p = Empty.rec (snotz (≤0→≡0 p)) +Fin>1→hasNonEqualTerm 1 p = Empty.rec (snotz (≤0→≡0 (pred-≤-pred p))) +Fin>1→hasNonEqualTerm (suc (suc n)) _ = fzero , fone , fzero≠fone + +isEmpty→Fin≡0 : (n : ℕ) → ¬ Fin n → 0 ≡ n +isEmpty→Fin≡0 0 _ = refl +isEmpty→Fin≡0 (suc n) p = Empty.rec (p fzero) + +isInhab→Fin>0 : (n : ℕ) → Fin n → 0 < n +isInhab→Fin>0 0 i = Empty.rec (¬Fin0 i) +isInhab→Fin>0 (suc n) _ = suc-≤-suc zero-≤ + +hasNonEqualTerm→Fin>1 : (n : ℕ) → (i j : Fin n) → ¬ i ≡ j → 1 < n +hasNonEqualTerm→Fin>1 0 i _ _ = Empty.rec (¬Fin0 i) +hasNonEqualTerm→Fin>1 1 i j p = Empty.rec (p (isContr→isProp isContrFin1 i j)) +hasNonEqualTerm→Fin>1 (suc (suc n)) _ _ _ = suc-≤-suc (suc-≤-suc zero-≤) + +Fin≤1→isProp : (n : ℕ) → n ≤ 1 → isProp (Fin n) +Fin≤1→isProp 0 _ = isPropFin0 +Fin≤1→isProp 1 _ = isContr→isProp isContrFin1 +Fin≤1→isProp (suc (suc n)) p = Empty.rec (¬-<-zero (pred-≤-pred p)) + +isProp→Fin≤1 : (n : ℕ) → isProp (Fin n) → n ≤ 1 +isProp→Fin≤1 0 _ = ≤-solver 0 1 +isProp→Fin≤1 1 _ = ≤-solver 1 1 +isProp→Fin≤1 (suc (suc n)) p = Empty.rec (fzero≠fone (p fzero fone)) diff --git a/Cubical/Data/FinSet/Base.agda b/Cubical/Data/FinSet/Base.agda index b1911f03ed..50031e8d51 100644 --- a/Cubical/Data/FinSet/Base.agda +++ b/Cubical/Data/FinSet/Base.agda @@ -1,3 +1,11 @@ +{- + +Definition of finite sets + +There are may different formulations of finite sets in constructive mathematics, +and we will use Bishop finiteness as is usually called in the literature. + +-} {-# OPTIONS --safe #-} module Cubical.Data.FinSet.Base where @@ -18,6 +26,8 @@ private ℓ : Level A : Type ℓ +-- definition of (Bishop) finite sets + isFinSet : Type ℓ → Type ℓ isFinSet A = ∃[ n ∈ ℕ ] A ≃ Fin n @@ -28,7 +38,29 @@ isFinSet→isSet = rec isPropIsSet (λ (_ , p) → isOfHLevelRespectEquiv 2 (inv isPropIsFinSet : isProp (isFinSet A) isPropIsFinSet = isPropPropTrunc --- the type of finite sets +-- the type of finite sets/propositions FinSet : (ℓ : Level) → Type (ℓ-suc ℓ) FinSet ℓ = TypeWithStr _ isFinSet + +FinProp : (ℓ : Level) → Type (ℓ-suc ℓ) +FinProp ℓ = Σ[ P ∈ FinSet ℓ ] isProp (P .fst) + +-- equality between finite sets/propositions + +FinSet≡ : (X Y : FinSet ℓ) → (X .fst ≡ Y .fst) ≃ (X ≡ Y) +FinSet≡ _ _ = Σ≡PropEquiv (λ _ → isPropIsFinSet) + +FinProp≡ : (X Y : FinProp ℓ) → (X .fst .fst ≡ Y .fst .fst) ≃ (X ≡ Y) +FinProp≡ X Y = compEquiv (FinSet≡ (X .fst) (Y .fst)) (Σ≡PropEquiv (λ _ → isPropIsProp)) + +-- hlevels of FinSet and FinProp + +isGroupoidFinSet : isGroupoid (FinSet ℓ) +isGroupoidFinSet X Y = + isOfHLevelRespectEquiv 2 (FinSet≡ X Y) + (isOfHLevel≡ 2 (isFinSet→isSet (X .snd)) (isFinSet→isSet (Y .snd))) + +isSetFinProp : isSet (FinProp ℓ) +isSetFinProp X Y = + isOfHLevelRespectEquiv 1 (FinProp≡ X Y) (isOfHLevel≡ 1 (X .snd) (Y .snd)) diff --git a/Cubical/Data/FinSet/Cardinality.agda b/Cubical/Data/FinSet/Cardinality.agda new file mode 100644 index 0000000000..160c9bbda7 --- /dev/null +++ b/Cubical/Data/FinSet/Cardinality.agda @@ -0,0 +1,626 @@ +{- + +Properties and Formulae about Cardinality + +This file contains: +- Relation between abstract properties and cardinality in special cases; +- Combinatorial formulae, namely, cardinality of A+B, A×B, ΣAB, ΠAB, etc; +- A general form of Pigeonhole Principle; +- Maximal value of numerical function on finite sets; +- Set truncation of FinSet is equivalent to ℕ; +- FinProp is equivalent to Bool. + +-} +{-# OPTIONS --safe #-} + +module Cubical.Data.FinSet.Cardinality where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_) +open import Cubical.Foundations.Equiv.Properties + +open import Cubical.HITs.PropositionalTruncation as Prop +open import Cubical.HITs.SetTruncation as Set + +open import Cubical.Data.Nat +open import Cubical.Data.Nat.Order +open import Cubical.Data.Unit +open import Cubical.Data.Empty as Empty +open import Cubical.Data.Bool hiding (_≟_) +open import Cubical.Data.Sum +open import Cubical.Data.Sigma + +open import Cubical.Data.Fin + renaming (pigeonhole to pigeonholeFin ; toℕ to cardFin) +open import Cubical.Data.Fin.LehmerCode +open import Cubical.Data.SumFin renaming (Fin to SumFin) +open import Cubical.Data.FinSet.Base +open import Cubical.Data.FinSet.Properties +open import Cubical.Data.FinSet.FiniteChoice +open import Cubical.Data.FinSet.Constructors +open import Cubical.Data.FinSet.Induction hiding (_+_) + +open import Cubical.Relation.Nullary + +open import Cubical.Functions.Fibration +open import Cubical.Functions.Embedding +open import Cubical.Functions.Surjection + +private + variable + ℓ ℓ' ℓ'' : Level + n : ℕ + X : FinSet ℓ + Y : FinSet ℓ' + +-- cardinality of finite sets + +card : FinSet ℓ → ℕ +card X = FinSet→FinSet' X .snd .fst + +∣≃card∣ : (X : FinSet ℓ) → ∥ X .fst ≃ Fin (card X) ∥ +∣≃card∣ X = FinSet→FinSet' X .snd .snd + +-- cardinality is invariant under equivalences + +cardEquiv : (X : FinSet ℓ)(Y : FinSet ℓ') → ∥ X .fst ≃ Y .fst ∥ → card X ≡ card Y +cardEquiv X Y e = + Prop.rec (isSetℕ _ _) (λ p → Fin-inj _ _ (ua p)) (∣invEquiv∣ (∣≃card∣ X) ⋆̂ e ⋆̂ ∣≃card∣ Y) + +cardInj : card X ≡ card Y → ∥ X .fst ≃ Y .fst ∥ +cardInj {X = X} {Y = Y} p = + ∣≃card∣ X ⋆̂ ∣ pathToEquiv (cong Fin p) ∣ ⋆̂ ∣invEquiv∣ (∣≃card∣ Y) + +cardReflection : card X ≡ n → ∥ X .fst ≃ Fin n ∥ +cardReflection {X = X} = cardInj {X = X} {Y = _ , isFinSetFin} + +card≡MereEquiv : (card X ≡ card Y) ≡ ∥ X .fst ≃ Y .fst ∥ +card≡MereEquiv {X = X} {Y = Y} = + hPropExt (isSetℕ _ _) isPropPropTrunc (cardInj {X = X} {Y = Y}) (cardEquiv X Y) + +-- special properties about specific cardinality + +module _ + {X : FinSet ℓ} where + + card≡0→isEmpty : card X ≡ 0 → ¬ X .fst + card≡0→isEmpty p x = + Prop.rec isProp⊥ (λ e → ¬Fin0 (transport (cong Fin p) (e .fst x))) (∣≃card∣ X) + + card>0→isInhab : card X > 0 → ∥ X .fst ∥ + card>0→isInhab p = + Prop.map (λ e → invEq e (Fin>0→isInhab _ p)) (∣≃card∣ X) + + card>1→hasNonEqualTerm : card X > 1 → ∥ Σ[ a ∈ X .fst ] Σ[ b ∈ X .fst ] ¬ a ≡ b ∥ + card>1→hasNonEqualTerm p = + Prop.map + (λ e → + e .fst (Fin>1→hasNonEqualTerm _ p .fst) , + e .fst (Fin>1→hasNonEqualTerm _ p .snd .fst) , + Fin>1→hasNonEqualTerm _ p .snd .snd ∘ invEq (congEquiv e)) + (∣invEquiv∣ (∣≃card∣ X)) + + card≡1→isContr : card X ≡ 1 → isContr (X .fst) + card≡1→isContr p = + Prop.rec isPropIsContr + (λ e → isOfHLevelRespectEquiv 0 (invEquiv (e ⋆ pathToEquiv (cong Fin p))) isContrFin1) (∣≃card∣ X) + + card≤1→isProp : card X ≤ 1 → isProp (X .fst) + card≤1→isProp p = + Prop.rec isPropIsProp (λ e → isOfHLevelRespectEquiv 1 (invEquiv e) (Fin≤1→isProp (card X) p)) (∣≃card∣ X) + + card≡n : card X ≡ n → ∥ X ≡ 𝔽in n ∥ + card≡n {n = n} p = + Prop.map + (λ e → + (λ i → + ua e i , + isProp→PathP {B = λ j → isFinSet (ua e j)} + (λ _ → isPropIsFinSet) (X .snd) (𝔽in n .snd) i )) + (∣≃card∣ X ⋆̂ ∣ pathToEquiv (cong Fin p) ⋆ invEquiv (𝔽in≃Fin n) ∣) + + card≡0 : card X ≡ 0 → X ≡ 𝟘 + card≡0 p = + propTruncIdempotent≃ + (isOfHLevelRespectEquiv + 1 (FinSet≡ X 𝟘) + (isOfHLevel≡ 1 + (card≤1→isProp (subst (λ a → a ≤ 1) (sym p) (≤-solver 0 1))) (isProp⊥*))) .fst + (card≡n p) + + card≡1 : card X ≡ 1 → X ≡ 𝟙 + card≡1 p = + propTruncIdempotent≃ + (isOfHLevelRespectEquiv + 1 (FinSet≡ X 𝟙) + (isOfHLevel≡ 1 + (card≤1→isProp (subst (λ a → a ≤ 1) (sym p) (≤-solver 1 1))) (isPropUnit*))) .fst + (Prop.map (λ q → q ∙ 𝔽in1≡𝟙) (card≡n p)) + +module _ + (X : FinSet ℓ) where + + isEmpty→card≡0 : ¬ X .fst → card X ≡ 0 + isEmpty→card≡0 p = + Prop.rec (isSetℕ _ _) (λ e → sym (isEmpty→Fin≡0 _ (p ∘ invEq e))) (∣≃card∣ X) + + isInhab→card>0 : ∥ X .fst ∥ → card X > 0 + isInhab→card>0 = Prop.rec2 m≤n-isProp (λ p x → isInhab→Fin>0 _ (p .fst x)) (∣≃card∣ X) + + hasNonEqualTerm→card>1 : {a b : X. fst} → ¬ a ≡ b → card X > 1 + hasNonEqualTerm→card>1 {a = a} {b = b} q = + Prop.rec m≤n-isProp (λ p → hasNonEqualTerm→Fin>1 _ (p .fst a) (p .fst b) (q ∘ invEq (congEquiv p))) (∣≃card∣ X) + + isContr→card≡1 : isContr (X .fst) → card X ≡ 1 + isContr→card≡1 p = cardEquiv X (_ , isFinSetUnit) ∣ isContr→≃Unit p ∣ + + isProp→card≤1 : isProp (X .fst) → card X ≤ 1 + isProp→card≤1 p = isProp→Fin≤1 (card X) (Prop.rec isPropIsProp (λ e → isOfHLevelRespectEquiv 1 e p) (∣≃card∣ X)) + +{- formulae about cardinality -} + +-- results to be used in direct induction on FinSet + +card𝟘 : card (𝟘 {ℓ}) ≡ 0 +card𝟘 {ℓ = ℓ} = isEmpty→card≡0 (𝟘 {ℓ}) (Empty.rec*) + +card𝟙 : card (𝟙 {ℓ}) ≡ 1 +card𝟙 {ℓ = ℓ} = isContr→card≡1 (𝟙 {ℓ}) isContrUnit* + +card𝔽in : (n : ℕ) → card (𝔽in {ℓ} n) ≡ n +card𝔽in {ℓ = ℓ} n = cardEquiv (𝔽in {ℓ} n) (_ , isFinSetFin) ∣ 𝔽in≃Fin n ∣ + +-- addition/product formula + +module _ + (X : FinSet ℓ ) + (Y : FinSet ℓ') where + + card+ : card (_ , isFinSet⊎ X Y) ≡ card X + card Y + card+ = + cardEquiv (_ , isFinSet⊎ X Y) (Fin (card X + card Y) , isFinSetFin) + (Prop.map2 + (λ e1 e2 → ⊎-equiv e1 e2 ⋆ invEquiv (isoToEquiv (Fin+≅Fin⊎Fin _ _))) + (∣≃card∣ X) (∣≃card∣ Y)) + + card× : card (_ , isFinSet× X Y) ≡ card X · card Y + card× = + cardEquiv (_ , isFinSet× X Y) (Fin (card X · card Y) , isFinSetFin) + (Prop.map2 + (λ e1 e2 → Σ-cong-equiv e1 (λ _ → e2) ⋆ factorEquiv) + (∣≃card∣ X) (∣≃card∣ Y)) + +-- total summation/product of numerical functions from finite sets + +module _ + (X : FinSet ℓ) + (f : X .fst → ℕ) where + + sum : ℕ + sum = card (_ , isFinSetΣ X (λ x → Fin (f x) , isFinSetFin)) + + prod : ℕ + prod = card (_ , isFinSetΠ X (λ x → Fin (f x) , isFinSetFin)) + +module _ + (f : 𝟘 {ℓ} .fst → ℕ) where + + sum𝟘 : sum 𝟘 f ≡ 0 + sum𝟘 = + isEmpty→card≡0 (_ , isFinSetΣ 𝟘 (λ x → Fin (f x) , isFinSetFin)) + ((invEquiv (Σ-cong-equiv-fst (invEquiv 𝟘≃Empty)) ⋆ ΣEmpty _) .fst) + + prod𝟘 : prod 𝟘 f ≡ 1 + prod𝟘 = + isContr→card≡1 (_ , isFinSetΠ 𝟘 (λ x → Fin (f x) , isFinSetFin)) + (isContrΠ⊥*) + +module _ + (f : 𝟙 {ℓ} .fst → ℕ) where + + sum𝟙 : sum 𝟙 f ≡ f tt* + sum𝟙 = + cardEquiv (_ , isFinSetΣ 𝟙 (λ x → Fin (f x) , isFinSetFin)) + (Fin (f tt*) , isFinSetFin) ∣ Σ-contractFst isContrUnit* ∣ + + prod𝟙 : prod 𝟙 f ≡ f tt* + prod𝟙 = + cardEquiv (_ , isFinSetΠ 𝟙 (λ x → Fin (f x) , isFinSetFin)) + (Fin (f tt*) , isFinSetFin) ∣ ΠUnit* _ ∣ + +module _ + (X : FinSet ℓ ) + (Y : FinSet ℓ') + (f : X .fst ⊎ Y .fst → ℕ) where + + sum⊎ : sum (_ , isFinSet⊎ X Y) f ≡ sum X (f ∘ inl) + sum Y (f ∘ inr) + sum⊎ = + cardEquiv (_ , isFinSetΣ (_ , isFinSet⊎ X Y) (λ x → Fin (f x) , isFinSetFin)) + (_ , isFinSet⊎ (_ , isFinSetΣ X (λ x → Fin (f (inl x)) , isFinSetFin)) + (_ , isFinSetΣ Y (λ y → Fin (f (inr y)) , isFinSetFin))) ∣ Σ⊎≃ ∣ + ∙ card+ (_ , isFinSetΣ X (λ x → Fin (f (inl x)) , isFinSetFin)) + (_ , isFinSetΣ Y (λ y → Fin (f (inr y)) , isFinSetFin)) + + prod⊎ : prod (_ , isFinSet⊎ X Y) f ≡ prod X (f ∘ inl) · prod Y (f ∘ inr) + prod⊎ = + cardEquiv (_ , isFinSetΠ (_ , isFinSet⊎ X Y) (λ x → Fin (f x) , isFinSetFin)) + (_ , isFinSet× (_ , isFinSetΠ X (λ x → Fin (f (inl x)) , isFinSetFin)) + (_ , isFinSetΠ Y (λ y → Fin (f (inr y)) , isFinSetFin))) ∣ Π⊎≃ ∣ + ∙ card× (_ , isFinSetΠ X (λ x → Fin (f (inl x)) , isFinSetFin)) + (_ , isFinSetΠ Y (λ y → Fin (f (inr y)) , isFinSetFin)) + +-- technical lemma +module _ + (n : ℕ)(f : 𝔽in {ℓ} (1 + n) .fst → ℕ) where + + sum𝔽in1+n : sum (𝔽in (1 + n)) f ≡ f (inl tt*) + sum (𝔽in n) (f ∘ inr) + sum𝔽in1+n = sum⊎ 𝟙 (𝔽in n) f ∙ (λ i → sum𝟙 (f ∘ inl) i + sum (𝔽in n) (f ∘ inr)) + + prod𝔽in1+n : prod (𝔽in (1 + n)) f ≡ f (inl tt*) · prod (𝔽in n) (f ∘ inr) + prod𝔽in1+n = prod⊎ 𝟙 (𝔽in n) f ∙ (λ i → prod𝟙 (f ∘ inl) i · prod (𝔽in n) (f ∘ inr)) + +sumConst𝔽in : (n : ℕ)(f : 𝔽in {ℓ} n .fst → ℕ)(c : ℕ)(h : (x : 𝔽in n .fst) → f x ≡ c) → sum (𝔽in n) f ≡ c · n +sumConst𝔽in 0 f c _ = sum𝟘 f ∙ 0≡m·0 c +sumConst𝔽in (suc n) f c h = + sum𝔽in1+n n f + ∙ (λ i → h (inl tt*) i + sumConst𝔽in n (f ∘ inr) c (h ∘ inr) i) + ∙ sym (·-suc c n) + +prodConst𝔽in : (n : ℕ)(f : 𝔽in {ℓ} n .fst → ℕ)(c : ℕ)(h : (x : 𝔽in n .fst) → f x ≡ c) → prod (𝔽in n) f ≡ c ^ n +prodConst𝔽in 0 f c _ = prod𝟘 f +prodConst𝔽in (suc n) f c h = + prod𝔽in1+n n f + ∙ (λ i → h (inl tt*) i · prodConst𝔽in n (f ∘ inr) c (h ∘ inr) i) + +module _ + (X : FinSet ℓ) + (f : X .fst → ℕ) + (c : ℕ)(h : (x : X .fst) → f x ≡ c) where + + sumConst : sum X f ≡ c · card X + sumConst = + elimProp + (λ X → (f : X .fst → ℕ)(c : ℕ)(h : (x : X .fst) → f x ≡ c) → sum X f ≡ c · (card X)) + (λ X → isPropΠ3 (λ _ _ _ → isSetℕ _ _)) + (λ n f c h → sumConst𝔽in n f c h ∙ (λ i → c · card𝔽in {ℓ = ℓ} n (~ i))) X f c h + + prodConst : prod X f ≡ c ^ card X + prodConst = + elimProp + (λ X → (f : X .fst → ℕ)(c : ℕ)(h : (x : X .fst) → f x ≡ c) → prod X f ≡ c ^ (card X)) + (λ X → isPropΠ3 (λ _ _ _ → isSetℕ _ _)) + (λ n f c h → prodConst𝔽in n f c h ∙ (λ i → c ^ card𝔽in {ℓ = ℓ} n (~ i))) X f c h + +private + ≡≤ : {m n l k r s : ℕ} → m ≤ n → l ≤ k → r ≡ m + l → s ≡ n + k → r ≤ s + ≡≤ {m = m} {l = l} {k = k} p q u v = subst2 (_≤_) (sym u) (sym v) (≤-+-≤ p q) + + ≡< : {m n l k r s : ℕ} → m < n → l ≤ k → r ≡ m + l → s ≡ n + k → r < s + ≡< {m = m} {l = l} {k = k} p q u v = subst2 (_<_) (sym u) (sym v) (<-+-≤ p q) + +sum≤𝔽in : (n : ℕ)(f g : 𝔽in {ℓ} n .fst → ℕ)(h : (x : 𝔽in n .fst) → f x ≤ g x) → sum (𝔽in n) f ≤ sum (𝔽in n) g +sum≤𝔽in 0 f g _ = subst2 (_≤_) (sym (sum𝟘 f)) (sym (sum𝟘 g)) ≤-refl +sum≤𝔽in (suc n) f g h = + ≡≤ (h (inl tt*)) (sum≤𝔽in n (f ∘ inr) (g ∘ inr) (h ∘ inr)) (sum𝔽in1+n n f) (sum𝔽in1+n n g) + +sum<𝔽in : (n : ℕ)(f g : 𝔽in {ℓ} n .fst → ℕ)(t : ∥ 𝔽in {ℓ} n .fst ∥)(h : (x : 𝔽in n .fst) → f x < g x) + → sum (𝔽in n) f < sum (𝔽in n) g +sum<𝔽in {ℓ = ℓ} 0 _ _ t _ = Empty.rec (<→≢ (isInhab→card>0 (𝔽in 0) t) (card𝟘 {ℓ = ℓ})) +sum<𝔽in (suc n) f g t h = + ≡< (h (inl tt*)) (sum≤𝔽in n (f ∘ inr) (g ∘ inr) (<-weaken ∘ h ∘ inr)) (sum𝔽in1+n n f) (sum𝔽in1+n n g) + +module _ + (X : FinSet ℓ) + (f g : X .fst → ℕ) where + + module _ + (h : (x : X .fst) → f x ≡ g x) where + + sum≡ : sum X f ≡ sum X g + sum≡ i = sum X (λ x → h x i) + + prod≡ : prod X f ≡ prod X g + prod≡ i = prod X (λ x → h x i) + + module _ + (h : (x : X .fst) → f x ≤ g x) where + + sum≤ : sum X f ≤ sum X g + sum≤ = + elimProp + (λ X → (f g : X .fst → ℕ)(h : (x : X .fst) → f x ≤ g x) → sum X f ≤ sum X g) + (λ X → isPropΠ3 (λ _ _ _ → m≤n-isProp)) sum≤𝔽in X f g h + + module _ + (t : ∥ X .fst ∥) + (h : (x : X .fst) → f x < g x) where + + sum< : sum X f < sum X g + sum< = + elimProp + (λ X → (f g : X .fst → ℕ)(t : ∥ X .fst ∥)(h : (x : X .fst) → f x < g x) → sum X f < sum X g) + (λ X → isPropΠ4 (λ _ _ _ _ → m≤n-isProp)) sum<𝔽in X f g t h + +module _ + (X : FinSet ℓ) + (f : X .fst → ℕ) where + + module _ + (c : ℕ)(h : (x : X .fst) → f x ≤ c) where + + sumBounded : sum X f ≤ c · card X + sumBounded = subst (λ a → sum X f ≤ a) (sumConst X (λ _ → c) c (λ _ → refl)) (sum≤ X f (λ _ → c) h) + + module _ + (c : ℕ)(h : (x : X .fst) → f x ≥ c) where + + sumBoundedBelow : sum X f ≥ c · card X + sumBoundedBelow = subst (λ a → sum X f ≥ a) (sumConst X (λ _ → c) c (λ _ → refl)) (sum≤ X (λ _ → c) f h) + +-- some combinatorial identities + +module _ + (X : FinSet ℓ ) + (Y : X .fst → FinSet ℓ') where + + cardΣ : card (_ , isFinSetΣ X Y) ≡ sum X (λ x → card (Y x)) + cardΣ = + cardEquiv (_ , isFinSetΣ X Y) (_ , isFinSetΣ X (λ x → Fin (card (Y x)) , isFinSetFin)) + (Prop.map Σ-cong-equiv-snd + (choice X (λ x → Y x .fst ≃ Fin (card (Y x))) (λ x → ∣≃card∣ (Y x)))) + + cardΠ : card (_ , isFinSetΠ X Y) ≡ prod X (λ x → card (Y x)) + cardΠ = + cardEquiv (_ , isFinSetΠ X Y) (_ , isFinSetΠ X (λ x → Fin (card (Y x)) , isFinSetFin)) + (Prop.map equivΠCod + (choice X (λ x → Y x .fst ≃ Fin (card (Y x))) (λ x → ∣≃card∣ (Y x)))) + +module _ + (X : FinSet ℓ ) + (Y : FinSet ℓ') where + + card→ : card (_ , isFinSet→ X Y) ≡ card Y ^ card X + card→ = cardΠ X (λ _ → Y) ∙ prodConst X (λ _ → card Y) (card Y) (λ _ → refl) + + card≃ : card (_ , isFinSet≃ X X) ≡ factorial (card X) + card≃ = + cardEquiv (_ , isFinSet≃ X X) (Fin (factorial (card X)) , isFinSetFin) + (Prop.map + (λ e → equivComp e e ⋆ lehmerEquiv ⋆ lehmerFinEquiv) + (∣≃card∣ X)) + +module _ + (X : FinSet ℓ ) + (Y : FinSet ℓ') + (f : X .fst → Y .fst) where + + sumCardFiber : card X ≡ sum Y (λ y → card (_ , isFinSetFiber X Y f y)) + sumCardFiber = + cardEquiv X (_ , isFinSetΣ Y (λ y → _ , isFinSetFiber X Y f y)) ∣ totalEquiv f ∣ + ∙ cardΣ Y (λ y → _ , isFinSetFiber X Y f y) + +-- the pigeonhole priniple + +-- a logical lemma +private + ¬ΠQ→¬¬ΣP : (X : Type ℓ) + (P : X → Type ℓ' ) + (Q : X → Type ℓ'') + (r : (x : X) → ¬ (P x) → Q x) + → ¬ ((x : X) → Q x) → ¬ ¬ (Σ X P) + ¬ΠQ→¬¬ΣP _ _ _ r g f = g (λ x → r x (λ p → f (x , p))) + +module _ + (f : X .fst → Y .fst) + (n : ℕ) where + + fiberCount : ((y : Y .fst) → card (_ , isFinSetFiber X Y f y) ≤ n) → card X ≤ n · card Y + fiberCount h = + subst (λ a → a ≤ _) (sym (sumCardFiber X Y f)) + (sumBounded Y (λ y → card (_ , isFinSetFiber X Y f y)) n h) + + module _ + (p : card X > n · card Y) where + + ¬¬pigeonHole : ¬ ¬ (Σ[ y ∈ Y .fst ] card (_ , isFinSetFiber X Y f y) > n) + ¬¬pigeonHole = + ¬ΠQ→¬¬ΣP (Y .fst) (λ y → _ > n) (λ y → _ ≤ n) + (λ y → <-asym') (λ h → <-asym p (fiberCount h)) + + pigeonHole : ∥ Σ[ y ∈ Y .fst ] card (_ , isFinSetFiber X Y f y) > n ∥ + pigeonHole = PeirceLaw (isFinSetΣ Y (λ _ → _ , isDecProp→isFinSet m≤n-isProp (≤Dec _ _))) ¬¬pigeonHole + +-- a special case, proved in Cubical.Data.Fin.Properties + +-- a technical lemma +private + Σ∥P∥→∥ΣP∥ : (X : Type ℓ)(P : X → Type ℓ') + → Σ X (λ x → ∥ P x ∥) → ∥ Σ X P ∥ + Σ∥P∥→∥ΣP∥ _ _ (x , p) = Prop.map (λ q → x , q) p + +module _ + (f : X .fst → Y .fst) + (p : card X > card Y) where + + fiberNonEqualTerm : Σ[ y ∈ Y .fst ] card (_ , isFinSetFiber X Y f y) > 1 + → ∥ Σ[ y ∈ Y .fst ] Σ[ a ∈ fiber f y ] Σ[ b ∈ fiber f y ] ¬ a ≡ b ∥ + fiberNonEqualTerm (y , p) = Σ∥P∥→∥ΣP∥ _ _ (y , card>1→hasNonEqualTerm {X = _ , isFinSetFiber X Y f y} p) + + nonInj : Σ[ y ∈ Y .fst ] Σ[ a ∈ fiber f y ] Σ[ b ∈ fiber f y ] ¬ a ≡ b + → Σ[ x ∈ X .fst ] Σ[ x' ∈ X .fst ] (¬ x ≡ x') × (f x ≡ f x') + nonInj (y , (x , p) , (x' , q) , t) .fst = x + nonInj (y , (x , p) , (x' , q) , t) .snd .fst = x' + nonInj (y , (x , p) , (x' , q) , t) .snd .snd .fst u = + t (λ i → u i , isSet→SquareP (λ i j → isFinSet→isSet (Y .snd)) p q (cong f u) refl i) + nonInj (y , (x , p) , (x' , q) , t) .snd .snd .snd = p ∙ sym q + + pigeonHole' : ∥ Σ[ x ∈ X .fst ] Σ[ x' ∈ X .fst ] (¬ x ≡ x') × (f x ≡ f x') ∥ + pigeonHole' = + Prop.map nonInj + (Prop.rec isPropPropTrunc fiberNonEqualTerm + (pigeonHole {X = X} {Y = Y} f 1 (subst (λ a → _ > a) (sym (·-identityˡ _)) p))) + +-- cardinality and injection/surjection + +module _ + (X : FinSet ℓ ) + (Y : FinSet ℓ') where + + module _ + (f : X .fst → Y .fst) where + + card↪Inequality' : isEmbedding f → card X ≤ card Y + card↪Inequality' p = + subst2 (_≤_) + (sym (sumCardFiber X Y f)) + (·-identityˡ _) + (sumBounded Y (λ y → card (_ , isFinSetFiber X Y f y)) 1 + (λ y → isProp→card≤1 (_ , isFinSetFiber X Y f y) + (isEmbedding→hasPropFibers p y))) + + card↠Inequality' : isSurjection f → card X ≥ card Y + card↠Inequality' p = + subst2 (_≥_) + (sym (sumCardFiber X Y f)) + (·-identityˡ _) + (sumBoundedBelow Y (λ y → card (_ , isFinSetFiber X Y f y)) 1 + (λ y → isInhab→card>0 (_ , isFinSetFiber X Y f y) (p y))) + + card↪Inequality : ∥ X .fst ↪ Y .fst ∥ → card X ≤ card Y + card↪Inequality = Prop.rec m≤n-isProp (λ (f , p) → card↪Inequality' f p) + + card↠Inequality : ∥ X .fst ↠ Y .fst ∥ → card X ≥ card Y + card↠Inequality = Prop.rec m≤n-isProp (λ (f , p) → card↠Inequality' f p) + +-- maximal value of numerical functions + +module _ + (X : Type ℓ) + (f : X → ℕ) where + + module _ + (x : X) where + + isMax : Type ℓ + isMax = (x' : X) → f x' ≤ f x + + isPropIsMax : isProp isMax + isPropIsMax = isPropΠ (λ _ → m≤n-isProp) + + uniqMax : (x x' : X) → isMax x → isMax x' → f x ≡ f x' + uniqMax x x' p q = ≤-antisym (q x) (p x') + + ΣMax : Type ℓ + ΣMax = Σ[ x ∈ X ] isMax x + + ∃Max : Type ℓ + ∃Max = ∥ ΣMax ∥ + + ∃Max→maxValue : ∃Max → ℕ + ∃Max→maxValue = + SetElim.rec→Set + isSetℕ (λ (x , p) → f x) + (λ (x , p) (x' , q) → uniqMax x x' p q) + +-- lemma about maximal value on sum type +module _ + (X : Type ℓ ) + (Y : Type ℓ') + (f : X ⊎ Y → ℕ) where + + ΣMax⊎-case : ((x , p) : ΣMax X (f ∘ inl))((y , q) : ΣMax Y (f ∘ inr)) + → Trichotomy (f (inl x)) (f (inr y)) → ΣMax (X ⊎ Y) f + ΣMax⊎-case (x , p) (y , q) (lt r) .fst = inr y + ΣMax⊎-case (x , p) (y , q) (lt r) .snd (inl x') = ≤-trans (p x') (<-weaken r) + ΣMax⊎-case (x , p) (y , q) (lt r) .snd (inr y') = q y' + ΣMax⊎-case (x , p) (y , q) (eq r) .fst = inr y + ΣMax⊎-case (x , p) (y , q) (eq r) .snd (inl x') = ≤-trans (p x') (_ , r) + ΣMax⊎-case (x , p) (y , q) (eq r) .snd (inr y') = q y' + ΣMax⊎-case (x , p) (y , q) (gt r) .fst = inl x + ΣMax⊎-case (x , p) (y , q) (gt r) .snd (inl x') = p x' + ΣMax⊎-case (x , p) (y , q) (gt r) .snd (inr y') = ≤-trans (q y') (<-weaken r) + + ∃Max⊎ : ∃Max X (f ∘ inl) → ∃Max Y (f ∘ inr) → ∃Max (X ⊎ Y) f + ∃Max⊎ = Prop.map2 (λ p q → ΣMax⊎-case p q (_≟_ _ _)) + +ΣMax𝟙 : (f : 𝟙 {ℓ} .fst → ℕ) → ΣMax _ f +ΣMax𝟙 f .fst = tt* +ΣMax𝟙 f .snd x = _ , cong f (sym (isContrUnit* .snd x)) + +∃Max𝟙 : (f : 𝟙 {ℓ} .fst → ℕ) → ∃Max _ f +∃Max𝟙 f = ∣ ΣMax𝟙 f ∣ + +∃Max𝔽in : (n : ℕ)(f : 𝔽in {ℓ} n .fst → ℕ)(x : ∥ 𝔽in {ℓ} n .fst ∥) → ∃Max _ f +∃Max𝔽in {ℓ = ℓ} 0 _ x = Empty.rec (<→≢ (isInhab→card>0 (𝔽in 0) x) (card𝟘 {ℓ = ℓ})) +∃Max𝔽in 1 f _ = + subst (λ X → (f : X .fst → ℕ) → ∃Max _ f) (sym 𝔽in1≡𝟙) ∃Max𝟙 f +∃Max𝔽in (suc (suc n)) f _ = + ∃Max⊎ (𝟙 .fst) (𝔽in (suc n) .fst) f (∃Max𝟙 (f ∘ inl)) (∃Max𝔽in (suc n) (f ∘ inr) ∣ * {n = n} ∣) + +module _ + (X : FinSet ℓ) + (f : X .fst → ℕ) + (x : ∥ X .fst ∥) where + + ∃MaxFinSet : ∃Max _ f + ∃MaxFinSet = + elimProp + (λ X → (f : X .fst → ℕ)(x : ∥ X .fst ∥) → ∃Max _ f) + (λ X → isPropΠ2 (λ _ _ → isPropPropTrunc)) ∃Max𝔽in X f x + + maxValue : ℕ + maxValue = ∃Max→maxValue _ _ ∃MaxFinSet + +-- card induces equivalence from set truncation of FinSet to natural numbers + +open Iso + +Iso-∥FinSet∥₂-ℕ : Iso ∥ FinSet ℓ ∥₂ ℕ +Iso-∥FinSet∥₂-ℕ .fun = Set.rec isSetℕ card +Iso-∥FinSet∥₂-ℕ .inv n = ∣ 𝔽in n ∣₂ +Iso-∥FinSet∥₂-ℕ .rightInv n = card𝔽in n +Iso-∥FinSet∥₂-ℕ {ℓ = ℓ} .leftInv = + Set.elim {B = λ X → ∣ 𝔽in (Set.rec isSetℕ card X) ∣₂ ≡ X} + (λ X → isSetPathImplicit) + (elimProp (λ X → ∣ 𝔽in (card X) ∣₂ ≡ ∣ X ∣₂) (λ X → squash₂ _ _) + (λ n i → ∣ 𝔽in (card𝔽in {ℓ = ℓ} n i) ∣₂)) + +-- this is the definition of natural numbers you learned from school +∥FinSet∥₂≃ℕ : ∥ FinSet ℓ ∥₂ ≃ ℕ +∥FinSet∥₂≃ℕ = isoToEquiv Iso-∥FinSet∥₂-ℕ + +-- FinProp is equivalent to Bool + +Bool→FinProp : Bool → FinProp ℓ +Bool→FinProp true = 𝟙 , isPropUnit* +Bool→FinProp false = 𝟘 , isProp⊥* + +injBool→FinProp : (x y : Bool) → Bool→FinProp {ℓ = ℓ} x ≡ Bool→FinProp y → x ≡ y +injBool→FinProp true true _ = refl +injBool→FinProp false false _ = refl +injBool→FinProp true false p = Empty.rec (snotz (cong (card ∘ fst) p)) +injBool→FinProp false true p = Empty.rec (znots (cong (card ∘ fst) p)) + +isEmbeddingBool→FinProp : isEmbedding (Bool→FinProp {ℓ = ℓ}) +isEmbeddingBool→FinProp = injEmbedding isSetBool isSetFinProp (λ {x} {y} → injBool→FinProp x y) + +card-case : (P : FinProp ℓ) → {n : ℕ} → card (P .fst) ≡ n → Σ[ x ∈ Bool ] Bool→FinProp x ≡ P +card-case P {n = 0} p = false , FinProp≡ (𝟘 , isProp⊥*) P .fst (cong fst (sym (card≡0 {X = P .fst} p))) +card-case P {n = 1} p = true , FinProp≡ (𝟙 , isPropUnit*) P .fst (cong fst (sym (card≡1 {X = P .fst} p))) +card-case P {n = suc (suc n)} p = + Empty.rec (¬-<-zero (pred-≤-pred (subst (λ a → a ≤ 1) p (isProp→card≤1 (P .fst) (P .snd))))) + +isSurjectionBool→FinProp : isSurjection (Bool→FinProp {ℓ = ℓ}) +isSurjectionBool→FinProp P = ∣ card-case P refl ∣ + +FinProp≃Bool : FinProp ℓ ≃ Bool +FinProp≃Bool = + invEquiv (Bool→FinProp , + isEmbedding×isSurjection→isEquiv (isEmbeddingBool→FinProp , isSurjectionBool→FinProp)) + +isFinSetFinProp : isFinSet (FinProp ℓ) +isFinSetFinProp = EquivPresIsFinSet (invEquiv FinProp≃Bool) isFinSetBool diff --git a/Cubical/Data/FinSet/Constructors.agda b/Cubical/Data/FinSet/Constructors.agda index 7221a9b014..5c15029ca9 100644 --- a/Cubical/Data/FinSet/Constructors.agda +++ b/Cubical/Data/FinSet/Constructors.agda @@ -1,6 +1,7 @@ {- -Closure properties of FinSet under several type constructors. +This files contains: +- Facts about constructions on finite sets, especially when they preserve finiteness. -} {-# OPTIONS --safe #-} @@ -9,24 +10,26 @@ module Cubical.Data.FinSet.Constructors where open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_) +open import Cubical.Foundations.Univalence -open import Cubical.HITs.PropositionalTruncation renaming (rec to TruncRec) +open import Cubical.HITs.PropositionalTruncation as Prop open import Cubical.Data.Nat open import Cubical.Data.Unit -open import Cubical.Data.Empty renaming (rec to EmptyRec) +open import Cubical.Data.Empty as Empty 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.SumFin renaming (Fin to SumFin) 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.Fibration open import Cubical.Functions.Embedding open import Cubical.Functions.Surjection @@ -84,6 +87,8 @@ module _ ≃FinΠ : ≃Fin ((x : X) → Y x) ≃FinΠ = ≃SumFin→Fin ≃SumFinΠ +-- closedness under several type constructors + module _ (X : FinSet ℓ) (Y : X .fst → FinSet ℓ') where @@ -123,11 +128,14 @@ module _ 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) + isFinSet∥∥ : isFinSet ∥ X .fst ∥ + isFinSet∥∥ = Prop.rec isPropIsFinSet (λ p → ∣ ≃Fin∥∥ (X .fst) p ∣) (X .snd) + 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) + isFinSetIsProp : isFinSet (isProp (X .fst)) + isFinSetIsProp = isFinSetΠ2 X (λ _ → X) (λ x x' → _ , isFinSet≡ x x') module _ (X : FinSet ℓ ) @@ -159,6 +167,12 @@ module _ isFinSet≃ : isFinSet (X .fst ≃ Y .fst) isFinSet≃ = isFinSetΣ (_ , isFinSet→) (λ f → _ , isFinSetIsEquiv X Y f) +module _ + (X Y : FinSet ℓ ) where + + isFinSetType≡ : isFinSet (X .fst ≡ Y .fst) + isFinSetType≡ = EquivPresIsFinSet (invEquiv univalence) (isFinSet≃ X Y) + module _ (X : FinSet ℓ) where @@ -194,3 +208,39 @@ module _ isFinSet↠ : isFinSet (X .fst ↠ Y .fst) isFinSet↠ = isFinSetΣ (_ , isFinSet→ X Y) (λ f → _ , isFinSetIsSurjection X Y f) + +-- a criterion of being finite set + +module _ + (X : Type ℓ)(Y : FinSet ℓ') + (f : X → Y .fst) + (h : (y : Y .fst) → isFinSet (fiber f y)) where + + isFinSetTotal : isFinSet X + isFinSetTotal = EquivPresIsFinSet (invEquiv (totalEquiv f)) (isFinSetΣ Y (λ y → _ , h y)) + +-- a criterion of fibers being finite sets, more general than the previous result + +module _ + (X : FinSet ℓ) + (Y : Type ℓ')(h : Discrete Y) + (f : X. fst → Y) where + + isFinSetFiberDec : (y : Y) → isFinSet (fiber f y) + isFinSetFiberDec y = isFinSetΣ X (λ x → _ , isDecProp→isFinSet (Discrete→isSet h _ _) (h (f x) y)) + +-- decidable predicate + +module _ + (X : FinSet ℓ) + (P : X .fst → Type ℓ') + (h : (x : X .fst) → isProp (P x)) + (dec : (x : X .fst) → Dec (P x)) where + + DecΣ : Dec ∥ Σ (X .fst) P ∥ + DecΣ = isFinSet→Dec∥∥ (isFinSetΣ X (λ x → _ , isDecProp→isFinSet (h x) (dec x))) + + DecΠ : Dec ((x : X .fst) → P x) + DecΠ = + EquivPresDec (propTruncIdempotent≃ (isPropΠ h)) + (isFinSet→Dec∥∥ (isFinSetΠ X (λ x → _ , isDecProp→isFinSet (h x) (dec x)))) diff --git a/Cubical/Data/FinSet/FiniteChoice.agda b/Cubical/Data/FinSet/FiniteChoice.agda index 0fe23135d4..0e5cb7c862 100644 --- a/Cubical/Data/FinSet/FiniteChoice.agda +++ b/Cubical/Data/FinSet/FiniteChoice.agda @@ -1,8 +1,7 @@ {- Axiom of Finite Choice - -Yep, it's a theorem actually. +- Yep, it's a theorem actually. -} {-# OPTIONS --safe #-} @@ -11,9 +10,9 @@ module Cubical.Data.FinSet.FiniteChoice where open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_) -open import Cubical.HITs.PropositionalTruncation renaming (rec to TruncRec ; elim to TruncElim) +open import Cubical.HITs.PropositionalTruncation as Prop open import Cubical.Data.Nat open import Cubical.Data.Unit @@ -64,7 +63,7 @@ module _ choice≃ : ((x : X) → ∥ Y x ∥) ≃ ∥ ((x : X) → Y x) ∥ choice≃ = - TruncRec + Prop.rec (isOfHLevel≃ 1 (isPropΠ (λ x → isPropPropTrunc)) (isPropPropTrunc)) (λ p → choice≃' X p Y) p diff --git a/Cubical/Data/FinSet/Induction.agda b/Cubical/Data/FinSet/Induction.agda new file mode 100644 index 0000000000..9e321bd874 --- /dev/null +++ b/Cubical/Data/FinSet/Induction.agda @@ -0,0 +1,132 @@ +{- + +Inductive eliminators to establish properties of all finite sets directly + +-} +{-# OPTIONS --safe #-} + +module Cubical.Data.FinSet.Induction where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_) +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence + +open import Cubical.HITs.PropositionalTruncation as Prop +open import Cubical.HITs.SetTruncation as Set + +open import Cubical.Data.Nat + renaming (_+_ to _+ℕ_) hiding (elim) +open import Cubical.Data.Unit +open import Cubical.Data.Empty +open import Cubical.Data.Sum + +open import Cubical.Data.Fin +open import Cubical.Data.SumFin renaming (Fin to SumFin) +open import Cubical.Data.FinSet.Base +open import Cubical.Data.FinSet.Properties +open import Cubical.Data.FinSet.Constructors + +private + variable + ℓ ℓ' : Level + +-- definitions mimicking that of natural numbers + +module _ + {ℓ : Level} where + + 𝟘 : FinSet ℓ + 𝟘 = ⊥* , ∣ 0 , uninhabEquiv rec* ¬Fin0 ∣ + + 𝟙 : FinSet ℓ + 𝟙 = Unit* , isContr→isFinSet (isContrUnit*) + + _+_ : FinSet ℓ → FinSet ℓ → FinSet ℓ + X + Y = X .fst ⊎ Y .fst , isFinSet⊎ X Y + + -- 𝔽in can be seen as a universe polymorphic version of SumFin + 𝔽in : ℕ → FinSet ℓ + 𝔽in 0 = 𝟘 + 𝔽in (suc n) = 𝟙 + 𝔽in n + + -- useful properties + + 𝟘≃Empty : 𝟘 .fst ≃ ⊥ + 𝟘≃Empty = uninhabEquiv rec* (λ x → x) + + 𝟙≃Unit : 𝟙 .fst ≃ Unit + 𝟙≃Unit = isContr→≃Unit (isContrUnit*) + + * : {n : ℕ} → 𝔽in (suc n) .fst + * = inl tt* + + 𝔽in≃SumFin : (n : ℕ) → 𝔽in n .fst ≃ SumFin n + 𝔽in≃SumFin 0 = 𝟘≃Empty + 𝔽in≃SumFin (suc n) = ⊎-equiv 𝟙≃Unit (𝔽in≃SumFin n) + + 𝔽in≃Fin : (n : ℕ) → 𝔽in n .fst ≃ Fin n + 𝔽in≃Fin n = 𝔽in≃SumFin n ⋆ SumFin≃Fin n + + -- 𝔽in preserves addition + + 𝟘+X≡X : {X : FinSet ℓ} → 𝟘 + X ≡ X + 𝟘+X≡X {X = X} i .fst = ua (⊎-swap-≃ ⋆ ⊎-equiv (idEquiv (X .fst)) 𝟘≃Empty ⋆ ⊎-⊥-≃) i + 𝟘+X≡X {X = X} i .snd = + isProp→PathP {B = λ i → isFinSet (𝟘+X≡X {X = X} i .fst)} + (λ _ → isPropIsFinSet) ((𝟘 + X) .snd) (X .snd) i + + 𝔽in1≡𝟙 : 𝔽in 1 ≡ 𝟙 + 𝔽in1≡𝟙 i .fst = ua (⊎-equiv (idEquiv (𝟙 .fst)) 𝟘≃Empty ⋆ ⊎-⊥-≃) i + 𝔽in1≡𝟙 i .snd = + isProp→PathP {B = λ i → isFinSet (𝔽in1≡𝟙 i .fst)} + (λ _ → isPropIsFinSet) (𝔽in 1 .snd) (𝟙 .snd) i + + 𝔽in+ : (m n : ℕ) → 𝔽in m + 𝔽in n ≡ 𝔽in (m +ℕ n) + 𝔽in+ 0 n = 𝟘+X≡X + 𝔽in+ (suc m) n i .fst = (ua (⊎-assoc-≃) ∙ (λ i → (𝟙 + 𝔽in+ m n i) .fst)) i + 𝔽in+ (suc m) n i .snd = + isProp→PathP {B = λ i → isFinSet (𝔽in+ (suc m) n i .fst)} + (λ _ → isPropIsFinSet) ((𝔽in (suc m) + 𝔽in n) .snd) (𝔽in (suc m +ℕ n) .snd) i + +-- every finite sets are merely equal to some 𝔽in + +∣≡𝔽in∣ : (X : FinSet ℓ) → ∥ Σ[ n ∈ ℕ ] X ≡ 𝔽in n ∥ +∣≡𝔽in∣ X = Prop.map (λ (n , p) → n , path X (n , p)) (X .snd) + where + path : (X : FinSet ℓ) → ((n , _) : ≃Fin (X .fst)) → X ≡ 𝔽in n + path X (n , p) i .fst = ua (p ⋆ invEquiv (𝔽in≃Fin n)) i + path X (n , p) i .snd = + isProp→PathP {B = λ i → isFinSet (path X (n , p) i .fst)} + (λ _ → isPropIsFinSet) (X .snd) (𝔽in n .snd) i + +-- the eliminators + +module _ + (P : FinSet ℓ → Type ℓ') + (h : (X : FinSet ℓ) → isProp (P X)) where + + module _ + (p : (n : ℕ) → P (𝔽in n)) where + + elimProp : (X : FinSet ℓ) → P X + elimProp X = Prop.rec (h X) (λ (n , q) → transport (λ i → P (q (~ i))) (p n)) (∣≡𝔽in∣ X) + + module _ + (p0 : P 𝟘) + (p1 : {X : FinSet ℓ} → P X → P (𝟙 + X)) where + + elimProp𝔽in : (n : ℕ) → P (𝔽in n) + elimProp𝔽in 0 = p0 + elimProp𝔽in (suc n) = p1 (elimProp𝔽in n) + + elimProp𝟙+ : (X : FinSet ℓ) → P X + elimProp𝟙+ = elimProp elimProp𝔽in + + module _ + (p0 : P 𝟘)(p1 : P 𝟙) + (p+ : {X Y : FinSet ℓ} → P X → P Y → P (X + Y)) where + + elimProp+ : (X : FinSet ℓ) → P X + elimProp+ = elimProp𝟙+ p0 (λ p → p+ p1 p) diff --git a/Cubical/Data/FinSet/Properties.agda b/Cubical/Data/FinSet/Properties.agda index d0064b1c52..f04cd44337 100644 --- a/Cubical/Data/FinSet/Properties.agda +++ b/Cubical/Data/FinSet/Properties.agda @@ -8,17 +8,19 @@ 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.Foundations.Equiv renaming (_∙ₑ_ to _⋆_) -open import Cubical.HITs.PropositionalTruncation +open import Cubical.HITs.PropositionalTruncation as Prop open import Cubical.Data.Nat open import Cubical.Data.Unit -open import Cubical.Data.Empty renaming (rec to EmptyRec) +open import Cubical.Data.Bool +open import Cubical.Data.Empty as Empty 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.SumFin + renaming (Fin to SumFin) hiding (discreteFin) open import Cubical.Data.FinSet.Base open import Cubical.Relation.Nullary @@ -31,16 +33,26 @@ private A : Type ℓ B : Type ℓ' --- infix operator to more conveniently compose equivalences +-- operators to more conveniently compose equivalences -_⋆_ = compEquiv +module _ + {A : Type ℓ}{B : Type ℓ'}{C : Type ℓ''} where -infixr 30 _⋆_ + infixr 30 _⋆̂_ + + _⋆̂_ : ∥ A ≃ B ∥ → ∥ B ≃ C ∥ → ∥ A ≃ C ∥ + _⋆̂_ = Prop.map2 (_⋆_) + +module _ + {A : Type ℓ}{B : Type ℓ'} where + + ∣invEquiv∣ : ∥ A ≃ B ∥ → ∥ B ≃ A ∥ + ∣invEquiv∣ = Prop.map invEquiv -- useful implications EquivPresIsFinSet : A ≃ B → isFinSet A → isFinSet B -EquivPresIsFinSet e = rec isPropIsFinSet (λ (n , p) → ∣ n , compEquiv (invEquiv e) p ∣) +EquivPresIsFinSet e = Prop.rec isPropIsFinSet (λ (n , p) → ∣ n , compEquiv (invEquiv e) p ∣) isFinSetFin : {n : ℕ} → isFinSet (Fin n) isFinSetFin = ∣ _ , pathToEquiv refl ∣ @@ -48,8 +60,11 @@ isFinSetFin = ∣ _ , pathToEquiv refl ∣ isFinSetUnit : isFinSet Unit isFinSetUnit = ∣ 1 , Unit≃Fin1 ∣ +isFinSetBool : isFinSet Bool +isFinSetBool = ∣ 2 , invEquiv (SumFin2≃Bool) ⋆ SumFin≃Fin 2 ∣ + isFinSet→Discrete : isFinSet A → Discrete A -isFinSet→Discrete = rec isPropDiscrete (λ (_ , p) → EquivPresDiscrete (invEquiv p) discreteFin) +isFinSet→Discrete = Prop.rec isPropDiscrete (λ (_ , p) → EquivPresDiscrete (invEquiv p) discreteFin) isContr→isFinSet : isContr A → isFinSet A isContr→isFinSet h = ∣ 1 , isContr→≃Unit* h ⋆ invEquiv (Unit≃Unit* ) ⋆ Unit≃Fin1 ∣ @@ -58,6 +73,23 @@ isDecProp→isFinSet : isProp A → Dec A → isFinSet A isDecProp→isFinSet h (yes p) = isContr→isFinSet (inhProp→isContr p h) isDecProp→isFinSet h (no ¬p) = ∣ 0 , uninhabEquiv ¬p ¬Fin0 ∣ +isDec→isFinSet∥∥ : Dec A → isFinSet ∥ A ∥ +isDec→isFinSet∥∥ dec = isDecProp→isFinSet isPropPropTrunc (Dec∥∥ dec) + +isFinSet→Dec∥∥ : isFinSet A → Dec ∥ A ∥ +isFinSet→Dec∥∥ = + Prop.rec (isPropDec isPropPropTrunc) + (λ (_ , p) → EquivPresDec (propTrunc≃ (invEquiv p)) (Dec∥Fin∥ _)) + +isFinProp→Dec : isFinSet A → isProp A → Dec A +isFinProp→Dec p h = subst Dec (propTruncIdempotent h) (isFinSet→Dec∥∥ p) + +PeirceLaw∥∥ : isFinSet A → NonEmpty ∥ A ∥ → ∥ A ∥ +PeirceLaw∥∥ p = Dec→Stable (isFinSet→Dec∥∥ p) + +PeirceLaw : isFinSet A → NonEmpty A → ∥ A ∥ +PeirceLaw p q = PeirceLaw∥∥ p (λ f → q (λ x → f ∣ x ∣)) + {- Alternative definition of finite sets @@ -80,9 +112,9 @@ isPropIsFinSet' {A = A} (n , equivn) (m , equivm) = Σ≡Prop (λ _ → isPropPropTrunc) n≡m where Fin-n≃Fin-m : ∥ Fin n ≃ Fin m ∥ - Fin-n≃Fin-m = rec + Fin-n≃Fin-m = Prop.rec isPropPropTrunc - (rec + (Prop.rec (isPropΠ λ _ → isPropPropTrunc) (λ hm hn → ∣ Fin n ≃⟨ invEquiv hn ⟩ A ≃⟨ hm ⟩ Fin m ■ ∣) equivm @@ -90,13 +122,13 @@ isPropIsFinSet' {A = A} (n , equivn) (m , equivm) = equivn Fin-n≡Fin-m : ∥ Fin n ≡ Fin m ∥ - Fin-n≡Fin-m = rec isPropPropTrunc (∣_∣ ∘ ua) Fin-n≃Fin-m + Fin-n≡Fin-m = Prop.map ua Fin-n≃Fin-m ∥n≡m∥ : ∥ n ≡ m ∥ - ∥n≡m∥ = rec isPropPropTrunc (∣_∣ ∘ Fin-inj n m) Fin-n≡Fin-m + ∥n≡m∥ = Prop.map (Fin-inj n m) Fin-n≡Fin-m n≡m : n ≡ m - n≡m = rec (isSetℕ n m) (λ p → p) ∥n≡m∥ + n≡m = Prop.rec (isSetℕ n m) (λ p → p) ∥n≡m∥ -- logical equivalence of two definitions @@ -127,11 +159,6 @@ FinSet≃FinSet' = FinSet≡FinSet' : FinSet ℓ ≡ FinSet' ℓ FinSet≡FinSet' = ua FinSet≃FinSet' --- cardinality of finite sets - -card : FinSet ℓ → ℕ -card = fst ∘ snd ∘ FinSet→FinSet' - -- definitions to reduce problems about FinSet to SumFin ≃Fin : Type ℓ → Type ℓ diff --git a/Cubical/Data/FinSet/Quotients.agda b/Cubical/Data/FinSet/Quotients.agda new file mode 100644 index 0000000000..fff576e32a --- /dev/null +++ b/Cubical/Data/FinSet/Quotients.agda @@ -0,0 +1,127 @@ +{- + +This file contains: +- The quotient of finite sets by decidable equivalence relation is still finite, by using equivalence class. + +-} +{-# OPTIONS --safe #-} + +module Cubical.Data.FinSet.Quotients where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_) + +open import Cubical.HITs.PropositionalTruncation as Prop +open import Cubical.HITs.SetQuotients as SetQuot +open import Cubical.HITs.SetQuotients.EqClass + +open import Cubical.Data.Sigma + +open import Cubical.Data.FinSet.Base +open import Cubical.Data.FinSet.Properties +open import Cubical.Data.FinSet.Constructors +open import Cubical.Data.FinSet.Cardinality + +open import Cubical.Relation.Nullary +open import Cubical.Relation.Nullary.DecidablePropositions +open import Cubical.Relation.Binary + +private + variable + ℓ ℓ' ℓ'' : Level + +open Iso + +module _ + (ℓ : Level) where + + Iso-DecProp-FinProp : Iso (DecProp ℓ) (FinProp ℓ) + Iso-DecProp-FinProp .fun ((P , p) , dec) = (P , isDecProp→isFinSet p dec) , p + Iso-DecProp-FinProp .inv ((P , h) , p) = (P , p) , isFinProp→Dec h p + Iso-DecProp-FinProp .leftInv ((P , p) , dec) i .fst .fst = P + Iso-DecProp-FinProp .leftInv ((P , p) , dec) i .fst .snd = p + Iso-DecProp-FinProp .leftInv ((P , p) , dec) i .snd = + isProp→PathP {B = λ i → Dec P} + (λ i → isPropDec (Iso-DecProp-FinProp .leftInv ((P , p) , dec) i .fst .snd)) + (Iso-DecProp-FinProp .inv (Iso-DecProp-FinProp .fun ((P , p) , dec)) .snd) dec i + Iso-DecProp-FinProp .rightInv ((P , h) , p) i .fst .fst = P + Iso-DecProp-FinProp .rightInv ((P , h) , p) i .fst .snd = + isProp→PathP {B = λ i → isFinSet P} (λ i → isPropIsFinSet) + (Iso-DecProp-FinProp .fun (Iso-DecProp-FinProp .inv ((P , h) , p)) .fst .snd) h i + Iso-DecProp-FinProp .rightInv ((P , h) , p) i .snd = p + +module _ + {ℓ ℓ' : Level} + (X : Type ℓ) where + + ℙFin : Type (ℓ-max ℓ (ℓ-suc ℓ')) + ℙFin = X → FinProp ℓ' + + isSetℙFin : isSet ℙFin + isSetℙFin = isSetΠ (λ _ → isSetFinProp) + + ℙFin→ℙDec : ℙFin → ℙDec {ℓ' = ℓ'} X + ℙFin→ℙDec P .fst x = P x .fst .fst , P x .snd + ℙFin→ℙDec P .snd x = isFinProp→Dec (P x .fst .snd) (P x .snd) + + Iso-ℙFin-ℙDec : Iso ℙFin (ℙDec {ℓ' = ℓ'} X) + Iso-ℙFin-ℙDec .fun = ℙFin→ℙDec + Iso-ℙFin-ℙDec .inv (P , dec) x .fst .fst = P x .fst + Iso-ℙFin-ℙDec .inv (P , dec) x .fst .snd = isDecProp→isFinSet (P x .snd) (dec x) + Iso-ℙFin-ℙDec .inv (P , dec) x .snd = P x .snd + Iso-ℙFin-ℙDec .leftInv P i x .fst .fst = P x .fst .fst + Iso-ℙFin-ℙDec .leftInv P i x .fst .snd = + isProp→PathP {B = λ i → isFinSet (P x .fst .fst)} (λ i → isPropIsFinSet) + (isDecProp→isFinSet (P x .snd) (ℙFin→ℙDec P .snd x)) (P x .fst .snd) i + Iso-ℙFin-ℙDec .leftInv P i x .snd = P x .snd + Iso-ℙFin-ℙDec .rightInv (P , dec) i .fst x = P x .fst , P x .snd + Iso-ℙFin-ℙDec .rightInv (P , dec) i .snd x = + isProp→PathP {B = λ i → Dec (P x .fst)} (λ i → isPropDec (P x .snd)) + (Iso-ℙFin-ℙDec .fun (Iso-ℙFin-ℙDec .inv (P , dec)) .snd x) (dec x) i + + ℙFin≃ℙDec : ℙFin ≃ (ℙDec {ℓ' = ℓ'} X) + ℙFin≃ℙDec = isoToEquiv Iso-ℙFin-ℙDec + +module _ + (X : FinSet ℓ) where + + isFinSetℙFin : isFinSet (ℙFin {ℓ' = ℓ'} (X .fst)) + isFinSetℙFin = isFinSet→ X (_ , isFinSetFinProp) + +open BinaryRelation + +module _ + (X : FinSet ℓ) + (R : X .fst → X .fst → Type ℓ') + (dec : (x x' : X .fst) → Dec (R x x')) where + + _∥Fin_ : Type (ℓ-max ℓ (ℓ-suc ℓ')) + _∥Fin_ = Σ[ P ∈ ℙFin {ℓ' = ℓ'} (X .fst) ] isEqClass (X .fst) R (ℙFin→ℙDec (X .fst) P .fst) + + isFinSetIsEqClass : (P : ℙFin {ℓ' = ℓ'} (X .fst)) + → isFinSet (isEqClass (X .fst) R (ℙFin→ℙDec (X .fst) P .fst)) + isFinSetIsEqClass P = + isFinSet∥∥ (_ , isFinSetΣ X (λ x → _ , + isFinSetΠ X (λ a → _ , + isFinSetType≡ (_ , P a .fst .snd) (_ , + isDec→isFinSet∥∥ (dec a x))))) + + ∥Fin≃∥Dec : _∥Fin_ ≃ _∥Dec_ (X .fst) R dec + ∥Fin≃∥Dec = Σ-cong-equiv-fst (ℙFin≃ℙDec (X .fst)) + + isFinSet∥Fin : isFinSet _∥Fin_ + isFinSet∥Fin = isFinSetΣ (_ , isFinSetℙFin X) (λ P → _ , isFinSetIsEqClass P) + +module _ + (X : FinSet ℓ) + (R : X .fst → X .fst → Type ℓ') + (h : isEquivRel R) + (dec : (x x' : X .fst) → Dec (R x x')) where + + -- the quotient of finite set by decidable equivalence relation is still finite set + isFinSetQuot : isFinSet (X .fst / R) + isFinSetQuot = + EquivPresIsFinSet + (∥Fin≃∥Dec X _ dec ⋆ ∥Dec≃∥ _ _ dec ⋆ invEquiv (equivQuot _ _ h)) (isFinSet∥Fin X _ dec) diff --git a/Cubical/Data/Nat/Base.agda b/Cubical/Data/Nat/Base.agda index 7c450c192c..427cdb8a2e 100644 --- a/Cubical/Data/Nat/Base.agda +++ b/Cubical/Data/Nat/Base.agda @@ -63,3 +63,9 @@ isOddT n = isEvenT (suc n) isZero : ℕ → Bool isZero zero = true isZero (suc n) = false + +-- exponential + +_^_ : ℕ → ℕ → ℕ +m ^ 0 = 1 +m ^ (suc n) = m · m ^ n diff --git a/Cubical/Data/Nat/Order.agda b/Cubical/Data/Nat/Order.agda index 50c5f5a44f..112d620082 100644 --- a/Cubical/Data/Nat/Order.agda +++ b/Cubical/Data/Nat/Order.agda @@ -17,7 +17,7 @@ open import Cubical.Induction.WellFounded open import Cubical.Relation.Nullary -infix 4 _≤_ _<_ +infix 4 _≤_ _<_ _≥_ _>_ _≤_ : ℕ → ℕ → Type₀ m ≤ n = Σ[ k ∈ ℕ ] k + m ≡ n @@ -25,6 +25,12 @@ m ≤ n = Σ[ k ∈ ℕ ] k + m ≡ n _<_ : ℕ → ℕ → Type₀ m < n = suc m ≤ n +_≥_ : ℕ → ℕ → Type₀ +m ≥ n = n ≤ m + +_>_ : ℕ → ℕ → Type₀ +m > n = n < m + data Trichotomy (m n : ℕ) : Type₀ where lt : m < n → Trichotomy m n eq : m ≡ n → Trichotomy m n @@ -92,6 +98,9 @@ pred-≤-pred (k , p) = k , injSuc ((sym (+-suc k _)) ∙ p) l3 : 0 ≡ i l3 = sym (snd (m+n≡0→m≡0×n≡0 l2)) +≤-+-≤ : m ≤ n → l ≤ k → m + l ≤ n + k +≤-+-≤ p q = ≤-trans (≤-+k p) (≤-k+ q) + ≤-k+-cancel : k + m ≤ k + n → m ≤ n ≤-k+-cancel {k} {m} (l , p) = l , inj-m+ (sub k m ∙ p) where @@ -154,8 +163,11 @@ predℕ-≤-predℕ {suc m} {suc n} ineq = pred-≤-pred ineq <-k+ : m < n → k + m < k + n <-k+ {m} {n} {k} p = subst (λ km → km ≤ k + n) (+-suc k m) (≤-k+ p) -+-<-+ : m < n → k < l → m + k < n + l -+-<-+ m