Benedikt Ahrens

On 20/11/2018 11:41, Daniel R. Grayson wrote: > If we insist that alternative definitions be proved equivalent to > existing ones, that will make a lot of work for us...

Alectryion is like stepping through the file, but without the hassle of installing Coq. It seems great as a first step.

Good point - as such, it cannot go into UniMath/UniMath, but in some satellite repository. There is code on W- and M-types in https://github.com/UniMath/UniMath/tree/master/UniMath/Induction. I have not studied that material,...

Thanks a lot for the notification. I cannot promise that I can take time to look at this soon, but I'll do my best.

The construction of `section_to_nat_trafo` can more efficiently be done without destructing pairs (` induction sd as [[sdob sdmor] [sdid sdcomp]].`) Same for `section_to_nat_trafo_bicat`.

On 21/04/2019 21:49, Langston Barrett wrote: > Not to reopen our favorite old can of worms... but has anyone expressed > opposition to @DanGrayson 's proposal(s) > for naming? It...

@Cypher1 thanks a lot for filing this issue. The file linked to has been renamed, that's why it looks like it has been deleted. It is this one: https://github.com/UniMath/UniMath/blob/master/UniMath/.dir-locals.el.in @DanGrayson...

@Cypher1 : does #1542 solve this issue for you?

On 18/12/2018 02:04, Daniel R. Grayson wrote: > In light of > > |@isofhlevelff : ∏ (n : ℕ) (X Y Z : UU) (f : X → Y) (g...

Ubuntu 22.04 is now available on Github Actions: https://github.blog/changelog/2022-08-09-github-actions-ubuntu-22-04-is-now-generally-available-on-github-hosted-runners/ That might mean that we could update the Coq submodule to the most recent version, which seems to be 8.15.1. See...