Martin Escardo, 8th December 2019.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Fin.Bishop where

open import Fin.Properties
open import Fin.Type
open import MLTT.Spartan
open import UF.Base
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.UA-FunExt
open import UF.Univalence
open import UF.UniverseEmbedding

\end{code}

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}

There are two ways of making π + π into a linear order. We choose the
following one.

\begin{code}

π+π-natural-finite-linear-order : finite-linear-order (π {π€} + π {π€})
π+π-natural-finite-linear-order {π€} = 2 , g
where
f : π {π€} + π {π€} β (π {π€β} + π {π€β}) + π {π€β}
f = +-cong π-lneutral'' one-π-only

f' : π {π€} + π {π€} β Fin 2
f' = f

g : π {π€} + π {π€} β Fin 2
g = +comm β f'

observation : (β g β (inl β) οΌ π) Γ (β g β (inr β) οΌ π)
observation = refl , refl

\end{code}

Exercise: If X β Fin n, then the type finite-linear-order X has n! elements (solved
elsewhere in TypeTopology).

\begin{code}

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 β β-cong-left fe (β-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}

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

open PropositionalTruncation pt

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