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 properties of lifts of families out of 26-descent #988

Merged
merged 18 commits into from
Jan 27, 2024
Merged

Refactor properties of lifts of families out of 26-descent #988

merged 18 commits into from
Jan 27, 2024

Commits on Jan 27, 2024

  1. WIP Refactor proof of dependent-pullback-property↔pullback-property 

    Mostly moves stuff out of 26-descent to more appropriate locations
    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    299019d View commit details
    Browse the repository at this point in the history

  2. dependent-universal-property-pushout↔universal-property-pushout

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    a90579a View commit details
    Browse the repository at this point in the history

  3. Prose for htpy-htpy-map-Σ

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    5f4f0a6 View commit details
    Browse the repository at this point in the history

  4. Prose for tr-precomp-family

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    f1d53e8 View commit details
    Browse the repository at this point in the history

  5. Prose for the naming "lifts" of elements

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    475fde9 View commit details
    Browse the repository at this point in the history

  6. "total space of lifts of families" -> "lifted families"

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    1e6cea5 View commit details
    Browse the repository at this point in the history

  7. Prose for tr-lift-family-of-elements-precomp

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    6e8bce2 View commit details
    Browse the repository at this point in the history

  8. Intro to precomposition of lifts of families of elements

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    8d7d3af View commit details
    Browse the repository at this point in the history

  9. Prose for dependent-pullback-property↔pullback-property

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    f240793 View commit details
    Browse the repository at this point in the history

  10. Prose for coherence-square-precomp-map-inv-distributive-Π-Σ

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    963ca2c View commit details
    Browse the repository at this point in the history

  11. Prose for `coherence-htpy-precomp-coherence-square-precomp-map-inv-di… 

    …stributive-Π-Σ`
    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    30b91a8 View commit details
    Browse the repository at this point in the history

  12. Fix typos

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    9ac77a9 View commit details
    Browse the repository at this point in the history

  13. Prose for coherence-triangle-precomp-lift-family-of-elements

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    b4d1236 View commit details
    Browse the repository at this point in the history

  14. Remove commented code

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    9db3c4b View commit details
    Browse the repository at this point in the history

  15. Table for equivalent conditions for being a pushout

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    b2a209f View commit details
    Browse the repository at this point in the history

  16. Make a diagram less ambiguous

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    d887713 View commit details
    Browse the repository at this point in the history

  17. Prose fixes

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    8d480b7 View commit details
    Browse the repository at this point in the history

  18. Review suggestions

    @VojtechStep
    VojtechStep committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    5741aae View commit details
    Browse the repository at this point in the history