{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":429926544,"defaultBranch":"master","name":"agda-unimath","ownerLogin":"UniMath","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-11-19T20:31:01.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/6826454?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1710096262.0","currentOid":""},"activityList":{"items":[{"before":"270c39f802bb63942c285064e92bc167445f0eb6","after":"4ddb39bee5e608596eaf0573ab33685caca466bd","ref":"refs/heads/master","pushedAt":"2024-06-05T14:39:07.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"EgbertRijke","name":"Egbert Rijke","path":"/EgbertRijke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1252282?s=80&v=4"},"commit":{"message":"Overview of SvDR20 formalization (#1144)\n\nI'm opening this so we can discuss how to write expositions to\r\n(partially) formalized papers in the library. Relevant to #1055","shortMessageHtmlLink":"Overview of SvDR20 formalization (#1144)"}},{"before":"dafc57adfaf30facce8185f15d505d103361a881","after":"270c39f802bb63942c285064e92bc167445f0eb6","ref":"refs/heads/master","pushedAt":"2024-06-05T14:19:29.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"EgbertRijke","name":"Egbert Rijke","path":"/EgbertRijke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1252282?s=80&v=4"},"commit":{"message":"Path-cosplit maps (#1153)\n\nA (mere) `k`-path-cosplit map is defined inductively\r\n- A (mere) `-2`-path-cosplit map is a map that is (merely) a retract\r\n- A (mere) `k+1`-path-cosplit map is a map whose action on\r\nidentifications is (merely) `k`-path-cosplit.\r\n\r\nWe show\r\n- Mere `k`-path-cosplitting is a property\r\n- `k`-truncated maps are `k`-path-cosplit\r\n- (merely) `k`-path-cosplit maps are (merely) `k+1`-path-cosplit\r\n- types that map into `k`-truncated types via (mere) `k`-path-cosplit\r\nmaps are `k`-truncated\r\n- (mere) `k`-path-cosplit maps into `k`-truncated types are\r\n`k`-truncated.","shortMessageHtmlLink":"Path-cosplit maps (#1153)"}},{"before":"b4aac3cdf6f7f3e23b7503fea13dc0375c529e4f","after":"dafc57adfaf30facce8185f15d505d103361a881","ref":"refs/heads/master","pushedAt":"2024-06-05T13:38:36.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"EgbertRijke","name":"Egbert Rijke","path":"/EgbertRijke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1252282?s=80&v=4"},"commit":{"message":"Characterization of various families over pushouts (#1148)\n\nThis PR characterizes (as in \"provides the expected descent data and\r\nshows equivalence\") the following type families over pushouts:\r\n- families of function types, `x ↦ P x → Q x`\r\n- families of equivalence types, `x ↦ P x ≃ Q x`\r\n- families of based identity types at `x₀ : X`, `x ↦ x₀ = x`\r\n\r\nIt also introduces sections of descent data, which correspond to\r\nsections of the associated type family","shortMessageHtmlLink":"Characterization of various families over pushouts (#1148)"}},{"before":"8ad6a6a799c7b471c291db12e459aff48b1ef652","after":"b4aac3cdf6f7f3e23b7503fea13dc0375c529e4f","ref":"refs/heads/master","pushedAt":"2024-06-04T15:11:37.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"EgbertRijke","name":"Egbert Rijke","path":"/EgbertRijke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1252282?s=80&v=4"},"commit":{"message":"Fiberwise orthogonal maps and closure properties of the right class (#1152)\n\nThis is the replacement for #1032.","shortMessageHtmlLink":"Fiberwise orthogonal maps and closure properties of the right class (#…"}},{"before":"3d161cc8220fedaa93fea09ae6c5abfe0328cdbc","after":"8ad6a6a799c7b471c291db12e459aff48b1ef652","ref":"refs/heads/master","pushedAt":"2024-06-04T14:42:36.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"EgbertRijke","name":"Egbert Rijke","path":"/EgbertRijke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1252282?s=80&v=4"},"commit":{"message":"Quasiidempotence is not a proposition (#1127)\n\nFollow-up to #1105.","shortMessageHtmlLink":"Quasiidempotence is not a proposition (#1127)"}},{"before":"6e41d5c00566099953f5a202e57e29b3f19546d6","after":"3d161cc8220fedaa93fea09ae6c5abfe0328cdbc","ref":"refs/heads/master","pushedAt":"2024-06-03T12:45:11.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"Change equiv-comp to comp-equiv (#1151)\n\nThe name `equiv-comp` was not in accordance with our general naming\r\nscheme for compositions of maps, where often we name `comp` first, and\r\nthen the kind of morphism that the composition operation acts on.","shortMessageHtmlLink":"Change equiv-comp to comp-equiv (#1151)"}},{"before":"7ed6b794680e805dfe831dfead71e8171b7aa251","after":"6e41d5c00566099953f5a202e57e29b3f19546d6","ref":"refs/heads/master","pushedAt":"2024-06-01T16:04:31.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"Characterize identity types of dependent sequential diagrams (#1149)\n\nEquivalences of dependent sequential diagrams characterize their\r\nidentity type","shortMessageHtmlLink":"Characterize identity types of dependent sequential diagrams (#1149)"}},{"before":"a57380f9f6ac6c4f320ae202e93eacdb530cdc26","after":"7ed6b794680e805dfe831dfead71e8171b7aa251","ref":"refs/heads/master","pushedAt":"2024-05-31T08:40:09.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"EgbertRijke","name":"Egbert Rijke","path":"/EgbertRijke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1252282?s=80&v=4"},"commit":{"message":"Refactor the descent property of pushouts (#1145)\n\nThe module `26-descent` is replaced with a collection of files written\r\nin the \"new\" style, defining descent data, morphisms and equivalences,\r\nand showing the descent property.\r\n\r\nThere is currently some duplication with the development in\r\n`26-id-pushout`, where I tried to make the absolute minimum changes\r\nrequired for it to typecheck, since I'll be replacing the entire file in\r\nan upcoming PR.","shortMessageHtmlLink":"Refactor the descent property of pushouts (#1145)"}},{"before":"78e562e9221f915adc0c864b61af6b58be94a2a9","after":"a57380f9f6ac6c4f320ae202e93eacdb530cdc26","ref":"refs/heads/master","pushedAt":"2024-05-23T16:02:34.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Zigzags of sequential diagrams (#1129)\n\nIn this PR I\r\n- compute the maps induced by functoriality on inclusion morphisms of\r\nshifts of sequential diagrams\r\n- define zigzags between sequential diagrams\r\n- show that both maps of colimits induced by a zigzag are equivalences","shortMessageHtmlLink":"Zigzags of sequential diagrams (#1129)"}},{"before":"20508c14ce56a5195e148bfe8b49ab0e1e35dcaf","after":"78e562e9221f915adc0c864b61af6b58be94a2a9","ref":"refs/heads/master","pushedAt":"2024-05-23T15:46:24.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Fix citation tag configuration for some references (#1143)\n\nFixes and simplifies some citation label configuration. It turns out the\r\nsystem is capable of handling edge cases for capitalization in names,\r\nsuch as \"de Jong, Tom\" without further input from us.","shortMessageHtmlLink":"Fix citation tag configuration for some references (#1143)"}},{"before":"b2a9814757623d2f4ce9476ba3ea2e6af6ed1793","after":"20508c14ce56a5195e148bfe8b49ab0e1e35dcaf","ref":"refs/heads/master","pushedAt":"2024-05-23T15:19:23.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"EgbertRijke","name":"Egbert Rijke","path":"/EgbertRijke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1252282?s=80&v=4"},"commit":{"message":"Add reference to MRR88 in files about apartness relations (#1128)","shortMessageHtmlLink":"Add reference to MRR88 in files about apartness relations (#1128)"}},{"before":"09efc0f40ddf53f243ea2c7e7b743b195a6797c4","after":"b2a9814757623d2f4ce9476ba3ea2e6af6ed1793","ref":"refs/heads/master","pushedAt":"2024-05-23T14:56:50.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"Null maps, null types and null type families (#1088)\n\nDefines `Y`-null maps, `Y`-null types and `Y`-null type families, and\r\nestablishes a few basic properties of these. Also formalizes the fiber\r\ncondition for orthogonal maps. Part of #930. Depends on #1086.\r\n\r\n- If `A` is a retract of `B` and `S` is a retract of `T` then\r\n`diagonal-exponential A S` is a retract of `diagonal-exponential B T`.\r\n- Null types\r\n - Null types are closed under equivalences in the base and exponent\r\n - Null types are closed under retracts in the base and exponent\r\n- A type is `Y`-null if and only if the terminal projection of `Y` is\r\northogonal to the terminal projection of `A`\r\n- Null families\r\n- Null families are closed under equivalences in the family and exponent\r\n - Null families are closed under retracts in the family and exponent\r\n- Null maps, equivalence of\r\n - Fiber condition\r\n - Pullback condition\r\n - Right orthogonal map to terminal projection condition\r\n - Local at terminal projection condition\r\n- Fiber condition for orthogonal maps","shortMessageHtmlLink":"Null maps, null types and null type families (#1088)"}},{"before":"2f512986366e93998a60eb745c64023e54b6b43e","after":"09efc0f40ddf53f243ea2c7e7b743b195a6797c4","ref":"refs/heads/master","pushedAt":"2024-04-30T15:10:17.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"Fixing a link (#1135)\n\nJust fixing a link :)","shortMessageHtmlLink":"Fixing a link (#1135)"}},{"before":"83e59f9b35fc7a32de017c671a6ee70ed3c6a895","after":"2f512986366e93998a60eb745c64023e54b6b43e","ref":"refs/heads/master","pushedAt":"2024-04-27T18:33:00.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Pin macOS version to one with Intel runners (#1131)\n\nThe `macOS-latest` runners are now macOS 14, and GitHub only provides\narm64 machines for those. The setup-agda action doesn't have prebuilt\nbinaries of Agda for that, so I'm pinning the macos version to 13.\n\nI also switched the website deployment workflow to run on Ubuntu instead\nof macos, since the Linux runners are consistently faster for us.","shortMessageHtmlLink":"Pin macOS version to one with Intel runners (#1131)"}},{"before":"54becd83181c32370687901e47c2da268de3ed8a","after":"83e59f9b35fc7a32de017c671a6ee70ed3c6a895","ref":"refs/heads/master","pushedAt":"2024-04-25T21:25:43.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"The discrete field of rational numbers (#1111)\n\nThe main goal of this pull request is to introduce the discrete field\r\nstructure on the rational numbers.\r\nIn order to do so, we introduce a few basic results in elementary number\r\ntheory and ring theory.\r\n\r\n### Elementary number theory\r\n- strict inequality on the rational numbers is invariant by translation;\r\n- the multiplicative monoid of rational numbers;\r\n- the nonzero rational numbers:\r\n - standard definition via `is-nonzero-ℚ`;\r\n - basic properties;\r\n - nonzero rational numbers are a multiplicative submonoid;\r\n- the positive integer fractions:\r\n - fractions with positive numerator;\r\n - basic properties;\r\n- positive integer fractions are invertible up to the similarity\r\nrelation;\r\n- the positive rational numbers:\r\n- rational numbers with positive underlying fractions, or, equivalently,\r\nwith positive numerator;\r\n - basic properties and notations;\r\n - positive rational numbers are an additive subsemigroup;\r\n - positive rational numbers are a multiplicative submonoid;\r\n - positive rational numbers are invertible;\r\n- the multiplicative group of positive rational numbers;\r\n- the ring of rational numbers is a division ring;\r\n- the discrete field of the rational numbers;\r\n- the multiplicative group of rational numbers:\r\n - the group of units of the ring of rational numbers;\r\n - basic properties and notations.\r\n### Ring theory\r\n- invertible elements of rings are stable under negatives;\r\n- invertible elements of nontrivial rings are nonzero.\r\n\r\n---------\r\n\r\nCo-authored-by: Fredrik Bakke ","shortMessageHtmlLink":"The discrete field of rational numbers (#1111)"}},{"before":"aa95b6e29ad252904e9e6e33f6ca82985822428c","after":"54becd83181c32370687901e47c2da268de3ed8a","ref":"refs/heads/master","pushedAt":"2024-04-25T13:26:36.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Postulate components of coherent two-sided inverses for function extensionality and univalence (#1119)\n\nChanges the postulates for funext and univalence such that there is\r\njudgmentally only one converse map to `htpy-eq` and `equiv-eq`. The main\r\nbenefit, however, is that now `eq-htpy` and `eq-equiv` will appear with\r\ntheir own names in Agda interactive mode, rather than as `pr1 (pr1\r\n(funext ... ...))` and `pr1 (pr1 (univalence ... ...))`.\r\n\r\nI leave it for potential future work to prove\r\n`is-retraction-eq-(equiv|htpy)'` and `coh-eq-(equiv|htpy)'` rather than\r\npostulate them, **_if_** we want this. Note that we could get away with\r\neven fewer postulates if we really wanted to (see\r\n[`TypeTopology/UF.Lower-FunExt`](https://www.cs.bham.ac.uk/~mhe/TypeTopology/UF.Lower-FunExt.html)).","shortMessageHtmlLink":"Postulate components of coherent two-sided inverses for function exte…"}},{"before":"de858a17ed5ced08a5249d6d31c658786e05f9d0","after":"aa95b6e29ad252904e9e6e33f6ca82985822428c","ref":"refs/heads/master","pushedAt":"2024-04-25T12:48:48.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"chore: Fix arrowheads in character diagrams (#1124)\n\nReplaces capital and lower-case `V` arrowheads in character diagrams\r\nwith the logical or character `∨`, and the caret arrowheads `^` with\r\nlogical and `∧`. Also fixes a couple of miscellaneous issues with some\r\ndiagrams like lacking indentation and whitespace.","shortMessageHtmlLink":"chore: Fix arrowheads in character diagrams (#1124)"}},{"before":"f095d75f52c0e31f27a8edae9f93d5333d3e431c","after":"de858a17ed5ced08a5249d6d31c658786e05f9d0","ref":"refs/heads/master","pushedAt":"2024-04-25T12:23:06.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"chore: Universal properties of colimits quantify over all universe levels (#1126)\n\nRefactors all universal properties and induction principles of colimits\r\nto quantify over all universe levels. This still leaves some lemmas\r\nabout pushout cocones in an awkward position, but I leave that for\r\nfuture work.","shortMessageHtmlLink":"chore: Universal properties of colimits quantify over all universe le…"}},{"before":"b9cf8449a5f45884387d9fe73c6f2bbd4a03f78f","after":"f095d75f52c0e31f27a8edae9f93d5333d3e431c","ref":"refs/heads/master","pushedAt":"2024-04-23T14:46:55.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"The loop of any circle is nontrivial (#1115)\n\nThis PR shows that the loop on any circle is nontrivial. I also changed\r\n\"fundamental cover\" to \"universal cover\" because that seemed to be the\r\nconventional name.","shortMessageHtmlLink":"The loop of any circle is nontrivial (#1115)"}},{"before":"cebf28ee740928fd88f0b096a013cc26aafe752c","after":"b9cf8449a5f45884387d9fe73c6f2bbd4a03f78f","ref":"refs/heads/master","pushedAt":"2024-04-20T19:51:08.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"chore: Remove redundant parentheses in universe level expressions (#1125)","shortMessageHtmlLink":"chore: Remove redundant parentheses in universe level expressions (#1125"}},{"before":"378ff01d1161241af7544a2ddb92aeacddd24db4","after":"cebf28ee740928fd88f0b096a013cc26aafe752c","ref":"refs/heads/master","pushedAt":"2024-04-20T07:25:48.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Rename `canonical-coequalizer` to `standard-coequalizer` (#1121)\n\nMakes the naming consistent with every other standard (co)limit.","shortMessageHtmlLink":"Rename canonical-coequalizer to standard-coequalizer (#1121)"}},{"before":"bc8998a29154615b32161cca5ae80dd516b76afb","after":"378ff01d1161241af7544a2ddb92aeacddd24db4","ref":"refs/heads/master","pushedAt":"2024-04-19T14:05:27.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Rewrite rules for pushouts (#1021)\n\nAdds strict β-laws for the standard pushouts in a new module\r\n`synthetic-homotopy-theory.rewriting-pushouts`.\r\n\r\n### Todo\r\n- [x] Wait for #885.\r\n- [x] ~Refactor postulates of universal properties to be phrased in\r\nterms of coherently invertible maps.~\r\n- [x] Add separate file for rewrites\r\n`synthetic-homotopy-theory.rewriting-pushouts`.","shortMessageHtmlLink":"Rewrite rules for pushouts (#1021)"}},{"before":"f4400b1796c531efde2e8439fc6a0a49622470db","after":"bc8998a29154615b32161cca5ae80dd516b76afb","ref":"refs/heads/master","pushedAt":"2024-04-18T10:24:19.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"Equivalences are closed under \"transfinite composition\" (#1117)\n\n- if a sequential diagram consists of equivalences, then injection maps\r\ninto its colimit are also equivalences\r\n- as a corollary, sequential colimits of sequential diagrams of\r\ncontractible types are contractible\r\n\r\nProgress towards #1080","shortMessageHtmlLink":"Equivalences are closed under \"transfinite composition\" (#1117)"}},{"before":"6fb97c00ee1c6690aac1617199a78368f919136e","after":"f4400b1796c531efde2e8439fc6a0a49622470db","ref":"refs/heads/master","pushedAt":"2024-04-17T10:49:49.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"EgbertRijke","name":"Egbert Rijke","path":"/EgbertRijke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1252282?s=80&v=4"},"commit":{"message":"Splitting idempotents (#1105)\n\n### Summary\r\n- Retracts of a type\r\n - Define retracts of a type \r\n - Characterize equality of retracts\r\n- Weakly constant maps\r\n - The type of fixed points of weakly constant maps is a proposition\r\n- Idempotent maps\r\n- Rename \"preidempotent maps\" to \"idempotent maps\". This mirrors how we\r\ntreat \"invertible maps\" vs \"coherently invertible maps\", although there\r\nis an essential difference between the two concepts: idempotent maps are\r\nnot \"coherentifiable\" like invertible maps. That role is taken by\r\n\"quasicoherently idempotent maps\" instead.\r\n- Quasicoherently idempotent maps (called \"quasiidempotent maps\" in\r\n[Shu17])\r\n - Define quasicoherently idempotent maps\r\n- Quasicoherently idempotent maps are closed under homotopy (without\r\nfunext)\r\n- Split idempotent maps\r\n - Define split idempotent maps\r\n - Split idempotent maps are quasicoherently idempotent\r\n - Idempotent maps on sets split\r\n - Weakly constant idempotent maps split\r\n - Quasicoherently idempotent maps split\r\n- Retracts of small types are small\r\n\r\nWork towards #1103.","shortMessageHtmlLink":"Splitting idempotents (#1105)"}},{"before":"2c0f6a62c6806f6ab5cd8959104df3cd85e34df9","after":"6fb97c00ee1c6690aac1617199a78368f919136e","ref":"refs/heads/master","pushedAt":"2024-04-17T08:55:59.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"Hereditary W-types (#1112)\n\nIn this PR I generalized the equivalence constructed in #1110, to\r\nsomething that I called \"hereditary W-types\". This PR is independent of\r\n#1110.","shortMessageHtmlLink":"Hereditary W-types (#1112)"}},{"before":"aa8c6b499d2cadd905af1531d6084578181cb517","after":"2c0f6a62c6806f6ab5cd8959104df3cd85e34df9","ref":"refs/heads/master","pushedAt":"2024-04-16T14:14:57.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"Descent data for sequential colimits and its version of the flattening lemma (#1109)\n\nSorry, this is bigger than I anticipated...\r\n\r\nThis PR\r\n- defines morphisms and equivalences between dependent sequential\r\ndiagrams\r\n- defines morphisms and equivalences of cocones under morphisms and\r\nequivalences of sequential diagrams\r\n- defines equifibered sequential diagrams\r\n- defines descent data for sequential colimits\r\n- shows the descent property of sequential colimits\r\n- proves a version of the flattening lemma expressed with families with\r\nassociated descent data\r\n- collects various helpers for converting between sequential stuff and\r\ncoequalizer stuff into one file\r\n- adds some auxiliary infrastructure along the way\r\n\r\nI took care to properly separate the work into commits, so it might be\r\nmore digestible to review it commit by commit.\r\n\r\nThis is progress towards #1080","shortMessageHtmlLink":"Descent data for sequential colimits and its version of the flattenin…"}},{"before":"ac75d87954fffca6d9a86cee4d2840abdef7dfdf","after":"aa8c6b499d2cadd905af1531d6084578181cb517","ref":"refs/heads/master","pushedAt":"2024-04-16T11:39:57.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"Fix line height in lists (#1114)\n\nAn issue discovered by @fredrik-bakke — code blocks in lists inherit\r\nbigger line spacing, making the ASCII diagrams more stretched.\r\n\r\nCompare\r\n![20240416 133603\r\nscreen](https://github.com/UniMath/agda-unimath/assets/15523887/20ff88b2-a26b-4153-9ffe-0a892fee5376)","shortMessageHtmlLink":"Fix line height in lists (#1114)"}},{"before":"aab86e6ce4c1f0fb95233c29b8faf4fa8a3498d2","after":"ac75d87954fffca6d9a86cee4d2840abdef7dfdf","ref":"refs/heads/master","pushedAt":"2024-04-14T20:34:17.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"fredrik-bakke","name":"Fredrik Bakke","path":"/fredrik-bakke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5176294?s=80&v=4"},"commit":{"message":"Acyclic maps are closed under retracts (#1113)\n\nEasy corollary as @fredrik-bakke added retracts of maps to the library","shortMessageHtmlLink":"Acyclic maps are closed under retracts (#1113)"}},{"before":"33140a8cffd322e01e85a373e4f4d5b511d3a4bc","after":"aab86e6ce4c1f0fb95233c29b8faf4fa8a3498d2","ref":"refs/heads/master","pushedAt":"2024-04-13T16:16:57.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"VojtechStep","name":"Vojtěch Štěpančík","path":"/VojtechStep","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15523887?s=80&v=4"},"commit":{"message":"Plane trees (#1110)\n\nThis is a short pull request introducing plane trees and proves that the\ntype of plane trees is equivalent to the type of full binary trees.\n\nThere are some related old files about binary trees which I will clean\nup in another pull request, but not here.","shortMessageHtmlLink":"Plane trees (#1110)"}},{"before":"c6939e9a9fda537b560ec164b44bf8dcd377b34f","after":"33140a8cffd322e01e85a373e4f4d5b511d3a4bc","ref":"refs/heads/master","pushedAt":"2024-04-12T14:59:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"EgbertRijke","name":"Egbert Rijke","path":"/EgbertRijke","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1252282?s=80&v=4"},"commit":{"message":"chore: Rename `universal-property-surj` to `universal-property-surjection` (#1108)","shortMessageHtmlLink":"chore: Rename universal-property-surj to `universal-property-surjec…"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEXTyPpwA","startCursor":null,"endCursor":null}},"title":"Activity · UniMath/agda-unimath"}