{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/136","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/136/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/136/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/136/events","html_url":"https://github.com/UniMath/UniMath/issues/136","id":101147848,"number":136,"title":"Coconus","user":{"login":"nyraghu","id":11349287,"avatar_url":"https://avatars.githubusercontent.com/u/11349287?v=3","gravatar_id":"","url":"https://api.github.com/users/nyraghu","html_url":"https://github.com/nyraghu","followers_url":"https://api.github.com/users/nyraghu/followers","following_url":"https://api.github.com/users/nyraghu/following{/other_user}","gists_url":"https://api.github.com/users/nyraghu/gists{/gist_id}","starred_url":"https://api.github.com/users/nyraghu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nyraghu/subscriptions","organizations_url":"https://api.github.com/users/nyraghu/orgs","repos_url":"https://api.github.com/users/nyraghu/repos","events_url":"https://api.github.com/users/nyraghu/events{/privacy}","received_events_url":"https://api.github.com/users/nyraghu/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":13,"created_at":"2015-08-15T06:39:36Z","updated_at":"2015-08-23T08:35:14Z","closed_at":null,"body":"uu0a.v says, \"Coconuses: spaces of paths which begin (coconusfromt) or end (coconustot) at a given point\" .  Why are these types called \"coconuses\"? Something to do with cocones?\r\n\r\nIn general, it'd be great to have a small comment explaining the etymology/motivation/purpose of each definition and theorem.  I understand it's a lot of work, and teaching isn't necessarily an aim of the UniMath library, but it'd be a tremendous help to people trying to learn about it."},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/133803361","html_url":"https://github.com/UniMath/UniMath/issues/136#issuecomment-133803361","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/136","id":133803361,"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":"2015-08-23T08:35:14Z","updated_at":"2015-08-23T08:35:14Z","body":"Do you want to give a name to the expression forall ( x y : T ) , x = y ? I now call it “no parts” i.e.\n\nnoparts(T)=forall(x y : T), x=y.\n\nThen one would have nopartscoconeto instead of connectedcoconustot\n\n(if we also apply coconus -> cocone and tot -> to and fromt -> from)\n\nThe name proofirrelevant was used to emphasize the connection with the usual concept of proof irrelevance.\n\nMany of these names have been chosen at the time when the code was written for reasons that were relevant at that particular moment.\n\nI am not sure that we should invest time in changing these names now.\n\nIf you have a good idea on how to organize terminology of a particular set of concepts you can implement it  by creating a file with notations that will, without changing the original names, introduce new names.\n\nVladimir.\n\n\n\n\n\n\n> On Aug 23, 2015, at 9:12 AM, N. Raghavendra <notifications@github.com> wrote:\n> \n> My apologies for bringing in confusion.\n> \n> I have another comment on the coconus part of uu0a.v. In Lemma connectedcoconustot, the inhabitedness of the type forall (c1 c2 : coconustot T t) is called the connectedness of the coconus. On the other hand, in Lemma proofirrelevancecontr, the inhabitedness of the type forall (x x' : X), x = x' is called the proof irrelevance of X. It'd perhaps be better if a single terminology is chosen for the inhabitedness of the type forall (x y : A), x = y.\n> \n> —\n> Reply to this email directly or view it on GitHub <https://github.com/UniMath/UniMath/issues/136#issuecomment-133796075>.\n> \n\n"}}