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