Partitions

module foundation.partitions where
Imports
open import foundation.contractible-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.fiber-inclusions
open import foundation.identity-types
open import foundation.inhabited-subtypes
open import foundation.inhabited-types
open import foundation.locally-small-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.sigma-decompositions
open import foundation.small-types
open import foundation.subtypes
open import foundation.surjective-maps

open import foundation-core.cartesian-product-types
open import foundation-core.dependent-pair-types
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.fundamental-theorem-of-identity-types
open import foundation-core.homotopies
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.subtype-identity-principle
open import foundation-core.type-arithmetic-dependent-pair-types
open import foundation-core.universe-levels

Idea

A partition of a type A is a subset P of the type of inhabited subsets of A such that for each a : A the type

  Σ (Q : inhabited-subtype (A)), P(Q) × Q(a)

is contractible. In other words, it is a collection P of inhabited subtypes of A such that each element of A is in a unique inhabited subtype in P.

Definition

is-partition-Prop :
  {l1 l2 l3 : Level} {A : UU l1} (P : subtype l3 (inhabited-subtype l2 A)) 
  Prop (l1  lsuc l2  l3)
is-partition-Prop {l1} {l2} {l3} {A} P =
  Π-Prop A
    ( λ x 
      is-contr-Prop
        ( Σ ( type-subtype P)
            ( λ Q  is-in-inhabited-subtype (inclusion-subtype P Q) x)))

is-partition :
  {l1 l2 l3 : Level} {A : UU l1} (P : subtype l3 (inhabited-subtype l2 A)) 
  UU (l1  lsuc l2  l3)
is-partition P = type-Prop (is-partition-Prop P)

partition :
  {l1 : Level} (l2 l3 : Level)  UU l1  UU (l1  lsuc l2  lsuc l3)
partition {l1} l2 l3 A = type-subtype (is-partition-Prop {l1} {l2} {l3} {A})

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

  subtype-partition : subtype l3 (inhabited-subtype l2 A)
  subtype-partition = pr1 P

  is-partition-subtype-partition : is-partition subtype-partition
  is-partition-subtype-partition = pr2 P

  is-block-partition : inhabited-subtype l2 A  UU l3
  is-block-partition = is-in-subtype subtype-partition

  is-prop-is-block-partition :
    (Q : inhabited-subtype l2 A)  is-prop (is-block-partition Q)
  is-prop-is-block-partition = is-prop-is-in-subtype subtype-partition

We introduce the type of blocks of a partition. However, we will soon be able to reduce the universe level of this type. Therefore we call this type of blocks large.

  block-partition-Large-Type : UU (l1  lsuc l2  l3)
  block-partition-Large-Type = type-subtype subtype-partition

  inhabited-subtype-block-partition-Large-Type :
    block-partition-Large-Type  inhabited-subtype l2 A
  inhabited-subtype-block-partition-Large-Type =
    inclusion-subtype subtype-partition

  is-emb-inhabited-subtype-block-partition-Large-Type :
    is-emb inhabited-subtype-block-partition-Large-Type
  is-emb-inhabited-subtype-block-partition-Large-Type =
    is-emb-inclusion-subtype subtype-partition

  emb-inhabited-subtype-block-partition-Large-Type :
    block-partition-Large-Type  inhabited-subtype l2 A
  emb-inhabited-subtype-block-partition-Large-Type =
    emb-subtype subtype-partition

  is-block-inhabited-subtype-block-partition-Large-Type :
    (B : block-partition-Large-Type) 
    is-block-partition (inhabited-subtype-block-partition-Large-Type B)
  is-block-inhabited-subtype-block-partition-Large-Type =
    is-in-subtype-inclusion-subtype subtype-partition

  subtype-block-partition-Large-Type :
    block-partition-Large-Type  subtype l2 A
  subtype-block-partition-Large-Type =
    subtype-inhabited-subtype  inhabited-subtype-block-partition-Large-Type

  is-inhabited-subtype-block-partition-Large-Type :
    (B : block-partition-Large-Type) 
    is-inhabited-subtype (subtype-block-partition-Large-Type B)
  is-inhabited-subtype-block-partition-Large-Type B =
    is-inhabited-subtype-inhabited-subtype
      ( inhabited-subtype-block-partition-Large-Type B)

  type-block-partition-Large-Type : block-partition-Large-Type  UU (l1  l2)
  type-block-partition-Large-Type Q =
    type-inhabited-subtype (inhabited-subtype-block-partition-Large-Type Q)

  inhabited-type-block-partition-Large-Type :
    block-partition-Large-Type  Inhabited-Type (l1  l2)
  inhabited-type-block-partition-Large-Type Q =
    inhabited-type-inhabited-subtype
      ( inhabited-subtype-block-partition-Large-Type Q)

  is-in-block-partition-Large-Type : block-partition-Large-Type  A  UU l2
  is-in-block-partition-Large-Type Q =
    is-in-inhabited-subtype (inhabited-subtype-block-partition-Large-Type Q)

  is-prop-is-in-block-partition-Large-Type :
    (Q : block-partition-Large-Type) (a : A) 
    is-prop (is-in-block-partition-Large-Type Q a)
  is-prop-is-in-block-partition-Large-Type Q =
    is-prop-is-in-inhabited-subtype
      ( inhabited-subtype-block-partition-Large-Type Q)

  large-block-element-partition : A  block-partition-Large-Type
  large-block-element-partition a =
    pr1 (center (is-partition-subtype-partition a))

  is-surjective-large-block-element-partition :
    is-surjective large-block-element-partition
  is-surjective-large-block-element-partition B =
    apply-universal-property-trunc-Prop
      ( is-inhabited-subtype-block-partition-Large-Type B)
      ( trunc-Prop (fib large-block-element-partition B))
      ( λ (a , u) 
        unit-trunc-Prop
          ( pair a
            ( eq-type-subtype
              ( subtype-partition)
              ( ap pr1
                ( ap
                  ( inclusion-subtype
                    ( λ Q  subtype-inhabited-subtype (pr1 Q) a))
                  ( contraction
                    ( is-partition-subtype-partition a)
                    ( pair B u)))))))

  is-locally-small-block-partition-Large-Type :
    is-locally-small (l1  l2) block-partition-Large-Type
  is-locally-small-block-partition-Large-Type =
    is-locally-small-type-subtype
      ( subtype-partition)
      ( is-locally-small-inhabited-subtype is-small')

  is-small-block-partition-Large-Type :
    is-small (l1  l2) block-partition-Large-Type
  is-small-block-partition-Large-Type =
    is-small-is-surjective
      ( is-surjective-large-block-element-partition)
      ( is-small-lmax l2 A)
      ( is-locally-small-block-partition-Large-Type)

The (small) type of blocks of a partition

We will now introduce the type of blocks of a partition, and show that the type of blocks containing a fixed element a is contractible. Once this is done, we will have no more use for the large type of blocks of a partition.

  block-partition : UU (l1  l2)
  block-partition = type-is-small is-small-block-partition-Large-Type

  compute-block-partition : block-partition-Large-Type  block-partition
  compute-block-partition = equiv-is-small is-small-block-partition-Large-Type

  map-compute-block-partition : block-partition-Large-Type  block-partition
  map-compute-block-partition = map-equiv compute-block-partition

  make-block-partition :
    (Q : inhabited-subtype l2 A)  is-block-partition Q  block-partition
  make-block-partition Q H = map-compute-block-partition (pair Q H)

  map-inv-compute-block-partition : block-partition  block-partition-Large-Type
  map-inv-compute-block-partition =
    map-inv-equiv compute-block-partition

  issec-map-inv-compute-block-partition :
    ( map-compute-block-partition  map-inv-compute-block-partition) ~ id
  issec-map-inv-compute-block-partition =
    issec-map-inv-equiv compute-block-partition

  isretr-map-inv-compute-block-partition :
    ( map-inv-compute-block-partition  map-compute-block-partition) ~ id
  isretr-map-inv-compute-block-partition =
    isretr-map-inv-equiv compute-block-partition

  inhabited-subtype-block-partition : block-partition  inhabited-subtype l2 A
  inhabited-subtype-block-partition =
    inhabited-subtype-block-partition-Large-Type 
    map-inv-compute-block-partition

  is-emb-inhabited-subtype-block-partition :
    is-emb inhabited-subtype-block-partition
  is-emb-inhabited-subtype-block-partition =
    is-emb-comp
      ( inhabited-subtype-block-partition-Large-Type)
      ( map-inv-compute-block-partition)
      ( is-emb-inhabited-subtype-block-partition-Large-Type)
      ( is-emb-is-equiv (is-equiv-map-inv-equiv compute-block-partition))

  emb-inhabited-subtype-block-partition :
    block-partition  inhabited-subtype l2 A
  pr1 emb-inhabited-subtype-block-partition = inhabited-subtype-block-partition
  pr2 emb-inhabited-subtype-block-partition =
    is-emb-inhabited-subtype-block-partition

  is-block-inhabited-subtype-block-partition :
    (B : block-partition) 
    is-block-partition (inhabited-subtype-block-partition B)
  is-block-inhabited-subtype-block-partition B =
    is-block-inhabited-subtype-block-partition-Large-Type
      ( map-inv-compute-block-partition B)

  subtype-block-partition : block-partition  subtype l2 A
  subtype-block-partition =
    subtype-block-partition-Large-Type  map-inv-compute-block-partition

  inhabited-type-block-partition : block-partition  Inhabited-Type (l1  l2)
  inhabited-type-block-partition B =
    inhabited-type-block-partition-Large-Type
      ( map-inv-compute-block-partition B)

  is-inhabited-subtype-block-partition :
    (B : block-partition)  is-inhabited-subtype (subtype-block-partition B)
  is-inhabited-subtype-block-partition B =
    is-inhabited-subtype-block-partition-Large-Type
      ( map-inv-compute-block-partition B)

  type-block-partition : block-partition  UU (l1  l2)
  type-block-partition B =
    type-block-partition-Large-Type (map-inv-compute-block-partition B)

  is-in-block-partition : (B : block-partition)  A  UU l2
  is-in-block-partition B =
    is-in-block-partition-Large-Type (map-inv-compute-block-partition B)

  is-prop-is-in-block-partition :
    (B : block-partition) (a : A)  is-prop (is-in-block-partition B a)
  is-prop-is-in-block-partition B =
    is-prop-is-in-block-partition-Large-Type
      ( map-inv-compute-block-partition B)

  compute-is-in-block-partition :
    (B : inhabited-subtype l2 A) (H : is-block-partition B) (x : A) 
    is-in-inhabited-subtype B x 
    is-in-block-partition (make-block-partition B H) x
  compute-is-in-block-partition B H x =
    equiv-tr
      ( λ C  is-in-block-partition-Large-Type C x)
      ( inv (isretr-map-inv-compute-block-partition (B , H)))

  make-is-in-block-partition :
    (B : inhabited-subtype l2 A) (H : is-block-partition B) (x : A) 
    is-in-inhabited-subtype B x 
    is-in-block-partition (make-block-partition B H) x
  make-is-in-block-partition B H x K =
    map-equiv (compute-is-in-block-partition B H x) K

  block-containing-element-partition : A  UU (l1  l2)
  block-containing-element-partition a =
    Σ block-partition  B  is-in-block-partition B a)

  is-contr-block-containing-element-partition :
    (a : A)  is-contr (block-containing-element-partition a)
  is-contr-block-containing-element-partition a =
    is-contr-equiv'
      ( Σ block-partition-Large-Type
        ( λ B  is-in-block-partition-Large-Type B a))
      ( equiv-Σ
        ( λ B  is-in-block-partition B a)
        ( compute-block-partition)
        ( λ B 
          equiv-tr
            ( λ C  is-in-block-partition-Large-Type C a)
            ( inv (isretr-map-inv-compute-block-partition B))))
      ( is-partition-subtype-partition a)

  center-block-containing-element-partition :
    (a : A)  block-containing-element-partition a
  center-block-containing-element-partition a =
    center (is-contr-block-containing-element-partition a)

  class-partition : A  block-partition
  class-partition a =
    pr1 (center-block-containing-element-partition a)

  is-block-class-partition :
    (a : A) 
    is-block-partition (inhabited-subtype-block-partition (class-partition a))
  is-block-class-partition a =
    is-block-inhabited-subtype-block-partition (class-partition a)

  is-in-block-class-partition :
    (a : A)  is-in-block-partition (class-partition a) a
  is-in-block-class-partition a =
    pr2 (center-block-containing-element-partition a)

  compute-base-type-partition : Σ block-partition type-block-partition  A
  compute-base-type-partition =
    ( right-unit-law-Σ-is-contr
      ( λ x  is-contr-block-containing-element-partition x)) ∘e
    ( equiv-left-swap-Σ)

Properties

Characterizing equality of partitions

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

  has-same-blocks-partition :
    {l4 : Level} (Q : partition l2 l4 A)  UU (l1  lsuc l2  l3  l4)
  has-same-blocks-partition Q =
    has-same-elements-subtype (subtype-partition P) (subtype-partition Q)

  refl-has-same-blocks-partition : has-same-blocks-partition P
  refl-has-same-blocks-partition =
    refl-has-same-elements-subtype (subtype-partition P)

  extensionality-partition :
    (Q : partition l2 l3 A)  (P  Q)  has-same-blocks-partition Q
  extensionality-partition =
    extensionality-type-subtype
      ( is-partition-Prop)
      ( is-partition-subtype-partition P)
      ( refl-has-same-elements-subtype (subtype-partition P))
      ( extensionality-subtype (subtype-partition P))

  eq-has-same-blocks-partition :
    (Q : partition l2 l3 A)  has-same-blocks-partition Q  P  Q
  eq-has-same-blocks-partition Q =
    map-inv-equiv (extensionality-partition Q)

Characterizing equality of blocks of partitions

module _
  {l1 l2 l3 : Level} {A : UU l1} (P : partition l2 l3 A) (B : block-partition P)
  where

  has-same-elements-block-partition-Prop :
    block-partition P  Prop (l1  l2)
  has-same-elements-block-partition-Prop C =
    has-same-elements-inhabited-subtype-Prop
      ( inhabited-subtype-block-partition P B)
      ( inhabited-subtype-block-partition P C)

  has-same-elements-block-partition :
    block-partition P  UU (l1  l2)
  has-same-elements-block-partition C =
    has-same-elements-inhabited-subtype
      ( inhabited-subtype-block-partition P B)
      ( inhabited-subtype-block-partition P C)

  is-prop-has-same-elements-block-partition :
    (C : block-partition P)  is-prop (has-same-elements-block-partition C)
  is-prop-has-same-elements-block-partition C =
    is-prop-has-same-elements-inhabited-subtype
      ( inhabited-subtype-block-partition P B)
      ( inhabited-subtype-block-partition P C)

  refl-has-same-elements-block-partition :
    has-same-elements-block-partition B
  refl-has-same-elements-block-partition =
    refl-has-same-elements-inhabited-subtype
      ( inhabited-subtype-block-partition P B)

  is-contr-total-has-same-elements-block-partition :
    is-contr
      ( Σ (block-partition P) has-same-elements-block-partition)
  is-contr-total-has-same-elements-block-partition =
    is-contr-equiv'
      ( Σ ( block-partition P)
          ( λ C 
            inhabited-subtype-block-partition P B 
            inhabited-subtype-block-partition P C))
      ( equiv-tot
        ( λ C 
          extensionality-inhabited-subtype
            ( inhabited-subtype-block-partition P B)
            ( inhabited-subtype-block-partition P C)))
      ( fundamental-theorem-id'
        ( λ C  ap (inhabited-subtype-block-partition P))
        ( is-emb-inhabited-subtype-block-partition P B))

  has-same-elements-eq-block-partition :
    (C : block-partition P)  (B  C) 
    has-same-elements-block-partition C
  has-same-elements-eq-block-partition .B refl =
    refl-has-same-elements-block-partition

  is-equiv-has-same-elements-eq-block-partition :
    (C : block-partition P) 
    is-equiv (has-same-elements-eq-block-partition C)
  is-equiv-has-same-elements-eq-block-partition =
    fundamental-theorem-id
      is-contr-total-has-same-elements-block-partition
      has-same-elements-eq-block-partition

  extensionality-block-partition :
    (C : block-partition P) 
    (B  C)  has-same-elements-block-partition C
  pr1 (extensionality-block-partition C) =
    has-same-elements-eq-block-partition C
  pr2 (extensionality-block-partition C) =
    is-equiv-has-same-elements-eq-block-partition C

  eq-has-same-elements-block-partition :
    (C : block-partition P) 
    has-same-elements-block-partition C  B  C
  eq-has-same-elements-block-partition C =
    map-inv-equiv (extensionality-block-partition C)

The type of blocks of a partition is a set

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

  is-set-block-partition : is-set (block-partition P)
  is-set-block-partition B C =
    is-prop-equiv
      ( extensionality-block-partition P B C)
      ( is-prop-has-same-elements-block-partition P B C)

  block-partition-Set : Set (l1  l2)
  pr1 block-partition-Set = block-partition P
  pr2 block-partition-Set = is-set-block-partition

The inclusion of a block into the base type of a partition is an embedding

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

  emb-inclusion-block-partition :
    (B : block-partition P)  type-block-partition P B  A
  emb-inclusion-block-partition B =
    comp-emb
      ( emb-equiv (compute-base-type-partition P))
      ( emb-fiber-inclusion
        ( type-block-partition P)
        ( is-set-block-partition P)
        ( B))

Two blocks of a partition are equal if they share a common element

module _
  {l1 l2 l3 : Level} {A : UU l1} (P : partition l2 l3 A)
  (B : block-partition P)
  where

  share-common-element-block-partition-Prop :
    (C : block-partition P)  Prop (l1  l2)
  share-common-element-block-partition-Prop C =
    ∃-Prop A
      ( λ a 
        is-in-block-partition P B a × is-in-block-partition P C a)

  share-common-element-block-partition :
    (C : block-partition P)  UU (l1  l2)
  share-common-element-block-partition C =
    type-Prop (share-common-element-block-partition-Prop C)

  eq-share-common-element-block-partition :
    (C : block-partition P)  share-common-element-block-partition C  B  C
  eq-share-common-element-block-partition C H =
    apply-universal-property-trunc-Prop H
      ( Id-Prop (block-partition-Set P) B C)
      ( λ (a , K , L) 
        ap
          ( pr1)
          ( eq-is-contr
            ( is-contr-block-containing-element-partition P a)
            { B , K}
            { C , L}))

The condition of being a partition is equivalent to the condition that the total space of all blocks is equivalent to the base type

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

  compute-total-block-partition :
    Σ (block-partition P) (type-block-partition P)  A
  compute-total-block-partition =
    ( right-unit-law-Σ-is-contr
      ( is-contr-block-containing-element-partition P)) ∘e
    ( equiv-left-swap-Σ)

  map-compute-total-block-partition :
    Σ (block-partition P) (type-block-partition P)  A
  map-compute-total-block-partition = map-equiv compute-total-block-partition

The type of partitions of A is equivalent to the type of set-indexed Σ-decompositions of A

The set-indexed Σ-decomposition obtained from a partition

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

  set-indexed-Σ-decomposition-partition :
    Set-Indexed-Σ-Decomposition (l1  l2) (l1  l2) A
  pr1 set-indexed-Σ-decomposition-partition = block-partition-Set P
  pr1 (pr2 set-indexed-Σ-decomposition-partition) =
    inhabited-type-block-partition P
  pr2 (pr2 set-indexed-Σ-decomposition-partition) =
    inv-equiv (compute-total-block-partition P)

The partition obtained from a set-indexed Σ-decomposition

module _
  {l1 l2 l3 : Level} {A : UU l1} (D : Set-Indexed-Σ-Decomposition l2 l3 A)
  where

  is-block-partition-Set-Indexed-Σ-Decomposition :
    {l4 : Level}  inhabited-subtype l4 A  UU (l1  l2  l4)
  is-block-partition-Set-Indexed-Σ-Decomposition Q =
    Σ ( indexing-type-Set-Indexed-Σ-Decomposition D)
      ( λ i 
        (x : A) 
        ( is-in-inhabited-subtype Q x) 
        ( index-Set-Indexed-Σ-Decomposition D x  i))

  is-prop-is-block-partition-Set-Indexed-Σ-Decomposition :
    {l4 : Level} (Q : inhabited-subtype l4 A) 
    is-prop (is-block-partition-Set-Indexed-Σ-Decomposition Q)
  is-prop-is-block-partition-Set-Indexed-Σ-Decomposition Q =
    apply-universal-property-trunc-Prop
      ( is-inhabited-subtype-inhabited-subtype Q)
      ( is-prop-Prop (is-block-partition-Set-Indexed-Σ-Decomposition Q))
      ( λ (a , q) 
        is-prop-all-elements-equal
          ( λ (i , H) (j , K) 
            eq-type-subtype
            ( λ u 
              Π-Prop A
              ( λ x 
                equiv-Prop
                ( subtype-inhabited-subtype Q x)
                  ( Id-Prop
                    ( indexing-set-Set-Indexed-Σ-Decomposition D)
                    ( pr1
                      ( map-matching-correspondence-Set-Indexed-Σ-Decomposition
                        D x))
                    ( u))))
            ( inv (map-equiv (H a) q)  map-equiv (K a) q)))

  subtype-partition-Set-Indexed-Σ-Decomposition :
    {l4 : Level}  subtype (l1  l2  l4) (inhabited-subtype l4 A)
  pr1 (subtype-partition-Set-Indexed-Σ-Decomposition Q) =
    is-block-partition-Set-Indexed-Σ-Decomposition Q
  pr2 (subtype-partition-Set-Indexed-Σ-Decomposition Q) =
    is-prop-is-block-partition-Set-Indexed-Σ-Decomposition Q

  is-partition-subtype-partition-Set-Indexed-Σ-Decomposition :
    is-partition (subtype-partition-Set-Indexed-Σ-Decomposition {l2})
  is-partition-subtype-partition-Set-Indexed-Σ-Decomposition a =
    is-contr-equiv
      ( Σ ( inhabited-subtype l2 A)
          ( has-same-elements-inhabited-subtype
              ( pair
                ( λ x 
                  Id-Prop
                    ( indexing-set-Set-Indexed-Σ-Decomposition D)
                    ( index-Set-Indexed-Σ-Decomposition D x)
                    ( index-Set-Indexed-Σ-Decomposition D a))
                ( unit-trunc-Prop (pair a refl)))))
      ( ( equiv-tot
          ( λ Q 
            ( ( ( equiv-map-Π
                  ( λ x 
                    inv-equiv
                      ( equiv-equiv-iff
                        ( Id-Prop
                          ( indexing-set-Set-Indexed-Σ-Decomposition D)
                          ( index-Set-Indexed-Σ-Decomposition D x)
                          ( index-Set-Indexed-Σ-Decomposition D a))
                        ( subtype-inhabited-subtype Q x)) ∘e
                    ( equiv-inv-equiv))) ∘e
                ( left-unit-law-Σ-is-contr
                  ( is-contr-total-path (index-Set-Indexed-Σ-Decomposition D a))
                  ( pair
                    ( index-Set-Indexed-Σ-Decomposition D a)
                    ( refl)))) ∘e
              ( equiv-right-swap-Σ)) ∘e
            ( equiv-tot  ie  pr2 ie a)))) ∘e
        ( associative-Σ
          ( inhabited-subtype l2 A)
          ( is-block-partition-Set-Indexed-Σ-Decomposition)
          ( λ B  is-in-inhabited-subtype (pr1 B) a)))
      ( is-contr-total-has-same-elements-inhabited-subtype
        ( pair
          ( λ x 
            Id-Prop
              ( indexing-set-Set-Indexed-Σ-Decomposition D)
              ( index-Set-Indexed-Σ-Decomposition D x)
              ( index-Set-Indexed-Σ-Decomposition D a))
          ( unit-trunc-Prop (pair a refl))))

partition-Set-Indexed-Σ-Decomposition :
  {l1 l2 l3 : Level} {A : UU l1} 
  Set-Indexed-Σ-Decomposition l2 l3 A  partition l2 (l1  l2) A
pr1 (partition-Set-Indexed-Σ-Decomposition D) =
  subtype-partition-Set-Indexed-Σ-Decomposition D
pr2 (partition-Set-Indexed-Σ-Decomposition D) =
  is-partition-subtype-partition-Set-Indexed-Σ-Decomposition D

The partition obtained from the set-indexed Σ-decomposition induced by a partition has the same blocks as the original partition

-- module _
--   {l1 l2 l3 : Level} {A : UU l1} (P : partition (l1 ⊔ l2) l3 A)
--   where

--   is-block-is-block-partition-set-indexed-Σ-decomposition-partition :
--     ( Q : inhabited-subtype (l1 ⊔ l2) A) →
--     is-block-partition
--       ( partition-Set-Indexed-Σ-Decomposition
--         ( set-indexed-Σ-decomposition-partition P))
--       ( Q) →
--     is-block-partition P Q
--   is-block-is-block-partition-set-indexed-Σ-decomposition-partition Q (i , H) =
--     apply-universal-property-trunc-Prop
--       ( is-inhabited-subtype-inhabited-subtype Q)
--       ( subtype-partition P Q)
--       ( λ (a , q) → {!  !})

{-  i : X  H : (x : A) → Q x ≃ (pr1 (inv-equiv
(compute-total-block-partition P) x) = i)  a : A  q : Q a

 H a q : pr1 (inv-equiv (compute-total-block-partition P) a) = i

 H' : (B : block)  -}

--   is-block-partition-set-indexed-Σ-decomposition-is-block-partition :
--     ( Q : inhabited-subtype (l1 ⊔ l2) A) →
--     is-block-partition P Q →
--     is-block-partition
--       ( partition-Set-Indexed-Σ-Decomposition
--         ( set-indexed-Σ-decomposition-partition P))
--       ( Q)
--   is-block-partition-set-indexed-Σ-decomposition-is-block-partition Q H = {!  !}
--
--   has-same-blocks-partition-set-indexed-Σ-decomposition-partition :
--     has-same-blocks-partition
--       ( partition-Set-Indexed-Σ-Decomposition
--         ( set-indexed-Σ-decomposition-partition P))
--       ( P)
--   pr1 (has-same-blocks-partition-set-indexed-Σ-decomposition-partition B) =
--     is-block-is-block-partition-set-indexed-Σ-decomposition-partition B
--   pr2 (has-same-blocks-partition-set-indexed-Σ-decomposition-partition B) =
--     is-block-partition-set-indexed-Σ-decomposition-is-block-partition B