Daniel R. Grayson

```sh COQC UniMath/CategoryTheory/All.v File "./UniMath/CategoryTheory/All.v", line 177, characters 0-65: Warning: New coercion path [adjunction_of_right_adjoint_over_id_data; left_adj_over_id] : right_adjoint_over_id_data >-> disp_functor is ambiguous with existing [functor_of_right_adjoint_over_id] : right_adjoint_over_id_data >-> disp_functor. [ambiguous-paths,typechecker] File...

Move some files

1

Okay, we can discuss it later. Or maybe I'll just do it. Maybe Dcpo.v should be moved, too. By the way, "Dcpo" is a horrible name for a file. Thanks!...

It would be good to start formalizing classical algebraic geometry, starting with the Zariski topology on Spec R and its sheaf of rings. Kevin Buzzard mentioned this in a recent...

I can't figure out how to compile under Debian 10 with BUILD_COQIDE=yes any longer. The library `liblablgtk-extras-ocaml-dev`, mentioned in the install file, is no longer there. Installing the libraries `liblablgtk2-ocaml-dev...

simplify some proofs

1

see https://github.com/UniMath/UniMath/pull/1227#issuecomment-497488244 for details

better name for proof irrelevance

1

A better name for the concept here might be good: ``` Definition isProofIrrelevant (X:UU) := ∏ x y:X, x = y. Lemma proofirrelevance (X : UU) : isaprop X ->...

true

4

This overrides the element of bool named "true": https://github.com/UniMath/UniMath/blob/10839eec83e48397b5544f249662d3b5d126b5cd/UniMath/CategoryTheory/SubobjectClassifier.v#L57

Now that Circle2.v fulfills the goals of Circle.v, we may remove Circle.v

Example: ``` make UniMath/SyntheticHomotopyTheory/Circle2.vo ``` The reason is that we call the makefile that Coq built recursively, and we aren't including the dependencies, I guess, so nothing happens if the...

unused package

6

The files in the package `Tactics` are unused. Can we remove them?