Martin Escardo, 2014, 21 March 2018, November-December 2019, March-April 2021 The type Fin n is a discrete set with n elements. * The function Fin : β β π€β is left-cancellable, or an injection (but not an embedding in the sense of univalent mathematics). * Exhaustive search over Fin n, or its compactness, finding a minimal element with a decidable property. * m β€ n iff there is an injection Fin m β Fin n. * Finite types, defined by the unspecified existence of an isomorphism with some Fin n. * Various forms of the pigeonhole principle, and its application to show that every element of a finite group has a finite order. * Kuratowski finiteness And more. Other interesting uses of the types Fin n is in the file https://www.cs.bham.ac.uk/~mhe/TypeTopology/ArithmeticViaEquivalence.html which proves commutativity of addition and multiplication, and more, using the corresponding properties for (finite) types. \begin{code} {-# OPTIONS --without-K --exact-split --safe #-} open import SpartanMLTT module Fin where Fin : β β π€β Μ Fin 0 = π Fin (succ n) = Fin n + π \end{code} We have zero and successor for finite sets, with the following types: \begin{code} fzero : {n : β} β Fin (succ n) fzero = inr * fsucc : {n : β} β Fin n β Fin (succ n) fsucc = inl \end{code} But it will more convenient to have them as patterns, for the sake of clarity in definitions by pattern matching: \begin{code} pattern π = inr * pattern π = inl (inr *) pattern π = inl (inl (inr *)) pattern suc i = inl i \end{code} The induction principle for Fin is proved by induction on β: \begin{code} Fin-induction : (P : (n : β) β Fin n β π€ Μ ) β ((n : β) β P (succ n) π) β ((n : β) (i : Fin n) β P n i β P (succ n) (suc i)) β (n : β) (i : Fin n) β P n i Fin-induction P Ξ² Ο 0 i = π-elim i Fin-induction P Ξ² Ο (succ n) π = Ξ² n Fin-induction P Ξ² Ο (succ n) (suc i) = Ο n i (Fin-induction P Ξ² Ο n i) \end{code} We will not use this induction principle explicitly. Instead, we will use the above pattern for similar definitions by induction. \begin{code} open import Unit-Properties positive-not-π : {n : β} {x : Fin (succ n)} β suc x β’ π positive-not-π {n} {x} p = π-is-not-π (g p) where f : Fin (succ (succ n)) β π€β Μ f π = π f (suc x) = π g : suc x β‘ π β π β‘ π g = ap f \end{code} The left cancellability of Fin uses the construction +π-cancellable defined in the module PlusOneLC.lagda. \begin{code} open import PlusOneLC open import UF-Equiv Fin-lc : (m n : β) β Fin m β Fin n β m β‘ n Fin-lc 0 0 p = refl Fin-lc (succ m) 0 p = π-elim (β p β π) Fin-lc 0 (succ n) p = π-elim (β p ββ»ΒΉ π) Fin-lc (succ m) (succ n) p = ap succ r where IH : Fin m β Fin n β m β‘ n IH = Fin-lc m n remark : Fin m + π β Fin n + π remark = p q : Fin m β Fin n q = +π-cancellable p r : m β‘ n r = IH q \end{code} Notice that Fin is an example of a map that is left-cancellable but not an embedding in the sense of univalent mathematics. Recall that a type is discrete if it has decidable equality. \begin{code} open import DiscreteAndSeparated Fin-is-discrete : (n : β) β is-discrete (Fin n) Fin-is-discrete 0 = π-is-discrete Fin-is-discrete (succ n) = +discrete (Fin-is-discrete n) π-is-discrete open import UF-Subsingletons renaming (β€Ξ© to β€) open import UF-Miscelanea Fin-is-set : (n : β) β is-set (Fin n) Fin-is-set n = discrete-types-are-sets (Fin-is-discrete n) \end{code} Added November 2019. The type Fin n is compact, or exhaustively searchable. \begin{code} open import CompactTypes Fin-Compact : (n : β) β Compact (Fin n) {π€} Fin-Compact 0 = π-Compact Fin-Compact (succ n) = +-Compact (Fin-Compact n) π-Compact Fin-Ξ -Compact : (n : β) β Ξ -Compact (Fin n) {π€} Fin-Ξ -Compact n = Ξ£-Compact-gives-Ξ -Compact (Fin n) (Fin-Compact n) Fin-Compactβ : (n : β) β Compactβ (Fin (succ n)) {π€} Fin-Compactβ n = Compact-pointed-gives-Compactβ (Fin-Compact (succ n)) π \end{code} Recall that X β£ Y is the type of left cancellable maps from X to Y, which should not be confused with the type X βͺ Y of embeddings of X into Y. However, for types that are sets, like Fin n, there is no difference between the embedding property and left cancellability. \begin{code} open import Plus-Properties open import Swap open import UF-LeftCancellable +π-cancel-lemma : {X Y : π€ Μ } β (π : X + π β£ Y + π) β β π β π β‘ π β X β£ Y +π-cancel-lemma {π€} {X} {Y} (f , l) p = g , m where g : X β Y g x = prβ (inl-preservation {π€} {π€} {π€} {π€} f p l x) a : (x : X) β f (suc x) β‘ suc (g x) a x = prβ (inl-preservation f p l x) m : left-cancellable g m {x} {x'} p = q where r = f (suc x) β‘β¨ a x β© suc (g x) β‘β¨ ap suc p β© suc (g x') β‘β¨ (a x')β»ΒΉ β© f (suc x') β q : x β‘ x' q = inl-lc (l r) +π-cancel : {X Y : π€ Μ } β is-discrete Y β X + π β£ Y + π β X β£ Y +π-cancel {π€} {X} {Y} i (f , e) = a where h : Y + π β Y + π h = swap (f π) π (+discrete i π-is-discrete (f π)) new-point-is-isolated d : left-cancellable h d = equivs-are-lc h (swap-is-equiv (f π) π (+discrete i π-is-discrete (f π)) new-point-is-isolated) f' : X + π β Y + π f' = h β f e' : left-cancellable f' e' = left-cancellable-closed-under-β f h e d p : f' π β‘ π p = swap-equationβ (f π) π (+discrete i π-is-discrete (f π)) new-point-is-isolated a : X β£ Y a = +π-cancel-lemma (f' , e') p open import NaturalsOrder open import UF-EquivalenceExamples \end{code} In set theory, natural numbers are defined as certain sets, and their order relation is inherited from the ordering of sets defined by the existence of injections, or left-cancellable maps. Here, in type theory, we have defined m β€ n by induction on m and n, in the style of Peano Arithmetic, but we can prove that this relation is characterized by this injection property: \begin{code} β£-gives-β€ : (m n : β) β (Fin m β£ Fin n) β m β€ n β£-gives-β€ 0 n e = zero-minimal n β£-gives-β€ (succ m) 0 (f , i) = π-elim (f π) β£-gives-β€ (succ m) (succ n) e = β£-gives-β€ m n (+π-cancel (Fin-is-discrete n) e) canonical-Fin-inclusion : (m n : β) β m β€ n β (Fin m β Fin n) canonical-Fin-inclusion 0 n l = unique-from-π canonical-Fin-inclusion (succ m) 0 l = π-elim l canonical-Fin-inclusion (succ m) (succ n) l = +functor IH unique-to-π where IH : Fin m β Fin n IH = canonical-Fin-inclusion m n l canonical-Fin-inclusion-lc : (m n : β) (l : m β€ n) β left-cancellable (canonical-Fin-inclusion m n l) canonical-Fin-inclusion-lc 0 n l {x} {y} p = π-elim x canonical-Fin-inclusion-lc (succ m) 0 l {x} {y} p = π-elim l canonical-Fin-inclusion-lc (succ m) (succ n) l {suc x} {suc y} p = Ξ³ where IH : canonical-Fin-inclusion m n l x β‘ canonical-Fin-inclusion m n l y β x β‘ y IH = canonical-Fin-inclusion-lc m n l Ξ³ : suc x β‘ suc y Ξ³ = ap suc (IH (inl-lc p)) canonical-Fin-inclusion-lc (succ m) (succ n) l {π} {π} p = refl β€-gives-β£ : (m n : β) β m β€ n β (Fin m β£ Fin n) β€-gives-β£ m n l = canonical-Fin-inclusion m n l , canonical-Fin-inclusion-lc m n l \end{code} An equivalent, shorter construction: \begin{code} β€-gives-β£' : (m n : β) β m β€ n β (Fin m β£ Fin n) β€-gives-β£' 0 n l = unique-from-π , (Ξ» {x} {x'} p β π-elim x) β€-gives-β£' (succ m) 0 l = π-elim l β€-gives-β£' (succ m) (succ n) l = g , j where IH : Fin m β£ Fin n IH = β€-gives-β£' m n l f : Fin m β Fin n f = prβ IH i : left-cancellable f i = prβ IH g : Fin (succ m) β Fin (succ n) g = +functor f unique-to-π j : left-cancellable g j {suc x} {suc x'} p = ap suc (i (inl-lc p)) j {suc x} {π} p = π-elim (+disjoint p) j {π} {suc y} p = π-elim (+disjoint' p) j {π} {π} p = refl \end{code} Added 9th December 2019. A version of the pigeonhole principle, which uses (one direction of) the above characterization of the relation m β€ n as the existence of an injection Fin m β Fin n: \begin{code} _has-a-repetition : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ f has-a-repetition = Ξ£ x κ domain f , Ξ£ x' κ domain f , (x β’ x') Γ (f x β‘ f x') pigeonhole-principle : (m n : β) (f : Fin m β Fin n) β m > n β f has-a-repetition pigeonhole-principle m n f g = Ξ³ where a : Β¬ (Ξ£ f κ (Fin m β Fin n), left-cancellable f) a = contrapositive (β£-gives-β€ m n) (less-not-bigger-or-equal n m g) b : Β¬ left-cancellable f b l = a (f , l) c : Β¬ ((i j : Fin m) β f i β‘ f j β i β‘ j) c Ο = b (Ξ» {i} {j} β Ο i j) d : ¬¬ (f has-a-repetition) d Ο = c Ξ΄ where Ξ΅ : (i j : Fin m) β f i β‘ f j β Β¬ (i β’ j) Ξ΅ i j p Ξ½ = Ο (i , j , Ξ½ , p) Ξ΄ : (i j : Fin m) β f i β‘ f j β i β‘ j Ξ΄ i j p = ¬¬-elim (Fin-is-discrete m i j) (Ξ΅ i j p) \end{code} A classical proof ends at this point. For a constructive proof, we need more steps. \begin{code} u : (i j : Fin m) β decidable ((i β’ j) Γ (f i β‘ f j)) u i j = Γ-preserves-decidability (Β¬-preserves-decidability (Fin-is-discrete m i j)) (Fin-is-discrete n (f i) (f j)) v : (i : Fin m) β decidable (Ξ£ j κ Fin m , (i β’ j) Γ (f i β‘ f j)) v i = Fin-Compact m _ (u i) w : decidable (f has-a-repetition) w = Fin-Compact m _ v Ξ³ : f has-a-repetition Ξ³ = ¬¬-elim w d \end{code} This, of course, doesn't give the most efficient algorithm, but it does give an algorithm for computing an argument of the function whose value is repeated. Added 2nd December 2019. An isomorphic copy of the type Fin n: \begin{code} Fin' : β β π€β Μ Fin' n = Ξ£ k κ β , k < n π' : {n : β} β Fin' (succ n) π' {n} = 0 , zero-minimal n suc' : {n : β} β Fin' n β Fin' (succ n) suc' (k , l) = succ k , l Fin-unprime : (n : β) β Fin' n β Fin n Fin-unprime 0 (k , l) = π-elim l Fin-unprime (succ n) (0 , l) = π Fin-unprime (succ n) (succ k , l) = suc (Fin-unprime n (k , l)) Fin-prime : (n : β) β Fin n β Fin' n Fin-prime 0 i = π-elim i Fin-prime (succ n) (suc i) = suc' (Fin-prime n i) Fin-prime (succ n) π = π' Ξ·Fin : (n : β) β Fin-prime n β Fin-unprime n βΌ id Ξ·Fin 0 (k , l) = π-elim l Ξ·Fin (succ n) (0 , *) = refl Ξ·Fin (succ n) (succ k , l) = ap suc' (Ξ·Fin n (k , l)) Ξ΅Fin : (n : β) β Fin-unprime n β Fin-prime n βΌ id Ξ΅Fin 0 i = π-elim i Ξ΅Fin (succ n) (suc i) = ap suc (Ξ΅Fin n i) Ξ΅Fin (succ n) π = refl Fin-prime-is-equiv : (n : β) β is-equiv (Fin-prime n) Fin-prime-is-equiv n = qinvs-are-equivs (Fin-prime n) (Fin-unprime n , Ξ΅Fin n , Ξ·Fin n) β-Fin : (n : β) β Fin n β Fin' n β-Fin n = Fin-prime n , Fin-prime-is-equiv n \end{code} Added 10th Dec 2019. We define the natural order of Fin n by reduction to the natural order of β so that the canonical embedding Fin n β β is order preserving and reflecting, using the above isomorphic manifestation of the type Fin n. \begin{code} open import NaturalNumbers-Properties Finβ¦β : {n : β} β Fin n β β Finβ¦β {n} = prβ β Fin-prime n Finβ¦β-property : {n : β} (i : Fin n) β Finβ¦β i < n Finβ¦β-property {n} i = prβ (Fin-prime n i) open import UF-Embeddings Finβ¦β-is-embedding : (n : β) β is-embedding (Finβ¦β {n}) Finβ¦β-is-embedding n = β-is-embedding (equivs-are-embeddings (Fin-prime n) (Fin-prime-is-equiv n)) (prβ-is-embedding (Ξ» i β <-is-prop-valued i n)) Finβ¦β-lc : (n : β) β left-cancellable (Finβ¦β {n}) Finβ¦β-lc n = embeddings-are-lc Finβ¦β (Finβ¦β-is-embedding n) _βΊ_ _βΌ_ : {n : β} β Fin n β Fin n β π€β Μ i βΊ j = Finβ¦β i < Finβ¦β j i βΌ j = Finβ¦β i β€ Finβ¦β j _is-lower-bound-of_ : {n : β} β Fin n β (Fin n β π€ Μ ) β π€ Μ i is-lower-bound-of A = β j β A j β i βΌ j lower-bounds-of : {n : β} β (Fin n β π€ Μ ) β Fin n β π€ Μ lower-bounds-of A = Ξ» i β i is-lower-bound-of A _is-upper-bound-of_ : {n : β} β Fin n β (Fin n β π€ Μ ) β π€ Μ i is-upper-bound-of A = β j β A j β j βΌ i _is-inf-of_ : {n : β} β Fin n β (Fin n β π€ Μ ) β π€ Μ i is-inf-of A = i is-lower-bound-of A Γ i is-upper-bound-of (lower-bounds-of A) inf-is-lb : {n : β} (i : Fin n) (A : Fin n β π€ Μ ) β i is-inf-of A β i is-lower-bound-of A inf-is-lb i A = prβ inf-is-ub-of-lbs : {n : β} (i : Fin n) (A : Fin n β π€ Μ ) β i is-inf-of A β i is-upper-bound-of (lower-bounds-of A) inf-is-ub-of-lbs i A = prβ inf-construction : {n : β} (A : Fin (succ n) β π€ Μ ) β detachable A β Ξ£ i κ Fin (succ n) , i is-inf-of A Γ (Ξ£ A β A i) inf-construction {π€} {zero} A Ξ΄ = π , (l , m) , Ξ΅ where l : π is-lower-bound-of A l π _ = β€-refl 0 l (suc i) _ = π-elim i m : (j : Fin 1) β j is-lower-bound-of A β j βΌ π m π _ = β€-refl 0 m (suc i) _ = π-elim i Ξ΅ : Ξ£ A β A π Ξ΅ (π , a) = a Ξ΅ (suc i , a) = π-elim i inf-construction {π€} {succ n} A Ξ΄ = Ξ³ (Ξ΄ π) where IH : Ξ£ i κ Fin (succ n) , i is-inf-of (A β suc) Γ ((Ξ£ j κ Fin (succ n) , A (suc j)) β A (suc i)) IH = inf-construction {π€} {n} (A β suc) (Ξ΄ β suc) i : Fin (succ n) i = prβ IH l : (j : Fin (succ n)) β A (suc j) β i βΌ j l = inf-is-lb i (A β suc) (prβ (prβ IH)) u : (j : Fin (succ n)) β ((k : Fin (succ n)) β A (suc k) β j βΌ k) β j βΌ i u = inf-is-ub-of-lbs i (A β suc) (prβ (prβ IH)) Ξ³ : decidable (A π) β Ξ£ i' κ Fin (succ (succ n)) , i' is-inf-of A Γ (Ξ£ A β A i') Ξ³ (suc a) = π , (Ο , Ο) , Ξ΅ where Ο : (j : Fin (succ (succ n))) β A j β π βΌ j Ο j b = zero-minimal (Finβ¦β j) Ο : (j : Fin (succ (succ n))) β j is-lower-bound-of A β j βΌ π Ο j l = l π a Ξ΅ : Ξ£ A β A π Ξ΅ _ = a Ξ³ (inr Ξ½) = suc i , (Ο , Ο) , Ξ΅ where Ο : (j : Fin (succ (succ n))) β A j β suc i βΌ j Ο π a = π-elim (Ξ½ a) Ο (suc j) a = l j a Ο : (j : Fin (succ (succ n))) β j is-lower-bound-of A β j βΌ suc i Ο π l = zero-minimal (Finβ¦β i) Ο (suc j) l = u j (l β suc) Ξ΅ : Ξ£ A β A (suc i) Ξ΅ (π , b) = π-elim (Ξ½ b) Ξ΅ (suc j , b) = prβ (prβ IH) (j , b) inf : {n : β} (A : Fin (succ n) β π€ Μ ) β detachable A β Fin (succ n) inf A Ξ΄ = prβ (inf-construction A Ξ΄) inf-property : {n : β} (A : Fin (succ n) β π€ Μ ) (Ξ΄ : detachable A) β (inf A Ξ΄) is-inf-of A inf-property A Ξ΄ = prβ (prβ (inf-construction A Ξ΄)) inf-is-attained : {n : β} (A : Fin (succ n) β π€ Μ ) (Ξ΄ : detachable A) β Ξ£ A β A (inf A Ξ΄) inf-is-attained A Ξ΄ = prβ (prβ (inf-construction A Ξ΄)) Ξ£βα΅’β : {n : β} β (Fin n β π€ Μ ) β π€ Μ Ξ£βα΅’β {π€} {n} A = Ξ£ i κ Fin n , A i Γ (i is-lower-bound-of A) Ξ£βα΅’β-gives-Ξ£ : {n : β} (A : Fin n β π€ Μ ) β Ξ£βα΅’β A β Ξ£ A Ξ£βα΅’β-gives-Ξ£ A (i , a , _) = (i , a) Ξ£-gives-Ξ£βα΅’β : {n : β} (A : Fin n β π€ Μ ) β detachable A β Ξ£ A β Ξ£βα΅’β A Ξ£-gives-Ξ£βα΅’β {π€} {0} A Ξ΄ (i , a) = π-elim i Ξ£-gives-Ξ£βα΅’β {π€} {succ n} A Ξ΄ Ο = inf A Ξ΄ , inf-is-attained A Ξ΄ Ο , inf-is-lb (inf A Ξ΄) A (inf-property A Ξ΄) ¬¬Σ-gives-Ξ£βα΅’β : {n : β} (A : Fin n β π€ Μ ) β detachable A β ¬¬ Ξ£ A β Ξ£βα΅’β A ¬¬Σ-gives-Ξ£βα΅’β {π€} {n} A Ξ΄ u = Ξ£-gives-Ξ£βα΅’β A Ξ΄ (¬¬-elim (Fin-Compact n A Ξ΄) u) is-prop-valued : {X : π€ Μ } β (X β π₯ Μ ) β π€ β π₯ Μ is-prop-valued A = β x β is-prop (A x) open import UF-FunExt open import UF-Subsingletons-FunExt open import UF-Base Ξ£βα΅’β-is-prop : FunExt β {n : β} (A : Fin n β π€ Μ ) β is-prop-valued A β is-prop (Ξ£βα΅’β A) Ξ£βα΅’β-is-prop {π€} fe {n} A h (i , a , l) (i' , a' , l') = Ξ³ where p : i β‘ i' p = Finβ¦β-lc n (β€-anti (Finβ¦β i) (Finβ¦β i') u v) where u : i βΌ i' u = l i' a' v : i' βΌ i v = l' i a H : β j β is-prop (A j Γ (j is-lower-bound-of A)) H j = Γ-is-prop (h j) (Ξ -is-prop (fe π€β π€) (Ξ» k β Ξ -is-prop (fe π€ π€β) (Ξ» b β β€-is-prop-valued (Finβ¦β j) (Finβ¦β k)))) Ξ³ : i , a , l β‘ i' , a' , l' Ξ³ = to-Ξ£-β‘ (p , H _ _ _) \end{code} Added 8th December 2019. One defines a type to be finite, in univalent mathematics, if it is isomorphic to Fin n for some n. But one has to careful to express this, if we want finiteness to be property rather than structure, with a suitably chosen notion of existence. The following is structure rather than property. It amounts to the type of finite linear orders on X. \begin{code} finite-linear-order : π€ Μ β π€ Μ finite-linear-order X = Ξ£ n κ β , X β Fin n \end{code} Exercise: If X β Fin n, then the type Finite X has n! elements (solve elsewhere in TypeTopology). \begin{code} open import UF-Univalence open import UF-Equiv-FunExt open import UF-UniverseEmbedding open import UF-UA-FunExt type-of-linear-orders-is-β : Univalence β (Ξ£ X κ π€ Μ , finite-linear-order X) β β type-of-linear-orders-is-β {π€} ua = (Ξ£ X κ π€ Μ , Ξ£ n κ β , X β Fin n) ββ¨ i β© (Ξ£ X κ π€ Μ , Ξ£ n κ β , Fin n β X) ββ¨ ii β© (Ξ£ X κ π€ Μ , Ξ£ n κ β , Lift π€ (Fin n) β X) ββ¨ iii β© (Ξ£ X κ π€ Μ , Ξ£ n κ β , Lift π€ (Fin n) β‘ X) ββ¨ iv β© β β where fe : FunExt fe = Univalence-gives-FunExt ua i = Ξ£-cong (Ξ» X β Ξ£-cong (Ξ» n β β-Sym fe)) ii = Ξ£-cong (Ξ» X β Ξ£-cong (Ξ» n β β-Comp fe X (Lift-β π€ (Fin n)))) iii = Ξ£-cong (Ξ» X β Ξ£-cong (Ξ» n β β-sym (univalence-β (ua π€) (Lift π€ (Fin n)) X))) iv = total-fiber-is-domain (Lift π€ β Fin) \end{code} Hence one considers the following notion of finiteness, which is property rather than structure: \begin{code} open import UF-PropTrunc module finiteness (pt : propositional-truncations-exist) where open PropositionalTruncation pt public is-finite : π€ Μ β π€ Μ is-finite X = Ξ£ n κ β , β₯ X β Fin n β₯ cardinality : (X : π€ Μ ) β is-finite X β β cardinality X = prβ cardinality-β : (X : π€ Μ ) (Ο : is-finite X) β β₯ X β Fin (cardinality X Ο) β₯ cardinality-β X = prβ being-finite-is-prop : (X : π€ Μ ) β is-prop (is-finite X) being-finite-is-prop X (m , d) (n , e) = Ξ³ where a : (m n : β) β X β Fin m β X β Fin n β m β‘ n a m n d e = Fin-lc m n (β-sym d β e) b : (m n : β) β β₯ X β Fin m β₯ β β₯ X β Fin n β₯ β m β‘ n b m n = β₯β₯-recβ β-is-set (a m n) Ξ³ : m , d β‘ n , e Ξ³ = to-Ξ£-β‘ (b m n d e , β₯β₯-is-prop _ _) \end{code} Equivalently, one can define finiteness as follows, with the truncation outside the Ξ£: \begin{code} is-finite' : π€ Μ β π€ Μ is-finite' X = β n κ β , X β Fin n being-finite'-is-prop : (X : π€ Μ ) β is-prop (is-finite' X) being-finite'-is-prop X = β₯β₯-is-prop finite-unprime : (X : π€ Μ ) β is-finite' X β is-finite X finite-unprime X = β₯β₯-rec (being-finite-is-prop X) Ξ³ where Ξ³ : (Ξ£ n κ β , X β Fin n) β Ξ£ n κ β , β₯ X β Fin n β₯ Ξ³ (n , e) = n , β£ e β£ finite-prime : (X : π€ Μ ) β is-finite X β is-finite' X finite-prime X (n , s) = β₯β₯-rec β₯β₯-is-prop (Ξ» e β β£ n , e β£) s \end{code} Finite types are compact, or exhaustively searchable. \begin{code} open CompactTypesPT pt finite-β₯Compactβ₯ : {X : π€ Μ } β is-finite X β β₯ Compact X {π₯} β₯ finite-β₯Compactβ₯ {π€} {π₯} {X} (n , Ξ±) = β₯β₯-functor (Ξ» (e : X β Fin n) β Compact-closed-under-β (β-sym e) (Fin-Compact n)) Ξ± finite-β-compact : Fun-Ext β {X : π€ Μ } β is-finite X β β-Compact X {π₯} finite-β-compact fe Ο = β₯Compactβ₯-gives-β-Compact fe (finite-β₯Compactβ₯ Ο) \end{code} Finite types are discrete and hence sets: \begin{code} finite-types-are-discrete : FunExt β {X : π€ Μ } β is-finite X β is-discrete X finite-types-are-discrete fe {X} (n , s) = β₯β₯-rec (being-discrete-is-prop fe) Ξ³ s where Ξ³ : X β Fin n β is-discrete X Ξ³ (f , e) = lc-maps-reflect-discreteness f (equivs-are-lc f e) (Fin-is-discrete n) finite-types-are-sets : FunExt β {X : π€ Μ } β is-finite X β is-set X finite-types-are-sets fe Ο = discrete-types-are-sets (finite-types-are-discrete fe Ο) \end{code} Example. The pigeonhole principle holds for finite types in the following form: \begin{code} finite-pigeonhole-principle : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) (Ο : is-finite X) (Ο : is-finite Y) β cardinality X Ο > cardinality Y Ο β β₯ f has-a-repetition β₯ finite-pigeonhole-principle {π€} {π₯} {X} {Y} f (m , s) (n , t) b = Ξ³ where h : Fin m β X β Y β Fin n β f has-a-repetition h (g , d) (h , e) = r r' where f' : Fin m β Fin n f' = h β f β g r' : f' has-a-repetition r' = pigeonhole-principle m n f' b r : f' has-a-repetition β f has-a-repetition r (i , j , u , p) = g i , g j , u' , p' where u' : g i β’ g j u' = contrapositive (equivs-are-lc g d) u p' : f (g i) β‘ f (g j) p' = equivs-are-lc h e p Ξ³ : β₯ f has-a-repetition β₯ Ξ³ = β₯β₯-functorβ h (β₯β₯-functor β-sym s) t \end{code} We now consider a situation in which anonymous existence gives explicit existence: \begin{code} Ξ£βα΅’β-from-β : FunExt β {n : β} (A : Fin n β π€ Μ ) β detachable A β is-prop-valued A β β A β Ξ£βα΅’β A Ξ£βα΅’β-from-β fe A Ξ΄ h = β₯β₯-rec (Ξ£βα΅’β-is-prop fe A h) (Ξ£-gives-Ξ£βα΅’β A Ξ΄) Fin-Ξ£-from-β' : FunExt β {n : β} (A : Fin n β π€ Μ ) β detachable A β is-prop-valued A β β A β Ξ£ A Fin-Ξ£-from-β' fe A Ξ΄ h e = Ξ£βα΅’β-gives-Ξ£ A (Ξ£βα΅’β-from-β fe A Ξ΄ h e) \end{code} But the prop-valuedness of A is actually not needed, with more work: \begin{code} Fin-Ξ£-from-β : FunExt β {n : β} (A : Fin n β π€ Μ ) β detachable A β β A β Ξ£ A Fin-Ξ£-from-β {π€} fe {n} A Ξ΄ e = g Ο' where A' : Fin n β π€ Μ A' x = β₯ A x β₯ Ξ΄' : detachable A' Ξ΄' x = d (Ξ΄ x) where d : decidable (A x) β decidable (A' x) d (inl a) = inl β£ a β£ d (inr u) = inr (β₯β₯-rec π-is-prop u) f : Ξ£ A β Ξ£ A' f (x , a) = x , β£ a β£ e' : β A' e' = β₯β₯-functor f e Ο' : Ξ£ A' Ο' = Fin-Ξ£-from-β' fe A' Ξ΄' (Ξ» x β β₯β₯-is-prop) e' g : Ξ£ A' β Ξ£ A g (x , a') = x , ¬¬-elim (Ξ΄ x) (Ξ» (u : Β¬ A x) β β₯β₯-rec π-is-prop u a') \end{code} We now assume function extensionality for a while: \begin{code} module _ (fe : FunExt) where \end{code} We now consider further variations of the finite pigeonhole principle. \begin{code} repeated-values : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β X β π€ β π₯ Μ repeated-values f x = Ξ£ x' κ domain f , (x β’ x') Γ (f x β‘ f x') repetitions-detachable : {m : β} {Y : π₯ Μ } (f : Fin m β Y) β is-finite Y β detachable (repeated-values f) repetitions-detachable {π₯} {m} {Y} f (n , t) i = Fin-Compact m (Ξ» j β (i β’ j) Γ (f i β‘ f j)) (Ξ» j β Γ-preserves-decidability (Β¬-preserves-decidability (Fin-is-discrete m i j)) (finite-types-are-discrete fe (n , t) (f i) (f j))) finite-pigeonhole-principle' : {m : β} {Y : π₯ Μ } (f : Fin m β Y) (Ο : is-finite Y) β m > cardinality Y Ο β f has-a-repetition finite-pigeonhole-principle' {π₯} {m} {Y} f (n , t) b = Ξ³ where h : Y β Fin n β f has-a-repetition h (h , e) = r r' where f' : Fin m β Fin n f' = h β f r' : f' has-a-repetition r' = pigeonhole-principle m n f' b r : f' has-a-repetition β f has-a-repetition r (i , j , u , p) = i , j , u , equivs-are-lc h e p Ξ³' : β₯ f has-a-repetition β₯ Ξ³' = β₯β₯-functor h t A : Fin m β π₯ Μ A i = Ξ£ j κ Fin m , (i β’ j) Γ (f i β‘ f j) Ξ³ : f has-a-repetition Ξ³ = Fin-Ξ£-from-β fe {m} A (repetitions-detachable f (n , t)) Ξ³' \end{code} We can easily derive the construction finite-pigeonhole-principle from finite-pigeonhole-principle', but at the expense of function extensionality, which was not needed in our original construction. Further versions of the pigeonhole principle are the following. \begin{code} finite-pigeonhole-principle'' : {m : β} {Y : π₯ Μ } (f : Fin m β Y) (Ο : is-finite Y) β m > cardinality Y Ο β Ξ£βα΅’β Ξ»(i : Fin m) β repeated-values f i finite-pigeonhole-principle'' {π₯} {m} {Y} f Ο g = Ξ£-gives-Ξ£βα΅’β (repeated-values f) (repetitions-detachable f Ο) (finite-pigeonhole-principle' f Ο g) β-finite-pigeonhole-principle : {Y : π₯ Μ } (f : β β Y) β is-finite Y β f has-a-repetition β-finite-pigeonhole-principle {π₯} {Y} f (m , t) = r r' where f' : Fin (succ m) β Y f' i = f (Finβ¦β i) r' : f' has-a-repetition r' = finite-pigeonhole-principle' f'(m , t) (<-succ m) r : f' has-a-repetition β f has-a-repetition r (i , j , u , p) = Finβ¦β i , Finβ¦β j , contrapositive (Finβ¦β-lc (succ m)) u , p \end{code} Added 13th December 2019. A well-known application of the pigeonhole principle is that every element has a (minimal) finite order in a finite group. This holds more generally for any finite type equipped with a left-cancellable binary operation _Β·_ and a distinguished element e, with the same construction. \begin{code} module _ {X : π€ Μ } (Ο : is-finite X) (_Β·_ : X β X β X) (lc : (x : X) β left-cancellable (x Β·_)) (e : X) where _β_ : X β β β X x β 0 = e x β (succ n) = x Β· (x β n) infixl 3 _β_ finite-order : (x : X) β Ξ£ k κ β , x β (succ k) β‘ e finite-order x = c a where a : Ξ£ m κ β , Ξ£ n κ β , (m β’ n) Γ (x β m β‘ x β n) a = β-finite-pigeonhole-principle (x β_) Ο b : (m : β) (n : β) β m β’ n β x β m β‘ x β n β Ξ£ k κ β , x β (succ k) β‘ e b 0 0 Ξ½ p = π-elim (Ξ½ refl) b 0 (succ n) Ξ½ p = n , (p β»ΒΉ) b (succ m) 0 Ξ½ p = m , p b (succ m) (succ n) Ξ½ p = b m n (Ξ» (q : m β‘ n) β Ξ½ (ap succ q)) (lc x p) c : type-of a β Ξ£ k κ β , x β (succ k) β‘ e c (m , n , Ξ½ , p) = b m n Ξ½ p \end{code} And of course then there is a minimal such k, by bounded minimization, because finite types are discrete: \begin{code} minimal-finite-order : (x : X) β Σμ Ξ»(k : β) β x β (succ k) β‘ e minimal-finite-order x = minimal-from-given A Ξ³ (finite-order x) where A : β β π€ Μ A n = x β (succ n) β‘ e Ξ³ : (n : β) β decidable (x β succ n β‘ e) Ξ³ n = finite-types-are-discrete fe Ο (x β succ n) e \end{code} Remark: the given construction finite-order already produces the minimal order, but it seems slightly more difficult to prove this than just compute the minimal order from any order. If we were interested in the efficiency of our constructions (functional programs!), we would have to consider this. Added 15th December 2019. If the type X i is compact for every i : Fin n, then the product type (i : Fin n) β X i is also compact. For that purpose we first consider generalized vector types. \begin{code} vec : (n : β) β (Fin n β π€ Μ ) β π€ Μ vec 0 X = π vec (succ n) X = X π Γ vec n (X β suc) Vec : π€ Μ β β β π€ Μ Vec X n = vec n (Ξ» _ β X) List : π€ Μ β π€ Μ List X = Ξ£ n κ β , Vec X n length : {X : π€ Μ } β List X β β length = prβ pattern [] = (0 , *) _β·_ : {X : π€ Μ } β X β List X β List X x β· (n , s) = succ n , x , s [_] : {X : π€ Μ } β X β List X [ x ] = x β· [] \end{code} Our list encoding satisfies Martin-LΓΆf's rules for lists: \begin{code} List-induction : {X : π€ Μ } (P : List X β π₯ Μ ) β P [] β ((x : X) (xs : List X) β P xs β P (x β· xs)) β (xs : List X) β P xs List-induction {π€} {π₯} {X} P p f = h where h : (xs : List X) β P xs h [] = p h (succ n , x , s) = f x (n , s) (h (n , s)) \end{code} With the computation rules holding definitionally, as required: \begin{code} List-induction-[] : {X : π€ Μ } (P : List X β π₯ Μ ) β (p : P []) β (f : (x : X) (xs : List X) β P xs β P (x β· xs)) β List-induction P p f [] β‘ p List-induction-[] {π€} {π₯} {X} P p f = refl List-induction-β· : {X : π€ Μ } (P : List X β π₯ Μ ) β (p : P []) β (f : (x : X) (xs : List X) β P xs β P (x β· xs)) β (x : X) β (xs : List X) β List-induction P p f (x β· xs) β‘ f x xs (List-induction P p f xs) List-induction-β· {π€} {π₯} {X} P p f x xs = refl \end{code} A version of the desired compactness construction: \begin{code} finite-product-compact : (n : β) (X : Fin n β π€ Μ ) β ((i : Fin n) β Compact (X i) {π€}) β Compact (vec n X) {π€} finite-product-compact zero X c = π-Compact finite-product-compact (succ n) X c = Γ-Compact (c π) (finite-product-compact n (X β suc) (c β suc)) \end{code} Standard operations on (generalized) vectors: \begin{code} pattern β¨β© = * pattern _::_ x xs = (x , xs) hd : {n : β} {X : Fin (succ n) β π€ Μ } β vec (succ n) X β X π hd (x :: xs) = x tl : {n : β} {X : Fin (succ n) β π€ Μ } β vec (succ n) X β vec n (X β suc) tl (x :: xs) = xs index : (n : β) {X : Fin n β π€ Μ } β vec n X β (i : Fin n) β X i index 0 xs i = π-elim i index (succ n) (x :: xs) π = x index (succ n) (x :: xs) (suc i) = index n xs i _!!_ : {n : β} {X : π€ Μ } β Vec X n β (i : Fin n) β X _!!_ {π€} {n} = index n \end{code} An isomorphic copy of vec n X. \begin{code} vec' : (n : β) β (Fin n β π€ Μ ) β π€ Μ vec' n X = (i : Fin n) β X i Vec' : π€ Μ β (n : β) β π€ Μ Vec' X n = vec' n (Ξ» _ β X) hd' : {n : β} {X : Fin (succ n) β π€ Μ } β vec' (succ n) X β X π hd' xs = xs π tl' : {n : β} {X : Fin (succ n) β π€ Μ } β vec' (succ n) X β vec' n (X β suc) tl' xs = Ξ» i β xs (suc i) β¨β©' : {X : Fin 0 β π€ Μ } β vec' 0 X β¨β©' = Ξ» i β unique-from-π i _::'_ : {n : β} {X : Fin (succ n) β π€ Μ } β X π β vec' n (X β suc) β vec' (succ n) X (x ::' xs) π = x (x ::' xs) (suc i) = xs i xedni : (n : β) {X : Fin n β π€ Μ } β ((i : Fin n) β X i) β vec n X xedni 0 xs' = β¨β© xedni (succ n) xs' = hd' xs' :: xedni n (tl' xs') vecΞ· : (n : β) {X : Fin n β π€ Μ } β xedni n {X} β index n {X} βΌ id vecΞ· zero β¨β© = refl vecΞ· (succ n) (x :: xs) = ap (x ::_) (vecΞ· n xs) module _ {π€} (fe : funext π€β π€) where vecΞ΅ : (n : β) {X : Fin n β π€ Μ } β index n {X} β xedni n {X} βΌ id vecΞ΅ 0 xs' = dfunext fe (Ξ» i β π-elim i) vecΞ΅ (succ n) xs' = dfunext fe h where h : (i : Fin (succ n)) β index (succ n) (xs' π :: xedni n (tl' xs')) i β‘ xs' i h π = refl h (suc i) = happly (vecΞ΅ n (tl' xs')) i vec-β : (n : β) {X : Fin n β π€ Μ } β vec n X β vec' n X vec-β n {X} = qinveq (index n) (xedni n {X} , vecΞ· n , vecΞ΅ n) \end{code} The desired compactness theorem: \begin{code} finitely-indexed-product-compact : (n : β) (X : Fin n β π€ Μ ) β ((i : Fin n) β Compact (X i)) β Compact ((i : Fin n) β X i) finitely-indexed-product-compact n X c = Compact-closed-under-β (vec-β n) (finite-product-compact n X c) \end{code} 9th Feb 2021. More operations on vectors. The stuff on vectors should be eventually moved to another module. \begin{code} β¨_β© : {X : π€ Μ } β X β Vec X 1 β¨ x β© = x :: β¨β© _β_ : β β β β β zero β n = n succ m β n = succ (m β n) append : {X : π€ Μ } (m n : β) β Vec X m β Vec X n β Vec X (m β n) append zero n β¨β© t = t append (succ m) n (x :: s) t = x :: append m n s t _++_ : {X : π€ Μ } {m n : β} β Vec X m β Vec X n β Vec X (m β n) _++_ = append _ _ plus-1-is-succ : (n : β) β n β 1 β‘ succ n plus-1-is-succ zero = refl plus-1-is-succ (succ n) = ap succ (plus-1-is-succ n) rev' : {X : π€ Μ } (n : β) β Vec X n β Vec X n rev' zero β¨β© = β¨β© rev' (succ n) (x :: s) = Ξ³ where IH : Vec _ (n β 1) IH = rev' n s ++ β¨ x β© Ξ³ : Vec _ (succ n) Ξ³ = transport (Vec _) (plus-1-is-succ n) IH rev : {X : π€ Μ } {n : β} β Vec X n β Vec X n rev = rev' _ _+β_ : β β β β β zero +β n = n succ m +β n = m +β succ n rev-append : {X : π€ Μ } (m n : β) β Vec X m β Vec X n β Vec X (m +β n) rev-append zero n β¨β© t = t rev-append (succ m) n (x :: s) t = rev-append m (succ n) s (x :: t) revβ : {X : π€ Μ } (m : β) β Vec X m β Vec X (m +β zero) revβ n s = rev-append n zero s β¨β© \end{code} Added 19th March 2021. \begin{code} having-three-distinct-points-covariant : {X : π€ Μ } {Y : π₯ Μ } β X βͺ Y β has-three-distinct-points X β has-three-distinct-points Y having-three-distinct-points-covariant (f , f-is-emb) ((x , y , z) , u , v , w) = Ξ³ where l : left-cancellable f l = embeddings-are-lc f f-is-emb Ξ³ : has-three-distinct-points (codomain f) Ξ³ = ((f x , f y , f z) , (Ξ» p β u (l p)) , (Ξ» q β v (l q)) , (Ξ» r β w (l r))) finite-type-with-three-distict-points : (k : β) β k β₯ 3 β has-three-distinct-points (Fin k) finite-type-with-three-distict-points (succ (succ (succ k))) * = ((π , π , π) , +disjoint' , (Ξ» a β +disjoint' (inl-lc a)) , +disjoint) finite-subsets-of-Ξ©-have-at-most-2-elements : funext π€ π€ β propext π€ β (k : β) β Fin k βͺ Ξ© π€ β k β€ 2 finite-subsets-of-Ξ©-have-at-most-2-elements {π€} fe pe k e = Ξ³ where Ξ± : k β₯ 3 β has-three-distinct-points (Ξ© π€) Ξ± g = having-three-distinct-points-covariant e (finite-type-with-three-distict-points k g) Ξ² : Β¬ (k β₯ 3) Ξ² = contrapositive Ξ± (no-three-distinct-propositions fe pe) Ξ³ : k β€ 2 Ξ³ = not-less-bigger-or-equal k 2 Ξ² \end{code} TODO. Think about Kuratowski finite subsets of Ξ©. That is, types A βͺ Ξ© π€ for which there is some surjection Fin k β A. Because any such type A doesn't have three distinct points, we are looking at characterizations of surjections of Fin k into types with no three distinct points. Addded 8th April 2021. \begin{code} module Kuratowski-finiteness (pt : propositional-truncations-exist) where open finiteness pt open import UF-ImageAndSurjection open ImageAndSurjection pt is-Kuratowski-finite : π€ Μ β π€ Μ is-Kuratowski-finite X = β n κ β , Fin n β X being-Kuratowski-finite-is-prop : {X : π€ Μ } β is-prop (is-Kuratowski-finite X) being-Kuratowski-finite-is-prop = β-is-prop finite-types-are-Kuratowski-finite : {X : π€ Μ } β is-finite X β is-Kuratowski-finite X finite-types-are-Kuratowski-finite {π€} {X} X-is-finite = Ξ³ where Ξ΄ : finite-linear-order X β is-Kuratowski-finite X Ξ΄ (n , π) = β£ n , (β π ββ»ΒΉ , equivs-are-surjections (βββ»ΒΉ-is-equiv π)) β£ Ξ³ : is-Kuratowski-finite X Ξ³ = β₯β₯-rec being-Kuratowski-finite-is-prop Ξ΄ (finite-prime X X-is-finite) \end{code} TODO. Conversely, if a Kuratowski finite is discrete (that is, it has decidable equality) then it is finite, because we can use the decidable equality to remove repetitions, as observed by Tom de Jong. We now give an example of a Kuratowski finite set that is not necessarily finite in the above sense (equivalent to some Fin n). \begin{code} module example {π€ : Universe} (X : π€ Μ ) (X-is-set : is-set X) (xβ xβ : X) (fe : Fun-Ext) where A : π€ Μ A = Ξ£ x κ X , (x β‘ xβ) β¨ (x β‘ xβ) A-is-set : is-set A A-is-set = subsets-of-sets-are-sets X (Ξ» x β (x β‘ xβ) β¨ (x β‘ xβ)) X-is-set β¨-is-prop ΞΉ : Fin 2 β A ΞΉ π = xβ , β£ inl refl β£ ΞΉ (suc x) = xβ , β£ inr refl β£ ΞΉ-surj : is-surjection ΞΉ ΞΉ-surj (x , s) = β₯β₯-functor Ξ³ s where Ξ³ : (x β‘ xβ) + (x β‘ xβ) β Ξ£ n κ Fin 2 , ΞΉ n β‘ (x , s) Ξ³ (inl p) = π , to-subtype-β‘ (Ξ» _ β β¨-is-prop) (p β»ΒΉ) Ξ³ (inr q) = π , to-subtype-β‘ (Ξ» _ β β¨-is-prop) (q β»ΒΉ) A-is-Kuratowski-finite : is-Kuratowski-finite A A-is-Kuratowski-finite = β£ 2 , ΞΉ , ΞΉ-surj β£ \end{code} But A is finite if and only if the equality xβ β‘ xβ is decidable, which is not the case in general. In fact, if we choose X as the type Ξ© of truth-values and xβ = β€ (true) and leave xβ : Ξ© arbitrary, then the decidability of xβ β‘ xβ amounts to excluded middle. \begin{code} finiteness-of-A : is-finite A β decidable (xβ β‘ xβ) finiteness-of-A = (j , k) where j : is-finite A β decidable (xβ β‘ xβ) j (0 , s) = β₯β₯-rec (decidability-of-prop-is-prop fe X-is-set) Ξ³ s where Ξ³ : A β π β decidable (xβ β‘ xβ) Ξ³ (g , i) = π-elim (g (xβ , β£ inl refl β£)) j (1 , s) = inl (β₯β₯-rec X-is-set Ξ³ s) where Ξ΄ : is-prop (Fin 1) Ξ΄ π π = refl Ξ³ : A β Fin 1 β xβ β‘ xβ Ξ³ (g , i) = ap prβ (equivs-are-lc g i (Ξ΄ (g (ΞΉ π)) (g (ΞΉ π)))) j (succ (succ n) , s) = β₯β₯-rec (decidability-of-prop-is-prop fe X-is-set) Ξ³ s where Ξ³ : A β Fin (succ (succ n)) β decidable (xβ β‘ xβ) Ξ³ (g , i) = Ξ² where h : xβ β‘ xβ β ΞΉ π β‘ ΞΉ π h = to-subtype-β‘ (Ξ» _ β β¨-is-prop) Ξ± : decidable (g (ΞΉ π) β‘ g (ΞΉ π)) β decidable (xβ β‘ xβ) Ξ± (inl p) = inl (ap prβ (equivs-are-lc g i p)) Ξ± (inr Ξ½) = inr (contrapositive (Ξ» p β ap g (h p)) Ξ½) Ξ² : decidable (xβ β‘ xβ) Ξ² = Ξ± (Fin-is-discrete (succ (succ n)) (g (ΞΉ π)) (g (ΞΉ π))) k : decidable (xβ β‘ xβ) β is-finite A k (inl p) = 1 , β£ singleton-β m l β£ where l : is-singleton (Fin 1) l = π , c where c : is-central (Fin 1) π c π = refl m : is-singleton A m = (ΞΉ π , c) where c : is-central A (ΞΉ π) c (x , s) = to-subtype-β‘ (Ξ» _ β β¨-is-prop) (β₯β₯-rec X-is-set Ξ³ s) where Ξ³ : (x β‘ xβ) + (x β‘ xβ) β xβ β‘ x Ξ³ (inl q) = q β»ΒΉ Ξ³ (inr q) = p β q β»ΒΉ k (inr Ξ½) = 2 , β£ β-sym (ΞΉ , ΞΉ-is-equiv) β£ where ΞΉ-lc : left-cancellable ΞΉ ΞΉ-lc {π} {π} p = refl ΞΉ-lc {π} {π} p = π-elim (Ξ½ (ap prβ p)) ΞΉ-lc {π} {π} p = π-elim (Ξ½ (ap prβ (p β»ΒΉ))) ΞΉ-lc {π} {π} p = refl ΞΉ-emb : is-embedding ΞΉ ΞΉ-emb = lc-maps-into-sets-are-embeddings ΞΉ ΞΉ-lc A-is-set ΞΉ-is-equiv : is-equiv ΞΉ ΞΉ-is-equiv = surjective-embeddings-are-equivs ΞΉ ΞΉ-emb ΞΉ-surj module example-excluded-middle {π€ : Universe} {p : Ξ© π€} (fe : Fun-Ext) (pe : Prop-Ext) where B : π€ βΊ Μ B = Ξ£ q κ Ξ© π€ , (q β‘ p) β¨ (q β‘ β€) open example (Ξ© π€) (Ξ©-is-set fe pe) p β€ fe B-is-Kuratowski-finite : is-Kuratowski-finite B B-is-Kuratowski-finite = A-is-Kuratowski-finite finiteness-of-B-equiv-to-EM : is-finite B β decidable (p β‘ β€) finiteness-of-B-equiv-to-EM = finiteness-of-A \end{code} Try to see if a more conceptual definition of A gives a shorter proof (only marginally, it turns out): \begin{code} module example-variation {π€ : Universe} (X : π€ Μ ) (X-is-set : is-set X) (x : Fin 2 β X) (fe : Fun-Ext) where A : π€ Μ A = image x A-is-set : is-set A A-is-set = subsets-of-sets-are-sets X (Ξ» y β y is-in-the-image-of x) X-is-set β-is-prop ΞΉ : Fin 2 β A ΞΉ = corestriction x ΞΉ-surj : is-surjection ΞΉ ΞΉ-surj = corestriction-is-surjection x A-is-Kuratowski-finite : is-Kuratowski-finite A A-is-Kuratowski-finite = β£ 2 , ΞΉ , ΞΉ-surj β£ finiteness-of-A : is-finite A β decidable (x π β‘ x π) finiteness-of-A = j , k where j : is-finite A β decidable (x π β‘ x π) j (0 , s) = β₯β₯-rec (decidability-of-prop-is-prop fe X-is-set) Ξ³ s where Ξ³ : A β π β decidable (x π β‘ x π) Ξ³ (g , i) = π-elim (g (x π , β£ π , refl β£)) j (1 , s) = inl (β₯β₯-rec X-is-set Ξ³ s) where Ξ΄ : is-prop (Fin 1) Ξ΄ π π = refl Ξ³ : A β Fin 1 β x π β‘ x π Ξ³ (g , i) = ap prβ (equivs-are-lc g i (Ξ΄ (g (ΞΉ π)) (g (ΞΉ π)))) j (succ (succ n) , s) = β₯β₯-rec (decidability-of-prop-is-prop fe X-is-set) Ξ³ s where Ξ³ : A β Fin (succ (succ n)) β decidable (x π β‘ x π) Ξ³ (g , i) = Ξ² where h : x π β‘ x π β ΞΉ π β‘ ΞΉ π h = to-subtype-β‘ (Ξ» y β being-in-the-image-is-prop y x) Ξ± : decidable (g (ΞΉ π) β‘ g (ΞΉ π)) β decidable (x π β‘ x π) Ξ± (inl p) = inl (ap prβ (equivs-are-lc g i p)) Ξ± (inr Ξ½) = inr (contrapositive (Ξ» p β ap g (h p)) Ξ½) Ξ² : decidable (x π β‘ x π) Ξ² = Ξ± (Fin-is-discrete (succ (succ n)) (g (ΞΉ π)) (g (ΞΉ π))) k : decidable (x π β‘ x π) β is-finite A k (inl p) = 1 , β£ singleton-β m l β£ where l : is-singleton (Fin 1) l = π , c where c : is-central (Fin 1) π c π = refl m : is-singleton A m = (ΞΉ π , c) where c : is-central A (ΞΉ π) c (y , s) = to-subtype-β‘ (Ξ» y β being-in-the-image-is-prop y x) (β₯β₯-rec X-is-set Ξ³ s) where Ξ³ : fiber x y β x π β‘ y Ξ³ (π , q) = q Ξ³ (π , q) = p β q k (inr Ξ½) = 2 , β£ β-sym (ΞΉ , ΞΉ-is-equiv) β£ where ΞΉ-lc : left-cancellable ΞΉ ΞΉ-lc {π} {π} p = refl ΞΉ-lc {π} {π} p = π-elim (Ξ½ (ap prβ p)) ΞΉ-lc {π} {π} p = π-elim (Ξ½ (ap prβ (p β»ΒΉ))) ΞΉ-lc {π} {π} p = refl ΞΉ-emb : is-embedding ΞΉ ΞΉ-emb = lc-maps-into-sets-are-embeddings ΞΉ ΞΉ-lc A-is-set ΞΉ-is-equiv : is-equiv ΞΉ ΞΉ-is-equiv = surjective-embeddings-are-equivs ΞΉ ΞΉ-emb ΞΉ-surj \end{code} Added 13 April 2021. Can every Kuratowski finite discrete type be equipped with a linear order? Recall that a type is called discrete if it has decidable equality. Steve Vickers asks this question for the internal language of a 1-topos, and provides a counter model for it in Section 2.4 of the following paper: S.J. Vickers. Strongly Algebraic = SFP (Topically). Mathematical Structures in Computer Science 11 (2001) pp. 717-742, http://dx.doi.org/10.1017/S0960129501003437 https://www.cs.bham.ac.uk/~sjv/SFP.pdf We here work in MLTT with propositional truncations, in Agda notation, and instead prove that, in the presence of univalence, it is false that every (Kuratowski) finite type with decidable equality can be equipped with a linear order. We prove more than what is needed in order to conclude that. There is a lemma contributed by Tom de Jong, with attribution given below. We also include an open problem related to this. \begin{code} open import Two-Properties select-equiv-with-π-lemma : FunExt β {X : π€ Μ } β X β π β (xβ : X) β β! xβ κ X , is-equiv (π-cases xβ xβ) select-equiv-with-π-lemma fe {X} π xβ = VI where nβ : π nβ = β π β xβ xβ : X xβ = β π ββ»ΒΉ (complement nβ) f : π β X f = π-cases xβ xβ I : xβ β’ xβ I p = complement-no-fp nβ q where q = nβ β‘β¨ ap β π β p β© β π β xβ β‘β¨ β-sym-is-rinv π (complement nβ) β© complement nβ β II : (x : X) β x β’ xβ β x β‘ xβ II x Ξ½ = equivs-are-lc β π β (ββ-is-equiv π) q where u : β π β x β’ β π β xβ u p = Ξ½ (equivs-are-lc β π β (ββ-is-equiv π) p) v : β π β xβ β’ β π β xβ v p = I (equivs-are-lc β π β (ββ-is-equiv π) (p β»ΒΉ)) q : β π β x β‘ β π β xβ q = π-things-distinct-from-a-third-are-equal (β π β x) (β π β xβ) (β π β xβ) u v Ξ΄ : is-discrete X Ξ΄ = equiv-to-discrete (β-sym π) π-is-discrete Ξ³ : (x : X) β decidable (x β‘ xβ) β π Ξ³ x (inl p) = β Ξ³ x (inr Ξ½) = β g : X β π g x = Ξ³ x (Ξ΄ x xβ) III : (n : π) (d : decidable (f n β‘ xβ)) β Ξ³ (f n) d β‘ n III β (inl p) = refl III β (inr Ξ½) = π-elim (Ξ½ refl) III β (inl p) = π-elim (I (p β»ΒΉ)) III β (inr Ξ½) = refl Ξ· : g β f βΌ id Ξ· n = III n (Ξ΄ (f n) xβ) IV : (x : X) (d : decidable (x β‘ xβ)) β f (Ξ³ x d) β‘ x IV x (inl p) = p β»ΒΉ IV x (inr Ξ½) = (II x Ξ½)β»ΒΉ Ξ΅ : f β g βΌ id Ξ΅ x = IV x (Ξ΄ x xβ) f-is-equiv : is-equiv f f-is-equiv = qinvs-are-equivs f (g , Ξ· , Ξ΅) c : Ξ£ xβ κ X , is-equiv (π-cases xβ xβ) c = xβ , f-is-equiv V : is-central _ c V (x , t) = q where Ξ½ : xβ β’ x Ξ½ r = zero-is-not-one s where s : β β‘ β s = equivs-are-lc (π-cases xβ x) t r p : xβ β‘ x p = (II x (β’-sym Ξ½))β»ΒΉ q : c β‘ (x , t) q = to-subtype-β‘ (Ξ» x β being-equiv-is-prop fe (π-cases xβ x)) p VI : β! xβ κ X , is-equiv (π-cases xβ xβ) VI = c , V select-equiv-with-π : FunExt β {X : π€ Μ } β β₯ X β π β₯ β X β X β π select-equiv-with-π fe {X} s xβ = Ξ³ where Ξ± : β₯ X β π β₯ β β! xβ κ X , is-equiv (π-cases xβ xβ) Ξ± = β₯β₯-rec (β!-is-prop (fe _ _)) (Ξ» π β select-equiv-with-π-lemma fe π xβ) Ξ² : Ξ£ xβ κ X , is-equiv (π-cases xβ xβ) Ξ² = description (Ξ± s) Ξ³ : X β π Ξ³ = β-sym (π-cases xβ (prβ Ξ²) , prβ Ξ²) \end{code} Hence finding an equivalence from the existence of an equivalence is logically equivalent to finding a point from the existence of an equivalence (exercise: moreover, these two things are typally equivalent): \begin{code} select-equiv-with-π-theorem : FunExt β {X : π€ Μ } β (β₯ X β π β₯ β X β π) β (β₯ X β π β₯ β X) select-equiv-with-π-theorem fe {X} = Ξ± , Ξ² where Ξ± : (β₯ X β π β₯ β X β π) β β₯ X β π β₯ β X Ξ± f s = β β-sym (f s) β β Ξ² : (β₯ X β π β₯ β X) β β₯ X β π β₯ β X β π Ξ² g s = select-equiv-with-π fe s (g s) \end{code} The following no-selection lemma is contributed by Tom de Jong: \begin{code} no-selection : is-univalent π€β β Β¬ ((X : π€β Μ ) β β₯ X β π β₯ β X) no-selection ua Ο = Ξ³ where f : {X : π€β Μ } β X β‘ π β X β π f {X} = idtoeq X π n : π n = Ο π β£ β-refl π β£ Ξ± : {X : π€β Μ } (p : X β‘ π) β Ο X β£ f p β£ β‘ β f p ββ»ΒΉ n Ξ± refl = refl p : π β‘ π p = eqtoid ua π π complement-β q : β£ f refl β£ β‘ β£ f p β£ q = β₯β₯-is-prop β£ f refl β£ β£ f p β£ r : f p β‘ complement-β r = idtoeq-eqtoid ua π π complement-β s = n β‘β¨ refl β© β f refl ββ»ΒΉ n β‘β¨ (Ξ± refl)β»ΒΉ β© Ο π β£ f refl β£ β‘β¨ ap (Ο π) q β© Ο π β£ f p β£ β‘β¨ Ξ± p β© β f p ββ»ΒΉ n β‘β¨ ap (Ξ» - β β - ββ»ΒΉ n) r β© β complement-β ββ»ΒΉ n β‘β¨ refl β© complement n β Ξ³ : π Ξ³ = complement-no-fp n s π-is-Fin2 : π β Fin 2 π-is-Fin2 = qinveq (π-cases π π) (g , Ξ· , Ξ΅) where g : Fin 2 β π g π = β g π = β Ξ· : g β π-cases π π βΌ id Ξ· β = refl Ξ· β = refl Ξ΅ : π-cases π π β g βΌ id Ξ΅ π = refl Ξ΅ π = refl open import UF-UA-FunExt no-orderability-of-finite-types : Univalence β Β¬ ((X : π€ Μ ) β is-finite X β finite-linear-order X) no-orderability-of-finite-types {π€} ua Ο = Ξ³ where fe : FunExt fe = Univalence-gives-FunExt ua Ξ± : (X : π€β Μ ) β β₯ X β π β₯ β X β π Ξ± X s = VII where X' : π€ Μ X' = Lift π€ X I : X β π β X' β Fin 2 I π = X' ββ¨ Lift-β π€ X β© X ββ¨ π β© π ββ¨ π-is-Fin2 β© Fin 2 β II : β₯ X' β Fin 2 β₯ II = β₯β₯-functor I s III : is-finite X' III = 2 , II IV : finite-linear-order X' IV = Ο X' III n : β n = prβ IV π : X' β Fin n π = prβ IV V : β₯ X' β Fin n β₯ β β₯ X' β Fin 2 β₯ β n β‘ 2 V = β₯β₯-recβ β-is-set (Ξ» π π β Fin-lc n 2 (β-sym π β π)) VI : n β‘ 2 VI = V β£ π β£ II VII = X ββ¨ β-Lift π€ X β© X' ββ¨ π β© Fin n ββ¨ idtoeq (Fin n) (Fin 2) (ap Fin VI) β© Fin 2 ββ¨ β-sym π-is-Fin2 β© π β Ο : (X : π€β Μ ) β β₯ X β π β₯ β X Ο X = lr-implication (select-equiv-with-π-theorem fe) (Ξ± X) Ξ³ : π Ξ³ = no-selection (ua π€β) Ο \end{code} Because univalence is consistent, it follows that, without univalence, the statement (X : π€ Μ ) β is-finite X β finite-linear-order X is not provable. The same holds if we replace is-finite by is-Kuratowski-finite or if we consider discrete Kuratowski finite types. \begin{code} no-orderability-of-K-finite-types : Univalence β Β¬ ((X : π€ Μ ) β is-Kuratowski-finite X β finite-linear-order X) no-orderability-of-K-finite-types {π€} ua Ο = no-orderability-of-finite-types ua Ο where Ο : (X : π€ Μ ) β is-finite X β finite-linear-order X Ο X i = Ο X (finite-types-are-Kuratowski-finite i) \end{code} And this gives an alternative answer the question by Steve Vickers mentioned above: \begin{code} no-orderability-of-discrete-K-finite-types : Univalence β Β¬ ((X : π€ Μ ) β is-Kuratowski-finite X β is-discrete X β finite-linear-order X) no-orderability-of-discrete-K-finite-types {π€} ua Ο = no-orderability-of-finite-types ua Ο where Ο : (X : π€ Μ ) β is-finite X β finite-linear-order X Ο X i = Ο X (finite-types-are-Kuratowski-finite i) (finite-types-are-discrete (Univalence-gives-FunExt ua) i) \end{code} TODO. Without univalence, maybe it is the case that from (X : π€ Μ ) β β₯ X β π β₯ β X we can deduce excluded middle or some other constructive taboo. One more notion of finiteness: \begin{code} is-subfinite : π€ Μ β π€ Μ is-subfinite X = β n κ β , X βͺ Fin n \end{code} TODO. Steve Vickers remarked (personal communication) that, in view of a remark given above, if a type is simultaneously Kuratowski finite and subfinite, then it is finite, because subfinite types, being subtypes of types with decidable equality, have decidable equality. Summary of finiteness notions for a type X: β n κ β , X β Fin n (is-finite X) Ξ£ n κ β , X β Fin n (finite-linear-order X) β n κ β , Fin n β X (is-Kuratowski-finite X) Ξ£ n κ β , Fin n β X (nameless, not considered yet) β n κ β , X βͺ Fin n (is-subfinite) Ξ£ n κ β , X βͺ Fin n (nameless, not considered yet)