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

Flattening lemma for pushouts #764

Merged
merged 9 commits into from
Sep 13, 2023
Merged

Flattening lemma for pushouts #764

merged 9 commits into from
Sep 13, 2023

Conversation

VojtechStep
Copy link
Collaborator

This PR proves the flattening lemma for pushouts, which was previously only stated.

@EgbertRijke
Copy link
Collaborator

A big congratulations!

@VojtechStep
Copy link
Collaborator Author

I'm not sure how I feel about including the odd computations lemmas, since I'm not using them anywhere (they were useful for a previous direction of the proof). The only "important" ones are in function-types.

@EgbertRijke
Copy link
Collaborator

You did a very good job refactoring everything and placing your functions in their natural files. I have certainly no complaints about it.

@EgbertRijke
Copy link
Collaborator

You should update your branch though:)

@VojtechStep
Copy link
Collaborator Author

You should update your branch though:)

I was waiting for the CI to finish at least once, so that it can reuse the cache 😅

@EgbertRijke
Copy link
Collaborator

I created the label "milestone" which can be used to celebrate pull requests that add an important feature to the library.

@fredrik-bakke
Copy link
Collaborator

How is this different from formalization target?

@EgbertRijke
Copy link
Collaborator

Aren't they for issues?

@EgbertRijke
Copy link
Collaborator

I think it feels more celebratory if a maintainer adds "milestone" to a PR than if they add "formalization target" to a PR

@fredrik-bakke
Copy link
Collaborator

It would make sense to use it when a formalization target is achieved as well, no?

@fredrik-bakke
Copy link
Collaborator

Alright, just curious

@EgbertRijke
Copy link
Collaborator

Let me add the "formalization target" label to this PR as well, and then Vojtech can tell us which one made him feel happier 😄

@fredrik-bakke
Copy link
Collaborator

lol

@fredrik-bakke
Copy link
Collaborator

See! That time he responded with a 😄-emoji!

@EgbertRijke
Copy link
Collaborator

Can I also comment that 7 years ago this was the state of the art:

https://github.com/HoTT/HoTT-Agda/blob/master/core/lib/types/Flattening.agda

Vojtech's proof looks very slick in comparison. We've come a long way in understanding how to prove stuff in book hott, as well as how to manage libraries such that these kinds of proofs can be so elegant as Vojtech's. Once more a big congratulations to you, Vojtech!

@VojtechStep
Copy link
Collaborator Author

See, what Egbert doesn't mention is that up until yesterday my proof was a monstrosity until he nudged me into using homotopy induction 🤣

@fredrik-bakke
Copy link
Collaborator

Homotopy induction is definitely nice! I've only just started using it myself too

@EgbertRijke
Copy link
Collaborator

Learn the way you will

@VojtechStep
Copy link
Collaborator Author

And FWIW I think the milestone label is a nice touch, and I'd leave formalization-target to issues 😁

@EgbertRijke EgbertRijke merged commit 413a1bf into UniMath:master Sep 13, 2023
4 checks passed
@VojtechStep
Copy link
Collaborator Author

Woohoo 🎉

fredrik-bakke pushed a commit to fredrik-bakke/agda-unimath that referenced this pull request Sep 21, 2023
@VojtechStep @fredrik-bakke
Flattening lemma for pushouts (UniMath#764)
2dd6865
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Sep 21, 2023
@fredrik-bakke
Squashed commit of the following:
a6b6523 
commit 6f8fdc1
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 23:22:39 2023 +0200

    hom-types are homs

commit d7cffc3
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 23:10:50 2023 +0200

    `is-set-hom`

commit 3a646ce
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 22:53:24 2023 +0200

    fix hom-set function categories

commit 3bfc7dd
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 22:49:08 2023 +0200

    rename hom-sets to `hom-set`

commit fd15e21
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 21:42:14 2023 +0200

    some comments

commit a95c86c
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Thu Sep 21 12:59:34 2023 +0200

    The classification of cyclic rings (UniMath#757)

    Co-authored-by: izak <gregapercic000@gmail.com>

commit df1e6e6
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 14:20:56 2023 +0200

    consistencies

commit 04cf136
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 14:14:52 2023 +0200

    add projections initial and terminal objects

commit 2ac83c1
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 12:42:50 2023 +0200

    Functors _between_ large...

commit 5577dbb
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 12:33:03 2023 +0200

    functors _between_ categories

commit 786664f
Merge: e0f6858 da7e412
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 12:26:28 2023 +0200

    Merge branch 'master' into functor-categories

commit e0f6858
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 02:08:26 2023 +0200

    pre-commit

commit 3933794
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 02:06:48 2023 +0200

    the functor category and natural isomorphisms

commit da7e412
Author: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
Date:   Wed Sep 20 19:01:16 2023 +0200

    Coforks, coequalizers of types, their flattening lemma (UniMath#792)

    This PR introduces coforks of parallel maps, the dependent and
    non-dependent universal properties of coequalizers, the construction of
    coequalizers from pushouts, and the flattening lemma for coequalizers,
    asserting that sigmas commute with coequalizers.

    This development mirrors the development of cocones and pushouts.

    I also changed the statement of the flattening lemma for pushouts to one
    that sounds more natural to me - we can construct a cocone of sigma
    types from any cocone, not just a pushout; the previous definition
    required the vertex to be a pushout in those definitions. Now the
    statement is "if a cocone is a pushout, then the cocone derived from it
    is a pushout too".

commit d9a8a02
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Wed Sep 20 03:07:19 2023 +0200

    refactor isomorphisms in small (pre-)categories

commit f47cf60
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Wed Sep 20 00:54:35 2023 +0200

    `is-iso` to `is-iso-hom`

commit 7955721
Merge: d1a36f7 eda7bb2
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Wed Sep 20 00:31:31 2023 +0200

    Merge remote-tracking branch 'agda-unimath/master' into functor-categories

commit d1a36f7
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Wed Sep 20 00:29:10 2023 +0200

    preliminary extensionality of functors

commit 30bfd00
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 15:30:00 2023 +0200

    split up definition `functor-precategory-Precategory`

commit 3e22d2a
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 15:14:06 2023 +0200

    a little refactoring of natural transformations

commit a9f5f27
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 15:13:08 2023 +0200

    Use `C` instead of `P` dependent products of precategories

commit eda7bb2
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Tue Sep 19 22:01:57 2023 +0200

    Isomorphisms in large categories and large precategories (UniMath#791)

commit cdc008d
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Tue Sep 19 13:19:50 2023 +0200

    Add a dot after the sentence "Content created by..." (UniMath#790)

commit a081293
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Tue Sep 19 13:01:42 2023 +0200

    Add the universal property of identity systems to the overview tables (UniMath#789)

commit fec9c63
Merge: 65483f6 9d2c235
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 02:26:31 2023 +0200

    Merge branch 'master' into functor-categories

commit 65483f6
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 02:25:24 2023 +0200

    `comp-natural-transformation-Large-Precategory` and associated refactoring

commit 9c166ae
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 00:05:11 2023 +0200

    pre-commit

commit 08af608
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 00:00:34 2023 +0200

    prepend `map-` to `(obj/hom)-functor`

commit 43ee8e8
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 23:47:47 2023 +0200

    small fixes

commit 51ec628
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 23:21:34 2023 +0200

    misc cleanup natural transformations

commit 8e6f821
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 23:19:43 2023 +0200

    define representing arrow category

commit 9d2c235
Author: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
Date:   Mon Sep 18 15:52:57 2023 +0200

    Fix website CI (UniMath#786)

commit 1bea263
Author: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
Date:   Mon Sep 18 09:52:52 2023 +0200

    Always enable git metadata, fetch whole git history in pages CI (UniMath#785)

commit b1f027f
Author: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
Date:   Mon Sep 18 03:25:35 2023 +0200

    Try to fix website CI (UniMath#784)

commit 6af959b
Author: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
Date:   Mon Sep 18 03:01:42 2023 +0200

    Automatically extract page contributor information during web build (UniMath#770)

commit b66c539
Merge: 47f04e3 539174a
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 01:19:20 2023 +0200

    Merge branch 'UniMath:master' into functor-categories

commit 47f04e3
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 01:18:42 2023 +0200

    links functors between categories

commit 539174a
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 00:39:14 2023 +0200

    Yoneda's lemma for categories (UniMath#783)

commit 0106784
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Sun Sep 17 18:05:43 2023 +0200

    Moving file about hexagons of identifications (UniMath#782)

commit b804ea5
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Sun Sep 17 11:45:44 2023 +0200

    Update README.md (UniMath#781)

commit f7d6658
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Sun Sep 17 11:24:59 2023 +0200

    Update README.md (UniMath#780)

commit f4f4ef2
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Sun Sep 17 11:13:37 2023 +0200

    Update README.md (UniMath#779)

commit 6df85b4
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Sun Sep 17 11:08:03 2023 +0200

    Fancy title on repo page (UniMath#778)

commit 1fb5dc5
Author: maybemabeline <142519092+maybemabeline@users.noreply.github.com>
Date:   Sat Sep 16 22:32:19 2023 +0200

    Equivalence between the first sphere and the circle (UniMath#776)

    Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>

commit 1fe0803
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Fri Sep 15 16:18:37 2023 +0200

    Define representations of monoids (UniMath#765)

commit c813a06
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Fri Sep 15 15:17:44 2023 +0200

    larger image, rounded corners (UniMath#774)

commit 0529896
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Fri Sep 15 13:23:30 2023 +0200

    update contributors (UniMath#773)

commit 5340335
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Fri Sep 15 10:58:02 2023 +0200

    update contributors, remove unused imports (UniMath#772)

commit 533cff1
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Fri Sep 15 01:08:32 2023 +0200

    Adding an art page (UniMath#771)

    Co-authored-by: Andrej Bauer <andrej.bauer@andrej.com>
    Co-authored-by: Matej Petković <Petkomat@users.noreply.github.com>

commit adf864e
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Thu Sep 14 16:44:32 2023 +0200

    Symmetric core of a relation (UniMath#754)

    In this PR we construct the symmetric core of a type valued relation and
    show that it is the right adjoint of the restriction functor from
    symmetric relations to relations. Everything we do in this PR is fully
    coherent and untruncated.

    ---------

    Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

commit 50fdf54
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Wed Sep 13 19:11:14 2023 +0200

    The one-object precategory of a monoid (UniMath#766)

commit 413a1bf
Author: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
Date:   Wed Sep 13 18:35:55 2023 +0200

    Flattening lemma for pushouts (UniMath#764)

commit d826323
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Wed Sep 13 17:00:53 2023 +0200

    rational commutative monoids (UniMath#763)

    This small PR factors out rational commutative monoids from UniMath#623.

    ---------

    Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@EgbertRijke EgbertRijke EgbertRijke left review comments

@fredrik-bakke fredrik-bakke fredrik-bakke approved these changes

Assignees
No one assigned
Labels
foundation 🏆 milestone 🏆 synthetic-homotopy-theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@VojtechStep @EgbertRijke @fredrik-bakke