Niels van der Weide
Niels van der Weide
Very nice!
List of packages: - [ ] Algebra - [ ] Algebraic Geometry (https://github.com/UniMath/UniMath/pull/1584) - [x] Bicategories - [ ] Category Theory - [ ] Combinatorics - [ ] Folds (https://github.com/UniMath/UniMath/pull/1584)...
It would be good to first identify all the packages on which no other package depends and do those first. Another thing: it might also be good to create a...
Both GrpdHITs and SetHITs should be compatible now with the structured proof format.
I think the next ones to rework would be: - Induction - SyntheticHomotopyTheory - Tactics And the subrepositories: - Type Theory - Large Cat Modules Category Theory must be done...
The reason to add this check, is because the corresponding guideline in the style guide can be checked purely mechanically, while it will never be checked by any code reviewer....
Note that there also are some other ways we can implement this change. Currently, all files that **directly** import https://github.com/UniMath/UniMath/blob/master/UniMath/Tactics/EnsureStructuredProofs.v, have to obey this check. However, in the adjusted files,...
> Still another option would be that Coq would provide a command-line option to activate these checks in all files - that could be overrun by a setting in the...
> However, it seems that this causes `GrothendieckConstruction/IsPullback.v` to hang at line 373. That might have been the reason for the lemma
> > That might have been the reason for the lemma > > Do you have a hypothesis why switching from a lemma about setcategories to a lemma about categories...