Multivariable polynomial functors

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)

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

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

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