Notation: mathematics, programming languages

meaning	mathematics	Haskell	Coq
	C	flip
	K	const
identity	I	id ($)
fixpoint combinator	Y	fix	fix
composition of functions	∘ B (combinator)	.
λ-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
constructing a list from elements	⟨x, y, z⟩	[x, y, z]
empty list		[]	nil
constructing 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
monad		Monad
neutral element of a monad	η	return
binary operation of a monad	μ	join
double arrow	⇒	=>	=>