Benedikt Ahrens

On 10/19/2017 10:06 PM, Daniel R. Grayson wrote: > I'll try to do it! Does that comment not apply to PartC? > It does, but in PartD it looks somewhat...

I suggest removing the use of the `now` tactical from Foundations. There are several issues with `now`: 1. The Coq `now` is defined in terms of the `easy` tactical, which...

I suggest not using `reflexivity` in Foundations. The tactic has 11 chars, its counterpart `apply idpath` has 12. There is very little benefit to using `reflexivity`, and in exchange one...

Here are my reasons to dislike `reflexivity`: 1. The name `reflexivity` is very much inspired by the idea of the identity type as a proposition. 2. I think it is...

I suggest replacing `unshelve refine (gradth f _ _ _).` in the proof of `UniqueConstruction_to_weq` by `use (gradth f)`. That is shorter and clearer. Similar with all the other occurrences...

On 11/06/2017 07:34 PM, Daniel R. Grayson wrote: > I'll remove `mkpair`, too, since `use tpair` is a fine alternative. > Yes, I think that is a good idea!

Should we strive to put all the Ltac definitions that are used in Foundations into Preamble? There is ``` Ltac contradicts a b := solve [ induction (a b) |...

``` Ltac intermediate_logeq Y' := apply (logeq_trans (Y := Y')). ``` defined in PartA, is only used twice in PartC, and does not really shorten the proof script. Can we...

``` Ltac intermediate_iscontr Y' := apply (iscontrweqb (Y := Y')). ``` from PartA is only used once in Ktheory. It is also defined again in Ktheory/Tactics. Maybe we can remove...

We still have quite a mess in UniMath regarding `Set Automatic Introduction.` The plan was to restrict usage to `Local (Un)Set Automatic Introduction.` Could we change that before Dec 11?