  Hypersafety properties of arity $n$ are program properties that relate $n$
traces of a program (or, more generally, traces of $n$ programs). Classic
examples include determinism, idempotence, and associativity. A number of
relational program logics have been introduced to target this class of
properties. Their aim is to construct simpler proofs by capitalizing on
structural similarities between the $n$ related programs. We propose an
unexplored, complementary proof principle that establishes hyper-triples (i.e.
hypersafety judgments) as a unifying compositional building block for proofs,
and we use it to develop a Logic for Hyper-triple Composition (LHC), which
supports forms of proof compositionality that were not achievable in previous
logics. We prove LHC sound and apply it to a number of challenging examples.
