# Pastebin pUFcfKGd
-- * The BHKCH intepretation of universal quantification:
--
--     A realizer of "for all x in X, A x" is a function that
--     transforms any x in X into a realizer of A x.
--
--     The interpretation of universal quantification is given by
--     dependent products, again built-in in Martin-Löf theory and in
--     Agda.
--
--     In Martin-Löf type theory, it is written Π.  In Agda, the
--     notation (x : X) → A x is used, where A : X → Set.
--
--     It is the type of functions that map any x : X to an element y : A x.
--     Notice that the type of the output depends on the input.
--
--     Agda allows you to write ∀(x : X) → A x to mean (x : X) → A x.
--     When types can be inferred by Agda, you can also write ∀ x → A x.