    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Examples showing how the generic n-ary operations the stdlib provides
    -- can be used
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --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.Base using (_×_; _,_)
    open import Data.Sum.Base using (inj₁; inj₂)
    open import Function.Base using (id; flip; _∘′_)
    open import Relation.Nullary
    open import Relation.Binary.Definitions 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