diff --git a/CHANGELOG.md b/CHANGELOG.md
index 83a1267aef..10d847f4bf 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -83,6 +83,10 @@ New modules
   Data.Nat.Induction
   Data.Fin.Induction
 
+  Data.Product.Nary.NonDependent
+  Function.Nary.NonDependent
+  Relation.Nary
+
   Data.Sign.Base
 
   Data.These.Base
@@ -94,8 +98,14 @@ New modules
 
   Relation.Binary.Construct.Closure.Equivalence.Properties
   Relation.Binary.Rewriting
+
+  Relation.Nullary.Decidable.Core
   ```
 
+* The function `#_` has been moved from `Data.Fin.Base` to `Data.Fin`
+  to break dependency cycles following the introduction of the module
+  `Data.Product.N-ary.Heterogeneous`.
+
 Deprecated features
 -------------------
 The following deprecations have occurred as part of a drive to improve
@@ -123,6 +133,10 @@ been attached to all deprecated names.
   renamed to `IndexedUniverse` to better follow the library conventions. The
   old module still exists exporting the old names, but has been deprecated.
 
+* The `Data.Product.N-ary` modules have been deprecated and their content
+  moved to `Data.Vec.Recursive` to make place for properly heterogeneous
+  n-ary products in `Data.Product.Nary`.
+
 #### Names
 
 * In `Relation.Binary.Core`:
@@ -631,6 +645,14 @@ Other minor additions
   been generalised so that the types of the two equal elements need not
   be at the same universe level.
 
+* Added new proof to `Relation.Binary.PropositionalEquality`:
+  ```
+  Congₙ  : ∀ n (f g : Arrows n as b) → Set _
+  congₙ  : ∀ n (f : Arrows n as b) → Congₙ n f f
+  Substₙ : ∀ n (f g : Arrows n as (Set r)) → Set _
+  substₙ : (f : Arrows n as (Set r)) → Substₙ n f f
+  ```
+
 * Added new proof to `Relation.Binary.PropositionalEquality.Core`:
   ```agda
   ≢-sym : Symmetric _≢_
diff --git a/README.agda b/README.agda
index f8a32fdf32..63b253efb1 100644
--- a/README.agda
+++ b/README.agda
@@ -269,6 +269,11 @@ import README.Function.Reasoning
 
 import README.Debug.Trace
 
+-- An exploration of the generic programs acting on n-ary functions and
+-- n-ary heterogeneous products
+
+import README.Nary
+
 -- Explaining the inspect idiom: use case, equivalent handwritten
 -- auxiliary definitions, and implementation details.
 
diff --git a/README/Nary.agda b/README/Nary.agda
new file mode 100644
index 0000000000..3ea619e746
--- /dev/null
+++ b/README/Nary.agda
@@ -0,0 +1,379 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Examples showing how the generic n-ary operations the stdlib provides
+-- can be used
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module README.Nary where
+
+open import Level using (Level)
+open import Data.Nat.Base
+open import Data.Nat.Properties
+open import Data.Fin using (Fin; fromℕ; #_; inject₁)
+open import Data.List
+open import Data.List.Properties
+open import Data.Product using (_×_; _,_)
+open import Data.Sum using (inj₁; inj₂)
+open import Function
+open import Relation.Nullary
+open import Relation.Binary using (module Tri); open Tri
+open import Relation.Binary.PropositionalEquality
+
+private
+  variable
+    a b c d e : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    D : Set d
+    E : Set e
+
+------------------------------------------------------------------------
+-- Introduction
+------------------------------------------------------------------------
+
+-- Function.Nary.NonDependent and Data.Product.N-ary.Heterogeneous provide
+-- a generic representation of n-ary heterogeneous (non dependent) products
+-- and the corresponding types of (non-dependent) n-ary functions. The
+-- representation works well with inference thus allowing us to use generic
+-- combinators to manipulate such functions.
+
+open import Data.Product.Nary.NonDependent
+open import Function.Nary.NonDependent
+open import Relation.Nary
+
+
+------------------------------------------------------------------------
+-- Generalised equality-manipulating combinators
+------------------------------------------------------------------------
+
+-- By default the standard library provides users with (we are leaving out
+-- the implicit arguments here):
+--
+-- cong   : (f : A₁      → B) → a₁ ≡ b₁           → f a₁   ≡ f b₁
+-- cong₂  : (f : A₁ → A₂ → B) → a₁ ≡ b₁ → a₂ ≡ b₂ → f a₁ a₂ ≡ f b₁ b₂
+--
+-- and
+--
+-- subst  : (P : A₁      → Set p) → a₁ ≡ b₁           → P a₁    → P b₁
+-- subst₂ : (P : A₁ → A₂ → Set p) → a₁ ≡ b₁ → a₂ ≡ b₂ → P a₁ a₂ → P b₁ b₂
+--
+-- This pattern can be generalised to any natural number `n`. Thanks to our
+-- library for n-ary functions, we can write the types and implementations
+-- of `congₙ` and `substₙ`.
+
+------------------------------------------------------------------------
+-- congₙ : ∀ n (f : A₁ → ⋯ → Aₙ → B) →
+--         a₁ ≡ b₁ → ⋯ aₙ ≡ bₙ → f a₁ ⋯ aₙ ≡ f b₁ ⋯ bₙ
+
+-- It may be used directly to prove something:
+
+_ : ∀ (as bs cs : List ℕ) →
+       zip (zip (as ++ []) (map id cs)) (reverse (reverse bs))
+     ≡ zip (zip as cs) bs
+_ = λ as bs cs → congₙ 3 (λ as bs → zip (zip as bs))
+                         (++-identityʳ as)
+                         (map-id cs)
+                         (reverse-involutive bs)
+
+-- Or as part of a longer derivation:
+
+_ : ∀ m n p q → suc (m + (p * n) + (q ^ (m + n)))
+              ≡ (m + 0) + (n * p) + (q ^ m * q ^ n) + 1
+_ = λ m n p q → begin
+    suc (m + (p * n) + (q ^ (m + n))) ≡⟨ +-comm 1 _ ⟩
+    m + (p * n) + (q ^ (m + n)) + 1   ≡⟨ congₙ 3 (λ m n p → m + n + p + 1)
+                                                 (+-comm 0 m)
+                                                 (*-comm p n)
+                                                 (^-distribˡ-+-* q m n)
+                                       ⟩
+    m + 0 + n * p + (q ^ m) * (q ^ n) + 1 ∎ where open ≡-Reasoning
+
+-- Partial application of the functional argument is fine: the number of arguments
+-- `congₙ` is going to take is determined by its first argument (a natural number)
+-- and not by the type of the function it works on.
+
+_ : ∀ m → (m +_) ≡ ((m + 0) +_)
+_ = λ m → congₙ 1 _+_ (+-comm 0 m)
+
+-- We don't have to work on the function's first argument either: we can just as
+-- easily use `congₙ` to act on the second one by `flip`ping it. See `holeₙ` for
+-- a generalisation of this idea allowing to target *any* of the function's
+-- arguments and not just the first or second one.
+
+_ : ∀ m → (_+ m) ≡ (_+ (m + 0))
+_ = λ m → congₙ 1 (flip _+_) (+-comm 0 m)
+
+------------------------------------------------------------------------
+-- substₙ : (P : A₁ → ⋯ → Aₙ → Set p) →
+--          a₁ ≡ b₁ → ⋯ aₙ ≡ bₙ → P a₁ ⋯ aₙ → P b₁ ⋯ bₙ
+
+-- We can play the same type of game with subst
+
+open import Agda.Builtin.Nat using (mod-helper)
+
+-- Because we know from the definition `mod-helper` that this equation holds:
+-- mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j
+-- we should be able to prove the slightly modified statement by transforming
+-- all the `x + 1` into `suc x`. We can do so using `substₙ`.
+
+_ : ∀ k m n j → mod-helper k m (n + 1) (j + 1) ≡ mod-helper (k + 1) m n j
+_ = λ k m n j →
+    let P sk sn sj = mod-helper k m sn sj ≡ mod-helper sk m n j
+    in substₙ P (+-comm 1 k) (+-comm 1 n) (+-comm 1 j) refl
+
+-----------------------------------------------------------------------
+-- Generic programs working on n-ary products & functions
+-----------------------------------------------------------------------
+
+-----------------------------------------------------------------------
+-- curryₙ   : ∀ n → (A₁ × ⋯ × Aₙ → B) → A₁ → ⋯ → Aₙ → B
+-- uncurryₙ : ∀ n → (A₁ → ⋯ → Aₙ → B) → A₁ × ⋯ × Aₙ → B
+
+-- The first thing we may want to do generically is convert between
+-- curried function types and uncurried ones. We can do this by using:
+
+-- They both work the same way so we will focus on curryₙ only here.
+-- If we pass to `curryₙ` the arity of its argument then we obtain a
+-- fully curried function.
+
+curry₁ : (A × B × C × D → E) → A → B → C → D → E
+curry₁ = curryₙ 4
+
+-- Note that here we are not flattening arbitrary nestings: products have
+-- to be right nested. Which means that if you have a deeply-nested product
+-- then it won't be affected by the procedure.
+
+curry₁' : (A × (B × C) × D → E) → A → (B × C) → D → E
+curry₁' = curryₙ 3
+
+-- When we are currying a function, we have no obligation to pass its exact
+-- arity as the parameter: we can decide to only curry part of it like so:
+-- Indeed (A₁ × ⋯ × Aₙ → B) can also be seen as (A₁ × ⋯ × (Aₖ × ⋯ × Aₙ) → B)
+
+curry₂ : (A × B × C × D → E) → A → B → (C × D) → E
+curry₂ = curryₙ 3
+
+-----------------------------------------------------------------------
+-- projₙ : ∀ n (k : Fin n) → (A₁ × ⋯ × Aₙ) → Aₖ₊₁
+
+-- Another useful class of functions to manipulate n-ary product is a
+-- generic projection function. Note the (k + 1) in the return index:
+-- Fin counts from 0 up.
+
+-- It behaves as one expects (Data.Fin's #_ comes in handy to write down
+-- Fin literals):
+
+proj₃ : (A × B × C × D × E) → C
+proj₃ = projₙ 5 (# 2)
+
+-- Of course we can once more project the "tail" of the n-ary product by
+-- passing `projₙ` a natural number which is smaller than the size of the
+-- n-ary product, seeing (A₁ × ⋯ × Aₙ) as (A₁ × ⋯ × (Aₖ × ⋯ × Aₙ)).
+
+proj₃' : (A × B × C × D × E) → C × D × E
+proj₃' = projₙ 3 (# 2)
+
+-----------------------------------------------------------------------
+-- insertₙ : ∀ n (k : Fin (suc n)) →
+--           B → (A₁ × ⋯ Aₙ) → (A₁ × ⋯ × Aₖ × B × Aₖ₊₁ × ⋯ Aₙ)
+
+insert₁ : C → (A × B × D × E) → (A × B × C × D × E)
+insert₁ = insertₙ 4 (# 2)
+
+insert₁' : C → (A × B × D × E) → (A × B × C × D × E)
+insert₁' = insertₙ 3 (# 2)
+
+-- Note that `insertₙ` takes a `Fin (suc n)`. Indeed in an n-ary product
+-- there are (suc n) positions at which one may insert a value. We may
+-- insert at the front or the back of the product:
+
+insert-front : A → (B × C × D × E) → (A × B × C × D × E)
+insert-front = insertₙ 4 (# 0)
+
+insert-back : E → (A × B × C × D) → (A × B × C × D × E)
+insert-back = insertₙ 4 (# 4)
+
+-----------------------------------------------------------------------
+-- removeₙ : ∀ n (k : Fin n) → (A₁ × ⋯ Aₙ) → (A₁ × ⋯ × Aₖ × Aₖ₊₂ × ⋯ Aₙ)
+
+-- Dual to `insertₙ`, we may remove a value.
+
+remove₁ : (A × B × C × D × E) → (A × B × D × E)
+remove₁ = removeₙ 5 (# 2)
+
+-- Inserting at `k` and then removing at `inject₁ k` should yield the identity
+
+remove-insert : C → (A × B × D × E) → (A × B × D × E)
+remove-insert c = removeₙ 5 (inject₁ k) ∘′ insertₙ 4 k c
+    where k = # 2
+
+-----------------------------------------------------------------------
+-- updateₙ : ∀ n (k : Fin n) (f : (a : Aₖ₊₁) → B a) →
+--           (p : A₁ × ⋯ Aₙ) → (A₁ × ⋯ × Aₖ × B (projₙ n k p) × Aₖ₊₂ × ⋯ Aₙ)
+
+-- We can not only project out, insert or remove values: we can update them
+-- in place. The type (and value) of the replacement at position k may depend
+-- upon the current value at position k.
+
+update₁ : (p : A × B × ℕ × C × D) → (A × B × Fin _ × C × D)
+update₁ = updateₙ 5 (# 2) fromℕ
+
+-- We can explicitly use the primed version of `updateₙ` to make it known to
+-- Agda that the update function is non dependent. This type of information
+-- is useful for inference: the tighter the constraints, the easier it is to
+-- find a solution (if possible).
+
+update₂ : (p : A × B × ℕ × C × D) → (A × B × List D × C × D)
+update₂ = λ p → updateₙ′ 5 (# 2) (λ n → replicate n (projₙ 5 (# 4) p)) p
+
+-----------------------------------------------------------------------
+-- _%=_⊢_ : ∀ n → (C → D) → (A₁ → ⋯ Aₙ → D → B) → A₁ → ⋯ → Aₙ → C → B
+
+-- Traditional composition (also known as the index update operator `_⊢_`
+-- in `Relation.Unary`) focuses solely on the first argument of an n-ary
+-- function. `_%=_⊢_` on the other hand allows us to touch any one of the
+-- arguments.
+
+-- In the following example we have a function `f : A → B` and `replicate`
+-- of type `ℕ → B → List B`. We want ̀f` to act on the second argument of
+-- replicate. Which we can do like so.
+
+compose₁ : (A → B) → ℕ → A → List B
+compose₁ f = 1 %= f ⊢ replicate
+
+-- Here we spell out the equivalent explicit variable-manipulation and
+-- prove the two functions equal.
+
+compose₁' : (A → B) → ℕ → A → List B
+compose₁' f n a = replicate n (f a)
+
+compose₁-eq : compose₁ {a} {A} {b} {B} ≡ compose₁'
+compose₁-eq = refl
+
+-----------------------------------------------------------------------
+-- _∷=_⊢_ : ∀ n → A → (A₁ → ⋯ Aₙ → A → B) → A₁ → ⋯ → Aₙ → B
+
+-- Partial application usually focuses on the first argument of a function.
+-- We can now partially apply a function in any of its arguments using
+-- `_∷=_⊢_`. Reusing our example involving replicate: we can specialise it
+-- to only output finite lists of `0`:
+
+apply₁ : ℕ → List ℕ
+apply₁ = 1 ∷= 0 ⊢ replicate
+
+apply₁-eq : apply₁ 3 ≡ 0 ∷ 0 ∷ 0 ∷ []
+apply₁-eq = refl
+
+------------------------------------------------------------------------
+-- holeₙ : ∀ n → (A → (A₁ → ⋯ Aₙ → B)) → A₁ → ⋯ → Aₙ → (A → B)
+
+-- As we have seen earlier, `cong` acts on a function's first variable.
+-- If we want to access the second one, we can use `flip`. But what about
+-- the fourth one? We typically use an explicit λ-abstraction shuffling
+-- variables. Not anymore.
+
+-- Reusing mod-helper just because it takes a lot of arguments:
+
+hole₁ : ∀ k m n j → mod-helper k (m + 1) n j ≡ mod-helper k (suc m) n j
+hole₁ = λ k m n j → cong (holeₙ 2 (mod-helper k) n j) (+-comm m 1)
+
+-----------------------------------------------------------------------
+-- mapₙ : ∀ n → (B → C) → (A₁ → ⋯ Aₙ → B) → (A₁ → ⋯ → Aₙ → C)
+
+-- (R →_) gives us the reader monad (and, a fortiori, functor). That is to
+-- say that given a function (A → B) and an (R → A) we can get an (R → B)
+-- This generalises to n-ary functions.
+
+-- Reusing our `composeₙ` example: instead of applying `f` to the replicated
+-- element, we can map it on the resulting list. Giving us:
+
+map₁ : (A → B) → ℕ → A → List B
+map₁ f = mapₙ 2 (map f) replicate
+
+------------------------------------------------------------------------
+-- constₙ : ∀ n → B → A₁ → ⋯ → Aₙ → B
+
+-- `const` is basically `pure` for the reader monad discussed above. Just
+-- like we can generalise the functorial action corresponding to the reader
+-- functor to n-ary functions, we can do the same for `pure`.
+
+const₁ : A → B → C → D → E → A
+const₁ = constₙ 4
+
+-- Together with `holeₙ`, this means we can make a constant function out
+-- of any of the arguments. The fourth for instance:
+
+const₂ : A → B → C → D → E → D
+const₂ = holeₙ 3 (constₙ 4)
+
+------------------------------------------------------------------------
+-- Generalised quantifiers
+------------------------------------------------------------------------
+
+-- As we have seen multiple times already, one of the advantages of working
+-- with non-dependent products is that they can be easily inferred. This is
+-- a prime opportunity to define generic quantifiers.
+
+-- And because n-ary relations are Set-terminated, there is no ambiguity
+-- where to split between arguments & codomain. As a consequence Agda can
+-- infer even `n`, the number of arguments. We can use notations which are
+-- just like the ones defined in `Relation.Unary`.
+
+------------------------------------------------------------------------
+-- ∃⟨_⟩ : (A₁ → ⋯ → Aₙ → Set r) → Set _
+-- ∃⟨ P ⟩ = ∃ λ a₁ → ⋯ → ∃ λ aₙ → P a₁ ⋯ aₙ
+
+-- Returning to our favourite function taking a lot of arguments: we can
+-- find a set of input for which it evaluates to 666
+
+exist₁ : ∃⟨ (λ k m n j → mod-helper k m n j ≡ 666) ⟩
+exist₁ = 19 , 793 , 3059 , 10 , refl
+
+------------------------------------------------------------------------
+-- ∀[_] : (A₁ → ⋯ → Aₙ → Set r) → Set _
+-- ∀[_] P = ∀ {a₁} → ⋯ → ∀ {aₙ} → P a₁ ⋯ aₙ
+
+all₁ : ∀[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ]
+all₁ {a₁} {a₂} = a₁ ≟ a₂
+
+------------------------------------------------------------------------
+-- Π : (A₁ → ⋯ → Aₙ → Set r) → Set _
+-- Π P = ∀ a₁ → ⋯ → ∀ aₙ → P a₁ ⋯ aₙ
+
+all₂ : Π[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ]
+all₂ = _≟_
+
+------------------------------------------------------------------------
+-- _⇒_ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set s) → (A₁ → ⋯ → Aₙ → Set _)
+-- P ⇒ Q = λ a₁ → ⋯ → λ aₙ → P a₁ ⋯ aₙ → Q a₁ ⋯ aₙ
+
+antisym : ∀[ _≤_ ⇒ _≥_ ⇒ _≡_ ]
+antisym = ≤-antisym
+
+------------------------------------------------------------------------
+-- _∪_ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set s) → (A₁ → ⋯ → Aₙ → Set _)
+-- P ∪ Q = λ a₁ → ⋯ → λ aₙ → P a₁ ⋯ aₙ ⊎ Q a₁ ⋯ aₙ
+
+≤->-connex : Π[ _≤_ ∪ _>_ ]
+≤->-connex m n with <-cmp m n
+... | tri< a ¬b ¬c = inj₁ (<⇒≤ a)
+... | tri≈ ¬a b ¬c = inj₁ (≤-reflexive b)
+... | tri> ¬a ¬b c = inj₂ c
+
+------------------------------------------------------------------------
+-- _∩_ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set s) → (A₁ → ⋯ → Aₙ → Set _)
+-- P ∩ Q = λ a₁ → ⋯ → λ aₙ → P a₁ ⋯ aₙ × Q a₁ ⋯ aₙ
+
+<-inversion : ∀[ _<_ ⇒ _≤_ ∩ _≢_ ]
+<-inversion m<n = <⇒≤ m<n , <⇒≢ m<n
+
+------------------------------------------------------------------------
+-- ∁ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set _)
+-- ∁ P = λ a₁ → ⋯ → λ aₙ → ¬ (P a₁ ⋯ aₙ)
+
+m<n⇒m≱n : ∀[ _>_ ⇒ ∁ _≤_ ]
+m<n⇒m≱n m>n m≤n = <⇒≱ m>n m≤n
diff --git a/src/Data/Fin.agda b/src/Data/Fin.agda
index 5bab778c37..106e0b67c4 100644
--- a/src/Data/Fin.agda
+++ b/src/Data/Fin.agda
@@ -8,6 +8,10 @@
 
 module Data.Fin where
 
+open import Relation.Nullary.Decidable.Core
+open import Data.Nat.Base using (suc)
+import Data.Nat.Properties as ℕₚ
+
 ------------------------------------------------------------------------
 -- Publicly re-export the contents of the base module
 
@@ -18,3 +22,10 @@ open import Data.Fin.Base public
 
 open import Data.Fin.Properties public
   using (_≟_; _≤?_; _<?_)
+
+-- # m = "m".
+
+infix 10 #_
+
+#_ : ∀ m {n} {m<n : True (suc m ℕₚ.≤? n)} → Fin n
+#_ _ {m<n = m<n} = fromℕ≤ (toWitness m<n)
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 284a6168ed..44b709ad87 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -13,15 +13,13 @@
 module Data.Fin.Base where
 
 open import Data.Empty using (⊥-elim)
-open import Data.Nat as ℕ
-  using (ℕ; zero; suc; z≤n; s≤s)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s)
 open import Function using (_∘_; _on_)
 open import Level using () renaming (zero to ℓ₀)
 open import Relation.Nullary using (yes; no)
-open import Relation.Nullary.Decidable using (True; toWitness)
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality
-  using (_≡_; _≢_; refl; cong)
+open import Relation.Nullary.Decidable.Core using (True; toWitness)
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 
 ------------------------------------------------------------------------
 -- Types
@@ -75,13 +73,6 @@ fromℕ≤″ zero    (ℕ.less-than-or-equal refl) = zero
 fromℕ≤″ (suc m) (ℕ.less-than-or-equal refl) =
   suc (fromℕ≤″ m (ℕ.less-than-or-equal refl))
 
--- # m = "m".
-
-infix 10 #_
-
-#_ : ∀ m {n} {m<n : True (suc m ℕ.≤? n)} → Fin n
-#_ _ {m<n = m<n} = fromℕ≤ (toWitness m<n)
-
 -- raise m "i" = "m + i".
 
 raise : ∀ {m} n → Fin m → Fin (n ℕ.+ m)
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index c67805fab3..8299cf1525 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -12,8 +12,7 @@ open import Level using (0ℓ)
 open import Function using (_∘_; flip)
 open import Relation.Binary
 open import Relation.Binary.Core
-open import Relation.Binary.PropositionalEquality.Core
-open import Relation.Binary.PropositionalEquality
+open import Agda.Builtin.Equality
 open import Relation.Nullary using (¬_)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Product/N-ary.agda b/src/Data/Product/N-ary.agda
index 6cd10fa451..0c557fbaf3 100644
--- a/src/Data/Product/N-ary.agda
+++ b/src/Data/Product/N-ary.agda
@@ -1,147 +1,11 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- N-ary products
+-- This module is DEPRECATED. Please use Data.Vec.Recursive instead.
 ------------------------------------------------------------------------
 
--- Vectors (as in Data.Vec) also represent n-ary products, so what is
--- the point of this module? The n-ary products below are intended to
--- be used with a fixed n, in which case the nil constructor can be
--- avoided: pairs are represented as pairs (x , y), not as triples
--- (x , y , unit).
-
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Product.N-ary where
 
-open import Data.Nat as Nat hiding (_^_)
-open import Data.Fin hiding (lift)
-open import Data.Product as P using (_×_ ; _,_ ; ∃₂ ; uncurry)
-open import Data.Sum using (_⊎_)
-open import Data.Unit
-open import Data.Empty
-open import Function
-open import Level using (Lift; lift)
-open import Relation.Binary.PropositionalEquality using (_≡_)
-
--- Types and patterns
-------------------------------------------------------------------------
-
-pattern 2+_ n = suc (suc n)
-
-infix 8 _^_
-_^_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ
-A ^ 0    = Lift _ ⊤
-A ^ 1    = A
-A ^ 2+ n = A × A ^ suc n
-
-pattern [] = lift tt
-
-module _  {a} {A : Set a} where
-
-  infix 3 _∈[_]_
-  _∈[_]_ : A → ∀ n → A ^ n → Set a
-  a ∈[ 0    ] as      = Lift _ ⊥
-  a ∈[ 1    ] a′      = a ≡ a′
-  a ∈[ 2+ n ] a′ , as = a ≡ a′ ⊎ a ∈[ suc n ] as
-
--- Basic operations
-------------------------------------------------------------------------
-
-module _  {a} {A : Set a} where
-
-  cons : ∀ n → A → A ^ n → A ^ suc n
-  cons 0       a _  = a
-  cons (suc n) a as = a , as
-
-  uncons : ∀ n → A ^ suc n → A × A ^ n
-  uncons 0        a        = a , lift tt
-  uncons (suc n)  (a , as) = a , as
-
-  head : ∀ n → A ^ suc n → A
-  head n as = P.proj₁ (uncons n as)
-
-  tail : ∀ n → A ^ suc n → A ^ n
-  tail n as = P.proj₂ (uncons n as)
-
-  lookup : ∀ {n} (k : Fin n) → A ^ n → A
-  lookup {suc n} zero    = head n
-  lookup {suc n} (suc k) = lookup k ∘′ tail n
-
-  replicate : ∀ n → A → A ^ n
-  replicate 0      a = []
-  replicate 1      a = a
-  replicate (2+ n) a = a , replicate (suc n) a
-
-  tabulate : ∀ n → (Fin n → A) → A ^ n
-  tabulate 0      f = []
-  tabulate 1      f = f zero
-  tabulate (2+ n) f = f zero , tabulate (suc n) (f ∘′ suc)
-
-  append : ∀ m n → A ^ m → A ^ n → A ^ (m Nat.+ n)
-  append 0      n xs       ys = ys
-  append 1      n x        ys = cons n x ys
-  append (2+ m) n (x , xs) ys = x , append (suc m) n xs ys
-
-  splitAt : ∀ m n → A ^ (m Nat.+ n) → A ^ m × A ^ n
-  splitAt 0       n xs = [] , xs
-  splitAt (suc m) n xs =
-    let (ys , zs) = splitAt m n (tail (m Nat.+ n) xs) in
-    cons m (head (m Nat.+ n) xs) ys , zs
-
-
--- Manipulating N-ary products
-------------------------------------------------------------------------
-
-module _ {a b} {A : Set a} {B : Set b} where
-
-  map : (A → B) → ∀ n → A ^ n → B ^ n
-  map f 0      as       = lift tt
-  map f 1      a        = f a
-  map f (2+ n) (a , as) = f a , map f (suc n) as
-
-  ap : ∀ n → (A → B) ^ n → A ^ n → B ^ n
-  ap 0      fs       ts       = []
-  ap 1      f        t        = f t
-  ap (2+ n) (f , fs) (t , ts) = f t , ap (suc n) fs ts
-
-module _ {a p} {A : Set a} {P : ℕ → Set p} where
-
-  foldr : P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (2+ n)) →
-          ∀ n → A ^ n → P n
-  foldr p0 p1 p2+ 0      as       = p0
-  foldr p0 p1 p2+ 1      a        = p1 a
-  foldr p0 p1 p2+ (2+ n) (a , as) = p2+ n a (foldr p0 p1 p2+ (suc n) as)
-
-foldl : ∀ {a p} {A : Set a} (P : ℕ → Set p) →
-        P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (2+ n)) →
-        ∀ n → A ^ n → P n
-foldl P p0 p1 p2+ 0      as       = p0
-foldl P p0 p1 p2+ 1      a        = p1 a
-foldl P p0 p1 p2+ (2+ n) (a , as) = let p1′ = p1 a in
-  foldl (P ∘′ suc) p1′ (λ a → p2+ 0 a p1′) (p2+ ∘ suc) (suc n) as
-
-module _ {a} {A : Set a} where
-
-  reverse : ∀ n → A ^ n → A ^ n
-  reverse = foldl (A ^_) [] id (λ n → _,_)
-
-module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
-
-  zipWith : (A → B → C) → ∀ n → A ^ n → B ^ n → C ^ n
-  zipWith f 0      as       bs       = []
-  zipWith f 1      a        b        = f a b
-  zipWith f (2+ n) (a , as) (b , bs) = f a b , zipWith f (suc n) as bs
-
-  unzipWith : (A → B × C) → ∀ n → A ^ n → B ^ n × C ^ n
-  unzipWith f 0      as       = [] , []
-  unzipWith f 1      a        = f a
-  unzipWith f (2+ n) (a , as) = P.zip _,_ _,_ (f a) (unzipWith f (suc n) as)
-
-module _ {a b} {A : Set a} {B : Set b} where
-
-  zip : ∀ n → A ^ n → B ^ n → (A × B) ^ n
-  zip = zipWith _,_
-
-  unzip : ∀ n → (A × B) ^ n → A ^ n × B ^ n
-  unzip = unzipWith id
+open import Data.Vec.Recursive public
diff --git a/src/Data/Product/N-ary/Categorical.agda b/src/Data/Product/N-ary/Categorical.agda
index ba9448972d..bff3287426 100644
--- a/src/Data/Product/N-ary/Categorical.agda
+++ b/src/Data/Product/N-ary/Categorical.agda
@@ -1,61 +1,12 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of N-ary products
+-- This module is DEPRECATED. Please use Data.Vec.Recursive.Categorical
+-- instead.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Product.N-ary.Categorical where
 
-open import Agda.Builtin.Nat
-open import Data.Product hiding (map)
-open import Data.Product.N-ary
-open import Function
-
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
-
-------------------------------------------------------------------------
--- Functor and applicative
-
-functor : ∀ {ℓ} n → RawFunctor {ℓ} (_^ n)
-functor n = record { _<$>_ = λ f → map f n }
-
-applicative : ∀ {ℓ} n → RawApplicative {ℓ} (_^ n)
-applicative n = record
-  { pure = replicate n
-  ; _⊛_  = ap n
-  }
-
-------------------------------------------------------------------------
--- Get access to other monadic functions
-
-module _ {f F} (App : RawApplicative {f} F) where
-
-  open RawApplicative App
-
-  sequenceA : ∀ {n A} → F A ^ n → F (A ^ n)
-  sequenceA {0}    _          = pure _
-  sequenceA {1}    fa         = fa
-  sequenceA {2+ n} (fa , fas) = _,_ <$> fa ⊛ sequenceA fas
-
-  mapA : ∀ {n a} {A : Set a} {B} → (A → F B) → A ^ n → F (B ^ n)
-  mapA f = sequenceA ∘ map f _
-
-  forA : ∀ {n a} {A : Set a} {B} → A ^ n → (A → F B) → F (B ^ n)
-  forA = flip mapA
-
-module _ {m M} (Mon : RawMonad {m} M) where
-
-  private App = RawMonad.rawIApplicative Mon
-
-  sequenceM : ∀ {n A} → M A ^ n → M (A ^ n)
-  sequenceM = sequenceA App
-
-  mapM : ∀ {n a} {A : Set a} {B} → (A → M B) → A ^ n → M (B ^ n)
-  mapM = mapA App
-
-  forM : ∀ {n a} {A : Set a} {B} → A ^ n → (A → M B) → M (B ^ n)
-  forM = forA App
+open import Data.Vec.Recursive.Categorical public
diff --git a/src/Data/Product/N-ary/Properties.agda b/src/Data/Product/N-ary/Properties.agda
index 74a7256af9..dc4b4d437c 100644
--- a/src/Data/Product/N-ary/Properties.agda
+++ b/src/Data/Product/N-ary/Properties.agda
@@ -1,91 +1,12 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Properties of n-ary products
+-- This module is DEPRECATED. Please use Data.Vec.Recursive.Properties
+-- instead.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Product.N-ary.Properties where
 
-open import Data.Nat.Base hiding (_^_)
-open import Data.Product
-open import Data.Product.N-ary
-open import Data.Vec using (Vec; _∷_)
-open import Function.Inverse using (_↔_; inverse)
-open import Relation.Binary.PropositionalEquality as P
-open ≡-Reasoning
-
-------------------------------------------------------------------------
--- Basic proofs
-
-module _ {a} {A : Set a} where
-
-  cons-head-tail-identity : ∀ n (as : A ^ suc n) → cons n (head n as) (tail n as) ≡ as
-  cons-head-tail-identity 0       as = P.refl
-  cons-head-tail-identity (suc n) as = P.refl
-
-  head-cons-identity : ∀ n a (as : A ^ n) → head n (cons n a as) ≡ a
-  head-cons-identity 0       a as = P.refl
-  head-cons-identity (suc n) a as = P.refl
-
-  tail-cons-identity : ∀ n a (as : A ^ n) → tail n (cons n a as) ≡ as
-  tail-cons-identity 0       a as = P.refl
-  tail-cons-identity (suc n) a as = P.refl
-
-  append-cons-commute : ∀ m n a (xs : A ^ m) ys →
-    append (suc m) n (cons m a xs) ys ≡ cons (m + n) a (append m n xs ys)
-  append-cons-commute 0       n a xs ys = P.refl
-  append-cons-commute (suc m) n a xs ys = P.refl
-
-  append-splitAt-identity : ∀ m n (as : A ^ (m + n)) → uncurry (append m n) (splitAt m n as) ≡ as
-  append-splitAt-identity 0       n as = P.refl
-  append-splitAt-identity (suc m) n as = begin
-    let x         = head (m + n) as in
-    let (xs , ys) = splitAt m n (tail (m + n) as) in
-    append (suc m) n (cons m (head (m + n) as) xs) ys
-      ≡⟨ append-cons-commute m n x xs ys ⟩
-    cons (m + n) x (append m n xs ys)
-      ≡⟨ P.cong (cons (m + n) x) (append-splitAt-identity m n (tail (m + n) as)) ⟩
-    cons (m + n) x (tail (m + n) as)
-      ≡⟨ cons-head-tail-identity (m + n) as ⟩
-    as
-      ∎
-
-------------------------------------------------------------------------
--- Conversion to and from Vec
-
-module _ {a} {A : Set a} where
-
-  toVec : ∀ n → A ^ n → Vec A n
-  toVec 0       _  = Vec.[]
-  toVec (suc n) xs = head n xs Vec.∷ toVec n (tail n xs)
-
-  fromVec : ∀ {n} → Vec A n → A ^ n
-  fromVec         Vec.[]       = []
-  fromVec {suc n} (x Vec.∷ xs) = cons n x (fromVec xs)
-
-  fromVec∘toVec : ∀ n (xs : A ^ n) → fromVec (toVec n xs) ≡ xs
-  fromVec∘toVec 0       _  = P.refl
-  fromVec∘toVec (suc n) xs = begin
-    cons n (head n xs) (fromVec (toVec n (tail n xs)))
-      ≡⟨ P.cong (cons n (head n xs)) (fromVec∘toVec n (tail n xs)) ⟩
-    cons n (head n xs) (tail n xs)
-      ≡⟨ cons-head-tail-identity n xs ⟩
-    xs ∎
-
-  toVec∘fromVec : ∀ {n} (xs : Vec A n) → toVec n (fromVec xs) ≡ xs
-  toVec∘fromVec         Vec.[]       = P.refl
-  toVec∘fromVec {suc n} (x Vec.∷ xs) = begin
-    head n (cons n x (fromVec xs)) Vec.∷ toVec n (tail n (cons n x (fromVec xs)))
-      ≡⟨ P.cong₂ (λ x xs → x Vec.∷ toVec n xs) hd-prf tl-prf ⟩
-    x Vec.∷ toVec n (fromVec xs)
-      ≡⟨ P.cong (x Vec.∷_) (toVec∘fromVec xs) ⟩
-    x Vec.∷ xs
-      ∎ where
-
-      hd-prf = head-cons-identity n x (fromVec xs)
-      tl-prf = tail-cons-identity n x (fromVec xs)
-
-  ↔Vec : ∀ n → A ^ n ↔ Vec A n
-  ↔Vec n = inverse (toVec n) fromVec (fromVec∘toVec n) toVec∘fromVec
+open import Data.Vec.Recursive.Properties public
diff --git a/src/Data/Product/Nary/NonDependent.agda b/src/Data/Product/Nary/NonDependent.agda
new file mode 100644
index 0000000000..380fb557de
--- /dev/null
+++ b/src/Data/Product/Nary/NonDependent.agda
@@ -0,0 +1,190 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Nondependent heterogeneous N-ary products
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Product.Nary.NonDependent where
+
+------------------------------------------------------------------------
+-- Concrete examples can be found in README.Nary. This file's comments
+-- are more focused on the implementation details and the motivations
+-- behind the design decisions.
+------------------------------------------------------------------------
+
+open import Level as L using (Level; _⊔_; Lift; 0ℓ)
+open import Agda.Builtin.Unit
+open import Data.Product
+open import Data.Sum using (_⊎_)
+open import Data.Nat.Base using (ℕ; zero; suc; pred)
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Function
+open import Relation.Nullary
+
+open import Function.Nary.NonDependent
+
+-- Provided n Levels and a corresponding "vector" of `n` Sets, we can build a big
+-- right-nested product type packing a value for each one of these Sets.
+-- We have two distinct but equivalent definitions:
+-- the first which is always ⊤-terminated
+-- the other which has a special case for n = 1 because we want our `(un)curryₙ`
+-- functions to work for user-written functions and products and they rarely are
+-- ⊤-terminated.
+
+Product⊤ : ∀ n {ls} → Sets n ls → Set (⨆ n ls)
+Product⊤ zero    as       = ⊤
+Product⊤ (suc n) (a , as) = a × Product⊤ n as
+
+Product : ∀ n {ls} → Sets n ls → Set (⨆ n ls)
+Product 0       _        = ⊤
+Product 1       (a , _)  = a
+Product (suc n) (a , as) = a × Product n as
+
+------------------------------------------------------------------------
+-- Generic Programs
+
+-- Once we have these type definitions, we can write generic programs
+-- over them. They will typically be split into two or three definitions:
+
+-- 1. action on the vector of n levels (if any)
+-- 2. action on the corresponding vector of n Sets
+-- 3. actual program, typed thank to the function defined in step 2.
+------------------------------------------------------------------------
+
+-- see Relation.Binary.PropositionalEquality for congₙ and substₙ, two
+-- equality-related generic programs.
+
+------------------------------------------------------------------------
+-- equivalence of Product and Product⊤
+
+toProduct : ∀ n {ls} {as : Sets n ls} → Product⊤ n as → Product n as
+toProduct 0             _        = _
+toProduct 1             (v , _)  = v
+toProduct (suc (suc n)) (v , vs) = v , toProduct _ vs
+
+toProduct⊤ : ∀ n {ls} {as : Sets n ls} → Product n as → Product⊤ n as
+toProduct⊤ 0             _        = _
+toProduct⊤ 1             v        = v , _
+toProduct⊤ (suc (suc n)) (v , vs) = v , toProduct⊤ _ vs
+
+------------------------------------------------------------------------
+-- (un)curry
+
+-- We start by defining `curryₙ` and `uncurryₙ` converting back and forth
+-- between `A₁ → ⋯ → Aₙ → B` and `(A₁ × ⋯ × Aₙ) → B` by induction on `n`.
+
+curryₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
+         (Product n as → b) → as ⇉ b
+curryₙ 0               f = f _
+curryₙ 1               f = f
+curryₙ (suc n@(suc _)) f = curryₙ n ∘′ curry f
+
+uncurryₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
+           as ⇉ b → (Product n as → b)
+uncurryₙ 0               f = const f
+uncurryₙ 1               f = f
+uncurryₙ (suc n@(suc _)) f = uncurry (uncurryₙ n ∘′ f)
+
+-- Variants for Product⊤
+
+curry⊤ₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
+          (Product⊤ n as → b) → as ⇉ b
+curry⊤ₙ n f = curryₙ n (f ∘ toProduct⊤ n)
+
+uncurry⊤ₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
+            as ⇉ b → (Product⊤ n as → b)
+uncurry⊤ₙ n f = uncurryₙ n f ∘ toProduct n
+
+------------------------------------------------------------------------
+-- projection of the k-th component
+
+-- To know at which Set level the k-th projection out of an n-ary product
+-- lives, we need to extract said level, by induction on k.
+
+Levelₙ : ∀ {n} → Levels n → Fin n → Level
+Levelₙ (l , _)  zero    = l
+Levelₙ (_ , ls) (suc k) = Levelₙ ls k
+
+-- Once we have the Sets used in the product, we can extract the one we
+-- are interested in, once more by induction on k.
+
+Projₙ : ∀ {n ls} → Sets n ls → ∀ k → Set (Levelₙ ls k)
+Projₙ (a , _)  zero    = a
+Projₙ (_ , as) (suc k) = Projₙ as k
+
+-- Finally, provided a Product of these sets, we can extract the k-th value.
+-- `projₙ` takes both `n` and `k` explicitly because we expect the user will
+-- be using a concrete `k` (potentially manufactured using `Data.Fin`'s `#_`)
+-- and it will not be possible to infer `n` from it.
+
+projₙ : ∀ n {ls} {as : Sets n ls} k → Product n as → Projₙ as k
+projₙ 1               zero    v        = v
+projₙ (suc n@(suc _)) zero    (v , _)  = v
+projₙ (suc n@(suc _)) (suc k) (_ , vs) = projₙ n k vs
+projₙ 1 (suc ()) v
+
+------------------------------------------------------------------------
+-- removal of the k-th component
+
+Levelₙ⁻ : ∀ {n} → Levels n → Fin n → Levels (pred n)
+Levelₙ⁻               (_ , ls) zero    = ls
+Levelₙ⁻ {suc (suc _)} (l , ls) (suc k) = l , Levelₙ⁻ ls k
+Levelₙ⁻ {1} _ (suc ())
+
+Removeₙ : ∀ {n ls} → Sets n ls → ∀ k → Sets (pred n) (Levelₙ⁻ ls k)
+Removeₙ               (_ , as) zero    = as
+Removeₙ {suc (suc _)} (a , as) (suc k) = a , Removeₙ as k
+Removeₙ {1} _ (suc ())
+
+removeₙ : ∀ n {ls} {as : Sets n ls} k →
+          Product n as → Product (pred n) (Removeₙ as k)
+removeₙ (suc zero)          zero    _        = _
+removeₙ (suc (suc _))       zero    (_ , vs) = vs
+removeₙ (suc (suc zero))    (suc k) (v , _)  = v
+removeₙ (suc (suc (suc _))) (suc k) (v , vs) = v , removeₙ _ k vs
+removeₙ (suc zero) (suc ()) _
+
+------------------------------------------------------------------------
+-- insertion of a k-th component
+
+Levelₙ⁺ : ∀ {n} → Levels n → Fin (suc n) → Level → Levels (suc n)
+Levelₙ⁺         ls       zero    l⁺ = l⁺ , ls
+Levelₙ⁺ {suc _} (l , ls) (suc k) l⁺ = l , Levelₙ⁺ ls k l⁺
+Levelₙ⁺ {0} _ (suc ())
+
+Insertₙ : ∀ {n ls l⁺} → Sets n ls → ∀ k (a⁺ : Set l⁺) → Sets (suc n) (Levelₙ⁺ ls k l⁺)
+Insertₙ         as       zero    a⁺ = a⁺ , as
+Insertₙ {suc _} (a , as) (suc k) a⁺ = a , Insertₙ as k a⁺
+Insertₙ {zero} _ (suc ()) _
+
+insertₙ : ∀ n {ls l⁺} {as : Sets n ls} {a⁺ : Set l⁺} k (v⁺ : a⁺) →
+          Product n as → Product (suc n) (Insertₙ as k a⁺)
+insertₙ 0             zero    v⁺ vs       = v⁺
+insertₙ (suc n)       zero    v⁺ vs       = v⁺ , vs
+insertₙ 1             (suc k) v⁺ vs       = vs , insertₙ 0 k v⁺ _
+insertₙ (suc (suc n)) (suc k) v⁺ (v , vs) = v , insertₙ _ k v⁺ vs
+insertₙ 0 (suc ()) _ _
+
+------------------------------------------------------------------------
+-- update of a k-th component
+
+Levelₙᵘ : ∀ {n} → Levels n → Fin n → Level → Levels n
+Levelₙᵘ (_ , ls) zero    lᵘ = lᵘ , ls
+Levelₙᵘ (l , ls) (suc k) lᵘ = l , Levelₙᵘ ls k lᵘ
+
+Updateₙ : ∀ {n ls lᵘ} (as : Sets n ls) k (aᵘ : Set lᵘ) → Sets n (Levelₙᵘ ls k lᵘ)
+Updateₙ (_ , as) zero    aᵘ = aᵘ , as
+Updateₙ (a , as) (suc k) aᵘ = a , Updateₙ as k aᵘ
+
+updateₙ : ∀ n {ls lᵘ} {as : Sets n ls} k {aᵘ : _ → Set lᵘ} (f : ∀ v → aᵘ v)
+          (vs : Product n as) → Product n (Updateₙ as k (aᵘ (projₙ n k vs)))
+updateₙ 1             zero    f v        = f v
+updateₙ (suc (suc _)) zero    f (v , vs) = f v , vs
+updateₙ (suc (suc _)) (suc k) f (v , vs) = v , updateₙ _ k f vs
+updateₙ 1 (suc ()) _ _
+
+updateₙ′ : ∀ n {ls lᵘ} {as : Sets n ls} k {aᵘ : Set lᵘ} (f : Projₙ as k → aᵘ) →
+           Product n as → Product n (Updateₙ as k aᵘ)
+updateₙ′ n k = updateₙ n k
diff --git a/src/Data/Unit.agda b/src/Data/Unit.agda
index 17747dfee4..8b51f3b592 100644
--- a/src/Data/Unit.agda
+++ b/src/Data/Unit.agda
@@ -11,8 +11,7 @@ module Data.Unit where
 open import Data.Sum
 open import Relation.Nullary
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as PropEq
-  using (_≡_; refl)
+import Relation.Binary.PropositionalEquality as PropEq
 
 ------------------------------------------------------------------------
 -- Re-export contents of base module
@@ -25,7 +24,6 @@ open import Data.Unit.Base public
 open import Data.Unit.Properties public
   using (_≟_; _≤?_)
 
-
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda
new file mode 100644
index 0000000000..17735f845c
--- /dev/null
+++ b/src/Data/Vec/Recursive.agda
@@ -0,0 +1,149 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Vectors defined by recursion
+------------------------------------------------------------------------
+
+-- What is the point of this module? The n-ary products below are intended
+-- to be used with a fixed n, in which case the nil constructor can be
+-- avoided: pairs are represented as pairs (x , y), not as triples
+-- (x , y , unit).
+-- Additionally, vectors defined by recursion enjoy η-rules. That is to say
+-- that two vectors of known length are definitionally equal whenever their
+-- elements are.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Vec.Recursive where
+
+open import Level using (Level; Lift; lift)
+open import Data.Nat.Base as Nat using (ℕ; zero; suc)
+open import Data.Empty
+open import Data.Fin.Base as Fin using (Fin; zero; suc)
+open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂)
+open import Data.Sum.Base as Sum using (_⊎_)
+open import Data.Unit.Base
+open import Data.Vec as Vec using (Vec; _∷_)
+open import Function
+open import Relation.Unary
+open import Agda.Builtin.Equality using (_≡_)
+
+private
+  variable
+    a b c p : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+-- Types and patterns
+------------------------------------------------------------------------
+
+pattern 2+_ n = suc (suc n)
+
+infix 8 _^_
+_^_ : Set a → ℕ → Set a
+A ^ 0    = Lift _ ⊤
+A ^ 1    = A
+A ^ 2+ n = A × A ^ suc n
+
+pattern [] = lift tt
+
+infix 3 _∈[_]_
+_∈[_]_ : {A : Set a} → A → ∀ n → A ^ n → Set a
+a ∈[ 0    ] as      = Lift _ ⊥
+a ∈[ 1    ] a′      = a ≡ a′
+a ∈[ 2+ n ] a′ , as = a ≡ a′ ⊎ a ∈[ suc n ] as
+
+-- Basic operations
+------------------------------------------------------------------------
+
+cons : ∀ n → A → A ^ n → A ^ suc n
+cons 0       a _  = a
+cons (suc n) a as = a , as
+
+uncons : ∀ n → A ^ suc n → A × A ^ n
+uncons 0        a        = a , lift tt
+uncons (suc n)  (a , as) = a , as
+
+head : ∀ n → A ^ suc n → A
+head n as = proj₁ (uncons n as)
+
+tail : ∀ n → A ^ suc n → A ^ n
+tail n as = proj₂ (uncons n as)
+
+fromVec : ∀[ Vec A ⇒ (A ^_) ]
+fromVec = Vec.foldr (_ ^_) (cons _) _
+
+toVec : Π[ (A ^_) ⇒ Vec A ]
+toVec 0       as = Vec.[]
+toVec (suc n) as = head n as ∷ toVec n (tail n as)
+
+lookup : ∀ {n} (k : Fin n) → A ^ n → A
+lookup zero        = head _
+lookup (suc {n} k) = lookup k ∘′ tail n
+
+replicate : ∀ n → A → A ^ n
+replicate n a = fromVec (Vec.replicate a)
+
+tabulate : ∀ n → (Fin n → A) → A ^ n
+tabulate n f = fromVec (Vec.tabulate f)
+
+append : ∀ m n → A ^ m → A ^ n → A ^ (m Nat.+ n)
+append 0      n xs       ys = ys
+append 1      n x        ys = cons n x ys
+append (2+ m) n (x , xs) ys = x , append (suc m) n xs ys
+
+splitAt : ∀ m n → A ^ (m Nat.+ n) → A ^ m × A ^ n
+splitAt 0       n xs = [] , xs
+splitAt (suc m) n xs =
+  let (ys , zs) = splitAt m n (tail (m Nat.+ n) xs) in
+  cons m (head (m Nat.+ n) xs) ys , zs
+
+
+-- Manipulating N-ary products
+------------------------------------------------------------------------
+
+map : (A → B) → ∀ n → A ^ n → B ^ n
+map f 0      as       = lift tt
+map f 1      a        = f a
+map f (2+ n) (a , as) = f a , map f (suc n) as
+
+ap : ∀ n → (A → B) ^ n → A ^ n → B ^ n
+ap 0      fs       ts       = []
+ap 1      f        t        = f t
+ap (2+ n) (f , fs) (t , ts) = f t , ap (suc n) fs ts
+
+module _ {P : ℕ → Set p} where
+
+  foldr : P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (2+ n)) →
+          ∀ n → A ^ n → P n
+  foldr p0 p1 p2+ 0      as       = p0
+  foldr p0 p1 p2+ 1      a        = p1 a
+  foldr p0 p1 p2+ (2+ n) (a , as) = p2+ n a (foldr p0 p1 p2+ (suc n) as)
+
+foldl : (P : ℕ → Set p) →
+        P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (2+ n)) →
+        ∀ n → A ^ n → P n
+foldl P p0 p1 p2+ 0      as       = p0
+foldl P p0 p1 p2+ 1      a        = p1 a
+foldl P p0 p1 p2+ (2+ n) (a , as) = let p1′ = p1 a in
+  foldl (P ∘′ suc) p1′ (λ a → p2+ 0 a p1′) (p2+ ∘ suc) (suc n) as
+
+reverse : ∀ n → A ^ n → A ^ n
+reverse = foldl (_ ^_) [] id (λ n → _,_)
+
+zipWith : (A → B → C) → ∀ n → A ^ n → B ^ n → C ^ n
+zipWith f 0      as       bs       = []
+zipWith f 1      a        b        = f a b
+zipWith f (2+ n) (a , as) (b , bs) = f a b , zipWith f (suc n) as bs
+
+unzipWith : (A → B × C) → ∀ n → A ^ n → B ^ n × C ^ n
+unzipWith f 0      as       = [] , []
+unzipWith f 1      a        = f a
+unzipWith f (2+ n) (a , as) = Prod.zip _,_ _,_ (f a) (unzipWith f (suc n) as)
+
+zip : ∀ n → A ^ n → B ^ n → (A × B) ^ n
+zip = zipWith _,_
+
+unzip : ∀ n → (A × B) ^ n → A ^ n × B ^ n
+unzip = unzipWith id
diff --git a/src/Data/Vec/Recursive/Categorical.agda b/src/Data/Vec/Recursive/Categorical.agda
new file mode 100644
index 0000000000..3548fab9eb
--- /dev/null
+++ b/src/Data/Vec/Recursive/Categorical.agda
@@ -0,0 +1,61 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A categorical view of vectors defined by recursion
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Vec.Recursive.Categorical where
+
+open import Agda.Builtin.Nat
+open import Data.Product hiding (map)
+open import Data.Vec.Recursive
+open import Function
+
+open import Category.Functor
+open import Category.Applicative
+open import Category.Monad
+
+------------------------------------------------------------------------
+-- Functor and applicative
+
+functor : ∀ {ℓ} n → RawFunctor {ℓ} (_^ n)
+functor n = record { _<$>_ = λ f → map f n }
+
+applicative : ∀ {ℓ} n → RawApplicative {ℓ} (_^ n)
+applicative n = record
+  { pure = replicate n
+  ; _⊛_  = ap n
+  }
+
+------------------------------------------------------------------------
+-- Get access to other monadic functions
+
+module _ {f F} (App : RawApplicative {f} F) where
+
+  open RawApplicative App
+
+  sequenceA : ∀ {n A} → F A ^ n → F (A ^ n)
+  sequenceA {0}    _          = pure _
+  sequenceA {1}    fa         = fa
+  sequenceA {2+ n} (fa , fas) = _,_ <$> fa ⊛ sequenceA fas
+
+  mapA : ∀ {n a} {A : Set a} {B} → (A → F B) → A ^ n → F (B ^ n)
+  mapA f = sequenceA ∘ map f _
+
+  forA : ∀ {n a} {A : Set a} {B} → A ^ n → (A → F B) → F (B ^ n)
+  forA = flip mapA
+
+module _ {m M} (Mon : RawMonad {m} M) where
+
+  private App = RawMonad.rawIApplicative Mon
+
+  sequenceM : ∀ {n A} → M A ^ n → M (A ^ n)
+  sequenceM = sequenceA App
+
+  mapM : ∀ {n a} {A : Set a} {B} → (A → M B) → A ^ n → M (B ^ n)
+  mapM = mapA App
+
+  forM : ∀ {n a} {A : Set a} {B} → A ^ n → (A → M B) → M (B ^ n)
+  forM = forA App
diff --git a/src/Data/Vec/Recursive/Properties.agda b/src/Data/Vec/Recursive/Properties.agda
new file mode 100644
index 0000000000..e1bce0d557
--- /dev/null
+++ b/src/Data/Vec/Recursive/Properties.agda
@@ -0,0 +1,85 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of n-ary products
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Vec.Recursive.Properties where
+
+open import Level using (Level)
+open import Data.Nat.Base hiding (_^_)
+open import Data.Product
+open import Data.Vec.Recursive
+open import Data.Vec using (Vec; _∷_)
+open import Function.Inverse using (_↔_; inverse)
+open import Relation.Binary.PropositionalEquality as P
+open ≡-Reasoning
+
+private
+  variable
+    a : Level
+    A : Set a
+
+------------------------------------------------------------------------
+-- Basic proofs
+
+cons-head-tail-identity : ∀ n (as : A ^ suc n) → cons n (head n as) (tail n as) ≡ as
+cons-head-tail-identity 0       as = P.refl
+cons-head-tail-identity (suc n) as = P.refl
+
+head-cons-identity : ∀ n a (as : A ^ n) → head n (cons n a as) ≡ a
+head-cons-identity 0       a as = P.refl
+head-cons-identity (suc n) a as = P.refl
+
+tail-cons-identity : ∀ n a (as : A ^ n) → tail n (cons n a as) ≡ as
+tail-cons-identity 0       a as = P.refl
+tail-cons-identity (suc n) a as = P.refl
+
+append-cons-commute : ∀ m n a (xs : A ^ m) ys →
+  append (suc m) n (cons m a xs) ys ≡ cons (m + n) a (append m n xs ys)
+append-cons-commute 0       n a xs ys = P.refl
+append-cons-commute (suc m) n a xs ys = P.refl
+
+append-splitAt-identity : ∀ m n (as : A ^ (m + n)) → uncurry (append m n) (splitAt m n as) ≡ as
+append-splitAt-identity 0       n as = P.refl
+append-splitAt-identity (suc m) n as = begin
+  let x         = head (m + n) as in
+  let (xs , ys) = splitAt m n (tail (m + n) as) in
+  append (suc m) n (cons m (head (m + n) as) xs) ys
+    ≡⟨ append-cons-commute m n x xs ys ⟩
+  cons (m + n) x (append m n xs ys)
+    ≡⟨ P.cong (cons (m + n) x) (append-splitAt-identity m n (tail (m + n) as)) ⟩
+  cons (m + n) x (tail (m + n) as)
+    ≡⟨ cons-head-tail-identity (m + n) as ⟩
+  as
+    ∎
+
+------------------------------------------------------------------------
+-- Conversion to and from Vec
+
+fromVec∘toVec : ∀ n (xs : A ^ n) → fromVec (toVec n xs) ≡ xs
+fromVec∘toVec 0       _  = P.refl
+fromVec∘toVec (suc n) xs = begin
+  cons n (head n xs) (fromVec (toVec n (tail n xs)))
+    ≡⟨ P.cong (cons n (head n xs)) (fromVec∘toVec n (tail n xs)) ⟩
+  cons n (head n xs) (tail n xs)
+    ≡⟨ cons-head-tail-identity n xs ⟩
+  xs ∎
+
+toVec∘fromVec : ∀ {n} (xs : Vec A n) → toVec n (fromVec xs) ≡ xs
+toVec∘fromVec             Vec.[]       = P.refl
+toVec∘fromVec {n = suc n} (x Vec.∷ xs) = begin
+  head n (cons n x (fromVec xs)) Vec.∷ toVec n (tail n (cons n x (fromVec xs)))
+    ≡⟨ P.cong₂ (λ x xs → x Vec.∷ toVec n xs) hd-prf tl-prf ⟩
+  x Vec.∷ toVec n (fromVec xs)
+    ≡⟨ P.cong (x Vec.∷_) (toVec∘fromVec xs) ⟩
+  x Vec.∷ xs
+    ∎ where
+
+  hd-prf = head-cons-identity _ x (fromVec xs)
+  tl-prf = tail-cons-identity _ x (fromVec xs)
+
+↔Vec : ∀ n → A ^ n ↔ Vec A n
+↔Vec n = inverse (toVec n) fromVec (fromVec∘toVec n) toVec∘fromVec
diff --git a/src/Function/Nary/NonDependent.agda b/src/Function/Nary/NonDependent.agda
new file mode 100644
index 0000000000..ca0b95f579
--- /dev/null
+++ b/src/Function/Nary/NonDependent.agda
@@ -0,0 +1,155 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Heterogeneous N-ary Functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Function.Nary.NonDependent where
+
+------------------------------------------------------------------------
+-- Concrete examples can be found in README.Nary. This file's comments
+-- are more focused on the implementation details and the motivations
+-- behind the design decisions.
+------------------------------------------------------------------------
+
+open import Level using (Level; 0ℓ; _⊔_; Lift)
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Product using (_×_; _,_)
+open import Data.Unit.Base
+open import Function using (_∘′_; _$′_; const; flip)
+open import Relation.Unary using (IUniversal)
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Type Definitions
+
+-- We want to define n-ary function spaces and generic n-ary operations on
+-- them such as (un)currying, zipWith, alignWith, etc.
+
+-- We want users to be able to use these seamlessly whenever n is concrete.
+
+-- In other words, we want Agda to infer the sets `A₁, ⋯, Aₙ` when we write
+-- `uncurryₙ n f` where `f` has type `A₁ → ⋯ → Aₙ → B`. For this to happen,
+-- we need the structure in which these Sets are stored to effectively
+-- η-expand to `A₁, ⋯, Aₙ` when the parameter `n` is known.
+
+-- Hence the following definitions:
+------------------------------------------------------------------------
+
+-- First, a "vector" of `n` Levels (defined by induction on n so that it
+-- may be built by η-expansion and unification). Each Level will be that
+-- of one of the Sets we want to take the n-ary product of.
+
+Levels : ℕ → Set
+Levels zero    = ⊤
+Levels (suc n) = Level × Levels n
+
+-- The overall Level of a `n` Sets of respective levels `l₁, ⋯, lₙ` will
+-- be the least upper bound `l₁ ⊔ ⋯ ⊔ lₙ` of all of the Levels involved.
+-- Hence the following definition of n-ary least upper bound:
+
+⨆ : ∀ n → Levels n → Level
+⨆ zero    _        = Level.zero
+⨆ (suc n) (l , ls) = l ⊔ (⨆ n ls)
+
+-- Second, a "vector" of `n` Sets whose respective Levels are determined
+-- by the `Levels n` input.
+
+Sets : ∀ n (ls : Levels n) → Set (Level.suc (⨆ n ls))
+Sets zero    _        = Lift _ ⊤
+Sets (suc n) (l , ls) = Set l × Sets n ls
+
+-- Third, a function type whose domains are given by a "vector" of `n` Sets
+-- `A₁, ⋯, Aₙ` and whose codomain is `B`. `Arrows` forms such a type of
+-- shape `A₁ → ⋯ → Aₙ → B` by induction on `n`.
+
+Arrows : ∀ n {r ls} → Sets n ls → Set r → Set (r ⊔ (⨆ n ls))
+Arrows zero    _        b = b
+Arrows (suc n) (a , as) b = a → Arrows n as b
+
+-- We introduce a notation for this definition
+
+infixr 0 _⇉_
+_⇉_ : ∀ {n ls r} → Sets n ls → Set r → Set (r ⊔ (⨆ n ls))
+_⇉_ = Arrows _
+
+
+
+------------------------------------------------------------------------
+-- Operations on Levels
+
+lmap : (Level → Level) → ∀ n → Levels n → Levels n
+lmap f zero    ls       = _
+lmap f (suc n) (l , ls) = f l , lmap f n ls
+
+ltabulate : ∀ n → (Fin n → Level) → Levels n
+ltabulate zero    f = _
+ltabulate (suc n) f = f zero , ltabulate n (f ∘′ suc)
+
+lreplicate : ∀ n → Level → Levels n
+lreplicate n ℓ = ltabulate n (const ℓ)
+
+0ℓs : ∀[ Levels ]
+0ℓs = lreplicate _ 0ℓ
+
+
+------------------------------------------------------------------------
+-- Operations on Sets
+
+_<$>_ : (∀ {l} → Set l → Set l) →
+        ∀ {n ls} → Sets n ls → Sets n ls
+_<$>_ f {zero}   as        = _
+_<$>_ f {suc n}  (a , as)  = f a , f <$> as
+
+-- generalised map
+
+smap : ∀ f → (∀ {l} → Set l → Set (f l)) →
+       ∀ n {ls} → Sets n ls → Sets n (lmap f n ls)
+smap f F zero    as       = _
+smap f F (suc n) (a , as) = F a , smap f F n as
+
+
+------------------------------------------------------------------------
+-- Operations on Functions
+
+-- mapping under n arguments
+
+mapₙ : ∀ n {ls} {as : Sets n ls} → (B → C) → as ⇉ B → as ⇉ C
+mapₙ zero    f v = f v
+mapₙ (suc n) f g = mapₙ n f ∘′ g
+
+-- compose function at the n-th position
+
+_%=_⊢_ : ∀ n {ls} {as : Sets n ls} → (A → B) → as ⇉ (B → C) → as ⇉ (A → C)
+n %= f ⊢ g = mapₙ n (_∘′ f) g
+
+-- partially apply function at the n-th position
+
+_∷=_⊢_ : ∀ n {ls} {as : Sets n ls} → A → as ⇉ (A → B) → as ⇉ B
+n ∷= x ⊢ g = mapₙ n (_$′ x) g
+
+-- hole at the n-th position
+
+holeₙ : ∀ n {ls} {as : Sets n ls} → (A → as ⇉ B) → as ⇉ (A → B)
+holeₙ zero    f = f
+holeₙ (suc n) f = holeₙ n ∘′ flip f
+
+-- function constant in its n first arguments
+
+-- Note that its type will only be inferred if it is used in a context
+-- specifying what the type of the function ought to be. Just like the
+-- usual const: there is no way to infer its domain from its argument.
+
+constₙ : ∀ n {ls r} {as : Sets n ls} {b : Set r} → b → as ⇉ b
+constₙ zero    v = v
+constₙ (suc n) v = const (constₙ n v)
+
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index b2a8eff9d6..b301d4f3c2 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -12,9 +12,13 @@ import Axiom.Extensionality.Propositional as Ext
 open import Axiom.UniquenessOfIdentityProofs
 open import Function
 open import Function.Equality using (Π; _⟶_; ≡-setoid)
-open import Level
+open import Function.Nary.NonDependent
+open import Level as L
 open import Data.Empty
+open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product
+open import Function.Nary.NonDependent
+
 open import Relation.Nullary using (yes ; no)
 open import Relation.Unary using (Pred)
 open import Relation.Binary
@@ -48,6 +52,32 @@ cong-app refl x = refl
 cong₂ : ∀ (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
 cong₂ f refl refl = refl
 
+------------------------------------------------------------------------
+-- n-ary versions of `cong` and `subst`
+
+Congₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
+        (f g : as ⇉ b) → Set (r ⊔ (⨆ n ls))
+Congₙ zero    f g = f ≡ g
+Congₙ (suc n) f g = ∀ {x y} → x ≡ y → Congₙ n (f x) (g y)
+
+congₙ : ∀ n {ls} {as : Sets n ls} {r} {b : Set r} →
+        (f : as ⇉ b) → Congₙ n f f
+congₙ zero    f      = refl
+congₙ (suc n) f refl = congₙ n (f _)
+
+Substₙ : ∀ n {r ls} {as : Sets n ls} →
+         (f g : as ⇉ Set r) → Set (r ⊔ (⨆ n ls))
+Substₙ zero    f g = f → g
+Substₙ (suc n) f g = ∀ {x y} → x ≡ y → Substₙ n (f x) (g y)
+
+substₙ : ∀ {n r ls} {as : Sets n ls} →
+        (f : as ⇉ Set r) → Substₙ n f f
+substₙ {zero}  f x    = x
+substₙ {suc n} f refl = substₙ (f _)
+
+------------------------------------------------------------------------
+-- Structure of equality as a binary relation
+
 setoid : Set a → Setoid _ _
 setoid A = record
   { Carrier       = A
diff --git a/src/Relation/Nary.agda b/src/Relation/Nary.agda
new file mode 100644
index 0000000000..158a3855a3
--- /dev/null
+++ b/src/Relation/Nary.agda
@@ -0,0 +1,128 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Heterogeneous N-ary Relations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Nary where
+
+------------------------------------------------------------------------
+-- Concrete examples can be found in README.Nary. This file's comments
+-- are more focused on the implementation details and the motivations
+-- behind the design decisions.
+------------------------------------------------------------------------
+
+open import Level using (Level; _⊔_)
+open import Data.Nat.Base using (zero; suc)
+open import Data.Product using (_×_; _,_)
+open import Data.Product.Nary.NonDependent using (Product⊤; curry⊤ₙ; uncurry⊤ₙ)
+open import Data.Sum using (_⊎_)
+open import Function using (_$_)
+open import Function.Nary.NonDependent
+open import Relation.Nullary using (¬_)
+import Relation.Unary as Unary
+
+private
+  variable
+    r : Level
+    R : Set r
+
+------------------------------------------------------------------------
+-- Generic type constructors
+
+-- `Relation.Unary` provides users with a wealth of combinators to work
+-- with indexed sets. We can generalise these to n-ary relations.
+
+-- The crucial thing to notice here is that because we are explicitly
+-- considering that the input function should be a `Set`-ended `Arrows`,
+-- all the other parameters are inferrable. This allows us to make the
+-- number arguments (`n`) implicit.
+------------------------------------------------------------------------
+
+------------------------------------------------------------------------
+-- Quantifiers
+
+-- If we already know how to quantify over one variable, we can easily
+-- describe how to quantify over `n` variables by induction over said `n`.
+
+quantₙ : (∀ {i l} {I : Set i} → (I → Set l) → Set (i ⊔ l)) →
+         ∀ n {ls} {as : Sets n ls} →
+         Arrows n as (Set r) → Set (r ⊔ (⨆ n ls))
+quantₙ Q zero     f = f
+quantₙ Q (suc n)  f = Q (λ x → quantₙ Q n (f x))
+
+infix 5 ∃⟨_⟩ Π[_] ∀[_]
+
+-- existential quantifier
+
+∃⟨_⟩ : ∀ {n ls r} {as : Sets n ls} → as ⇉ Set r → Set (r ⊔ (⨆ n ls))
+∃⟨_⟩ = quantₙ Unary.Satisfiable _
+
+-- explicit universal quantifiers
+
+Π[_] : ∀ {n ls r} {as : Sets n ls} → as ⇉ Set r → Set (r ⊔ (⨆ n ls))
+Π[_] = quantₙ Unary.Universal _
+
+-- implicit universal quantifiers
+
+∀[_] : ∀ {n ls r} {as : Sets n ls} → as ⇉ Set r → Set (r ⊔ (⨆ n ls))
+∀[_] = quantₙ Unary.IUniversal _
+
+
+
+------------------------------------------------------------------------
+-- Pointwise liftings of k-ary operators
+
+-- Rather than having multiple ad-hoc lifting functions for various arities
+-- we have a fully generic liftₙ functional which lifts a k-ary operator
+-- to work with k n-ary functions whose respective codomains match the domains
+-- of the operator.
+-- The type of liftₙ is fairly unreadable. Here it is written with ellipsis:
+
+-- liftₙ : ∀ k n. (B₁ → ⋯ → Bₖ → R) →
+--                (A₁ → ⋯ → Aₙ → B₁) →
+--                       ⋮
+--                (A₁ → ⋯ → Aₙ → B₁) →
+--                (A₁ → ⋯ → Aₙ → R)
+
+liftₙ : ∀ k n {ls rs} {as : Sets n ls} {bs : Sets k rs} →
+        Arrows k bs R → Arrows k (smap _ (Arrows n as) k bs) (Arrows n as R)
+liftₙ k n op = curry⊤ₙ k λ fs →
+               curry⊤ₙ n λ vs →
+               uncurry⊤ₙ k op $
+               palg _ _ k (λ f → uncurry⊤ₙ n f vs) fs where
+
+  -- The bulk of the work happens in this auxiliary definition:
+  palg : ∀ f (F : ∀ {l} → Set l → Set (f l)) n {ls} {as : Sets n ls} →
+         (∀ {l} {r : Set l} → F r → r) → Product⊤ n (smap f F n as) → Product⊤ n as
+  palg f F zero    alg ps       = _
+  palg f F (suc n) alg (p , ps) = alg p , palg f F n alg ps
+
+
+-- implication
+
+infixr 6 _⇒_
+_⇒_ : ∀ {n} {ls r s} {as : Sets n ls} →
+      as ⇉ Set r → as ⇉ Set s → as ⇉ Set (r ⊔ s)
+_⇒_ = liftₙ 2 _ (λ A B → A → B)
+
+-- conjunction
+
+infixr 7 _∩_
+_∩_ : ∀ {n} {ls r s} {as : Sets n ls} →
+      as ⇉ Set r → as ⇉ Set s → as ⇉ Set (r ⊔ s)
+_∩_ = liftₙ 2 _ _×_
+
+-- disjunction
+
+infixr 8 _∪_
+_∪_ : ∀ {n} {ls r s} {as : Sets n ls} →
+      as ⇉ Set r → as ⇉ Set s → as ⇉ Set (r ⊔ s)
+_∪_ = liftₙ 2 _ _⊎_
+
+-- negation
+
+∁ : ∀ {n ls r} {as : Sets n ls} → as ⇉ Set r → as ⇉ Set r
+∁ = liftₙ 1 _ ¬_
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 0a535ac5be..5a363d1ec0 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -8,18 +8,12 @@
 
 module Relation.Nullary.Decidable where
 
-open import Data.Bool.Base using (Bool; false; true; not; T)
-open import Data.Empty
-open import Data.Product hiding (map)
-open import Data.Unit
+open import Level using (Level)
 open import Function
-open import Function.Equality using (_⟨$⟩_; module Π)
-open import Function.Equivalence
-  using (_⇔_; equivalence; module Equivalence)
-open import Function.Injection using (Injection; module Injection)
-open import Level using (Level; Lift)
-open import Relation.Binary using (Setoid; module Setoid; Decidable)
-open import Relation.Binary.PropositionalEquality
+open import Function.Equality    using (_⟨$⟩_; module Π)
+open import Function.Equivalence using (_⇔_; equivalence; module Equivalence)
+open import Function.Injection   using (Injection; module Injection)
+open import Relation.Binary      using (Setoid; module Setoid; Decidable)
 open import Relation.Nullary
 
 private
@@ -29,40 +23,9 @@ private
     Q : Set q
 
 ------------------------------------------------------------------------
--- Conversion to and from Bool
+-- Re-exporting the core definitions
 
-⌊_⌋ : Dec P → Bool
-⌊ yes _ ⌋ = true
-⌊ no  _ ⌋ = false
-
-------------------------------------------------------------------------
--- Types for whether a type is occupied or not
-
-True : Dec P → Set
-True Q = T ⌊ Q ⌋
-
-False : Dec P → Set
-False Q = T (not ⌊ Q ⌋)
-
--- Gives a witness to the "truth".
-
-toWitness : ∀ {Q : Dec P} → True Q → P
-toWitness {Q = yes p} _  = p
-
--- Establishes a "truth", given a witness.
-
-fromWitness : ∀ {Q : Dec P} → P → True Q
-fromWitness {Q = yes p} = const _
-fromWitness {Q = no ¬p} = ¬p
-
--- Variants for False.
-
-toWitnessFalse : ∀ {Q : Dec P} → False Q → ¬ P
-toWitnessFalse {Q = no  ¬p} _  = ¬p
-
-fromWitnessFalse : ∀ {Q : Dec P} → ¬ P → False Q
-fromWitnessFalse {Q = yes p} = flip _$_ p
-fromWitnessFalse {Q = no ¬p} = const _
+open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
 -- Maps
@@ -88,30 +51,3 @@ module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} whe
   via-injection inj dec x y with dec (to inj ⟨$⟩ x) (to inj ⟨$⟩ y)
   ... | yes injx≈injy = yes (Injection.injective inj injx≈injy)
   ... | no  injx≉injy = no (λ x≈y → injx≉injy (Π.cong (to inj) x≈y))
-
-------------------------------------------------------------------------
--- Extracting proofs
-
-module _ {p} {P : Set p} where
-
--- If a decision procedure returns "yes", then we can extract the
--- proof using from-yes.
-
-  From-yes : Dec P → Set p
-  From-yes (yes _) = P
-  From-yes (no  _) = Lift p ⊤
-
-  from-yes : (p : Dec P) → From-yes p
-  from-yes (yes p) = p
-  from-yes (no  _) = _
-
--- If a decision procedure returns "no", then we can extract the proof
--- using from-no.
-
-  From-no : Dec P → Set p
-  From-no (no  _) = ¬ P
-  From-no (yes _) = Lift p ⊤
-
-  from-no : (p : Dec P) → From-no p
-  from-no (no ¬p) = ¬p
-  from-no (yes _) = _
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
new file mode 100644
index 0000000000..b940d1176f
--- /dev/null
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -0,0 +1,81 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Operations on and properties of decidable relations
+--
+-- This file contains some core definitions which are re-exported by
+-- Relation.Nullary.Decidable
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Nullary.Decidable.Core where
+
+open import Level using (Level; Lift)
+open import Data.Bool.Base using (Bool; false; true; not; T)
+open import Data.Unit.Base using (⊤)
+open import Function
+
+open import Relation.Nullary
+
+private
+  variable
+    p q : Level
+    P : Set p
+    Q : Set q
+
+⌊_⌋ : Dec P → Bool
+⌊ yes _ ⌋ = true
+⌊ no  _ ⌋ = false
+
+True : Dec P → Set
+True Q = T ⌊ Q ⌋
+
+False : Dec P → Set
+False Q = T (not ⌊ Q ⌋)
+
+-- Gives a witness to the "truth".
+
+toWitness : {Q : Dec P} → True Q → P
+toWitness {Q = yes p} _  = p
+toWitness {Q = no  _} ()
+
+-- Establishes a "truth", given a witness.
+
+fromWitness : {Q : Dec P} → P → True Q
+fromWitness {Q = yes p} = const _
+fromWitness {Q = no ¬p} = ¬p
+
+-- Variants for False.
+
+toWitnessFalse : {Q : Dec P} → False Q → ¬ P
+toWitnessFalse {Q = yes _}  ()
+toWitnessFalse {Q = no  ¬p} _  = ¬p
+
+fromWitnessFalse : {Q : Dec P} → ¬ P → False Q
+fromWitnessFalse {Q = yes p} = flip _$_ p
+fromWitnessFalse {Q = no ¬p} = const _
+
+-- If a decision procedure returns "yes", then we can extract the
+-- proof using from-yes.
+
+module _ {p} {P : Set p} where
+
+  From-yes : Dec P → Set p
+  From-yes (yes _) = P
+  From-yes (no  _) = Lift p ⊤
+
+  from-yes : (p : Dec P) → From-yes p
+  from-yes (yes p) = p
+  from-yes (no  _) = _
+
+-- If a decision procedure returns "no", then we can extract the proof
+-- using from-no.
+
+  From-no : Dec P → Set p
+  From-no (no  _) = ¬ P
+  From-no (yes _) = Lift p ⊤
+
+  from-no : (p : Dec P) → From-no p
+  from-no (no ¬p) = ¬p
+  from-no (yes _) = _