# Decidable posets

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, Victor Blanchi, fernabnor and louismntnu.

Created on 2023-05-03.

module order-theory.decidable-posets where
Imports
open import foundation.binary-relations
open import foundation.decidable-propositions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

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

## Idea

A decidable poset is a poset of which the ordering relation is decidable. It follows that decidable posets have decidable equality.

## Definition

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

is-decidable-leq-Poset-Prop : Prop (l1  l2)
is-decidable-leq-Poset-Prop =
is-decidable-leq-Preorder-Prop (preorder-Poset X)

is-decidable-leq-Poset : UU (l1  l2)
is-decidable-leq-Poset = type-Prop is-decidable-leq-Poset-Prop

is-prop-is-decidable-leq-Poset : is-prop is-decidable-leq-Poset
is-prop-is-decidable-leq-Poset = is-prop-type-Prop is-decidable-leq-Poset-Prop

Decidable-Poset : (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
Decidable-Poset l1 l2 = Σ (Poset l1 l2) is-decidable-leq-Poset

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

poset-Decidable-Poset : Poset l1 l2
poset-Decidable-Poset = pr1 X

preorder-Decidable-Poset : Preorder l1 l2
preorder-Decidable-Poset = preorder-Poset poset-Decidable-Poset

is-decidable-leq-Decidable-Poset :
is-decidable-leq-Poset (poset-Decidable-Poset)
is-decidable-leq-Decidable-Poset = pr2 X

type-Decidable-Poset : UU l1
type-Decidable-Poset = type-Poset poset-Decidable-Poset

leq-Decidable-Poset-Prop : (x y : type-Decidable-Poset)  Prop l2
leq-Decidable-Poset-Prop = leq-Poset-Prop poset-Decidable-Poset

leq-Decidable-Poset : (x y : type-Decidable-Poset)  UU l2
leq-Decidable-Poset = leq-Poset poset-Decidable-Poset

is-prop-leq-Decidable-Poset :
(x y : type-Decidable-Poset)  is-prop (leq-Decidable-Poset x y)
is-prop-leq-Decidable-Poset = is-prop-leq-Poset poset-Decidable-Poset

decidable-preorder-Decidable-Poset : Decidable-Preorder l1 l2
pr1 decidable-preorder-Decidable-Poset = preorder-Decidable-Poset
pr2 decidable-preorder-Decidable-Poset = is-decidable-leq-Decidable-Poset

leq-decidable-poset-decidable-Prop :
(x y : type-Decidable-Poset)  Decidable-Prop l2
leq-decidable-poset-decidable-Prop =
leq-Decidable-Preorder-Decidable-Prop decidable-preorder-Decidable-Poset

concatenate-eq-leq-Decidable-Poset :
{x y z : type-Decidable-Poset}  x  y
leq-Decidable-Poset y z  leq-Decidable-Poset x z
concatenate-eq-leq-Decidable-Poset =
concatenate-eq-leq-Poset poset-Decidable-Poset

concatenate-leq-eq-Decidable-Poset :
{x y z : type-Decidable-Poset}
leq-Decidable-Poset x y  y  z  leq-Decidable-Poset x z
concatenate-leq-eq-Decidable-Poset =
concatenate-leq-eq-Poset poset-Decidable-Poset

refl-leq-Decidable-Poset : is-reflexive leq-Decidable-Poset
refl-leq-Decidable-Poset = refl-leq-Poset poset-Decidable-Poset

transitive-leq-Decidable-Poset : is-transitive leq-Decidable-Poset
transitive-leq-Decidable-Poset = transitive-leq-Poset poset-Decidable-Poset

antisymmetric-leq-Decidable-Poset : is-antisymmetric leq-Decidable-Poset
antisymmetric-leq-Decidable-Poset =
antisymmetric-leq-Poset poset-Decidable-Poset

is-set-type-Decidable-Poset : is-set type-Decidable-Poset
is-set-type-Decidable-Poset = is-set-type-Poset poset-Decidable-Poset

set-Decidable-Poset : Set l1
set-Decidable-Poset = set-Poset poset-Decidable-Poset