Subposets

module order-theory.subposets where
Imports
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import order-theory.posets
open import order-theory.preorders
open import order-theory.subpreorders

Idea

A subposet of a poset P is a subtype of P. By restriction of the ordering on P, subposets have again the structure of a poset.

Definitions

Subposets

module _
  {l1 l2 l3 : Level} (X : Poset l1 l2) (S : type-Poset X  Prop l3)
  where

  type-Subposet : UU (l1  l3)
  type-Subposet = type-Subpreorder (preorder-Poset X) S

  eq-type-Subposet :
    (x y : type-Subposet)  Id (pr1 x) (pr1 y)  Id x y
  eq-type-Subposet = eq-type-Subpreorder (preorder-Poset X) S

  leq-Subposet-Prop : (x y : type-Subposet)  Prop l2
  leq-Subposet-Prop = leq-Subpreorder-Prop (preorder-Poset X) S

  leq-Subposet : (x y : type-Subposet)  UU l2
  leq-Subposet = leq-Subpreorder (preorder-Poset X) S

  is-prop-leq-Subposet :
    (x y : type-Subposet)  is-prop (leq-Subposet x y)
  is-prop-leq-Subposet = is-prop-leq-Subpreorder (preorder-Poset X) S

  refl-leq-Subposet : (x : type-Subposet)  leq-Subposet x x
  refl-leq-Subposet = refl-leq-Subpreorder (preorder-Poset X) S

  transitive-leq-Subposet :
    (x y z : type-Subposet) 
    leq-Subposet y z  leq-Subposet x y  leq-Subposet x z
  transitive-leq-Subposet = transitive-leq-Subpreorder (preorder-Poset X) S

  antisymmetric-leq-Subposet :
    (x y : type-Subposet)  leq-Subposet x y  leq-Subposet y x  Id x y
  antisymmetric-leq-Subposet x y H K =
    eq-type-Subposet x y (antisymmetric-leq-Poset X (pr1 x) (pr1 y) H K)

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

  poset-Subposet : Poset (l1  l3) l2
  pr1 poset-Subposet = preorder-Subposet
  pr2 poset-Subposet = antisymmetric-leq-Subposet

Inclusion of sub-posets

module _
  {l1 l2 : Level} (X : Poset l1 l2)
  where

  module _
    {l3 l4 : Level} (S : type-Poset X  Prop l3)
    (T : type-Poset X  Prop l4)
    where

    inclusion-Subposet-Prop : Prop (l1  l3  l4)
    inclusion-Subposet-Prop =
      inclusion-Subpreorder-Prop (preorder-Poset X) S T

    inclusion-Subposet : UU (l1  l3  l4)
    inclusion-Subposet = inclusion-Subpreorder (preorder-Poset X) S T

    is-prop-inclusion-Subposet : is-prop inclusion-Subposet
    is-prop-inclusion-Subposet =
      is-prop-inclusion-Subpreorder (preorder-Poset X) S T

  refl-inclusion-Subposet :
    {l3 : Level} (S : type-Poset X  Prop l3) 
    inclusion-Subposet S S
  refl-inclusion-Subposet = refl-inclusion-Subpreorder (preorder-Poset X)

  transitive-inclusion-Subposet :
    {l3 l4 l5 : Level} (S : type-Poset X  Prop l3)
    (T : type-Poset X  Prop l4)
    (U : type-Poset X  Prop l5) 
    inclusion-Subposet T U  inclusion-Subposet S T 
    inclusion-Subposet S U
  transitive-inclusion-Subposet =
    transitive-inclusion-Subpreorder (preorder-Poset X)

  sub-poset-Preorder : (l : Level)  Preorder (l1  lsuc l) (l1  l)
  pr1 (sub-poset-Preorder l) = type-Poset X  Prop l
  pr1 (pr2 (sub-poset-Preorder l)) = inclusion-Subposet-Prop
  pr1 (pr2 (pr2 (sub-poset-Preorder l))) = refl-inclusion-Subposet
  pr2 (pr2 (pr2 (sub-poset-Preorder l))) = transitive-inclusion-Subposet