Finitely graded posets

module order-theory.finitely-graded-posets where
Imports
open import elementary-number-theory.inequality-standard-finite-types
open import elementary-number-theory.modular-arithmetic
open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equality-dependent-pair-types
open import foundation.functions
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import order-theory.bottom-elements-posets
open import order-theory.posets
open import order-theory.preorders
open import order-theory.top-elements-posets
open import order-theory.total-orders

open import univalent-combinatorics.standard-finite-types

Idea

A finitely graded poset consists of a family of types indexed by Fin (succ-ℕ k) equipped with an ordering relation from Fin (inl i) to Fin (succ-Fin (inl i)) for each i : Fin k.

Finitely-Graded-Poset : (l1 l2 : Level) (k : )  UU (lsuc l1  lsuc l2)
Finitely-Graded-Poset l1 l2 k =
  Σ ( Fin (succ-ℕ k)  Set l1)
    ( λ X 
      (i : Fin k)  type-Set (X (inl-Fin k i)) 
      type-Set (X (succ-Fin (succ-ℕ k) (inl-Fin k i)))  Prop l2)

module _
  {l1 l2 : Level} {k : } (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    (i : Fin (succ-ℕ k))
    where

    face-Finitely-Graded-Poset-Set : Set l1
    face-Finitely-Graded-Poset-Set = pr1 X i

    face-Finitely-Graded-Poset : UU l1
    face-Finitely-Graded-Poset =
      type-Set face-Finitely-Graded-Poset-Set

    is-set-face-Finitely-Graded-Poset :
      is-set face-Finitely-Graded-Poset
    is-set-face-Finitely-Graded-Poset =
      is-set-type-Set face-Finitely-Graded-Poset-Set

  module _
    (i : Fin k) (y : face-Finitely-Graded-Poset (inl-Fin k i))
    (z : face-Finitely-Graded-Poset (succ-Fin (succ-ℕ k) (inl-Fin k i)))
    where

    adjacent-Finitely-Graded-Poset-Prop : Prop l2
    adjacent-Finitely-Graded-Poset-Prop = pr2 X i y z

    adjacent-Finitely-Graded-Poset : UU l2
    adjacent-Finitely-Graded-Poset =
      type-Prop adjacent-Finitely-Graded-Poset-Prop

    is-prop-adjacent-Finitely-Graded-Poset :
      is-prop adjacent-Finitely-Graded-Poset
    is-prop-adjacent-Finitely-Graded-Poset =
      is-prop-type-Prop adjacent-Finitely-Graded-Poset-Prop

  set-Finitely-Graded-Poset : Set l1
  set-Finitely-Graded-Poset =
    Σ-Set (Fin-Set (succ-ℕ k)) face-Finitely-Graded-Poset-Set

  type-Finitely-Graded-Poset : UU l1
  type-Finitely-Graded-Poset = type-Set set-Finitely-Graded-Poset

  is-set-type-Finitely-Graded-Poset : is-set type-Finitely-Graded-Poset
  is-set-type-Finitely-Graded-Poset =
    is-set-type-Set set-Finitely-Graded-Poset

  element-face-Finitely-Graded-Poset :
    {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset i 
    type-Finitely-Graded-Poset
  element-face-Finitely-Graded-Poset {i} x = pair i x

  shape-Finitely-Graded-Poset :
    type-Finitely-Graded-Poset  Fin (succ-ℕ k)
  shape-Finitely-Graded-Poset (pair i x) = i

  face-type-Finitely-Graded-Poset :
    (x : type-Finitely-Graded-Poset) 
    face-Finitely-Graded-Poset (shape-Finitely-Graded-Poset x)
  face-type-Finitely-Graded-Poset (pair i x) = x

  module _
    {i : Fin (succ-ℕ k)} (x : face-Finitely-Graded-Poset i)
    where

If chains with jumps are never used, we'd like to call the following chains.

    data
      path-faces-Finitely-Graded-Poset :
        {j : Fin (succ-ℕ k)} (y : face-Finitely-Graded-Poset j) 
        UU (l1  l2)
        where
        refl-path-faces-Finitely-Graded-Poset :
          path-faces-Finitely-Graded-Poset x
        cons-path-faces-Finitely-Graded-Poset :
          {j : Fin k} {y : face-Finitely-Graded-Poset (inl-Fin k j)}
          {z : face-Finitely-Graded-Poset (succ-Fin (succ-ℕ k) (inl-Fin k j))} 
          adjacent-Finitely-Graded-Poset j y z 
          path-faces-Finitely-Graded-Poset y 
          path-faces-Finitely-Graded-Poset z

  tr-refl-path-faces-Finitely-Graded-Poset :
    {i j : Fin (succ-ℕ k)} (p : Id j i) (x : face-Finitely-Graded-Poset j) 
    path-faces-Finitely-Graded-Poset
      ( tr face-Finitely-Graded-Poset p x)
      ( x)
  tr-refl-path-faces-Finitely-Graded-Poset refl x =
    refl-path-faces-Finitely-Graded-Poset

  concat-path-faces-Finitely-Graded-Poset :
    {i1 i2 i3 : Fin (succ-ℕ k)}
    {x : face-Finitely-Graded-Poset i1}
    {y : face-Finitely-Graded-Poset i2}
    {z : face-Finitely-Graded-Poset i3} 
    path-faces-Finitely-Graded-Poset y z 
    path-faces-Finitely-Graded-Poset x y 
    path-faces-Finitely-Graded-Poset x z
  concat-path-faces-Finitely-Graded-Poset
    refl-path-faces-Finitely-Graded-Poset K = K
  concat-path-faces-Finitely-Graded-Poset
    ( cons-path-faces-Finitely-Graded-Poset x H) K =
    cons-path-faces-Finitely-Graded-Poset x
      ( concat-path-faces-Finitely-Graded-Poset H K)

  path-elements-Finitely-Graded-Poset :
    (x y : type-Finitely-Graded-Poset)  UU (l1  l2)
  path-elements-Finitely-Graded-Poset (pair i x) (pair j y) =
    path-faces-Finitely-Graded-Poset x y

  refl-path-elements-Finitely-Graded-Poset :
    (x : type-Finitely-Graded-Poset) 
    path-elements-Finitely-Graded-Poset x x
  refl-path-elements-Finitely-Graded-Poset x =
    refl-path-faces-Finitely-Graded-Poset

  concat-path-elements-Finitely-Graded-Poset :
    (x y z : type-Finitely-Graded-Poset) 
    path-elements-Finitely-Graded-Poset y z 
    path-elements-Finitely-Graded-Poset x y 
    path-elements-Finitely-Graded-Poset x z
  concat-path-elements-Finitely-Graded-Poset x y z =
    concat-path-faces-Finitely-Graded-Poset

  leq-type-path-faces-Finitely-Graded-Poset :
    {i1 i2 : Fin (succ-ℕ k)} (x : face-Finitely-Graded-Poset i1)
    (y : face-Finitely-Graded-Poset i2) 
    path-faces-Finitely-Graded-Poset x y  leq-Fin (succ-ℕ k) i1 i2
  leq-type-path-faces-Finitely-Graded-Poset {i1} x .x
    refl-path-faces-Finitely-Graded-Poset = refl-leq-Fin (succ-ℕ k) i1
  leq-type-path-faces-Finitely-Graded-Poset {i1} x y
    ( cons-path-faces-Finitely-Graded-Poset {i3} {z} H K) =
     transitive-leq-Fin
       ( succ-ℕ k)
       ( i1)
       ( inl-Fin k i3)
       ( succ-Fin (succ-ℕ k) (inl-Fin k i3))
       ( leq-succ-Fin k i3)
       ( leq-type-path-faces-Finitely-Graded-Poset x z K)

Antisymmetry of path-elements-Finitely-Graded-Poset

eq-path-elements-Finitely-Graded-Poset :
  {l1 l2 : Level} {k : } (X : Finitely-Graded-Poset l1 l2 k)
  (x y : type-Finitely-Graded-Poset X) 
  (p : Id (shape-Finitely-Graded-Poset X x)
          (shape-Finitely-Graded-Poset X y)) 
  path-elements-Finitely-Graded-Poset X x y  Id x y
eq-path-elements-Finitely-Graded-Poset {k} X (pair i1 x) (pair .i1 .x) p
  refl-path-faces-Finitely-Graded-Poset = refl
eq-path-elements-Finitely-Graded-Poset {k = succ-ℕ k} X (pair i1 x)
  (pair .(succ-Fin (succ-ℕ (succ-ℕ k)) (inl-Fin (succ-ℕ k) i2)) y) p
  (cons-path-faces-Finitely-Graded-Poset {i2} {z} H K) =
  ex-falso
    ( has-no-fixed-points-succ-Fin
      { succ-ℕ (succ-ℕ k)}
      ( inl-Fin (succ-ℕ k) i2)
      ( λ (q : is-one-ℕ (succ-ℕ (succ-ℕ k))) 
        is-nonzero-succ-ℕ k (is-injective-succ-ℕ q))
      ( antisymmetric-leq-Fin
        ( succ-ℕ (succ-ℕ k))
        ( succ-Fin (succ-ℕ (succ-ℕ k)) (inl-Fin (succ-ℕ k) i2))
        ( inl-Fin (succ-ℕ k) i2)
        ( transitive-leq-Fin
          ( succ-ℕ (succ-ℕ k))
          ( skip-zero-Fin (succ-ℕ k) i2)
          ( i1)
          ( inl i2)
          ( leq-type-path-faces-Finitely-Graded-Poset X x z K)
          ( tr
            ( leq-Fin
              ( succ-ℕ (succ-ℕ k))
              ( succ-Fin (succ-ℕ (succ-ℕ k)) (inl-Fin (succ-ℕ k) i2)))
            ( inv p)
            ( refl-leq-Fin
              ( succ-ℕ (succ-ℕ k))
              ( succ-Fin (succ-ℕ (succ-ℕ k)) (inl-Fin (succ-ℕ k) i2)))))
        ( leq-succ-Fin (succ-ℕ k) i2)))

module _
  {l1 l2 : Level} {k : } (X : Finitely-Graded-Poset l1 l2 k)
  where

  abstract
    eq-path-faces-Finitely-Graded-Poset :
      {i : Fin (succ-ℕ k)} (x y : face-Finitely-Graded-Poset X i) 
      path-faces-Finitely-Graded-Poset X x y  Id x y
    eq-path-faces-Finitely-Graded-Poset {i} x y H =
      map-left-unit-law-Σ-is-contr
        ( is-proof-irrelevant-is-prop
          ( is-set-Fin (succ-ℕ k) i i)
          ( refl))
        ( refl)
        ( pair-eq-Σ
          ( eq-path-elements-Finitely-Graded-Poset X
            ( element-face-Finitely-Graded-Poset X x)
            ( element-face-Finitely-Graded-Poset X y)
            ( refl)
            ( H)))

  antisymmetric-path-elements-Finitely-Graded-Poset :
    (x y : type-Finitely-Graded-Poset X) 
    path-elements-Finitely-Graded-Poset X x y 
    path-elements-Finitely-Graded-Poset X y x 
    Id x y
  antisymmetric-path-elements-Finitely-Graded-Poset (pair i x) (pair j y) H K =
    eq-path-elements-Finitely-Graded-Poset X (pair i x) (pair j y)
      ( antisymmetric-leq-Fin (succ-ℕ k)
        ( shape-Finitely-Graded-Poset X (pair i x))
        ( shape-Finitely-Graded-Poset X (pair j y))
        ( leq-type-path-faces-Finitely-Graded-Poset X x y H)
        ( leq-type-path-faces-Finitely-Graded-Poset X y x K))
      ( H)

Poset structure on the underlying type of a finitely graded poset

module _
  {l1 l2 : Level} {k : } (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    (x y : type-Finitely-Graded-Poset X)
    where

    leq-Finitely-Graded-Poset-Prop : Prop (l1  l2)
    leq-Finitely-Graded-Poset-Prop =
      trunc-Prop (path-elements-Finitely-Graded-Poset X x y)

    leq-Finitely-Graded-Poset : UU (l1  l2)
    leq-Finitely-Graded-Poset = type-Prop leq-Finitely-Graded-Poset-Prop

    is-prop-leq-Finitely-Graded-Poset : is-prop leq-Finitely-Graded-Poset
    is-prop-leq-Finitely-Graded-Poset =
      is-prop-type-Prop leq-Finitely-Graded-Poset-Prop

  refl-leq-Finitely-Graded-Poset :
    (x : type-Finitely-Graded-Poset X)  leq-Finitely-Graded-Poset x x
  refl-leq-Finitely-Graded-Poset x =
    unit-trunc-Prop (refl-path-elements-Finitely-Graded-Poset X x)

  transitive-leq-Finitely-Graded-Poset :
    (x y z : type-Finitely-Graded-Poset X) 
    leq-Finitely-Graded-Poset y z  leq-Finitely-Graded-Poset x y 
    leq-Finitely-Graded-Poset x z
  transitive-leq-Finitely-Graded-Poset x y z H K =
    apply-universal-property-trunc-Prop H
      ( leq-Finitely-Graded-Poset-Prop x z)
      ( λ L 
        apply-universal-property-trunc-Prop K
          ( leq-Finitely-Graded-Poset-Prop x z)
          ( λ M 
            unit-trunc-Prop
              ( concat-path-elements-Finitely-Graded-Poset X x y z L M)))

  antisymmetric-leq-Finitely-Graded-Poset :
    (x y : type-Finitely-Graded-Poset X) 
    leq-Finitely-Graded-Poset x y  leq-Finitely-Graded-Poset y x  Id x y
  antisymmetric-leq-Finitely-Graded-Poset x y H K =
    apply-universal-property-trunc-Prop H
      ( Id-Prop (set-Finitely-Graded-Poset X) x y)
      ( λ L 
        apply-universal-property-trunc-Prop K
          ( Id-Prop (set-Finitely-Graded-Poset X) x y)
          ( λ M 
            antisymmetric-path-elements-Finitely-Graded-Poset X x y L M))

  preorder-Finitely-Graded-Poset : Preorder l1 (l1  l2)
  pr1 preorder-Finitely-Graded-Poset = type-Finitely-Graded-Poset X
  pr1 (pr2 preorder-Finitely-Graded-Poset) = leq-Finitely-Graded-Poset-Prop
  pr1 (pr2 (pr2 preorder-Finitely-Graded-Poset)) =
    refl-leq-Finitely-Graded-Poset
  pr2 (pr2 (pr2 preorder-Finitely-Graded-Poset)) =
    transitive-leq-Finitely-Graded-Poset

  poset-Finitely-Graded-Poset : Poset l1 (l1  l2)
  pr1 poset-Finitely-Graded-Poset = preorder-Finitely-Graded-Poset
  pr2 poset-Finitely-Graded-Poset = antisymmetric-leq-Finitely-Graded-Poset

Least and largest elements in finitely graded posets

We make sure that the least element is a face of type zero-Fin, and that the largest element is a face of type neg-one-Fin.

module _
  {l1 l2 : Level} {k : } (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    (x : face-Finitely-Graded-Poset X (zero-Fin k))
    where

    is-bottom-element-Finitely-Graded-Poset-Prop : Prop (l1  l2)
    is-bottom-element-Finitely-Graded-Poset-Prop =
      is-bottom-element-Poset-Prop
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

    is-bottom-element-Finitely-Graded-Poset : UU (l1  l2)
    is-bottom-element-Finitely-Graded-Poset =
      is-bottom-element-Poset
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

    is-prop-is-bottom-element-Finitely-Graded-Poset :
      is-prop is-bottom-element-Finitely-Graded-Poset
    is-prop-is-bottom-element-Finitely-Graded-Poset =
      is-prop-is-bottom-element-Poset
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

  has-bottom-element-Finitely-Graded-Poset : UU (l1  l2)
  has-bottom-element-Finitely-Graded-Poset =
    Σ ( face-Finitely-Graded-Poset X (zero-Fin k))
      ( is-bottom-element-Finitely-Graded-Poset)

  all-elements-equal-has-bottom-element-Finitely-Graded-Poset :
    all-elements-equal has-bottom-element-Finitely-Graded-Poset
  all-elements-equal-has-bottom-element-Finitely-Graded-Poset
    ( pair x H)
    ( pair y K) =
    eq-type-subtype
      ( is-bottom-element-Finitely-Graded-Poset-Prop)
      ( apply-universal-property-trunc-Prop
        ( H (element-face-Finitely-Graded-Poset X y))
        ( Id-Prop (face-Finitely-Graded-Poset-Set X (zero-Fin k)) x y)
        ( eq-path-faces-Finitely-Graded-Poset X x y))

  is-prop-has-bottom-element-Finitely-Graded-Poset :
    is-prop has-bottom-element-Finitely-Graded-Poset
  is-prop-has-bottom-element-Finitely-Graded-Poset =
    is-prop-all-elements-equal
      all-elements-equal-has-bottom-element-Finitely-Graded-Poset

  has-bottom-element-Finitely-Graded-Poset-Prop : Prop (l1  l2)
  pr1 has-bottom-element-Finitely-Graded-Poset-Prop =
    has-bottom-element-Finitely-Graded-Poset
  pr2 has-bottom-element-Finitely-Graded-Poset-Prop =
    is-prop-has-bottom-element-Finitely-Graded-Poset

  module _
    (x : face-Finitely-Graded-Poset X (neg-one-Fin k))
    where

    is-top-element-Finitely-Graded-Poset-Prop : Prop (l1  l2)
    is-top-element-Finitely-Graded-Poset-Prop =
      is-top-element-Poset-Prop
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

    is-top-element-Finitely-Graded-Poset : UU (l1  l2)
    is-top-element-Finitely-Graded-Poset =
      is-top-element-Poset
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

    is-prop-is-top-element-Finitely-Graded-Poset :
      is-prop is-top-element-Finitely-Graded-Poset
    is-prop-is-top-element-Finitely-Graded-Poset =
      is-prop-is-top-element-Poset
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

  has-top-element-Finitely-Graded-Poset : UU (l1  l2)
  has-top-element-Finitely-Graded-Poset =
    Σ ( face-Finitely-Graded-Poset X (neg-one-Fin k))
      ( is-top-element-Finitely-Graded-Poset)

  all-elements-equal-has-top-element-Finitely-Graded-Poset :
    all-elements-equal has-top-element-Finitely-Graded-Poset
  all-elements-equal-has-top-element-Finitely-Graded-Poset
    (pair x H) (pair y K) =
    eq-type-subtype
      ( is-top-element-Finitely-Graded-Poset-Prop)
      ( apply-universal-property-trunc-Prop
        ( K (element-face-Finitely-Graded-Poset X x))
        ( Id-Prop (face-Finitely-Graded-Poset-Set X (neg-one-Fin k)) x y)
        ( eq-path-faces-Finitely-Graded-Poset X x y))

  is-prop-has-top-element-Finitely-Graded-Poset :
    is-prop has-top-element-Finitely-Graded-Poset
  is-prop-has-top-element-Finitely-Graded-Poset =
    is-prop-all-elements-equal
      all-elements-equal-has-top-element-Finitely-Graded-Poset

  has-top-element-Finitely-Graded-Poset-Prop : Prop (l1  l2)
  pr1 has-top-element-Finitely-Graded-Poset-Prop =
    has-top-element-Finitely-Graded-Poset
  pr2 has-top-element-Finitely-Graded-Poset-Prop =
    is-prop-has-top-element-Finitely-Graded-Poset

  has-bottom-and-top-element-Finitely-Graded-Poset-Prop : Prop (l1  l2)
  has-bottom-and-top-element-Finitely-Graded-Poset-Prop =
    prod-Prop
      has-bottom-element-Finitely-Graded-Poset-Prop
      has-top-element-Finitely-Graded-Poset-Prop

  has-bottom-and-top-element-Finitely-Graded-Poset : UU (l1  l2)
  has-bottom-and-top-element-Finitely-Graded-Poset =
    type-Prop has-bottom-and-top-element-Finitely-Graded-Poset-Prop

  is-prop-has-bottom-and-top-element-Finitely-Graded-Poset :
    is-prop has-bottom-and-top-element-Finitely-Graded-Poset
  is-prop-has-bottom-and-top-element-Finitely-Graded-Poset =
    is-prop-type-Prop has-bottom-and-top-element-Finitely-Graded-Poset-Prop

Finitely graded subposets

module _
  {l1 l2 l3 : Level} {k : } (X : Finitely-Graded-Poset l1 l2 k)
  (S : {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l3)
  where

  module _
    (i : Fin (succ-ℕ k))
    where

    face-set-Finitely-Graded-Subposet : Set (l1  l3)
    face-set-Finitely-Graded-Subposet =
      Σ-Set
        ( face-Finitely-Graded-Poset-Set X i)
        ( λ x  set-Prop (S x))

    face-Finitely-Graded-Subposet : UU (l1  l3)
    face-Finitely-Graded-Subposet = type-Set face-set-Finitely-Graded-Subposet

    is-set-face-Finitely-Graded-Subposet : is-set face-Finitely-Graded-Subposet
    is-set-face-Finitely-Graded-Subposet =
      is-set-type-Set face-set-Finitely-Graded-Subposet

    eq-face-Finitely-Graded-Subposet :
      (x y : face-Finitely-Graded-Subposet)  Id (pr1 x) (pr1 y)  Id x y
    eq-face-Finitely-Graded-Subposet x y = eq-type-subtype S

    emb-face-Finitely-Graded-Subposet :
      face-Finitely-Graded-Subposet  face-Finitely-Graded-Poset X i
    emb-face-Finitely-Graded-Subposet = emb-subtype S

    map-emb-face-Finitely-Graded-Subposet :
      face-Finitely-Graded-Subposet  face-Finitely-Graded-Poset X i
    map-emb-face-Finitely-Graded-Subposet =
      map-emb emb-face-Finitely-Graded-Subposet

    is-emb-map-emb-face-Finitely-Graded-Subposet :
      is-emb map-emb-face-Finitely-Graded-Subposet
    is-emb-map-emb-face-Finitely-Graded-Subposet =
      is-emb-map-emb emb-face-Finitely-Graded-Subposet

  module _
    (i : Fin k) (y : face-Finitely-Graded-Subposet (inl-Fin k i))
    (z : face-Finitely-Graded-Subposet (succ-Fin (succ-ℕ k) (inl-Fin k i)))
    where

    adjacent-Finitely-Graded-subPoset-Prop : Prop l2
    adjacent-Finitely-Graded-subPoset-Prop =
      adjacent-Finitely-Graded-Poset-Prop X i (pr1 y) (pr1 z)

    adjacent-Finitely-Graded-Subposet : UU l2
    adjacent-Finitely-Graded-Subposet =
      type-Prop adjacent-Finitely-Graded-subPoset-Prop

    is-prop-adjacent-Finitely-Graded-Subposet :
      is-prop adjacent-Finitely-Graded-Subposet
    is-prop-adjacent-Finitely-Graded-Subposet =
      is-prop-type-Prop adjacent-Finitely-Graded-subPoset-Prop

  element-set-Finitely-Graded-Subposet : Set (l1  l3)
  element-set-Finitely-Graded-Subposet =
    Σ-Set (Fin-Set (succ-ℕ k)) face-set-Finitely-Graded-Subposet

  type-Finitely-Graded-Subposet : UU (l1  l3)
  type-Finitely-Graded-Subposet =
    type-Set element-set-Finitely-Graded-Subposet

  emb-type-Finitely-Graded-Subposet :
    type-Finitely-Graded-Subposet  type-Finitely-Graded-Poset X
  emb-type-Finitely-Graded-Subposet =
    tot-emb emb-face-Finitely-Graded-Subposet

  map-emb-type-Finitely-Graded-Subposet :
    type-Finitely-Graded-Subposet  type-Finitely-Graded-Poset X
  map-emb-type-Finitely-Graded-Subposet =
    map-emb emb-type-Finitely-Graded-Subposet

  is-emb-map-emb-type-Finitely-Graded-Subposet :
    is-emb map-emb-type-Finitely-Graded-Subposet
  is-emb-map-emb-type-Finitely-Graded-Subposet =
    is-emb-map-emb emb-type-Finitely-Graded-Subposet

  is-injective-map-emb-type-Finitely-Graded-Subposet :
    is-injective map-emb-type-Finitely-Graded-Subposet
  is-injective-map-emb-type-Finitely-Graded-Subposet =
    is-injective-is-emb is-emb-map-emb-type-Finitely-Graded-Subposet

  is-set-type-Finitely-Graded-Subposet :
    is-set type-Finitely-Graded-Subposet
  is-set-type-Finitely-Graded-Subposet =
    is-set-type-Set element-set-Finitely-Graded-Subposet

  leq-Finitely-Graded-Subposet-Prop :
    (x y : type-Finitely-Graded-Subposet)  Prop (l1  l2)
  leq-Finitely-Graded-Subposet-Prop x y =
    leq-Finitely-Graded-Poset-Prop X
      ( map-emb-type-Finitely-Graded-Subposet x)
      ( map-emb-type-Finitely-Graded-Subposet y)

  leq-Finitely-Graded-Subposet :
    (x y : type-Finitely-Graded-Subposet)  UU (l1  l2)
  leq-Finitely-Graded-Subposet x y =
    type-Prop (leq-Finitely-Graded-Subposet-Prop x y)

  is-prop-leq-Finitely-Graded-Subposet :
    (x y : type-Finitely-Graded-Subposet) 
    is-prop (leq-Finitely-Graded-Subposet x y)
  is-prop-leq-Finitely-Graded-Subposet x y =
    is-prop-type-Prop (leq-Finitely-Graded-Subposet-Prop x y)

  refl-leq-Finitely-Graded-Subposet :
    (x : type-Finitely-Graded-Subposet)  leq-Finitely-Graded-Subposet x x
  refl-leq-Finitely-Graded-Subposet x =
    refl-leq-Finitely-Graded-Poset X
      ( map-emb-type-Finitely-Graded-Subposet x)

  transitive-leq-Finitely-Graded-Subposet :
    (x y z : type-Finitely-Graded-Subposet) 
    leq-Finitely-Graded-Subposet y z  leq-Finitely-Graded-Subposet x y 
    leq-Finitely-Graded-Subposet x z
  transitive-leq-Finitely-Graded-Subposet x y z =
    transitive-leq-Finitely-Graded-Poset X
      ( map-emb-type-Finitely-Graded-Subposet x)
      ( map-emb-type-Finitely-Graded-Subposet y)
      ( map-emb-type-Finitely-Graded-Subposet z)

  antisymmetric-leq-Finitely-Graded-Subposet :
    (x y : type-Finitely-Graded-Subposet) 
    leq-Finitely-Graded-Subposet x y  leq-Finitely-Graded-Subposet y x  Id x y
  antisymmetric-leq-Finitely-Graded-Subposet x y H K =
    is-injective-map-emb-type-Finitely-Graded-Subposet
      ( antisymmetric-leq-Finitely-Graded-Poset X
        ( map-emb-type-Finitely-Graded-Subposet x)
        ( map-emb-type-Finitely-Graded-Subposet y)
        ( H)
        ( K))

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

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

Inclusion of finitely graded subposets

module _
  {l1 l2 : Level} {k : } (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    {l3 l4 : Level}
    (S : {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l3)
    (T : {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l4)
    where

    inclusion-Finitely-Graded-Subposet-Prop : Prop (l1  l3  l4)
    inclusion-Finitely-Graded-Subposet-Prop =
      Π-Prop
        ( Fin (succ-ℕ k))
        ( λ i 
          Π-Prop
            ( face-Finitely-Graded-Poset X i)
            ( λ x  hom-Prop (S x) (T x)))

    inclusion-Finitely-Graded-Subposet : UU (l1  l3  l4)
    inclusion-Finitely-Graded-Subposet =
      type-Prop inclusion-Finitely-Graded-Subposet-Prop

    is-prop-inclusion-Finitely-Graded-Subposet :
      is-prop inclusion-Finitely-Graded-Subposet
    is-prop-inclusion-Finitely-Graded-Subposet =
      is-prop-type-Prop inclusion-Finitely-Graded-Subposet-Prop

  refl-inclusion-Finitely-Graded-Subposet :
    {l3 : Level}
    (S : {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l3) 
    inclusion-Finitely-Graded-Subposet S S
  refl-inclusion-Finitely-Graded-Subposet S i x = id

  transitive-inclusion-Finitely-Graded-Subposet :
    {l3 l4 l5 : Level}
    (S : {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l3)
    (T : {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l4)
    (U : {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l5) 
    inclusion-Finitely-Graded-Subposet T U 
    inclusion-Finitely-Graded-Subposet S T 
    inclusion-Finitely-Graded-Subposet S U
  transitive-inclusion-Finitely-Graded-Subposet S T U g f i x =
    (g i x)  (f i x)

  Finitely-Graded-subposet-Preorder :
    (l : Level)  Preorder (l1  lsuc l) (l1  l)
  pr1 (Finitely-Graded-subposet-Preorder l) =
    {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l
  pr1 (pr2 (Finitely-Graded-subposet-Preorder l)) =
    inclusion-Finitely-Graded-Subposet-Prop
  pr1 (pr2 (pr2 (Finitely-Graded-subposet-Preorder l))) =
    refl-inclusion-Finitely-Graded-Subposet
  pr2 (pr2 (pr2 (Finitely-Graded-subposet-Preorder l))) =
    transitive-inclusion-Finitely-Graded-Subposet

Chains in finitely graded posets

module _
  {l1 l2 : Level} {k : } (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    {l3 : Level}
    (S : {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l3)
    where

    is-chain-Finitely-Graded-Subposet-Prop : Prop (l1  l2  l3)
    is-chain-Finitely-Graded-Subposet-Prop =
      is-total-Poset-Prop (poset-Finitely-Graded-Subposet X S)

    is-chain-Finitely-Graded-Subposet : UU (l1  l2  l3)
    is-chain-Finitely-Graded-Subposet =
      type-Prop is-chain-Finitely-Graded-Subposet-Prop

    is-prop-is-chain-Finitely-Graded-Subposet :
      is-prop is-chain-Finitely-Graded-Subposet
    is-prop-is-chain-Finitely-Graded-Subposet =
      is-prop-type-Prop is-chain-Finitely-Graded-Subposet-Prop

  chain-Finitely-Graded-Poset : (l : Level)  UU (l1  l2  lsuc l)
  chain-Finitely-Graded-Poset l = Σ _ (is-chain-Finitely-Graded-Subposet {l})

  module _
    {l : Level} (C : chain-Finitely-Graded-Poset l)
    where

    subtype-chain-Finitely-Graded-Poset :
      {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l
    subtype-chain-Finitely-Graded-Poset = pr1 C

module _
  {l1 l2 l3 l4 : Level} {k : } (X : Finitely-Graded-Poset l1 l2 k)
  (C : chain-Finitely-Graded-Poset X l3) (D : chain-Finitely-Graded-Poset X l4)
  where

  inclusion-chain-Finitely-Graded-Poset-Prop : Prop (l1  l3  l4)
  inclusion-chain-Finitely-Graded-Poset-Prop =
    inclusion-Finitely-Graded-Subposet-Prop X
      ( subtype-chain-Finitely-Graded-Poset X C)
      ( subtype-chain-Finitely-Graded-Poset X D)

  inclusion-chain-Finitely-Graded-Poset : UU (l1  l3  l4)
  inclusion-chain-Finitely-Graded-Poset =
    inclusion-Finitely-Graded-Subposet X
      ( subtype-chain-Finitely-Graded-Poset X C)
      ( subtype-chain-Finitely-Graded-Poset X D)

  is-prop-inclusion-chain-Finitely-Graded-Poset :
    is-prop inclusion-chain-Finitely-Graded-Poset
  is-prop-inclusion-chain-Finitely-Graded-Poset =
    is-prop-inclusion-Finitely-Graded-Subposet X
      ( subtype-chain-Finitely-Graded-Poset X C)
      ( subtype-chain-Finitely-Graded-Poset X D)

Maximal chains in preorders

module _
  {l1 l2 : Level} {k : } (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    {l3 : Level} (C : chain-Finitely-Graded-Poset X l3)
    where

    is-maximal-chain-Finitely-Graded-Poset-Prop : Prop (l1  l2  lsuc l3)
    is-maximal-chain-Finitely-Graded-Poset-Prop =
      Π-Prop
        ( chain-Finitely-Graded-Poset X l3)
        ( λ D  inclusion-chain-Finitely-Graded-Poset-Prop X D C)

    is-maximal-chain-Finitely-Graded-Poset : UU (l1  l2  lsuc l3)
    is-maximal-chain-Finitely-Graded-Poset =
      type-Prop is-maximal-chain-Finitely-Graded-Poset-Prop

    is-prop-is-maximal-chain-Finitely-Graded-Poset :
      is-prop is-maximal-chain-Finitely-Graded-Poset
    is-prop-is-maximal-chain-Finitely-Graded-Poset =
      is-prop-type-Prop is-maximal-chain-Finitely-Graded-Poset-Prop

  maximal-chain-Finitely-Graded-Poset :
    (l : Level)  UU (l1  l2  lsuc l)
  maximal-chain-Finitely-Graded-Poset l =
    Σ _ (is-maximal-chain-Finitely-Graded-Poset {l})

  module _
    {l3 : Level} (C : maximal-chain-Finitely-Graded-Poset l3)
    where

    chain-maximal-chain-Finitely-Graded-Poset :
      chain-Finitely-Graded-Poset X l3
    chain-maximal-chain-Finitely-Graded-Poset = pr1 C

    is-maximal-chain-maximal-chain-Finitely-Graded-Poset :
      is-maximal-chain-Finitely-Graded-Poset
        chain-maximal-chain-Finitely-Graded-Poset
    is-maximal-chain-maximal-chain-Finitely-Graded-Poset = pr2 C

    subtype-maximal-chain-Finitely-Graded-Poset :
      {i : Fin (succ-ℕ k)}  face-Finitely-Graded-Poset X i  Prop l3
    subtype-maximal-chain-Finitely-Graded-Poset =
      subtype-chain-Finitely-Graded-Poset X
        chain-maximal-chain-Finitely-Graded-Poset