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
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).