# Homotopy Type Theory diagonal > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

# Contents

## Definition

Given a type $S$ and the product type $S \times S$, the diagonal is the set of all pairs that are equal to each other

$\Delta(S) \coloneqq \sum_{(x,y):S \times S} x = y$