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/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md
index a231b5f29e..4904b22306 100644
--- a/src/foundation/universal-property-identity-types.lagda.md
+++ b/src/foundation/universal-property-identity-types.lagda.md
@@ -31,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
 ```
 
@@ -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/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.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..31d0fc02f9
--- /dev/null
+++ b/src/trees/multivariable-polynomial-functors.lagda.md
@@ -0,0 +1,372 @@
+# Multivariable polynomial functors
+
+```agda
+module trees.multivariable-polynomial-functors where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-homotopies
+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.fundamental-theorem-of-identity-types
+open import foundation.homotopies
+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-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
+```
+
+</details>
+
+## Idea
+
+{{#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
+  𝑃 A B 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 → 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 → 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 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)
+    {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
+```
+
+### 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 =
+    map-equiv (compute-type-id-polynomial-functor X i)
+
+  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
+      ( 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)
+  coh-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.
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 l7 : Level}
+  {I : UU l1} {J : UU l2} {K : UU l3}
+  (𝑄@(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)
+  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 {k} c) (λ d → B i {j} (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)
+
+  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
+      ( 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)
+  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
+```
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.