Dirichlet products of species of types

Content created by Egbert Rijke and Victor Blanchi.

Created on 2023-05-25.
Last modified on 2023-05-25.

module species.dirichlet-products-species-of-types where
Imports 
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.product-decompositions
open import foundation.universe-levels

open import species.species-of-types

Idea

The Dirichlet product of two species of types S and T on X is defined as

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

Definition

module _
  {l1 l2 l3 : Level}
  (S : species-types l1 l2)
  (T : species-types l1 l3)
  where

  dirichlet-product-species-types : species-types l1 (lsuc l1 ⊔ l2 ⊔ l3)
  dirichlet-product-species-types X =
    Σ ( binary-product-Decomposition l1 l1 X)
      ( λ d →
        S (left-summand-binary-product-Decomposition d) ×
        T (right-summand-binary-product-Decomposition d))

Recent changes