{-# OPTIONS --without-K #-}
module function.core where

open import level

-- copied from Agda's standard library

infixr 9 _∘_ _∘'_
infixr 0 _$_

_∘_ :  {a b c}
      {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)

_∘'_ :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
       (B  C)  (A  B)  (A  C)
f ∘' g = _∘_ f g

id :  {a} {A : Set a}  A  A
id x = x

const :  {a b} {A : Set a} {B : Set b}  A  B  A
const x = λ _  x

_$_ :  {a b} {A : Set a} {B : A  Set b} 
      ((x : A)  B x)  ((x : A)  B x)
f $ x = f x

flip :  {a b c} {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