search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
378 stars 22 forks source link

Operator \fin never defined #114

Closed pierrecagne closed 3 years ago

pierrecagne commented 3 years ago

The first occurrence of the \fin operator is in chapter 4:

Recall the finite set $\bn{2}:\fin_2$ from \cref{def:finiteset}, containing two elements.

It seems it is not defined before.

\fin_n is used as a alias for \FinSet_n in section 4, but seems to denote the pointed type (\FinSet_n,\bn n) in section 5.