Strict orders

Content created by Fredrik Bakke.

Created on 2025-05-02.
Last modified on 2025-05-02.

module order-theory.strict-orders where
Imports 
open import foundation.binary-relations
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalence-relations
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.negation
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import order-theory.similarity-of-elements-strict-preorders
open import order-theory.strict-preorders
open import order-theory.strictly-preordered-sets

Idea

A strict order is a strict preorder satisfying the extensionality principle that similar elements are equal. More concretely, if and are such that for every , we have

then .

The extensionality principle of strict orders is slightly different to that of ordinals. For ordinals, elements are equal already if they are similar from below. Namely, only the first of the two conditions above must be satisfied in order for two elements to be equal.

The extensionality principle of strict orders can be recovered as a special case of the extensionality principle of semicategories as considered in Example 8.16 of The Univalence Principle [ANST25].

Definitions

The extensionality principle of strict orders

extensionality-principle-Strict-Preorder :
  {l1 l2 : Level} → Strict-Preorder l1 l2 → UU (l1 ⊔ l2)
extensionality-principle-Strict-Preorder P =
  (x y : type-Strict-Preorder P) → sim-Strict-Preorder P x y → x ＝ y

The type of strict orders

Strict-Order : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Strict-Order l1 l2 =
  Σ (Strict-Preorder l1 l2) (extensionality-principle-Strict-Preorder)

module _
  {l1 l2 : Level} (A : Strict-Order l1 l2)
  where

  strict-preorder-Strict-Order : Strict-Preorder l1 l2
  strict-preorder-Strict-Order = pr1 A

  extensionality-Strict-Order :
    extensionality-principle-Strict-Preorder strict-preorder-Strict-Order
  extensionality-Strict-Order = pr2 A

  type-Strict-Order : UU l1
  type-Strict-Order = type-Strict-Preorder strict-preorder-Strict-Order

  le-Strict-Order : type-Strict-Order → type-Strict-Order → UU l2
  le-Strict-Order = le-Strict-Preorder strict-preorder-Strict-Order

  is-prop-le-Strict-Order :
    (x y : type-Strict-Order) → is-prop (le-Strict-Order x y)
  is-prop-le-Strict-Order =
    is-prop-le-Strict-Preorder strict-preorder-Strict-Order

  le-prop-Strict-Order : type-Strict-Order → type-Strict-Order → Prop l2
  le-prop-Strict-Order = le-prop-Strict-Preorder strict-preorder-Strict-Order

  is-irreflexive-le-Strict-Order : is-irreflexive le-Strict-Order
  is-irreflexive-le-Strict-Order =
    is-irreflexive-le-Strict-Preorder strict-preorder-Strict-Order

  is-transitive-le-Strict-Order : is-transitive le-Strict-Order
  is-transitive-le-Strict-Order =
    is-transitive-le-Strict-Preorder strict-preorder-Strict-Order

Properties

The ordering of a strict order is antisymmetric

module _
  {l1 l2 : Level} (A : Strict-Order l1 l2)
  where

  is-antisymmetric-le-Strict-Order : is-antisymmetric (le-Strict-Order A)
  is-antisymmetric-le-Strict-Order =
    is-antisymmetric-le-Strict-Preorder (strict-preorder-Strict-Order A)

Strict orders are sets

module _
  {l1 l2 : Level} (A : Strict-Order l1 l2)
  where

  is-set-type-Strict-Order : is-set (type-Strict-Order A)
  is-set-type-Strict-Order =
    is-set-prop-in-id
      ( sim-Strict-Preorder (strict-preorder-Strict-Order A))
      ( is-prop-sim-Strict-Preorder (strict-preorder-Strict-Order A))
      ( refl-sim-Strict-Preorder (strict-preorder-Strict-Order A))
      ( extensionality-Strict-Order A)

  set-Strict-Order : Set l1
  set-Strict-Order = (type-Strict-Order A , is-set-type-Strict-Order)

  strictly-preordered-set-Strict-Order : Strictly-Preordered-Set l1 l2
  strictly-preordered-set-Strict-Order =
    make-Strictly-Preordered-Set
      ( strict-preorder-Strict-Order A)
      ( is-set-type-Strict-Order)

The extensionality principle is a proposition

module _
  {l1 l2 : Level} (A : Strict-Preorder l1 l2)
  where

  abstract
    is-proof-irrelevant-extensionality-principle-Strict-Preorder :
      is-proof-irrelevant (extensionality-principle-Strict-Preorder A)
    is-proof-irrelevant-extensionality-principle-Strict-Preorder H =
      ( H ,
        ( λ K →
          eq-htpy
            ( λ x →
              eq-htpy
                ( λ y →
                  eq-htpy
                    ( λ _ →
                      eq-is-prop (is-set-type-Strict-Order (A , H) x y))))))

  is-prop-extensionality-principle-Strict-Preorder :
      is-prop (extensionality-principle-Strict-Preorder A)
  is-prop-extensionality-principle-Strict-Preorder =
    is-prop-is-proof-irrelevant
      ( is-proof-irrelevant-extensionality-principle-Strict-Preorder)

  extensionality-principle-prop-Strict-Preorder : Prop (l1 ⊔ l2)
  extensionality-principle-prop-Strict-Preorder =
    ( extensionality-principle-Strict-Preorder A ,
      is-prop-extensionality-principle-Strict-Preorder)

References

[ANST25]
Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis. The univalence principle. Mem. Amer. Math. Soc., 305(1541):vii+175, 2025. arXiv:2102.06275, doi:10.1090/memo/1541.

See also

Recent changes