Tuples of types

module foundation.tuples-of-types where

Imports

open import elementary-number-theory.natural-numbers

open import foundation-core.universe-levels

open import univalent-combinatorics.standard-finite-types

Idea

An n-tuple of types is a type family Fin n → UU.

Definition

tuple-types : (l : Level) (n : ℕ) → UU (lsuc l)
tuple-types l n = Fin n → UU l

Properties

The tuple of types `A j` for `i ≠ j`, given `i`

{-
tuple-types-complement-point :
  {l : Level} {n : ℕ} (A : tuple-types l (succ-ℕ n)) (i : Fin (succ-ℕ n)) →
  tuple-types l n
tuple-types-complement-point A i = {!!}
-}