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)