Strict well-orders, and least elements

One construction ahead needs to choose: the axiom of choice, at the end of the book, has to pick an element out of each cell of a family, and the classical way to make that choice is to well-order the candidates and take the least one that qualifies.

The reflection argument was expected to be a second consumer and is not. It was delivered with no order at all, as a ladder whose limit answers for every matrix at once, built jointly rather than selected from. So this vocabulary has one consumer rather than two, and it is L.Choice.Transversal, the last chapter of the book: the search below is what picks a point out of each cell of a disjoint family.

This chapter provides the vocabulary. A strict well-order on a type is a relation that is trichotomous, irreflexive, transitive and well founded, bundled as a record so that later chapters can carry one around as data. The bundle is level-generic in a way worth one remark: the carrier and the relation take separate universe levels, because the order that Part 4 eventually builds compares formulas, which are small, by data that mentions ordinals, which are not.

The theorem is that a non-empty subset has a least element, and it is unique. Uniqueness is free from trichotomy. Existence is not: deciding, at each step, whether anything smaller still qualifies is exactly a decision about an arbitrary predicate, so this is the second place the book spends the excluded middle. Unlike the first, here the cost buys a genuine choice function rather than a comparison.

The assumption sits on that one theorem rather than on the chapter, which is worth doing wherever it can be done: the bundle, the uniqueness of least elements, and everything a later chapter needs in order to state an order are constructive, and only the search is not.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Truth
open import Base.Classical using ( LEM )

module L.WellOrder.Base {ℓₚ : Level} where

open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ )
open import Cubical.Relation.Nullary using ( ¬_; isProp¬ )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Sum using ( _⊎_; inl; inr )

Trichotomy, as data

Three mutually exclusive alternatives, carried as an inductive type rather than a nested sum, so that a proof can name the case it is in.

data Tri {ℓ₁ ℓ₂ ℓ₃ : Level} (A : Type ℓ₁) (B : Type ℓ₂) (C : Type ℓ₃)
       : Type (ℓ-max ℓ₁ (ℓ-max ℓ₂ ℓ₃)) where
  lt : A → Tri A B C
  eq : B → Tri A B C
  gt : C → Tri A B C

The bundle

The four laws, packaged. Well-foundedness is the library's accessibility predicate, which is what makes the least-element search below terminate.

record SWO {ℓc : Level} (A : Type ℓc) : Type (ℓ-max ℓc (ℓ-suc ℓₚ)) where
  field
    _<∙_   : A → A → Type ℓₚ
    tri∙   : (a b : A) → Tri (a <∙ b) (a ≡ b) (b <∙ a)
    irr∙   : (a : A) → ¬ a <∙ a
    trans∙ : (a b c : A) → a <∙ b → b <∙ c → a <∙ c
    wf∙    : WellFounded _<∙_

Least elements

Being least for a predicate is satisfying it while nothing satisfying it is strictly smaller. That is a proposition, and so is being a least element: given two, trichotomy rules out both strict cases and leaves equality. This is what lets the search below deliver an honest element out of a merely truncated non-emptiness, since a proposition-valued goal absorbs the truncation.

module _ {ℓc : Level} {A : Type ℓc} (w : SWO {ℓc} A) where
  open SWO w

  IsLeast : {ℓ'' : Level} → (A → hProp ℓ'') → A → Type (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))
  IsLeast P a = ⟨ P a ⟩ × ((b : A) → ⟨ P b ⟩ → ¬ b <∙ a)

  isPropIsLeast : {ℓ'' : Level} (P : A → hProp ℓ'') (a : A) → isProp (IsLeast P a)
  isPropIsLeast P a = isProp× (snd (P a)) (isPropΠ λ b → isPropΠ λ _ → isProp¬ _)

  isPropLeastOf : {ℓ'' : Level} (P : A → hProp ℓ'')
                → isProp (Σ[ a ∈ A ] IsLeast P a)
  isPropLeastOf P (m , pm , minm) (m' , pm' , minm') =
    Σ≡Prop (isPropIsLeast P) (decide (tri∙ m m'))
    where
    decide : Tri (m <∙ m') (m ≡ m') (m' <∙ m) → m ≡ m'
    decide (lt m<m') = Empty.rec (minm' m pm m<m')
    decide (eq e)    = e
    decide (gt m'<m) = Empty.rec (minm m' pm' m'<m)

And the search. Start anywhere in the subset and descend: ask whether some smaller element still satisfies the predicate; if one does, recurse into it, which terminates because the relation is well founded; if none does, the current element is least by definition. The question asked at each step is about an arbitrary predicate, and that is where the excluded middle enters.

  leastOf : {ℓ'' : Level} → LEM (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))
          → (P : A → hProp ℓ'')
          → ∥ Σ[ a ∈ A ] ⟨ P a ⟩ ∥₁ → Σ[ a ∈ A ] IsLeast P a
  leastOf {ℓ''} lem P =
    PT.rec (isPropLeastOf P) (λ { (a₀ , pa₀) → go a₀ (wf∙ a₀) pa₀ })
    where
    go : (a : A) → Acc _<∙_ a → ⟨ P a ⟩ → Σ[ m ∈ A ] IsLeast P m
    go a (acc rs) pa = decide (lem (Smaller , squash₁))
      where
      Smaller : Type (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))
      Smaller = ∥ Σ[ b ∈ A ] ((b <∙ a) × ⟨ P b ⟩) ∥₁
      decide : Smaller ⊎ (Smaller → Empty.⊥) → Σ[ m ∈ A ] IsLeast P m
      decide (inl q) = PT.rec (isPropLeastOf P)
        (λ { (b , (b<a , pb)) → go b (rs b b<a) pb }) q
      decide (inr ¬q) = a , (pa , λ b pb b<a → ¬q ∣ b , (b<a , pb) ∣₁)

Recap

SWO bundles a strict well-order, and leastOf extracts the least element of any non-empty subset, uniquely (isPropLeastOf). The bundle is the interface the choice construction takes; it does not care which order it is handed, which is why the chapter is generic. The excluded middle is spent once, on the decision at each descent step, and the level discipline (carrier and relation separately generic) is what will let the order of Part 4 compare small things by large data.