11. Glossary

11.1. Acronyms

ATP
automated theorem prover
ITP
interactive theorem prover (aka proof assistant); some popular examples are: Agda, Coq, Lean, and NuPrl.
ATP (v)
automated theorem proving
ITP (v)
interactive theorem proving
CiC
Calculus of Inductive Constructions
TT
TT stands for intuitionistic type theory, which takes as its starting point the Curry-Howard correspondence. TT extends Curry-Howard to predicate logic by introducing dependent types. TT internalizes the interpretation of intuitionistic logic proposed by Brouwer, Heyting, and Kolmogorov—the so-called BHK interpretation. The types in TT play a similar role to sets in set theory but functions definable in TT are always computable.
ITT
intensional intuitionistic type theory.
ETT
extensional intuitionistic type theory.
ER
equality reflection
UIP
uniqueness of identity proofs
Agda
An intensional, predicative ITP supporting dependent types and based on Martin Lof type theory; url: https://wiki.portal.chalmers.se/agda/pmwiki.php
Coq
An intensional, impredicative ITP supporting dependent types and based on CiC; url: http://coq.inria.fr
NuPRL
An extensional, predicative ITP supporting dependent types and based on Martin Lof type theory; url: http://www.nuprl.org/
Lean
An extensional, impredicative ITP supporting dependent types and based on CiC; url: https://leanprover.github.io/

11.2. Nomenclature

abstract category
An abstract category is one whose objects are not sets or whose morphisms are not functions defined on sets. Our next example is somewhere in between. The objects are sets, but the morphisms are not necessarily total functions; that is, they may be defined on only a part of the source object.
algebraic lattice
a lattice generated by its compact elements.
arity
Given a signature \(σ = (F, ρ)\), each operation symbol \(f ∈ F\) is assigned a value \(ρ f\), called the arity of \(f\). (Intuitively, the arity can be thought of as the “number of arguments” that \(f\) takes as “input”.)
Boolean algebra
..todo:: fill in definition
Boolean algebra homomorphism
a lattice homomorphism that also preserves complementation (but every lattice homomorphism between Boolean lattices automatically preserves complementation, so we may characterize the morphisms of this category more simply as the lattice homomorphisms).
category of categories
has categories as objects and functors as morphisms.
category of small categories
(see Cat)
codomain
If \(f : A → B\) is a function or relation from \(A\) to \(B\), then \(B\) is called the codomain of \(f\), denoted by \(\mathrm{cod} f\).
commutative diagram
A commutative diagram is a diagram with the following property: for all objects \(C\) and \(D\), all paths from \(C\) to \(D\) yield the same morphism.
compact element
an element \(x\) of a lattice \(L\) is called compact provide for all \(Y ⊆ L\), if \(x ≤ ⋁ Y\), then there exists a finite subset \(F ⊆ Y\) such that \(x ≤ ⋁ F\).
complete lattice
a poset whose universe is closed under arbitrary meets and joins.
complete lattice homomorphism
a function \(f: X → Y\) preserving complete meets and joins.
component
If \(α : F ⇒ G\) is a natural transformation, then the component of α at \(A\) is the morphism \(α_A : FA → GA\).
concrete category
A concrete category is one whose objects are sets and whose morphisms are functions defined on these sets (possibly satisfying some other special properties).
consecutive functions
If \(f : A → B\) and \(g : B → C\), then \(\mathrm{cod} f = \mathrm{dom} g\) and we say that \(f\) and \(g\) are consecutive functions.
contravariant powerset functor
The contravariant powerset functor is a functor \(P : \mathbf{Set} → \mathbf{Set}\) such that for each \(g : B → A\) the morphism \(g^← : PA → PB\) is given by \(g^← (S) = \{b ∈ B : g(b) ∈ S\}\) for each \(S ⊆ A\).
coproduct
Given two objects \(A\) and \(B\) a coproduct (or sum) of \(A\) and \(B\) is denoted by \(A+B\) and defined to be an object with morphisms \(ι_1 : A → A + B\) and \(ι_2 : B → A + B\) such that for every object \(X\) and all morphisms \(u : A → Y\) and \(v : B → Y\) there exists a unique morphism \([u,v] : A+B → Y\) such that \([u,v] ∘ ι_1 = u\) and \([u,v] ∘ ι_2 = v\).
Curry-Howard correspondence
the correspondence between propositions and types, and proofs and programs; a proposition is identified with the type of its proofs, and a proof is a program of that type.
covariant powerset functor
The (covariant) powerset functor is a functor \(P : \mathbf{Set} → \mathbf{Set}\) such that for each \(f : A → B\) the morphism \(Pf : PA → PB\) is given by \(Pf(S) = \{f(x) : x ∈ S\}\) for each \(S \subseteq A\).
dependent type
A dependent type is actually a family of types indexed by some parameter. That is, a dependent type provides a type schema, which is a collection of types indexed by a set of values. For example, the type Fin n of finite sets of size n is a type that depends on the value n. For more details, see the section on Dependent Types in the Theorem Proving in Lean manual.
directed graph
A directed graph is a relational structure consisting of a vertex set \(V\) (whose elements are called vertices) and an edge set \(E\subseteq V^2\) (whose elements are called edges).
domain
If \(f : A → B\) is a function or relation from \(A\) to \(B\), then \(A\) is called the domain of \(f\), denoted by \(\mathrm{dom} f\).
endofunctor
A functor that maps a category to itself is called an endofunctor.
endomorphism
A morphism \(f : A → A\) (i.e., \(\mathrm{src} f = \mathrm{tar} f\)) is called an endomorphism.
epimorphism
A morphism \(f: A → B\) is called an epimorphism if for every object \(Y\) and pair \(y_1, y_2: B → Y\) of morphisms, \(y_1 ∘ f = y_2 ∘ f\) implies \(y_1 = y_2\). When \(f: A → B\) is an epimorphism we often say “\(f\) is epi” and write \(f: ↠ B\).
equivalent categories
Two categories \(\mathcal C\) and \(\mathcal D\) are called equivalent categories if there are functors \(F : \mathcal C → \mathcal D\) and \(G : \mathcal D → \mathcal C\) together with natural isomorphisms \(ε : FG ≅ \mathrm{id}_{\mathcal D}\), and \(η : \mathrm{id}_{\mathcal C} ≅ GF\). We say that \(F\) is an equivalence with an inverse equivalence \(G\) and denote the equivalence by \(F : \mathcal C ≃ \mathcal D : G\).
essentially surjective on objects
A functor \(F : C → D\) is called essentially surjective on objects if for every object \(D ∈ \mathcal D\), there is some \(A ∈ \mathcal C\) such that \(F A\) is isomorphic to \(D\).
existential image functor
the functor \(∃ f : P(A) → P(B)\) defined by \(∃ f(X) = \{f(x) : x ∈ X\},\) for \(X ∈ P(A)\).
evaluation functor
The evaluation functor is the functor \(Ev : \mathcal C × \mathbf{Set}^{\mathcal C} → \mathbf{Set}\), which takes each pair \((A, F) ∈ \mathcal C_{\mathrm{obj}} × \mathbf{Set}^{{\mathcal C}_{\mathrm{obj}}}\) of objects to the set \(Ev(A, F) = FA\), and takes each pair \((g, μ) ∈ \mathcal C_{\mathrm{obj}} × \mathbf{Set}^{\mathcal C_{\mathrm{mor}}}\) of morphisms to a function on sets, namely, \(Ev(g, μ) = μ_{A'} ∘ F g = F' g ∘ μ_A\), where \(g ∈ \mathcal C(A, A')\) and \(μ : F ⇒ F'\).
evaluation natural transformation
The evaluation natural transformation is denoted by \(eval^A : F_A → \mathrm{id}_{\mathbf{Set}}\) and defined by…
extensional
An extensional definition of a term lists everything that qualifies as something to which that term refers. (See also function extensionality.)
faithful functor

A functor \(F : \mathcal C → \mathcal D\) is called faithful if for all objects \(A\), \(B\) in \(\mathcal C_{\mathrm{obj}}\), the map \(\mathcal C(A, B) → \mathcal D(F A, F B)\) is injective.

(Note: A faithful functor need not be injective on morphisms.)

finite ordinals
The category \(\mathrm{Ord}_{\mathrm{fin}}\) of finite ordinals (also called the simplex category \(\Delta\)) has \(\underline n = \{0, 1, \dots, n-1\}\) for objects (for each \(n ∈ ℕ\)) and \(f : \underline n → \underline m\) monotone functions for morphisms.
free algebra
Let \(\mathcal V\) be a variety of algebras of a certain signature. Let \(X\) be a set. The free algebra generated by \(X\) is denoted by \(\mathbb F(X)\) and is defined as follows: for every algebra \(\mathbf A = ⟨A, \dots⟩ ∈ \mathcal V\) and every function \(f : X → A\), there exists a unique homomorphism \(h:\mathbb F(X) → \mathbf A\) such that \(\forall x ∈ X, h(x) = f(x)\). We say that \(\mathbb F (X)\) is universal for \(\mathcal V\).
free monoid

Todo

fill in definition

full embedding
a fully faithful functor that is injective on objects.
full functor

A functor \(F : \mathcal C → \mathcal D\) is called full if for all objects \(A\), \(B\) in \(\mathcal C\), the map \(\mathcal C(A, B) → \mathcal D(F A, F B)\) is surjective.

(N.B. A full functor need not be surjective on morphisms.)

full subcategory
If there exists a full embedding \(F : \mathcal C → \mathcal D\), then \(\mathcal C\) is called a full subcategory of \(\mathcal D\).
fully faithful functor
a functor that is both full and faithfull.
function extensionality
the principle that takes two functions \(f : X → Y\) and \(g : X → Y\) to be equal just in case \(f(x) = g(x)\) holds for all \(x : X\).
functor
A functor \(F : \mathcal C → \mathcal D\) consists of a function \(F_0\) that maps objects of \(\mathcal C\) to objects of \(\mathcal D\) and a function \(F_1\) that maps morphisms of \(\mathcal C\) to morphisms of \(\mathcal D\) such that \(F\) preserves (co)domains of morphisms, identities, and compositions.
functor category
The functor category from \(\mathcal C\) to \(\mathcal D\) has functors \(F : \mathcal C → \mathcal D\) as objects and natural transformations \(α : F ⇒ G\) as morphisms.
generalized element
A morphism \(h: X → A\) is sometimes called a generalized element of \(A\). A morphism \(f\) is mono when it is injective on the generalized elements of its domain.
global element
see point
graph morphism
Let \(𝐆_1 =(V_1, E_1)\) and \(𝐆_2 = (V_2, E_2)\) be graphs. We say that a pair of functions \(f=(f_v,f_e)\) is a graph morphism from \(𝐆_1\) to \(𝐆_2\) provided \(f_v : V_1 → V_2\), \(f_e : E_1 → E_2\), and for any edge \(e = (v_1,v_2) ∈ E_1\) we have that we have \(f_e(e) = (f_v(v_1), f_v(v_2))\).
group
A group \(𝐆 = (G, e, \ ^{-1}, ⋆)\) consists of a set \(G\) together with a nullary (constant) operation \(e\), a unary (inverse) operation \(\ ^{-1}: G → G\), and a binary operation \(⋆ : G^2 → G\), such that \((G, e, ⋆)\) is a monoid and \(x ⋆ x^{-1} = e\) for all \(x ∈ G\).
Heyting algebra
A Heyting algebra \(⟨L, ∧, ∨, ⊥, ⊤, →⟩\) is a bounded lattice with least and greatest elements ⊥ and ⊤, and a binary “implication” → that satisfies \(∀ a, b, c ∈ L, \ (c ∧ a ≤ b \ ⟺ \ c ≤ a → b)\). Logically, this says a → b is the weakest proposition for which the modus ponens rule, \(\{a → b, a\} ⊢ b\), is sound. The class of Heyting algebras forms a variety that is finitely axiomatizable.
Heyting algebra homomorphism
a lattice homomorphism that also preserves Heyting implications; that is, if \(x, x' ∈ X\), then \(f(x → x') = f(x) → f(x')\).
hom set
Some authors require that \(\mathcal C(A,B)\) always be a set and call \(\mathcal C(A,B)\) the hom set from \(A\) to \(B\).
impredicative
A self-referencing definition is called impredicative. A definition is said to be impredicative if it invokes (mentions or quantifies over) the set being defined, or (more commonly) another set which contains the thing being defined.
initial object
An object \(\mathbf{0}\) in a category is called an initial (or a free) object if for every object \(A\) in the same category there exists a unique morphism \(!_A:\mathbf{0}\to A\).
intensional
An intensional definition of a term specifies necessary and sufficient conditions that the term satisfies. In the case of nouns, this is equivalent to specifying all the properties that an object must have in order to be something to which the term refers.
isomorphism
A morphism \(f: A → B\) is called an isomorphism if there exists a morphism \(g: A → B\) such that \(g ∘ f= \mathrm{id}_A\) and \(f ∘ g = \mathrm{id}_B\). We write \(f^{-1}\) to denote \(g\) when it exists.
Kleene closure
(see free monoid)
lattice
a poset whose universe is closed under all finite meets and joins is called a lattice.
lattice homomorphism
a function \(f: X → Y\) preserving finite meets and joins.
locally small category
A category \(\mathcal C\) is locally small if for every pair \(A\), \(B\) of objects in \(\mathcal C\) the collection of morphisms from \(A\) to \(B\) is a set.
metaprogram
a program whose purpose is to modify the behavior of other programs; proof tactics form an important class of metaprograms.
monoid
A monoid \(𝐌 = (M, e, ⋆)\) consists of a set \(M\) with a a unit element \(e ∈ M\) and a binary operation \(⋆ : M^2 → M\) such that for all \(x,y,z ∈ M\), \(x ⋆ e = x = e ⋆ x\) and \((x ⋆ y) ⋆ z = x ⋆ (y ⋆ z)\).
monoid homomorphism
Given monoids \(𝐌_1 = (M_1, e_1, ⋆)\) and \(𝐌_2 = (M_2, e_2, ∗)\) we say that a function \(f : M_1 → M_2\) is a monoid homomorphism from \(𝐌_1\) to \(𝐌_2\) provided \(f\) preserves the nullary (identity) and binary operations; that is, \(f(e_1) = e_2\) and \(f (x ⋆ y) = f(x) ∗ f(y)\) for all \(x, y ∈ M_1\).
monomorphism
A morphism \(f: A → B\) is called a monomorphism if for every object \(X\) and every pair \(h, h' : X → A\) of morphisms, \(f ∘ h = f ∘ h'\) implies \(h = h'\). When \(f\) is a monomorphism we often say \(f\) is “mono” and write \(f: A ↣ B\).
monotone function
Given posets \(⟨A, ≤ᴬ⟩\) and \((B, ≤ᴮ)\) we say that a function \(f: A → B\) is monotone from \(⟨A, ≤ᴬ⟩\) to \(⟨B, ≤ᴮ ⟩\) when for any \(x, y ∈ A\) we have that \(x ≤ᴬ y\) implies that \(f(x) ≤ᴮ f(y)\).
natural isomorphism
An isomorphism in a functor category is referred to as a natural isomorphism.
natural transformation
Given functors \(F, G : \mathcal C → \mathcal D\), a natural transformation \(α : F ⇒ G\) is a family \(\{α_A : A ∈ \mathcal C_{\mathrm{obj}}\}\) of morphisms in \(\mathcal D\) indexed by the objects of \(\mathcal C\) such that, for each \(A ∈ \mathcal C_{\mathrm{obj}}\), the map \(\alpha_A\) is a morphism from \(FA\) to \(GA\) satisfying the naturality condition, \(Gf ∘ α_A = α_B ∘ Ff\), for each \(f : A → B\) in \(\mathcal C_{\mathrm{mor}}\). We shall write \(α : F ⇒ G : \mathcal C → \mathcal D\) to indicate that α is a natural transformation from \(F\) to \(G\), where \(F, G : \mathcal C → \mathcal D\).
naturally isomorphic
If there is a natural isomorphism between the functors \(F\) and \(G\), then we call \(F\) and \(G\) naturally isomorphic.
opposite category
Given a category \(\mathcal C\) the opposite (or dual) category \(\mathcal C^{\mathrm{op}}\) has the same objects as \(\mathcal C\) and whenever \(f: A → B\) is a morphism in \(\mathcal C\) we define \(f : B → A\) to be a morphism in \(\mathcal C^{\mathrm{op}}\).
parallel morphisms
Morphisms \(f,g : A → B\) are called parallel morphisms just in case \(\mathrm{src} f = \mathrm{src} g\) and \(\mathrm{tar} f = \mathrm{tar} g\).
partial function
A partial function from \(A\) to \(B\) is a total function on some (potentially proper) subset \(\operatorname{dom}_f\) of \(A\).
point
Given a category with an initial object \(\mathbf{1}\) and another object \(A\), the morphisms with domain \(\mathbf{1}\) and codomain \(A\) are called the points or global elements of \(A\).
polymorphic function
a function that operates in the “same way” independently of the object parameter.
poset
A poset \((A, ≤)\) consists of a set \(A\) and a binary relation \(≤ \ ⊆ A^2\) such that for all \(x, y, z ∈ A\) we have \(x ≤ x\);:math:x ≤ y and \(y ≤ x\) imply \(x = y\); and \(x ≤ y\) and \(y ≤ z\) imply \(x ≤ z\).
predicative
The opposite of impredicative, predicative refers to building stratified (or ramified) theories where quantification over lower levels results in variables of some new type, distinguished from the lower types that the variable ranges over.
product
Given two objects \(A\) and \(B\) a product of \(A\) and \(B\) is denoted \(A × B\) and is defined to be an object with morphisms \(p_1 : A \times B → A\) and \(p_2 : A \times B → B\) such that for every object \(X\) and all morphisms \(x_1 : X → A\) and \(x_2 : X → B\) there exists a unique morphism \(h : X → A \times B\) such that \(p_1 \circ h = x_1\) and \(p_2 \circ h = x_2\). We usually use \(π_1 : A \times B → A\) and \(π_2 : A \times B → B\) to denote the projections and \(⟨x_1, x_2⟩\) for the unique map \(h : X → A \times B\).
proof tactic
an automated procedure for constructing and manipulating proof terms.
relation
Given sets \(A\) and \(B\), a relation from \(A\) to \(B\) is a subset of \(A × B\).
relational product
Given relations \(R : A → B\) and \(S : B → C\) we denote and define the relational product (or composition) of \(S\) and \(R\) to be \(S ∘ R = \{(a,c) : (∃ b ∈ B) a \mathrel{R} b ∧ b \mathrel{S} c \}\).
relational structure
A relational structure \(𝐀 = ⟨A, ℛ⟩\) is a set \(A\) together with a collection \(ℛ\) of relations on \(A\).
self-dual
A category \(\mathcal C\) is called self-dual if \(\mathcal C^{\mathrm{op}} = \mathcal C\).
signature
a pair \(σ = (F, ρ)\) consisting of a collection \(F\) of operation symbols and an arity function \(ρ : F → β\) that maps each operation symbol to its arity; here, \(β\) denotes the arity type.
simplex category
(see finite ordinals)
small category
A category is called small if both its objects and morphisms form sets.
source vertex
Given a directed graph \(\mathbf G = (V,E)\) and an edge \(e=(v_1,v_2) ∈ E\), we refer to \(v_1\) as the source vertex of \(e\).
target vertex
Given a directed graph \(\mathbf G = (V,E)\) and an edge \(e=(v_1,v_2)\in E\), we refer to \(v_2\) as the target vertex of \(e\).
terminal object
An object \(\mathbf{1}\) is called a terminal (or bound) object if for every object \(A\) in the same category there exists a unique morphism \(⟨\ ⟩_A: A → \mathbf{1}\).
total function
Given sets \(A\) and \(B\), a total function \(f\) from \(A\) to \(B\) is what we typically mean by a “function” from \(A\) to \(B\).
underlying set functor
The underlying set functor of \(𝐌\) is denoted by \(U(𝐌)\), or by \(|𝐌|\); it returns the universe of the structure \(𝐌\), and for each morphism \(f\), \(Uf\) (or \(|f|\)) is \(f\) viewed simply as a function on sets.
universal image functor
the functor \(∀ f : P(A) → P(B)\) defined by \(∀ f (X) = \{y ∈ B : f^{-1}(\{y\}) \subseteq X\}\), for \(X ∈ P(A)\).
universal mapping property
Let \(η_A : A → |𝐀^*|\) be the function that maps \(a ∈ A\) to the “one-letter word” \(a ∈ A^*\). The functors \(K (= \ ^∗)\) and \(U (= |\ |)\) are related by the universal mapping property of monoids, which says that for every monoid \(𝐌\) and every function \(f : A → U 𝐌\) there exists a unique morphism \(f̂ : KA → 𝐌\) such that \(f = f̂ ∘ η\).
universal property
The unique morphism property of initial object is what we refer to as a universal property, and we say that the free object in a category \(\mathcal C\) is universal for all other objects in \(\mathcal C\).

11.3. Categories

1
The only object is \(0\); the only morphism is the identity \(\operatorname{id}_0: 0 ↦ 0\).
2
There are two objects, \(0\) and \(1\); there is one nonidentity morphism \(f: 0 ↦ 1\).
3
There are three objects, \(0\), \(1\), and \(2\); there are three nonidentity morphisms: \(f: 0 ↦ 1\), \(g: 1 ↦ 2\), and \(h: 0 ↦ 2\).
Cat
the (large) category of small categories; it has small categories as objects and functors \(F : \mathcal C → \mathcal D\) as morphisms.
Set
the category whose objects are the sets and whose morphisms are the functions on sets.
Grph
the category whose objects are the (directed) graphs; the morphisms are the \(graph morphisms <graph morphism>\).
Mon
the category whose objects are the monoids and whose morphisms are the monoid homomorphisms.
Par
the category whose objects are sets and whose morphisms are the partial functions.
Rel
the category whose objects are sets and whose morphisms are the relations on sets.
Fin
a category whose objects are the finite sets; the morphisms are the functions on finite sets.
Pos
a category whose objects are the posets; the morphisms are the monotone functions.
Lat
a category whose objects are the lattices; the morphisms are the lattice homomorphisms.
CLat
a category whose objects are the complete lattices; the morphisms are the complete lattice homomorphisms.
BLat
a category whose objects are the Boolean lattices; the morphisms are the Boolean lattice homomorphisms.
HLat
a category whose objects are the Heyting lattices; the morphisms are the Heyting lattice homomorphisms
ACLat
a category whose objects are algebraic, complete lattices; the morphisms are the complete lattice homomorphisms.
Arrow
Given a category \(\mathcal C\), the arrow category \(\mathcal C^→\) has as objects the triples \((A, B, f)\) satisfying \(A, B ∈ \mathcal C_{\mathrm{obj}}\) and \(f ∈ \mathcal C(A,B)\), and as morphisms the pairs \((h_1, h_2) : (A, B, f) → (C, D, g)\) such that \(h_1 ∈ \mathcal C(A,C)\), \(h_2 ∈ \mathcal C(B, D)\) and \(g \circ h_1 = h_2 \circ f\).
Slice
Given a category \(\mathcal C\) and an object \(C ∈ \mathcal C_{\mathrm{obj}} \)mathcal C/C` has objects the pairs \((A, f)\) such that \(f ∈ \mathcal C(A, C)\), and morphisms \(h : (A, f) → (B, g)\) such that \(h ∈ \mathcal C(A, B)\) and \(g ∘ h = f\).
Comma
Given categories \(\mathcal C\) and \(\mathcal D\) and functors \(F : \mathcal C → \mathcal D\) and \(G : \mathcal C' → \mathcal D\) (with a common codomain), the comma category is denoted by \((F ↓ G)\) and has objects the triples \((A, f, A')\), where \(A ∈ \mathcal C_{\mathrm{obj}}\), \(A' ∈ \mathcal C'_{\mathrm{obj}}\), and \(f ∈ \mathcal D(FA, GA')\), and morphisms the pairs \((φ, ψ) : (A, f, A') → (B, g, B')\), where \(φ ∈ \mathcal C(A, B)\), \(ψ ∈ \mathcal C'(A',B')\) and \(G ψ ∘ f = g ∘ F φ\).