Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Elisabeth Stenholm, Julian KG, fernabnor and louismntnu.

Created on 2022-01-06.

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.binary-relations
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.function-types
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.transport-along-identifications
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)
Σ ( 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

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

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

shape-Finitely-Graded-Poset (pair i x) = i

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
{j : Fin (succ-ℕ k)} (y : face-Finitely-Graded-Poset j) →
UU (l1 ⊔ l2)
where
{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))} →

{i j : Fin (succ-ℕ k)} (p : Id j i) (x : face-Finitely-Graded-Poset j) →
( x)

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

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

(x y z : type-Finitely-Graded-Poset) →

{i1 i2 : Fin (succ-ℕ k)} (x : face-Finitely-Graded-Poset i1)
path-faces-Finitely-Graded-Poset x y → leq-Fin (succ-ℕ k) i1 i2
refl-path-faces-Finitely-Graded-Poset = refl-leq-Fin (succ-ℕ k) i1
( 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)


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)
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
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
{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-Σ
( refl)
( H)))

(x y : type-Finitely-Graded-Poset 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 _
where

leq-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)

leq-Finitely-Graded-Poset : UU (l1 ⊔ l2)

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

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)

poset-Finitely-Graded-Poset : Poset l1 (l1 ⊔ l2)


### 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-Poset-Prop

is-bottom-element-Finitely-Graded-Poset : UU (l1 ⊔ l2)
is-bottom-element-Poset

is-prop-is-bottom-element-Poset

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

( pair x H)
( pair y K) =
eq-type-subtype
( apply-universal-property-trunc-Prop
( Id-Prop (face-Finitely-Graded-Poset-Set X (zero-Fin k)) x y)

is-prop-all-elements-equal

has-bottom-element-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)

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-Poset-Prop

is-top-element-Finitely-Graded-Poset : UU (l1 ⊔ l2)
is-top-element-Poset

is-prop-is-top-element-Poset

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

(pair x H) (pair y K) =
eq-type-subtype
( apply-universal-property-trunc-Prop
( Id-Prop (face-Finitely-Graded-Poset-Set X (neg-one-Fin k)) x y)

is-prop-all-elements-equal

has-top-element-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)

has-bottom-and-top-element-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)
product-Prop

has-bottom-and-top-element-Finitely-Graded-Poset : UU (l1 ⊔ l2)



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)
Σ-Set
( λ x → set-Prop (S x))

face-Finitely-Graded-Subposet : UU (l1 ⊔ l3)

(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

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

element-set-Finitely-Graded-Subposet : Set (l1 ⊔ l3)

type-Finitely-Graded-Subposet : UU (l1 ⊔ l3)

(x y : type-Finitely-Graded-Subposet) → Prop (l1 ⊔ l2)

(x y : type-Finitely-Graded-Subposet) → UU (l1 ⊔ l2)

(x y z : type-Finitely-Graded-Subposet) →

antisymmetric-leq-Finitely-Graded-Subposet x y H K =
( H)
( K))

preorder-Finitely-Graded-Subposet : Preorder (l1 ⊔ l3) (l1 ⊔ l2)

poset-Finitely-Graded-Subposet : Poset (l1 ⊔ l3) (l1 ⊔ l2)


### 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)
Π-Prop
( Fin (succ-ℕ k))
( λ i →
Π-Prop
( λ x → hom-Prop (S x) (T x)))

inclusion-Finitely-Graded-Subposet : UU (l1 ⊔ l3 ⊔ l4)

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

{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) →
transitive-inclusion-Finitely-Graded-Subposet S T U g f i x =
(g i x) ∘ (f i x)

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


### 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 : UU (l1 ⊔ l2 ⊔ l3)

chain-Finitely-Graded-Poset : (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l)

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

{i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l

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

inclusion-chain-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l3 ⊔ l4)

inclusion-chain-Finitely-Graded-Poset : UU (l1 ⊔ l3 ⊔ l4)



### 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)
Π-Prop
( λ D → inclusion-chain-Finitely-Graded-Poset-Prop X D C)

is-maximal-chain-Finitely-Graded-Poset : UU (l1 ⊔ l2 ⊔ lsuc l3)

(l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l)

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