Iterated cartesian products of types equipped with endomorphisms

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-05-10.
Last modified on 2024-02-06.

module
  structured-types.iterated-cartesian-products-types-equipped-with-endomorphisms
  where

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-list-Type-With-Endomorphism :
  {l : Level} → list (Type-With-Endomorphism l) → Type-With-Endomorphism l
iterated-product-list-Type-With-Endomorphism nil =
  trivial-Type-With-Endomorphism
iterated-product-list-Type-With-Endomorphism (cons A L) =
  product-Type-With-Endomorphism A
    ( iterated-product-list-Type-With-Endomorphism L)

Recent changes

• 2024-02-06. Fredrik Bakke. Rename (co)prod to (co)product (#1017).
• 2023-10-08. Egbert Rijke and Fredrik Bakke. Refactoring types with automorphisms/endomorphisms and descent data for the circle (#812).
• 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).