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.

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

Separating Objects #412

Closed
TOTBWF opened this issue Jul 19, 2024 · 0 comments · Fixed by #413
Closed

Separating Objects #412

TOTBWF opened this issue Jul 19, 2024 · 0 comments · Fixed by #413
Assignees
Labels
category-theory For issues/pull requests relating to the Cat.* namespace

Comments

@TOTBWF
Copy link
Collaborator

TOTBWF commented Jul 19, 2024

No description provided.

@TOTBWF TOTBWF added the category-theory For issues/pull requests relating to the Cat.* namespace label Jul 19, 2024
@TOTBWF TOTBWF self-assigned this Jul 19, 2024
@TOTBWF TOTBWF mentioned this issue Jul 22, 2024
3 tasks
TOTBWF added a commit that referenced this issue Jul 26, 2024
# Description

This PR defines a bunch of classes of
[separators](https://ncatlab.org/nlab/show/separator), and proves some
various properties. In particular, this PR covers the following results
from Borceux Vol 1, 4.5. Closes #412.

* 4.5.1:
  * is-separating-family
  * is-separator
* 4.5.2:
  * (⇒) separating-family→epic
  * (⇐) epic→separating-family
* 4.5.3
  * is-strong-separating-family
  * is-regular-separating-family
* 4.5.4:
  * is-dense-separating-family
  * is-dense-separator
* 4.5.5:
  * dense-separator→regular-separator
  * regular-separator→strong-separator
* 4.5.7:
  * is-jointly-faithful
  * is-jointly-conservative
* 4.5.8:
  * (⇒) separating-family→jointly-faithful
  * (⇐) jointly-faithful→separating-family
* 4.5.9:
  * (⇒) separator→faithful
  * (⇐) faithful→separator
* 4.5.10:
  * (⇒) strong-separating-family→jointly-conservative
  * (⇐) lex+jointly-conservative→strong-separating-family
* 4.5.11:
  * (⇒) strong-separator→conservative
  * (⇐) lex+conservative→strong-separator
* 4.5.12: equalisers+jointly-conservative→separating-family
* 4.5.13: N/A
* 4.5.14
  * (⇒) dense-separating-family→jointly-ff
  * (⇐) jointly-ff→dense-separating-family
* 4.5.16: zero+separating-family→separator

## Checklist

Before submitting a merge request, please check the items below:

- [x] I've read [the contributing
guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md).
- [x] The imports of new modules have been sorted with
`support/sort-imports.hs` (or `nix run --experimental-features
nix-command -f . sort-imports`).
- [x] All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content,
and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title
with `chore:`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
category-theory For issues/pull requests relating to the Cat.* namespace
Projects
Status: Done
Development

Successfully merging a pull request may close this issue.

1 participant