Large subposets
module order-theory.large-subposets where
Imports
open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositions open import foundation.subtypes open import foundation.universe-levels open import order-theory.large-posets open import order-theory.large-preorders open import order-theory.large-subpreorders
Idea
A large subposet of a large poset P
consists of a subtype S : type-Large-Poset P l1 → Prop (γ l1) for each
universe level l1 such that the implication
((x ≤ y) ∧ (y ≤ x)) → (x ∈ S → y ∈ S)
holds for every x y : P. Note that for elements of the same universe level,
this is automatic by antisymmetry.
Definition
module _ {α : Level → Level} {β : Level → Level → Level} (γ : Level → Level) (P : Large-Poset α β) where record Large-Subposet : UUω where field large-subpreorder-Large-Subposet : Large-Subpreorder γ (large-preorder-Large-Poset P) is-closed-under-sim-Large-Subposet : {l1 l2 : Level} (x : type-Large-Poset P l1) (y : type-Large-Poset P l2) → leq-Large-Poset P x y → leq-Large-Poset P y x → is-in-Large-Subpreorder ( large-preorder-Large-Poset P) ( large-subpreorder-Large-Subposet) ( x) → is-in-Large-Subpreorder ( large-preorder-Large-Poset P) ( large-subpreorder-Large-Subposet) ( y) open Large-Subposet public module _ {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level} (P : Large-Poset α β) (S : Large-Subposet γ P) where large-preorder-Large-Subposet : Large-Preorder (λ l → α l ⊔ γ l) (λ l1 l2 → β l1 l2) large-preorder-Large-Subposet = large-preorder-Large-Subpreorder ( large-preorder-Large-Poset P) ( large-subpreorder-Large-Subposet S) is-in-Large-Subposet : {l1 : Level} → type-Large-Poset P l1 → UU (γ l1) is-in-Large-Subposet = is-in-Large-Subpreorder ( large-preorder-Large-Poset P) ( large-subpreorder-Large-Subposet S) type-Large-Subposet : (l1 : Level) → UU (α l1 ⊔ γ l1) type-Large-Subposet = type-Large-Subpreorder ( large-preorder-Large-Poset P) ( large-subpreorder-Large-Subposet S) leq-Large-Subposet-Prop : {l1 l2 : Level} → type-Large-Subposet l1 → type-Large-Subposet l2 → Prop (β l1 l2) leq-Large-Subposet-Prop = leq-Large-Subpreorder-Prop ( large-preorder-Large-Poset P) ( large-subpreorder-Large-Subposet S) leq-Large-Subposet : {l1 l2 : Level} → type-Large-Subposet l1 → type-Large-Subposet l2 → UU (β l1 l2) leq-Large-Subposet = leq-Large-Subpreorder ( large-preorder-Large-Poset P) ( large-subpreorder-Large-Subposet S) is-prop-leq-Large-Subposet : {l1 l2 : Level} → (x : type-Large-Subposet l1) (y : type-Large-Subposet l2) → is-prop (leq-Large-Subposet x y) is-prop-leq-Large-Subposet = is-prop-leq-Large-Subpreorder ( large-preorder-Large-Poset P) ( large-subpreorder-Large-Subposet S) refl-leq-Large-Subposet : {l1 : Level} (x : type-Large-Subposet l1) → leq-Large-Subposet x x refl-leq-Large-Subposet = refl-leq-Large-Subpreorder ( large-preorder-Large-Poset P) ( large-subpreorder-Large-Subposet S) transitive-leq-Large-Subposet : {l1 l2 l3 : Level} (x : type-Large-Subposet l1) (y : type-Large-Subposet l2) (z : type-Large-Subposet l3) → leq-Large-Subposet y z → leq-Large-Subposet x y → leq-Large-Subposet x z transitive-leq-Large-Subposet = transitive-leq-Large-Subpreorder ( large-preorder-Large-Poset P) ( large-subpreorder-Large-Subposet S) antisymmetric-leq-Large-Subposet : {l1 : Level} (x : type-Large-Subposet l1) (y : type-Large-Subposet l1) → leq-Large-Subposet x y → leq-Large-Subposet y x → x ＝ y antisymmetric-leq-Large-Subposet {l1} (x , p) (y , q) H K = eq-type-subtype ( large-subpreorder-Large-Subposet S {l1}) ( antisymmetric-leq-Large-Poset P x y H K) large-poset-Large-Subposet : Large-Poset (λ l → α l ⊔ γ l) β large-preorder-Large-Poset large-poset-Large-Subposet = large-preorder-Large-Subposet antisymmetric-leq-Large-Poset large-poset-Large-Subposet = antisymmetric-leq-Large-Subposet