foundations.Finite.md.
Version of Sunday, January 22, 2023, 10:42 PM
Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3
{-# OPTIONS --without-K --exact-split #-}
module foundations.Finite where
open import foundations.Core
open import foundations.Fin
open import foundations.NaturalsType
open import foundations.Nat
open import foundations.TypesofMorphisms
isFinite : ∀ {ℓ₁} → Type ℓ₁ → Type ℓ₁
isFinite {ℓ} X = ∑[ n ∶ ℕ ] ∥ X ≃ Fin ℓ n ∥
_is-finite : ∀ {ℓ₁} → Type ℓ₁ → Type ℓ₁
A is-finite = isFinite A
isDiscrete : ∀ {ℓ₁} → Type ℓ₁ → Type ℓ₁
isDiscrete {ℓ} X = ((a b : X) → (a ≡ b) + ( a ≠ b))
being-discrete-is-prop : ∀ {ℓ} → (X : Type ℓ)
→ isSet X
→ isProp (isDiscrete X)
being-discrete-is-prop X X-is-set
= pi-is-prop λ _ → pi-is-prop (λ _
→ +-prop (X-is-set _ _) (pi-is-prop (λ _ → 𝟘-is-prop))
λ {(p , ¬p) → ⊥-elim (¬p p)})
Fin-≡-Fin
: ∀ {ℓ}{n m}
→ Fin ℓ n ≡ Fin ℓ m
→ n ≡ m
Fin-≡-Fin p = Fin₁-is-inj _ _ _ p
being-finite-is-prop
: ∀ {ℓ} {X : Type ℓ}
→ (X is-finite) is-prop
being-finite-is-prop {ℓ = ℓ}
(n , p1) (m , p2) =
let
f-prop : ((n , p1) ≡ (m , p2)) is-prop
f-prop = (∑-set ℕ-is-set
(λ a → prop-is-set trunc-is-prop) _ _)
in
trunc-elim f-prop (trunc-elim (pi-is-prop (λ _ → f-prop))
(λ e1 e2 → pair= (Fin₁-is-inj-≃ ℓ n m (≃-trans (≃-sym e1) e2)
, trunc-is-prop _ _))
p1)
p2
𝟘-is-finite : ∀ {ℓ} → (𝟘 ℓ) is-finite
𝟘-is-finite = (0 , ∣ qinv-≃ (λ ()) (((λ { (zero , ()) ; (succ _ , ())})
, (λ {(zero , ()) ; (succ _ , ())})
, λ {()})) ∣)
𝟙-is-finite : ∀ {ℓ} → (𝟙 ℓ) is-finite
𝟙-is-finite {ℓ = ℓ}
= (1 , ∣ qinv-≃ (λ { ∗ → zero , ∗}) ((λ { p → ∗})
, (λ { (zero , ∗) → idp ; (succ n , p) → ⊥-elim {ℓ}{ℓ} (n<0 ℓ {n = n} p)})
, λ { ∗ → idp}) ∣)
Fin-is-finite
: ∀ {ℓ} {n : ℕ}
→ (Fin ℓ n) is-finite
Fin-is-finite {n = n} = (n , ∣ idEqv ∣)
FinSet : ∀ {ℓ} → Type (lsuc ℓ)
FinSet {ℓ = ℓ} = ∑[ A ∶ Type ℓ ] isFinite A
cardinal : ∀ {ℓ }(X : Type ℓ) → isFinite X → ℕ
cardinal X (n , _) = n
same-cardinal
: ∀ {ℓ}
→ {X Y : Type ℓ}
→ (e : X ≃ Y)
→ (fin-X : X is-finite)
→ (fin-Y : Y is-finite)
→ cardinal X fin-X ≡ cardinal Y fin-Y
same-cardinal {ℓ}{X = X}{Y} e X-is-finite Y-is-finite
= trunc-elim (ℕ-is-set _ _)
(λ e1
→ trunc-elim (ℕ-is-set _ _)
(λ e2 → Fin₁-is-inj-≃ ℓ _ _
(≃-trans (≃-sym e1) (≃-trans e e2)))
(π₂ Y-is-finite))
(π₂ (X-is-finite))
inhabited-has-positive-cardinality
: ∀ {ℓ}{A : Type ℓ}
→ (af : A is-finite)
→ (x : A)
→ (cardinal A af) ≡ 0 → ⊥ ℓ
inhabited-has-positive-cardinality {ℓ = ℓ} A-is-finite x idp
= trunc-elim (⊥-is-prop )
(λ e → n<0 ℓ {ℓ} {π₁ (π₁ e x)} (proj₂ (apply e x)))
(proj₂ (A-is-finite))
Just for practicallity, we need the following consequence of being finite. Any property for \([n]\) holds for any finite \(n\) elements.
isFinite-→-isSet
: ∀ {ℓ} (X : Type ℓ)
→ isFinite X
→ isSet X
isFinite-→-isSet {ℓ = ℓ}
X (n , ∥X≃[n]∥)
= trunc-elim
set-is-prop
(λ e → equiv-preserves-sets (≃-sym e) (Fin-is-set ℓ))
∥X≃[n]∥
equiv-preserves-finiteness
: ∀ {ℓ}{A B : Type ℓ} -- The levels may be different in theory.
→ A ≃ B
→ isFinite A
→ isFinite B
equiv-preserves-finiteness {A = A} A≃B A-is-finite
= trunc-elim being-finite-is-prop (λ A≃[n] →
(π₁ A-is-finite) , ∣ (≃-trans (≃-sym A≃B) A≃[n]) ∣)
(π₂ A-is-finite)
equiv-preserves-decidable-equality
: ∀ {ℓ}{A B : Type ℓ} -- The levels may be different in theory.
→ A ≃ B
→ isDiscrete B
→ isDiscrete A
equiv-preserves-decidable-equality {A = A} f-≃@(f , _) B-is-discrete
x y with B-is-discrete (f x) (f y)
... | inl fx=fy = inl helper
where
helper : x ≡ y
helper = ! (rlmap-inverse-h f-≃ x)
· (ap (rapply f-≃) fx=fy) · rlmap-inverse-h f-≃ y
... | inr fx≠fy = inr (λ x=y → ⊥-elim (fx≠fy (ap f x=y)))
isFinite-→-isDec
: ∀ {ℓ} {X : Type ℓ}
→ isFinite X
→ isDiscrete X
isFinite-→-isDec {ℓ}{X = X} X-is-Finite@(n , ∥X≃[n]∥)
= trunc-elim
(pi-is-prop (λ p → pi-is-prop (\ q
→ +-prop
(isFinite-→-isSet X X-is-Finite _ _)
(pi-is-prop (λ p → ⊥-is-prop))
λ {(p≡q , p≠q) → p≠q p≡q})))
(λ e → equiv-preserves-decidable-equality e (FinIsDec ℓ))
∥X≃[n]∥
decidable-→-≡-is-finite
: ∀ {ℓ} {X : Type ℓ}
→ ((a b : X) → (a ≡ b) + ( a ≠ b))
→ ∀ x y → (x ≡ y) is-finite
decidable-→-≡-is-finite {ℓ}{X = X} dec x y = helper
where
X-is-set : isSet X
X-is-set = hedberg dec
helper : _
helper with dec x y
... | inl idp = equiv-preserves-finiteness (≃-sym eq) 𝟙-is-finite
where
eq : (x ≡ y) ≃ 𝟙 ℓ
eq = prop-inhabited-≃𝟙 (X-is-set x x) idp
... | inr x≠y = equiv-preserves-finiteness (≃-sym eq) 𝟘-is-finite
where
eq : (x ≡ y) ≃ 𝟘 ℓ
eq = qinv-≃ (λ {idp → ⊥-elim (x≠y idp)})
(((λ ()) , (λ {()}) , λ {p → ⊥-elim (x≠y p)}))
≡-finite
: ∀ {ℓ} {X : Type ℓ}
→ isFinite X
→ ∀ {x y : X} → isFinite (x ≡ y)
≡-finite {X = X} X-is-finite {x}{y} =
decidable-→-≡-is-finite (isFinite-→-isDec X-is-finite) x y
decidable-prop-is-finite
: ∀ {ℓ} {X : Type ℓ}
→ isProp X
→ X + ¬ X
→ isFinite X
decidable-prop-is-finite {ℓ} {X} X-is-prop (inl x)
= equiv-preserves-finiteness (≃-sym X-≃-𝟙) 𝟙-is-finite
where
X-≃-𝟙 : X ≃ 𝟙 ℓ
X-≃-𝟙 = prop-inhabited-≃𝟙 X-is-prop x
decidable-prop-is-finite {ℓ} {X} X-is-prop (inr ¬X)
= equiv-preserves-finiteness (≃-sym X-≃-𝟘) 𝟘-is-finite
where
X-≃-𝟘 : X ≃ 𝟘 ℓ
X-≃-𝟘 = prop-ext-≃ X-is-prop 𝟘-is-prop (¬X , λ ())
trunc-finite-lemma : ∀ {ℓ} → {X : Type ℓ}
→ isFinite X
→ X
→ isFinite ∥ X ∥
trunc-finite-lemma {ℓ} {X} X-is-finite a
= equiv-preserves-finiteness (≃-sym helper) 𝟙-is-finite
where
helper : ∥ X ∥ ≃ 𝟙 ℓ
helper = prop-ext-≃ trunc-is-prop 𝟙-is-prop
((λ _ → ∗) , λ { ∗ → ∣ a ∣} )
trunc-finite-zero-size : ∀ {ℓ} → {X : Type ℓ}
→ isFinite X
→ X ≃ 𝟘 ℓ
→ isFinite ∥ X ∥
trunc-finite-zero-size {ℓ} {X} X-is-finite e
= equiv-preserves-finiteness (≃-sym helper) 𝟘-is-finite
where
helper : ∥ X ∥ ≃ 𝟘 ℓ
helper = prop-ext-≃ trunc-is-prop 𝟘-is-prop
((λ x → trunc-elim 𝟘-is-prop (apply e) x) , λ {()})
trunc-is-finite-positive-size : ∀ {ℓ} → {X : Type ℓ}
→ ((m , p) : isFinite X)
→ _<_ ℓ 0 m
→ isFinite (∥ X ∥)
trunc-is-finite-positive-size {ℓ} {X} (m , p) o
= 1 , trunc-elim trunc-is-prop (λ e →
∣ ≃-trans
( prop-ext-≃ trunc-is-prop 𝟙-is-prop ((λ _ → ∗)
, λ _ → ∣ (rapply e) (zero , o) ∣))
(𝟙-≃-⟦1⟧ ℓ) ∣ ) p
∥∥-finite
: ∀ {ℓ} → {X : Type ℓ}
→ isFinite X
→ isFinite ∥ X ∥
∥∥-finite {ℓ}{X} X-is-finite
with _≟nat_ ℓ (π₁ X-is-finite) zero
... | yes idp = trunc-elim being-finite-is-prop
( λ X≃[0] → trunc-finite-zero-size X-is-finite
(≃-trans X≃[0] (≃-sym (𝟘-≃-⟦0⟧ ℓ))) ) (π₂ X-is-finite)
... | no n>0 = trunc-is-finite-positive-size X-is-finite (n≠0 ℓ n>0)
module
_
(∏-finite : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂}
→ isFinite A → ((a : A) → isFinite (B a)) → isFinite (∏ A B))
(∑-finite : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂}
→ isFinite A → ((a : A) → isFinite (B a)) → isFinite (∑ A B))
where
≃-finite
: ∀ {ℓ} → {X Y : Type ℓ}
→ isFinite X → isFinite Y
-- ──────────────────────
→ isFinite (X ≃ Y)
≃-finite {X = X} {Y} X-is-finite Y-is-finite
= ∑-finite (∏-finite X-is-finite (λ _ → Y-is-finite))
(λ _ → ∏-finite Y-is-finite
(λ _ → contr-is-finite))
where
fib-is-finite : ∀ {f : X → Y} → {b : Y} → isFinite (fib f b)
fib-is-finite {f = f} {b}
= ∑-finite X-is-finite (λ _ → ≡-finite Y-is-finite)
contr-is-finite : ∀ {f : X → Y} → {b : Y} → isFinite (isContr (fib f b))
contr-is-finite {f = f} {b} = ∑-finite fib-is-finite (λ _ →
∏-finite fib-is-finite (λ _ → ≡-finite fib-is-finite))
(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides (2022-07-06)(d3a4a8cf) minors by jonathan.cubides (2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides (2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides (2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides (2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides (2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides (2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides (2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides (2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides (2021-12-15)(0630ce66) Minor fixes by jonathan.cubides (2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides (2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides (2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides (2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides