Skip to content

Subframes and quotient locales via nuclei #613

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
Merged
merged 15 commits into from
May 11, 2023
Merged

Subframes and quotient locales via nuclei #613

merged 15 commits into from
May 11, 2023

Conversation

EgbertRijke
Copy link
Collaborator

No description provided.

@EgbertRijke EgbertRijke marked this pull request as ready for review May 10, 2023 21:56
@EgbertRijke EgbertRijke changed the title Galois connections Towards subframes and quotient locales via nuclei May 10, 2023
fredrik-bakke
fredrik-bakke approved these changes May 11, 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.

Looks good to me :)

@EgbertRijke
Copy link
Collaborator Author

Done!

@EgbertRijke EgbertRijke changed the title Towards subframes and quotient locales via nuclei Subframes and quotient locales via nuclei May 11, 2023
@EgbertRijke EgbertRijke merged commit 06c59ad into UniMath:master May 11, 2023
fredrik-bakke pushed a commit to fredrik-bakke/agda-unimath that referenced this pull request May 18, 2023
@EgbertRijke @fredrik-bakke
Subframes and quotient locales via nuclei (UniMath#613)
76bf8c7
fredrik-bakke pushed a commit to fredrik-bakke/agda-unimath that referenced this pull request May 20, 2023
@EgbertRijke @fredrik-bakke
Subframes and quotient locales via nuclei (UniMath#613)
ee5a96c
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request May 28, 2023
@fredrik-bakke
Squashed commit of the following:
f64c83c 
commit 3b74252
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 27 22:51:21 2023 -0400

    fix indentation

commit 880504d
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 27 21:03:31 2023 -0400

    remove punctuation at end of headers

commit cb2a09c
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 27 21:03:15 2023 -0400

    pre-commit autoremove punctuation at end of header

commit f19934c
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 27 20:52:42 2023 -0400

    add remarks about missing contents

commit 582e75c
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 27 20:34:57 2023 -0400

    pre-commit detect empty sections at end of file

commit 3d53688
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 27 19:45:19 2023 -0400

    remove empty code blocks

commit 437056c
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 27 19:45:04 2023 -0400

    compatibility markdown-conventions and fix-imports

commit 8c7f782
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 27 19:38:57 2023 -0400

    pre-commit autoremove empty code blocks

commit 6f84849
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 14:28:44 2023 +0200

    fix some indentation and then give up for the moment

commit ccdad61
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 14:05:31 2023 +0200

    add `indentation_conventions.py`

commit ba930b4
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 13:33:11 2023 +0200

    rename pre-commit scripts

commit 2cd2433
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 13:09:02 2023 +0200

    Add and enforce section conventions

commit db60c6f
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 12:07:41 2023 +0200

    rename `remove_extra_blank_lines.py`
    to `blank_line_conventions.py`

commit 0d1f085
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 12:05:11 2023 +0200

    Fix top section headers not at start of file

commit 986a68d
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 11:52:20 2023 +0200

    swap to using `_-ℤ_`

commit cea0cf6
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 10:53:52 2023 +0200

    define infix operator `_-ℤ_` for difference

commit b2cd359
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 10:44:42 2023 +0200

    Fix empty subsubsections

commit ecd6061
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 10:05:23 2023 +0200

    fix empty subsections

commit 3823a10
Merge: 23e5534 92c52ba
Author: Fredrik Bakke <[email protected]>
Date:   Sun May 21 06:43:30 2023 +0200

    Merge branch 'UniMath:master' into modalities3

commit 23e5534
Author: Jonathan Cubides <[email protected]>
Date:   Fri May 19 01:04:26 2023 +0200

    Fix: missing logo (UniMath#625)

    Minor fix due to a local cache issue

commit 0ba07cd
Author: Jonathan Cubides <[email protected]>
Date:   Fri May 19 00:09:46 2023 +0200

    Enable  TOC  and fix minor warnings (UniMath#602)

    - Enhance TOC
    - Solves some warnings seen here:
    https://github.com/UniMath/agda-unimath/actions/runs/4991616992/jobs/8939272325#step:12:1304
    - Closes UniMath#614
    - Removes the background from the agda logo.

    I tried syncing SVG stroke colours with agda-logo.css (so it responds to
    the colour theme), but no luck yet. We need more time to figure it out.
    the following is related and the suggestion included in my experiment.

    - rust-lang/mdBook#773

    ---------

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

commit 9b80ef0
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 13 20:29:54 2023 +0200

    Remove unused imports and fix some unaddressed comments (UniMath#621)

    Sorry, my script wasn't finished when I made the last commit in UniMath#620,
    and here are the remaining unused imports. This PR also fixes some
    comments I made earlier that went unaddressed.

    I'm wondering, are the imports scripts interfering with people's merging
    process a lot? If so, we don't have to merge those changes now.

commit 3b658d0
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 13 19:14:02 2023 +0200

    Refactor to use infix binary operators for arithmetic (UniMath#620)

    - Refactor to use infix binary operators for arithmetic.
    - Define infix binary operators for arithmetic operations on the
    Eisenstein integers, Gaussian integers,half integers, and truncation
    levels.
    - Swap to using left/right instead of a `'` for different laws for
    binary arithmetic operators.
    - Some additional refactoring for Eisenstein integers and Gaussian
    integers

    Note that the non-infix variants of the operators are still used some
    places, matching how `Id` and `pair` are used.

commit f77b71e
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 13 14:39:13 2023 +0200

    Define binary operator notations for `mul-ℕ`, `mul-ℤ`, and `exp-ℕ`. (UniMath#618)

    They are `_*ℕ_`, `_*ℤ_`, and `_^ℕ_` respectively.

    In addition to what the title says, I've also refactored the files
    - `multiplication-natural-numbers`
    - `multiplication-integers`
    - `exponentiation-natural-numbers`
    - `absolute-value-integers`

    to use the binary operators where it's natural, to get a sense for how
    this would look. It should be possible to change most usages easily
    enough* with a nice enough regex, but I don't want to do this before I
    get some feedback on whether it is preferable.

    Also, pairs like `is-injective-mul-succ-ℕ` and
    `is-injective-mul-succ-ℕ'` should perhaps be renamed to something like
    `is-injective-left-mul-succ-ℕ` and `is-injective-right-mul-succ-ℕ`.

commit ee5a96c
Author: Egbert Rijke <[email protected]>
Date:   Fri May 12 00:52:35 2023 +0200

    Subframes and quotient locales via nuclei (UniMath#613)

commit 750f151
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 20 17:16:03 2023 +0200

    small fixes

commit e1f3af4
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 20 00:40:58 2023 +0200

    add `is-emb-map-prod`

commit 973a00f
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 20 00:40:29 2023 +0200

    fix expressions in some headers

commit e3f8a25
Author: Fredrik Bakke <[email protected]>
Date:   Tue May 16 14:05:02 2023 +0200

    Swap from `md` to `text` code blocks (UniMath#622)

    - Fix diagrams in `pullback-hom`
    - Swap from `md` to `text` code blocks
    - Register Collatz' bijection in the OEIS file

commit c7398a7
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 13 20:29:54 2023 +0200

    Remove unused imports and fix some unaddressed comments (UniMath#621)

    Sorry, my script wasn't finished when I made the last commit in UniMath#620,
    and here are the remaining unused imports. This PR also fixes some
    comments I made earlier that went unaddressed.

    I'm wondering, are the imports scripts interfering with people's merging
    process a lot? If so, we don't have to merge those changes now.

commit 001e8d7
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 13 19:14:02 2023 +0200

    Refactor to use infix binary operators for arithmetic (UniMath#620)

    - Refactor to use infix binary operators for arithmetic.
    - Define infix binary operators for arithmetic operations on the
    Eisenstein integers, Gaussian integers,half integers, and truncation
    levels.
    - Swap to using left/right instead of a `'` for different laws for
    binary arithmetic operators.
    - Some additional refactoring for Eisenstein integers and Gaussian
    integers

    Note that the non-infix variants of the operators are still used some
    places, matching how `Id` and `pair` are used.

commit fde878d
Author: Fredrik Bakke <[email protected]>
Date:   Sat May 13 14:39:13 2023 +0200

    Define binary operator notations for `mul-ℕ`, `mul-ℤ`, and `exp-ℕ`. (UniMath#618)

    They are `_*ℕ_`, `_*ℤ_`, and `_^ℕ_` respectively.

    In addition to what the title says, I've also refactored the files
    - `multiplication-natural-numbers`
    - `multiplication-integers`
    - `exponentiation-natural-numbers`
    - `absolute-value-integers`

    to use the binary operators where it's natural, to get a sense for how
    this would look. It should be possible to change most usages easily
    enough* with a nice enough regex, but I don't want to do this before I
    get some feedback on whether it is preferable.

    Also, pairs like `is-injective-mul-succ-ℕ` and
    `is-injective-mul-succ-ℕ'` should perhaps be renamed to something like
    `is-injective-left-mul-succ-ℕ` and `is-injective-right-mul-succ-ℕ`.

commit 76bf8c7
Author: Egbert Rijke <[email protected]>
Date:   Fri May 12 00:52:35 2023 +0200

    Subframes and quotient locales via nuclei (UniMath#613)

commit 375210c
Author: VictorBlanchi <[email protected]>
Date:   Thu May 11 16:49:27 2023 +0200

    Iterated cartesian product is closed by permutation (UniMath#617)

    I have shown that the 3 definitions of iterated cartesian product of
    types is closed by permutation.

commit 730861a
Author: Fredrik Bakke <[email protected]>
Date:   Thu May 11 15:51:39 2023 +0200

    alignment of pullback-hom diagrams

commit dab6d30
Author: Fredrik Bakke <[email protected]>
Date:   Thu May 11 12:33:08 2023 +0200

    some nitpicking

commit 469dba3
Author: Fredrik Bakke <[email protected]>
Date:   Wed May 10 21:08:12 2023 +0200

    wording `26-descent`
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 approved these changes

Assignees
No one assigned
Labels
cleanup order-theory
Projects
None yet
Milestone
No milestone
Development

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