From 2fcd82c09173a90b5a48e24d0bfd300cbacacc2c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 16 Jun 2025 15:57:32 +0100
Subject: [PATCH 1/8] define multivariable polynomial functors

---
 src/trees.lagda.md                            |   1 +
 ...multivariable-polynomial-functors.lagda.md | 253 ++++++++++++++++++
 src/trees/polynomial-endofunctors.lagda.md    |  65 +++--
 3 files changed, 291 insertions(+), 28 deletions(-)
 create mode 100644 src/trees/multivariable-polynomial-functors.lagda.md

diff --git a/src/trees.lagda.md b/src/trees.lagda.md
index 4da5e8d445..ccadfa4206 100644
--- a/src/trees.lagda.md
+++ b/src/trees.lagda.md
@@ -44,6 +44,7 @@ open import trees.morphisms-directed-trees public
 open import trees.morphisms-enriched-directed-trees public
 open import trees.multiset-indexed-dependent-products-of-types public
 open import trees.multisets public
+open import trees.multivariable-polynomial-functors public
 open import trees.planar-binary-trees public
 open import trees.plane-trees public
 open import trees.polynomial-endofunctors public
diff --git a/src/trees/multivariable-polynomial-functors.lagda.md b/src/trees/multivariable-polynomial-functors.lagda.md
new file mode 100644
index 0000000000..94adcb781c
--- /dev/null
+++ b/src/trees/multivariable-polynomial-functors.lagda.md
@@ -0,0 +1,253 @@
+# Multivariable polynomial functors
+
+```agda
+module trees.multivariable-polynomial-functors where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-homotopies
+open import foundation.commuting-triangles-of-maps
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-function-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.structure-identity-principle
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import foundation-core.retractions
+open import foundation-core.torsorial-type-families
+```
+
+</details>
+
+## Idea
+
+{{#concept "Multivariable polynomial functors"}} are a generalization of the
+notion of [polynomial endofunctors](trees.polynomial-endofunctors.md) to the
+case where one has a family of types(variables) as opposed to a single type.
+
+Given a family of types `A : J → 𝒰` and a type family
+`B : I → {j : J} → A j → 𝒱` over `A`, we have a multivariable polynomial functor
+`P A B` with action on type families given by
+
+```text
+  X j ↦ Σ (a : A j), ((i : I) → B i a → X i)
+```
+
+## Definitions
+
+### The type of multivariable polynomial functors
+
+```agda
+polynomial-functor :
+  {l1 l2 : Level} (l3 l4 : Level) →
+  UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
+polynomial-functor l3 l4 I J =
+  Σ (J → UU l3) (λ A → (I → {j : J} → A j → UU l4))
+
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1} {J : UU l2}
+  (𝑃 : polynomial-functor l3 l4 I J)
+  where
+
+  shape-polynomial-functor : J → UU l3
+  shape-polynomial-functor = pr1 𝑃
+
+  position-polynomial-functor :
+    I → {j : J} → shape-polynomial-functor j → UU l4
+  position-polynomial-functor = pr2 𝑃
+```
+
+### The action on type families of a multivariable polynomial functor
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {I : UU l1} {J : UU l2}
+  where
+
+  type-polynomial-functor' :
+    (A : J → UU l3) (B : I → {j : J} → A j → UU l4) →
+    (I → UU l5) → (J → UU (l1 ⊔ l3 ⊔ l4 ⊔ l5))
+  type-polynomial-functor' A B X j =
+    Σ (A j) (λ a → (i : I) → B i a → X i)
+
+  type-polynomial-functor :
+    (𝑃 : polynomial-functor l3 l4 I J) →
+    (I → UU l5) → (J → UU (l1 ⊔ l3 ⊔ l4 ⊔ l5))
+  type-polynomial-functor (A , B) =
+    type-polynomial-functor' A B
+```
+
+### Characterizing equality in `type-polynomial-functor`
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {I : UU l1} {J : UU l2}
+  {𝑃@(A , B) : polynomial-functor l3 l4 I J}
+  {X : I → UU l5}
+  where
+
+  Eq-type-polynomial-functor :
+    (x y : (j : J) → type-polynomial-functor 𝑃 X j) →
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+  Eq-type-polynomial-functor x y =
+    (j : J) →
+    Σ ( pr1 (x j) ＝ pr1 (y j))
+      ( λ p →
+        (i : I) →
+        coherence-triangle-maps (pr2 (x j) i) (pr2 (y j) i) (tr (B i {j}) p))
+
+  refl-Eq-type-polynomial-functor :
+    (x : (j : J) → type-polynomial-functor 𝑃 X j) →
+    Eq-type-polynomial-functor x x
+  refl-Eq-type-polynomial-functor x j = (refl , λ i → refl-htpy)
+
+  Eq-eq-type-polynomial-functor :
+    (x y : (j : J) → type-polynomial-functor 𝑃 X j) →
+    x ＝ y → Eq-type-polynomial-functor x y
+  Eq-eq-type-polynomial-functor x .x refl =
+    refl-Eq-type-polynomial-functor x
+
+  is-torsorial-Eq-type-polynomial-functor :
+    (x : (j : J) → type-polynomial-functor 𝑃 X j) →
+    is-torsorial (Eq-type-polynomial-functor x)
+  is-torsorial-Eq-type-polynomial-functor x =
+    is-torsorial-Eq-Π
+      ( λ j →
+        is-torsorial-Eq-structure
+          { D =
+            λ a y p →
+            (i : I) →
+            coherence-triangle-maps (pr2 (x j) i) (y i) (tr (B i {j}) p)}
+          ( is-torsorial-Id (pr1 (x j)))
+          ( pr1 (x j) , refl)
+          (is-torsorial-binary-htpy (pr2 (x j))))
+
+  is-equiv-Eq-eq-type-polynomial-functor :
+    (x y : (j : J) → type-polynomial-functor 𝑃 X j) →
+    is-equiv (Eq-eq-type-polynomial-functor x y)
+  is-equiv-Eq-eq-type-polynomial-functor x =
+    fundamental-theorem-id
+      ( is-torsorial-Eq-type-polynomial-functor x)
+      ( Eq-eq-type-polynomial-functor x)
+
+  eq-Eq-type-polynomial-functor :
+    (x y : (j : J) → type-polynomial-functor 𝑃 X j) →
+    Eq-type-polynomial-functor x y → x ＝ y
+  eq-Eq-type-polynomial-functor x y =
+    map-inv-is-equiv (is-equiv-Eq-eq-type-polynomial-functor x y)
+
+  is-retraction-eq-Eq-type-polynomial-functor :
+    (x y : (j : J) → type-polynomial-functor 𝑃 X j) →
+    is-retraction
+      ( Eq-eq-type-polynomial-functor x y)
+      ( eq-Eq-type-polynomial-functor x y)
+  is-retraction-eq-Eq-type-polynomial-functor x y =
+    is-retraction-map-inv-is-equiv
+      ( is-equiv-Eq-eq-type-polynomial-functor x y)
+
+  coh-refl-eq-Eq-type-polynomial-functor :
+    (x : (j : J) → type-polynomial-functor 𝑃 X j) →
+    ( eq-Eq-type-polynomial-functor x x
+      ( refl-Eq-type-polynomial-functor x)) ＝ refl
+  coh-refl-eq-Eq-type-polynomial-functor x =
+    is-retraction-eq-Eq-type-polynomial-functor x x refl
+```
+
+### An action on dependent functions of multivariable polynomial functors
+
+The following construction is not quite right for "the" action on dependent
+functions, since given a type family `Y` over a type family `X`, the
+construction gives only a dependent function of approximately type
+
+```text
+  (x : 𝑃 X) → 𝑃 (Σ B Y x)
+```
+
+rather than
+
+```text
+  (x : 𝑃 X) → 𝑃 (Y x).
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {I : UU l1} {J : UU l2}
+  where
+
+  dmap-Σ-polynomial-functor' :
+    (A : J → UU l3) (B : I → {j : J} → A j → UU l4)
+    {X : I → UU l5} {Y : (i : I) → X i → UU l6}
+    (f : (i : I) (x : X i) → Y i x) →
+    (x : (j : J) → type-polynomial-functor' A B X j) →
+    (j : J) →
+    type-polynomial-functor' A B
+      ( λ i → Σ (B i (pr1 (x j))) (Y i ∘ pr2 (x j) i))
+      ( j)
+  dmap-Σ-polynomial-functor' A B f x j =
+    ( pr1 (x j) , (λ i b → (b , f i (pr2 (x j) i b))))
+```
+
+### The action on functions of multivariable polynomial functors
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {I : UU l1} {J : UU l2}
+  where
+
+  map-polynomial-functor' :
+    (A : J → UU l3) (B : I → {j : J} → A j → UU l4)
+    {X : I → UU l5} {Y : I → UU l6}
+    (f : (i : I) → X i → Y i) →
+    ((j : J) → type-polynomial-functor' A B X j) →
+    ((j : J) → type-polynomial-functor' A B Y j)
+  map-polynomial-functor' A B f x j =
+    ( pr1 (x j) , (λ i b → f i (pr2 (x j) i b)))
+
+  map-polynomial-functor :
+    (𝑃 : polynomial-functor l3 l4 I J)
+    {X : I → UU l5} {Y : I → UU l6}
+    (f : (i : I) → X i → Y i) →
+    ((j : J) → type-polynomial-functor 𝑃 X j) →
+    ((j : J) → type-polynomial-functor 𝑃 Y j)
+  map-polynomial-functor (A , B) = map-polynomial-functor' A B
+```
+
+### The action on homotopies of multivariable polynomial functors
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} {I : UU l1} {J : UU l2}
+  where
+
+  binary-htpy-polynomial-functor' :
+    (A : J → UU l3) (B : I → {j : J} → A j → UU l4)
+    {X : I → UU l5} {Y : I → UU l6} {f g : (i : I) → X i → Y i} →
+    binary-htpy f g →
+    binary-htpy (map-polynomial-functor' A B f) (map-polynomial-functor' A B g)
+  binary-htpy-polynomial-functor' A B {f = f} {g} H x j =
+    eq-pair-eq-fiber
+      ( eq-binary-htpy
+        ( pr2 (map-polynomial-functor' A B f x j))
+        ( pr2 (map-polynomial-functor' A B g x j))
+        ( λ i → H i ∘ pr2 (x j) i))
+
+  binary-htpy-polynomial-functor :
+    (𝑃 : polynomial-functor l3 l4 I J)
+    {X : I → UU l5} {Y : I → UU l6} {f g : (i : I) → X i → Y i} →
+    binary-htpy f g →
+    binary-htpy (map-polynomial-functor 𝑃 f) (map-polynomial-functor 𝑃 g)
+  binary-htpy-polynomial-functor (A , B) = binary-htpy-polynomial-functor' A B
+```
diff --git a/src/trees/polynomial-endofunctors.lagda.md b/src/trees/polynomial-endofunctors.lagda.md
index 793fbf9b59..6434bacb73 100644
--- a/src/trees/polynomial-endofunctors.lagda.md
+++ b/src/trees/polynomial-endofunctors.lagda.md
@@ -21,6 +21,8 @@ open import foundation.transport-along-identifications
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
+open import foundation-core.commuting-triangles-of-maps
+open import foundation-core.retractions
 open import foundation-core.torsorial-type-families
 ```
 
@@ -28,15 +30,16 @@ open import foundation-core.torsorial-type-families
 
 ## Idea
 
-Given a type `A` equipped with a type family `B` over `A`, the **polynomial
-endofunctor** `P A B` is defined by
+Given a type `A` equipped with a type family `B` over `A`, the
+{{#concept "polynomial endofunctor"}} `𝑃 A B` is defined by
 
 ```text
   X ↦ Σ (x : A), (B x → X)
 ```
 
-Polynomial endofunctors are important in the study of W-types, and also in the
-study of combinatorial species.
+Polynomial endofunctors are important in the study of
+[W-types](trees.w-types.md), and also in the study of
+[combinatorial species](species.md).
 
 ## Definitions
 
@@ -59,49 +62,50 @@ module _
   Eq-type-polynomial-endofunctor :
     (x y : type-polynomial-endofunctor A B X) → UU (l1 ⊔ l2 ⊔ l3)
   Eq-type-polynomial-endofunctor x y =
-    Σ (pr1 x ＝ pr1 y) (λ p → (pr2 x) ~ ((pr2 y) ∘ (tr B p)))
+    Σ (pr1 x ＝ pr1 y) (λ p → coherence-triangle-maps (pr2 x) (pr2 y) (tr B p))
 
   refl-Eq-type-polynomial-endofunctor :
     (x : type-polynomial-endofunctor A B X) →
     Eq-type-polynomial-endofunctor x x
-  refl-Eq-type-polynomial-endofunctor (pair x α) = pair refl refl-htpy
+  refl-Eq-type-polynomial-endofunctor (x , α) = (refl , refl-htpy)
+
+  Eq-eq-type-polynomial-endofunctor :
+    (x y : type-polynomial-endofunctor A B X) →
+    x ＝ y → Eq-type-polynomial-endofunctor x y
+  Eq-eq-type-polynomial-endofunctor x .x refl =
+    refl-Eq-type-polynomial-endofunctor x
 
   is-torsorial-Eq-type-polynomial-endofunctor :
     (x : type-polynomial-endofunctor A B X) →
     is-torsorial (Eq-type-polynomial-endofunctor x)
-  is-torsorial-Eq-type-polynomial-endofunctor (pair x α) =
+  is-torsorial-Eq-type-polynomial-endofunctor (x , α) =
     is-torsorial-Eq-structure
       ( is-torsorial-Id x)
-      ( pair x refl)
+      ( x , refl)
       ( is-torsorial-htpy α)
 
-  Eq-type-polynomial-endofunctor-eq :
-    (x y : type-polynomial-endofunctor A B X) →
-    x ＝ y → Eq-type-polynomial-endofunctor x y
-  Eq-type-polynomial-endofunctor-eq x .x refl =
-    refl-Eq-type-polynomial-endofunctor x
-
-  is-equiv-Eq-type-polynomial-endofunctor-eq :
+  is-equiv-Eq-eq-type-polynomial-endofunctor :
     (x y : type-polynomial-endofunctor A B X) →
-    is-equiv (Eq-type-polynomial-endofunctor-eq x y)
-  is-equiv-Eq-type-polynomial-endofunctor-eq x =
+    is-equiv (Eq-eq-type-polynomial-endofunctor x y)
+  is-equiv-Eq-eq-type-polynomial-endofunctor x =
     fundamental-theorem-id
       ( is-torsorial-Eq-type-polynomial-endofunctor x)
-      ( Eq-type-polynomial-endofunctor-eq x)
+      ( Eq-eq-type-polynomial-endofunctor x)
 
   eq-Eq-type-polynomial-endofunctor :
     (x y : type-polynomial-endofunctor A B X) →
     Eq-type-polynomial-endofunctor x y → x ＝ y
   eq-Eq-type-polynomial-endofunctor x y =
-    map-inv-is-equiv (is-equiv-Eq-type-polynomial-endofunctor-eq x y)
+    map-inv-is-equiv (is-equiv-Eq-eq-type-polynomial-endofunctor x y)
 
   is-retraction-eq-Eq-type-polynomial-endofunctor :
     (x y : type-polynomial-endofunctor A B X) →
-    ( ( eq-Eq-type-polynomial-endofunctor x y) ∘
-      ( Eq-type-polynomial-endofunctor-eq x y)) ~ id
+    is-retraction
+      ( Eq-eq-type-polynomial-endofunctor x y)
+      ( eq-Eq-type-polynomial-endofunctor x y)
   is-retraction-eq-Eq-type-polynomial-endofunctor x y =
     is-retraction-map-inv-is-equiv
-      ( is-equiv-Eq-type-polynomial-endofunctor-eq x y)
+      ( is-equiv-Eq-eq-type-polynomial-endofunctor x y)
 
   coh-refl-eq-Eq-type-polynomial-endofunctor :
     (x : type-polynomial-endofunctor A B X) →
@@ -128,17 +132,22 @@ htpy-polynomial-endofunctor :
   {l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2) {X : UU l3} {Y : UU l4}
   {f g : X → Y} →
   f ~ g → map-polynomial-endofunctor A B f ~ map-polynomial-endofunctor A B g
-htpy-polynomial-endofunctor A B {X = X} {Y} {f} {g} H (pair x α) =
+htpy-polynomial-endofunctor A B {f = f} {g} H (x , α) =
   eq-Eq-type-polynomial-endofunctor
-    ( map-polynomial-endofunctor A B f (pair x α))
-    ( map-polynomial-endofunctor A B g (pair x α))
-    ( pair refl (H ·r α))
+    ( map-polynomial-endofunctor A B f (x , α))
+    ( map-polynomial-endofunctor A B g (x , α))
+    ( refl , H ·r α)
 
 coh-refl-htpy-polynomial-endofunctor :
   {l1 l2 l3 l4 : Level} (A : UU l1) (B : A → UU l2) {X : UU l3} {Y : UU l4}
   (f : X → Y) →
   htpy-polynomial-endofunctor A B (refl-htpy {f = f}) ~ refl-htpy
-coh-refl-htpy-polynomial-endofunctor A B {X = X} {Y} f (pair x α) =
+coh-refl-htpy-polynomial-endofunctor A B f (x , α) =
   coh-refl-eq-Eq-type-polynomial-endofunctor
-    ( map-polynomial-endofunctor A B f (pair x α))
+    ( map-polynomial-endofunctor A B f (x , α))
 ```
+
+## See also
+
+- [Multivariable polynomial functors](trees.multivariable-polynomial-functors.md)
+  for the generalization of polynomial endofunctors to type families.

From 151a7e3cd401cfdc4d590171ae99059c74b76d99 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 16 Jun 2025 16:54:46 +0100
Subject: [PATCH 2/8] The identity multivariable polynomial functor

---
 ...universal-property-identity-types.lagda.md | 85 ++++++++++---------
 ...multivariable-polynomial-functors.lagda.md | 42 ++++++++-
 2 files changed, 85 insertions(+), 42 deletions(-)

diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md
index a231b5f29e..c0be19e51b 100644
--- a/src/foundation/universal-property-identity-types.lagda.md
+++ b/src/foundation/universal-property-identity-types.lagda.md
@@ -19,6 +19,8 @@ open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.preunivalence
+open import foundation-core.sections
+open import foundation-core.retractions
 open import foundation.univalence
 open import foundation.universe-levels
 
@@ -46,47 +48,48 @@ also known as the **type theoretic Yoneda lemma**.
 ## Theorem
 
 ```agda
-ev-refl :
-  {l1 l2 : Level} {A : UU l1} (a : A) {B : (x : A) → a ＝ x → UU l2} →
-  ((x : A) (p : a ＝ x) → B x p) → B a refl
-ev-refl a f = f a refl
-
-ev-refl' :
-  {l1 l2 : Level} {A : UU l1} (a : A) {B : (x : A) → x ＝ a → UU l2} →
-  ((x : A) (p : x ＝ a) → B x p) → B a refl
-ev-refl' a f = f a refl
-
-abstract
-  is-equiv-ev-refl :
-    {l1 l2 : Level} {A : UU l1} (a : A)
-    {B : (x : A) → a ＝ x → UU l2} → is-equiv (ev-refl a {B})
-  is-equiv-ev-refl a =
-    is-equiv-is-invertible
-      ( ind-Id a _)
-      ( λ b → refl)
-      ( λ f → eq-htpy
-        ( λ x → eq-htpy
-          ( ind-Id a
-            ( λ x' p' → ind-Id a _ (f a refl) x' p' ＝ f x' p')
-            ( refl) x)))
-
-equiv-ev-refl :
-  {l1 l2 : Level} {A : UU l1} (a : A) {B : (x : A) → a ＝ x → UU l2} →
-  ((x : A) (p : a ＝ x) → B x p) ≃ (B a refl)
-pr1 (equiv-ev-refl a) = ev-refl a
-pr2 (equiv-ev-refl a) = is-equiv-ev-refl a
-
-equiv-ev-refl' :
-  {l1 l2 : Level} {A : UU l1} (a : A) {B : (x : A) → x ＝ a → UU l2} →
-  ((x : A) (p : x ＝ a) → B x p) ≃ B a refl
-equiv-ev-refl' a {B} =
-  ( equiv-ev-refl a) ∘e
-  ( equiv-Π-equiv-family (λ x → equiv-precomp-Π (equiv-inv a x) (B x)))
-
-is-equiv-ev-refl' :
-  {l1 l2 : Level} {A : UU l1} (a : A)
-  {B : (x : A) → x ＝ a → UU l2} → is-equiv (ev-refl' a {B})
-is-equiv-ev-refl' a = is-equiv-map-equiv (equiv-ev-refl' a)
+module _
+  {l1 l2 : Level} {A : UU l1} (a : A) {B : (x : A) → a ＝ x → UU l2}
+  where
+
+  ev-refl : ((x : A) (p : a ＝ x) → B x p) → B a refl
+  ev-refl f = f a refl
+
+  is-retraction-ev-refl : is-retraction (ind-Id a B) ev-refl
+  is-retraction-ev-refl = refl-htpy
+
+  abstract
+    is-section-ev-refl : is-section (ind-Id a B) ev-refl
+    is-section-ev-refl f =
+      eq-htpy
+        ( λ x →
+          eq-htpy
+            ( ind-Id a
+              ( λ x' p' → ind-Id a _ (f a refl) x' p' ＝ f x' p')
+              ( refl)
+              ( x)))
+
+  is-equiv-ev-refl : is-equiv ev-refl
+  is-equiv-ev-refl =
+    is-equiv-is-invertible (ind-Id a B) is-retraction-ev-refl is-section-ev-refl
+
+  equiv-ev-refl : ((x : A) (p : a ＝ x) → B x p) ≃ B a refl
+  equiv-ev-refl = (ev-refl , is-equiv-ev-refl)
+
+module _
+  {l1 l2 : Level} {A : UU l1} (a : A) {B : (x : A) → x ＝ a → UU l2}
+  where
+
+  ev-refl' : ((x : A) (p : x ＝ a) → B x p) → B a refl
+  ev-refl' f = f a refl
+
+  equiv-ev-refl' : ((x : A) (p : x ＝ a) → B x p) ≃ B a refl
+  equiv-ev-refl' =
+    ( equiv-ev-refl a) ∘e
+    ( equiv-Π-equiv-family (λ x → equiv-precomp-Π (equiv-inv a x) (B x)))
+
+  is-equiv-ev-refl' : is-equiv ev-refl'
+  is-equiv-ev-refl' = is-equiv-map-equiv equiv-ev-refl'
 ```
 
 ### The type of fiberwise maps from `Id a` to a torsorial type family `B` is equivalent to the type of fiberwise equivalences
diff --git a/src/trees/multivariable-polynomial-functors.lagda.md b/src/trees/multivariable-polynomial-functors.lagda.md
index 94adcb781c..6d3f6a3bdd 100644
--- a/src/trees/multivariable-polynomial-functors.lagda.md
+++ b/src/trees/multivariable-polynomial-functors.lagda.md
@@ -8,7 +8,8 @@ module trees.multivariable-polynomial-functors where
 
 ```agda
 open import foundation.binary-homotopies
-open import foundation.commuting-triangles-of-maps
+open import foundation-core.commuting-triangles-of-maps
+open import foundation-core.commuting-squares-of-maps
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-function-types
@@ -22,6 +23,9 @@ open import foundation.homotopy-induction
 open import foundation.identity-types
 open import foundation.structure-identity-principle
 open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-unit-type
+open import foundation.unit-type
+open import foundation.universal-property-identity-types
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
@@ -251,3 +255,39 @@ module _
     binary-htpy (map-polynomial-functor 𝑃 f) (map-polynomial-functor 𝑃 g)
   binary-htpy-polynomial-functor (A , B) = binary-htpy-polynomial-functor' A B
 ```
+
+### The identity multivariable polynomial functor
+
+```agda
+module _
+  {l1 : Level} {I : UU l1}
+  where
+
+  id-polynomial-functor : polynomial-functor lzero l1 I I
+  id-polynomial-functor = (λ i' → unit) , (λ i {i'} * → (i' ＝ i))
+
+  compute-type-id-polynomial-functor :
+    {l2 : Level} (X : I → UU l2) (i : I) →
+    type-polynomial-functor id-polynomial-functor X i ≃ X i
+  compute-type-id-polynomial-functor X i =
+    equivalence-reasoning
+      Σ unit (λ * → (i' : I) → i ＝ i' → X i')
+      ≃ ((i' : I) → i ＝ i' → X i')
+        by left-unit-law-Σ (λ * → (i' : I) → i ＝ i' → X i')
+      ≃ X i
+        by equiv-ev-refl i
+
+  map-compute-type-id-polynomial-functor :
+    {l2 : Level} (X : I → UU l2) (i : I) →
+    type-polynomial-functor id-polynomial-functor X i → X i
+  map-compute-type-id-polynomial-functor X i x = pr2 x i refl
+
+  compute-map-id-polynomial-functor :
+    {l2 l3 : Level} {X : I → UU l2} {Y : I → UU l3} (f : (i : I) → X i → Y i)
+    (x : (i : I) → type-polynomial-functor id-polynomial-functor X i) →
+    (i : I) →
+    map-compute-type-id-polynomial-functor Y i
+      ( map-polynomial-functor id-polynomial-functor f x i) ＝
+    f i (map-compute-type-id-polynomial-functor X i (x i))
+  compute-map-id-polynomial-functor f i = refl-htpy
+```

From 13bbafde9267480a7170ab6e4e50b2a75e85485f Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 16 Jun 2025 17:52:35 +0100
Subject: [PATCH 3/8] composition of polynomials

---
 ...multivariable-polynomial-functors.lagda.md | 100 +++++++++++++++---
 1 file changed, 84 insertions(+), 16 deletions(-)

diff --git a/src/trees/multivariable-polynomial-functors.lagda.md b/src/trees/multivariable-polynomial-functors.lagda.md
index 6d3f6a3bdd..0db39e5e15 100644
--- a/src/trees/multivariable-polynomial-functors.lagda.md
+++ b/src/trees/multivariable-polynomial-functors.lagda.md
@@ -19,6 +19,7 @@ open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopies
+open import foundation.cartesian-product-types
 open import foundation.homotopy-induction
 open import foundation.identity-types
 open import foundation.structure-identity-principle
@@ -215,17 +216,15 @@ module _
     (A : J → UU l3) (B : I → {j : J} → A j → UU l4)
     {X : I → UU l5} {Y : I → UU l6}
     (f : (i : I) → X i → Y i) →
-    ((j : J) → type-polynomial-functor' A B X j) →
-    ((j : J) → type-polynomial-functor' A B Y j)
-  map-polynomial-functor' A B f x j =
-    ( pr1 (x j) , (λ i b → f i (pr2 (x j) i b)))
+    (j : J) →
+    type-polynomial-functor' A B X j → type-polynomial-functor' A B Y j
+  map-polynomial-functor' A B f j (a , x) = (a , (λ i b → f i (x i b)))
 
   map-polynomial-functor :
     (𝑃 : polynomial-functor l3 l4 I J)
     {X : I → UU l5} {Y : I → UU l6}
     (f : (i : I) → X i → Y i) →
-    ((j : J) → type-polynomial-functor 𝑃 X j) →
-    ((j : J) → type-polynomial-functor 𝑃 Y j)
+    (j : J) → type-polynomial-functor 𝑃 X j → type-polynomial-functor 𝑃 Y j
   map-polynomial-functor (A , B) = map-polynomial-functor' A B
 ```
 
@@ -241,12 +240,8 @@ module _
     {X : I → UU l5} {Y : I → UU l6} {f g : (i : I) → X i → Y i} →
     binary-htpy f g →
     binary-htpy (map-polynomial-functor' A B f) (map-polynomial-functor' A B g)
-  binary-htpy-polynomial-functor' A B {f = f} {g} H x j =
-    eq-pair-eq-fiber
-      ( eq-binary-htpy
-        ( pr2 (map-polynomial-functor' A B f x j))
-        ( pr2 (map-polynomial-functor' A B g x j))
-        ( λ i → H i ∘ pr2 (x j) i))
+  binary-htpy-polynomial-functor' A B {f = f} {g} H j x =
+    eq-pair-eq-fiber (eq-binary-htpy _ _ (λ i → H i ∘ pr2 x i))
 
   binary-htpy-polynomial-functor :
     (𝑃 : polynomial-functor l3 l4 I J)
@@ -280,14 +275,87 @@ module _
   map-compute-type-id-polynomial-functor :
     {l2 : Level} (X : I → UU l2) (i : I) →
     type-polynomial-functor id-polynomial-functor X i → X i
-  map-compute-type-id-polynomial-functor X i x = pr2 x i refl
+  map-compute-type-id-polynomial-functor X i =
+    map-equiv (compute-type-id-polynomial-functor X i)
 
   compute-map-id-polynomial-functor :
     {l2 l3 : Level} {X : I → UU l2} {Y : I → UU l3} (f : (i : I) → X i → Y i)
     (x : (i : I) → type-polynomial-functor id-polynomial-functor X i) →
     (i : I) →
-    map-compute-type-id-polynomial-functor Y i
-      ( map-polynomial-functor id-polynomial-functor f x i) ＝
-    f i (map-compute-type-id-polynomial-functor X i (x i))
+    ( map-compute-type-id-polynomial-functor Y i
+      ( map-polynomial-functor id-polynomial-functor f i (x i))) ＝
+    ( f i (map-compute-type-id-polynomial-functor X i (x i)))
   compute-map-id-polynomial-functor f i = refl-htpy
 ```
+
+### Composition of multivariable polynomial functors
+
+Given two multivariable polynomial functors `𝑃 A B : (I → Type) → (J → Type)`
+and `𝑃 C D : (J → Type) → (K → Type)`, then the composite functor
+`𝑃 C D ∘ 𝑃 A B` is again a polynomial functor. The resulting composite shapes
+and positions are computed via convolution.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 l7 : Level}
+  {I : UU l1} {J : UU l2} {K : UU l3}
+  (𝑃@(A , B) : polynomial-functor l4 l5 I J)
+  (𝑄@(C , D) : polynomial-functor l6 l7 J K)
+  where
+
+  shape-comp-polynomial-functor : K → UU (l2 ⊔ l4 ⊔ l6 ⊔ l7)
+  shape-comp-polynomial-functor k = Σ (C k) (λ c → (j : J) → D j c → A j)
+
+  position-comp-polynomial-functor :
+    I → {k : K} → shape-comp-polynomial-functor k → UU (l2 ⊔ l5 ⊔ l7)
+  position-comp-polynomial-functor i {k} (c , a) =
+    Σ J (λ j → Σ (D j c) (λ d → B i (a j d)))
+
+  comp-polynomial-functor :
+    polynomial-functor (l2 ⊔ l4 ⊔ l6 ⊔ l7) (l2 ⊔ l5 ⊔ l7) I K
+  comp-polynomial-functor =
+    ( shape-comp-polynomial-functor , position-comp-polynomial-functor)
+
+  map-compute-type-comp-polynomial-functor :
+    {l8 : Level} (X : I → UU l8) (k : K) →
+    type-polynomial-functor comp-polynomial-functor X k →
+    type-polynomial-functor 𝑄 (type-polynomial-functor 𝑃 X) k
+  map-compute-type-comp-polynomial-functor X k ((c , a) , x) =
+    (c , (λ j d → (a j d , (λ i b → x i (j , d , b)))))
+
+  map-inv-compute-type-comp-polynomial-functor :
+    {l8 : Level} (X : I → UU l8) (k : K) →
+    type-polynomial-functor 𝑄 (type-polynomial-functor 𝑃 X) k →
+    type-polynomial-functor comp-polynomial-functor X k
+  map-inv-compute-type-comp-polynomial-functor X k (c , q) =
+    ((c , (λ j d → pr1 (q j d))) , (λ i (j , d , b) → pr2 (q j d) i b))
+
+  is-equiv-map-compute-type-comp-polynomial-functor :
+    {l8 : Level} (X : I → UU l8) (k : K) →
+    is-equiv (map-compute-type-comp-polynomial-functor X k)
+  is-equiv-map-compute-type-comp-polynomial-functor X k =
+    is-equiv-is-invertible
+      ( map-inv-compute-type-comp-polynomial-functor X k)
+      ( refl-htpy)
+      ( refl-htpy)
+
+  compute-type-comp-polynomial-functor :
+    {l8 : Level} (X : I → UU l8) (k : K) →
+    type-polynomial-functor comp-polynomial-functor X k ≃
+    type-polynomial-functor 𝑄 (type-polynomial-functor 𝑃 X) k
+  compute-type-comp-polynomial-functor X k =
+    ( map-compute-type-comp-polynomial-functor X k ,
+      is-equiv-map-compute-type-comp-polynomial-functor X k)
+
+  compute-map-comp-polynomial-functor :
+    {l8 l9 : Level} {X : I → UU l8} {Y : I → UU l9} (f : (i : I) → X i → Y i)
+    (x : (k : K) → type-polynomial-functor comp-polynomial-functor X k) →
+    (k : K) →
+    map-compute-type-comp-polynomial-functor Y k
+      ( map-polynomial-functor comp-polynomial-functor f k (x k)) ＝
+    map-polynomial-functor 𝑄
+      ( map-polynomial-functor 𝑃 f)
+      ( k)
+      ( map-compute-type-comp-polynomial-functor X k (x k))
+  compute-map-comp-polynomial-functor f x k = refl
+```

From 53cdfeb5a6568ff3a41d68beb0f6cd96d986b3d2 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 16 Jun 2025 17:54:21 +0100
Subject: [PATCH 4/8] remove unused imports

---
 src/trees/multivariable-polynomial-functors.lagda.md | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/src/trees/multivariable-polynomial-functors.lagda.md b/src/trees/multivariable-polynomial-functors.lagda.md
index 0db39e5e15..bf859d2308 100644
--- a/src/trees/multivariable-polynomial-functors.lagda.md
+++ b/src/trees/multivariable-polynomial-functors.lagda.md
@@ -8,19 +8,13 @@ module trees.multivariable-polynomial-functors where
 
 ```agda
 open import foundation.binary-homotopies
-open import foundation-core.commuting-triangles-of-maps
-open import foundation-core.commuting-squares-of-maps
-open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-function-types
 open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
 open import foundation.function-types
-open import foundation.functoriality-dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopies
-open import foundation.cartesian-product-types
-open import foundation.homotopy-induction
 open import foundation.identity-types
 open import foundation.structure-identity-principle
 open import foundation.transport-along-identifications
@@ -28,8 +22,8 @@ open import foundation.type-arithmetic-unit-type
 open import foundation.unit-type
 open import foundation.universal-property-identity-types
 open import foundation.universe-levels
-open import foundation.whiskering-homotopies-composition
 
+open import foundation-core.commuting-triangles-of-maps
 open import foundation-core.retractions
 open import foundation-core.torsorial-type-families
 ```

From a7fc45996d2ea6333505c4b98ea9466ec6612048 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 16 Jun 2025 17:54:34 +0100
Subject: [PATCH 5/8] pre-commit

---
 src/foundation/universal-property-identity-types.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md
index c0be19e51b..4904b22306 100644
--- a/src/foundation/universal-property-identity-types.lagda.md
+++ b/src/foundation/universal-property-identity-types.lagda.md
@@ -19,8 +19,6 @@ open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.preunivalence
-open import foundation-core.sections
-open import foundation-core.retractions
 open import foundation.univalence
 open import foundation.universe-levels
 
@@ -33,6 +31,8 @@ open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.propositional-maps
 open import foundation-core.propositions
+open import foundation-core.retractions
+open import foundation-core.sections
 open import foundation-core.torsorial-type-families
 ```
 

From 2aaa9fc1e2ef32997db03703468fc286c3a0341c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 16 Jun 2025 18:25:52 +0100
Subject: [PATCH 6/8] edits

---
 ...multivariable-polynomial-functors.lagda.md | 40 +++++++++----------
 1 file changed, 20 insertions(+), 20 deletions(-)

diff --git a/src/trees/multivariable-polynomial-functors.lagda.md b/src/trees/multivariable-polynomial-functors.lagda.md
index bf859d2308..dd021950e7 100644
--- a/src/trees/multivariable-polynomial-functors.lagda.md
+++ b/src/trees/multivariable-polynomial-functors.lagda.md
@@ -23,6 +23,7 @@ open import foundation.unit-type
 open import foundation.universal-property-identity-types
 open import foundation.universe-levels
 
+open import foundation-core.commuting-squares-of-maps
 open import foundation-core.commuting-triangles-of-maps
 open import foundation-core.retractions
 open import foundation-core.torsorial-type-families
@@ -111,7 +112,7 @@ module _
   refl-Eq-type-polynomial-functor :
     (x : (j : J) → type-polynomial-functor 𝑃 X j) →
     Eq-type-polynomial-functor x x
-  refl-Eq-type-polynomial-functor x j = (refl , λ i → refl-htpy)
+  refl-Eq-type-polynomial-functor x j = (refl , (λ i → refl-htpy))
 
   Eq-eq-type-polynomial-functor :
     (x y : (j : J) → type-polynomial-functor 𝑃 X j) →
@@ -234,7 +235,7 @@ module _
     {X : I → UU l5} {Y : I → UU l6} {f g : (i : I) → X i → Y i} →
     binary-htpy f g →
     binary-htpy (map-polynomial-functor' A B f) (map-polynomial-functor' A B g)
-  binary-htpy-polynomial-functor' A B {f = f} {g} H j x =
+  binary-htpy-polynomial-functor' A B H j x =
     eq-pair-eq-fiber (eq-binary-htpy _ _ (λ i → H i ∘ pr2 x i))
 
   binary-htpy-polynomial-functor :
@@ -274,11 +275,12 @@ module _
 
   compute-map-id-polynomial-functor :
     {l2 l3 : Level} {X : I → UU l2} {Y : I → UU l3} (f : (i : I) → X i → Y i)
-    (x : (i : I) → type-polynomial-functor id-polynomial-functor X i) →
     (i : I) →
-    ( map-compute-type-id-polynomial-functor Y i
-      ( map-polynomial-functor id-polynomial-functor f i (x i))) ＝
-    ( f i (map-compute-type-id-polynomial-functor X i (x i)))
+    coherence-square-maps
+      ( map-compute-type-id-polynomial-functor X i)
+      ( map-polynomial-functor id-polynomial-functor f i)
+      ( f i)
+      ( map-compute-type-id-polynomial-functor Y i)
   compute-map-id-polynomial-functor f i = refl-htpy
 ```
 
@@ -286,8 +288,7 @@ module _
 
 Given two multivariable polynomial functors `𝑃 A B : (I → Type) → (J → Type)`
 and `𝑃 C D : (J → Type) → (K → Type)`, then the composite functor
-`𝑃 C D ∘ 𝑃 A B` is again a polynomial functor. The resulting composite shapes
-and positions are computed via convolution.
+`𝑃 C D ∘ 𝑃 A B` is again a polynomial functor.
 
 ```agda
 module _
@@ -298,12 +299,13 @@ module _
   where
 
   shape-comp-polynomial-functor : K → UU (l2 ⊔ l4 ⊔ l6 ⊔ l7)
-  shape-comp-polynomial-functor k = Σ (C k) (λ c → (j : J) → D j c → A j)
+  shape-comp-polynomial-functor k =
+    Σ (C k) (λ c → (j : J) → D j {k} c → A j)
 
   position-comp-polynomial-functor :
     I → {k : K} → shape-comp-polynomial-functor k → UU (l2 ⊔ l5 ⊔ l7)
   position-comp-polynomial-functor i {k} (c , a) =
-    Σ J (λ j → Σ (D j c) (λ d → B i (a j d)))
+    Σ J (λ j → Σ (D j {k} c) (λ d → B i {j} (a j d)))
 
   comp-polynomial-functor :
     polynomial-functor (l2 ⊔ l4 ⊔ l6 ⊔ l7) (l2 ⊔ l5 ⊔ l7) I K
@@ -342,14 +344,12 @@ module _
       is-equiv-map-compute-type-comp-polynomial-functor X k)
 
   compute-map-comp-polynomial-functor :
-    {l8 l9 : Level} {X : I → UU l8} {Y : I → UU l9} (f : (i : I) → X i → Y i)
-    (x : (k : K) → type-polynomial-functor comp-polynomial-functor X k) →
-    (k : K) →
-    map-compute-type-comp-polynomial-functor Y k
-      ( map-polynomial-functor comp-polynomial-functor f k (x k)) ＝
-    map-polynomial-functor 𝑄
-      ( map-polynomial-functor 𝑃 f)
-      ( k)
-      ( map-compute-type-comp-polynomial-functor X k (x k))
-  compute-map-comp-polynomial-functor f x k = refl
+    {l8 l9 : Level} {X : I → UU l8} {Y : I → UU l9}
+    (f : (i : I) → X i → Y i) (k : K) →
+    coherence-square-maps
+      ( map-compute-type-comp-polynomial-functor X k)
+      ( map-polynomial-functor comp-polynomial-functor f k)
+      ( map-polynomial-functor 𝑄 (map-polynomial-functor 𝑃 f) k)
+      ( map-compute-type-comp-polynomial-functor Y k)
+  compute-map-comp-polynomial-functor f k x = refl
 ```

From bec24f5da85aad24e9d3870a1df7e81753edcd22 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 16 Jun 2025 18:26:22 +0100
Subject: [PATCH 7/8] order

---
 src/trees/multivariable-polynomial-functors.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/trees/multivariable-polynomial-functors.lagda.md b/src/trees/multivariable-polynomial-functors.lagda.md
index dd021950e7..40f0bebab6 100644
--- a/src/trees/multivariable-polynomial-functors.lagda.md
+++ b/src/trees/multivariable-polynomial-functors.lagda.md
@@ -294,8 +294,8 @@ and `𝑃 C D : (J → Type) → (K → Type)`, then the composite functor
 module _
   {l1 l2 l3 l4 l5 l6 l7 : Level}
   {I : UU l1} {J : UU l2} {K : UU l3}
-  (𝑃@(A , B) : polynomial-functor l4 l5 I J)
   (𝑄@(C , D) : polynomial-functor l6 l7 J K)
+  (𝑃@(A , B) : polynomial-functor l4 l5 I J)
   where
 
   shape-comp-polynomial-functor : K → UU (l2 ⊔ l4 ⊔ l6 ⊔ l7)

From 88c8f6487342b7cb845ea6a95b7a2b073b5fa903 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 17 Jun 2025 16:47:06 +0100
Subject: [PATCH 8/8] edits

---
 src/foundation/structure.lagda.md             |  4 ++
 src/species/hasse-weil-species.lagda.md       |  3 +-
 ...multivariable-polynomial-functors.lagda.md | 39 +++++++++++++------
 3 files changed, 34 insertions(+), 12 deletions(-)

diff --git a/src/foundation/structure.lagda.md b/src/foundation/structure.lagda.md
index 6a5b9217b7..819a679062 100644
--- a/src/foundation/structure.lagda.md
+++ b/src/foundation/structure.lagda.md
@@ -64,3 +64,7 @@ has-structure-equiv' :
   {l1 l2 : Level} (𝒫 : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → 𝒫 Y → 𝒫 X
 has-structure-equiv' 𝒫 e = tr 𝒫 (inv (eq-equiv e))
 ```
+
+## See also
+
+- [Species of types](species.species-of-types.md)
diff --git a/src/species/hasse-weil-species.lagda.md b/src/species/hasse-weil-species.lagda.md
index 4538f31367..849e510d62 100644
--- a/src/species/hasse-weil-species.lagda.md
+++ b/src/species/hasse-weil-species.lagda.md
@@ -26,7 +26,8 @@ types that preserves cartesian products. The **Hasse-Weil species** is a species
 of finite inhabited types defined for any finite inhabited type `k` as
 
 ```text
-Σ (p : structure-semisimple-commutative-ring-Finite-Type k) ; S (commutative-finite-ring-finite-semisimple-commutative-ring-structure-semisimple-commutative-ring-Finite-Type k p)
+Σ ( p : structure-semisimple-commutative-ring-Finite-Type k),
+  ( S (commutative-finite-ring-finite-semisimple-commutative-ring-structure-semisimple-commutative-ring-Finite-Type k p))
 ```
 
 ## Definitions
diff --git a/src/trees/multivariable-polynomial-functors.lagda.md b/src/trees/multivariable-polynomial-functors.lagda.md
index 40f0bebab6..31d0fc02f9 100644
--- a/src/trees/multivariable-polynomial-functors.lagda.md
+++ b/src/trees/multivariable-polynomial-functors.lagda.md
@@ -33,16 +33,15 @@ open import foundation-core.torsorial-type-families
 
 ## Idea
 
-{{#concept "Multivariable polynomial functors"}} are a generalization of the
-notion of [polynomial endofunctors](trees.polynomial-endofunctors.md) to the
-case where one has a family of types(variables) as opposed to a single type.
-
-Given a family of types `A : J → 𝒰` and a type family
-`B : I → {j : J} → A j → 𝒱` over `A`, we have a multivariable polynomial functor
-`P A B` with action on type families given by
+{{#concept "Multivariable polynomial functors" Agda=polynomial-functor}} are a
+generalization of the notion of
+[polynomial endofunctors](trees.polynomial-endofunctors.md) to the case of
+families of types (variables). Given a family of types `A : J → Type` and a type
+family `B : I → {j : J} → A j → Type` over `A`, we have a multivariable
+polynomial functor `𝑃 A B` with action on type families given by
 
 ```text
-  X j ↦ Σ (a : A j), ((i : I) → B i a → X i)
+  𝑃 A B X j := Σ (a : A j), ((i : I) → B i a → X i).
 ```
 
 ## Definitions
@@ -273,7 +272,7 @@ module _
   map-compute-type-id-polynomial-functor X i =
     map-equiv (compute-type-id-polynomial-functor X i)
 
-  compute-map-id-polynomial-functor :
+  coh-map-id-polynomial-functor :
     {l2 l3 : Level} {X : I → UU l2} {Y : I → UU l3} (f : (i : I) → X i → Y i)
     (i : I) →
     coherence-square-maps
@@ -281,7 +280,7 @@ module _
       ( map-polynomial-functor id-polynomial-functor f i)
       ( f i)
       ( map-compute-type-id-polynomial-functor Y i)
-  compute-map-id-polynomial-functor f i = refl-htpy
+  coh-map-id-polynomial-functor f i = refl-htpy
 ```
 
 ### Composition of multivariable polynomial functors
@@ -343,7 +342,7 @@ module _
     ( map-compute-type-comp-polynomial-functor X k ,
       is-equiv-map-compute-type-comp-polynomial-functor X k)
 
-  compute-map-comp-polynomial-functor :
+  coh-map-comp-polynomial-functor :
     {l8 l9 : Level} {X : I → UU l8} {Y : I → UU l9}
     (f : (i : I) → X i → Y i) (k : K) →
     coherence-square-maps
@@ -351,5 +350,23 @@ module _
       ( map-polynomial-functor comp-polynomial-functor f k)
       ( map-polynomial-functor 𝑄 (map-polynomial-functor 𝑃 f) k)
       ( map-compute-type-comp-polynomial-functor Y k)
+  coh-map-comp-polynomial-functor f k x = refl
+
+  compute-map-comp-polynomial-functor :
+    {l8 l9 : Level} {X : I → UU l8} {Y : I → UU l9}
+    (f : (i : I) → X i → Y i) (k : K) →
+    ( map-polynomial-functor comp-polynomial-functor f k) ~
+    ( map-inv-compute-type-comp-polynomial-functor Y k) ∘
+    ( map-polynomial-functor 𝑄 (map-polynomial-functor 𝑃 f) k) ∘
+    ( map-compute-type-comp-polynomial-functor X k)
   compute-map-comp-polynomial-functor f k x = refl
+
+  compute-map-comp-polynomial-functor' :
+    {l8 l9 : Level} {X : I → UU l8} {Y : I → UU l9}
+    (f : (i : I) → X i → Y i) (k : K) →
+    ( map-polynomial-functor 𝑄 (map-polynomial-functor 𝑃 f) k) ~
+    ( map-compute-type-comp-polynomial-functor Y k) ∘
+    ( map-polynomial-functor comp-polynomial-functor f k) ∘
+    ( map-inv-compute-type-comp-polynomial-functor X k)
+  compute-map-comp-polynomial-functor' f k x = refl
 ```