Ordinals as a quotient inductive-inductive type

This module is the foundation of the library. It defines the type Ord of ordinals — Brouwer trees — as a quotient inductive-inductive type (QIIT), mutually with its order _≤_, following Kraus, Nordvall Forsberg and Xu, Type-Theoretic Approaches to Ordinals. It also derives the two eliminators (elimProp, ≤-elimProp) that every later module is built from, and the basic order lemmas.

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

module QIITOrd.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Path
open import Cubical.Data.Nat as ℕ using (ℕ)
open import Cubical.Data.Sigma
open import Cubical.Relation.Nullary using (¬_)
open import Cubical.Relation.Binary.Base using (Rel; module BinaryRelation)
open BinaryRelation using (isRefl'; isTrans')

We reuse the cubical library’s binary-relation vocabulary: Rel A B ℓ is the type of ℓ-valued relations, and BinaryRelation’s isRefl' / isTrans' are the (implicit-argument) reflexivity and transitivity predicates. We only ever need homogeneous relations Rel A A ℓ.

Sequences and bisimulation

A limit ordinal is built from a sequence ℕ → A. Two such sequences should give the same limit exactly when they are mutually cofinal — they bisimulate. f ≼ g says every f n is dominated by some g m (the existence is a propositional truncation ∃), and f ≈ g is bisimilarity: f ≼ g and g ≼ f. This is stated generally for any relation _≤_, so the same definitions serve both the order on ordinals and, later, the order on order-codes.

module Bisimulation {ℓ ℓ'} {A : Type ℓ} (_≤_ : Rel A A ℓ') where
  private Seq = ℕ → A

  _≼⟨_⟩_ : Seq → ℕ → Seq → Type _
  f ≼⟨ n ⟩ g = ∃[ m ∈ ℕ ] f n ≤ g m

  _≼_ : Rel Seq Seq _
  f ≼ g = ∀ n → f ≼⟨ n ⟩ g

  _≈_ : Rel Seq Seq _
  f ≈ g = f ≼ g × g ≼ f

A sequence is monotone when suc (f n) ≤ f (suc n), i.e. it strictly increases. A MonoSeq bundles a sequence with that proof, and f [ n ] projects out its n-th term. Limits will be taken only of monotone sequences.

module MonotonicSequence {ℓ ℓ'} {A : Type ℓ} (suc : A → A) (_≤_ : Rel A A ℓ') where
  private Seq = ℕ → A

  isMonoSeq : Seq → Type _
  isMonoSeq f = ∀ n → suc (f n) ≤ f (ℕ.suc n)

  MonoSeq : Type _
  MonoSeq = Σ[ f ∈ Seq ] isMonoSeq f

  infix  _[_]
  _[_] : MonoSeq → ℕ → A
  f [ n ] = fst f n

The QIIT definition

Ord and _≤_ are declared mutually: _≤_ already appears in the type of lim (through MonoSeq), and Ord appears in the type of _≤_. We first forward-declare both, plus a private copy pre-suc of the successor (needed to instantiate MonotonicSequence before suc itself is in scope), then open the two helper modules at _≤_ so that MonoSeq, _≼_, ≈, _[_] are available.

data Ord : Type
data _≤_ : Rel Ord Ord ℓ-zero
private pre-suc : Ord → Ord

open Bisimulation _≤_ public
open MonotonicSequence pre-suc _≤_ public

variable
  α β γ : Ord
  f g h : MonoSeq
  n : ℕ

Ord has the three ordinal formers — zero, suc, and lim of a monotone sequence — and two higher constructors that make it a QIIT: l≡l quotients bisimilar limits to be equal (the path constructor), and isSetOrd truncates Ord to a set, so all of its path structure is determined by these.

data Ord where
  zero     : Ord
  suc      : Ord → Ord
  lim      : MonoSeq → Ord
  l≡l      : fst f ≈ fst g → lim f ≡ lim g
  isSetOrd : isSet Ord

The order _≤_ is generated by: zero is least (z≤); suc is monotone (s≤s); lim f is an upper bound of its sequence and the least one (≤l and l≤); together with transitivity and the proof that _≤_ is propositional. The last two are constructors because _≤_ is defined simultaneously with Ord, so we cannot derive them after the fact.

data _≤_ where
  z≤      : zero ≤ α
  s≤s     : α ≤ β → suc α ≤ suc β
  ≤l      : α ≤ f [ n ] → α ≤ lim f
  l≤      : (∀ n → f [ n ] ≤ α) → lim f ≤ α
  ≤-trans : isTrans' _≤_
  isProp≤ : isProp (α ≤ β)

pre-suc = suc

This completes the QIIT.

Transfinite induction into propositions

The work-horse recursor elimProp is structural recursion on Ord into a proposition-valued family P. Because each P α is a proposition, the two higher constructors are discharged automatically: the l≡l case by isProp→PathP and the isSetOrd case by isProp→SquareP. The user only supplies the zero/suc/lim methods — and in the lim method the inductive hypothesis arrives already unpacked as ∀ n → P (f [ n ]). This unpacking is what later lets transitivity of the order-code be defined structurally.

elimProp : ∀ {ℓ} {P : Ord → Type ℓ} →
  (∀ α → isProp (P α)) →
  P zero →
  (∀ {α} → P α → P (suc α)) →
  (∀ {f} → (∀ n → P (f [ n ])) → P (lim f)) →
  (α : Ord) → P α
elimProp Pprop Pz Ps Pl zero    = Pz
elimProp Pprop Pz Ps Pl (suc α) = Ps (elimProp Pprop Pz Ps Pl α)
elimProp Pprop Pz Ps Pl (lim f) = Pl λ n → elimProp Pprop Pz Ps Pl (fst f n)
elimProp Pprop Pz Ps Pl (l≡l {f} {g} f≈g i) = isProp→PathP
  (λ j → Pprop (l≡l f≈g j))
  (Pl λ n → elimProp Pprop Pz Ps Pl (fst f n))
  (Pl λ n → elimProp Pprop Pz Ps Pl (fst g n)) i
elimProp Pprop Pz Ps Pl (isSetOrd _ _ p q i j) = isProp→SquareP
  (λ i j → Pprop $ isSetOrd _ _ _ _ i j) refl refl
  (λ i → elimProp Pprop Pz Ps Pl (p i))
  (λ i → elimProp Pprop Pz Ps Pl (q i)) i j

Dually, ≤-elimProp is structural recursion on a derivation of α ≤ β into a proposition-valued family. Its l≤ method is the subtle one: it supplies, in addition to the induction hypotheses on the proofs f [ n ] ≤ α, the sequence’s monotonicity hypotheses ∀ n → P (snd f n). That extra hypothesis is exactly what encode≤ needs later, and is why a plain “induction on the derivation” is not enough.

≤-elimProp : ∀ {ℓ} {P : ∀ {α β} → α ≤ β → Type ℓ} →
  (∀ {α β} (α≤β : α ≤ β) → isProp (P α≤β)) →
  (∀ {α} → P (z≤ {α})) →
  (∀ {α β} (α≤β : α ≤ β) → P α≤β → P (s≤s α≤β)) →
  (∀ {α f n} (α≤f : α ≤ f [ n ]) → P α≤f → P (≤l {f = f} α≤f)) →
  (∀ {f α} (f≤α : ∀ n → f [ n ] ≤ α) → (∀ n → P (f≤α n)) → (∀ n → P (snd f n)) → P (l≤ {f} f≤α)) →
  (∀ {α β γ} {α≤β : α ≤ β} {β≤γ : β ≤ γ} → P α≤β → P β≤γ → P (≤-trans α≤β β≤γ)) →
  (α≤β : α ≤ β) → P α≤β
≤-elimProp Pprop Pz Ps Pu Pl Pt z≤          = Pz
≤-elimProp Pprop Pz Ps Pu Pl Pt (s≤s α≤β)   = Ps α≤β $ ≤-elimProp Pprop Pz Ps Pu Pl Pt α≤β
≤-elimProp Pprop Pz Ps Pu Pl Pt (≤l α≤f)    = Pu α≤f $ ≤-elimProp Pprop Pz Ps Pu Pl Pt α≤f
≤-elimProp Pprop Pz Ps Pu Pl Pt (l≤ {f} f≤) = Pl f≤
  (λ n → ≤-elimProp Pprop Pz Ps Pu Pl Pt (f≤ n))
  (λ n → ≤-elimProp Pprop Pz Ps Pu Pl Pt (snd f n))
≤-elimProp Pprop Pz Ps Pu Pl Pt (≤-trans α≤β β≤γ) = Pt
  (≤-elimProp Pprop Pz Ps Pu Pl Pt α≤β)
  (≤-elimProp Pprop Pz Ps Pu Pl Pt β≤γ)
≤-elimProp Pprop Pz Ps Pu Pl Pt (isProp≤ α≤β β≤γ i) = isProp→PathP
  (λ i → Pprop (isProp≤ α≤β β≤γ i))
  (≤-elimProp Pprop Pz Ps Pu Pl Pt α≤β)
  (≤-elimProp Pprop Pz Ps Pu Pl Pt β≤γ) i

Derived order notations

The strict order is α < β := suc α ≤ β, and we set up the usual negated and flipped notations, plus a couple of small numerals.

Seq = ℕ → Ord
one = suc zero
two = suc one

_≢_ : Rel Ord Ord _
α ≢ β = ¬ α ≡ β

_≥_ : Rel Ord Ord _
α ≥ β = β ≤ α

_≰_ : Rel Ord Ord _
α ≰ β = ¬ α ≤ β

_≱_ : Rel Ord Ord _
α ≱ β = ¬ β ≤ α

_<_ : Rel Ord Ord _
α < β = suc α ≤ β

_>_ : Rel Ord Ord _
α > β = β < α

_≮_ : Rel Ord Ord _
α ≮ β = ¬ α < β

_≯_ : Rel Ord Ord _
α ≯ β = ¬ β < α

Basic order properties

Reflexivity is the first real use of elimProp: it follows the constructors, with the limit case combining l≤ and ≤l. From it we get that equal ordinals are related, that every sequence element is ≤ its limit (f≤l, the upper-bound property as a closed term), and the one inversion that needs no encode-decode: from lim f ≤ α we read back f [ n ] ≤ α just by transitivity with f≤l.

≤-refl : isRefl' _≤_
≤-refl = elimProp (λ α → isProp≤ {α} {α}) z≤ s≤s (λ ih → l≤ λ n → ≤l (ih n)) _

≡⇒≤ : α ≡ β → α ≤ β
≡⇒≤ α≡β = subst (_≤ _) (sym α≡β) ≤-refl

f≤l : f [ n ] ≤ lim f
f≤l = ≤l ≤-refl

l≤-inv : lim f ≤ α → ∀ n → f [ n ] ≤ α
l≤-inv l≤α n = ≤-trans f≤l l≤α

≤-reasoning

Equational-style reasoning combinators for chaining ≤, <, and ≡ steps; these make the limit proofs below (and throughout the library) readable.

infixr  _≤⟨_⟩_ _<⟨_⟩_ _<⟨_⟩suc_ _=⟨_⟩_ _=˘⟨_⟩_
infix   _≤∎

_≤⟨_⟩_ : (α : Ord) → α ≤ β → β ≤ γ → α ≤ γ
_≤⟨_⟩_ _ = ≤-trans

_<⟨_⟩_ : (α : Ord) → α < β → β ≤ γ → α < γ
_<⟨_⟩_ _ = ≤-trans

_<⟨_⟩suc_ : (α : Ord) → α < β → β ≤ γ → α < γ
_<⟨_⟩suc_ = _<⟨_⟩_

_=⟨_⟩_ : (α : Ord) → α ≡ β → β ≤ γ → α ≤ γ
α =⟨ α≡β ⟩ β≤γ = subst (_≤ _) (sym α≡β) β≤γ

_=˘⟨_⟩_ : (α : Ord) → β ≡ α → β ≤ γ → α ≤ γ
α =˘⟨ β≡α ⟩ β≤γ = subst (_≤ _) β≡α β≤γ

_≤∎ : ∀ α → α ≤ α
_ ≤∎ = ≤-refl

Finally, α ≤ suc α (again by elimProp, the limit case using the reasoning combinators), and the two evident relations between α ≤ β and the successor.

≤s : α ≤ suc α
≤s = elimProp (λ α → isProp≤ {α} {suc α}) z≤ s≤s
  (λ {f} f≤sf → l≤ λ n →
    f [ n ]       ≤⟨ f≤sf n ⟩
    suc (f [ n ]) ≤⟨ s≤s f≤l ⟩
    suc (lim f)   ≤∎) _

s≤→≤ : suc α ≤ β → α ≤ β
s≤→≤ = ≤-trans ≤s

≤→≤s : α ≤ β → α ≤ suc β
≤→≤s α≤β = ≤-trans α≤β ≤s