Fin

Alice Laroche, 25th September 2023
With additions by Fredrik Nordvall Forsberg on 9 October 2025

Fin n is an ordinal


{-# OPTIONS --safe --without-K --lossy-unification #-}

module Ordinals.Fin where

open import Fin.Embeddings
open import Fin.Order
open import Fin.Type
open import MLTT.Spartan hiding (_^_)
open import MLTT.Plus-Properties
open import Naturals.Addition renaming (_+_ to _+β„•_)
open import Naturals.Multiplication
open import Naturals.Exponentiation
open import Notation.Order
open import Ordinals.Equivalence
open import Ordinals.Maps
open import Ordinals.Notions
open import Ordinals.Type
open import UF.Base
open import UF.Equiv
open import UF.FunExt
open import UF.UA-FunExt
open import UF.Univalence

import Naturals.Order as β„•

<-is-prop-valued : (n : β„•) β†’ is-prop-valued {X = Fin n} _<_
<-is-prop-valued n i j = β„•.<-is-prop-valued ⟦ i ⟧ ⟦ j ⟧

<-is-well-founded : (n : β„•) β†’ is-well-founded {X = Fin n} _<_
<-is-well-founded n i = recurs (β„•.<-is-well-founded (⟦ i ⟧))
 where
  recurs : {i : Fin n}
         β†’ is-accessible {X = β„•} _<_ (⟦ i ⟧)
         β†’ is-accessible {X = Fin n} _<_ i
  recurs (acc rec₁) = acc (Ξ» j r β†’ recurs (rec₁ ⟦ j ⟧ r))

<-is-extensional : (n : β„•) β†’ is-extensional {X = Fin n} _<_
<-is-extensional 0 x y iβ‰Όj jβ‰Όi = 𝟘-elim x
<-is-extensional (succ n) 𝟎 𝟎 iβ‰Όj jβ‰Όi = refl
<-is-extensional (succ n) 𝟎 (suc x) iβ‰Όj jβ‰Όi = 𝟘-elim (jβ‰Όi 𝟎 ⋆)
<-is-extensional (succ n) (suc i) 𝟎 iβ‰Όj jβ‰Όi = 𝟘-elim (iβ‰Όj 𝟎 ⋆)
<-is-extensional (succ n) (suc i) (suc j) i≼j j≼i =
 ap suc (<-is-extensional n i j (iβ‰Όj ∘ suc) (jβ‰Όi ∘ suc))

<-trans : (n : β„•) β†’ is-transitive {X = Fin n} _<_
<-trans n i j k = β„•.<-trans ⟦ i ⟧ ⟦ j ⟧ ⟦ k ⟧

<-is-well-order : (n : β„•) β†’ is-well-order {X = Fin n} _<_
<-is-well-order n = <-is-prop-valued n
                  , <-is-well-founded n
                  , <-is-extensional n
                  , <-trans n

Fin-ordinal : (n : β„•) β†’ Ord
Fin-ordinal n = Fin n , _<_ , <-is-well-order n


Added 9 October 2025 by Fredrik Nordvall Forsberg.

The construction of finite ordinals, from natural numbers to ordinals, preserves
many arithmetical operations.


module _ (ua : Univalence) where

 private
  fe : FunExt
  fe = Univalence-gives-FunExt ua

  fe' : Fun-Ext
  fe' {𝓀} {π“₯} = fe 𝓀 π“₯

 open import Ordinals.Arithmetic fe
 open import Ordinals.AdditionProperties ua
 open import Ordinals.MultiplicationProperties ua
 open import Ordinals.OrdinalOfOrdinals ua

 Fin-ordinal-zero : Fin-ordinal 0 ＝ πŸ˜β‚’
 Fin-ordinal-zero =
  eqtoidβ‚’ (ua _) fe' (Fin-ordinal 0) πŸ˜β‚’
          (id ,  (Ξ» x y l β†’ 𝟘-elim x) , id-is-equiv 𝟘 , (Ξ» x y l β†’ 𝟘-elim x))

 Fin-ordinal-succ : (n : β„•) β†’ Fin-ordinal (succ n) ＝ πŸ™β‚’ +β‚’ Fin-ordinal n
 Fin-ordinal-succ n = eqtoidβ‚’ (ua _) fe' Ξ± Ξ² (f , f-order-equiv)
  where
   Ξ± = Fin-ordinal (succ n)
   Ξ² = πŸ™β‚’ +β‚’ Fin-ordinal n

   f : Fin n + πŸ™ β†’ πŸ™ + Fin n
   f = +-commutative

   f-equiv : is-equiv f
   f-equiv = qinvs-are-equivs f (g , Ξ΅ , Ξ·)
    where
     g : πŸ™ + Fin n β†’ Fin n + πŸ™
     g = +-commutative

     Ξ΅ : βˆ€ x β†’ g (f x) ＝  x
     Ξ΅ (inl x) = refl
     Ξ΅ (inr x) = refl

     Ξ· : βˆ€ x β†’ f (g x) ＝  x
     Ξ· (inl x) = refl
     Ξ· (inr x) = refl

   f-order-preserving : is-order-preserving Ξ± Ξ² f
   f-order-preserving (inl n) (inl m) l = l
   f-order-preserving (inr ⋆) (inl m) l = l
   f-order-preserving (inl n) (inr ⋆) l = 𝟘-elim l
   f-order-preserving (inr ⋆) (inr ⋆) l = 𝟘-elim l

   f-order-reflecting : is-order-reflecting Ξ± Ξ² f
   f-order-reflecting (inl n) (inl m) l = l
   f-order-reflecting (inr ⋆) (inl m) l = l
   f-order-reflecting (inl n) (inr ⋆) l = 𝟘-elim l
   f-order-reflecting (inr ⋆) (inr ⋆) l = 𝟘-elim l

   f-order-equiv : is-order-equiv Ξ± Ξ² f
   f-order-equiv = order-preserving-reflecting-equivs-are-order-equivs
                    Ξ± Ξ² f f-equiv f-order-preserving f-order-reflecting


The construction of finite ordinals preserves addition.


 Fin-ordinal-+β‚’ : (n m : β„•)
                β†’ Fin-ordinal (n +β„• m) ＝ Fin-ordinal n +β‚’ Fin-ordinal m
 Fin-ordinal-+β‚’ zero m =
  F (0 +β„• m)    ＝⟨ ap F (zero-left-neutral m) ⟩
  F m           ＝⟨ πŸ˜β‚’-left-neutral (F m) ⁻¹ ⟩
  πŸ˜β‚’ +β‚’ F m     ＝⟨ ap (_+β‚’ F m) Fin-ordinal-zero ⁻¹ ⟩
  F zero +β‚’ F m ∎
   where
    F = Fin-ordinal
 Fin-ordinal-+β‚’ (succ n) m =
  F (succ n +β„• m)    ＝⟨ ap F (succ-left n m) ⟩
  F (succ (n +β„• m))  ＝⟨ Fin-ordinal-succ (n +β„• m) ⟩
  πŸ™β‚’ +β‚’ F (n +β„• m)   ＝⟨ ap (πŸ™β‚’ +β‚’_) (Fin-ordinal-+β‚’ n m) ⟩
  πŸ™β‚’ +β‚’ (F n +β‚’ F m) ＝⟨ +β‚’-assoc πŸ™β‚’ (F n) (F m) ⁻¹ ⟩
  (πŸ™β‚’ +β‚’ F n) +β‚’ F m ＝⟨ ap (_+β‚’ F m) (Fin-ordinal-succ n ⁻¹) ⟩
  F (succ n) +β‚’ F m  ∎
   where
    F = Fin-ordinal

 Fin-ordinal-one : Fin-ordinal 1 ＝ πŸ™β‚’
 Fin-ordinal-one = Fin-ordinal 1       ＝⟨ Fin-ordinal-succ 0 ⟩
                   πŸ™β‚’ +β‚’ Fin-ordinal 0 ＝⟨ ap (πŸ™β‚’ +β‚’_) Fin-ordinal-zero ⟩
                   πŸ™β‚’ +β‚’ πŸ˜β‚’            ＝⟨ πŸ˜β‚’-right-neutral πŸ™β‚€ ⟩
                   πŸ™β‚’                  ∎

 Fin-ordinal-succ' : (n : β„•) β†’ Fin-ordinal (succ n) ＝ Fin-ordinal n +β‚’ πŸ™β‚’
 Fin-ordinal-succ' n =
  Fin-ordinal (succ n)           ＝⟨refl⟩
  Fin-ordinal (n +β„• 1)           ＝⟨ Fin-ordinal-+β‚’ n 1 ⟩
  Fin-ordinal n +β‚’ Fin-ordinal 1 ＝⟨ ap (Fin-ordinal n +β‚’_) Fin-ordinal-one ⟩
  Fin-ordinal n +β‚’ πŸ™β‚’            ∎

 Fin-ordinal-two : Fin-ordinal 2 ＝ πŸšβ‚’
 Fin-ordinal-two = Fin-ordinal-succ' 1 βˆ™ ap (_+β‚’ πŸ™β‚’) Fin-ordinal-one

 Fin-ordinal-three : Fin-ordinal 3 ＝ πŸ›β‚’
 Fin-ordinal-three = Fin-ordinal-succ' 2 βˆ™ ap (_+β‚’ πŸ™β‚’) Fin-ordinal-two


The construction of finite ordinals preserves multiplication.


 Fin-ordinal-Γ—β‚’ : (n m : β„•)
                β†’ Fin-ordinal (n * m) ＝ Fin-ordinal n Γ—β‚’ Fin-ordinal m
 Fin-ordinal-Γ—β‚’ n zero = transport⁻¹ (Ξ» - β†’ - ＝ Fin-ordinal n Γ—β‚’ -)
                                     Fin-ordinal-zero
                                     (Γ—β‚’-πŸ˜β‚’-right (Fin-ordinal n) ⁻¹)
 Fin-ordinal-Γ—β‚’ n (succ m) =
  F (n +β„• n * m)          ＝⟨ Fin-ordinal-+β‚’ n (n * m) ⟩
  F n +β‚’ F (n * m)        ＝⟨ ap (F n +β‚’_) (Fin-ordinal-Γ—β‚’ n m) ⟩
  F n +β‚’ F n Γ—β‚’ F m       ＝⟨ I ⟩
  F n Γ—β‚’ πŸ™β‚€ +β‚’ F n Γ—β‚’ F m ＝⟨ Γ—β‚’-distributes-+β‚’-right (F n) πŸ™β‚’ (F m) ⁻¹ ⟩
  F n Γ—β‚’ (πŸ™β‚€ +β‚’ F m)      ＝⟨ ap (F n Γ—β‚’_) (Fin-ordinal-succ m ⁻¹) ⟩
  F n Γ—β‚’ F (succ m)       ∎
   where
    F = Fin-ordinal
    I = ap (_+β‚’ F n Γ—β‚’ F m) (πŸ™β‚’-right-neutral-Γ—β‚’ (F n) ⁻¹)


The construction of finite ordinals is order preserving.


 Fin-ordinal-preserves-≀ : {n m : β„•} β†’ n ≀ m β†’ Fin-ordinal n ⊴ Fin-ordinal m
 Fin-ordinal-preserves-≀ {zero} {m} l =
  transport⁻¹ (_⊴ Fin-ordinal m) Fin-ordinal-zero (πŸ˜β‚’-least-⊴ (Fin-ordinal m))
 Fin-ordinal-preserves-≀ {succ n} {zero}   l = 𝟘-elim l
 Fin-ordinal-preserves-≀ {succ n} {succ m} l =
  transport₂⁻¹ _⊴_ (Fin-ordinal-succ n)
                   (Fin-ordinal-succ m)
                   (+β‚’-right-monotone-⊴ πŸ™β‚’ (Fin-ordinal n)
                                           (Fin-ordinal m)
                                           (Fin-ordinal-preserves-≀ l))

 Fin-ordinal-succ-positive : (n : β„•) β†’ πŸ™β‚’ ⊴ Fin-ordinal (succ n)
 Fin-ordinal-succ-positive n =
  transport (_⊴ Fin-ordinal (succ n)) Fin-ordinal-one (Fin-ordinal-preserves-≀ ⋆)


The construction of finite ordinals preserves exponentiation whenever the base
is positive.


 open import UF.PropTrunc
 open import UF.Size

 module _ (pt : propositional-truncations-exist)
          (sr : Set-Replacement pt)
        where

  open import Ordinals.Exponentiation.Supremum ua pt sr

  Fin-ordinal-^β‚’ : (n m : β„•)
                 β†’ let n' = succ n
                   in Fin-ordinal (n' ^ m) ＝ Fin-ordinal n' ^β‚’ Fin-ordinal m
  Fin-ordinal-^β‚’ n zero =
   Fin-ordinal (succ n ^ zero)             ＝⟨refl⟩
   Fin-ordinal 1                            ＝⟨ Fin-ordinal-one ⟩
   πŸ™β‚€                                       ＝⟨ I ⟩
   Fin-ordinal (succ n) ^β‚’ πŸ˜β‚’               ＝⟨ II ⟩
   Fin-ordinal (succ n) ^β‚’ Fin-ordinal zero ∎
    where
     I = ^β‚’-satisfies-zero-specification (Fin-ordinal (succ n)) ⁻¹
     II = ap (Fin-ordinal (succ n) ^β‚’_) (Fin-ordinal-zero ⁻¹)
  Fin-ordinal-^β‚’ n (succ m) =
   Fin-ordinal (n' ^ succ m)                        ＝⟨refl⟩
   Fin-ordinal (n' * n' ^ m)                        ＝⟨ I ⟩
   Fin-ordinal (n' ^ m * n')                        ＝⟨ II ⟩
   Fin-ordinal (n' ^ m) Γ—β‚’ Fin-ordinal n'           ＝⟨ III ⟩
   Fin-ordinal n' ^β‚’ Fin-ordinal m Γ—β‚’ Fin-ordinal n' ＝⟨ IV ⟩
   Fin-ordinal n' ^β‚’ (Fin-ordinal m +β‚’ πŸ™β‚€)           ＝⟨ V ⟩
   Fin-ordinal n' ^β‚’ Fin-ordinal (succ m)            ∎
    where
     n' = succ n

     I = ap Fin-ordinal (mult-commutativity n' (n' ^ m))
     II = Fin-ordinal-Γ—β‚’ (n' ^ m) n'
     III = ap (_Γ—β‚’ Fin-ordinal n') (Fin-ordinal-^β‚’ n m)
     IV = ^β‚’-satisfies-succ-specification (Fin-ordinal n')
                                          (Fin-ordinal-succ-positive n)
                                          (Fin-ordinal m) ⁻¹
     V = ap (Fin-ordinal n' ^β‚’_) (Fin-ordinal-succ' m ⁻¹)