{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/390","repository_url":"https://api.github.com/repos/UniMath/UniMath","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/390/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/390/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/390/events","html_url":"https://github.com/UniMath/UniMath/pull/390","id":163046611,"number":390,"title":"change notation for \"forall\"","user":{"login":"DanGrayson","id":700228,"avatar_url":"https://avatars.githubusercontent.com/u/700228?v=3","gravatar_id":"","url":"https://api.github.com/users/DanGrayson","html_url":"https://github.com/DanGrayson","followers_url":"https://api.github.com/users/DanGrayson/followers","following_url":"https://api.github.com/users/DanGrayson/following{/other_user}","gists_url":"https://api.github.com/users/DanGrayson/gists{/gist_id}","starred_url":"https://api.github.com/users/DanGrayson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DanGrayson/subscriptions","organizations_url":"https://api.github.com/users/DanGrayson/orgs","repos_url":"https://api.github.com/users/DanGrayson/repos","events_url":"https://api.github.com/users/DanGrayson/events{/privacy}","received_events_url":"https://api.github.com/users/DanGrayson/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-06-29T23:01:28Z","updated_at":"2016-06-30T13:30:56Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/390","html_url":"https://github.com/UniMath/UniMath/pull/390","diff_url":"https://github.com/UniMath/UniMath/pull/390.diff","patch_url":"https://github.com/UniMath/UniMath/pull/390.patch"},"body":"We rename our notation for ∀ to Π.\r\n\r\nWe make a global definition for ∀ that applies just to families of\r\npropositions and yields a proposition (hProp).\r\n\r\nWe change all existing uses of \"forall\" and ∀ to Π.  Later on, those\r\nthat applied to hProps could be switched back to ∀.\r\n\r\nThe reason we change all uses of \"forall\" is that ∀ is normally read as\r\n\"for all\".\r\n\r\nHere is the definition of ∀ from Propositions.v:\r\n```\r\n    Lemma isaprop_forall_hProp (X:UU) (Y:X->hProp) : isaprop (Π x, Y x).\r\n    Proof. intros. apply impred_isaprop. intro x. apply propproperty. Defined.\r\n\r\n    Definition forall_hProp {X:UU} (Y:X->hProp) : hProp := hProppair (Π x, Y x) (isaprop_forall_hProp X Y).\r\n\r\n    Notation \"∀  x .. y , P\" := (forall_hProp (fun x => .. (forall_hProp (fun y => P)) ..))\r\n      (at level 200, x binder, y binder, right associativity) : type_scope.\r\n```\r\n\r\nThis resolves #369 ."},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/229658407","html_url":"https://github.com/UniMath/UniMath/pull/390#issuecomment-229658407","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/390","id":229658407,"user":{"login":"vladimirias","id":424011,"avatar_url":"https://avatars.githubusercontent.com/u/424011?v=3","gravatar_id":"","url":"https://api.github.com/users/vladimirias","html_url":"https://github.com/vladimirias","followers_url":"https://api.github.com/users/vladimirias/followers","following_url":"https://api.github.com/users/vladimirias/following{/other_user}","gists_url":"https://api.github.com/users/vladimirias/gists{/gist_id}","starred_url":"https://api.github.com/users/vladimirias/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vladimirias/subscriptions","organizations_url":"https://api.github.com/users/vladimirias/orgs","repos_url":"https://api.github.com/users/vladimirias/repos","events_url":"https://api.github.com/users/vladimirias/events{/privacy}","received_events_url":"https://api.github.com/users/vladimirias/received_events","type":"User","site_admin":false},"created_at":"2016-06-30T13:30:55Z","updated_at":"2016-06-30T13:30:55Z","body":"I think that the use of “forall” should be permitted. It is a Coq identifier and someone who starts to write in UniMath may prefer to use it rather than to go through an extra hurdle of learning how to use unicode.\n\n\n> On Jun 29, 2016, at 7:01 PM, Daniel R. Grayson <notifications@github.com> wrote:\n> \n> We rename our notation for ∀ to Π.\n> \n> We make a global definition for ∀ that applies just to families of\n> propositions and yields a proposition (hProp).\n> \n> We change all existing uses of \"forall\" and ∀ to Π. Later on, those\n> that applied to hProps could be switched back to ∀.\n> \n> The reason we change all uses of \"forall\" is that ∀ is normally read as\n> \"for all\".\n> \n> Here is the definition of ∀ from Propositions.v:\n> \n>     Lemma isaprop_forall_hProp (X:UU) (Y:X->hProp) : isaprop (Π x, Y x).\n>     Proof. intros. apply impred_isaprop. intro x. apply propproperty. Defined.\n> \n>     Definition forall_hProp {X:UU} (Y:X->hProp) : hProp := hProppair (Π x, Y x) (isaprop_forall_hProp X Y).\n> \n>     Notation \"∀  x .. y , P\" := (forall_hProp (fun x => .. (forall_hProp (fun y => P)) ..))\n>       (at level 200, x binder, y binder, right associativity) : type_scope.\n> This resolves #369 <https://github.com/UniMath/UniMath/issues/369> .\n> \n> You can view, comment on, or merge this pull request online at:\n> \n>   https://github.com/UniMath/UniMath/pull/390 <https://github.com/UniMath/UniMath/pull/390>\n> Commit Summary\n> \n> change notation for \"forall\"\n> File Changes\n> \n> M UniMath/CategoryTheory/Epis.v <https://github.com/UniMath/UniMath/pull/390/files#diff-0> (4)\n> M UniMath/CategoryTheory/HLevel_n_is_of_hlevel_Sn.v <https://github.com/UniMath/UniMath/pull/390/files#diff-1> (10)\n> M UniMath/CategoryTheory/HorizontalComposition.v <https://github.com/UniMath/UniMath/pull/390/files#diff-2> (2)\n> M UniMath/CategoryTheory/Monads.v <https://github.com/UniMath/UniMath/pull/390/files#diff-3> (14)\n> M UniMath/CategoryTheory/Monics.v <https://github.com/UniMath/UniMath/pull/390/files#diff-4> (4)\n> M UniMath/CategoryTheory/PointedFunctors.v <https://github.com/UniMath/UniMath/pull/390/files#diff-5> (4)\n> M UniMath/CategoryTheory/PreAdditive.v <https://github.com/UniMath/UniMath/pull/390/files#diff-6> (8)\n> M UniMath/CategoryTheory/PrecategoriesWithAbgrops.v <https://github.com/UniMath/UniMath/pull/390/files#diff-7> (2)\n> M UniMath/CategoryTheory/PrecategoriesWithBinOps.v <https://github.com/UniMath/UniMath/pull/390/files#diff-8> (2)\n> M UniMath/CategoryTheory/ProductPrecategory.v <https://github.com/UniMath/UniMath/pull/390/files#diff-9> (10)\n> M UniMath/CategoryTheory/category_hset_structures.v <https://github.com/UniMath/UniMath/pull/390/files#diff-10> (18)\n> M UniMath/CategoryTheory/chains.v <https://github.com/UniMath/UniMath/pull/390/files#diff-11> (6)\n> M UniMath/CategoryTheory/cocontfunctors.v <https://github.com/UniMath/UniMath/pull/390/files#diff-12> (50)\n> M UniMath/CategoryTheory/covyoneda.v <https://github.com/UniMath/UniMath/pull/390/files#diff-13> (2)\n> M UniMath/CategoryTheory/equivalences.v <https://github.com/UniMath/UniMath/pull/390/files#diff-14> (26)\n> M UniMath/CategoryTheory/exponentials.v <https://github.com/UniMath/UniMath/pull/390/files#diff-15> (2)\n> M UniMath/CategoryTheory/functor_categories.v <https://github.com/UniMath/UniMath/pull/390/files#diff-16> (70)\n> M UniMath/CategoryTheory/limits/BinDirectSums.v <https://github.com/UniMath/UniMath/pull/390/files#diff-17> (10)\n> M UniMath/CategoryTheory/limits/FunctorsPointwiseBinCoproduct.v <https://github.com/UniMath/UniMath/pull/390/files#diff-18> (8)\n> M UniMath/CategoryTheory/limits/FunctorsPointwiseBinProduct.v <https://github.com/UniMath/UniMath/pull/390/files#diff-19> (8)\n> M UniMath/CategoryTheory/limits/FunctorsPointwiseCoproduct.v <https://github.com/UniMath/UniMath/pull/390/files#diff-20> (2)\n> M UniMath/CategoryTheory/limits/FunctorsPointwiseProduct.v <https://github.com/UniMath/UniMath/pull/390/files#diff-21> (2)\n> M UniMath/CategoryTheory/limits/bincoproducts.v <https://github.com/UniMath/UniMath/pull/390/files#diff-22> (14)\n> M UniMath/CategoryTheory/limits/binproducts.v <https://github.com/UniMath/UniMath/pull/390/files#diff-23> (14)\n> M UniMath/CategoryTheory/limits/cats/limits.v <https://github.com/UniMath/UniMath/pull/390/files#diff-24> (60)\n> M UniMath/CategoryTheory/limits/coequalizers.v <https://github.com/UniMath/UniMath/pull/390/files#diff-25> (8)\n> M UniMath/CategoryTheory/limits/cokernels.v <https://github.com/UniMath/UniMath/pull/390/files#diff-26> (4)\n> M UniMath/CategoryTheory/limits/cones.v <https://github.com/UniMath/UniMath/pull/390/files#diff-27> (14)\n> M UniMath/CategoryTheory/limits/coproducts.v <https://github.com/UniMath/UniMath/pull/390/files#diff-28> (44)\n> M UniMath/CategoryTheory/limits/equalizers.v <https://github.com/UniMath/UniMath/pull/390/files#diff-29> (8)\n> M UniMath/CategoryTheory/limits/graphs/bincoproducts.v <https://github.com/UniMath/UniMath/pull/390/files#diff-30> (10)\n> M UniMath/CategoryTheory/limits/graphs/binproducts.v <https://github.com/UniMath/UniMath/pull/390/files#diff-31> (10)\n> M UniMath/CategoryTheory/limits/graphs/colimits.v <https://github.com/UniMath/UniMath/pull/390/files#diff-32> (76)\n> M UniMath/CategoryTheory/limits/graphs/initial.v <https://github.com/UniMath/UniMath/pull/390/files#diff-33> (4)\n> M UniMath/CategoryTheory/limits/graphs/limits.v <https://github.com/UniMath/UniMath/pull/390/files#diff-34> (128)\n> M UniMath/CategoryTheory/limits/graphs/pullbacks.v <https://github.com/UniMath/UniMath/pull/390/files#diff-35> (8)\n> M UniMath/CategoryTheory/limits/graphs/terminal.v <https://github.com/UniMath/UniMath/pull/390/files#diff-36> (2)\n> M UniMath/CategoryTheory/limits/graphs/zero.v <https://github.com/UniMath/UniMath/pull/390/files#diff-37> (4)\n> M UniMath/CategoryTheory/limits/initial.v <https://github.com/UniMath/UniMath/pull/390/files#diff-38> (12)\n> M UniMath/CategoryTheory/limits/kernels.v <https://github.com/UniMath/UniMath/pull/390/files#diff-39> (4)\n> M UniMath/CategoryTheory/limits/more_on_pullbacks.v <https://github.com/UniMath/UniMath/pull/390/files#diff-40> (4)\n> M UniMath/CategoryTheory/limits/products.v <https://github.com/UniMath/UniMath/pull/390/files#diff-41> (72)\n> M UniMath/CategoryTheory/limits/pullbacks.v <https://github.com/UniMath/UniMath/pull/390/files#diff-42> (8)\n> M UniMath/CategoryTheory/limits/pushouts.v <https://github.com/UniMath/UniMath/pull/390/files#diff-43> (8)\n> M UniMath/CategoryTheory/limits/terminal.v <https://github.com/UniMath/UniMath/pull/390/files#diff-44> (12)\n> M UniMath/CategoryTheory/limits/zero.v <https://github.com/UniMath/UniMath/pull/390/files#diff-45> (6)\n> M UniMath/CategoryTheory/lists.v <https://github.com/UniMath/UniMath/pull/390/files#diff-46> (38)\n> M UniMath/CategoryTheory/opp_precat.v <https://github.com/UniMath/UniMath/pull/390/files#diff-47> (2)\n> M UniMath/CategoryTheory/precategories.v <https://github.com/UniMath/UniMath/pull/390/files#diff-48> (48)\n> M UniMath/CategoryTheory/precomp_ess_surj.v <https://github.com/UniMath/UniMath/pull/390/files#diff-49> (48)\n> M UniMath/CategoryTheory/precomp_fully_faithful.v <https://github.com/UniMath/UniMath/pull/390/files#diff-50> (10)\n> M UniMath/CategoryTheory/rezk_completion.v <https://github.com/UniMath/UniMath/pull/390/files#diff-51> (4)\n> M UniMath/CategoryTheory/slicecat.v <https://github.com/UniMath/UniMath/pull/390/files#diff-52> (4)\n> M UniMath/CategoryTheory/sub_precategories.v <https://github.com/UniMath/UniMath/pull/390/files#diff-53> (12)\n> M UniMath/CategoryTheory/trees.v <https://github.com/UniMath/UniMath/pull/390/files#diff-54> (10)\n> M UniMath/CategoryTheory/yoneda.v <https://github.com/UniMath/UniMath/pull/390/files#diff-55> (2)\n> M UniMath/Dedekind/Complements.v <https://github.com/UniMath/UniMath/pull/390/files#diff-56> (30)\n> M UniMath/Dedekind/DecidableDedekindCuts.v <https://github.com/UniMath/UniMath/pull/390/files#diff-57> (6)\n> M UniMath/Dedekind/Fields.v <https://github.com/UniMath/UniMath/pull/390/files#diff-58> (2)\n> M UniMath/Dedekind/NonnegativeRationals.v <https://github.com/UniMath/UniMath/pull/390/files#diff-59> (242)\n> M UniMath/Dedekind/NonnegativeReals.v <https://github.com/UniMath/UniMath/pull/390/files#diff-60> (420)\n> M UniMath/Dedekind/Reals.v <https://github.com/UniMath/UniMath/pull/390/files#diff-61> (266)\n> M UniMath/Dedekind/Sets.v <https://github.com/UniMath/UniMath/pull/390/files#diff-62> (50)\n> M UniMath/Folds/UnicodeNotations.v <https://github.com/UniMath/UniMath/pull/390/files#diff-63> (2)\n> M UniMath/Folds/folds_isomorphism.v <https://github.com/UniMath/UniMath/pull/390/files#diff-64> (28)\n> M UniMath/Folds/folds_pre_2_cat.v <https://github.com/UniMath/UniMath/pull/390/files#diff-65> (74)\n> M UniMath/Folds/folds_precat.v <https://github.com/UniMath/UniMath/pull/390/files#diff-66> (28)\n> M UniMath/Folds/from_precats_to_folds_and_back.v <https://github.com/UniMath/UniMath/pull/390/files#diff-67> (4)\n> M UniMath/Foundations/Algebra/Apartness.v <https://github.com/UniMath/UniMath/pull/390/files#diff-68> (44)\n> M UniMath/Foundations/Algebra/Archimedean.v <https://github.com/UniMath/UniMath/pull/390/files#diff-69> (68)\n> M UniMath/Foundations/Algebra/BinaryOperations.v <https://github.com/UniMath/UniMath/pull/390/files#diff-70> (84)\n> M UniMath/Foundations/Algebra/ConstructiveStructures.v <https://github.com/UniMath/UniMath/pull/390/files#diff-71> (164)\n> M UniMath/Foundations/Algebra/DivisionRig.v <https://github.com/UniMath/UniMath/pull/390/files#diff-72> (52)\n> M UniMath/Foundations/Algebra/Domains_and_Fields.v <https://github.com/UniMath/UniMath/pull/390/files#diff-73> (30)\n> M UniMath/Foundations/Algebra/IteratedBinaryOperations.v <https://github.com/UniMath/UniMath/pull/390/files#diff-74> (4)\n> M UniMath/Foundations/Algebra/Monoids_and_Groups.v <https://github.com/UniMath/UniMath/pull/390/files#diff-75> (44)\n> M UniMath/Foundations/Algebra/Rigs_and_Rings.v <https://github.com/UniMath/UniMath/pull/390/files#diff-76> (98)\n> M UniMath/Foundations/Algebra/Tests.v <https://github.com/UniMath/UniMath/pull/390/files#diff-77> (4)\n> M UniMath/Foundations/Basics/PartA.v <https://github.com/UniMath/UniMath/pull/390/files#diff-78> (268)\n> M UniMath/Foundations/Basics/PartB.v <https://github.com/UniMath/UniMath/pull/390/files#diff-79> (88)\n> M UniMath/Foundations/Basics/PartC.v <https://github.com/UniMath/UniMath/pull/390/files#diff-80> (92)\n> M UniMath/Foundations/Basics/PartD.v <https://github.com/UniMath/UniMath/pull/390/files#diff-81> (256)\n> M UniMath/Foundations/Basics/Preamble.v <https://github.com/UniMath/UniMath/pull/390/files#diff-82> (22)\n> M UniMath/Foundations/Basics/Propositions.v <https://github.com/UniMath/UniMath/pull/390/files#diff-83> (42)\n> M UniMath/Foundations/Basics/Sets.v <https://github.com/UniMath/UniMath/pull/390/files#diff-84> (230)\n> M UniMath/Foundations/Basics/Tests.v <https://github.com/UniMath/UniMath/pull/390/files#diff-85> (26)\n> M UniMath/Foundations/Basics/UnivalenceAxiom.v <https://github.com/UniMath/UniMath/pull/390/files#diff-86> (20)\n> M UniMath/Foundations/Combinatorics/FiniteSequences.v <https://github.com/UniMath/UniMath/pull/390/files#diff-87> (18)\n> M UniMath/Foundations/Combinatorics/FiniteSets.v <https://github.com/UniMath/UniMath/pull/390/files#diff-88> (16)\n> M UniMath/Foundations/Combinatorics/OrderedSets.v <https://github.com/UniMath/UniMath/pull/390/files#diff-89> (48)\n> M UniMath/Foundations/Combinatorics/StandardFiniteSets.v <https://github.com/UniMath/UniMath/pull/390/files#diff-90> (56)\n> M UniMath/Foundations/Combinatorics/Tests.v <https://github.com/UniMath/UniMath/pull/390/files#diff-91> (24)\n> M UniMath/Foundations/NumberSystems/Integers.v <https://github.com/UniMath/UniMath/pull/390/files#diff-92> (6)\n> M UniMath/Foundations/NumberSystems/NaturalNumbers.v <https://github.com/UniMath/UniMath/pull/390/files#diff-93> (6)\n> M UniMath/Ktheory/AbelianGroup.v <https://github.com/UniMath/UniMath/pull/390/files#diff-94> (58)\n> M UniMath/Ktheory/AbelianMonoid.v <https://github.com/UniMath/UniMath/pull/390/files#diff-95> (34)\n> M UniMath/Ktheory/AffineLine.v <https://github.com/UniMath/UniMath/pull/390/files#diff-96> (144)\n> M UniMath/Ktheory/Bifunctor.v <https://github.com/UniMath/UniMath/pull/390/files#diff-97> (20)\n> M UniMath/Ktheory/Circle.v <https://github.com/UniMath/UniMath/pull/390/files#diff-98> (4)\n> M UniMath/Ktheory/DirectSum.v <https://github.com/UniMath/UniMath/pull/390/files#diff-99> (16)\n> M UniMath/Ktheory/Equivalences.v <https://github.com/UniMath/UniMath/pull/390/files#diff-100> (18)\n> M UniMath/Ktheory/Group.v <https://github.com/UniMath/UniMath/pull/390/files#diff-101> (44)\n> M UniMath/Ktheory/GroupAction.v <https://github.com/UniMath/UniMath/pull/390/files#diff-102> (14)\n> M UniMath/Ktheory/Halfline.v <https://github.com/UniMath/UniMath/pull/390/files#diff-103> (8)\n> M UniMath/Ktheory/Interval.v <https://github.com/UniMath/UniMath/pull/390/files#diff-104> (4)\n> M UniMath/Ktheory/Magma.v <https://github.com/UniMath/UniMath/pull/390/files#diff-105> (8)\n> M UniMath/Ktheory/MetricTree.v <https://github.com/UniMath/UniMath/pull/390/files#diff-106> (16)\n> M UniMath/Ktheory/Monoid.v <https://github.com/UniMath/UniMath/pull/390/files#diff-107> (42)\n> M UniMath/Ktheory/MoreEquivalences.v <https://github.com/UniMath/UniMath/pull/390/files#diff-108> (28)\n> M UniMath/Ktheory/Nat.v <https://github.com/UniMath/UniMath/pull/390/files#diff-109> (38)\n> M UniMath/Ktheory/Precategories.v <https://github.com/UniMath/UniMath/pull/390/files#diff-110> (64)\n> M UniMath/Ktheory/QuotientSet.v <https://github.com/UniMath/UniMath/pull/390/files#diff-111> (8)\n> M UniMath/Ktheory/RawMatrix.v <https://github.com/UniMath/UniMath/pull/390/files#diff-112> (30)\n> M UniMath/Ktheory/Representation.v <https://github.com/UniMath/UniMath/pull/390/files#diff-113> (34)\n> M UniMath/Ktheory/StandardCategories.v <https://github.com/UniMath/UniMath/pull/390/files#diff-114> (2)\n> M UniMath/Ktheory/Test.v <https://github.com/UniMath/UniMath/pull/390/files#diff-115> (8)\n> M UniMath/Ktheory/Utilities.v <https://github.com/UniMath/UniMath/pull/390/files#diff-116> (78)\n> M UniMath/SubstitutionSystems/BinProductOfSignatures.v <https://github.com/UniMath/UniMath/pull/390/files#diff-117> (4)\n> M UniMath/SubstitutionSystems/BinSumOfSignatures.v <https://github.com/UniMath/UniMath/pull/390/files#diff-118> (4)\n> M UniMath/SubstitutionSystems/Lam.v <https://github.com/UniMath/UniMath/pull/390/files#diff-119> (4)\n> M UniMath/SubstitutionSystems/LamHSET.v <https://github.com/UniMath/UniMath/pull/390/files#diff-120> (2)\n> M UniMath/SubstitutionSystems/LamSignature.v <https://github.com/UniMath/UniMath/pull/390/files#diff-121> (14)\n> M UniMath/SubstitutionSystems/LiftingInitial.v <https://github.com/UniMath/UniMath/pull/390/files#diff-122> (10)\n> M UniMath/SubstitutionSystems/MonadsFromSubstitutionSystems.v <https://github.com/UniMath/UniMath/pull/390/files#diff-123> (10)\n> M UniMath/SubstitutionSystems/SignatureExamples.v <https://github.com/UniMath/UniMath/pull/390/files#diff-124> (2)\n> M UniMath/SubstitutionSystems/Signatures.v <https://github.com/UniMath/UniMath/pull/390/files#diff-125> (8)\n> M UniMath/SubstitutionSystems/SubstitutionSystems.v <https://github.com/UniMath/UniMath/pull/390/files#diff-126> (28)\n> M UniMath/SubstitutionSystems/SubstitutionSystems_Summary.v <https://github.com/UniMath/UniMath/pull/390/files#diff-127> (58)\n> M UniMath/SubstitutionSystems/SumOfSignatures.v <https://github.com/UniMath/UniMath/pull/390/files#diff-128> (14)\n> M UniMath/Tactics/Abmonoids_Tactics.v <https://github.com/UniMath/UniMath/pull/390/files#diff-129> (20)\n> M UniMath/Tactics/Nat_Tactics.v <https://github.com/UniMath/UniMath/pull/390/files#diff-130> (24)\n> Patch Links:\n> \n> https://github.com/UniMath/UniMath/pull/390.patch <https://github.com/UniMath/UniMath/pull/390.patch>\n> https://github.com/UniMath/UniMath/pull/390.diff <https://github.com/UniMath/UniMath/pull/390.diff>\n> —\n> You are receiving this because you are subscribed to this thread.\n> Reply to this email directly, view it on GitHub <https://github.com/UniMath/UniMath/pull/390>, or mute the thread <https://github.com/notifications/unsubscribe/AAZ4S-_BZaPVGzFvgVhBZKN6tu5_TZGdks5qQvlIgaJpZM4JBpt0>.\n> \n\n"}}
{"actor":{"display_login":"vladimirias"}}