New profunctors #51
Merged
New profunctors #51
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
|
@stschaef I left a few holes of varying difficulty from where we left off. |
Co-authored-by: Steven Schaefer <stschaef@umich.edu>
maxsnew
force-pushed
the
new-profunctors
branch
from
81699db to
41eccc3
Compare
|
@stschaef I rebased so make sure you use the latest version |
…into new-profunctors
maxsnew
commented
Feb 16, 2024
Cubical/Categories/Displayed/Constructions/IsomorphismMore.agda
Outdated
Show resolved
Hide resolved
…into new-profunctors
stschaef
added a commit
to stschaef/cubical-categorical-logic
that referenced
this pull request
Feb 20, 2024
* new definition of profunctor * progress on slick functor comprehension Co-authored-by: Steven Schaefer <stschaef@umich.edu> * Graph of a profunctor as a displayed category * fix the definition of Graph lol * work on Comma categories * introduction principle for Grothendieck construction * more Functor^D combinators, IsoComma functor constructor * more IsoComma stuff, use Preorder^D a bit less * more progress on Comma cat stuff, probably done for today * start porting FunctorComprehension proof to use Graph/IsoComma * hasPropHomsIsoCommaD * one more hole filled * invMoveLinv * hasPropHomsIsoCommaD1 * hasContrHomsIsoCommaᴰ₁ done * fullyfaithfulcomposition * fullcomposefull, faithfulcomposefaithful * Define new FunctorComprehension, more displayed stuff * Port Adjoints, BinProducts to new format. Better definition of BinProducts * bifunctorial construction of the product of presheaves * simplify definition of product of presheaves functor * compositional definition of BinProduct UMP, Intro rule for Redundant Prod * Define Relators, Natural Elements of Relators * whiskered pi-elt * get counit-elt from whiskering, some naming changes * A few new combinators, fixing definitions broken by changes * fix whitespace * mk\intsrfunctor * Universal Elements as structure to Representations as structure * define the natural isomorphism from representability * line lengths * line lengths but for real * make some local defs private * clean up --------- Co-authored-by: Steven Schaefer <stschaef@umich.edu>
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.
No description provided.