# 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$