Double powersets

module foundation.double-powersets where
Imports
open import foundation.existential-quantification
open import foundation.powersets
open import foundation.propositional-truncations

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

open import order-theory.large-posets
open import order-theory.posets

Definitions

The double powerset

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

  double-powerset-Large-Poset :
    UU l1 
    Large-Poset
      ( λ l3  l1  lsuc l2  lsuc l3)
      ( λ l3 l4  l1  lsuc l2  l3  l4)
  double-powerset-Large-Poset A = powerset-Large-Poset (powerset l2 A)

  double-powerset-Poset :
    (l : Level)  UU l1  Poset (l1  lsuc l2  lsuc l) (l1  lsuc l2  l)
  double-powerset-Poset l A =
    poset-Large-Poset (double-powerset-Large-Poset A) l

  double-powerset : (l3 : Level)  UU l1  UU (l1  lsuc l2  lsuc l3)
  double-powerset l3 A = type-Poset (double-powerset-Poset l3 A)

Operations on the double powerset

Intersections of subtypes of powersets

intersection-double-powerset :
  {l1 l2 l3 : Level} {A : UU l1} 
  double-powerset l2 l3 A  powerset (l1  lsuc l2  l3) A
intersection-double-powerset F a =
  Π-Prop (type-subtype F)  X  inclusion-subtype F X a)

module _
  {l1 l2 l3 : Level} {A : UU l1} (F : double-powerset l2 l3 A)
  where

  inclusion-intersection-double-powerset :
    (X : type-subtype F) 
    intersection-double-powerset F  inclusion-subtype F X
  inclusion-intersection-double-powerset X a f = f X

  universal-property-intersection-double-powerset :
    {l : Level} (P : powerset l A)
    (H : (X : type-subtype F)  P  inclusion-subtype F X) 
    P  intersection-double-powerset F
  universal-property-intersection-double-powerset P H a p X = H X a p

Unions of subtypes of powersets

union-double-powerset :
  {l1 l2 l3 : Level} {A : UU l1} 
  double-powerset l2 l3 A  powerset (l1  lsuc l2  l3) A
union-double-powerset F a =
  ∃-Prop (type-subtype F)  X  is-in-subtype (inclusion-subtype F X) a)

module _
  {l1 l2 l3 : Level} {A : UU l1} (F : double-powerset l2 l3 A)
  where

  type-union-double-powerset : UU (l1  lsuc l2  l3)
  type-union-double-powerset = type-subtype (union-double-powerset F)

  inclusion-union-double-powerset :
    (X : type-subtype F)  inclusion-subtype F X  union-double-powerset F
  inclusion-union-double-powerset X a = intro-∃ X

  universal-property-union-double-powerset :
    {l : Level} (P : powerset l A)
    (H : (X : type-subtype F)  inclusion-subtype F X  P) 
    union-double-powerset F  P
  universal-property-union-double-powerset P H a =
    map-universal-property-trunc-Prop
      ( P a)
      ( λ X  H (pr1 X) a (pr2 X))