Cauchy products of species of types in a subuniverse

Content created by Fredrik Bakke and Egbert Rijke.

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

module species.cauchy-products-species-of-types-in-subuniverses where
Imports 
open import foundation.cartesian-product-types
open import foundation.coproduct-decompositions
open import foundation.coproduct-decompositions-subuniverse
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-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.propositions
open import foundation.subuniverses
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.univalence
open import foundation.universe-levels

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

Idea

The Cauchy product of two species S and T from P to Q of types in a subuniverse is defined by

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

If Q is closed under products and dependent pair types over types in P, then the Cauchy product is also a species of subuniverse from P to Q.

Definition

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

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

  type-cauchy-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-cauchy-product-species-subuniverse S T X =
    Σ ( binary-coproduct-Decomposition-subuniverse P X)
      ( λ d →
        inclusion-subuniverse
          ( subuniverse-global-subuniverse Q l3)
          ( S (left-summand-binary-coproduct-Decomposition-subuniverse P X d)) ×
        inclusion-subuniverse
          ( subuniverse-global-subuniverse Q l4)
          ( T (right-summand-binary-coproduct-Decomposition-subuniverse P X d)))

Subuniverses closed under the Cauchy product of species in a subuniverse

is-closed-under-cauchy-product-species-subuniverse :
  {l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse (λ l → l)) →
  UUω
is-closed-under-cauchy-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-cauchy-product-species-subuniverse P Q S T X)

The Cauchy product of species in a subuniverse

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

  cauchy-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 (cauchy-product-species-subuniverse S T X) =
    type-cauchy-product-species-subuniverse P Q S T X
  pr2 (cauchy-product-species-subuniverse S T X) = C1 S T X

Properties

Cauchy product is associative

module _
  {l1 l2 l3 l4 l5 : Level} (P : subuniverse l1 l2)
  (Q : global-subuniverse (λ l → l))
  ( C1 : is-closed-under-cauchy-product-species-subuniverse P Q)
  ( C2 : is-closed-under-coproducts-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-cauchy-product-species-subuniverse :
      type-cauchy-product-species-subuniverse P Q
        ( cauchy-product-species-subuniverse P Q C1 S T)
        ( U)
        ( X) ≃
      Σ ( ternary-coproduct-Decomposition-subuniverse P X)
        ( λ d →
          inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
            ( S
              ( first-summand-ternary-coproduct-Decomposition-subuniverse
                P X d)) ×
            ( inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
              ( T
                ( second-summand-ternary-coproduct-Decomposition-subuniverse
                  P X d)) ×
              inclusion-subuniverse ( subuniverse-global-subuniverse Q l5)
              ( U
                ( third-summand-ternary-coproduct-Decomposition-subuniverse
                  P X d))))
    equiv-left-iterated-cauchy-product-species-subuniverse =
      ( ( equiv-Σ
          ( λ d →
            inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
            ( S
              ( first-summand-ternary-coproduct-Decomposition-subuniverse
                  P X d)) ×
            ( inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
              ( T
                ( second-summand-ternary-coproduct-Decomposition-subuniverse
                    P X d)) ×
              inclusion-subuniverse ( subuniverse-global-subuniverse Q l5)
              ( U
                ( third-summand-ternary-coproduct-Decomposition-subuniverse
                    P X d)))))
          ( ( equiv-Σ
              ( _)
              ( associative-product _ _ _ ∘e commutative-product)
              ( λ x →
                equiv-postcomp-equiv
                  ( ( ( associative-coproduct) ∘e
                    ( ( commutative-coproduct _ _))))
                  ( inclusion-subuniverse P X)) ∘e
              equiv-ternary-left-iterated-coproduct-Decomposition-subuniverse
                P X C2))
          ( λ d → associative-product _ _ _) ∘e
        ( ( inv-associative-Σ
            ( binary-coproduct-Decomposition-subuniverse P X)
            ( λ z → binary-coproduct-Decomposition-subuniverse P (pr1 z))
            ( _)) ∘e
          ( ( equiv-tot λ d → right-distributive-product-Σ))))

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

    equiv-associative-cauchy-product-species-subuniverse :
      type-cauchy-product-species-subuniverse P Q
        ( cauchy-product-species-subuniverse P Q C1 S T)
        ( U)
        ( X) ≃
      type-cauchy-product-species-subuniverse P Q
        ( S)
        ( cauchy-product-species-subuniverse P Q C1 T U)
        ( X)
    equiv-associative-cauchy-product-species-subuniverse =
      inv-equiv (equiv-right-iterated-cauchy-product-species-subuniverse) ∘e
      equiv-left-iterated-cauchy-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-cauchy-product-species-subuniverse :
      cauchy-product-species-subuniverse P Q C1
        ( cauchy-product-species-subuniverse P Q C1 S T)
        ( U) ＝
      cauchy-product-species-subuniverse P Q C1
        ( S)
        ( cauchy-product-species-subuniverse P Q C1 T U)
    associative-cauchy-product-species-subuniverse =
      eq-equiv-fam-subuniverse
        ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5))
        ( cauchy-product-species-subuniverse P Q C1
          ( cauchy-product-species-subuniverse P Q C1 S T)
          ( U))
        ( cauchy-product-species-subuniverse P Q C1
          ( S)
          ( cauchy-product-species-subuniverse P Q C1 T U))
        ( equiv-associative-cauchy-product-species-subuniverse S T U)

Cauchy product is commutative

module _
  {l1 l2 l3 l4 : Level}
  (P : subuniverse l1 l2)
  (Q : global-subuniverse (λ l → l))
  (C1 : is-closed-under-cauchy-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-cauchy-product-species-subuniverse :
    (X : type-subuniverse P) →
    type-cauchy-product-species-subuniverse P Q S T X ≃
    type-cauchy-product-species-subuniverse P Q T S X
  equiv-commutative-cauchy-product-species-subuniverse X =
    equiv-Σ
      ( λ d →
        inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
          ( T (left-summand-binary-coproduct-Decomposition-subuniverse P X d)) ×
        inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
          ( S (right-summand-binary-coproduct-Decomposition-subuniverse P X d)))
      ( equiv-commutative-binary-coproduct-Decomposition-subuniverse P X)
      ( λ _ → commutative-product)

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

Unit laws of Cauchy product

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

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

  equiv-right-unit-law-cauchy-product-species-subuniverse :
    (X : type-subuniverse P) →
    type-cauchy-product-species-subuniverse P Q
      ( S)
      ( unit-cauchy-product-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q l1)
        ( C3))
      ( X) ≃
    inclusion-subuniverse (subuniverse-global-subuniverse Q l3) (S X)
  equiv-right-unit-law-cauchy-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-empty-right-summand-binary-coproduct-Decomposition-subuniverse
            P
            X
            C2)) ∘e
        ( ( inv-associative-Σ
            ( binary-coproduct-Decomposition-subuniverse P X)
            ( λ d →
              inclusion-subuniverse
                ( subuniverse-global-subuniverse Q l1)
                ( unit-cauchy-product-species-subuniverse
                  ( P)
                  ( subuniverse-global-subuniverse Q l1)
                  ( C3)
                  ( right-summand-binary-coproduct-Decomposition-subuniverse
                      P X d)))
            ( λ z →
              inclusion-subuniverse
                ( subuniverse-global-subuniverse Q l3)
                ( S
                  ( left-summand-binary-coproduct-Decomposition-subuniverse
                    P
                    X
                    (pr1 z))))) ∘e
          ( ( equiv-tot (λ _ → commutative-product))))))

  equiv-left-unit-law-cauchy-product-species-subuniverse :
    (X : type-subuniverse P) →
    type-cauchy-product-species-subuniverse P Q
      ( unit-cauchy-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-cauchy-product-species-subuniverse X =
    equiv-right-unit-law-cauchy-product-species-subuniverse X ∘e
    equiv-commutative-cauchy-product-species-subuniverse
      ( P)
      ( Q)
      ( C1)
      ( unit-cauchy-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-cauchy-product-species-subuniverse P Q)
  ( C2 : is-closed-under-coproducts-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))
        ( cauchy-product-species-subuniverse P Q C1 S T)
        ( X) ≃
      Σ ( binary-coproduct-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-coproduct-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))))
      ≃
      cauchy-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-cauchy-product-Σ-extension-species-subuniverse :
    Σ-extension-species-subuniverse
      ( P)
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
      ( cauchy-product-species-subuniverse P Q C1 S T)
      ( X) ≃
    cauchy-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-cauchy-product-Σ-extension-species-subuniverse =
    ( ( reassociate') ∘e
      ( ( equiv-tot
            ( λ d →
              equiv-Σ-equiv-base
                (λ p →
                    ( inclusion-subuniverse
                        ( subuniverse-global-subuniverse Q l3)
                        ( S
                          ( left-summand-binary-coproduct-Decomposition d ,
                            pr1 p))) ×
                    ( inclusion-subuniverse
                        ( subuniverse-global-subuniverse Q l4)
                        ( T
                          ( right-summand-binary-coproduct-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-coproduct-Decomposition
                              ( d))))
                        ( C2
                          ( pr1 p)
                          ( pr2 p))))))) ∘e
        ( reassociate)))

Recent changes