Closed interval preserving maps between total orders

Content created by Louis Wasserman.

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

module order-theory.closed-interval-preserving-maps-total-orders where
Imports 
open import foundation.images-subtypes
open import foundation.propositions
open import foundation.universe-levels

open import order-theory.closed-interval-preserving-maps-posets
open import order-theory.closed-intervals-total-orders
open import order-theory.total-orders

Idea

A map between total orders f : X → Y is closed interval preserving if the image of a closed interval in X is always a closed interval in Y. Equivalently, it is a closed interval preserving map on the underlying posets.

Definition

module _
  {l1 l2 l3 l4 : Level} (X : Total-Order l1 l2) (Y : Total-Order l3 l4)
  (f : type-Total-Order X → type-Total-Order Y)
  where

  is-closed-interval-map-prop-Total-Order :
    ([a,b] : closed-interval-Total-Order X) →
    ([c,d] : closed-interval-Total-Order Y) →
    Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  is-closed-interval-map-prop-Total-Order =
    is-closed-interval-map-prop-Poset
      ( poset-Total-Order X)
      ( poset-Total-Order Y)
      ( f)

  is-closed-interval-map-Total-Order :
    ([a,b] : closed-interval-Total-Order X) →
    ([c,d] : closed-interval-Total-Order Y) →
    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  is-closed-interval-map-Total-Order [a,b] [c,d] =
    type-Prop (is-closed-interval-map-prop-Total-Order [a,b] [c,d])

Recent changes