Ordinals

[finegeometer]

I got nerd-sniped into implementing ordinals. I hope this is useful!

This is my first time contributing to a project, so please tell me if I'm doing anything wrong.

There are a few things that bother me.

• I chose to include both the strict and nonstrict orders in the definition of ordinal, rather than deriving the latter from the former. This is useful, in that it allows the nonstrict order to definitionally equal a preexisting order. But I'm still not convinced it was the right choice. What do you think?
• I went into this with the intention to implement ordinals, and that's what I did. But some of the theory generalizes to extensional well-founded orders that need not be transitive. If we care to provide that generalization, that might force a rewrite.
• This implementation of ordinals isn't particularly conducive to providing an is-well-order predicate, since the underlying type is bundled deeply into the Ordinal structure.
• Naming things is always hard, and I don't know whether I did a good job.
• I chose to index ordinals by a single universe level, since that felt most natural. An alternative would have been to use two universe levels, analagous to Poset. I don't know which choice is better.

[Lavenza]

Pull request preview

New pages

• Order.Ordinal.Base (+670, -0)

Changed pages

• HoTT (+36, -0)
• 1Lab.Path.IdentitySystem (+12, -0)
• Data.Wellfounded.Properties (+8, -0)

[TOTBWF]

Thanks so much for the contribution! I'll split up the review a bit to not make it too overwhelming :)

First round is focused on some big-picture design questions, proof cleanup, some automation tips. I totally agree that packaging up both the strict and non-strict orders is a good idea, but I'm a bit unsure about bisimulations as a bespoke definition.

[TOTBWF]

We should be able to simplify this proof quite a bit by using Poset-path from https://1lab.dev/Order.Univalent.html#516

[TOTBWF]

I think the following API might be easier to use, as we don't need Equiv.to and Equiv.from everywhere, and we don't have to unpack pairs.

record is-simulation
  (α : Ordinal ℓ₁) (β : Ordinal ℓ₂)
  (f : ⌞ α ⌟ → ⌞ β ⌟) : Type (ℓ₁ ⊔ ℓ₂) where
  no-eta-equality
  private
    module α = Ordinal α
    module β = Ordinal β
  field
    pres-< : ∀ {x y} → x α.< y → f x β.< f y
    sim : ∀ {x y} → y β.< f x → ⌞ α ⌟
    simulates : ∀ {x y} → (y<fx : y β.< f x) → f (sim y<fx) ≡ y
    sim-< : ∀ {x y} → (y<fx : y β.< f x) → sim y<fx α.< x

  reflect-≤ :  ∀ {x y} → f x β.≤ f y → x α.≤ y
  reflect-≤ {x} {y} fx≤fy = go (α.<-wf x) (α.<-wf y) fx≤fy where
    go : ∀ {x y} → Acc α._<_ x → Acc α._<_ y → f x β.≤ f y → x α.≤ y
    go {x} {y} (acc hx) (acc hy) fx≤fy =
      Equiv.from α.≤-transforms-< λ {z} z<x →
        let fz<fy : f z β.< f y
            fz<fy = β.<-≤-trans (pres-< z<x) fx≤fy

            fy* : ⌞ α ⌟
            fy* = sim fz<fy

            fy*<y : fy* α.< y
            fy*<y = sim-< fz<fy

            fy*≡z : sim fz<fy ≡ z
            fy*≡z =
              α.≤-antisym
                (go (hy fy* fy*<y) (hx z z<x) (β.≤-refl' (simulates fz<fy)))
                (go (hx z z<x) (hy fy* fy*<y) (β.≤-refl' (sym (simulates fz<fy))))
        in subst (α._< y) fy*≡z fy*<y

  has-injective : injective f
  has-injective p = α.≤-antisym
    (reflect-≤ (β.≤-refl' p))
    (reflect-≤ (β.≤-refl' (sym p)))

  segment : (x : α.Ob) → ⌞ Subordinal α x ⌟ → ⌞ Subordinal β (f x) ⌟
  segment x (y , y<x) = f y , pres-< y<x

  segment-is-equiv : ∀ {x} → is-equiv (segment x)
  segment-is-equiv {x = x} .is-eqv (y , y<fx) .centre =
    (sim y<fx , sim-< y<fx) , Σ-prop-path! (simulates y<fx)
  segment-is-equiv {x = x} .is-eqv (y , y<fx) .paths ((z , z<x) , fz=y) =
    Σ-prop-path! $ Σ-prop-path! $ has-injective (simulates y<fx ∙ sym (ap fst fz=y))

[TOTBWF]

Seems like this could be nicer if we defined the strict order on ordinals using something like

record is-bounded-simulation
  (α : Ordinal ℓ₁) (β : Ordinal ℓ₂)
  (f : ⌞ α ⌟ → ⌞ β ⌟) : Type (ℓ₁ ⊔ ℓ₂)
  where
  no-eta-equality
  private
    module α = Ordinal α
    module β = Ordinal β
  field
    has-simulation : is-simulation α β f

  open is-simulation has-simulation public

  field
    bound : ⌞ β ⌟
    reflect : ∀ (x : ⌞ β ⌟) → x β.< bound → ⌞ α ⌟
    reflect-simulation : is-simulation (Subordinal β bound) α (uncurry reflect)

This gives us a bit more control over <ₒ→≤ₒ, as we are just dropping the bound.

[finegeometer]

Thank you!

I've followed most of your advice. The exceptions are as follows:

I'm not sure how I feel about defining bisimulation by hand like this. It does look like this is handy for bootstrapping the ordinal of ordinals, but it seems like a more natural move is to prove that ≤ₒ is antisymmetric without the intermediate notion.

This is what I tried originally. I got stuck on proving that if an equivalence is a simulation, then its inverse is also a simulation. It's provable, of course, but it felt like I was being forced to do too much at once, so I broke it up with this definition of _≃ₒ_.

Also, the definition of _≃ₒ_ is basically "strictly monotone isomorphism". If there was any preexisting theory about strict orders, then I'd think this concept would have already existed in the library.

We should be able to simplify this proof quite a bit by using Poset-path from https://1lab.dev/Order.Univalent.html#516

I tried that. The form in which Poset-path asks for the data was inconvenient enough that I went back to this method.

I think the following API might be easier to use... (referring to is-simulation)

Thanks for the suggestion, but when I tried it, I didn't like the resulting code.
What did help is adding sim, sim-<, and simulates as associated functions.

Seems like this could be nicer if we defined the strict order on ordinals...

I'm not convinced. Since I've already set up a decent API for working with Subordinal and _≃ₒ_, it's very convenient for _<ₒ_ to be constructed of them. This suggestion would force code working with _<ₒ_ to dig deeper into the implementation details of ordinals, rather than reusing preexisting functions.

---

Finally, you mention that you like the decision to package both the strict and non-strict orders into the definition of Ordinal. While I tend to agree (I wrote it this way for a reason!), I'd like to point out one issue you may not have considered.

When we define ordinal arithmetic, the strict order on α × β will be lexicographic: (x₁ , x₂) < (y₁ , y₂) iff x₂ < y₂ ∗ (x₁ < y₁ × x₂ ≤ y₂), where _∗_ is imported from Homotopy.Join. But there seems to only be a convenient expression for the non-strict order if we accept the law of excluded middle. So we seem to be stuck between two bad options: require LEM in the definition of α × β, or use an unpleasant definition of ≤.

If we did not bundle the non-strict order into Ordinal, then users would not be expecting _≤_ to be definitionally nice, so this would be less of a problem.

[TOTBWF]

Thanks for making the changes! That makes sense WRT _≃ₒ_, looks like that was wishful thinking on my end 😀 .

I can hack together something that uses Poset-path; it should be a few lines with declare-record-path, as that will take care of all of the is-prop->pathp calls for us.

I still do think that breaking up segment-is-equiv is a good idea though. The main reason is that the current definition
leads to really ugly goals. If sim shows up in a goal somewhere, agda is liable to print it as fst (equiv→inverse segment-is-equiv (_ , h)) which really makes things harder to read.

For the Lex order, Favonia has a trick that we used in agda-mugen that we can use. The idea is that you can extend an order on a poset with a conditional bit of data like so:

_≤[_]_ : ∀ (x : Ob) (K : Type r') (y : Ob) → Type (o ⊔ r ⊔ r')
x ≤[ K ] y = (x ≤ y) × (x ≡ y → K)

The non-strict lex order can neatly be defined using this:

_≤_ : ∀ (x y : ⌞ A ⌟ × ⌞ B ⌟) → Type (o ⊔ r ⊔ r')
(a1, b1) ≤ (a2, b2)  = a1 A.≤[ b1 B.≤ b2 ] a2

[finegeometer]

Responding to your comment about the lex order:

Theorem: If the strict order (x₁ , x₂) < (y₁ , y₂) ⇔ x₂ < y₂ ∨ (x₂ ≤ y₂ ∧ x₁ < y₁) and non-strict order (x₁ , x₂) ≤ (y₁ , y₂) ⇔ x₂ ≤ y₂ ∧ (x₂ ≡ y₂ → x₁ ≤ y₁) define an ordinal, then excluded middle holds.

Proof:

Observe that propositions form an ordinal, where P < Q ⇔ (¬ P ∧ Q) and P ≤ Q ⇔ (P → Q).

Now, for any proposition P, we have (⊥ , P) < (⊤ , P) ≤ (P , ⊤). By one of the rules relating the orders, we therefore have (⊥ , P) < (P , ⊤), which implies ¬ P ∨ P.

[anshwad10]

@finegeometer Have you taken a look at @LuuBluum 's formalization of ordinals in the cubical library? I noticed they define the strict order on the product a bit differently than you did. Regarding _≃ₒ_, I don't really see why it is necessary; Earlier I was formalizing ordinals in Arend and I was able to prove that ≤ of ordinals is antisymmetric just fine (here it is in a gist, may be hard to read if you don't know Arend though)