Coproducts of species of types

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

Created on 2023-03-21.
Last modified on 2024-02-06.

module species.coproducts-species-of-types where
Imports 
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.equivalences
open import foundation.functoriality-dependent-function-types
open import foundation.type-theoretic-principle-of-choice
open import foundation.universal-property-coproduct-types
open import foundation.universe-levels

open import species.morphisms-species-of-types
open import species.species-of-types

Idea

The coproduct of two species of types F and G is the pointwise coproduct.

Definition

Coproduct on objects

coproduct-species-types :
  {l1 l2 l3 : Level} (F : species-types l1 l2) (G : species-types l1 l3) →
  species-types l1 (l2 ⊔ l3)
coproduct-species-types F G X = F X + G X

Universal properties

Proof of (hom-species-types (species-types-coproduct F G) H) ≃ ((hom-species-types F H) × (hom-species-types G H)).

equiv-universal-property-coproduct-species-types :
  {l1 l2 l3 l4 : Level}
  (F : species-types l1 l2)
  (G : species-types l1 l3)
  (H : species-types l1 l4) →
  hom-species-types (coproduct-species-types F G) H ≃
  ((hom-species-types F H) × (hom-species-types G H))
equiv-universal-property-coproduct-species-types F G H =
  ( distributive-Π-Σ) ∘e
  ( equiv-Π-equiv-family (λ X → equiv-universal-property-coproduct (H X)))

Recent changes