Morita equivalence #44
Draft
Conversation
This file contains 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
added 27 commits
September 21, 2021 17:01
(taking a snapshot: heading home)
Abandon 2-categorical def. of adjunction since I don't want to formulate 2-categories
Also, might freeze this branch until after deadline
takes a horribly long time to type-check though
Also refactor out the property 'f left-adjoint-to g' in preparation for dualisation (since I want to avoid re-doing the naturality proof again :D)
Also, instantiate the naturality condition for each of one arguments of the pair, since it simplifies the proofs
Define universal arrows Start proving that a universal arrow from every object gives a left adjoint
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Speculative investigation of taking advantage of morita equivalence
To do so, we need to implement some category theoretic machinery.
It would be much better to port @JacquesCarette and @HuStmpHrrr 's agda categories library, but we probably want to introduce more eta-equality into the type-theory to gain all the dualisation benefits.