Iterated cartesian products of pointed types

module structured-types.iterated-pointed-cartesian-product-types where

open import foundation.dependent-pair-types
open import foundation.unit-type
open import foundation.universe-levels

open import lists.lists

open import structured-types.pointed-cartesian-product-types
open import structured-types.pointed-types

Idea

Given a list of pointed types l we define recursively the iterated pointed cartesian product of l.

Definition

iterated-product-Pointed-Type :
  {l : Level} → (L : list (Pointed-Type l)) → Pointed-Type l
iterated-product-Pointed-Type nil = raise-unit _ , raise-star
iterated-product-Pointed-Type (cons x L) =
  x ×∗ (iterated-product-Pointed-Type L)