clean up

next task: add coq, Foundations, RezkCompletion as submodules
then: make a bug branch for what happens if we implement
    (* destruct F as [F1 F2]. *)
    set (F1 := F.1).
    set (F2 := F.2).
in Categories.v