Products of tuples of types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-09-12.
Last modified on 2023-06-08.

module foundation.products-of-tuples-of-types where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.tuples-of-types
open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types

Idea

The product of an n-tuple of types is just the dependent product.

Definition

Products of n-tuples of types

product-tuple-types :
  {l : Level} (n : ℕ) → tuple-types l n → UU l
product-tuple-types n A = (i : Fin n) → A i

The projection maps

pr-product-tuple-types :
  {l : Level} {n : ℕ} (A : tuple-types l n) (i : Fin n) →
  product-tuple-types n A → A i
pr-product-tuple-types A i f = f i

{-
equiv-universal-property-product-tuple-types :
  {l : Level} {n : ℕ} (A : tuple-types l (succ-ℕ n)) (i : Fin (succ-ℕ n)) →
  ( product-tuple-types (succ-ℕ n) A) ≃
  ( ( product-tuple-types n {!!}) × A i)
equiv-universal-property-product-tuple-types A i =
  {!!}
  -}

Recent changes