Comonoids, duality, and related displayed tech#584
Draft
jajaperson wants to merge 53 commits intothe1lab:mainfrom
Draft
Comonoids, duality, and related displayed tech#584jajaperson wants to merge 53 commits intothe1lab:mainfrom
jajaperson wants to merge 53 commits intothe1lab:mainfrom
Conversation
Since duality of monoids and comonoids should be constructed as a functor
displayed over the isomorphism
$(\mathcal C^\mathrm{op})^\mathrm{op} \cong \mathcal C$, this refactors
`Cat.Base` slightly by removing the `C^op^op≡C` in favour of defining
the underlying isomorphism in a separate module, which can then be used
to define a path between precategories.
Also I sorted some imports.
So that we can use it without importing all the bicategory stuff.
For consistency with `Cat.Reasoning`.
Member
New pages
Changed pages
|
We may want to revert to not exporting `inverse-unique₀` and just using `inverse-unique refl refl`. However, since separating this out made sense from an expository point of view, I have made use of `inverse-unique₀` throughout the library.
The intention is to later show this to be a displayed isomorphism of displayed categories.
It's not used anywhere and with agda/agda#8318 merged there shouldn't ever be a reason to.
This ensures that `cabal build shake` succeeds without warnings, as a first step towards making it possible to build the 1Lab without Nix.
Replace the bespoke `mkDerivation` with an equivalent `callCabal2nix` so that dependencies and other build options are only tracked in one place. These changes are made with *four* use cases in mind: - `nix-build` for building the 1Lab; - `nix-shell --run '1lab-shake all'` for working on the 1Lab interactively; - `nix-shell -A shakefile --run 'cabal run 1lab-shake -- all'` for working on the 1Lab *and the build script* interactively; - `cabal run 1lab-shake -- all` outside of a Nix shell, after following the instructions in the README for setting up dependencies.
Since 9.10 is the default version in nixpkgs, Haskell dependencies are now available from cache.nixos.org.
`all-pages.agda` is already generated by the shakefile. To build the 1Lab as an Agda library, one can use `agda --build-library`.
Both available mechanisms for determining whether we are in a nix-shell invocation are currently broken: - the `inNixShell` argument is not set by nix-direnv; - the `IN_NIX_SHELL` environment variable is an environment variable, so it affects nix-build calls inside nix shells. So we keep the shells separate instead.
jajaperson
force-pushed
the
monoidal-internalization
branch
from
143542b to
8b48936
Compare
Contributor
Author
|
The functions-over stuff was straying into the realm of centipede type theory, so I have moved the relevant stuff into a different branch where it will stay unless I can find an actual use for it. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
WIP
Description
This PR is working up to proving$\mathrm{Mon}(\mathcal C^\mathrm{op})^\mathrm{op}$ and $\mathrm{Comon}(\mathcal C)$ are equivalent as displayed categories. This has involved defining a lot of displayed machinery.
Checklist
Before submitting a merge request, please check the items below:
support/sort-imports.hs(ornix run --experimental-features nix-command -f . sort-imports).If your change affects many files without adding substantial content, and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title with
chore:.Footnotes
Ahrens, Benedikt, and Peter LeFanu Lumsdaine. 2017. “Displayed Categories.” In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), edited by Dale Miller, vol. 84. Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSCD.2017.5. ↩