What if Pair and Either were primitive, and other arities of product and coproduct types were generated from them?

NTypes.agda

module NTypes where

open import Data.Empty using (⊥)
open import Agda.Builtin.Unit using (⊤)
open import Data.Nat using (ℕ; zero; suc)
open import Function using (id; _∘_)

infixr 5 _∧_ _v_ _-ary_to_ _,_

record _∧_ (a : Set) (b : Set) : Set where
  constructor _,_
  field 1st : a
  field 2nd : b

_∙ : {a : Set} → a -> a ∧ ⊤
_∙ x = x , _

data _v_ a b : Set where
  ←|_ : a → a v b
  |→_ : b → a v b

NSet : ℕ → Set₁
NSet zero = Set
NSet (suc n) = Set → NSet n

_-ary_to_ : (n : ℕ) → (Set → Set → Set) → Set → NSet n
n -ary f to t0 = nary n id f t0 where
  nary : (n : ℕ) → (Set → Set) → (Set → Set → Set) → Set → NSet n
  nary zero k _ t0 = k t0
  nary (suc n) k f t0 t = nary n (k ∘ f t) f t0

/\ : (n : ℕ) → NSet n
/\ n = n -ary _∧_ to ⊤

\/ : (n : ℕ) → NSet n
\/ n = n -ary _v_ to ⊥

data F : Set where
  f ph : F

data O : Set where
  o oo ooo : O

foo : /\ 3 F O O
foo = ph , oo , ooo ∙

eff : \/ 3 F O O
eff = ←| f

off : \/ 3 F O O
off = |→ ←| o

oof : \/ 3 F O O
oof = |→ |→ ←| oo