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

Continuation modalities and Lawvere–Tierney topologies #1157

Merged
merged 24 commits into from
Nov 5, 2024
Merged

Continuation modalities and Lawvere–Tierney topologies #1157

merged 24 commits into from
Nov 5, 2024

Commits on Jul 6, 2024

  1. add continuation modalities

    @fredrik-bakke
    fredrik-bakke committed Jul 6, 2024
    Configuration menu
    Copy the full SHA
    c9e36e7 View commit details
    Browse the repository at this point in the history

  2. fix some wording reflective subuniverses

    @fredrik-bakke
    fredrik-bakke committed Jul 6, 2024
    Configuration menu
    Copy the full SHA
    90b112d View commit details
    Browse the repository at this point in the history

  3. double negation is an instance of a continuation

    @fredrik-bakke
    fredrik-bakke committed Jul 6, 2024
    Configuration menu
    Copy the full SHA
    77672c3 View commit details
    Browse the repository at this point in the history

  4. Continuations on propositions define Lawvere–Tierney topologies

    @fredrik-bakke
    fredrik-bakke committed Jul 6, 2024
    Configuration menu
    Copy the full SHA
    86ce4f2 View commit details
    Browse the repository at this point in the history

Commits on Jul 7, 2024

  1. new module structured-types.continuations

    @fredrik-bakke
    fredrik-bakke committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    bfbfe43 View commit details
    Browse the repository at this point in the history

  2. define small and large lawvere-tierney topologies

    @fredrik-bakke
    fredrik-bakke committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    bc52e1d View commit details
    Browse the repository at this point in the history

  3. The double negation modality defines a Lawvere–Tierney topology

    @fredrik-bakke
    fredrik-bakke committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    57e61f2 View commit details
    Browse the repository at this point in the history

  4. fix link

    @fredrik-bakke
    fredrik-bakke committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    7d24858 View commit details
    Browse the repository at this point in the history

  5. fix links

    @fredrik-bakke
    fredrik-bakke committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    235b24e View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2024

  1. move continuations file to foundation

    @fredrik-bakke
    fredrik-bakke committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    59f5e4b View commit details
    Browse the repository at this point in the history

  2. pre-commit

    @fredrik-bakke
    fredrik-bakke committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    24c385e View commit details
    Browse the repository at this point in the history

  3. fixes

    @fredrik-bakke
    fredrik-bakke committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    7839234 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into continuation-modalities

    @fredrik-bakke
    fredrik-bakke authored Jul 10, 2024
    Configuration menu
    Copy the full SHA
    5119c92 View commit details
    Browse the repository at this point in the history

Commits on Jul 11, 2024

  1. A → R is continuation R-stable

    @fredrik-bakke
    fredrik-bakke committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    26a3b55 View commit details
    Browse the repository at this point in the history

Commits on Aug 21, 2024

  1. add continuation modalities to list of higher modalities

    @fredrik-bakke
    fredrik-bakke committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    a4aecbb View commit details
    Browse the repository at this point in the history

Commits on Sep 7, 2024

  1. Merge branch 'master' into continuation-modalities

    @fredrik-bakke
    fredrik-bakke authored Sep 7, 2024
    Configuration menu
    Copy the full SHA
    f8a0338 View commit details
    Browse the repository at this point in the history

Commits on Sep 25, 2024

  1. Merge branch 'master' into continuation-modalities

    @fredrik-bakke
    fredrik-bakke authored Sep 25, 2024
    Configuration menu
    Copy the full SHA
    d99c75f View commit details
    Browse the repository at this point in the history

Commits on Oct 15, 2024

  1. Merge branch 'master' into continuation-modalities

    @fredrik-bakke
    fredrik-bakke authored Oct 15, 2024
    Configuration menu
    Copy the full SHA
    6ca13b5 View commit details
    Browse the repository at this point in the history

Commits on Nov 4, 2024

  1. Merge branch 'master' into continuation-modalities

    @fredrik-bakke
    fredrik-bakke authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    d501b57 View commit details
    Browse the repository at this point in the history

  2. Update src/orthogonal-factorization-systems/large-lawvere-tierney-top… 

    …ologies.lagda.md

Co-authored-by: Egbert Rijke <[email protected]>
    @fredrik-bakke @EgbertRijke
    fredrik-bakke and EgbertRijke authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    d85756a View commit details
    Browse the repository at this point in the history

  3. Update src/orthogonal-factorization-systems/continuation-modalities.l… 

    …agda.md

Co-authored-by: Egbert Rijke <[email protected]>
    @fredrik-bakke @EgbertRijke
    fredrik-bakke and EgbertRijke authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    16af517 View commit details
    Browse the repository at this point in the history

  4. Update src/foundation/continuations.lagda.md 

    Co-authored-by: Egbert Rijke <[email protected]>
    @fredrik-bakke @EgbertRijke
    fredrik-bakke and EgbertRijke authored Nov 4, 2024
    Configuration menu
    Copy the full SHA
    6a250e8 View commit details
    Browse the repository at this point in the history

  5. rephrase

    @fredrik-bakke
    fredrik-bakke committed Nov 4, 2024
    Configuration menu
    Copy the full SHA
    ce98e40 View commit details
    Browse the repository at this point in the history

  6. rewording 2

    @fredrik-bakke
    fredrik-bakke committed Nov 4, 2024
    Configuration menu
    Copy the full SHA
    7a41268 View commit details
    Browse the repository at this point in the history