Definition 1.4.6 (Endorelations).  Let S be a set. We define:
Rel(S) :=: {[ps,t]s,t ∈ S | ps,t is a proposition for each s, t ∈ S}
[ps,t]s,t ∈ S = [qs,t]s,t ∈ S  :⇔  ∀ s, t ∈ S : [ps,t  ⇔  qs,t]  (ps,t is a proposition for each s, t ∈ S, qs,t is a proposition for each s, t ∈ S)
Rel(S, S) =: Rel(S) via≺ = [s ≺ t]s,t ∈ S
Well-definedness.  No proof.
We write “let ≺ be a relation on S” for “let ≺ ∈ Rel(S).”
Remarks.

Since endorelations are used often, we encode them as a separate construction with an appropriate embedding, mainly to improve rendering.

References.