Iterated cartesian products of types equipped with endomorphisms

Content created by Fredrik Bakke and Victor Blanchi.

Created on 2023-05-10.
Last modified on 2023-05-13.

module structured-types.iterated-cartesian-products-types-equipped-with-endomorphisms where
Imports 
open import foundation.universe-levels

open import lists.lists

open import structured-types.cartesian-products-types-equipped-with-endomorphisms
open import structured-types.types-equipped-with-endomorphisms

Idea

From a list of a types equipped with endomorphisms, we define its iterated cartesian product recursively via the cartesian product of types equipped with endomorphism.

Definitions

iterated-product-Endo-list :
  {l : Level} → list (Endo l) → Endo l
iterated-product-Endo-list nil = trivial-Endo
iterated-product-Endo-list (cons A L) =
  product-Endo A (iterated-product-Endo-list L)

Recent changes