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 : π¦ βΊ Μ

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}

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.

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 _::_ 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 (succ n) xs' = hd' xs' :: xedni n (tl' xs')

vecΞ· : (n : β) {X : Fin n β π€ Μ } β xedni n {X} β index n {X} βΌ id
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

_β_ : β β β β β
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' (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}

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

β 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}

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.

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

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 β©
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 β©
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)

\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' (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' (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β β©
π-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β β©
π-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}