Benedikt Ahrens

Improve CI for satellite repos

5

- put compilation of each satellite repo in a separate "step" - continue CI upon failure of a step (see https://stackoverflow.com/questions/58858429/how-to-run-a-github-actions-step-even-if-the-previous-step-fails-while-still-f)

Confusion about CI sanity checks

2

I am confused by the output of the sanity check to a (draft) PR: https://github.com/UniMath/UniMath/actions/runs/3903770065/jobs/6668606428 It says that the CI run has failed, but I don't see which of the...

PR #1604 exhibits some shortcomings of the current organization of category theory, in particular, of the way in which material is distributed between `CategoryTheory` and `Bicategories`. This issue could host...

Integrate binary installation instructions for UniMath

1

For the School on Univalent Mathematics at Cortona in July 2022, @amato-gianluca and @maggesi (I believe) wrote very good installation instructions for precompiled Coq and UniMath. These instructions are available...

The instructions at https://github.com/UniMath/Schools/blob/master/installation.md are outdated. Instead, we should point to the installation instructions located at https://github.com/UniMath/UniMath/issues/1587.

Upstreaming some of the material in `Auxiliary` to UniMath/UniMath?

1

Great work was done by @peterlefanulumsdaine in #202 regarding organization of auxiliary material in `Auxiliary`. Question: would some of the material from `Auxiliary` fit well into UniMath/UniMath? The advantages of...

File https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v contains admitted statements: - https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v#L44 - https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v#L90 - https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v#L91 Fragments or complete proofs are there, but do not type-check in a reasonable amount of time, or at all....

Put notations in scope or make them local

1

as suggested by Anders

see https://github.com/UniMath/UniMath/issues/362#issuecomment-225556634