Closed interval preserving maps between posets

Content created by Louis Wasserman.

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

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

open import order-theory.closed-intervals-posets
open import order-theory.posets

Idea

A map between posets f : X → Y is closed interval preserving if the image of a closed interval in X is always a closed interval in Y.

Definition

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

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

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

Recent changes