Large meet-subsemilattices
module order-theory.large-meet-subsemilattices where
Imports
open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositions open import foundation.universe-levels open import order-theory.greatest-lower-bounds-large-posets open import order-theory.large-meet-semilattices open import order-theory.large-posets open import order-theory.large-preorders open import order-theory.large-subposets open import order-theory.top-elements-large-posets
Idea
A large meet-subsemilattice of a
large meet-semilattice L is a
large subposet S of L that is closed
under meets and contains the top element.
Definitions
The predicate that a large subposet is closed under meets
module _ {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level} (L : Large-Meet-Semilattice α β) (S : Large-Subposet γ (large-poset-Large-Meet-Semilattice L)) where is-closed-under-meets-Large-Subposet : UUω is-closed-under-meets-Large-Subposet = {l1 l2 : Level} (x : type-Large-Meet-Semilattice L l1) (y : type-Large-Meet-Semilattice L l2) → is-in-Large-Subposet (large-poset-Large-Meet-Semilattice L) S x → is-in-Large-Subposet (large-poset-Large-Meet-Semilattice L) S y → is-in-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( S) ( meet-Large-Meet-Semilattice L x y)
The predicate that a large subposet contains the top element
module _ {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level} (L : Large-Meet-Semilattice α β) (S : Large-Subposet γ (large-poset-Large-Meet-Semilattice L)) where contains-top-Large-Subposet : UU (γ lzero) contains-top-Large-Subposet = is-in-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( S) ( top-Large-Meet-Semilattice L)
The predicate that a large subposet is a large meet-subsemilattice
module _ {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level} (L : Large-Meet-Semilattice α β) (S : Large-Subposet γ (large-poset-Large-Meet-Semilattice L)) where record is-large-meet-subsemilattice-Large-Subposet : UUω where field is-closed-under-meets-is-large-meet-subsemilattice-Large-Subposet : is-closed-under-meets-Large-Subposet L S contains-top-is-large-meet-subsemilattice-Large-Poset : contains-top-Large-Subposet L S open is-large-meet-subsemilattice-Large-Subposet public
Large meet-subsemilattices
module _ {α : Level → Level} {β : Level → Level → Level} (γ : Level → Level) (L : Large-Meet-Semilattice α β) where record Large-Meet-Subsemilattice : UUω where field large-subposet-Large-Meet-Subsemilattice : Large-Subposet γ (large-poset-Large-Meet-Semilattice L) is-closed-under-meets-Large-Meet-Subsemilattice : is-closed-under-meets-Large-Subposet L ( large-subposet-Large-Meet-Subsemilattice) contains-top-Large-Meet-Subsemilattice : contains-top-Large-Subposet L ( large-subposet-Large-Meet-Subsemilattice) open Large-Meet-Subsemilattice public module _ {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level} (L : Large-Meet-Semilattice α β) (S : Large-Meet-Subsemilattice γ L) where large-poset-Large-Meet-Subsemilattice : Large-Poset (λ l → α l ⊔ γ l) β large-poset-Large-Meet-Subsemilattice = large-poset-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( large-subposet-Large-Meet-Subsemilattice S) large-preorder-Large-Meet-Subsemilattice : Large-Preorder (λ l → α l ⊔ γ l) (λ l1 l2 → β l1 l2) large-preorder-Large-Meet-Subsemilattice = large-preorder-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( large-subposet-Large-Meet-Subsemilattice S) is-in-Large-Meet-Subsemilattice : {l1 : Level} → type-Large-Meet-Semilattice L l1 → UU (γ l1) is-in-Large-Meet-Subsemilattice = is-in-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( large-subposet-Large-Meet-Subsemilattice S) type-Large-Meet-Subsemilattice : (l1 : Level) → UU (α l1 ⊔ γ l1) type-Large-Meet-Subsemilattice = type-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( large-subposet-Large-Meet-Subsemilattice S) leq-Large-Meet-Subsemilattice-Prop : {l1 l2 : Level} → type-Large-Meet-Subsemilattice l1 → type-Large-Meet-Subsemilattice l2 → Prop (β l1 l2) leq-Large-Meet-Subsemilattice-Prop = leq-Large-Subposet-Prop ( large-poset-Large-Meet-Semilattice L) ( large-subposet-Large-Meet-Subsemilattice S) leq-Large-Meet-Subsemilattice : {l1 l2 : Level} → type-Large-Meet-Subsemilattice l1 → type-Large-Meet-Subsemilattice l2 → UU (β l1 l2) leq-Large-Meet-Subsemilattice = leq-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( large-subposet-Large-Meet-Subsemilattice S) is-prop-leq-Large-Meet-Subsemilattice : {l1 l2 : Level} → (x : type-Large-Meet-Subsemilattice l1) (y : type-Large-Meet-Subsemilattice l2) → is-prop (leq-Large-Meet-Subsemilattice x y) is-prop-leq-Large-Meet-Subsemilattice = is-prop-leq-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( large-subposet-Large-Meet-Subsemilattice S) refl-leq-Large-Meet-Subsemilattice : {l1 : Level} (x : type-Large-Meet-Subsemilattice l1) → leq-Large-Meet-Subsemilattice x x refl-leq-Large-Meet-Subsemilattice = refl-leq-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( large-subposet-Large-Meet-Subsemilattice S) transitive-leq-Large-Meet-Subsemilattice : {l1 l2 l3 : Level} (x : type-Large-Meet-Subsemilattice l1) (y : type-Large-Meet-Subsemilattice l2) (z : type-Large-Meet-Subsemilattice l3) → leq-Large-Meet-Subsemilattice y z → leq-Large-Meet-Subsemilattice x y → leq-Large-Meet-Subsemilattice x z transitive-leq-Large-Meet-Subsemilattice = transitive-leq-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( large-subposet-Large-Meet-Subsemilattice S) antisymmetric-leq-Large-Meet-Subsemilattice : {l1 : Level} (x : type-Large-Meet-Subsemilattice l1) (y : type-Large-Meet-Subsemilattice l1) → leq-Large-Meet-Subsemilattice x y → leq-Large-Meet-Subsemilattice y x → x ＝ y antisymmetric-leq-Large-Meet-Subsemilattice = antisymmetric-leq-Large-Subposet ( large-poset-Large-Meet-Semilattice L) ( large-subposet-Large-Meet-Subsemilattice S) is-closed-under-sim-Large-Meet-Subsemilattice : {l1 l2 : Level} (x : type-Large-Meet-Semilattice L l1) (y : type-Large-Meet-Semilattice L l2) → leq-Large-Meet-Semilattice L x y → leq-Large-Meet-Semilattice L y x → is-in-Large-Meet-Subsemilattice x → is-in-Large-Meet-Subsemilattice y is-closed-under-sim-Large-Meet-Subsemilattice = is-closed-under-sim-Large-Subposet ( large-subposet-Large-Meet-Subsemilattice S) meet-Large-Meet-Subsemilattice : {l1 l2 : Level} (x : type-Large-Meet-Subsemilattice l1) (y : type-Large-Meet-Subsemilattice l2) → type-Large-Meet-Subsemilattice (l1 ⊔ l2) pr1 (meet-Large-Meet-Subsemilattice (x , p) (y , q)) = meet-Large-Meet-Semilattice L x y pr2 (meet-Large-Meet-Subsemilattice (x , p) (y , q)) = is-closed-under-meets-Large-Meet-Subsemilattice S x y p q is-greatest-binary-lower-bound-meet-Large-Meet-Subsemilattice : {l1 l2 : Level} (x : type-Large-Meet-Subsemilattice l1) (y : type-Large-Meet-Subsemilattice l2) → is-greatest-binary-lower-bound-Large-Poset ( large-poset-Large-Meet-Subsemilattice) ( x) ( y) ( meet-Large-Meet-Subsemilattice x y) is-greatest-binary-lower-bound-meet-Large-Meet-Subsemilattice (x , p) (y , q) (z , r) = is-greatest-binary-lower-bound-meet-Large-Meet-Semilattice L x y z has-meets-Large-Meet-Subsemilattice : has-meets-Large-Poset ( large-poset-Large-Meet-Subsemilattice) meet-has-meets-Large-Poset has-meets-Large-Meet-Subsemilattice = meet-Large-Meet-Subsemilattice is-greatest-binary-lower-bound-meet-has-meets-Large-Poset has-meets-Large-Meet-Subsemilattice = is-greatest-binary-lower-bound-meet-Large-Meet-Subsemilattice top-Large-Meet-Subsemilattice : type-Large-Meet-Subsemilattice lzero pr1 top-Large-Meet-Subsemilattice = top-Large-Meet-Semilattice L pr2 top-Large-Meet-Subsemilattice = contains-top-Large-Meet-Subsemilattice S is-top-element-top-Large-Meet-Subsemilattice : {l1 : Level} (x : type-Large-Meet-Subsemilattice l1) → leq-Large-Meet-Subsemilattice x top-Large-Meet-Subsemilattice is-top-element-top-Large-Meet-Subsemilattice (x , p) = is-top-element-top-Large-Meet-Semilattice L x has-top-element-Large-Meet-Subsemilattice : has-top-element-Large-Poset ( large-poset-Large-Meet-Subsemilattice) top-has-top-element-Large-Poset has-top-element-Large-Meet-Subsemilattice = top-Large-Meet-Subsemilattice is-top-element-top-has-top-element-Large-Poset has-top-element-Large-Meet-Subsemilattice = is-top-element-top-Large-Meet-Subsemilattice is-large-meet-semilattice-Large-Meet-Subsemilattice : is-large-meet-semilattice-Large-Poset ( large-poset-Large-Meet-Subsemilattice) has-meets-is-large-meet-semilattice-Large-Poset is-large-meet-semilattice-Large-Meet-Subsemilattice = has-meets-Large-Meet-Subsemilattice has-top-element-is-large-meet-semilattice-Large-Poset is-large-meet-semilattice-Large-Meet-Subsemilattice = has-top-element-Large-Meet-Subsemilattice large-meet-semilattice-Large-Meet-Subsemilattice : Large-Meet-Semilattice (λ l → α l ⊔ γ l) β large-poset-Large-Meet-Semilattice large-meet-semilattice-Large-Meet-Subsemilattice = large-poset-Large-Meet-Subsemilattice is-large-meet-semilattice-Large-Meet-Semilattice large-meet-semilattice-Large-Meet-Subsemilattice = is-large-meet-semilattice-Large-Meet-Subsemilattice