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

Refactor files about identity types and homotopies #1014

Merged
merged 155 commits into from Feb 6, 2024
Merged

Refactor files about identity types and homotopies #1014

merged 155 commits into from Feb 6, 2024

Commits on Jan 29, 2024

  1. replace whisk\b with whisker

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    52c1e0f View commit details
    Browse the repository at this point in the history

  2. replace htpy-right-whisker with right-whisker-htpy, and htpy-left-whi… 

    …sker with left-whisker-htpy
    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    0ac9514 View commit details
    Browse the repository at this point in the history

  3. replace whisker-htpy-inv-htpy with whisker-inv-htpy

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    b34b11a View commit details
    Browse the repository at this point in the history

  4. replace whisker-comp with whisker-htpy

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    b6cbf11 View commit details
    Browse the repository at this point in the history

  5. replace associative-left/right-whisker-htpy with preserves-comp-left/… 

    …right-whisker-htpy
    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    fd1a8a6 View commit details
    Browse the repository at this point in the history

  6. make pre-commit

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    4e8c333 View commit details
    Browse the repository at this point in the history

  7. replace identification-left/right-whisker with left/right-whisker-ide… 

    …ntification
    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    dc27e79 View commit details
    Browse the repository at this point in the history

  8. factoring out whiskering of identifications

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    8c0b254 View commit details
    Browse the repository at this point in the history

  9. refactor

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    480a4ae View commit details
    Browse the repository at this point in the history

  10. moving file

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    89f0e61 View commit details
    Browse the repository at this point in the history

  11. renaming imports

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    9f9bd6f View commit details
    Browse the repository at this point in the history

  12. a bunch of refactoring

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    01355e9 View commit details
    Browse the repository at this point in the history

  13. new file

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    1b24310 View commit details
    Browse the repository at this point in the history

  14. work

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    8fd598e View commit details
    Browse the repository at this point in the history

  15. refactoring the action of functions on higher identifications

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    42babf0 View commit details
    Browse the repository at this point in the history

  16. refactoring the action of functions on higher identifications

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    3501d46 View commit details
    Browse the repository at this point in the history

  17. adding idea section

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    3245ff8 View commit details
    Browse the repository at this point in the history

  18. fix imports

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    7a89f01 View commit details
    Browse the repository at this point in the history

  19. refactoring commuting squares of maps

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    dbdc723 View commit details
    Browse the repository at this point in the history

  20. fixing the order of arguments of pasting lemmas of commuting squares

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    9aef0a2 View commit details
    Browse the repository at this point in the history

  21. make pre-commit

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    167a59e View commit details
    Browse the repository at this point in the history

  22. refactoring foundation-core.commuting-squares-identifications

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    9e71bd8 View commit details
    Browse the repository at this point in the history

  23. more explaining

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    80147c1 View commit details
    Browse the repository at this point in the history

  24. make pre-commit

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    28c194f View commit details
    Browse the repository at this point in the history

  25. more explanations and diagrams

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    ec0550e View commit details
    Browse the repository at this point in the history

  26. using action on higher identifications

    @EgbertRijke
    EgbertRijke committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    f28203d View commit details
    Browse the repository at this point in the history

Commits on Jan 30, 2024

  1. factoring out the action of maps on commuting triangles of identifica… 

    …tions
    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    406c632 View commit details
    Browse the repository at this point in the history

  2. further refactoring commuting triangles of identifications'

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    5c2d109 View commit details
    Browse the repository at this point in the history

  3. compute map-coherence-triangle-identifications with refl on the right

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    b2b5727 View commit details
    Browse the repository at this point in the history

  4. edits

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    309638c View commit details
    Browse the repository at this point in the history

  5. make pre-commit

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    f3c1fab View commit details
    Browse the repository at this point in the history

  6. edits

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    dad9c26 View commit details
    Browse the repository at this point in the history

  7. rename whisker-identification-Ω² to whisker-Ω²

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    810bebe View commit details
    Browse the repository at this point in the history

  8. removing superfluous entries

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    0c68fd4 View commit details
    Browse the repository at this point in the history

  9. adding file about whiskering of higher hommotopies

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    fb97716 View commit details
    Browse the repository at this point in the history

  10. make pre-commit

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    e05fbfa View commit details
    Browse the repository at this point in the history

  11. renaming whiskering of higher homotopies

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    752d8ba View commit details
    Browse the repository at this point in the history

  12. trying to use left-whisker-htpy2 in places where I used ap2 before

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    5e2e182 View commit details
    Browse the repository at this point in the history

  13. closing parenthesis

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    748f99e View commit details
    Browse the repository at this point in the history

  14. edits

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    cfd18d2 View commit details
    Browse the repository at this point in the history

  15. make pre-commit

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    6adf32c View commit details
    Browse the repository at this point in the history

  16. adding new files to the table about identity types

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    c21d199 View commit details
    Browse the repository at this point in the history

  17. unifying the duplicate entries for pastings of commuting squares of i… 

    …dentifications
    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    fa752c2 View commit details
    Browse the repository at this point in the history

  18. unifying the duplicate entries for pastings of commuting squares of i… 

    …dentifications
    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    e49e5ce View commit details
    Browse the repository at this point in the history

  19. splicing commuting triangles of identifications

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    4cc4a8e View commit details
    Browse the repository at this point in the history

  20. make pre-commit

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    8cf9a28 View commit details
    Browse the repository at this point in the history

  21. removing a bunch of ap concats

    @EgbertRijke
    EgbertRijke committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    65c4a23 View commit details
    Browse the repository at this point in the history

Commits on Jan 31, 2024

  1. Merge branch 'master' of github.com:UniMath/agda-unimath into whisker

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    4bce993 View commit details
    Browse the repository at this point in the history

  2. formatting

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    eaf7af3 View commit details
    Browse the repository at this point in the history

  3. fix import

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    edc4c3a View commit details
    Browse the repository at this point in the history

  4. setup for whiskering of commuting squares of identifications

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    1e9de32 View commit details
    Browse the repository at this point in the history

  5. make pre-commit

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    fa5aba5 View commit details
    Browse the repository at this point in the history

  6. edits

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    110c111 View commit details
    Browse the repository at this point in the history

  7. implementing whiskering in many files

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    87ee190 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'master' of github.com:UniMath/agda-unimath into whisker

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    379ba7e View commit details
    Browse the repository at this point in the history

  9. renaming

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    d239ab2 View commit details
    Browse the repository at this point in the history

  10. in the middle of some work

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    16b6099 View commit details
    Browse the repository at this point in the history

  11. edits

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    a4c7267 View commit details
    Browse the repository at this point in the history

  12. refactoring identity types

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    9c3121c View commit details
    Browse the repository at this point in the history

  13. explanation

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    6ffcaff View commit details
    Browse the repository at this point in the history

  14. make pre-commit

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    8a034fa View commit details
    Browse the repository at this point in the history

  15. concatenation lemmas for commuting squares of identifications

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    fe3fd1e View commit details
    Browse the repository at this point in the history

  16. make pre-commit

    @EgbertRijke
    EgbertRijke committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    144a497 View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2024

  1. fix

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    5e0c38f View commit details
    Browse the repository at this point in the history

  2. fix broken link

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    c1ff686 View commit details
    Browse the repository at this point in the history

  3. finish a sentence

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    0df50c5 View commit details
    Browse the repository at this point in the history

  4. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    d1a6240 View commit details
    Browse the repository at this point in the history

  5. removing a duplicate sentence

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    993cc00 View commit details
    Browse the repository at this point in the history

  6. adding in some extra diagrams

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    11d5e70 View commit details
    Browse the repository at this point in the history

  7. adding some extra corollaries

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    eb4994d View commit details
    Browse the repository at this point in the history

  8. typos

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    ac6ab17 View commit details
    Browse the repository at this point in the history

  9. shortening proofs of pasting lemmas of commuting squares of identific… 

    …ations
    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    3c95ce3 View commit details
    Browse the repository at this point in the history

  10. removing more duplicates

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    79c35d3 View commit details
    Browse the repository at this point in the history

  11. merging foundation-core and foundation files of commuting squares of … 

    …identifications
    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    15a48ac View commit details
    Browse the repository at this point in the history

  12. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    0a3f52f View commit details
    Browse the repository at this point in the history

  13. renaming horizontal concatenation of homotopies

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    16b9877 View commit details
    Browse the repository at this point in the history

  14. fix name whisker-square-htpy to whisker-coherence-square-htpy

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    059ec25 View commit details
    Browse the repository at this point in the history

  15. rename comp-htpy to concat-htpy

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    d6ffa28 View commit details
    Browse the repository at this point in the history

  16. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    8a9dafe View commit details
    Browse the repository at this point in the history

  17. remove lossy-unification

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    8d4e2a8 View commit details
    Browse the repository at this point in the history

  18. uniform naming

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    4e47643 View commit details
    Browse the repository at this point in the history

  19. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    2cf5330 View commit details
    Browse the repository at this point in the history

  20. wip

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    f65af31 View commit details
    Browse the repository at this point in the history

  21. general whiskering operations

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    f779897 View commit details
    Browse the repository at this point in the history

  22. new scheme

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    e4481f7 View commit details
    Browse the repository at this point in the history

  23. work

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    539b491 View commit details
    Browse the repository at this point in the history

  24. work on lifting squares

    @EgbertRijke
    EgbertRijke committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    2c0be80 View commit details
    Browse the repository at this point in the history

Commits on Feb 2, 2024

  1. work

    @EgbertRijke
    EgbertRijke committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    a5a337b View commit details
    Browse the repository at this point in the history

  2. work

    @EgbertRijke
    EgbertRijke committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    9e4d1d8 View commit details
    Browse the repository at this point in the history

  3. work

    @EgbertRijke
    EgbertRijke committed Feb 2, 2024
    Configuration menu
    Copy the full SHA
    2177aa4 View commit details
    Browse the repository at this point in the history

Commits on Feb 3, 2024

  1. work

    @EgbertRijke
    EgbertRijke committed Feb 3, 2024
    Configuration menu
    Copy the full SHA
    c82391b View commit details
    Browse the repository at this point in the history

  2. using double-whisker-comp

    @EgbertRijke
    EgbertRijke committed Feb 3, 2024
    Configuration menu
    Copy the full SHA
    0e97f4f View commit details
    Browse the repository at this point in the history

  3. higher homotopies of morphisms of arrows

    @EgbertRijke
    EgbertRijke committed Feb 3, 2024
    Configuration menu
    Copy the full SHA
    a1d8f5e View commit details
    Browse the repository at this point in the history

  4. solving the exercise for fredrik

    @EgbertRijke
    EgbertRijke committed Feb 3, 2024
    Configuration menu
    Copy the full SHA
    d33dcbf View commit details
    Browse the repository at this point in the history

  5. work

    @EgbertRijke
    EgbertRijke committed Feb 3, 2024
    Configuration menu
    Copy the full SHA
    693d771 View commit details
    Browse the repository at this point in the history

  6. The left unit law of concatenation of homotopies of morphisms of arrows

    @EgbertRijke
    EgbertRijke committed Feb 3, 2024
    Configuration menu
    Copy the full SHA
    e3b0e7f View commit details
    Browse the repository at this point in the history

  7. work

    @EgbertRijke
    EgbertRijke committed Feb 3, 2024
    Configuration menu
    Copy the full SHA
    ee511ce View commit details
    Browse the repository at this point in the history

Commits on Feb 4, 2024

  1. work

    @EgbertRijke
    EgbertRijke committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    9f32284 View commit details
    Browse the repository at this point in the history

  2. the right unit law for concatenation of homotopies of morphisms of ar… 

    …rows
    @EgbertRijke
    EgbertRijke committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    6ec3bac View commit details
    Browse the repository at this point in the history

  3. complete characterization of identity type of lifting squares

    @EgbertRijke
    EgbertRijke committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    47a6c7d View commit details
    Browse the repository at this point in the history

  4. complete refactoring of lifting squares

    @EgbertRijke
    EgbertRijke committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    28b76a4 View commit details
    Browse the repository at this point in the history

  5. refactoring pullback-hom

    @EgbertRijke
    EgbertRijke committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    f133d25 View commit details
    Browse the repository at this point in the history

  6. implementing changes in orthogonal maps

    @EgbertRijke
    EgbertRijke committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    1a983af View commit details
    Browse the repository at this point in the history

  7. It compiles again

    @EgbertRijke
    EgbertRijke committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    7bf3cda View commit details
    Browse the repository at this point in the history

  8. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    f7e785c View commit details
    Browse the repository at this point in the history

  9. fix broken links

    @EgbertRijke
    EgbertRijke committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    60c5912 View commit details
    Browse the repository at this point in the history

  10. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 4, 2024
    Configuration menu
    Copy the full SHA
    7b50668 View commit details
    Browse the repository at this point in the history

Commits on Feb 5, 2024

  1. resolving first batch of review comments

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    f64eaec View commit details
    Browse the repository at this point in the history

  2. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    c754ab3 View commit details
    Browse the repository at this point in the history

  3. coherence-map-inv-is-invertible

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    887afb6 View commit details
    Browse the repository at this point in the history

  4. whiskering triangles of homotopies

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    4d6d295 View commit details
    Browse the repository at this point in the history

  5. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    22bf080 View commit details
    Browse the repository at this point in the history

  6. fixing some names

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    3da108a View commit details
    Browse the repository at this point in the history

  7. addressing duplications in function extensionality

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    3abe9e2 View commit details
    Browse the repository at this point in the history

  8. complete the removal of duplicate entries in function extensionality

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    619becd View commit details
    Browse the repository at this point in the history

  9. formatting dependent coforks

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    c90bab1 View commit details
    Browse the repository at this point in the history

  10. address misnamings

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    c7afd14 View commit details
    Browse the repository at this point in the history

  11. addressing final comments

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    fcc1b54 View commit details
    Browse the repository at this point in the history

  12. add new file to table

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    e256ef5 View commit details
    Browse the repository at this point in the history

  13. fix misspelled Agda names in concept macros

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    bb061ee View commit details
    Browse the repository at this point in the history

  14. improve namings of coherence-square-inv-... entries

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    573d9cf View commit details
    Browse the repository at this point in the history

  15. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    9cf3706 View commit details
    Browse the repository at this point in the history

  16. resolve merge conflicts

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    e98f6cc View commit details
    Browse the repository at this point in the history

  17. typos

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    8988a6e View commit details
    Browse the repository at this point in the history

  18. non- to non

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    4db0da6 View commit details
    Browse the repository at this point in the history

  19. suggestions from the review

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    3c3158d View commit details
    Browse the repository at this point in the history

  20. more review suggestions

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    867a349 View commit details
    Browse the repository at this point in the history

  21. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    292a150 View commit details
    Browse the repository at this point in the history

  22. review comments

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    1ec2cbb View commit details
    Browse the repository at this point in the history

  23. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    b29c36c View commit details
    Browse the repository at this point in the history

  24. updating informal remarks about function extensionality

    @EgbertRijke
    EgbertRijke committed Feb 5, 2024
    Configuration menu
    Copy the full SHA
    8942712 View commit details
    Browse the repository at this point in the history

Commits on Feb 6, 2024

  1. add compute-htpy-eq-refl

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    090572e View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of github.com:UniMath/agda-unimath into whisker

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    80eaeb7 View commit details
    Browse the repository at this point in the history

  3. (_∙_)

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

  4. line break

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    28cea10 View commit details
    Browse the repository at this point in the history

  5. eq-pair-eq-fiber

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    e97048a View commit details
    Browse the repository at this point in the history

  6. edits

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    c2b40f9 View commit details
    Browse the repository at this point in the history

  7. Update src/foundation/whiskering-homotopies-concatenation.lagda.md 

    Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
    @EgbertRijke @fredrik-bakke
    EgbertRijke and fredrik-bakke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    b59e8b9 View commit details
    Browse the repository at this point in the history

  8. Update src/foundation/whiskering-homotopies-concatenation.lagda.md 

    Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
    @EgbertRijke @fredrik-bakke
    EgbertRijke and fredrik-bakke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    4e7896e View commit details
    Browse the repository at this point in the history

  9. Update src/foundation/whiskering-homotopies-concatenation.lagda.md 

    Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
    @EgbertRijke @fredrik-bakke
    EgbertRijke and fredrik-bakke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    58ae443 View commit details
    Browse the repository at this point in the history

  10. Update src/foundation/whiskering-homotopies-composition.lagda.md 

    Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
    @EgbertRijke @fredrik-bakke
    EgbertRijke and fredrik-bakke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    adc703d View commit details
    Browse the repository at this point in the history

  11. Update src/foundation/whiskering-homotopies-composition.lagda.md 

    Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
    @EgbertRijke @fredrik-bakke
    EgbertRijke and fredrik-bakke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    f7529cd View commit details
    Browse the repository at this point in the history

  12. edit

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    053b299 View commit details
    Browse the repository at this point in the history

  13. Merge branch 'whisker' of github.com:EgbertRijke/agda-unimath into wh… 

    …isker
    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    d70471b View commit details
    Browse the repository at this point in the history

  14. make pre-commit

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    52071b4 View commit details
    Browse the repository at this point in the history

  15. lifting structures of squares

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    012d9cd View commit details
    Browse the repository at this point in the history

  16. more eq-pair-eq-fiber

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    ac916e5 View commit details
    Browse the repository at this point in the history

  17. Update src/foundation/commuting-squares-of-homotopies.lagda.md 

    Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
    @EgbertRijke @fredrik-bakke
    EgbertRijke and fredrik-bakke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    cd47a0d View commit details
    Browse the repository at this point in the history

  18. making the library compile

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    c6069aa View commit details
    Browse the repository at this point in the history

  19. edits

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    555074a View commit details
    Browse the repository at this point in the history

  20. coherence squares of homotopies

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    b20d392 View commit details
    Browse the repository at this point in the history

  21. coherence squares homotopies

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    84f100b View commit details
    Browse the repository at this point in the history

  22. Done

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    1b3183c View commit details
    Browse the repository at this point in the history

  23. final comment

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    22aa216 View commit details
    Browse the repository at this point in the history

  24. addressing wrong Agda field in concept macro

    @EgbertRijke
    EgbertRijke committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    3757f61 View commit details
    Browse the repository at this point in the history