open import foundation.dependent-pair-types
open import foundation.functions
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import order-theory.greatest-lower-bounds-large-posets
open import order-theory.large-frames
open import order-theory.large-meet-semilattices
open import order-theory.large-meet-subsemilattices
open import order-theory.large-posets
open import order-theory.large-preorders
open import order-theory.large-subposets
open import order-theory.large-subpreorders
open import order-theory.large-subsuplattices
open import order-theory.large-suplattices
open import order-theory.least-upper-bounds-large-posets
open import order-theory.top-elements-large-posets

Idea

A large subframe of a large frame is a large subposet which is closed under meets, contains the top element, and is closed under suprema.

Definition

record
  Large-Subframe
    {α : Level → Level} {β : Level → Level → Level} (γ : Level → Level)
    (F : Large-Frame α β) :
  UUω
  where
  field
    large-subposet-Large-Subframe :
      Large-Subposet γ (large-poset-Large-Frame F)
    is-closed-under-meets-Large-Subframe :
      is-closed-under-meets-Large-Subposet
        ( large-meet-semilattice-Large-Frame F)
        ( large-subposet-Large-Subframe)
    contains-top-Large-Subframe :
      contains-top-Large-Subposet
        ( large-meet-semilattice-Large-Frame F)
        ( large-subposet-Large-Subframe)
    is-closed-under-sup-Large-Subframe :
      is-closed-under-sup-Large-Subposet
        ( large-suplattice-Large-Frame F)
        ( large-subposet-Large-Subframe)

open Large-Subframe public

module _
  {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level}
  (F : Large-Frame α β) (S : Large-Subframe γ F)
  where

  large-poset-Large-Subframe :
    Large-Poset (λ l → α l ⊔ γ l) β
  large-poset-Large-Subframe =
    large-poset-Large-Subposet
      ( large-poset-Large-Frame F)
      ( large-subposet-Large-Subframe S)

  large-subpreorder-Large-Subframe :
    Large-Subpreorder γ (large-preorder-Large-Frame F)
  large-subpreorder-Large-Subframe =
    large-subpreorder-Large-Subposet (large-subposet-Large-Subframe S)

  large-preorder-Large-Subframe :
    Large-Preorder (λ l → α l ⊔ γ l) (λ l1 l2 → β l1 l2)
  large-preorder-Large-Subframe =
    large-preorder-Large-Subposet
      ( large-poset-Large-Frame F)
      ( large-subposet-Large-Subframe S)

  is-in-Large-Subframe :
    {l1 : Level} → type-Large-Frame F l1 → UU (γ l1)
  is-in-Large-Subframe =
    is-in-Large-Subposet
      ( large-poset-Large-Frame F)
      ( large-subposet-Large-Subframe S)

  type-Large-Subframe : (l1 : Level) → UU (α l1 ⊔ γ l1)
  type-Large-Subframe =
    type-Large-Subposet
      ( large-poset-Large-Frame F)
      ( large-subposet-Large-Subframe S)

  leq-Large-Subframe-Prop :
    {l1 l2 : Level} →
    type-Large-Subframe l1 →
    type-Large-Subframe l2 →
    Prop (β l1 l2)
  leq-Large-Subframe-Prop =
    leq-Large-Subposet-Prop
      ( large-poset-Large-Frame F)
      ( large-subposet-Large-Subframe S)

  leq-Large-Subframe :
    {l1 l2 : Level} →
    type-Large-Subframe l1 →
    type-Large-Subframe l2 →
    UU (β l1 l2)
  leq-Large-Subframe =
    leq-Large-Subposet
      ( large-poset-Large-Frame F)
      ( large-subposet-Large-Subframe S)

  is-prop-leq-Large-Subframe :
    {l1 l2 : Level} →
    (x : type-Large-Subframe l1)
    (y : type-Large-Subframe l2) →
    is-prop (leq-Large-Subframe x y)
  is-prop-leq-Large-Subframe =
    is-prop-leq-Large-Subposet
      ( large-poset-Large-Frame F)
      ( large-subposet-Large-Subframe S)

  refl-leq-Large-Subframe :
    {l1 : Level} (x : type-Large-Subframe l1) →
    leq-Large-Subframe x x
  refl-leq-Large-Subframe =
    refl-leq-Large-Subposet
      ( large-poset-Large-Frame F)
      ( large-subposet-Large-Subframe S)

  transitive-leq-Large-Subframe :
    {l1 l2 l3 : Level}
    (x : type-Large-Subframe l1)
    (y : type-Large-Subframe l2)
    (z : type-Large-Subframe l3) →
    leq-Large-Subframe y z → leq-Large-Subframe x y →
    leq-Large-Subframe x z
  transitive-leq-Large-Subframe =
    transitive-leq-Large-Subposet
      ( large-poset-Large-Frame F)
      ( large-subposet-Large-Subframe S)

  antisymmetric-leq-Large-Subframe :
    {l1 : Level}
    (x : type-Large-Subframe l1)
    (y : type-Large-Subframe l1) →
    leq-Large-Subframe x y →
    leq-Large-Subframe y x →
    x ＝ y
  antisymmetric-leq-Large-Subframe =
    antisymmetric-leq-Large-Subposet
      ( large-poset-Large-Frame F)
      ( large-subposet-Large-Subframe S)

  is-closed-under-sim-Large-Subframe :
    {l1 l2 : Level}
    (x : type-Large-Frame F l1)
    (y : type-Large-Frame F l2) →
    leq-Large-Frame F x y →
    leq-Large-Frame F y x →
    is-in-Large-Subframe x →
    is-in-Large-Subframe y
  is-closed-under-sim-Large-Subframe =
    is-closed-under-sim-Large-Subposet
      ( large-subposet-Large-Subframe S)

  meet-Large-Subframe :
    {l1 l2 : Level}
    (x : type-Large-Subframe l1)
    (y : type-Large-Subframe l2) →
    type-Large-Subframe (l1 ⊔ l2)
  pr1 (meet-Large-Subframe (x , p) (y , q)) =
    meet-Large-Frame F x y
  pr2 (meet-Large-Subframe (x , p) (y , q)) =
    is-closed-under-meets-Large-Subframe S x y p q

  is-greatest-binary-lower-bound-meet-Large-Subframe :
    {l1 l2 : Level}
    (x : type-Large-Subframe l1)
    (y : type-Large-Subframe l2) →
    is-greatest-binary-lower-bound-Large-Poset
      ( large-poset-Large-Subframe)
      ( x)
      ( y)
      ( meet-Large-Subframe x y)
  is-greatest-binary-lower-bound-meet-Large-Subframe
    (x , p) (y , q) (z , r) =
    is-greatest-binary-lower-bound-meet-Large-Frame F x y z

  has-meets-Large-Subframe :
    has-meets-Large-Poset
      ( large-poset-Large-Subframe)
  meet-has-meets-Large-Poset
    has-meets-Large-Subframe =
    meet-Large-Subframe
  is-greatest-binary-lower-bound-meet-has-meets-Large-Poset
    has-meets-Large-Subframe =
    is-greatest-binary-lower-bound-meet-Large-Subframe

  top-Large-Subframe :
    type-Large-Subframe lzero
  pr1 top-Large-Subframe = top-Large-Frame F
  pr2 top-Large-Subframe = contains-top-Large-Subframe S

  is-top-element-top-Large-Subframe :
    {l1 : Level} (x : type-Large-Subframe l1) →
    leq-Large-Subframe x top-Large-Subframe
  is-top-element-top-Large-Subframe (x , p) =
    is-top-element-top-Large-Frame F x

  has-top-element-Large-Subframe :
    has-top-element-Large-Poset
      ( large-poset-Large-Subframe)
  top-has-top-element-Large-Poset
    has-top-element-Large-Subframe =
    top-Large-Subframe
  is-top-element-top-has-top-element-Large-Poset
    has-top-element-Large-Subframe =
    is-top-element-top-Large-Subframe

  is-large-meet-semilattice-Large-Subframe :
    is-large-meet-semilattice-Large-Poset
      ( large-poset-Large-Subframe)
  has-meets-is-large-meet-semilattice-Large-Poset
    is-large-meet-semilattice-Large-Subframe =
    has-meets-Large-Subframe
  has-top-element-is-large-meet-semilattice-Large-Poset
    is-large-meet-semilattice-Large-Subframe =
    has-top-element-Large-Subframe

  large-meet-semilattice-Large-Subframe :
    Large-Meet-Semilattice (λ l → α l ⊔ γ l) β
  large-poset-Large-Meet-Semilattice
    large-meet-semilattice-Large-Subframe =
    large-poset-Large-Subframe
  is-large-meet-semilattice-Large-Meet-Semilattice
    large-meet-semilattice-Large-Subframe =
    is-large-meet-semilattice-Large-Subframe

  sup-Large-Subframe :
    {l1 l2 : Level} {I : UU l1} (x : I → type-Large-Subframe l2) →
    type-Large-Subframe (l1 ⊔ l2)
  pr1 (sup-Large-Subframe x) = sup-Large-Frame F (pr1 ∘ x)
  pr2 (sup-Large-Subframe x) =
    is-closed-under-sup-Large-Subframe S
      ( pr1 ∘ x)
      ( pr2 ∘ x)

  is-least-upper-bound-sup-Large-Subframe :
    {l1 l2 : Level} {I : UU l1} (x : I → type-Large-Subframe l2) →
    is-least-upper-bound-family-of-elements-Large-Poset
      ( large-poset-Large-Subframe)
      ( x)
      ( sup-Large-Subframe x)
  is-least-upper-bound-sup-Large-Subframe x y =
    is-least-upper-bound-sup-Large-Frame F (pr1 ∘ x) (pr1 y)

  is-large-suplattice-Large-Subframe :
    is-large-suplattice-Large-Poset (large-poset-Large-Subframe)
  sup-has-least-upper-bound-family-of-elements-Large-Poset
    ( is-large-suplattice-Large-Subframe x) =
    sup-Large-Subframe x
  is-least-upper-bound-sup-has-least-upper-bound-family-of-elements-Large-Poset
    ( is-large-suplattice-Large-Subframe x) =
    is-least-upper-bound-sup-Large-Subframe x

  large-suplattice-Large-Subframe :
    Large-Suplattice (λ l → α l ⊔ γ l) β
  large-poset-Large-Suplattice
    large-suplattice-Large-Subframe =
    large-poset-Large-Subframe
  is-large-suplattice-Large-Suplattice
    large-suplattice-Large-Subframe =
    is-large-suplattice-Large-Subframe

  distributive-meet-sup-Large-Subframe :
    {l1 l2 l3 : Level} (x : type-Large-Subframe l1)
    {I : UU l2} (y : I → type-Large-Subframe l3) →
    meet-Large-Subframe x (sup-Large-Subframe y) ＝
    sup-Large-Subframe (λ i → meet-Large-Subframe x (y i))
  distributive-meet-sup-Large-Subframe x y =
    eq-type-subtype
      ( large-subpreorder-Large-Subframe)
      ( distributive-meet-sup-Large-Frame F (pr1 x) (pr1 ∘ y))

  large-frame-Large-Subframe :
    Large-Frame (λ l → α l ⊔ γ l) β
  large-poset-Large-Frame
    large-frame-Large-Subframe =
    large-poset-Large-Subframe
  is-large-meet-semilattice-Large-Frame
    large-frame-Large-Subframe =
    is-large-meet-semilattice-Large-Subframe
  is-large-suplattice-Large-Frame
    large-frame-Large-Subframe =
    is-large-suplattice-Large-Subframe
  distributive-meet-sup-Large-Frame
    large-frame-Large-Subframe =
    distributive-meet-sup-Large-Subframe