Martin Escardo, November 2019

Other interesting uses of the types Fin n is in the file
which proves commutativity of addition and multiplication, and more,
using the corresponding properties for (finite) types.


{-# 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


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


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


The type Fin n is compact, or exhaustively searchable.


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 ๐ŸŽ


Added 15th December 2019.

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


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)


Finite types are compact, or exhaustively searchable.


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โˆฅ ฯ†)


Finite types are discrete and hence sets:


 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
   ฮณ : 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 ฮณ
   ฮณ : P โ†’ ๐Ÿ˜
   ฮณ p = โˆฅโˆฅ-rec ๐Ÿ˜-is-prop (ฮป (f , _) โ†’ f p) s

 finite-propositions-are-decidable {๐“ค} {P} i (succ n , s) = inl ฮณ
   ฮณ : 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 = ฮณ
   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