relation.refl_gen: Reflexive closure. refl_gen r relates everything r related, plus for all
a it relates a with itself. So refl_gen r a b ↔ r a b ∨ a = b.
relation.trans_gen: Transitive closure. trans_gen r relates everything r related
transitively. So trans_gen r a b ↔ ∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b.
relation.refl_trans_gen: Reflexive transitive closure. refl_trans_gen r relates everything
r related transitively, plus for all a it relates a with itself. So
refl_trans_gen r a b ↔ (∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b) ∨ a = b. It is the same as
the reflexive closure of the transitive closure, or the transitive closure of the reflexive
closure. In terms of rewriting systems, this means that a can be rewritten to b in a number of
relation.comp: Relation composition. We provide notation ∘r. For r : α → β → Prop and
s : β → γ → Prop, r ∘r srelates a : α and c : γ iff there exists b : β that's related to
relation.map: Image of a relation under a pair of maps. For r : α → β → Prop, f : α → γ,
g : β → δ, map r f g is the relation γ → δ → Prop relating f a and g b for all a, b
related by r.
relation.join: Join of a relation. For r : α → α → Prop, join r a b ↔ ∃ c, r a c ∧ r b c. In
terms of rewriting systems, this means that a and b can be rewritten to the same term.
A function f : α → β is a fibration between the relation rα and rβ if for all
a : α and b : β, whenever b : β and f a are related by rβ, b is the image
of some a' : α under f, and a' and a are related by rα.
The map of a relation r through a pair of functions pushes the
relation to the codomains of the functions. The resulting relation is
defined by having pairs of terms related if they have preimages
related by r.
The join of a relation on a single type is a new relation for which
pairs of terms are related if there is a third term they are both
related to. For example, if r is a relation representing rewrites
in a term rewriting system, then confluence is the property that if
a rewrites to both b and c, then join r relates b and c