The identity relation m a t h r m i d i f x . . ⋄ l s e i ⊆ A × A mathrm{id}{ifx..lse\par i}\subseteq A\times A is the relation given by the Identity Type on A 𝐴 A .