Reed Mullanix
Reed Mullanix
See #16 for more details on the motivation behind this. So far, the code has been way simpler to work with, and the parser has been reduced down to almost...
# Description This PR defines the displayed category of F-algebras, and proceeds to prove Lambeks's lemma and Adamek's theorem. Additionally, it proves that a left adjoint to the forgetful functor...
# Description This PR defines various closures of relations, and also adds the basics of rewriting theory. Highlights include: - Newmans Lemma - Commutative Union Lemma - Church-Rosser is equivalent...
# Description It's a solver for adjoints! Nothing too surprising here, though the evaluation algorithm is pretty fun.
# Description This PR proves that left/right vertical adjoints are (op)fibred. It also performs some housekeeping, most notably by re-exporting `Displayed` from `Cat.Displayed.Reasoning`, like we do with `Cat.Reasoning`. It also...
In #207, I was looking for a better name for the chaotic bifibration; @ncfavier came up with a much better one, so we should use that!
Currently, our definition of cartesian only requires _binary_ products, which is somewhat non-standard. We should probably create a new module `Cat.Cartesian` that exposes this new definition, along with some helpers...
## Patch Description This PR adds the `case-bash!` tactic, which automates the process of performing exhaustive case splits followed by `refl`. This is best demonstrated with, well, a demo! ```agda...
This should be a simple matter of using a font with proper unicode support in ImGui.
The semantics for NuPRL's types are based off of Partial Equivalence Relations, where `a : A` if `a = a in A` under the associated PER. In short, the types...