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

Simplicial Type Theory #1118

Draft
wants to merge 105 commits into
base: master
Choose a base branch
from
Draft

Simplicial Type Theory #1118

wants to merge 105 commits into from

Commits on Apr 17, 2024

  1. the directed interval type

    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    eb9f3e6 View commit details
    Browse the repository at this point in the history

  2. The directed relation on the directed interval type

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

  3. standard simplicial cubes

    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    db3b59a View commit details
    Browse the repository at this point in the history

  4. Simplicial arrows

    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    c6b8d8e View commit details
    Browse the repository at this point in the history

  5. simplicial edges

    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    db2f1bb View commit details
    Browse the repository at this point in the history

  6. _→₂_ notation simplicial edges

    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    692f30a View commit details
    Browse the repository at this point in the history

  7. The action on simplicial edges of functions

    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    146189d View commit details
    Browse the repository at this point in the history

  8. Simplicial natural transformations

    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    cbb0a42 View commit details
    Browse the repository at this point in the history

  9. The canonical inclusion of the booleans into the directed interval is… 

    … an embedding
    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    cda98ba View commit details
    Browse the repository at this point in the history

  10. Horizontal composition of simplicial arrows of functions

    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    ecd606e View commit details
    Browse the repository at this point in the history

  11. Horizontal composition of simplicial edges between functions

    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    1c71fe4 View commit details
    Browse the repository at this point in the history

  12. Whiskering operations on simplicial arrows of functions

    @fredrik-bakke
    fredrik-bakke committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    b4ac7e4 View commit details
    Browse the repository at this point in the history

Commits on Apr 18, 2024

  1. Whiskering operations on simplicial edges between functions

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

  2. inline (leq|Id)-2-Prop

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

  3. The boundary of the standard simplicial cube

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

  4. WIP 2-simplices

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

  5. comma types

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

Commits on Apr 19, 2024

  1. Merge branch 'master' into simplicial-type-theory

    @fredrik-bakke
    fredrik-bakke authored Apr 19, 2024
    Configuration menu
    Copy the full SHA
    e7c473a View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2024

  1. action on simplicial edges of dependent functions

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

  2. some work

    @fredrik-bakke
    fredrik-bakke committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    a64843d View commit details
    Browse the repository at this point in the history

  3. dependent simplicial edges

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

  4. Characterizing equality of dependent simplicial edges over a fixed edge

    @fredrik-bakke
    fredrik-bakke committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    938888e View commit details
    Browse the repository at this point in the history

Commits on Apr 23, 2024

  1. free directed loops

    @fredrik-bakke
    fredrik-bakke committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    c373277 View commit details
    Browse the repository at this point in the history

  2. The universal property of the directed circle

    @fredrik-bakke
    fredrik-bakke committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    0ce1e43 View commit details
    Browse the repository at this point in the history

  3. the directed circle

    @fredrik-bakke
    fredrik-bakke committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    897cf05 View commit details
    Browse the repository at this point in the history

  4. rewritinf rules for the directed circle

    @fredrik-bakke
    fredrik-bakke committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    df77481 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into simplicial-type-theory

    @fredrik-bakke
    fredrik-bakke authored Apr 23, 2024
    Configuration menu
    Copy the full SHA
    866ff56 View commit details
    Browse the repository at this point in the history

  6. fix links

    @fredrik-bakke
    fredrik-bakke committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    c3c1464 View commit details
    Browse the repository at this point in the history

  7. negated equality universal-cover-circle

    @fredrik-bakke
    fredrik-bakke committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    a43ed06 View commit details
    Browse the repository at this point in the history

  8. pre-commit

    @fredrik-bakke
    fredrik-bakke committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    8084b1d View commit details
    Browse the repository at this point in the history

  9. The loop of the circle is nontrivial

    @fredrik-bakke
    fredrik-bakke committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    fc9641e View commit details
    Browse the repository at this point in the history

Commits on Apr 24, 2024

  1. simplicially discrete types

    @fredrik-bakke
    fredrik-bakke committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    0f14dc1 View commit details
    Browse the repository at this point in the history

  2. a space

    @fredrik-bakke
    fredrik-bakke committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    997c85f View commit details
    Browse the repository at this point in the history

Commits on Apr 25, 2024

  1. duality postcomposition pullbacks <-> pullback property pushouts

    @fredrik-bakke
    fredrik-bakke committed Apr 25, 2024
    Configuration menu
    Copy the full SHA
    92e41f2 View commit details
    Browse the repository at this point in the history

  2. Simplicial mapping cylinders

    @fredrik-bakke
    fredrik-bakke committed Apr 25, 2024
    Configuration menu
    Copy the full SHA
    804d5fa View commit details
    Browse the repository at this point in the history

  3. nit foundation

    @fredrik-bakke
    fredrik-bakke committed Apr 25, 2024
    Configuration menu
    Copy the full SHA
    0202ce2 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into simplicial-type-theory

    @fredrik-bakke
    fredrik-bakke authored Apr 25, 2024
    Configuration menu
    Copy the full SHA
    16759ec View commit details
    Browse the repository at this point in the history

Commits on Apr 29, 2024

  1. fixes pushout-products

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    ff4d2da View commit details
    Browse the repository at this point in the history

  2. propositions are local at inhabited types

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    9582b53 View commit details
    Browse the repository at this point in the history

  3. todos orthogonal maps

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    0b31700 View commit details
    Browse the repository at this point in the history

  4. Constant free directed loops

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    e91338a View commit details
    Browse the repository at this point in the history

  5. standard simplicial joins

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    9f1dcd1 View commit details
    Browse the repository at this point in the history

  6. wip directed circle

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

  7. the representing arrow and directed edge

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

  8. informal definition simplicial suspension

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

  9. small fixes comma types

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    09a0edf View commit details
    Browse the repository at this point in the history

  10. two easy examples of simplicially discrete types

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    d1dd5a5 View commit details
    Browse the repository at this point in the history

  11. simplicial cones

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    750c2c8 View commit details
    Browse the repository at this point in the history

  12. informal definition simplicial spine

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    aa47a4e View commit details
    Browse the repository at this point in the history

  13. Merge branch 'master' into simplicial-type-theory

    @fredrik-bakke
    fredrik-bakke authored Apr 29, 2024
    Configuration menu
    Copy the full SHA
    e9c3c2a View commit details
    Browse the repository at this point in the history

  14. rename directed relation module

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    20380d0 View commit details
    Browse the repository at this point in the history

  15. "simplicial edge" -> "directed edge"

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    59d064d View commit details
    Browse the repository at this point in the history

  16. pre-commit

    @fredrik-bakke
    fredrik-bakke committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    679ca2e View commit details
    Browse the repository at this point in the history

  17. add reference RS17

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

Commits on Apr 30, 2024

  1. small fixes

    @fredrik-bakke
    fredrik-bakke committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    cd2cce9 View commit details
    Browse the repository at this point in the history

Commits on May 1, 2024

  1. simplicially covariant type families

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

Commits on May 2, 2024

  1. the directed interval is not 0-connected

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

  2. strengthen The directed interval is not connected

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

  3. strengthen The directed interval is not connected

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

Commits on May 6, 2024

  1. max and min operators on directed interval

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

  2. prose fixes erasing-equality

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

  3. add --confluence-check flag

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

  4. fix rewriting-directed-circle

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

  5. fix rewriting-directed-circle

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

Commits on May 21, 2024

  1. some nicer type setting

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

Commits on Jun 1, 2024

  1. define Simplicially fully-faithful maps

    @fredrik-bakke
    fredrik-bakke committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    edb5321 View commit details
    Browse the repository at this point in the history

Commits on Jun 3, 2024

  1. add reference MR23b

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

  2. some work on logic

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

  3. more characterizations of directed edges

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

  4. two corollaries for simplicially discrete types

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

  5. pre-commit

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

  6. detailed analysis of the image factorization of bool -> 𝟚

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

  7. globularly coskeletal types

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

  8. a remark on standard simplices

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

  9. incomplete proof loop of directed circle is nontrivial

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

  10. line wrap

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

  11. rename relation to inequality directed interval type

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

  12. wip simplicial spines

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

  13. wip directed edges in the booleans

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

  14. Merge branch 'master' into simplicial-type-theory

    @fredrik-bakke
    fredrik-bakke authored Jun 3, 2024
    Configuration menu
    Copy the full SHA
    025ef51 View commit details
    Browse the repository at this point in the history

  15. null types are closed under Pi, exponentials, products and Sigma

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

  16. simplicially discrete types are closed under Pi, exponentials, produc… 

    …ts and Sigma
    @fredrik-bakke
    fredrik-bakke committed Jun 3, 2024
    Configuration menu
    Copy the full SHA
    7600f0e View commit details
    Browse the repository at this point in the history

Commits on Jun 4, 2024

  1. is-orthogonal-htpy

    @fredrik-bakke
    fredrik-bakke committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    10930ef View commit details
    Browse the repository at this point in the history

  2. The canonical projection from a coproduct to the booleans

    @fredrik-bakke
    fredrik-bakke committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    fb4ef17 View commit details
    Browse the repository at this point in the history

  3. closure properties of null maps

    @fredrik-bakke
    fredrik-bakke committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    d3fec69 View commit details
    Browse the repository at this point in the history

  4. a remark on null types

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

  5. A family over a simplicially discrete type is a family of simpliciall… 

    …y discrete types if and only if the dependent sum is
    @fredrik-bakke
    fredrik-bakke committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    51536e0 View commit details
    Browse the repository at this point in the history

  6. characterizing directed edges in the booleans

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

  7. some fixes

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

  8. rename coskeletal to globularly coskeletal

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

  9. factor out coproducts of null types

    @fredrik-bakke
    fredrik-bakke committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    cfcf354 View commit details
    Browse the repository at this point in the history

  10. The hom-types of a truncated type are truncated

    @fredrik-bakke
    fredrik-bakke committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    c8571f1 View commit details
    Browse the repository at this point in the history

Commits on Jun 5, 2024

  1. work

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

Commits on Jun 12, 2024

  1. idk

    @fredrik-bakke
    fredrik-bakke committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    406223f View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2024

  1. wip stt

    @fredrik-bakke
    fredrik-bakke committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    913e3dd View commit details
    Browse the repository at this point in the history

Commits on Sep 18, 2024

  1. Base change of sections

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

Commits on Sep 19, 2024

  1. informal proof Retracts of transposing adjunctions

    @fredrik-bakke
    fredrik-bakke committed Sep 19, 2024
    Configuration menu
    Copy the full SHA
    87a679f View commit details
    Browse the repository at this point in the history

  2. delete irrelevant code transposing adjunctions

    @fredrik-bakke
    fredrik-bakke committed Sep 19, 2024
    Configuration menu
    Copy the full SHA
    4b5c48d View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2024

  1. more stuff transposing adjunctions

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

Commits on Oct 3, 2024

  1. typo horizontal comp directed edges functions

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

  2. change notation natural transformations

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

  3. horizontal composition natural transformations

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

  4. additions adjunctions

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

  5. late onset pre-commit

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

  6. wip normed maps

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