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 _