Agda

Agda is a dependently-typed functional programming language and theorem-prover.

Records

no-eta-equality

Record η-equality is most often disabled for one of two reasons:

for efficiency — η-equality slows down the type-checker; or
to print shorter normal forms in the goal display [cite:@amelia2025eta].

Unification

In Agda, unification of two terms is the process of deducing which variable substitutions, if any, must be applied to make two terms identical.

Levels

For $Type A \Typen u$ and $Type B \Typen v$ ,

\begin{matrix} A ⊎ B & : u ⊔ v \\ A \times B & : u ⊔ v \\ A \to B & : u ⊔ v \end{matrix}

Resources

https://doisinkidney.com/posts/2018-09-20-agda-tips.html