This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Iterated cartesian products of types equipped with endomorphisms

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)