Cartesian product polynomial endofunctors

Content created by Fredrik Bakke.

Created on 2026-02-05.
Last modified on 2026-02-05.

module trees.cartesian-product-polynomial-endofunctors where
Imports 
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.type-arithmetic-coproduct-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universal-property-coproduct-types
open import foundation.universe-levels

open import trees.polynomial-endofunctors

Idea

For every pair of polynomial endofunctors 𝑃 and 𝑄 there is a cartesian product polynomial endofunctor 𝑃 × 𝑄 given on shapes by (𝑃 × 𝑄)₀ := 𝑃₀ × 𝑄₀ and on positions by (𝑃 × 𝑄)₁(a , c) := 𝑃₁(a) + 𝑄₁(c). This polynomial endofunctor satisfies the equivalence

  (𝑃 × 𝑄)(X) ≃ 𝑃(X) × 𝑄(X).

Definition

module _
  {l1 l2 l3 l4 : Level}
  (P@(A , B) : polynomial-endofunctor l1 l2)
  (Q@(C , D) : polynomial-endofunctor l3 l4)
  where

  shape-product-polynomial-endofunctor : UU (l1 ⊔ l3)
  shape-product-polynomial-endofunctor = A × C

  position-product-polynomial-endofunctor :
    shape-product-polynomial-endofunctor → UU (l2 ⊔ l4)
  position-product-polynomial-endofunctor (a , c) = B a + D c

  product-polynomial-endofunctor : polynomial-endofunctor (l1 ⊔ l3) (l2 ⊔ l4)
  product-polynomial-endofunctor =
    ( shape-product-polynomial-endofunctor ,
      position-product-polynomial-endofunctor)

  compute-type-product-polynomial-endofunctor :
    {l : Level} {X : UU l} →
    type-polynomial-endofunctor product-polynomial-endofunctor X ≃
    type-polynomial-endofunctor P X × type-polynomial-endofunctor Q X
  compute-type-product-polynomial-endofunctor {X = X} =
    ( inv-distributive-product-Σ) ∘e
    ( equiv-tot (λ x → equiv-universal-property-coproduct X))

Recent changes