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

Hofmann-Streicher universes for graphs and globular types #1196

Merged
merged 97 commits into from
Dec 3, 2024
Merged

Hofmann-Streicher universes for graphs and globular types #1196

merged 97 commits into from
Dec 3, 2024

Commits on Sep 24, 2024

  1. work on universal objects

    Egbert Rijke committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    645fdb9 View commit details
    Browse the repository at this point in the history

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

    Egbert Rijke committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    c2abb43 View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2024

  1. adding infrastructure for globular types

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

Commits on Oct 9, 2024

  1. work

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

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

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

Commits on Oct 11, 2024

  1. computation of the universal globular type, and correspondence of dep… 

    …endendent globular types with morphisms into the universal globular type
    @EgbertRijke
    EgbertRijke committed Oct 11, 2024
    Configuration menu
    Copy the full SHA
    72731cb View commit details
    Browse the repository at this point in the history

Commits on Oct 13, 2024

  1. reflexive globular maps

    @EgbertRijke
    EgbertRijke committed Oct 13, 2024
    Configuration menu
    Copy the full SHA
    bb31cac View commit details
    Browse the repository at this point in the history

  2. sections and pi

    @EgbertRijke
    EgbertRijke committed Oct 13, 2024
    Configuration menu
    Copy the full SHA
    f56cc6a View commit details
    Browse the repository at this point in the history

  3. typo

    @EgbertRijke
    EgbertRijke committed Oct 13, 2024
    Configuration menu
    Copy the full SHA
    70213c1 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' of github.com:UniMath/agda-unimath into globular

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

  5. make pre-commit

    @EgbertRijke
    EgbertRijke committed Oct 13, 2024
    Configuration menu
    Copy the full SHA
    90651f3 View commit details
    Browse the repository at this point in the history

Commits on Oct 14, 2024

  1. working towards duality of directed graphs

    @EgbertRijke
    EgbertRijke committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    0285824 View commit details
    Browse the repository at this point in the history

Commits on Oct 15, 2024

  1. duality for directed graphs

    @EgbertRijke
    EgbertRijke committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    d421336 View commit details
    Browse the repository at this point in the history

  2. fibers and sections

    @EgbertRijke
    EgbertRijke committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    c98f6e2 View commit details
    Browse the repository at this point in the history

  3. wild category of pointed types

    @EgbertRijke
    EgbertRijke committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    cbc1744 View commit details
    Browse the repository at this point in the history

  4. mention the categorical laws, which were duplicated

    @EgbertRijke
    EgbertRijke committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    8c3e39f View commit details
    Browse the repository at this point in the history

  5. small edits

    @EgbertRijke
    EgbertRijke committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    9c4ac74 View commit details
    Browse the repository at this point in the history

Commits on Oct 17, 2024

  1. work

    @EgbertRijke
    EgbertRijke committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    7629b7d View commit details
    Browse the repository at this point in the history

  2. refactor reflexive and transitive globular types

    @EgbertRijke
    EgbertRijke committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    45f2d8b View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2024

  1. lots of work

    @EgbertRijke
    EgbertRijke committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    f445848 View commit details
    Browse the repository at this point in the history

  2. maps

    @EgbertRijke
    EgbertRijke committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    b9ea44a View commit details
    Browse the repository at this point in the history

  3. colax functors of noncoherent wild higher precategories

    @EgbertRijke
    EgbertRijke committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    cab0051 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' of github.com:UniMath/agda-unimath into globular

    @EgbertRijke
    EgbertRijke committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    fe3a463 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' of github.com:UniMath/agda-unimath into globular

    @EgbertRijke
    EgbertRijke committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    b4a6ea7 View commit details
    Browse the repository at this point in the history

  6. work

    @EgbertRijke
    EgbertRijke committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    b16dbd3 View commit details
    Browse the repository at this point in the history

  7. large (co)lax reflexive globular maps

    @EgbertRijke
    EgbertRijke committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    c9f1f92 View commit details
    Browse the repository at this point in the history

  8. variations of transitive globular maps

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

Commits on Oct 21, 2024

  1. refacotr colax functors of noncoherent large wild precategories

    @EgbertRijke
    EgbertRijke committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    d958890 View commit details
    Browse the repository at this point in the history

  2. make pre-commit

    @EgbertRijke
    EgbertRijke committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    f2bec34 View commit details
    Browse the repository at this point in the history

  3. fix concept macros

    @EgbertRijke
    EgbertRijke committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    d019b03 View commit details
    Browse the repository at this point in the history

  4. make pre-commit

    @EgbertRijke
    EgbertRijke committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    66679f5 View commit details
    Browse the repository at this point in the history

  5. reflexive graphs

    @EgbertRijke
    EgbertRijke committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    f340e81 View commit details
    Browse the repository at this point in the history

  6. reflexive graphs

    @EgbertRijke
    EgbertRijke committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    5236141 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' of github.com:UniMath/agda-unimath into globular

    @EgbertRijke
    EgbertRijke committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    7d88972 View commit details
    Browse the repository at this point in the history

  8. make pre-commit

    @EgbertRijke
    EgbertRijke committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    0773c07 View commit details
    Browse the repository at this point in the history

  9. fix bugs

    @EgbertRijke
    EgbertRijke committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    04893a9 View commit details
    Browse the repository at this point in the history

  10. work on broken links

    @EgbertRijke
    EgbertRijke committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    f38ef28 View commit details
    Browse the repository at this point in the history

  11. make pre-commit

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

Commits on Oct 22, 2024

  1. work on reflexive graphs

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

  2. bugs

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

Commits on Oct 23, 2024

  1. work

    @EgbertRijke
    EgbertRijke committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    c12c18d View commit details
    Browse the repository at this point in the history

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

    @EgbertRijke
    EgbertRijke committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    a889dcd View commit details
    Browse the repository at this point in the history

  3. fibers of morphisms of reflexive graphs

    @EgbertRijke
    EgbertRijke committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    6221b38 View commit details
    Browse the repository at this point in the history

  4. make pre-commit

    @EgbertRijke
    EgbertRijke committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    e5ad3f5 View commit details
    Browse the repository at this point in the history

  5. typo

    @EgbertRijke
    EgbertRijke committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    c8b9596 View commit details
    Browse the repository at this point in the history

Commits on Oct 24, 2024

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

    @EgbertRijke
    EgbertRijke committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    7851d96 View commit details
    Browse the repository at this point in the history

  2. dependent products of reflexive graphs

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

  3. minor edit

    @EgbertRijke
    EgbertRijke committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    b39c097 View commit details
    Browse the repository at this point in the history

Commits on Oct 25, 2024

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

    @EgbertRijke
    EgbertRijke committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    077e3a9 View commit details
    Browse the repository at this point in the history

  2. review comments

    @EgbertRijke
    EgbertRijke committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    d1e5448 View commit details
    Browse the repository at this point in the history

  3. base change of universal dependent directed graph

    @EgbertRijke
    EgbertRijke committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    7d1a041 View commit details
    Browse the repository at this point in the history

Commits on Nov 5, 2024

  1. upstream master

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

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

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

  3. some review comments

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

  4. -> laxly

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

  5. review comment

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

  6. typo

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

  7. -> lax

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

  8. concept

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

Commits on Nov 12, 2024

  1. pointwise extensions of families of globular types

    @EgbertRijke
    EgbertRijke committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    a3a945c View commit details
    Browse the repository at this point in the history

  2. file for extensive globular types

    @EgbertRijke
    EgbertRijke committed Nov 12, 2024
    Configuration menu
    Copy the full SHA
    221e5d8 View commit details
    Browse the repository at this point in the history

Commits on Nov 14, 2024

  1. superglobular types

    @EgbertRijke
    EgbertRijke committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    392b591 View commit details
    Browse the repository at this point in the history

  2. superglobular types

    @EgbertRijke
    EgbertRijke committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    d3789b6 View commit details
    Browse the repository at this point in the history

  3. uniform

    @EgbertRijke
    EgbertRijke committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    4626f95 View commit details
    Browse the repository at this point in the history

  4. structure

    @EgbertRijke
    EgbertRijke committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    668bd20 View commit details
    Browse the repository at this point in the history

  5. removing the itemization formatting in record

    @EgbertRijke
    EgbertRijke committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    45a4ea8 View commit details
    Browse the repository at this point in the history

  6. unbolden text with added colon

    @EgbertRijke
    EgbertRijke committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    d5a255b View commit details
    Browse the repository at this point in the history

  7. correcting an incorrect definition of discrete relations

    @EgbertRijke
    EgbertRijke committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    774d2ae View commit details
    Browse the repository at this point in the history

  8. Update src/foundation/discrete-relations.lagda.md 

    Co-authored-by: Fredrik Bakke <[email protected]>
    @EgbertRijke @fredrik-bakke
    EgbertRijke and fredrik-bakke authored Nov 14, 2024
    Configuration menu
    Copy the full SHA
    bf7aab7 View commit details
    Browse the repository at this point in the history

  9. fix broken Agda reference

    @EgbertRijke
    EgbertRijke committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    79b6cf2 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'discrete-graphs' of github.com:EgbertRijke/agda-unimath… 

    … into discrete-graphs
    @EgbertRijke
    EgbertRijke committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    0b304f7 View commit details
    Browse the repository at this point in the history

Commits on Nov 15, 2024

  1. factor out discrete globular types

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    bc2b2be View commit details
    Browse the repository at this point in the history

  2. implementing discreteness via adjointness

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    7d0819d View commit details
    Browse the repository at this point in the history

  3. bugs

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    fdd6436 View commit details
    Browse the repository at this point in the history

  4. bugs

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    cef5ecd View commit details
    Browse the repository at this point in the history

  5. adjointness for discrete directed graphs

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    3189352 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'master' of github.com:UniMath/agda-unimath into globular

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    f123e98 View commit details
    Browse the repository at this point in the history

  7. edit discrete reflexive globular types

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    444251a View commit details
    Browse the repository at this point in the history

  8. discrete globular types

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    8a74a9a View commit details
    Browse the repository at this point in the history

  9. ᵣ to refl

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    84b899d View commit details
    Browse the repository at this point in the history

  10. partially revert long copattern matchings

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    5362869 View commit details
    Browse the repository at this point in the history

  11. make pre-commit

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    58b750e View commit details
    Browse the repository at this point in the history

  12. discrete dependent reflexive graphs

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

  13. make pre-commit

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    01fb7d6 View commit details
    Browse the repository at this point in the history

  14. discrete dependent reflexive globular types

    @EgbertRijke
    EgbertRijke committed Nov 15, 2024
    Configuration menu
    Copy the full SHA
    092b19a View commit details
    Browse the repository at this point in the history

Commits on Nov 16, 2024

  1. adjust text for discrete binary relations

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

  2. make pre-commit

    @EgbertRijke
    EgbertRijke committed Nov 16, 2024
    Configuration menu
    Copy the full SHA
    9cb7cf0 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'discrete-graphs' into globular

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

Commits on Nov 17, 2024

  1. moving files to globular types namespace

    @EgbertRijke
    EgbertRijke committed Nov 17, 2024
    Configuration menu
    Copy the full SHA
    ea117bb View commit details
    Browse the repository at this point in the history

  2. fix imports

    @EgbertRijke
    EgbertRijke committed Nov 17, 2024
    Configuration menu
    Copy the full SHA
    44edc1e View commit details
    Browse the repository at this point in the history

  3. resolve merge conflicts

    @EgbertRijke
    EgbertRijke committed Nov 17, 2024
    Configuration menu
    Copy the full SHA
    bc5b08a View commit details
    Browse the repository at this point in the history

  4. make pre-commit

    @EgbertRijke
    EgbertRijke committed Nov 17, 2024
    Configuration menu
    Copy the full SHA
    ef70c90 View commit details
    Browse the repository at this point in the history

Commits on Nov 20, 2024

  1. resolve merge conflicts

    @EgbertRijke
    EgbertRijke committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    3013c3f View commit details
    Browse the repository at this point in the history

  2. bug

    @EgbertRijke
    EgbertRijke committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    735ea9c View commit details
    Browse the repository at this point in the history

  3. make pre-commit

    @EgbertRijke
    EgbertRijke committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    18b0121 View commit details
    Browse the repository at this point in the history

Commits on Dec 3, 2024

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

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

  2. review

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