Klaus Andrey

feature request: custom method to display error message

4

Hello I like ko and ko.validation plugin. Good work, guys. Thank you. I'm trying to use ko and validation in my project now. Problem which I faced is next: I...

comment search in snippets because it is too slow for jscoq and leave warning

2

comment search in snippets because it is too slow for jscoq and leave warning in example in ch2.v/ch2.html. Search (odd _). Search eq odd -coprime. should be kind of (*...

`Eval compute in tnth [tuple 1; 2; 3] (sub_ord 1).` I think this example (provided by Emilio Jesús Gallego Arias) might be added to the first part of book where...

I think a (sub)chapter about differences between coercions and canonical structures might be added somewhere after Chapter 6.3. I think content may be built on 1-2 examples of coercions from...

Error: Command failed: /bin/sh: 1: Google: not found after gulp serve

2

Hello I receive error `Error: Command failed: /bin/sh: 1: Google: not found` after entering `gulp serve` in console. I'm not sure how imporant it is. steps to reproduce the issue...

typo in commit

1

I think there is a typo in the commit https://github.com/HoTT/book/commit/7606d8151ac50dcba28fad80aef4edf042218c31 this is removed from the line 1421 ``` For example, with univalence, we will be able to show $(\bool, \bfalse)...