Subtypes leq Posets

Content created by Viktor Yudov.

Created on 2024-02-05.
Last modified on 2024-02-05.

module order-theory.subtypes-leq-posets where
Imports 
open import foundation.dependent-pair-types
open import foundation.subtypes
open import foundation.universe-levels

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

Idea

TODO

Definition

module _
  {l1 : Level} (l2 : Level) (A : UU l1)
  where

  subtypes-leq-Preorder : Preorder (l1 ⊔ lsuc l2) (l1 ⊔ l2)
  pr1 subtypes-leq-Preorder = subtype l2 A
  pr1 (pr2 subtypes-leq-Preorder) = leq-prop-subtype
  pr1 (pr2 (pr2 subtypes-leq-Preorder)) = refl-leq-subtype
  pr2 (pr2 (pr2 subtypes-leq-Preorder)) = transitive-leq-subtype

  subtypes-leq-Poset : Poset (l1 ⊔ lsuc l2) (l1 ⊔ l2)
  pr1 subtypes-leq-Poset = subtypes-leq-Preorder
  pr2 subtypes-leq-Poset = antisymmetric-leq-subtype

Recent changes