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}

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}