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

isnType #147

Open DanGrayson opened 2 years ago

DanGrayson commented 2 years ago

In this text:

Screen Shot 2022-08-18 at 10 28 48 AM

the predicate isnType is undefined. Also, it would look better if the n occurred as a subscript, instead of inline.