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.tuples-of-types where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.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 = {!!}
-}

Recent changes