Martin Escardo, November 2019

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 --safe --without-K #-}

module Fin.Topology where

open import Fin.Bishop
open import Fin.Properties
open import Fin.Type
open import MLTT.Plus-Properties
open import MLTT.Spartan
open import MLTT.SpartanList
open import Notation.Order
open import TypeTopology.CompactTypes
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.ExcludedMiddle
open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.SubtypeClassifier
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

\end{code}

Recall that a type is discrete if it has decidable equality.

\begin{code}

Fin-is-discrete : {n : โ} โ is-discrete (Fin n)
Fin-is-discrete {0     } = ๐-is-discrete
Fin-is-discrete {succ n} = +-is-discrete (Fin-is-discrete {n}) ๐-is-discrete

Fin-is-set : {n : โ} โ is-set (Fin n)
Fin-is-set = discrete-types-are-sets Fin-is-discrete

\end{code}

The type Fin n is compact, or exhaustively searchable.

\begin{code}

Fin-Compact : {n : โ} โ is-Compact (Fin n) {๐ค}
Fin-Compact {๐ค} {0}      = ๐-is-Compact
Fin-Compact {๐ค} {succ n} = +-is-Compact (Fin-Compact {๐ค} {n}) ๐-is-Compact

Fin-ฮ -Compact : (n : โ) โ is-ฮ -Compact (Fin n) {๐ค}
Fin-ฮ -Compact n = ฮฃ-Compact-types-are-ฮ -Compact (Fin n) Fin-Compact

Fin-Compactโ : (n : โ) โ is-Compactโ (Fin (succ n)) {๐ค}
Fin-Compactโ n = Compact-pointed-gives-Compactโ Fin-Compact ๐

\end{code}

If the type X i is compact for every i : Fin n, then the product type
(i : Fin n) โ X i is also compact.

\begin{code}

finite-product-compact : (n : โ) (X : Fin n โ ๐ค ฬ )
โ ((i : Fin n) โ is-Compact (X i) {๐ค})
โ is-Compact (vec n X) {๐ค}

finite-product-compact zero     X c = ๐-is-Compact
finite-product-compact (succ n) X c = ร-is-Compact
(c ๐)
(finite-product-compact n (X โ suc) (c โ suc))

finitely-indexed-product-compact : funext ๐คโ ๐ค
โ (n : โ) (X : Fin n โ ๐ค ฬ )
โ ((i : Fin n) โ is-Compact (X i))
โ is-Compact ((i : Fin n) โ X i)

finitely-indexed-product-compact fe n X c = Compact-closed-under-โ
(vec-โ fe n)
(finite-product-compact n X c)

\end{code}

Finite types are compact, or exhaustively searchable.

\begin{code}

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

open PropositionalTruncation pt
open CompactTypesPT pt
open finiteness pt

finite-โฅCompactโฅ : {X : ๐ค ฬ } โ is-finite X โ โฅ is-Compact X {๐ฅ} โฅ
finite-โฅCompactโฅ {๐ค} {๐ฅ} {X} (n , ฮฑ) =
โฅโฅ-functor (ฮป (e : X โ Fin n) โ Compact-closed-under-โ (โ-sym e) Fin-Compact) ฮฑ

finite-types-are-โ-Compact : Fun-Ext โ {X : ๐ค ฬ } โ is-finite X โ is-โ-Compact X {๐ฅ}
finite-types-are-โ-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

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 ฯ)

finite-propositions-are-decidable' : Fun-Ext
โ {P : ๐ค ฬ }
โ is-prop P
โ is-finite P
โ is-decidable P
finite-propositions-are-decidable' fe i j =
โ-Compact-propositions-are-decidable i (finite-types-are-โ-Compact fe j)

finite-propositions-are-decidable : {P : ๐ค ฬ }
โ is-prop P
โ is-finite P
โ is-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

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 : ๐ฆ โบ ฬ
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}