Merge pull request #630 from kangrongji/combinatorics

Cardinality and Quotients of Finite Sets

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

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)

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_)

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

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

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

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

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

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)

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)

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)

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)

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

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 ()

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

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)

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))

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))