    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Simple combinators working solely on and with functions
    ------------------------------------------------------------------------

    -- The contents of this module is also accessible via the `Function`
    -- module. See `Function.Strict` for strict versions of these
    -- combinators.

    {-# OPTIONS --cubical-compatible --safe #-}

    module Function.Base where

    open import Level using (Level)

    private
      variable
        a b c d e : Level
        A : Set a
        B : Set b
        C : Set c
        D : Set d
        E : Set e

    ------------------------------------------------------------------------
    -- Some simple functions

    id : A → A
    id x = x

    const : A → B → A
    const x = λ _ → x

    constᵣ : A → B → B
    constᵣ _ = id

    ------------------------------------------------------------------------
    -- Operations on dependent functions

    -- These are functions whose output has a type that depends on the
    -- value of the input to the function.

    infixr 9 _∘_ _∘₂_
    infixl 8 _ˢ_
    infixl 0 _|>_
    infix  0 case_returning_of_ case_return_of_
    infixr -1 _$_

    -- Composition

    _∘_ : ∀ {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
          (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
          ((x : A) → C (g x))
    f ∘ g = λ x → f (g x)
    {-# INLINE _∘_ #-}

    _∘₂_ : ∀ {A₁ : Set a} {A₂ : A₁ → Set d}
             {B : (x : A₁) → A₂ x → Set b}
             {C : {x : A₁} → {y : A₂ x} → B x y → Set c} →
           ({x : A₁} → {y : A₂ x} → (z : B x y) → C z) →
           (g : (x : A₁) → (y : A₂ x) → B x y) →
           ((x : A₁) → (y : A₂ x) → C (g x y))
    f ∘₂ g = λ x y → f (g x y)

    -- Flipping order of arguments

    flip : ∀ {A : Set a} {B : Set b} {C : A → B → Set c} →
           ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
    flip f = λ y x → f x y
    {-# INLINE flip #-}

    -- Application - note that _$_ is right associative, as in Haskell.
    -- If you want a left associative infix application operator, use
    -- RawFunctor._<$>_ from Effect.Functor.

    _$_ : ∀ {A : Set a} {B : A → Set b} →
          ((x : A) → B x) → ((x : A) → B x)
    f $ x = f x
    {-# INLINE _$_ #-}

    -- Flipped application (aka pipe-forward)

    _|>_ : ∀ {A : Set a} {B : A → Set b} →
           (a : A) → (∀ a → B a) → B a
    _|>_ = flip _$_
    {-# INLINE _|>_ #-}

    -- The S combinator - written infix as in Conor McBride's paper
    -- "Outrageous but Meaningful Coincidences: Dependent type-safe syntax
    -- and evaluation".

    _ˢ_ : ∀ {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c} →
          ((x : A) (y : B x) → C x y) →
          (g : (x : A) → B x) →
          ((x : A) → C x (g x))
    f ˢ g = λ x → f x (g x)
    {-# INLINE _ˢ_ #-}

    -- Converting between implicit and explicit function spaces.

    _$- : ∀ {A : Set a} {B : A → Set b} → ((x : A) → B x) → ({x : A} → B x)
    f $- = f _
    {-# INLINE _$- #-}

    λ- : ∀ {A : Set a} {B : A → Set b} → ({x : A} → B x) → ((x : A) → B x)
    λ- f = λ x → f
    {-# INLINE λ- #-}

    -- Case expressions (to be used with pattern-matching lambdas, see
    -- README.Case).

    case_returning_of_ : ∀ {A : Set a} (x : A) (B : A → Set b) →
                      ((x : A) → B x) → B x
    case x returning B of f = f x
    {-# INLINE case_returning_of_ #-}

    ------------------------------------------------------------------------
    -- Non-dependent versions of dependent operations

    -- Any of the above operations for dependent functions will also work
    -- for non-dependent functions but sometimes Agda has difficulty
    -- inferring the non-dependency. Primed (′ = \prime) versions of the
    -- operations are therefore provided below that sometimes have better
    -- inference properties.

    infixr 9 _∘′_ _∘₂′_
    infixl 0 _|>′_
    infix  0 case_of_
    infixr -1 _$′_

    -- Composition

    _∘′_ : (B → C) → (A → B) → (A → C)
    f ∘′ g = _∘_ f g

    _∘₂′_ : (C → D) → (A → B → C) → (A → B → D)
    f ∘₂′ g = _∘₂_ f g

    -- Flipping order of arguments

    flip′ : (A → B → C) → (B → A → C)
    flip′ = flip

    -- Application

    _$′_ : (A → B) → (A → B)
    _$′_ = _$_

    -- Flipped application (aka pipe-forward)

    _|>′_ : A → (A → B) → B
    _|>′_ = _|>_

    -- Case expressions (to be used with pattern-matching lambdas, see
    -- README.Case).

    case_of_ : A → (A → B) → B
    case x of f = case x returning _ of f
    {-# INLINE case_of_ #-}

    ------------------------------------------------------------------------
    -- Operations that are only defined for non-dependent functions

    infixl 1 _⟨_⟩_
    infixl 0 _∋_

    -- Binary application

    _⟨_⟩_ : A → (A → B → C) → B → C
    x ⟨ f ⟩ y = f x y

    -- In Agda you cannot annotate every subexpression with a type
    -- signature. This function can be used instead.

    _∋_ : (A : Set a) → A → A
    A ∋ x = x

    -- Conversely it is sometimes useful to be able to extract the
    -- type of a given expression.

    typeOf : {A : Set a} → A → Set a
    typeOf {A = A} _ = A

    -- Construct an element of the given type by instance search.

    it : {A : Set a} → {{A}} → A
    it {{x}} = x

    ------------------------------------------------------------------------
    -- Composition of a binary function with other functions

    infixr 0 _-⟪_⟫-_ _-⟨_⟫-_
    infixl 0 _-⟪_⟩-_
    infixr 1 _-⟨_⟩-_ ∣_⟫-_ ∣_⟩-_
    infixl 1 _on_ _on₂_ _-⟪_∣ _-⟨_∣

    -- Two binary functions

    _-⟪_⟫-_ : (A → B → C) → (C → D → E) → (A → B → D) → (A → B → E)
    f -⟪ _*_ ⟫- g = λ x y → f x y * g x y

    -- A single binary function on the left

    _-⟪_∣ : (A → B → C) → (C → B → D) → (A → B → D)
    f -⟪ _*_ ∣ = f -⟪ _*_ ⟫- constᵣ

    -- A single binary function on the right

    ∣_⟫-_ : (A → C → D) → (A → B → C) → (A → B → D)
    ∣ _*_ ⟫- g = const -⟪ _*_ ⟫- g

    -- A single unary function on the left

    _-⟨_∣ : (A → C) → (C → B → D) → (A → B → D)
    f -⟨ _*_ ∣ = f ∘₂ const -⟪ _*_ ∣

    -- A single unary function on the right

    ∣_⟩-_ : (A → C → D) → (B → C) → (A → B → D)
    ∣ _*_ ⟩- g = ∣ _*_ ⟫- g ∘₂ constᵣ

    -- A binary function and a unary function

    _-⟪_⟩-_ : (A → B → C) → (C → D → E) → (B → D) → (A → B → E)
    f -⟪ _*_ ⟩- g = f -⟪ _*_ ⟫- ∣ constᵣ ⟩- g

    -- A unary function and a binary function

    _-⟨_⟫-_ : (A → C) → (C → D → E) → (A → B → D) → (A → B → E)
    f -⟨ _*_ ⟫- g = f -⟨ const ∣ -⟪ _*_ ⟫- g

    -- Two unary functions

    _-⟨_⟩-_ : (A → C) → (C → D → E) → (B → D) → (A → B → E)
    f -⟨ _*_ ⟩- g = f -⟨ const ∣ -⟪ _*_ ⟫- ∣ constᵣ ⟩- g

    -- A single binary function on both sides

    _on₂_ : (C → C → D) → (A → B → C) → (A → B → D)
    _*_ on₂ f = f -⟪ _*_ ⟫- f

    -- A single unary function on both sides

    _on_ : (B → B → C) → (A → B) → (A → A → C)
    _*_ on f = f -⟨ _*_ ⟩- f

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 1.4

    _-[_]-_ = _-⟪_⟫-_
    {-# WARNING_ON_USAGE _-[_]-_
    "Warning: Function._-[_]-_ was deprecated in v1.4.
    Please use _-⟪_⟫-_ instead."
    #-}

    -- Version 2.0

    case_return_of_ = case_returning_of_
    {-# WARNING_ON_USAGE case_return_of_
    "case_return_of_ was deprecated in v2.0.
    Please use case_returning_of_ instead."
    #-}