Dirichlet products of species of types in subuniverses

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-04-27.
Last modified on 2024-02-06.

module species.dirichlet-products-species-of-types-in-subuniverses where
Imports 
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.global-subuniverses
open import foundation.homotopies
open import foundation.identity-types
open import foundation.product-decompositions
open import foundation.product-decompositions-subuniverse
open import foundation.propositions
open import foundation.subuniverses
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.unit-type
open import foundation.univalence
open import foundation.universe-levels

open import species.dirichlet-products-species-of-types
open import species.species-of-types-in-subuniverses

Idea

The Dirichlet product of two species of subuniverse S and T from P to Q on X is defined as

  Σ (k : P) (Σ (k' : P) (Σ (e : k × k' ≃ X) S(k) × T(k')))

If Q is stable by product and dependent pair type over P type, then the dirichlet product is also a species of subuniverse from P to Q

Definition

The underlying type of the Dirichlet product of species in a subuniverse

module _
  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
  (Q : global-subuniverse (λ l → l))
  where

  type-dirichlet-product-species-subuniverse :
    (S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
    (T : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
    (X : type-subuniverse P) → UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
  type-dirichlet-product-species-subuniverse S T X =
    Σ ( binary-product-Decomposition-Subuniverse P X)
      ( λ d →
        inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
          ( S (left-summand-binary-product-Decomposition-Subuniverse P X d)) ×
        inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
          ( T (right-summand-binary-product-Decomposition-Subuniverse P X d)))

Subuniverses closed under the Dirichlet product of species in a subuniverse

is-closed-under-dirichlet-product-species-subuniverse :
  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l)) →
  UUω
is-closed-under-dirichlet-product-species-subuniverse {l1} {l2} P Q =
  {l3 l4 : Level}
  (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
  (X : type-subuniverse P) →
  is-in-subuniverse
    ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
    ( type-dirichlet-product-species-subuniverse P Q S T X)

The Dirichlet product of species of types in a subuniverse

module _
  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
  (Q : global-subuniverse (λ l → l))
  ( C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
  where

  dirichlet-product-species-subuniverse :
    species-subuniverse P ( subuniverse-global-subuniverse Q l3) →
    species-subuniverse P ( subuniverse-global-subuniverse Q l4) →
    species-subuniverse P
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
  pr1 (dirichlet-product-species-subuniverse S T X) =
    type-dirichlet-product-species-subuniverse P Q S T X
  pr2 (dirichlet-product-species-subuniverse S T X) = C1 S T X

Properties

Associativity

module _
  {l1 l2 l3 l4 l5 : Level} (P : subuniverse l1 l2)
  ( Q : global-subuniverse (λ l → l))
  ( C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
  ( C2 : is-closed-under-products-subuniverse P)
  where

  module _
    (S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
    (T : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
    (U : species-subuniverse P ( subuniverse-global-subuniverse Q l5))
    (X : type-subuniverse P)
    where

    equiv-left-iterated-dirichlet-product-species-subuniverse :
      type-dirichlet-product-species-subuniverse P Q
        ( dirichlet-product-species-subuniverse P Q C1 S T)
        ( U)
        ( X) ≃
      Σ ( ternary-product-Decomposition-Subuniverse P X)
        ( λ d →
          inclusion-subuniverse
            ( subuniverse-global-subuniverse Q l3)
            ( S
              ( first-summand-ternary-product-Decomposition-Subuniverse
                P
                X
                d)) ×
            ( inclusion-subuniverse
              ( subuniverse-global-subuniverse Q l4)
              ( T
                ( second-summand-ternary-product-Decomposition-Subuniverse
                  P
                  X
                  d)) ×
              inclusion-subuniverse
                ( subuniverse-global-subuniverse Q l5)
                ( U
                  ( third-summand-ternary-product-Decomposition-Subuniverse
                    P
                    X
                    d))))
    equiv-left-iterated-dirichlet-product-species-subuniverse =
      ( ( equiv-Σ
          ( λ d →
            inclusion-subuniverse
              ( subuniverse-global-subuniverse Q l3)
              ( S
                ( first-summand-ternary-product-Decomposition-Subuniverse
                  P
                  X
                  d)) ×
            ( inclusion-subuniverse
              ( subuniverse-global-subuniverse Q l4)
              ( T
                ( second-summand-ternary-product-Decomposition-Subuniverse
                  P
                  X
                  d)) ×
              inclusion-subuniverse
                ( subuniverse-global-subuniverse Q l5)
                ( U
                  ( third-summand-ternary-product-Decomposition-Subuniverse
                    P
                    X
                    d)))))
          ( ( equiv-Σ
              ( _)
              ( associative-product _ _ _ ∘e commutative-product)
              ( λ x →
                equiv-postcomp-equiv
                  ( ( associative-product _ _ _ ∘e
                    ( commutative-product)))
                  ( inclusion-subuniverse P X)) ∘e
              equiv-ternary-left-iterated-product-Decomposition-Subuniverse
                P
                X
                C2))
          ( λ d → associative-product _ _ _) ∘e
        ( ( inv-associative-Σ
            ( binary-product-Decomposition-Subuniverse P X)
            ( λ z → binary-product-Decomposition-Subuniverse P (pr1 z))
            ( _)) ∘e
          ( ( equiv-tot λ d → right-distributive-product-Σ))))

    equiv-right-iterated-dirichlet-product-species-subuniverse :
      type-dirichlet-product-species-subuniverse P Q
        ( S)
        ( dirichlet-product-species-subuniverse P Q C1 T U)
        ( X) ≃
      Σ ( ternary-product-Decomposition-Subuniverse P X)
        ( λ d →
          inclusion-subuniverse
            ( subuniverse-global-subuniverse Q l3)
            ( S
              ( first-summand-ternary-product-Decomposition-Subuniverse
                P
                X
                d)) ×
            ( inclusion-subuniverse
              ( subuniverse-global-subuniverse Q l4)
              ( T
                ( second-summand-ternary-product-Decomposition-Subuniverse
                  P
                  X
                  d)) ×
                inclusion-subuniverse
                  ( subuniverse-global-subuniverse Q l5)
                  ( U
                    ( third-summand-ternary-product-Decomposition-Subuniverse
                      P
                      X
                      d))))
    equiv-right-iterated-dirichlet-product-species-subuniverse =
      ( ( equiv-Σ-equiv-base
          ( _)
          ( equiv-ternary-right-iterated-product-Decomposition-Subuniverse
            P
            X
            C2)) ∘e
        ( ( inv-associative-Σ
            ( binary-product-Decomposition-Subuniverse P X)
            ( λ z → binary-product-Decomposition-Subuniverse P (pr1 (pr2 z)))
            ( _)) ∘e
          ( ( equiv-tot (λ d → left-distributive-product-Σ)))))

    equiv-associative-dirichlet-product-species-subuniverse :
      type-dirichlet-product-species-subuniverse P Q
        ( dirichlet-product-species-subuniverse P Q C1 S T)
        ( U)
        ( X) ≃
      type-dirichlet-product-species-subuniverse P Q
        ( S)
        ( dirichlet-product-species-subuniverse P Q C1 T U)
        ( X)
    equiv-associative-dirichlet-product-species-subuniverse =
      inv-equiv (equiv-right-iterated-dirichlet-product-species-subuniverse) ∘e
      equiv-left-iterated-dirichlet-product-species-subuniverse

  module _
    (S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
    (T : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
    (U : species-subuniverse P ( subuniverse-global-subuniverse Q l5))
    where

    associative-dirichlet-product-species-subuniverse :
      dirichlet-product-species-subuniverse P Q C1
        ( dirichlet-product-species-subuniverse P Q C1 S T)
        ( U) ＝
      dirichlet-product-species-subuniverse P Q C1
        ( S)
        ( dirichlet-product-species-subuniverse P Q C1 T U)
    associative-dirichlet-product-species-subuniverse =
      eq-equiv-fam-subuniverse
        ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5))
        ( dirichlet-product-species-subuniverse P Q C1
          ( dirichlet-product-species-subuniverse P Q C1 S T)
          ( U))
        ( dirichlet-product-species-subuniverse P Q C1
          ( S)
          ( dirichlet-product-species-subuniverse P Q C1 T U))
        ( equiv-associative-dirichlet-product-species-subuniverse S T U)

Dirichlet product is commutative

module _
  {l1 l2 l3 l4 : Level}
  (P : subuniverse l1 l2)
  (Q : global-subuniverse (λ l → l))
  (C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
  (S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
  (T : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
  where

  equiv-commutative-dirichlet-product-species-subuniverse :
    (X : type-subuniverse P) →
    type-dirichlet-product-species-subuniverse P Q S T X ≃
    type-dirichlet-product-species-subuniverse P Q T S X
  equiv-commutative-dirichlet-product-species-subuniverse X =
    equiv-Σ
      ( λ d →
        inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
          ( T (left-summand-binary-product-Decomposition-Subuniverse P X d)) ×
        inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
          ( S (right-summand-binary-product-Decomposition-Subuniverse P X d)))
      ( equiv-commutative-binary-product-Decomposition-Subuniverse P X)
      ( λ _ → commutative-product)

  commutative-dirichlet-product-species-subuniverse :
    dirichlet-product-species-subuniverse P Q C1 S T ＝
    dirichlet-product-species-subuniverse P Q C1 T S
  commutative-dirichlet-product-species-subuniverse =
    eq-equiv-fam-subuniverse
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
      ( dirichlet-product-species-subuniverse P Q C1 S T)
      ( dirichlet-product-species-subuniverse P Q C1 T S)
      ( equiv-commutative-dirichlet-product-species-subuniverse)

Unit laws of Dirichlet product

unit-dirichlet-product-species-subuniverse :
  {l1 l2 l3 : Level} →
  (P : subuniverse l1 l2) (Q : subuniverse l1 l3) →
  ( (X : type-subuniverse P) →
    is-in-subuniverse Q ( is-contr (inclusion-subuniverse P X))) →
  species-subuniverse P Q
unit-dirichlet-product-species-subuniverse P Q C X =
  is-contr (inclusion-subuniverse P X) , C X

module _
  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l))
  (C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
  (C2 : is-in-subuniverse P (raise-unit l1))
  (C3 :
    (X : type-subuniverse P) →
    is-in-subuniverse
      ( subuniverse-global-subuniverse Q l1)
      ( is-contr (inclusion-subuniverse P X)))
  (S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
  where

  equiv-right-unit-law-dirichlet-product-species-subuniverse :
    (X : type-subuniverse P) →
    type-dirichlet-product-species-subuniverse P Q
      ( S)
      ( unit-dirichlet-product-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q l1)
        ( C3))
      ( X) ≃
    inclusion-subuniverse (subuniverse-global-subuniverse Q l3) (S X)
  equiv-right-unit-law-dirichlet-product-species-subuniverse X =
    ( ( left-unit-law-Σ-is-contr
        ( is-torsorial-equiv-subuniverse P X)
        ( X , id-equiv)) ∘e
      ( ( equiv-Σ-equiv-base
          ( λ p →
            inclusion-subuniverse
              ( subuniverse-global-subuniverse Q l3)
              ( S (pr1 (p))))
          (equiv-is-contr-right-summand-binary-product-Decomposition-Subuniverse
            P
            X
            C2)) ∘e
        ( ( inv-associative-Σ
            ( binary-product-Decomposition-Subuniverse P X)
            ( λ d →
              inclusion-subuniverse
                ( subuniverse-global-subuniverse Q l1)
                ( unit-dirichlet-product-species-subuniverse
                  ( P)
                  ( subuniverse-global-subuniverse Q l1)
                  ( C3)
                  ( right-summand-binary-product-Decomposition-Subuniverse
                    P
                    X
                    d)))
            ( λ z →
              inclusion-subuniverse
                ( subuniverse-global-subuniverse Q l3)
                ( S
                  ( left-summand-binary-product-Decomposition-Subuniverse
                    P
                    X
                    (pr1 z))))) ∘e
          ( ( equiv-tot (λ _ → commutative-product))))))

  equiv-left-unit-law-dirichlet-product-species-subuniverse :
    (X : type-subuniverse P) →
    type-dirichlet-product-species-subuniverse P Q
      ( unit-dirichlet-product-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q l1)
        ( C3))
      ( S)
      ( X) ≃
    inclusion-subuniverse (subuniverse-global-subuniverse Q l3) (S X)
  equiv-left-unit-law-dirichlet-product-species-subuniverse X =
    equiv-right-unit-law-dirichlet-product-species-subuniverse X ∘e
    equiv-commutative-dirichlet-product-species-subuniverse
      ( P)
      ( Q)
      ( C1)
      ( unit-dirichlet-product-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q l1)
        ( C3))
      ( S)
      ( X)

Equivalent form with species of types

module _
  {l1 l2 l3 l4 : Level} (P : subuniverse l1 l2)
  ( Q : global-subuniverse (λ l → l))
  ( C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
  ( C2 : is-closed-under-products-subuniverse P)
  (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
  (X : UU l1)
  where

  private
    reassociate :
      Σ-extension-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
        ( dirichlet-product-species-subuniverse P Q C1 S T)
        ( X) ≃
      Σ ( binary-product-Decomposition l1 l1 X)
        ( λ (A , B , e) →
          Σ ( ( is-in-subuniverse P A × is-in-subuniverse P B) ×
              is-in-subuniverse P X)
            ( λ ((pA , pB) , pX) →
              inclusion-subuniverse
                ( subuniverse-global-subuniverse Q l3)
                ( S (A , pA)) ×
              inclusion-subuniverse
                ( subuniverse-global-subuniverse Q l4)
                ( T (B , pB))))
    pr1 reassociate (pX , ((A , pA) , (B , pB) , e) , s , t) =
      (A , B , e) , ((pA , pB) , pX) , (s , t)
    pr2 reassociate = is-equiv-is-invertible
      ( λ ((A , B , e) , ((pA , pB) , pX) , (s , t)) →
        ( pX , ((A , pA) , (B , pB) , e) , s , t))
      ( refl-htpy)
      ( refl-htpy)

    reassociate' :
      Σ ( binary-product-Decomposition l1 l1 X)
        ( λ d →
          Σ ( Σ (pr1 (P (pr1 d))) (λ v → pr1 (P (pr1 (pr2 d)))))
          (λ p → pr1 (S (pr1 d , pr1 p)) × pr1 (T (pr1 (pr2 d) , pr2 p))))
      ≃
      dirichlet-product-species-types
        ( Σ-extension-species-subuniverse P
          ( subuniverse-global-subuniverse Q l3) S)
        ( Σ-extension-species-subuniverse P
          ( subuniverse-global-subuniverse Q l4) T)
        ( X)
    pr1 reassociate' (d , (pA , pB) , s , t) =
      d , (pA , s) , (pB , t)
    pr2 reassociate' =
      is-equiv-is-invertible
        ( λ ( d , (pA , s) , (pB , t)) → (d , (pA , pB) , s , t))
        ( refl-htpy)
        ( refl-htpy)

  equiv-dirichlet-product-Σ-extension-species-subuniverse :
    Σ-extension-species-subuniverse
      ( P)
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
      ( dirichlet-product-species-subuniverse P Q C1 S T)
      ( X) ≃
    dirichlet-product-species-types
      ( Σ-extension-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q l3)
        ( S))
      ( Σ-extension-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q l4)
        ( T))
      ( X)
  equiv-dirichlet-product-Σ-extension-species-subuniverse =
    ( ( reassociate') ∘e
      ( ( equiv-tot
          ( λ d →
            equiv-Σ-equiv-base
              (λ p →
                  ( inclusion-subuniverse
                    ( subuniverse-global-subuniverse Q l3)
                    ( S
                      ( left-summand-binary-product-Decomposition d ,
                        pr1 p))) ×
                  ( inclusion-subuniverse
                    ( subuniverse-global-subuniverse Q l4)
                    ( T
                      ( right-summand-binary-product-Decomposition d ,
                        pr2 p))))
              ( inv-equiv
                ( equiv-add-redundant-prop
                  ( is-prop-type-Prop (P X))
                  ( λ p →
                    tr
                      ( is-in-subuniverse P)
                      ( inv
                        ( eq-equiv
                          ( matching-correspondence-binary-product-Decomposition
                            ( d))))
                      ( C2
                        ( pr1 p)
                        ( pr2 p))))))) ∘e
        ( reassociate)))

Recent changes