Agda-2.3.2.2: benchmark/Syntacticosmos/Basics.agda

module Basics where

id : {A : Set} -> A -> A
id a = a

_o_ : {A : Set}{B : A -> Set}{C : (a : A)(b : B a) -> Set} ->
      ({a : A}(b : B a) -> C a b) -> (g : (a : A) -> B a) ->
      (a : A) -> C a (g a)
_o_ f g a = f (g a)