Order preserving maps on preorders

module order-theory.order-preserving-maps-preorders where
Imports
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtype-identity-principle
open import foundation.universe-levels

open import order-theory.preorders

Idea

A map f : P → Q between the underlying types of two preorders is said to be order preserving if x ≤ y in P implies f x ≤ f y in Q.

Definition

Order preserving maps

module _
  {l1 l2 l3 l4 : Level} (P : Preorder l1 l2) (Q : Preorder l3 l4)
  where

  preserves-order-Preorder-Prop :
    (type-Preorder P  type-Preorder Q)  Prop (l1  l2  l4)
  preserves-order-Preorder-Prop f =
    Π-Prop
      ( type-Preorder P)
      ( λ x 
        Π-Prop
          ( type-Preorder P)
          ( λ y 
            hom-Prop
              ( leq-Preorder-Prop P x y)
              ( leq-Preorder-Prop Q (f x) (f y))))

  preserves-order-Preorder :
    (type-Preorder P  type-Preorder Q)  UU (l1  l2  l4)
  preserves-order-Preorder f =
    type-Prop (preserves-order-Preorder-Prop f)

  is-prop-preserves-order-Preorder :
    (f : type-Preorder P  type-Preorder Q) 
    is-prop (preserves-order-Preorder f)
  is-prop-preserves-order-Preorder f =
    is-prop-type-Prop (preserves-order-Preorder-Prop f)

  type-hom-Preorder : UU (l1  l2  l3  l4)
  type-hom-Preorder =
    Σ (type-Preorder P  type-Preorder Q) preserves-order-Preorder

  map-hom-Preorder : type-hom-Preorder  type-Preorder P  type-Preorder Q
  map-hom-Preorder = pr1

  preserves-order-map-hom-Preorder :
    (f : type-hom-Preorder)  preserves-order-Preorder (map-hom-Preorder f)
  preserves-order-map-hom-Preorder = pr2

Homotopies of order preserving maps

module _
  {l1 l2 l3 l4 : Level} (P : Preorder l1 l2) (Q : Preorder l3 l4)
  where

  htpy-hom-Preorder : (f g : type-hom-Preorder P Q)  UU (l1  l3)
  htpy-hom-Preorder f g = map-hom-Preorder P Q f ~ map-hom-Preorder P Q g

  refl-htpy-hom-Preorder : (f : type-hom-Preorder P Q)  htpy-hom-Preorder f f
  refl-htpy-hom-Preorder f = refl-htpy

  htpy-eq-hom-Preorder :
    (f g : type-hom-Preorder P Q)  Id f g  htpy-hom-Preorder f g
  htpy-eq-hom-Preorder f .f refl = refl-htpy-hom-Preorder f

  is-contr-total-htpy-hom-Preorder :
    (f : type-hom-Preorder P Q) 
    is-contr (Σ (type-hom-Preorder P Q) (htpy-hom-Preorder f))
  is-contr-total-htpy-hom-Preorder f =
    is-contr-total-Eq-subtype
      ( is-contr-total-htpy (map-hom-Preorder P Q f))
      ( is-prop-preserves-order-Preorder P Q)
      ( map-hom-Preorder P Q f)
      ( refl-htpy)
      ( preserves-order-map-hom-Preorder P Q f)

  is-equiv-htpy-eq-hom-Preorder :
    (f g : type-hom-Preorder P Q)  is-equiv (htpy-eq-hom-Preorder f g)
  is-equiv-htpy-eq-hom-Preorder f =
    fundamental-theorem-id
      ( is-contr-total-htpy-hom-Preorder f)
      ( htpy-eq-hom-Preorder f)

  extensionality-hom-Preorder :
    (f g : type-hom-Preorder P Q)  Id f g  htpy-hom-Preorder f g
  pr1 (extensionality-hom-Preorder f g) = htpy-eq-hom-Preorder f g
  pr2 (extensionality-hom-Preorder f g) = is-equiv-htpy-eq-hom-Preorder f g

  eq-htpy-hom-Preorder :
    (f g : type-hom-Preorder P Q)  htpy-hom-Preorder f g  Id f g
  eq-htpy-hom-Preorder f g =
    map-inv-is-equiv (is-equiv-htpy-eq-hom-Preorder f g)

The identity order preserving map

module _
  {l1 l2 : Level} (P : Preorder l1 l2)
  where

  preserves-order-id-Preorder :
    preserves-order-Preorder P P (id {A = type-Preorder P})
  preserves-order-id-Preorder x y = id

  id-hom-Preorder : type-hom-Preorder P P
  pr1 id-hom-Preorder = id
  pr2 id-hom-Preorder = preserves-order-id-Preorder

Composing order preserving maps

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  (P : Preorder l1 l2) (Q : Preorder l3 l4) (R : Preorder l5 l6)
  where

  preserves-order-comp-Preorder :
    (g : type-hom-Preorder Q R) (f : type-hom-Preorder P Q) 
    preserves-order-Preorder P R
      ( map-hom-Preorder Q R g  map-hom-Preorder P Q f)
  preserves-order-comp-Preorder g f x y H =
    preserves-order-map-hom-Preorder Q R g
      ( map-hom-Preorder P Q f x)
      ( map-hom-Preorder P Q f y)
      ( preserves-order-map-hom-Preorder P Q f x y H)

  comp-hom-Preorder :
    (g : type-hom-Preorder Q R) (f : type-hom-Preorder P Q) 
    type-hom-Preorder P R
  pr1 (comp-hom-Preorder g f) =
     map-hom-Preorder Q R g  map-hom-Preorder P Q f
  pr2 (comp-hom-Preorder g f) =
    preserves-order-comp-Preorder g f

Unit laws for composition of order preserving maps

module _
  {l1 l2 l3 l4 : Level} (P : Preorder l1 l2) (Q : Preorder l3 l4)
  where

  left-unit-law-comp-hom-Preorder :
    (f : type-hom-Preorder P Q) 
    Id ( comp-hom-Preorder P Q Q (id-hom-Preorder Q) f) f
  left-unit-law-comp-hom-Preorder f =
    eq-htpy-hom-Preorder P Q
      ( comp-hom-Preorder P Q Q (id-hom-Preorder Q) f)
      ( f)
      ( refl-htpy)

  right-unit-law-comp-hom-Preorder :
    (f : type-hom-Preorder P Q) 
    Id (comp-hom-Preorder P P Q f (id-hom-Preorder P)) f
  right-unit-law-comp-hom-Preorder f =
    eq-htpy-hom-Preorder P Q
      ( comp-hom-Preorder P P Q f (id-hom-Preorder P))
      ( f)
      ( refl-htpy)

Associativity of composition of order preserving maps

module _
  {l1 l2 l3 l4 l5 l6 l7 l8 : Level} (P : Preorder l1 l2) (Q : Preorder l3 l4)
  (R : Preorder l5 l6) (S : Preorder l7 l8)
  (h : type-hom-Preorder R S)
  (g : type-hom-Preorder Q R)
  (f : type-hom-Preorder P Q)
  where

  associative-comp-hom-Preorder :
    Id ( comp-hom-Preorder P Q S (comp-hom-Preorder Q R S h g) f)
       ( comp-hom-Preorder P R S h (comp-hom-Preorder P Q R g f))
  associative-comp-hom-Preorder =
    eq-htpy-hom-Preorder P S
      ( comp-hom-Preorder P Q S (comp-hom-Preorder Q R S h g) f)
      ( comp-hom-Preorder P R S h (comp-hom-Preorder P Q R g f))
      ( refl-htpy)