Todd Waugh Ambridge, January 2024

# Finite types

\begin{code}
{-# OPTIONS --without-K --safe #-}

open import MLTT.Spartan
open import UF.DiscreteAndSeparated
open import UF.Sets
open import UF.Sets-Properties
open import UF.Equiv
open import UF.EquivalenceExamples
open import Fin.Type
open import Fin.Bishop
open import Fin.ArithmeticViaEquivalence
open import MLTT.SpartanList

module TWA.Thesis.Chapter2.Finite where

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 (succ n) = +-is-set (Fin n) πŸ™ (Fin-is-set n) πŸ™-is-set

finite-is-discrete
 : {F : 𝓀 Μ‡ } β†’ (f : finite-linear-order F) β†’ is-discrete F
finite-is-discrete (n , f)
 = equiv-to-discrete (≃-sym f) (Fin-is-discrete n)

finite-is-set : {F : 𝓀 Μ‡ } β†’ (f : finite-linear-order F) β†’ is-set F
finite-is-set (n , f) = equiv-to-set f (Fin-is-set n)

πŸ™-is-finite : finite-linear-order (πŸ™ {𝓦})
πŸ™-is-finite = 1 , qinveq g (h , Ξ· , ΞΌ)
 where
  g : πŸ™ β†’ Fin 1
  g ⋆ = 𝟎
  h : Fin 1 β†’ πŸ™
  h 𝟎 = ⋆
  η : h ∘ g ∼ id
  Ξ· ⋆ = refl
  μ : g ∘ h ∼ id
  μ 𝟎 = refl
  ΞΌ (suc ())

𝟚-is-finite : finite-linear-order 𝟚
𝟚-is-finite = 2 , qinveq g (h , η , μ)
 where
  g : 𝟚 β†’ Fin 2
  g β‚€ = 𝟎
  g ₁ = 𝟏
  h : Fin 2 β†’ 𝟚
  h 𝟎 = β‚€
  h 𝟏 = ₁
  η : h ∘ g ∼ id
  Ξ· β‚€ = refl
  Ξ· ₁ = refl
  μ : g ∘ h ∼ id
  μ 𝟎 = refl
  μ 𝟏 = refl

+-is-finite : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
            β†’ finite-linear-order X
            β†’ finite-linear-order Y
            β†’ finite-linear-order (X + Y)
+-is-finite (n , e) (m , f)
 = n +' m , (+-cong e f ● ≃-sym (Fin+homo n m))

Γ—-is-finite : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
            β†’ finite-linear-order X
            β†’ finite-linear-order Y
            β†’ finite-linear-order (X Γ— Y)
Γ—-is-finite (n , e) (m , f)
 = n Γ—' m , (Γ—-cong e f ● ≃-sym (FinΓ—homo n m))

vec-is-finite : (Ο΅ : β„•) {F : Fin Ο΅ β†’ 𝓀 Μ‡ }
              β†’ (f : (n : Fin Ο΅) β†’ finite-linear-order (F n))
              β†’ finite-linear-order (vec Ο΅ F)
vec-is-finite 0 f = πŸ™-is-finite
vec-is-finite (succ Ο΅) f
 = Γ—-is-finite (f 𝟎) (vec-is-finite Ο΅ (f ∘ suc))

pointed : 𝓀 Μ‡ β†’ 𝓀 Μ‡
pointed X = X
\end{code}