Rijke Finite Types and the Number of Finite Groups

Cubical/Data/Bool/Base.agda

@@ -61,6 +61,10 @@ Bool→Type : Bool → Type₀
 Bool→Type true = Unit
 Bool→Type false = ⊥
 
+Bool→Type* : Bool → Type ℓ
+Bool→Type* true = Unit*
+Bool→Type* false = ⊥*
+
 True : Dec A → Type₀
 True Q = Bool→Type (Dec→Bool Q)
 

Cubical/Data/Bool/Properties.agda

@@ -6,21 +6,28 @@ open import Cubical.Core.Everything
 open import Cubical.Functions.Involution
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
 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 as Empty
 open import Cubical.Data.Sigma
 
+open import Cubical.HITs.PropositionalTruncation hiding (rec)
+
 open import Cubical.Relation.Nullary
 open import Cubical.Relation.Nullary.DecidableEq
 
+private
+  variable
+    ℓ : Level
+    A : Type ℓ
+
 notnot : ∀ x → not (not x) ≡ x
 notnot true  = refl
 notnot false = refl
@@ -41,9 +48,6 @@ notEq : Bool ≡ Bool
 notEq = involPath {f = not} notnot
 
 private
-  variable
-    ℓ : Level
-
   -- This computes to false as expected
   nfalse : Bool
   nfalse = transp (λ i → notEq i) i0 true
@@ -222,14 +226,129 @@ Iso.leftInv IsoBool→∙ (f , p) =
   ΣPathP ((funExt (λ { false → refl ; true → sym p}))
         , λ i j → p (~ i ∨ j))
 
+-- import here to avoid conflicts
+open import Cubical.Data.Unit
+
+-- relation to hProp
+
+BoolProp≃BoolProp* : {a : Bool} → Bool→Type a ≃ Bool→Type* {ℓ} a
+BoolProp≃BoolProp* {a = true} = Unit≃Unit*
+BoolProp≃BoolProp* {a = false} = uninhabEquiv Empty.rec Empty.rec*
+
+Bool→TypeInj : (a b : Bool) → Bool→Type a ≃ Bool→Type b → a ≡ b
+Bool→TypeInj true true _ = refl
+Bool→TypeInj true false p = Empty.rec (p .fst tt)
+Bool→TypeInj false true p = Empty.rec (invEq p tt)
+Bool→TypeInj false false _ = refl
+
+Bool→TypeInj* : (a b : Bool) → Bool→Type* {ℓ} a ≃ Bool→Type* {ℓ} b → a ≡ b
+Bool→TypeInj* true true _ = refl
+Bool→TypeInj* true false p = Empty.rec* (p .fst tt*)
+Bool→TypeInj* false true p = Empty.rec* (invEq p tt*)
+Bool→TypeInj* false false _ = refl
+
+isPropBool→Type : {a : Bool} → isProp (Bool→Type a)
+isPropBool→Type {a = true} = isPropUnit
+isPropBool→Type {a = false} = isProp⊥
+
+isPropBool→Type* : {a : Bool} → isProp (Bool→Type* {ℓ} a)
+isPropBool→Type* {a = true} = isPropUnit*
+isPropBool→Type* {a = false} = isProp⊥*
+
+DecBool→Type : {a : Bool} → Dec (Bool→Type a)
+DecBool→Type {a = true} = yes tt
+DecBool→Type {a = false} = no (λ x → x)
+
+DecBool→Type* : {a : Bool} → Dec (Bool→Type* {ℓ} a)
+DecBool→Type* {a = true} = yes tt*
+DecBool→Type* {a = false} = no (λ (lift x) → x)
+
+Dec→DecBool : {P : Type ℓ} → (dec : Dec P) → P → Bool→Type (Dec→Bool dec)
+Dec→DecBool (yes p) _ = tt
+Dec→DecBool (no ¬p) q = Empty.rec (¬p q)
+
+DecBool→Dec : {P : Type ℓ} → (dec : Dec P) → Bool→Type (Dec→Bool dec) → P
+DecBool→Dec (yes p) _ = p
+
+Dec≃DecBool : {P : Type ℓ} → (h : isProp P)(dec : Dec P) → P ≃ Bool→Type (Dec→Bool dec)
+Dec≃DecBool h dec = propBiimpl→Equiv h isPropBool→Type (Dec→DecBool dec) (DecBool→Dec dec)
+
+Bool≡BoolDec : {a : Bool} → a ≡ Dec→Bool (DecBool→Type {a = a})
+Bool≡BoolDec {a = true} = refl
+Bool≡BoolDec {a = false} = refl
+
+Dec→DecBool* : {P : Type ℓ} → (dec : Dec P) → P → Bool→Type* {ℓ} (Dec→Bool dec)
+Dec→DecBool* (yes p) _ = tt*
+Dec→DecBool* (no ¬p) q = Empty.rec (¬p q)
+
+DecBool→Dec* : {P : Type ℓ} → (dec : Dec P) → Bool→Type* {ℓ} (Dec→Bool dec) → P
+DecBool→Dec* (yes p) _ = p
+
+Dec≃DecBool* : {P : Type ℓ} → (h : isProp P)(dec : Dec P) → P ≃ Bool→Type* {ℓ} (Dec→Bool dec)
+Dec≃DecBool* h dec = propBiimpl→Equiv h isPropBool→Type* (Dec→DecBool* dec) (DecBool→Dec* dec)
+
+Bool≡BoolDec* : {a : Bool} → a ≡ Dec→Bool (DecBool→Type* {ℓ} {a = a})
+Bool≡BoolDec* {a = true} = refl
+Bool≡BoolDec* {a = false} = refl
+
+Bool→Type× : (a b : Bool) → Bool→Type (a and b) → Bool→Type a × Bool→Type b
+Bool→Type× true true _ = tt , tt
+Bool→Type× true false p = Empty.rec p
+Bool→Type× false true p = Empty.rec p
+Bool→Type× false false p = Empty.rec p
+
+Bool→Type×' : (a b : Bool) → Bool→Type a × Bool→Type b → Bool→Type (a and b)
+Bool→Type×' true true _ = tt
+Bool→Type×' true false (_ , p) = Empty.rec p
+Bool→Type×' false true (p , _) = Empty.rec p
+Bool→Type×' false false (p , _) = Empty.rec p
+
+Bool→Type×≃ : (a b : Bool) → Bool→Type a × Bool→Type b ≃ Bool→Type (a and b)
+Bool→Type×≃ a b =
+  propBiimpl→Equiv (isProp× isPropBool→Type isPropBool→Type) isPropBool→Type
+    (Bool→Type×' a b) (Bool→Type× a b)
+
+Bool→Type⊎ : (a b : Bool) → Bool→Type (a or b) → Bool→Type a ⊎ Bool→Type b
+Bool→Type⊎ true true _ = inl tt
+Bool→Type⊎ true false _ = inl tt
+Bool→Type⊎ false true _ = inr tt
+Bool→Type⊎ false false p = Empty.rec p
+
+Bool→Type⊎' : (a b : Bool) → Bool→Type a ⊎ Bool→Type b → Bool→Type (a or b)
+Bool→Type⊎' true true _ = tt
+Bool→Type⊎' true false _ = tt
+Bool→Type⊎' false true _ = tt
+Bool→Type⊎' false false (inl p) = Empty.rec p
+Bool→Type⊎' false false (inr p) = Empty.rec p
+
+PropBoolP→P : (dec : Dec A) → Bool→Type (Dec→Bool dec) → A
+PropBoolP→P (yes p) _ = p
+
+P→PropBoolP : (dec : Dec A) → A → Bool→Type (Dec→Bool dec)
+P→PropBoolP (yes p) _ = tt
+P→PropBoolP (no ¬p) = ¬p
+
+Bool≡ : Bool → Bool → Bool
+Bool≡ true true = true
+Bool≡ true false = false
+Bool≡ false true = false
+Bool≡ false false = true
+
+Bool≡≃ : (a b : Bool) → (a ≡ b) ≃ Bool→Type (Bool≡ a b)
+Bool≡≃ true true = isContr→≃Unit (inhProp→isContr refl (isSetBool _ _))
+Bool≡≃ true false = uninhabEquiv true≢false Empty.rec
+Bool≡≃ false true = uninhabEquiv false≢true Empty.rec
+Bool≡≃ false false = isContr→≃Unit (inhProp→isContr refl (isSetBool _ _))
 open Iso
 
+-- Bool is equivalent to bi-point type
+
 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 .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/Fin/Base.agda

@@ -68,6 +68,9 @@ fsplit (suc k , k<sn) = inr ((k , pred-≤-pred k<sn) , toℕ-injective refl)
 inject< : ∀ {m n} (m<n : m < n) → Fin m → Fin n
 inject< m<n (k , k<m) = k , <-trans k<m m<n
 
+flast : Fin (suc k)
+flast {k = k} = k , suc-≤-suc ≤-refl
+
 -- Fin 0 is empty
 ¬Fin0 : ¬ Fin 0
 ¬Fin0 (k , k<0) = ¬-<-zero k<0

Cubical/Data/FinInd.agda

@@ -16,7 +16,7 @@ This definition is weaker than `isFinSet`.
 module Cubical.Data.FinInd where
 
 open import Cubical.Data.Nat
-open import Cubical.Data.Fin
+open import Cubical.Data.SumFin
 open import Cubical.Data.Sigma
 open import Cubical.Data.FinSet
 open import Cubical.Foundations.Prelude
@@ -34,10 +34,10 @@ isFinInd : Type ℓ → Type ℓ
 isFinInd A = ∃[ n ∈ ℕ ] Fin n ↠ A
 
 isFinSet→isFinInd : isFinSet A → isFinInd A
-isFinSet→isFinInd = PT.rec
-  squash
-  λ (n , equiv) →
-    ∣ n , invEq equiv , section→isSurjection (retEq equiv) ∣
+isFinSet→isFinInd h = PT.elim
+  (λ _ → squash)
+  (λ equiv →
+    ∣ _ , invEq equiv , section→isSurjection (retEq equiv) ∣) (h .snd)
 
 isFinInd-S¹ : isFinInd S¹
 isFinInd-S¹ = ∣ 1 , f , isSurjection-f ∣

Cubical/Data/FinSet/Base.agda

@@ -13,30 +13,66 @@ 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.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)
+open import Cubical.Foundations.Univalence
 
-open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation as Prop
 
 open import Cubical.Data.Nat
-open import Cubical.Data.Fin
+open import Cubical.Data.Fin renaming (Fin to Finℕ) hiding (isSetFin)
+open import Cubical.Data.SumFin
 open import Cubical.Data.Sigma
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' ℓ'' : Level
     A : Type ℓ
 
 -- definition of (Bishop) finite sets
 
+-- this definition makes cardinality computation more efficient
 isFinSet : Type ℓ → Type ℓ
-isFinSet A = ∃[ n ∈ ℕ ] A ≃ Fin n
+isFinSet A = Σ[ n ∈ ℕ ] ∥ A ≃ Fin n ∥
+
+isFinOrd : Type ℓ → Type ℓ
+isFinOrd A = Σ[ n ∈ ℕ ] A ≃ Fin n
+
+isFinOrd→isFinSet : isFinOrd A → isFinSet A
+isFinOrd→isFinSet (_ , p) = _ , ∣ p ∣
 
 -- finite sets are sets
+
 isFinSet→isSet : isFinSet A → isSet A
-isFinSet→isSet = rec isPropIsSet (λ (_ , p) → isOfHLevelRespectEquiv 2 (invEquiv p) isSetFin)
+isFinSet→isSet p = rec isPropIsSet (λ e → isOfHLevelRespectEquiv 2 (invEquiv e) isSetFin) (p .snd)
+
+-- isFinSet is proposition
 
 isPropIsFinSet : isProp (isFinSet A)
-isPropIsFinSet = isPropPropTrunc
+isPropIsFinSet p q = Σ≡PropEquiv (λ _ → isPropPropTrunc) .fst (
+  Prop.elim2
+    (λ _ _ → isSetℕ _ _)
+    (λ p q → Fin-inj _ _ (ua (invEquiv (SumFin≃Fin _) ⋆ (invEquiv p) ⋆ q ⋆ SumFin≃Fin _)))
+    (p .snd) (q .snd))
+
+-- isFinOrd is Set
+-- ordering can be seen as extra structures over finite sets
+
+isSetIsFinOrd : isSet (isFinOrd A)
+isSetIsFinOrd = isOfHLevelΣ 2 isSetℕ (λ _ → isOfHLevel⁺≃ᵣ 1 isSetFin)
+
+-- alternative definition of isFinSet
+
+isFinSet' : Type ℓ → Type ℓ
+isFinSet' A = ∥ Σ[ n ∈ ℕ ] A ≃ Fin n ∥
+
+isFinSet→isFinSet' : isFinSet A → isFinSet' A
+isFinSet→isFinSet' (_ , p) = Prop.rec isPropPropTrunc (λ p → ∣ _ , p ∣) p
+
+isFinSet'→isFinSet : isFinSet' A → isFinSet A
+isFinSet'→isFinSet = Prop.rec isPropIsFinSet (λ (n , p) → _ , ∣ p ∣ )
+
+isFinSet≡isFinSet' : isFinSet A ≡ isFinSet' A
+isFinSet≡isFinSet' = hPropExt isPropIsFinSet isPropPropTrunc isFinSet→isFinSet' isFinSet'→isFinSet
 
 -- the type of finite sets/propositions
 
@@ -46,6 +82,11 @@ FinSet ℓ = TypeWithStr _ isFinSet
 FinProp : (ℓ : Level) → Type (ℓ-suc ℓ)
 FinProp ℓ = Σ[ P ∈ FinSet ℓ ] isProp (P .fst)
 
+-- cardinality of finite sets
+
+card : FinSet ℓ → ℕ
+card X = X .snd .fst
+
 -- equality between finite sets/propositions
 
 FinSet≡ : (X Y : FinSet ℓ) → (X .fst ≡ Y .fst) ≃ (X ≡ Y)