Some constructions on polynomial endofunctors

src/foundation/type-arithmetic-dependent-pair-types.lagda.md

@@ -296,12 +296,25 @@ module _
       is-section-map-inv-interchange-Σ-Σ
       is-retraction-map-inv-interchange-Σ-Σ
 
+  is-equiv-map-inv-interchange-Σ-Σ : is-equiv map-inv-interchange-Σ-Σ
+  is-equiv-map-inv-interchange-Σ-Σ =
+    is-equiv-is-invertible
+      map-interchange-Σ-Σ
+      is-retraction-map-inv-interchange-Σ-Σ
+      is-section-map-inv-interchange-Σ-Σ
+
   interchange-Σ-Σ :
     Σ (Σ A B) (λ t → Σ (C (pr1 t)) (D (pr1 t) (pr2 t))) ≃
     Σ (Σ A C) (λ t → Σ (B (pr1 t)) (λ y → D (pr1 t) y (pr2 t)))
   pr1 interchange-Σ-Σ = map-interchange-Σ-Σ
   pr2 interchange-Σ-Σ = is-equiv-map-interchange-Σ-Σ
 
+  inv-interchange-Σ-Σ :
+    Σ (Σ A C) (λ t → Σ (B (pr1 t)) (λ y → D (pr1 t) y (pr2 t))) ≃
+    Σ (Σ A B) (λ t → Σ (C (pr1 t)) (D (pr1 t) (pr2 t)))
+  pr1 inv-interchange-Σ-Σ = map-inv-interchange-Σ-Σ
+  pr2 inv-interchange-Σ-Σ = is-equiv-map-inv-interchange-Σ-Σ
+
   interchange-Σ-Σ-Σ :
     Σ A (λ x → Σ (B x) (λ y → Σ (C x) (D x y))) ≃
     Σ A (λ x → Σ (C x) (λ z → Σ (B x) (λ y → D x y z)))
@@ -415,6 +428,18 @@ module _
 
   inv-right-distributive-product-Σ : Σ A (λ a → B a × C) ≃ (Σ A B) × C
   inv-right-distributive-product-Σ = inv-associative-Σ
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : UU l3} {D : C → UU l4}
+  where
+
+  distributive-product-Σ :
+    (Σ A B) × (Σ C D) ≃ Σ (A × C) (λ (a , c) → B a × D c)
+  distributive-product-Σ = interchange-Σ-Σ (λ _ _ → D)
+
+  inv-distributive-product-Σ :
+    Σ (A × C) (λ (a , c) → B a × D c) ≃ (Σ A B) × (Σ C D)
+  inv-distributive-product-Σ = inv-interchange-Σ-Σ (λ _ _ → D)
 ```
 
 ## See also

src/trees.lagda.md

@@ -16,11 +16,13 @@ open import trees.binary-w-types public
 open import trees.bounded-multisets public
 open import trees.cartesian-morphisms-polynomial-endofunctors public
 open import trees.cartesian-natural-transformations-polynomial-endofunctors public
+open import trees.cartesian-product-polynomial-endofunctors public
 open import trees.coalgebra-of-directed-trees public
 open import trees.coalgebra-of-enriched-directed-trees public
 open import trees.coalgebras-polynomial-endofunctors public
 open import trees.combinator-directed-trees public
 open import trees.combinator-enriched-directed-trees public
+open import trees.coproduct-polynomial-endofunctors public
 open import trees.directed-trees public
 open import trees.elementhood-relation-coalgebras-polynomial-endofunctors public
 open import trees.elementhood-relation-w-types public
@@ -32,6 +34,7 @@ open import trees.extensional-w-types public
 open import trees.fibers-directed-trees public
 open import trees.fibers-enriched-directed-trees public
 open import trees.full-binary-trees public
+open import trees.function-polynomial-endofunctors public
 open import trees.functoriality-combinator-directed-trees public
 open import trees.functoriality-fiber-directed-tree public
 open import trees.functoriality-w-types public

src/trees/cartesian-product-polynomial-endofunctors.lagda.md

@@ -0,0 +1,66 @@
+# Cartesian product polynomial endofunctors
+
+```agda
+module trees.cartesian-product-polynomial-endofunctors where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+For every pair of [polynomial endofunctors](trees.polynomial-endofunctors.md)
+`𝑃` and `𝑄` there is a
+{{#concept "cartesian product polynomial endofunctor" Disambiguation="on types" Agda=product-polynomial-endofunctor}}
+`𝑃 × 𝑄` given on shapes by `(𝑃 × 𝑄)₀ := 𝑃₀ × 𝑄₀` and on positions by
+`(𝑃 × 𝑄)₁(a , c) := 𝑃₁(a) + 𝑄₁(c)`. This polynomial endofunctor satisfies the
+[equivalence](foundation-core.equivalences.md)
+
+```text
+  (𝑃 × 𝑄)(X) ≃ 𝑃(X) × 𝑄(X).
+```
+
+## Definition
+
+```agda
+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))
+```

src/trees/coproduct-polynomial-endofunctors.lagda.md

@@ -0,0 +1,115 @@
+# Coproduct polynomial endofunctors
+
+```agda
+module trees.coproduct-polynomial-endofunctors where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.identity-types
+open import foundation.retractions
+open import foundation.sections
+open import foundation.universe-levels
+
+open import trees.polynomial-endofunctors
+```
+
+</details>
+
+## Idea
+
+For every pair of [polynomial endofunctors](trees.polynomial-endofunctors.md)
+`𝑃` and `𝑄` there is a
+{{#concept "coproduct polynomial endofunctor" Disambiguation="on types" Agda=coproduct-polynomial-endofunctor}}
+`𝑃 + 𝑄` given on shapes by `(𝑃 + 𝑄)₀ := 𝑃₀ + 𝑄₀` and on positions by
+`(𝑃 + 𝑄)₁(inl a) := 𝑃₁(a)` and `(𝑃 + 𝑄)₁(inr c) := 𝑄₁(c)`. This polynomial
+endofunctor satisfies the [equivalence](foundation-core.equivalences.md)
+
+```text
+  (𝑃 + 𝑄)(X) ≃ 𝑃(X) + 𝑄(X).
+```
+
+Note that for this definition to make sense, the positions of `𝑃` and `𝑄` have
+to live in the same universe.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (P@(A , B) : polynomial-endofunctor l1 l3)
+  (Q@(C , D) : polynomial-endofunctor l2 l3)
+  where
+
+  shape-coproduct-polynomial-endofunctor : UU (l1 ⊔ l2)
+  shape-coproduct-polynomial-endofunctor = A + C
+
+  position-coproduct-polynomial-endofunctor :
+    shape-coproduct-polynomial-endofunctor → UU l3
+  position-coproduct-polynomial-endofunctor (inl a) = B a
+  position-coproduct-polynomial-endofunctor (inr c) = D c
+
+  coproduct-polynomial-endofunctor : polynomial-endofunctor (l1 ⊔ l2) l3
+  coproduct-polynomial-endofunctor =
+    ( shape-coproduct-polynomial-endofunctor ,
+      position-coproduct-polynomial-endofunctor)
+
+  map-compute-type-coproduct-polynomial-endofunctor :
+    {l : Level} {X : UU l} →
+    type-polynomial-endofunctor coproduct-polynomial-endofunctor X →
+    type-polynomial-endofunctor P X + type-polynomial-endofunctor Q X
+  map-compute-type-coproduct-polynomial-endofunctor (inl a , b) = inl (a , b)
+  map-compute-type-coproduct-polynomial-endofunctor (inr c , d) = inr (c , d)
+
+  map-inv-compute-type-coproduct-polynomial-endofunctor :
+    {l : Level} {X : UU l} →
+    type-polynomial-endofunctor P X + type-polynomial-endofunctor Q X →
+    type-polynomial-endofunctor coproduct-polynomial-endofunctor X
+  map-inv-compute-type-coproduct-polynomial-endofunctor (inl (a , b)) =
+    (inl a , b)
+  map-inv-compute-type-coproduct-polynomial-endofunctor (inr (c , d)) =
+    (inr c , d)
+
+  is-section-map-inv-compute-type-coproduct-polynomial-endofunctor :
+    {l : Level} {X : UU l} →
+    is-section
+      ( map-compute-type-coproduct-polynomial-endofunctor {X = X})
+      ( map-inv-compute-type-coproduct-polynomial-endofunctor {X = X})
+  is-section-map-inv-compute-type-coproduct-polynomial-endofunctor (inl x) =
+    refl
+  is-section-map-inv-compute-type-coproduct-polynomial-endofunctor (inr y) =
+    refl
+
+  is-retraction-map-inv-compute-type-coproduct-polynomial-endofunctor :
+    {l : Level} {X : UU l} →
+    is-retraction
+      ( map-compute-type-coproduct-polynomial-endofunctor {X = X})
+      ( map-inv-compute-type-coproduct-polynomial-endofunctor {X = X})
+  is-retraction-map-inv-compute-type-coproduct-polynomial-endofunctor
+    ( inl x , _) =
+    refl
+  is-retraction-map-inv-compute-type-coproduct-polynomial-endofunctor
+    ( inr y , _) =
+    refl
+
+  is-equiv-map-compute-type-coproduct-polynomial-endofunctor :
+    {l : Level} {X : UU l} →
+    is-equiv (map-compute-type-coproduct-polynomial-endofunctor {X = X})
+  is-equiv-map-compute-type-coproduct-polynomial-endofunctor =
+    is-equiv-is-invertible
+      ( map-inv-compute-type-coproduct-polynomial-endofunctor)
+      ( is-section-map-inv-compute-type-coproduct-polynomial-endofunctor)
+      ( is-retraction-map-inv-compute-type-coproduct-polynomial-endofunctor)
+
+  compute-type-coproduct-polynomial-endofunctor :
+    {l : Level} {X : UU l} →
+    type-polynomial-endofunctor coproduct-polynomial-endofunctor X ≃
+    type-polynomial-endofunctor P X + type-polynomial-endofunctor Q X
+  compute-type-coproduct-polynomial-endofunctor =
+    ( map-compute-type-coproduct-polynomial-endofunctor ,
+      is-equiv-map-compute-type-coproduct-polynomial-endofunctor)
+```

src/trees/function-polynomial-endofunctors.lagda.md

@@ -0,0 +1,63 @@
+# Function polynomial endofunctors
+
+```agda
+module trees.function-polynomial-endofunctors where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.type-theoretic-principle-of-choice
+open import foundation.universal-property-dependent-pair-types
+open import foundation.universe-levels
+
+open import trees.polynomial-endofunctors
+```
+
+</details>
+
+## Idea
+
+Given a [polynomial endofunctor](trees.polynomial-endofunctors.md) `𝑃` and a
+type `I` then there is a
+{{#concept "function polynomial endofunctor" Disambiguation="on types" Agda=function-polynomial-endofunctor}}
+`𝑃ᴵ` given on shapes by `(𝑃ᴵ)₀ := I → 𝑃₀` and on positions by
+`(𝑃ᴵ)₁(f) := Σ (i : I), 𝑃₁(f(i))`. This polynomial endofunctor satisfies the
+[equivalence](foundation-core.equivalences.md)
+
+```text
+  𝑃ᴵ(X) ≃ (I → 𝑃(X)).
+```
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (I : UU l1)
+  (P@(A , B) : polynomial-endofunctor l2 l3)
+  where
+
+  shape-function-polynomial-endofunctor : UU (l1 ⊔ l2)
+  shape-function-polynomial-endofunctor = I → A
+
+  position-function-polynomial-endofunctor :
+    shape-function-polynomial-endofunctor → UU (l1 ⊔ l3)
+  position-function-polynomial-endofunctor f = Σ I (B ∘ f)
+
+  function-polynomial-endofunctor : polynomial-endofunctor (l1 ⊔ l2) (l1 ⊔ l3)
+  function-polynomial-endofunctor =
+    ( shape-function-polynomial-endofunctor ,
+      position-function-polynomial-endofunctor)
+
+  compute-type-function-polynomial-endofunctor :
+    {l : Level} {X : UU l} →
+    type-polynomial-endofunctor function-polynomial-endofunctor X ≃
+    (I → type-polynomial-endofunctor P X)
+  compute-type-function-polynomial-endofunctor =
+    inv-distributive-Π-Σ ∘e equiv-tot (λ f → equiv-ev-pair)
+```