# Notation: mathematics, programming languages

composition of functions .
λ-abstraction
λxy (λ-calculus)
λx.y (λ-calculus)
\ x -> y fun x => y
not equal /= <> (Prop)
equal = == = (Prop)
lower or equal <= <=
greater or equal >= >=
is of type name : type name :: type name : type
logical negation ¬ not ~ (Prop)
material implication
->
function type constructor -> ->
categorical product a × b (a, b) a * b
conjunction && /\ (Prop)
categorical sum + Either + (Type)
disjunction || \/ (Prop)
verum True True (Prop)
falsum, absurd, contradiction False False (Prop)
empty set Empty_set
singleton set
{*}
{∙}
() unit
inhabitant of the singleton set
*
() tt
universal quantification forall forall
existential quantification forall (before data constructor)
exists
ex
sig
sigT
construction of a list from elements ⟨x, y, z⟩ [x, y, z]
empty list [] nil
construction of a list from a head and a tail x : xs x :: xs
concatenation of lists ++ app
tuple constructor ⟨x, y, z⟩ (x, y, z) (x, y, z)
natural numbers nat
covariant Hom functor Hom(a,−) Reader a
contravariant Hom functor Hom(−,a) Writer a
functor Functor
lax monoidal functor Applicative