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

Duskin's Monadicity Theorem #76

Draft
wants to merge 14 commits into
base: main
Choose a base branch
from
Draft

Duskin's Monadicity Theorem #76

wants to merge 14 commits into from

Commits on May 15, 2022

  1. defn: sections, retractions, split monos/epis

    @TOTBWF
    TOTBWF committed May 15, 2022
    Configuration menu
    Copy the full SHA
    bf86b57 View commit details
    Browse the repository at this point in the history

  2. defn: Add id₂ to Cat.Reasoning

    @TOTBWF
    TOTBWF committed May 15, 2022
    Configuration menu
    Copy the full SHA
    9f8475d View commit details
    Browse the repository at this point in the history

  3. defn: split coequalizers

    @TOTBWF
    TOTBWF committed May 15, 2022
    4 Configuration menu
    Copy the full SHA
    72ca5a3 View commit details
    Browse the repository at this point in the history

  4. defn: absoluteness of split coequalisers

    @TOTBWF
    TOTBWF committed May 15, 2022
    3 Configuration menu
    Copy the full SHA
    b01a536 View commit details
    Browse the repository at this point in the history

  5. fix: tweak public exports of Finitely-complete

    @TOTBWF
    TOTBWF committed May 15, 2022
    Configuration menu
    Copy the full SHA
    4b774fb View commit details
    Browse the repository at this point in the history

  6. defn: Split coequalizers induce quotients

    @TOTBWF
    TOTBWF committed May 15, 2022
    Configuration menu
    Copy the full SHA
    8b8e735 View commit details
    Browse the repository at this point in the history

  7. format: formatting fixes for split coequalisers

    @TOTBWF
    TOTBWF committed May 15, 2022
    Configuration menu
    Copy the full SHA
    b010e02 View commit details
    Browse the repository at this point in the history

  8. format: formatting fixes for split coequaliser properties

    @TOTBWF
    TOTBWF committed May 15, 2022
    Configuration menu
    Copy the full SHA
    bad2d4c View commit details
    Browse the repository at this point in the history

  9. refactor: define product diagrams over the 2 object category

    @TOTBWF
    TOTBWF committed May 15, 2022
    Configuration menu
    Copy the full SHA
    df55454 View commit details
    Browse the repository at this point in the history

Commits on May 16, 2022

  1. defn: split epis of kernel pairs are split coequalizers

    @TOTBWF
    TOTBWF committed May 16, 2022
    Configuration menu
    Copy the full SHA
    3508d94 View commit details
    Browse the repository at this point in the history

  2. defn: reflection of colimits, isomorphisms of colimit coapexes

    @TOTBWF
    TOTBWF committed May 16, 2022
    Configuration menu
    Copy the full SHA
    1a79e3d View commit details
    Browse the repository at this point in the history

  3. defn: conservative functors preserve colimits

    @TOTBWF
    TOTBWF committed May 16, 2022
    Configuration menu
    Copy the full SHA
    4f00251 View commit details
    Browse the repository at this point in the history

  4. defn: coequalisers are colimits

    @TOTBWF
    TOTBWF committed May 16, 2022
    Configuration menu
    Copy the full SHA
    782abd7 View commit details
    Browse the repository at this point in the history

  5. fixup: avoid subst in conservative-reflects-limits 

    Closes #77
    @plt-amy
    plt-amy committed May 16, 2022
    Configuration menu
    Copy the full SHA
    1633a24 View commit details
    Browse the repository at this point in the history