update contributors, remove unused imports #772
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Note that we're currently not including co-authors of commits on our contributors page. This seems to be an oversight. |
EgbertRijke
commented
Sep 15, 2023
fredrik-bakke
pushed a commit
to fredrik-bakke/agda-unimath
that referenced
this pull request
Sep 21, 2023
fredrik-bakke
added a commit
to fredrik-bakke/agda-unimath
that referenced
this pull request
Sep 21, 2023
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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.