open import 1Lab.Path
open import 1Lab.Type

module Data.Product.NAry where


# n-Ary productsπ

This is an alternative definition of the type of n-ary products, which, unlike Vec, is defined by recursion on the length.

Vecβ : β {β} β Type β β Nat β Type β
Vecβ A 0             = Lift _ β€
Vecβ A 1             = A
Vecβ A (suc (suc n)) = A Γ Vecβ A (suc n)


The point of having the type Vecβ around is that its inhabitants can be written using the usual tuple syntax, so that we can define a From-product βtype classβ for those type constructors (possibly indexed by the length) which can be built as a sequence of arguments.

_ : Vecβ Nat 3
_ = 1 , 2 , 3

record From-product {β} (A : Type β) (T : Nat β Type β) : Type β where
field from-prod : β n β Vecβ A n β T n


Shuffling the arguments to from-prod slightly, we arrive at the βlist syntaxβ construction:

[_] : β {β} {A : Type β} {T : Nat β Type β} {n} β¦ fp : From-product A T β¦
β Vecβ A n β T n
[_] β¦ fp = fp β¦ = fp .From-product.from-prod _