# The well-ordering principle of the standard finite types

```agda
module elementary-number-theory.well-ordering-principle-standard-finite-types where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.inequality-standard-finite-types
open import elementary-number-theory.modular-arithmetic-standard-finite-types
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.well-ordering-principle-natural-numbers

open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.decidable-subtypes
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.hilberts-epsilon-operators
open import foundation.identity-types
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-empty-type
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universe-levels

open import univalent-combinatorics.counting
open import univalent-combinatorics.decidable-dependent-pair-types
open import univalent-combinatorics.standard-finite-types
```

</details>

## Idea

The standard finite types inherit a well-ordering principle from the natural
numbers.

## Properties

### For any decidable family `P` over `Fin n`, if `P x` doesn't hold for all `x` then there exists an `x` for which `P x` is false

```agda
exists-not-not-for-all-Fin :
  {l : Level} (k : ℕ) {P : Fin k → UU l} → (is-decidable-fam P) →
  ¬ ((x : Fin k) → P x) → Σ (Fin k) (λ x → ¬ (P x))
exists-not-not-for-all-Fin {l} zero-ℕ d H = ex-falso (H ind-empty)
exists-not-not-for-all-Fin {l} (succ-ℕ k) {P} d H with d (inr star)
... | inl p =
  T ( exists-not-not-for-all-Fin k
      ( λ x → d (inl x))
      ( λ f → H (ind-coproduct P f (ind-unit p))))
  where
  T : Σ (Fin k) (λ x → ¬ (P (inl x))) → Σ (Fin (succ-ℕ k)) (λ x → ¬ (P x))
  T z = pair (inl (pr1 z)) (pr2 z)
... | inr f = pair (inr star) f

exists-not-not-for-all-count :
  {l1 l2 : Level} {X : UU l1} (P : X → UU l2) →
  (is-decidable-fam P) → count X →
  ¬ ((x : X) → P x) → Σ X (λ x → ¬ (P x))
exists-not-not-for-all-count {l1} {l2} {X} P p e =
  ( g) ∘
  ( ( exists-not-not-for-all-Fin
      ( number-of-elements-count e)
      ( p ∘ map-equiv-count e)) ∘ f)
  where
  k : ℕ
  k = number-of-elements-count e
  P' : Fin k → UU l2
  P' = P ∘ map-equiv (pr2 e)
  f : ¬ ((x : X) → P x) → ¬ ((x : Fin k) → P' x)
  f nf f' =
    nf
      ( λ x →
        tr
          ( P)
          ( htpy-eq-equiv (right-inverse-law-equiv (pr2 e)) x)
          ( f' (map-inv-equiv (pr2 e) x)))
  g : Σ (Fin k) (λ x → ¬ (P' x)) → Σ X (λ x → ¬ (P x))
  pr1 (g (pair l np)) = map-equiv (pr2 e) l
  pr2 (g (pair l np)) x = np x
```

```agda
is-lower-bound-Fin :
  {l : Level} (k : ℕ) (P : Fin k → UU l) → Fin k → UU l
is-lower-bound-Fin k P x = (y : Fin k) → P y → leq-Fin k x y

abstract
  is-prop-is-lower-bound-Fin :
    {l : Level} (k : ℕ) {P : Fin k → UU l} (x : Fin k) →
    is-prop (is-lower-bound-Fin k P x)
  is-prop-is-lower-bound-Fin k x =
    is-prop-Π (λ y → is-prop-function-type (is-prop-leq-Fin k x y))

  is-lower-bound-fin-Prop :
    {l : Level} (k : ℕ) (P : Fin k → UU l) (x : Fin k) → Prop l
  pr1 (is-lower-bound-fin-Prop k P x) = is-lower-bound-Fin k P x
  pr2 (is-lower-bound-fin-Prop k P x) = is-prop-is-lower-bound-Fin k x

minimal-element-Fin :
  {l : Level} (k : ℕ) (P : Fin k → UU l) → UU l
minimal-element-Fin k P =
  Σ (Fin k) (λ x → (P x) × is-lower-bound-Fin k P x)

abstract
  all-elements-equal-minimal-element-Fin :
    {l : Level} (k : ℕ) (P : subtype l (Fin k)) →
    all-elements-equal (minimal-element-Fin k (is-in-subtype P))
  all-elements-equal-minimal-element-Fin k P
    (pair x (pair p l)) (pair y (pair q m)) =
    eq-type-subtype
      ( λ t →
        product-Prop (P t) (is-lower-bound-fin-Prop k (is-in-subtype P) t))
      ( antisymmetric-leq-Fin k x y (l y q) (m x p))

abstract
  is-prop-minimal-element-Fin :
    {l : Level} (k : ℕ) (P : subtype l (Fin k)) →
    is-prop (minimal-element-Fin k (is-in-subtype P))
  is-prop-minimal-element-Fin k P =
    is-prop-all-elements-equal (all-elements-equal-minimal-element-Fin k P)

minimal-element-Fin-Prop :
  {l : Level} (k : ℕ) (P : subtype l (Fin k)) → Prop l
pr1 (minimal-element-Fin-Prop k P) = minimal-element-Fin k (is-in-subtype P)
pr2 (minimal-element-Fin-Prop k P) = is-prop-minimal-element-Fin k P

is-lower-bound-inl-Fin :
  {l : Level} (k : ℕ) {P : Fin (succ-ℕ k) → UU l} {x : Fin k} →
  is-lower-bound-Fin k (P ∘ inl) x →
  is-lower-bound-Fin (succ-ℕ k) P (inl-Fin k x)
is-lower-bound-inl-Fin k H (inl y) p = H y p
is-lower-bound-inl-Fin k {P} {x} H (inr star) p =
  ( leq-neg-one-Fin k (inl x))

well-ordering-principle-Σ-Fin :
  {l : Level} (k : ℕ) {P : Fin k → UU l} → ((x : Fin k) → is-decidable (P x)) →
  Σ (Fin k) P → minimal-element-Fin k P
pr1 (well-ordering-principle-Σ-Fin (succ-ℕ k) d (pair (inl x) p)) =
  inl (pr1 (well-ordering-principle-Σ-Fin k (λ x' → d (inl x')) (pair x p)))
pr1 (pr2 (well-ordering-principle-Σ-Fin (succ-ℕ k) d (pair (inl x) p))) =
  pr1 (pr2 (well-ordering-principle-Σ-Fin k (λ x' → d (inl x')) (pair x p)))
pr2 (pr2 (well-ordering-principle-Σ-Fin (succ-ℕ k) d (pair (inl x) p))) =
  is-lower-bound-inl-Fin k (pr2 (pr2 m))
  where
  m = well-ordering-principle-Σ-Fin k (λ x' → d (inl x')) (pair x p)
well-ordering-principle-Σ-Fin (succ-ℕ k) {P} d (pair (inr star) p)
  with
  is-decidable-Σ-Fin k (λ t → d (inl t))
... | inl t =
  pair
    ( inl (pr1 m))
    ( pair (pr1 (pr2 m)) (is-lower-bound-inl-Fin k (pr2 (pr2 m))))
  where
  m = well-ordering-principle-Σ-Fin k (λ x' → d (inl x')) t
... | inr f =
  pair
    ( inr star)
    ( pair p g)
  where
  g : (y : Fin (succ-ℕ k)) → P y → leq-Fin (succ-ℕ k) (neg-one-Fin k) y
  g (inl y) q = ex-falso (f (pair y q))
  g (inr star) q = refl-leq-Fin (succ-ℕ k) (neg-one-Fin k)

well-ordering-principle-∃-Fin :
  {l : Level} (k : ℕ) (P : decidable-subtype l (Fin k)) →
  exists (Fin k) (subtype-decidable-subtype P) →
  minimal-element-Fin k (is-in-decidable-subtype P)
well-ordering-principle-∃-Fin k P H =
  apply-universal-property-trunc-Prop H
    ( minimal-element-Fin-Prop k (subtype-decidable-subtype P))
    ( well-ordering-principle-Σ-Fin k
      ( is-decidable-decidable-subtype P))
```

### Hilbert's `ε`-operator for decidable subtypes of standard finite types

```agda
ε-operator-decidable-subtype-Fin :
  {l : Level} (k : ℕ) (P : decidable-subtype l (Fin k)) →
  ε-operator-Hilbert (type-decidable-subtype P)
ε-operator-decidable-subtype-Fin {l} zero-ℕ P t =
  ex-falso (apply-universal-property-trunc-Prop t empty-Prop pr1)
ε-operator-decidable-subtype-Fin {l} (succ-ℕ k) P t =
  map-Σ
    ( is-in-decidable-subtype P)
    ( mod-succ-ℕ k)
    ( λ x → id)
    ( ε-operator-total-Q
      ( map-trunc-Prop
        ( map-Σ
          ( type-Prop ∘ Q)
          ( nat-Fin (succ-ℕ k))
          ( λ x →
            tr (is-in-decidable-subtype P) (inv (is-section-nat-Fin k x))))
        ( t)))
  where
  Q : ℕ → Prop l
  Q n = subtype-decidable-subtype P (mod-succ-ℕ k n)
  is-decidable-Q : (n : ℕ) → is-decidable (type-Prop (Q n))
  is-decidable-Q n =
    is-decidable-decidable-subtype P (mod-succ-ℕ k n)
  ε-operator-total-Q : ε-operator-Hilbert (type-subtype Q)
  ε-operator-total-Q =
    ε-operator-decidable-subtype-ℕ Q is-decidable-Q
```

```agda
abstract
  elim-trunc-decidable-fam-Fin :
    {l1 : Level} {k : ℕ} {B : Fin k → UU l1} →
    ((x : Fin k) → is-decidable (B x)) →
    type-trunc-Prop (Σ (Fin k) B) → Σ (Fin k) B
  elim-trunc-decidable-fam-Fin {l1} {zero-ℕ} {B} d y =
    ex-falso (is-empty-type-trunc-Prop pr1 y)
  elim-trunc-decidable-fam-Fin {l1} {succ-ℕ k} {B} d y
    with d (inr star)
  ... | inl x = pair (inr star) x
  ... | inr f =
    map-Σ-map-base inl B
      ( elim-trunc-decidable-fam-Fin {l1} {k} {B ∘ inl}
        ( λ x → d (inl x))
        ( map-equiv-trunc-Prop
          ( ( ( right-unit-law-coproduct-is-empty
                ( Σ (Fin k) (B ∘ inl))
                ( B (inr star)) f) ∘e
              ( equiv-coproduct id-equiv (left-unit-law-Σ (B ∘ inr)))) ∘e
            ( right-distributive-Σ-coproduct (Fin k) unit B))
          ( y)))
```