Created augmented simplex category.

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work

BSD 3-Clause "New" or "Revised" License

755 stars 70 forks source link

Created augmented simplex category. #111

Closed patrick-nicodemus closed 2 years ago

jwiegley commented 2 years ago

I imagine the backup files ending in ~ were not meant to be included?

patrick-nicodemus commented 2 years ago

Yes, thank you. I'm currently de-SSReflecting the proofs, in particular eliminating the use of tacticals ":" and "=>" where they make things overly concise/impenetrable. I am currently planning to leave in the views like "apply/eqP" and "move/leP" because the math-comp library is heavily written in boolean-reflection lemmas and so efficiently converting between boolean and "propositional" forms of a sentence seems necessary to make use of the library. When I post the updated proofs you can let me know if this seems maintainable or we should come up with another workaround.

jwiegley commented 2 years ago

Thanks you for being so considerate, @patrick-nicodemus, the use of views should be fine.

Would you mind if I offered a PR onto your PR in order to normalize certain patterns of use to fit with the rest of the library?

patrick-nicodemus commented 2 years ago

Alright, I have gone through the files and rewritten the proofs in response to your comments.

Require statements have been broken up into separate lines/sentences.
"Require Import Category.Lib" is at the head of each file.
The body of all the proofs has been substantially stylistically changed to look closer to "vanilla" Coq than SSReflect. Please let me know if there's anyting else I can do here, if there's anything that looks unclear and needs to be commented let me know.

You can open the PR if that's the easiest way to make the changes you're suggesting.

patrick-nicodemus commented 2 years ago

I need to get this cleaned up before integrating it.