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
- 2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
- 2023-05-10. Victor Blanchi. Iterated cartesian products of concrete groups (#566).