    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- A module used for creating function pipelines, see
    -- README.Function.Reasoning for examples
    ------------------------------------------------------------------------

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

    module Function.Reasoning where

    open import Function.Base using (_∋_)

    -- Need to give _∋_ a new name as syntax cannot contain underscores
    infixl 0 ∋-syntax
    ∋-syntax = _∋_

    -- Create ∶ syntax
    syntax ∋-syntax A a = a ∶ A

    -- Export pipeline functions
    open import Function.Base public using (_|>_; _|>′_)