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

Literature – Idempotents in Intensional Type Theory #1160

Merged
merged 17 commits into from
Aug 21, 2024
Merged

Literature – Idempotents in Intensional Type Theory #1160

merged 17 commits into from
Aug 21, 2024

Commits on Aug 2, 2024

  1. add uniqueness of identity proofs

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

  2. update reference

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

  3. add module idempotents-in-intensional-type-theory

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

  4. remaining sections

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

  5. add "WIP" info

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

Commits on Aug 3, 2024

  1. The action of tot on retracts

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

  2. use extensionality prefix for retract lemmas

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

  3. characterization of identity of quasicoherently idempotent maps

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

  4. edits literature file

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

  5. define coherently idempotent maps

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

  6. link formalization for 9 Coherent idempotents

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

Commits on Aug 5, 2024

  1. finishing toches

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

  2. fixes

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

Commits on Aug 17, 2024

  1. Apply suggestions from code review 

    Co-authored-by: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
    @fredrik-bakke @VojtechStep
    fredrik-bakke and VojtechStep authored Aug 17, 2024
    Configuration menu
    Copy the full SHA
    5357793 View commit details
    Browse the repository at this point in the history

Commits on Aug 18, 2024

  1. :=

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

Commits on Aug 21, 2024

  1. explain corollary 4.7

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

  2. Merge branch 'master' into literature-idempotents-split

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