{-# OPTIONS --universe-polymorphism #-}
module Function.NP where

open import Function       public
open import Data.Nat       using (ℕ; zero; suc)
open import Data.Bool      using (Bool)
open import Data.Vec.N-ary using (N-ary; N-ary-level)
import Category.Monad.Identity as Id
open import Category.Monad renaming (module RawMonad to Monad; RawMonad to Monad)
open import Category.Applicative renaming (module RawApplicative to Applicative; RawApplicative to Applicative)

id-app : ∀ {f} → Applicative {f} id
id-app = rawIApplicative
  where open Monad Id.IdentityMonad

_→⟨_⟩_ : ∀ {a b} (A : Set a) (n : ℕ) (B : Set b) → Set (N-ary-level a b n)
A →⟨ n ⟩ B = N-ary n A B

_→⟨_⟩₀_ : ∀ (A : Set) (n : ℕ) (B : Set) → Set
A →⟨ zero  ⟩₀ B = B
A →⟨ suc n ⟩₀ B = A → A →⟨ n ⟩₀ B

_→⟨_⟩₁_ : ∀ (A : Set) (n : ℕ) (B : Set₁) → Set₁
A →⟨ zero  ⟩₁ B = B
A →⟨ suc n ⟩₁ B = A → A →⟨ n ⟩₁ B

Endo : ∀ {a} → Set a → Set a
Endo A = A → A

Cmp : ∀ {a} → Set a → Set a
Cmp A = A → A → Bool

-- If you run a version of Agda without the support of instance
-- arguments, simply comment this definition, very few code rely on it.
-- … : ∀ {a} {A : Set a} ⦃ x : A ⦄ → A
-- … ⦃ x ⦄ = x