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 #-}

module Fin where

open import SpartanMLTT
open import UF-Subsingletons renaming (⊀Ω to ⊀)
open import Plus-Properties

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

suc-lc : {n : β„•} {j k : Fin n} β†’ fsucc j ≑ fsucc k β†’ j ≑ k
suc-lc = inl-lc

\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.

The largest element of Fin (succ n) is βŸͺ n ⟫ (TODO: formulate and prove this).

\begin{code}

βŸͺ_⟫ : (n : β„•) β†’ Fin (succ n)
βŸͺ 0 ⟫      = fzero
βŸͺ succ n ⟫ = fsucc βŸͺ n ⟫

Fin0-is-empty : is-empty (Fin 0)
Fin0-is-empty i = i

Fin1-is-singleton : is-singleton (Fin 1)
Fin1-is-singleton = 𝟎 , γ
 where
  Ξ³ : (i : Fin 1) β†’ 𝟎 ≑ i
  γ 𝟎 = refl

Fin0-is-prop : is-prop (Fin 0)
Fin0-is-prop i = 𝟘-elim i

Fin1-is-prop : is-prop (Fin 1)
Fin1-is-prop 𝟎 𝟎 = refl

open import Unit-Properties

positive-not-𝟎 : {n : β„•} {x : Fin n} β†’ fsucc x β‰’ 𝟎
positive-not-𝟎 {0}      {x} p = 𝟘-elim x
positive-not-𝟎 {succ n} {x} p = πŸ™-is-not-𝟘 (g p)
 where
  f : Fin (succ (succ n)) β†’ 𝓀₀ Μ‡
  f 𝟎       = 𝟘
  f (suc x) = πŸ™

  g : suc x ≑ 𝟎 β†’ πŸ™ ≑ 𝟘
  g = ap f

when-Fin-is-prop : (n : β„•) β†’ is-prop (Fin n) β†’ (n ≑ 0) + (n ≑ 1)
when-Fin-is-prop 0               i = inl refl
when-Fin-is-prop 1               i = inr refl
when-Fin-is-prop (succ (succ n)) i = 𝟘-elim (positive-not-𝟎 (i 𝟏 𝟎))

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

⟦_⟧ : {n : β„•} β†’ Fin n β†’ β„•
⟦_⟧ {n} = pr₁ ∘ Fin-prime n

⟦⟧-property : {n : β„•} (k : Fin n) β†’ ⟦ k ⟧ < n
⟦⟧-property {n} k = prβ‚‚ (Fin-prime n k)

open import UF-Embeddings

⟦_⟧-is-embedding : (n : β„•) β†’ is-embedding (⟦_⟧ {n})
⟦_⟧-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))

⟦βŸͺ⟫⟧-property : {n : β„•} β†’ ⟦ βŸͺ n ⟫ ⟧ ≑ n
⟦βŸͺ⟫⟧-property {0}      = refl
⟦βŸͺ⟫⟧-property {succ n} = ap succ (⟦βŸͺ⟫⟧-property {n})


⟦_⟧-lc : (n : β„•) β†’ left-cancellable (⟦_⟧ {n})
⟦_⟧-lc n = embeddings-are-lc ⟦_⟧ (⟦_⟧-is-embedding n)

coerce : {n : β„•} {i : Fin n} β†’ Fin ⟦ i ⟧ β†’ Fin n
coerce {succ n} {suc i} 𝟎       = 𝟎
coerce {succ n} {suc i} (suc j) = suc (coerce j)

coerce-lc : {n : β„•} {i : Fin n} (j k : Fin ⟦ i ⟧)
          β†’ coerce {n} {i} j ≑ coerce {n} {i} k β†’ j ≑ k
coerce-lc {succ n} {suc i} 𝟎       𝟎       p = refl
coerce-lc {succ n} {suc i} 𝟎       (suc j) p = 𝟘-elim (+disjoint' p)
coerce-lc {succ n} {suc i} (suc j) 𝟎       p = 𝟘-elim (+disjoint p)
coerce-lc {succ n} {suc i} (suc j) (suc k) p = ap suc (coerce-lc {n} j k (suc-lc p))

incl : {n : β„•} {k : β„•} β†’ k ≀ n β†’ Fin k β†’ Fin n
incl {succ n} {succ k} l 𝟎 = 𝟎
incl {succ n} {succ k} l (suc i) = suc (incl l i)

incl-lc : {n : β„•} {k : β„•} (l : k ≀ n)
        β†’ (i j : Fin k) β†’ incl l i ≑ incl l j β†’ i ≑ j
incl-lc {succ n} {succ k} l 𝟎       𝟎       p = refl
incl-lc {succ n} {succ k} l 𝟎       (suc j) p = 𝟘-elim (positive-not-𝟎 (p ⁻¹))
incl-lc {succ n} {succ k} l (suc i) 𝟎       p = 𝟘-elim (positive-not-𝟎 p)
incl-lc {succ n} {succ k} l (suc i) (suc j) p = ap suc (incl-lc l i j (suc-lc p))

_/_ : {n : β„•} (k : Fin (succ n)) β†’ Fin ⟦ k ⟧ β†’ Fin n
k / i = incl (⟦⟧-property k) i

_β•±_ :  (n : β„•) β†’ Fin n β†’ Fin (succ n)
n β•± k = incl (≀-succ n) k

\end{code}

TODO. Show that the above coersions are left cancellable (easy).

TODO. Find better names for the coersions (hard).

\begin{code}

_β‰Ί_ _β‰Ό_ : {n : β„•} β†’ Fin n β†’ Fin n β†’ 𝓀₀ Μ‡
i β‰Ί j = ⟦ i ⟧ < ⟦ j ⟧
i β‰Ό j = ⟦ i ⟧ ≀ ⟦ 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 (⟦_⟧ 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 (⟦_⟧ 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 = ⟦_⟧-lc n (≀-anti (⟦_⟧ i) (⟦_⟧ 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 (⟦_⟧ j) (⟦_⟧ k))))

  Ξ³ : i , a , l ≑ i' , a' , l'
  Ξ³ = to-Ξ£-≑ (p , H _ _ _)

{-
module _ {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
         (X-is-compact : Compact X)
         {n : β„•}
       where

 Inf : (X β†’ Fin n) β†’ Fin n
 Inf p = {!!}
  where
   A : X β†’ ? Μ‡
   A x = (x : X) β†’ p x ≀
-}

\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
be 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 (solved
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

 _has-cardinality_ : 𝓀 Μ‡ β†’ β„• β†’ 𝓀 Μ‡
 X has-cardinality n = βˆ₯ X ≃ Fin n βˆ₯

 is-finite : 𝓀 Μ‡ β†’ 𝓀 Μ‡
 is-finite X = Ξ£ n κž‰ β„• , X has-cardinality n

 cardinality : (X : 𝓀 Μ‡ ) β†’ is-finite X β†’ β„•
 cardinality X = pr₁

 cardinality-≃ : (X : 𝓀 Μ‡ ) (Ο† : is-finite X) β†’ X has-cardinality (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
   Ξ± : (m n : β„•) β†’ X ≃ Fin m β†’ X ≃ Fin n β†’ m ≑ n
   Ξ± m n d e = Fin-lc m n (≃-sym d ● e)

   Ξ² : (m n : β„•) β†’ βˆ₯ X ≃ Fin m βˆ₯ β†’ βˆ₯ X ≃ Fin n βˆ₯ β†’ m ≑ n
   Ξ² m n = βˆ₯βˆ₯-recβ‚‚ β„•-is-set (Ξ± m n)

   Ξ³ : m , d ≑ n , e
   Ξ³ = to-Ξ£-≑ (Ξ² 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'-gives-finite : (X : 𝓀 Μ‡ ) β†’ is-finite' X β†’ is-finite X
 finite'-gives-finite X = βˆ₯βˆ₯-rec (being-finite-is-prop X) Ξ³
  where
   Ξ³ : (Ξ£ n κž‰ β„• , X ≃ Fin n) β†’ Ξ£ n κž‰ β„• , βˆ₯ X ≃ Fin n βˆ₯
   γ (n , e) = n , ∣ e ∣

 finite-gives-finite' : (X : 𝓀 Μ‡ ) β†’ is-finite X β†’ is-finite' X
 finite-gives-finite' 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-types-are-βˆƒ-Compact : Fun-Ext β†’ {X : 𝓀 Μ‡ } β†’ is-finite X β†’ βˆƒ-Compact X {π“₯}
 finite-types-are-βˆƒ-Compact fe Ο† = βˆ₯Compactβˆ₯-gives-βˆƒ-Compact fe (finite-βˆ₯Compactβˆ₯ Ο†)

 finite-propositions-are-decidable' : Fun-Ext
                                    β†’ {P : 𝓀 Μ‡ }
                                    β†’ is-prop P
                                    β†’ is-finite P
                                    β†’ decidable P
 finite-propositions-are-decidable' fe i j =
  βˆƒ-Compact-propositions-are-decidable i (finite-types-are-βˆƒ-Compact fe j)

\end{code}

But function extensionality is not needed:

\begin{code}

 finite-propositions-are-decidable : {P : 𝓀 Μ‡ }
                                   β†’ is-prop P
                                   β†’ is-finite P
                                   β†’ decidable P
 finite-propositions-are-decidable {𝓀} {P} i (0 , s) = inr Ξ³
  where
   Ξ³ : P β†’ 𝟘
   Ξ³ p = βˆ₯βˆ₯-rec 𝟘-is-prop (Ξ» (f , _) β†’ f p) s

 finite-propositions-are-decidable {𝓀} {P} i (succ n , s) = inl Ξ³
  where
   Ξ³ : P
   Ξ³ = βˆ₯βˆ₯-rec i (Ξ» 𝕗 β†’ ⌜ 𝕗 ⌝⁻¹ 𝟎) s

 open import UF-ExcludedMiddle

 summands-of-finite-sum-always-finite-gives-EM :

   ((𝓀 π“₯ : Universe) (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ )
          β†’ is-finite (Ξ£ A)
          β†’ (x : X) β†’ is-finite (A x))

  β†’ (𝓦 : Universe) β†’ funext 𝓦 𝓦 β†’ propext 𝓦 β†’ EM 𝓦
 summands-of-finite-sum-always-finite-gives-EM Ο• 𝓦 fe pe P i = Ξ³
  where
   X : 𝓦 ⁺ Μ‡
   X = Ξ© 𝓦

   A : X β†’ 𝓦 Μ‡
   A p = p holds

   e : Ξ£ A ≃ (Ξ£ P κž‰ 𝓦 Μ‡ , is-prop P Γ— P)
   e = Ξ£-assoc

   s : is-singleton (Ξ£ A)
   s = equiv-to-singleton e (the-true-props-form-a-singleton-type fe pe)

   f : Ξ£ A ≃ Fin 1
   f = singleton-≃ s Fin1-is-singleton

   j : is-finite (Ξ£ A)
   j = 1 , ∣ f ∣

   k : is-finite P
   k = Ο• (𝓦 ⁺) 𝓦 X A j (P , i)

   Ξ³ : P + Β¬ P
   Ξ³ = finite-propositions-are-decidable i k

\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 = Ξ³
  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')

   Ξ³ : Ξ£ A
   Ξ³ = g Οƒ'

\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 (⟦_⟧ 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) = ⟦_⟧ i , ⟦_⟧ j , contrapositive (⟦_⟧-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 (Agda constructions are
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' : β„• β†’ 𝓀 Μ‡ β†’ 𝓀 Μ‡
Vec' n X = 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.

Added 8th April 2021.

\begin{code}

module Kuratowski-finiteness (pt : propositional-truncations-exist) where

 open finiteness pt
 open import UF-ImageAndSurjection
 open ImageAndSurjection pt
 open CompactTypesPT pt

 is-Kuratowski-finite : 𝓀 Μ‡ β†’ 𝓀 Μ‡
 is-Kuratowski-finite X = βˆƒ n κž‰ β„• , Fin n β†  X

 Kuratowski-data : 𝓀 Μ‡ β†’ 𝓀 Μ‡
 Kuratowski-data X = Ξ£ n κž‰ β„• , Fin n β†  X

 being-Kuratowski-finite-is-prop : {X : 𝓀 Μ‡ } β†’ is-prop (is-Kuratowski-finite X)
 being-Kuratowski-finite-is-prop = βˆƒ-is-prop

 Kuratowski-finite-types-are-βˆƒ-compact : Fun-Ext
                                       β†’ {X : 𝓀 Μ‡ }
                                       β†’ is-Kuratowski-finite X
                                       β†’ βˆƒ-Compact X {𝓀}
 Kuratowski-finite-types-are-βˆƒ-compact fe {X} i = Ξ³
  where
   Ξ± : Kuratowski-data X β†’ Compact X
   Ξ± (n , f , s) = surjection-Compact f fe s (Fin-Compact n)

   Ξ² : βˆ₯ Compact X βˆ₯
   Ξ² = βˆ₯βˆ₯-functor Ξ± i

   Ξ³ : βˆƒ-Compact X
   Ξ³ = βˆ₯Compactβˆ₯-gives-βˆƒ-Compact fe Ξ²

 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-gives-finite' X X-is-finite)

\end{code}

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
(and implemented by Martin Escardo):

\begin{code}

 dkf-lemma : funext 𝓀 𝓀₀
           β†’ {X : 𝓀 Μ‡ }
           β†’ is-discrete X
           β†’ Kuratowski-data X
           β†’ finite-linear-order X
 dkf-lemma {𝓀} fe {X} Ξ΄ (n , 𝕗) = Ξ³ X Ξ΄ n 𝕗
  where
   Ξ³ : (X : 𝓀 Μ‡ ) β†’ is-discrete X β†’ (n : β„•) β†’ (Fin n β†  X) β†’ finite-linear-order X
   Ξ³ X Ξ΄ 0        (f , s) = 0 , empty-≃-𝟘 (Ξ» x β†’ βˆ₯βˆ₯-rec 𝟘-is-prop pr₁ (s x))
   Ξ³ X Ξ΄ (succ n) (f , s) = I Ξ”
    where
     A : Fin n β†’ 𝓀 Μ‡
     A j = f (suc j) ≑ f 𝟎

     Ξ” : decidable (Ξ£ A)
     Ξ” = Fin-Compact n A (Ξ» j β†’ Ξ΄ (f (suc j)) (f 𝟎))

     g : Fin n β†’ X
     g i = f (suc i)

     I : decidable (Ξ£ A) β†’ finite-linear-order X
     I (inl (j , p)) = IH
      where
       II : (x : X) β†’ (Ξ£ i κž‰ Fin (succ n) , f i ≑ x) β†’ (Ξ£ i κž‰ Fin n , g i ≑ x)
       II x (𝟎 ,     q) = j , (p βˆ™ q)
       II x (suc i , q) = i , q

       III : is-surjection g
       III x = βˆ₯βˆ₯-functor (II x) (s x)

       IH : finite-linear-order X
       IH = Ξ³ X Ξ΄ n (g , III)

     I (inr Ξ½) = succ n' , IX
      where
       X' = X βˆ– f 𝟎

       Ξ΄' : is-discrete X'
       Ξ΄' = lc-maps-reflect-discreteness pr₁ (pr₁-lc (negations-are-props fe)) Ξ΄

       g' : Fin n β†’ X'
       g' i = g i , (Ξ» (p : f (suc i) ≑ f 𝟎) β†’ Ξ½ (i , p))

       IV : is-surjection g'
       IV (x , u) = VII
        where
         V : βˆƒ i κž‰ Fin (succ n) , f i ≑ x
         V = s x

         VI : (Ξ£ i κž‰ Fin (succ n) , f i ≑ x) β†’ (Ξ£ i κž‰ Fin n , g' i ≑ (x , u))
         VI (𝟎     , p) = 𝟘-elim (u (p ⁻¹))
         VI (suc i , p) = i , to-subtype-≑ (Ξ» _ β†’ negations-are-props fe) p

         VII : βˆƒ i κž‰ Fin n , g' i ≑ (x , u)
         VII = βˆ₯βˆ₯-functor VI V

       IH : finite-linear-order X'
       IH = Ξ³ X' Ξ΄' n (g' , IV)

       n' : β„•
       n' = pr₁ IH

       VIII : X' ≃ Fin n'
       VIII = prβ‚‚ IH

       IX = X           β‰ƒβŸ¨ remove-and-add-isolated-point fe (f 𝟎) (Ξ΄ (f 𝟎)) ⟩
           (X' + πŸ™)     β‰ƒβŸ¨ +cong VIII (≃-refl πŸ™) ⟩
           (Fin n' + πŸ™) β– 

 Kuratowski-finite-discrete-types-are-finite : funext 𝓀 𝓀₀
                                             β†’ {X : 𝓀 Μ‡ }
                                             β†’ is-discrete X
                                             β†’ is-Kuratowski-finite X
                                             β†’ is-finite X
 Kuratowski-finite-discrete-types-are-finite {𝓀} fe {X} Ξ΄ ΞΊ =
  finite'-gives-finite X (βˆ₯βˆ₯-functor (dkf-lemma fe Ξ΄) ΞΊ)


 surjections-preserve-K-finiteness : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                   β†’ is-surjection f
                                   β†’ is-Kuratowski-finite X
                                   β†’ is-Kuratowski-finite Y
 surjections-preserve-K-finiteness {𝓀} {π“₯} {X} {Y} f s i = j
  where
   Ξ³ : Kuratowski-data X β†’ Kuratowski-data Y
   γ (n , g , t) = n , f ∘ g , ∘-is-surjection t s

   j : is-Kuratowski-finite Y
   j = βˆ₯βˆ₯-functor Ξ³ i


 total-K-finite-gives-index-type-K-finite' : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ )
                                           β†’ is-Kuratowski-finite (Ξ£ A)
                                           β†’ is-Kuratowski-finite (Ξ£ x κž‰ X , βˆ₯ A x βˆ₯)
 total-K-finite-gives-index-type-K-finite' X A i = Ξ³
  where
   ΞΆ : (x : X) β†’ A x β†’ βˆ₯ A x βˆ₯
   ΢ x a = ∣ a ∣

   ΞΆ-is-surjection : (x : X) β†’ is-surjection (ΞΆ x)
   ΞΆ-is-surjection x = pt-is-surjection

   f : Ξ£ A β†’ Ξ£ x κž‰ X , βˆ₯ A x βˆ₯
   f = NatΞ£ ΞΆ

   f-is-surjection : is-surjection f
   f-is-surjection = NatΞ£-is-surjection A (Ξ» x β†’ βˆ₯ A x βˆ₯) ΞΆ ΞΆ-is-surjection

   Ξ³ : is-Kuratowski-finite (Ξ£ x κž‰ X , βˆ₯ A x βˆ₯)
   Ξ³ = surjections-preserve-K-finiteness f f-is-surjection i

 total-K-finite-gives-index-type-K-finite : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                                          β†’ is-Kuratowski-finite (Ξ£ A)
                                          β†’ ((x : X) β†’ βˆ₯ A x βˆ₯)
                                          β†’ is-Kuratowski-finite X
 total-K-finite-gives-index-type-K-finite A i s =
  surjections-preserve-K-finiteness pr₁ (pr₁-is-surjection A s) i

\end{code}

The finiteness of all Kuratowski finite types gives the discreteness of
all sets (and hence excluded middle, because the type of truth values
is a set).

\begin{code}

 doubleton : {X : 𝓀 Μ‡ } β†’ X β†’ X β†’ 𝓀 Μ‡
 doubleton {𝓀} {X} xβ‚€ x₁ = Ξ£ x κž‰ X , (x ≑ xβ‚€) ∨ (x ≑ x₁)

 doubleton-is-set : {X : 𝓀 Μ‡ } (xβ‚€ x₁ : X)
                  β†’ is-set X
                  β†’ is-set (doubleton xβ‚€ x₁)
 doubleton-is-set {𝓀} {X} xβ‚€ x₁ i = subsets-of-sets-are-sets
                                      X (Ξ» x β†’ (x ≑ xβ‚€) ∨ (x ≑ x₁)) i ∨-is-prop

 doubleton-map : {X : 𝓀 Μ‡ } (xβ‚€ x₁ : X) β†’ Fin 2 β†’ doubleton xβ‚€ x₁
 doubleton-map xβ‚€ x₁ 𝟎 = xβ‚€ , ∣ inl refl ∣
 doubleton-map xβ‚€ x₁ 𝟏 = x₁ , ∣ inr refl ∣

 doubleton-map-is-surjection : {X : 𝓀 Μ‡ } {xβ‚€ x₁ : X}
                             β†’ is-surjection (doubleton-map xβ‚€ x₁)
 doubleton-map-is-surjection {𝓀} {X} {xβ‚€} {x₁} (x , s) = βˆ₯βˆ₯-functor Ξ³ s
  where
   Ξ³ : (x ≑ xβ‚€) + (x ≑ x₁) β†’ Ξ£ n κž‰ Fin 2 , doubleton-map xβ‚€ x₁ n ≑ (x , s)
   Ξ³ (inl p) = 𝟎 , to-subtype-≑ (Ξ» _ β†’ ∨-is-prop) (p ⁻¹)
   Ξ³ (inr q) = 𝟏 , to-subtype-≑ (Ξ» _ β†’ ∨-is-prop) (q ⁻¹)

 doubletons-are-Kuratowki-finite : {X : 𝓀 Μ‡ } (xβ‚€ x₁ : X)
                                 β†’ is-Kuratowski-finite (doubleton xβ‚€ x₁)
 doubletons-are-Kuratowki-finite xβ‚€ x₁ = ∣ 2 , doubleton-map xβ‚€ x₁ , doubleton-map-is-surjection ∣


 decidable-equality-gives-doubleton-finite : {X : 𝓀 Μ‡ } (xβ‚€ x₁ : X)
                                           β†’ is-set X
                                           β†’ decidable (xβ‚€ ≑ x₁)
                                           β†’ is-finite (Ξ£ x κž‰ X , (x ≑ xβ‚€) ∨ (x ≑ x₁))
 decidable-equality-gives-doubleton-finite xβ‚€ x₁ X-is-set Ξ΄ = Ξ³ Ξ΄
  where
   Ξ³ : decidable (xβ‚€ ≑ x₁) β†’ is-finite (doubleton xβ‚€ x₁)
   Ξ³ (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 (doubleton xβ‚€ x₁)
     m = (doubleton-map xβ‚€ x₁ 𝟎 , c)
      where
       c : is-central (doubleton xβ‚€ x₁) (doubleton-map xβ‚€ x₁ 𝟎)
       c (y , s) = to-subtype-≑ (Ξ» _ β†’ ∨-is-prop) (βˆ₯βˆ₯-rec X-is-set Ξ± s)
        where
         Ξ± : (y ≑ xβ‚€) + (y ≑ x₁) β†’ xβ‚€ ≑ y
         α (inl q) = q ⁻¹
         Ξ± (inr q) = p βˆ™ q ⁻¹

   Ξ³ (inr Ξ½) = 2 , ∣ ≃-sym (doubleton-map xβ‚€ x₁ , f-is-equiv) ∣
    where
     doubleton-map-lc : left-cancellable (doubleton-map xβ‚€ x₁)
     doubleton-map-lc {𝟎} {𝟎} p = refl
     doubleton-map-lc {𝟎} {𝟏} p = 𝟘-elim (Ξ½ (ap pr₁ p))
     doubleton-map-lc {𝟏} {𝟎} p = 𝟘-elim (Ξ½ (ap pr₁ (p ⁻¹)))
     doubleton-map-lc {𝟏} {𝟏} p = refl

     doubleton-map-is-embedding : is-embedding (doubleton-map xβ‚€ x₁)
     doubleton-map-is-embedding = lc-maps-into-sets-are-embeddings
                                   (doubleton-map xβ‚€ x₁)
                                   doubleton-map-lc
                                   (doubleton-is-set xβ‚€ x₁ X-is-set)

     f-is-equiv : is-equiv (doubleton-map xβ‚€ x₁)
     f-is-equiv = surjective-embeddings-are-equivs
                   (doubleton-map xβ‚€ x₁)
                   doubleton-map-is-embedding
                   doubleton-map-is-surjection

 doubleton-finite-gives-decidable-equality : funext 𝓀 𝓀₀
                                           β†’ {X : 𝓀 Μ‡ } (xβ‚€ x₁ : X)
                                           β†’ is-set X
                                           β†’ is-finite (Ξ£ x κž‰ X , (x ≑ xβ‚€) ∨ (x ≑ x₁))
                                           β†’ decidable (xβ‚€ ≑ x₁)
 doubleton-finite-gives-decidable-equality fe xβ‚€ x₁ X-is-set Ο• = Ξ΄
  where
   Ξ³ : is-finite (doubleton xβ‚€ x₁) β†’ decidable (xβ‚€ ≑ x₁)
   Ξ³ (0 , s) = βˆ₯βˆ₯-rec (decidability-of-prop-is-prop fe X-is-set) Ξ± s
    where
     Ξ± : doubleton xβ‚€ x₁ ≃ 𝟘 β†’ decidable (xβ‚€ ≑ x₁)
     Ξ± (g , i) = 𝟘-elim (g (xβ‚€ , ∣ inl refl ∣))

   Ξ³ (1 , s) = inl (βˆ₯βˆ₯-rec X-is-set Ξ² s)
    where
     Ξ± : is-prop (Fin 1)
     α 𝟎 𝟎 = refl

     Ξ² : doubleton xβ‚€ x₁ ≃ Fin 1 β†’ xβ‚€ ≑ x₁
     Ξ² (g , i) = ap pr₁ (equivs-are-lc g i (Ξ± (g (doubleton-map xβ‚€ x₁ 𝟎)) (g (doubleton-map xβ‚€ x₁ 𝟏))))

   Ξ³ (succ (succ n) , s) = βˆ₯βˆ₯-rec (decidability-of-prop-is-prop fe X-is-set) f s
    where
     f : doubleton xβ‚€ x₁ ≃ Fin (succ (succ n)) β†’ decidable (xβ‚€ ≑ x₁)
     f (g , i) = Ξ²
      where
       h : xβ‚€ ≑ x₁ β†’ doubleton-map xβ‚€ x₁ 𝟎 ≑ doubleton-map xβ‚€ x₁ 𝟏
       h = to-subtype-≑ (Ξ» _ β†’ ∨-is-prop)

       Ξ± : decidable (g (doubleton-map xβ‚€ x₁ 𝟎) ≑ g (doubleton-map xβ‚€ x₁ 𝟏)) β†’ 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 (doubleton-map xβ‚€ x₁ 𝟎)) (g (doubleton-map xβ‚€ x₁ 𝟏)))

   Ξ΄ : decidable (xβ‚€ ≑ x₁)
   Ξ΄ = Ξ³ Ο•

 all-K-finite-types-finite-gives-all-sets-discrete :

     funext 𝓀 𝓀₀
   β†’ ((A : 𝓀 Μ‡ ) β†’ is-Kuratowski-finite A β†’ is-finite A)
   β†’ (X : 𝓀 Μ‡ ) β†’ is-set X β†’ is-discrete X

 all-K-finite-types-finite-gives-all-sets-discrete {𝓀} fe Ο• X X-is-set xβ‚€ x₁ =
  doubleton-finite-gives-decidable-equality
   fe xβ‚€ x₁ X-is-set
   (Ο• (doubleton xβ‚€ x₁)
   (doubletons-are-Kuratowki-finite xβ‚€ x₁))

 open import UF-ExcludedMiddle

 all-K-finite-types-finite-gives-EM :

     ((𝓀 : Universe) (A : 𝓀 Μ‡ ) β†’ is-Kuratowski-finite A β†’ is-finite A)
   β†’ (𝓀 : Universe) β†’ FunExt β†’ PropExt β†’ EM 𝓀
 all-K-finite-types-finite-gives-EM Ο• 𝓀 fe pe =
  Ξ©-discrete-gives-EM (fe 𝓀 𝓀) (pe 𝓀)
   (all-K-finite-types-finite-gives-all-sets-discrete
     (fe (𝓀 ⁺) 𝓀₀) (Ο• (𝓀 ⁺)) (Ξ© 𝓀) (Ξ©-is-set (fe 𝓀 𝓀) (pe 𝓀)))

\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 also include an open problem related to this.

The following no-selection lemma is contributed by Tom de Jong:

\begin{code}

 open import Two-Properties

 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 s = ⌜ ≃-sym (Ξ± X s) ⌝ β‚€

   γ : 𝟘
   Ξ³ = 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 Kuratowski finite discrete 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 to the question by Steve Vickers
mentioned above:

\begin{code}

 no-orderability-of-K-finite-discrete-types :

  Univalence β†’ Β¬ ((X : 𝓀 Μ‡ ) β†’ is-Kuratowski-finite X β†’ is-discrete X β†’ finite-linear-order X)

 no-orderability-of-K-finite-discrete-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.

(It seems not. More later.)

One more notion of finiteness:

\begin{code}

 is-subfinite : 𝓀 Μ‡ β†’ 𝓀 Μ‡
 is-subfinite X = βˆƒ n κž‰ β„• , X β†ͺ Fin n

 subfiniteness-data : 𝓀 Μ‡ β†’ 𝓀 Μ‡
 subfiniteness-data X = Ξ£ n κž‰ β„• , X β†ͺ Fin n

\end{code}

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.

\begin{code}

 Kuratowski-subfinite-types-are-finite : funext 𝓀 𝓀₀
                                       β†’ {X : 𝓀 Μ‡ }
                                       β†’ is-Kuratowski-finite X
                                       β†’ is-subfinite X
                                       β†’ is-finite X
 Kuratowski-subfinite-types-are-finite fe {X} k = Ξ³
  where
  Ξ΄ : subfiniteness-data X β†’ is-finite X
  Ξ΄ (n , f , e) = Kuratowski-finite-discrete-types-are-finite fe
                   (embeddings-reflect-discreteness f e (Fin-is-discrete n)) k

  Ξ³ : is-subfinite X β†’ is-finite X
  Ξ³ = βˆ₯βˆ₯-rec (being-finite-is-prop X) Ξ΄

\end{code}

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

     βˆƒ n κž‰ β„• , X β†ͺ Fin n  (is-subfinite)
     Ξ£ n κž‰ β„• , X β†ͺ Fin n  (subfiniteness-data)

Addendum.

\begin{code}

 select-equiv-with-𝟚-lemma₁ : FunExt
                            β†’ {X : 𝓀 Μ‡ } (xβ‚€ : X)
                            β†’ is-prop (Ξ£ x₁ κž‰ X , is-equiv (𝟚-cases xβ‚€ x₁))
 select-equiv-with-𝟚-lemma₁ fe {X} xβ‚€ (y , i) (z , j) = V
  where
   f g : 𝟚 β†’ X
   f = 𝟚-cases xβ‚€ y
   g = 𝟚-cases xβ‚€ z

   f' g' : X β†’ 𝟚
   f' = inverse f i
   g' = inverse g j

   I : z β‰’ xβ‚€
   I p = zero-is-not-one
          (β‚€        β‰‘βŸ¨ (inverses-are-retractions g j β‚€)⁻¹ ⟩
           g' (g β‚€) β‰‘βŸ¨ refl ⟩
           g' xβ‚€    β‰‘βŸ¨ ap g' (p ⁻¹) ⟩
           g' z     β‰‘βŸ¨ refl ⟩
           g' (g ₁) β‰‘βŸ¨ inverses-are-retractions g j ₁ ⟩
           ₁        ∎)

   II : (n : 𝟚) β†’ f n ≑ z β†’ ₁ ≑ n
   II β‚€ p = 𝟘-elim (I (p ⁻¹))
   II ₁ p = refl

   III : f (f' z) ≑ z
   III = inverses-are-sections f i z

   IV : y ≑ z
   IV = equivs-are-lc f' (inverses-are-equivs f i)
         (f' y     β‰‘βŸ¨ refl ⟩
          f' (f ₁) β‰‘βŸ¨ inverses-are-retractions f i ₁ ⟩
          ₁        β‰‘βŸ¨ II (f' z) III ⟩
          f' z     ∎)

   V : (y , i) ≑ (z , j)
   V = to-subtype-≑ (Ξ» x₁ β†’ being-equiv-is-prop fe (𝟚-cases xβ‚€ x₁)) IV

 select-equiv-with-𝟚-lemmaβ‚‚ : FunExt
                            β†’ {X : 𝓀 Μ‡ }
                            β†’ X ≃ 𝟚
                            β†’ (xβ‚€ : X) β†’ Ξ£ x₁ κž‰ X , is-equiv (𝟚-cases xβ‚€ x₁)
 select-equiv-with-𝟚-lemmaβ‚‚ fe {X} (f , i) xβ‚€ = Ξ³ (f xβ‚€) xβ‚€ refl
  where
   Ξ³ : (n : 𝟚) (xβ‚€ : X) β†’ n ≑ f xβ‚€ β†’ Ξ£ x₁ κž‰ X , is-equiv (𝟚-cases xβ‚€ x₁)
   Ξ³ β‚€ xβ‚€ p = (x₁ , j)
    where
     x₁ : X
     x₁ = inverse f i ₁

     h : inverse f i ∼ 𝟚-cases xβ‚€ x₁
     h β‚€ = inverse f i β‚€      β‰‘βŸ¨ ap (inverse f i) p ⟩
           inverse f i (f xβ‚€) β‰‘βŸ¨ inverses-are-retractions f i xβ‚€ ⟩
           xβ‚€                 β‰‘βŸ¨ refl ⟩
           𝟚-cases xβ‚€ x₁ β‚€    ∎
     h ₁ = refl

     j : is-equiv (𝟚-cases xβ‚€ x₁)
     j = equiv-closed-under-∼' (inverses-are-equivs f i) h

   Ξ³ ₁ xβ‚€ p = (x₁ , j)
    where
     x₁ : X
     x₁ = inverse f i β‚€

     h : inverse f i ∘ complement ∼ 𝟚-cases xβ‚€ x₁
     h β‚€ = inverse f i (complement β‚€) β‰‘βŸ¨ refl ⟩
           inverse f i ₁              β‰‘βŸ¨ ap (inverse f i) p ⟩
           inverse f i (f xβ‚€)         β‰‘βŸ¨ inverses-are-retractions f i xβ‚€ ⟩
           xβ‚€                         β‰‘βŸ¨ refl  ⟩
           𝟚-cases xβ‚€ x₁ β‚€            ∎
     h ₁ = refl

     j : is-equiv (𝟚-cases xβ‚€ x₁)
     j = equiv-closed-under-∼'
         (∘-is-equiv complement-is-equiv (inverses-are-equivs f i)) h

 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 (select-equiv-with-𝟚-lemma₁ fe xβ‚€)
             (Ξ» 𝕙 β†’ select-equiv-with-𝟚-lemmaβ‚‚ fe 𝕙 xβ‚€)

   Ξ² : Ξ£ x₁ κž‰ X , is-equiv (𝟚-cases xβ‚€ x₁)
   Ξ² = Ξ± 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}