Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Dependent Universal Property of Suspensions #690

Merged
merged 24 commits into from
Aug 20, 2023
Merged

Dependent Universal Property of Suspensions #690

merged 24 commits into from
Aug 20, 2023

Conversation

morphismz
Copy link
Contributor

This pr contains:

  • the definition of a dependent suspension structure
  • the definition of the function dependent-ev-suspension
  • the definition of the dependent universal property of suspensions

@EgbertRijke
Copy link
Collaborator

A merge conflict came up after merging your previous PR on the adjunction.

@morphismz
Copy link
Contributor Author

A merge conflict came up after merging your previous PR on the adjunction.

Thanks for the heads up! Looks like it was just a difference in imports. Should be fixed now.

EgbertRijke
EgbertRijke reviewed Aug 10, 2023
View reviewed changes
Copy link
Collaborator

@EgbertRijke EgbertRijke left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In general, put lambda-expressions in parentheses like everything else. I know that agda allows and encourages lambda-expressions to not be in parentheses, but having such inconsistent style makes the code harder to read.

src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
@morphismz
Copy link
Contributor Author

sorry about all the formatting errors! I'll make sure to be better about that in subsequent prs. This one should be fixed, though.

@EgbertRijke
Copy link
Collaborator

Awesome! I thought I'd just go through them systematically, since you are a serious contributor now:)

@morphismz
Copy link
Contributor Author

Thanks, the feedback is helpful! And let me know if there is anything else to do on this pr.

Also, in general, should I mark the conversations as resolved when I make those changes? Or leave it to the reviewer to come back and mark them as resolved when they agree my changes fix the problem?

fredrik-bakke
fredrik-bakke reviewed Aug 18, 2023
View reviewed changes
Copy link
Collaborator

@fredrik-bakke fredrik-bakke left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems some of Egbert's comments were not resolved properly. I've taken the liberty to reopen them and suggest the proper formatting. I also inserted a couple of my own suggestions. Hope this helps!

src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
src/synthetic-homotopy-theory/suspensions-of-types.lagda.md Outdated Show resolved Hide resolved
@morphismz @fredrik-bakke
Apply suggestions from code review
d601b03 
implement suggestions

Co-authored-by: Fredrik Bakke <[email protected]>
@morphismz
Copy link
Contributor Author

Oh thanks Fredrik. I think I misunderstood some of the suggestions, and mistakenly thought I implemented some of the others.

@fredrik-bakke
Copy link
Collaborator

No worries! The comments can be a bit hard to keep track of sometimes. If you're using VS Code, I can recommend using the GitHub Pull Requests and Issues extension. It will display the comments directly in your code where they were placed.

Anyways, everything seems to be in order now, so I'll merge this PR. Thank you again!

@fredrik-bakke fredrik-bakke merged commit 94f5928 into UniMath:master Aug 20, 2023
@morphismz morphismz deleted the dependent-up-susp branch August 21, 2023 03:09
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Aug 22, 2023
@morphismz @EgbertRijke @fredrik-bakke
Dependent Universal Property of Suspensions (UniMath#690)
34c2ecf 
This pr contains:

- the definition of a dependent suspension structure
- the definition of the function dependent-ev-suspension
- the definition of the dependent universal property of suspensions

---------

Co-authored-by: Egbert Rijke <[email protected]>
Co-authored-by: Fredrik Bakke <[email protected]>
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Aug 22, 2023
@fredrik-bakke
Squashed commit of the following:
e36ae09 
commit b02a0ad
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 22 13:19:51 2023 +0200

    file-conventions simplification

commit 7a45f75
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 22 13:13:14 2023 +0200

    Fix UniMath#704

commit a37f4f2
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 22 11:42:54 2023 +0200

    vscode ignore pull requests in `master`

commit 2c189a0
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 22 11:42:32 2023 +0200

    Fix `os.walk` yields directories that don't exist
    Probably due to caching

commit 165321c
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 21 23:08:26 2023 +0200

    Cyclic groups (UniMath#697)

    This PR introduces cyclic groups to the library, in several equivalent
    forms.

    ---------

    Co-authored-by: Fredrik Bakke <[email protected]>

commit 85d19a5
Author: maybemabeline <[email protected]>
Date:   Mon Aug 21 21:24:18 2023 +0200

    Refactor nilradical proof for prime ideals (UniMath#699)

    I refactored the proof that the nilradical is included in every prime
    ideal as discussed in the discord server. I also added some auxiliary
    functions for prime ideals viewed as radical ideals. Regarding the last
    function, I wasn't sure whether to keep it because agda accepts
    membership in a prime ideal and in the corresponding radical ideal as
    definitionally equal, but in the nilradical proof it feels wrong to
    prove something for prime ideals using a function about radical ideals
    directly.
    I also wasn't sure whether the naming of these functions follows
    conventions correctly.

    ---------

    Co-authored-by: Fredrik Bakke <[email protected]>

commit 34c2ecf
Author: Raymond Baker <[email protected]>
Date:   Sun Aug 20 04:16:03 2023 -0600

    Dependent Universal Property of Suspensions (UniMath#690)

    This pr contains:

    - the definition of a dependent suspension structure
    - the definition of the function dependent-ev-suspension
    - the definition of the dependent universal property of suspensions

    ---------

    Co-authored-by: Egbert Rijke <[email protected]>
    Co-authored-by: Fredrik Bakke <[email protected]>

commit 7c87d5f
Author: Fredrik Bakke <[email protected]>
Date:   Fri Aug 18 16:26:57 2023 +0200

    Compatibility patch agda-mode (UniMath#698)

    A compatibility patch for version `0.4.0` of agda-mode. With this
    version, agda-mode defined its own file format for literate agda
    markdown files, conflicting with the file format defined by agda-syntax.

commit 7ef1685
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 14 11:04:53 2023 +0200

    adding overview to installation guide (UniMath#695)

commit 12e37b1
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 7 15:53:53 2023 +0200

    Recovering the guidelines for direct clones (UniMath#694)

commit 7fc8097
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 7 14:23:29 2023 +0200

    Normalizers, normal closures, normal cores, and centralizers (UniMath#693)

    This PR adds normalizers, normal closures, normal cores, and
    centralizers to the library.

commit 58ce51d
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 7 10:34:46 2023 +0200

    Guidelines for forking the repository and creating branches within clone (UniMath#692)

commit 7608668
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 7 09:17:33 2023 +0200

    Recommend cloning shallow library (UniMath#691)

    This PR recommends users to clone a shallow copy of the library, to
    address UniMath#689.

commit 37c577e
Author: Raymond Baker <[email protected]>
Date:   Mon Aug 7 00:21:29 2023 -0600

    suspension loop space adjunction (UniMath#688)

    This pr contains:
    - definition of the underlying map of the equivalance
    - definition of the underlying map of the inverse

    Proof that these maps are in fact inverses of each other must wait until
    another pr since I first must formalize the dependent universal property
    of suspensions

commit 013e3f5
Author: Egbert Rijke <[email protected]>
Date:   Thu Aug 3 11:48:37 2023 +0200

    Adding comments to the style guides that (subsection) titles should be on one line (UniMath#687)

    ...even if they are longer than the 80 character line limit.

commit dd04229
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 1 14:33:32 2023 +0200

    Small constructions from large ones in order theory (UniMath#680)

    Defines
    - small semigroups from large semigroups
    - small preorders from large preorders
    - small posets from large posets
    - small suplattices from large suplattices
    - small meet semilattices from large meet semilattices
    - large preorders are large precategories
    - large posets are large categories

commit 3dce59f
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 8 13:40:43 2023 +0200

    small edits

commit 4f8e685
Author: Fredrik Bakke <[email protected]>
Date:   Sat Aug 5 23:02:04 2023 +0200

    redefine wide function classes to contain all equivalences

commit f60a810
Author: Fredrik Bakke <[email protected]>
Date:   Sat Aug 5 22:53:32 2023 +0200

    Having equivs is the same as having identities

commit 126c487
Author: Fredrik Bakke <[email protected]>
Date:   Sat Aug 5 21:18:34 2023 +0200

    random fixes
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fredrik-bakke fredrik-bakke fredrik-bakke left review comments

@EgbertRijke EgbertRijke EgbertRijke left review comments

Assignees
No one assigned
Labels
synthetic-homotopy-theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@morphismz @EgbertRijke @fredrik-bakke