Iterated cartesian products of pointed types

Content created by Fredrik Bakke and Victor Blanchi.

Created on 2023-05-10.
Last modified on 2025-10-31.

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)

Recent changes

• 2025-10-31. Fredrik Bakke. chore: Concepts in structured-types (#1658).
• 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).