Subpreorders

module order-theory.subpreorders where

Imports

open import foundation.dependent-pair-types
open import foundation.functions
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import order-theory.preorders

Idea

A subpreorder of a preorder P is a subtype of P. By restriction of the ordering on P, the subpreorder inherits the structure of a preorder.

Definition

Subpreorders

Subpreorder :
  {l1 l2 : Level} (l3 : Level) → Preorder l1 l2 → UU (l1 ⊔ lsuc l3)
Subpreorder l3 P = subtype l3 (type-Preorder P)

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

  type-Subpreorder : UU (l1 ⊔ l3)
  type-Subpreorder = type-subtype S

  eq-type-Subpreorder :
    (x y : type-Subpreorder) → Id (pr1 x) (pr1 y) → Id x y
  eq-type-Subpreorder x y = eq-type-subtype S

  leq-Subpreorder-Prop : (x y : type-Subpreorder) → Prop l2
  leq-Subpreorder-Prop x y = leq-Preorder-Prop P (pr1 x) (pr1 y)

  leq-Subpreorder : (x y : type-Subpreorder) → UU l2
  leq-Subpreorder x y = type-Prop (leq-Subpreorder-Prop x y)

  is-prop-leq-Subpreorder :
    (x y : type-Subpreorder) → is-prop (leq-Subpreorder x y)
  is-prop-leq-Subpreorder x y =
    is-prop-type-Prop (leq-Subpreorder-Prop x y)

  refl-leq-Subpreorder : (x : type-Subpreorder) → leq-Subpreorder x x
  refl-leq-Subpreorder x = refl-leq-Preorder P (pr1 x)

  transitive-leq-Subpreorder :
    (x y z : type-Subpreorder) →
    leq-Subpreorder y z → leq-Subpreorder x y → leq-Subpreorder x z
  transitive-leq-Subpreorder x y z =
    transitive-leq-Preorder P (pr1 x) (pr1 y) (pr1 z)

  preorder-Subpreorder : Preorder (l1 ⊔ l3) l2
  pr1 preorder-Subpreorder = type-Subpreorder
  pr1 (pr2 preorder-Subpreorder) = leq-Subpreorder-Prop
  pr1 (pr2 (pr2 preorder-Subpreorder)) = refl-leq-Subpreorder
  pr2 (pr2 (pr2 preorder-Subpreorder)) = transitive-leq-Subpreorder

Inclusions of subpreorders

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

  module _
    {l3 l4 : Level} (S : type-Preorder P → Prop l3)
    (T : type-Preorder P → Prop l4)
    where

    inclusion-Subpreorder-Prop : Prop (l1 ⊔ l3 ⊔ l4)
    inclusion-Subpreorder-Prop =
      Π-Prop (type-Preorder P) (λ x → hom-Prop (S x) (T x))

    inclusion-Subpreorder : UU (l1 ⊔ l3 ⊔ l4)
    inclusion-Subpreorder = type-Prop inclusion-Subpreorder-Prop

    is-prop-inclusion-Subpreorder : is-prop inclusion-Subpreorder
    is-prop-inclusion-Subpreorder =
      is-prop-type-Prop inclusion-Subpreorder-Prop

  refl-inclusion-Subpreorder :
    {l3 : Level} (S : type-Preorder P → Prop l3) →
    inclusion-Subpreorder S S
  refl-inclusion-Subpreorder S x = id

  transitive-inclusion-Subpreorder :
    {l3 l4 l5 : Level} (S : type-Preorder P → Prop l3)
    (T : type-Preorder P → Prop l4)
    (U : type-Preorder P → Prop l5) →
    inclusion-Subpreorder T U → inclusion-Subpreorder S T →
    inclusion-Subpreorder S U
  transitive-inclusion-Subpreorder S T U g f x = (g x) ∘ (f x)

  Sub-Preorder : (l : Level) → Preorder (l1 ⊔ lsuc l) (l1 ⊔ l)
  pr1 (Sub-Preorder l) = type-Preorder P → Prop l
  pr1 (pr2 (Sub-Preorder l)) = inclusion-Subpreorder-Prop
  pr1 (pr2 (pr2 (Sub-Preorder l))) = refl-inclusion-Subpreorder
  pr2 (pr2 (pr2 (Sub-Preorder l))) = transitive-inclusion-Subpreorder