{"action":"created","comment":{"url":"https://api.github.com/repos/HoTT/HoTT/pulls/comments/22879030","id":22879030,"diff_hunk":"@@ -0,0 +1,284 @@\n+(* -*- mode: coq; mode: visual-line -*-  *)\n+\n+(** * Decidable propositions *)\n+\n+Require Import HoTT.Basics HoTT.Types.\n+Require Import TruncType HProp UnivalenceImpliesFunext.\n+Require Import hit.Truncations.\n+Local Open Scope equiv_scope.\n+Local Open Scope path_scope.\n+\n+(** ** Definitions *)\n+\n+(** A decidable proposition is, morally speaking, an hprop that is decidable.  However, we only require that it be an hprop under the additional assumption of [Funext]; this enables decidable propositions to usually be used without [Funext] hypotheses. *)\n+\n+Record DProp :=\n+  { dprop_type : Type ;\n+    ishprop_dprop : Funext -> IsHProp dprop_type ;\n+    dec_dprop : Decidable dprop_type\n+  }.\n+\n+(** A fancier definition, which would have the property that negation is judgmentally involutive, would be\n+\n+<<\n+Record DProp :=\n+  { dprop_holds : Type ;\n+    ishprop_holds : Funext -> IsHProp dprop_holds ;\n+    dprop_denies : Type ;\n+    ishprop_denies : Funext -> IsHProp dprop_denies ;\n+    holds_or_denies : dprop_holds + dprop_denies ;\n+    denies_or_holds : dprop_denies + dprop_holds ;\n+    not_holds_and_denies : dprop_holds -> dprop_denies -> Empty\n+  }.\n+>>\n+\n+At some point we may want to go that route, but it would be more work.  In particualar, [Instance]s of [Decidable] wouldn't be automatically computed for us, and the characterization of the homotopy type of [DProp] itself would be a lot harder. *)\n+\n+Coercion dprop_type : DProp >-> Sortclass.\n+Global Existing Instance ishprop_dprop.\n+Global Existing Instance dec_dprop.\n+\n+(** Sometimes, however, we have decidable props that are hprops without funext, and we want to remember that. *)\n+\n+Record DHProp :=\n+  { dhprop_hprop : hProp ;\n+    dec_dhprop : Decidable dhprop_hprop\n+  }.\n+\n+Coercion dhprop_hprop : DHProp >-> hProp.\n+Global Existing Instance dec_dhprop.\n+\n+Definition dhprop_to_dprop : DHProp -> DProp\n+  := fun P => Build_DProp P (fun _ => _) _.\n+\n+Coercion dhprop_to_dprop : DHProp >-> DProp.\n+\n+(** In particular, [True] and [False] are always hprops. *)\n+\n+Definition True : DHProp\n+  := Build_DHProp Unit_hp (inl tt).\n+\n+Definition False : DHProp\n+  := Build_DHProp False_hp (inr idmap).\n+\n+(** Decidable props can be coerced to [Bool]. *)\n+\n+Definition dprop_to_bool (P : DProp) : Bool\n+  := if dec P then true else false.\n+\n+Coercion dprop_to_bool : DProp >-> Bool.\n+\n+(** And back again, but we don't declare that as a coercion. *)\n+\n+Definition bool_to_dhprop (b : Bool) : DHProp\n+  := if b then True else False.\n+\n+(** ** The type of decidable props *)\n+\n+Definition issig_dprop\n+  : { X : Type & { _ : Funext -> IsHProp X & Decidable X } } <~> DProp.\n+Proof.\n+  issig Build_DProp dprop_type ishprop_dprop dec_dprop.\n+Defined.\n+\n+Definition equiv_path_dprop `{Funext} (P Q : DProp)\n+: (P = Q :> Type) <~> (P = Q :> DProp).\n+Proof.\n+  destruct P as [P hP dP]. destruct Q as [Q hQ dQ].\n+  refine (equiv_compose'\n+            (equiv_inverse (equiv_ap' (equiv_inverse issig_dprop) _ _))\n+            _); cbn.\n+  refine (equiv_compose'\n+            (equiv_ap' (equiv_inverse\n+                          (equiv_sigma_assoc _ (fun Xp => Decidable Xp.1)))\n+                       ((P;hP);dP) ((Q;hQ);dQ)) _).\n+  refine (equiv_compose' (equiv_path_sigma_hprop _ _) _); cbn.\n+  { intros [X hX]; exact _. }\n+  refine (equiv_path_sigma_hprop (P;hP) (Q;hQ)).\n+Defined.\n+\n+Definition path_dprop `{Funext} {P Q : DProp}\n+: (P = Q :> Type) -> (P = Q :> DProp)\n+  := equiv_path_dprop P Q.\n+\n+Global Instance ishset_dprop `{Univalence} : IsHSet DProp.\n+Proof.\n+  intros P Q.\n+  refine (trunc_equiv' _ (n := -1) (equiv_path_dprop P Q)).\n+Defined.\n+\n+Global Instance isequiv_dprop_to_bool `{Univalence}\n+: IsEquiv dprop_to_bool.\n+Proof.\n+  refine (isequiv_adjointify dprop_to_bool\n+            (fun b:Bool => if b then True else False) _ _).\n+  - intros []; reflexivity.\n+  - intros P; unfold dprop_to_bool.\n+    destruct (dec P); symmetry; apply path_dprop, path_universe_uncurried.\n+    + apply if_hprop_then_equiv_Unit; [ exact _ | assumption ].\n+    + apply if_not_hprop_then_equiv_Empty; [ exact _ | assumption ].\n+Defined.\n+\n+Definition equiv_dprop_to_bool `{Univalence}\n+: DProp <~> Bool\n+  := BuildEquiv _ _ dprop_to_bool _.\n+\n+(** ** Operations *)\n+\n+(** We define the logical operations on decidable hprops to be the operations on ordinary hprops, with decidability carrying over.  For the operations which preserve hprops without funext, we define separate versions that act on [DHProp]. *)\n+\n+Definition dand (b1 b2 : DProp) : DProp\n+  := Build_DProp (b1 * b2) _ _.\n+\n+Definition dhand (b1 b2 : DHProp) : DHProp\n+  := Build_DHProp (BuildhProp (b1 * b2)) _.\n+\n+Definition dor (b1 b2 : DProp) : DProp\n+  := Build_DProp (hor b1 b2) _ _.\n+\n+Definition dhor (b1 b2 : DHProp) : DHProp\n+  := Build_DHProp (BuildhProp (hor b1 b2)) _.\n+\n+Definition dneg (b : DProp) : DProp\n+  := Build_DProp (~b) _ _.\n+\n+Definition dimpl (b1 b2 : DProp) : DProp\n+  := Build_DProp (b1 -> b2) _ _.\n+\n+Infix \"&&\" := dand : dprop_scope.\n+Infix \"&&\" := dhand : dhprop_scope.\n+Infix \"||\" := dor : dprop_scope.\n+Infix \"||\" := dhor : dhprop_scope.\n+Infix \"->\" := dimpl : dprop_scope.\n+Notation \"!! P\" := (dneg P) (at level 75, right associativity)\n+                   : dprop_scope.\n+\n+Delimit Scope dprop_scope with dprop.\n+Delimit Scope dhprop_scope with dhprop.\n+Local Open Scope dprop_scope.\n+\n+(** ** Computation *)\n+\n+(** In order to be able to \"compute\" with [DProp]s like booleans, we define a couple of typeclasses. *)\n+\n+Class IsTrue (P : DProp) :=\n+  dprop_istrue : P.\n+\n+Class IsFalse (P : DProp) :=\n+  dprop_isfalse : ~ P.\n+\n+Global Instance true_istrue : IsTrue True := tt.\n+\n+Global Instance false_isfalse : IsFalse False := idmap.\n+\n+Global Instance dand_true_true {P Q} `{IsTrue P} `{IsTrue Q}\n+: IsTrue (P && Q).\n+Proof.\n+  exact (dprop_istrue, dprop_istrue).\n+Defined.\n+\n+Global Instance dand_false_l {P Q} `{IsFalse P}\n+: IsFalse (P && Q).\n+Proof.\n+  intros [p q].\n+  exact (dprop_isfalse p).\n+Defined.\n+\n+Global Instance dand_false_r {P Q} `{IsFalse Q}\n+: IsFalse (P && Q).\n+Proof.\n+  intros [p q].\n+  exact (dprop_isfalse q).\n+Defined.\n+\n+Global Instance dhand_true_true {P Q : DHProp} `{IsTrue P} `{IsTrue Q}\n+: IsTrue (P && Q)%dhprop.\n+Proof.\n+  (** Why does Coq need the argument [P] here? *)","path":"theories/DProp.v","position":197,"original_position":197,"commit_id":"de9ba6d5273dca034346f6a2eabba654a9a634e3","original_commit_id":"de9ba6d5273dca034346f6a2eabba654a9a634e3","user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"body":"My understanding: when you say ` it needs to fill in type classes for `?1 : IsTrue ?2`, and also separately needs to unify `IsTrue ?2` with `P`.  Apparently, it does typeclass resolution first (since `Typeclasses Strict Resolution` is `Local` to `Overture`), and decides that `?1` should be `H0`, and `?2` should therefore be `Q`.  It then tries to unify `IsTrue Q` with `P`, and fails.  If you `Set Typeclasses Strict Resolution`, then it doesn't know how to unify `IsTrue ?2` with `P`.  (Apparently unification is unwilling to unfold `IsTrue`?  I'm not really sure what's going on here.  @mattam82, any idea what's going on if you `Set Typeclasses Strict Resolution` at the top, and then do `refine (_, _)`, and then `refine (_ : IsTrue _)`---why does it fail, rather than unfolding `IsTrue` and unifying the evar with `P`?)","created_at":"2015-01-13T17:41:40Z","updated_at":"2015-01-13T17:41:40Z","html_url":"https://github.com/HoTT/HoTT/pull/683#discussion_r22879030","pull_request_url":"https://api.github.com/repos/HoTT/HoTT/pulls/683","_links":{"self":{"href":"https://api.github.com/repos/HoTT/HoTT/pulls/comments/22879030"},"html":{"href":"https://github.com/HoTT/HoTT/pull/683#discussion_r22879030"},"pull_request":{"href":"https://api.github.com/repos/HoTT/HoTT/pulls/683"}}},"pull_request":{"url":"https://api.github.com/repos/HoTT/HoTT/pulls/683","id":27270312,"html_url":"https://github.com/HoTT/HoTT/pull/683","diff_url":"https://github.com/HoTT/HoTT/pull/683.diff","patch_url":"https://github.com/HoTT/HoTT/pull/683.patch","issue_url":"https://api.github.com/repos/HoTT/HoTT/issues/683","number":683,"state":"open","locked":false,"title":"Decidable props","user":{"login":"mikeshulman","id":646600,"avatar_url":"https://avatars.githubusercontent.com/u/646600?v=3","gravatar_id":"","url":"https://api.github.com/users/mikeshulman","html_url":"https://github.com/mikeshulman","followers_url":"https://api.github.com/users/mikeshulman/followers","following_url":"https://api.github.com/users/mikeshulman/following{/other_user}","gists_url":"https://api.github.com/users/mikeshulman/gists{/gist_id}","starred_url":"https://api.github.com/users/mikeshulman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mikeshulman/subscriptions","organizations_url":"https://api.github.com/users/mikeshulman/orgs","repos_url":"https://api.github.com/users/mikeshulman/repos","events_url":"https://api.github.com/users/mikeshulman/events{/privacy}","received_events_url":"https://api.github.com/users/mikeshulman/received_events","type":"User","site_admin":false},"body":"See discussion at #654.  There are some unresolved questions and other possibilities to explore, but let's not let the perfect be the enemy of the good.  This adds `DHProp` (decidable props that are hprops without funext) to the previously linked implementation.","created_at":"2015-01-13T13:20:43Z","updated_at":"2015-01-13T17:41:40Z","closed_at":null,"merged_at":null,"merge_commit_sha":"03ae6d600f8742712d87dea196b854e7835d71d4","assignee":null,"milestone":null,"commits_url":"https://api.github.com/repos/HoTT/HoTT/pulls/683/commits","review_comments_url":"https://api.github.com/repos/HoTT/HoTT/pulls/683/comments","review_comment_url":"https://api.github.com/repos/HoTT/HoTT/pulls/comments/{number}","comments_url":"https://api.github.com/repos/HoTT/HoTT/issues/683/comments","statuses_url":"https://api.github.com/repos/HoTT/HoTT/statuses/de9ba6d5273dca034346f6a2eabba654a9a634e3","head":{"label":"mikeshulman:dprop-nofunext","ref":"dprop-nofunext","sha":"de9ba6d5273dca034346f6a2eabba654a9a634e3","user":{"login":"mikeshulman","id":646600,"avatar_url":"https://avatars.githubusercontent.com/u/646600?v=3","gravatar_id":"","url":"https://api.github.com/users/mikeshulman","html_url":"https://github.com/mikeshulman","followers_url":"https://api.github.com/users/mikeshulman/followers","following_url":"https://api.github.com/users/mikeshulman/following{/other_user}","gists_url":"https://api.github.com/users/mikeshulman/gists{/gist_id}","starred_url":"https://api.github.com/users/mikeshulman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mikeshulman/subscriptions","organizations_url":"https://api.github.com/users/mikeshulman/orgs","repos_url":"https://api.github.com/users/mikeshulman/repos","events_url":"https://api.github.com/users/mikeshulman/events{/privacy}","received_events_url":"https://api.github.com/users/mikeshulman/received_events","type":"User","site_admin":false},"repo":{"id":2769614,"name":"HoTT","full_name":"mikeshulman/HoTT","owner":{"login":"mikeshulman","id":646600,"avatar_url":"https://avatars.githubusercontent.com/u/646600?v=3","gravatar_id":"","url":"https://api.github.com/users/mikeshulman","html_url":"https://github.com/mikeshulman","followers_url":"https://api.github.com/users/mikeshulman/followers","following_url":"https://api.github.com/users/mikeshulman/following{/other_user}","gists_url":"https://api.github.com/users/mikeshulman/gists{/gist_id}","starred_url":"https://api.github.com/users/mikeshulman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mikeshulman/subscriptions","organizations_url":"https://api.github.com/users/mikeshulman/orgs","repos_url":"https://api.github.com/users/mikeshulman/repos","events_url":"https://api.github.com/users/mikeshulman/events{/privacy}","received_events_url":"https://api.github.com/users/mikeshulman/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/mikeshulman/HoTT","description":"Homotopy type theory","fork":true,"url":"https://api.github.com/repos/mikeshulman/HoTT","forks_url":"https://api.github.com/repos/mikeshulman/HoTT/forks","keys_url":"https://api.github.com/repos/mikeshulman/HoTT/keys{/key_id}","collaborators_url":"https://api.github.com/repos/mikeshulman/HoTT/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/mikeshulman/HoTT/teams","hooks_url":"https://api.github.com/repos/mikeshulman/HoTT/hooks","issue_events_url":"https://api.github.com/repos/mikeshulman/HoTT/issues/events{/number}","events_url":"https://api.github.com/repos/mikeshulman/HoTT/events","assignees_url":"https://api.github.com/repos/mikeshulman/HoTT/assignees{/user}","branches_url":"https://api.github.com/repos/mikeshulman/HoTT/branches{/branch}","tags_url":"https://api.github.com/repos/mikeshulman/HoTT/tags","blobs_url":"https://api.github.com/repos/mikeshulman/HoTT/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/mikeshulman/HoTT/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/mikeshulman/HoTT/git/refs{/sha}","trees_url":"https://api.github.com/repos/mikeshulman/HoTT/git/trees{/sha}","statuses_url":"https://api.github.com/repos/mikeshulman/HoTT/statuses/{sha}","languages_url":"https://api.github.com/repos/mikeshulman/HoTT/languages","stargazers_url":"https://api.github.com/repos/mikeshulman/HoTT/stargazers","contributors_url":"https://api.github.com/repos/mikeshulman/HoTT/contributors","subscribers_url":"https://api.github.com/repos/mikeshulman/HoTT/subscribers","subscription_url":"https://api.github.com/repos/mikeshulman/HoTT/subscription","commits_url":"https://api.github.com/repos/mikeshulman/HoTT/commits{/sha}","git_commits_url":"https://api.github.com/repos/mikeshulman/HoTT/git/commits{/sha}","comments_url":"https://api.github.com/repos/mikeshulman/HoTT/comments{/number}","issue_comment_url":"https://api.github.com/repos/mikeshulman/HoTT/issues/comments/{number}","contents_url":"https://api.github.com/repos/mikeshulman/HoTT/contents/{+path}","compare_url":"https://api.github.com/repos/mikeshulman/HoTT/compare/{base}...{head}","merges_url":"https://api.github.com/repos/mikeshulman/HoTT/merges","archive_url":"https://api.github.com/repos/mikeshulman/HoTT/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/mikeshulman/HoTT/downloads","issues_url":"https://api.github.com/repos/mikeshulman/HoTT/issues{/number}","pulls_url":"https://api.github.com/repos/mikeshulman/HoTT/pulls{/number}","milestones_url":"https://api.github.com/repos/mikeshulman/HoTT/milestones{/number}","notifications_url":"https://api.github.com/repos/mikeshulman/HoTT/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/mikeshulman/HoTT/labels{/name}","releases_url":"https://api.github.com/repos/mikeshulman/HoTT/releases{/id}","created_at":"2011-11-14T02:23:07Z","updated_at":"2015-01-13T08:25:43Z","pushed_at":"2015-01-13T13:18:57Z","git_url":"git://github.com/mikeshulman/HoTT.git","ssh_url":"git@github.com:mikeshulman/HoTT.git","clone_url":"https://github.com/mikeshulman/HoTT.git","svn_url":"https://github.com/mikeshulman/HoTT","homepage":"http://homotopytypetheory.org/","size":8244,"stargazers_count":7,"watchers_count":7,"language":"Coq","has_issues":false,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":3,"mirror_url":null,"open_issues_count":0,"forks":3,"open_issues":0,"watchers":7,"default_branch":"master"}},"base":{"label":"HoTT:master","ref":"master","sha":"444ca3b5f4f0995349659e81aad4379408da66ab","user":{"login":"HoTT","id":692156,"avatar_url":"https://avatars.githubusercontent.com/u/692156?v=3","gravatar_id":"","url":"https://api.github.com/users/HoTT","html_url":"https://github.com/HoTT","followers_url":"https://api.github.com/users/HoTT/followers","following_url":"https://api.github.com/users/HoTT/following{/other_user}","gists_url":"https://api.github.com/users/HoTT/gists{/gist_id}","starred_url":"https://api.github.com/users/HoTT/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/HoTT/subscriptions","organizations_url":"https://api.github.com/users/HoTT/orgs","repos_url":"https://api.github.com/users/HoTT/repos","events_url":"https://api.github.com/users/HoTT/events{/privacy}","received_events_url":"https://api.github.com/users/HoTT/received_events","type":"Organization","site_admin":false},"repo":{"id":1529601,"name":"HoTT","full_name":"HoTT/HoTT","owner":{"login":"HoTT","id":692156,"avatar_url":"https://avatars.githubusercontent.com/u/692156?v=3","gravatar_id":"","url":"https://api.github.com/users/HoTT","html_url":"https://github.com/HoTT","followers_url":"https://api.github.com/users/HoTT/followers","following_url":"https://api.github.com/users/HoTT/following{/other_user}","gists_url":"https://api.github.com/users/HoTT/gists{/gist_id}","starred_url":"https://api.github.com/users/HoTT/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/HoTT/subscriptions","organizations_url":"https://api.github.com/users/HoTT/orgs","repos_url":"https://api.github.com/users/HoTT/repos","events_url":"https://api.github.com/users/HoTT/events{/privacy}","received_events_url":"https://api.github.com/users/HoTT/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/HoTT/HoTT","description":"Homotopy type theory","fork":false,"url":"https://api.github.com/repos/HoTT/HoTT","forks_url":"https://api.github.com/repos/HoTT/HoTT/forks","keys_url":"https://api.github.com/repos/HoTT/HoTT/keys{/key_id}","collaborators_url":"https://api.github.com/repos/HoTT/HoTT/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/HoTT/HoTT/teams","hooks_url":"https://api.github.com/repos/HoTT/HoTT/hooks","issue_events_url":"https://api.github.com/repos/HoTT/HoTT/issues/events{/number}","events_url":"https://api.github.com/repos/HoTT/HoTT/events","assignees_url":"https://api.github.com/repos/HoTT/HoTT/assignees{/user}","branches_url":"https://api.github.com/repos/HoTT/HoTT/branches{/branch}","tags_url":"https://api.github.com/repos/HoTT/HoTT/tags","blobs_url":"https://api.github.com/repos/HoTT/HoTT/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/HoTT/HoTT/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/HoTT/HoTT/git/refs{/sha}","trees_url":"https://api.github.com/repos/HoTT/HoTT/git/trees{/sha}","statuses_url":"https://api.github.com/repos/HoTT/HoTT/statuses/{sha}","languages_url":"https://api.github.com/repos/HoTT/HoTT/languages","stargazers_url":"https://api.github.com/repos/HoTT/HoTT/stargazers","contributors_url":"https://api.github.com/repos/HoTT/HoTT/contributors","subscribers_url":"https://api.github.com/repos/HoTT/HoTT/subscribers","subscription_url":"https://api.github.com/repos/HoTT/HoTT/subscription","commits_url":"https://api.github.com/repos/HoTT/HoTT/commits{/sha}","git_commits_url":"https://api.github.com/repos/HoTT/HoTT/git/commits{/sha}","comments_url":"https://api.github.com/repos/HoTT/HoTT/comments{/number}","issue_comment_url":"https://api.github.com/repos/HoTT/HoTT/issues/comments/{number}","contents_url":"https://api.github.com/repos/HoTT/HoTT/contents/{+path}","compare_url":"https://api.github.com/repos/HoTT/HoTT/compare/{base}...{head}","merges_url":"https://api.github.com/repos/HoTT/HoTT/merges","archive_url":"https://api.github.com/repos/HoTT/HoTT/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/HoTT/HoTT/downloads","issues_url":"https://api.github.com/repos/HoTT/HoTT/issues{/number}","pulls_url":"https://api.github.com/repos/HoTT/HoTT/pulls{/number}","milestones_url":"https://api.github.com/repos/HoTT/HoTT/milestones{/number}","notifications_url":"https://api.github.com/repos/HoTT/HoTT/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/HoTT/HoTT/labels{/name}","releases_url":"https://api.github.com/repos/HoTT/HoTT/releases{/id}","created_at":"2011-03-26T15:59:20Z","updated_at":"2015-01-13T02:02:48Z","pushed_at":"2015-01-12T19:57:21Z","git_url":"git://github.com/HoTT/HoTT.git","ssh_url":"git@github.com:HoTT/HoTT.git","clone_url":"https://github.com/HoTT/HoTT.git","svn_url":"https://github.com/HoTT/HoTT","homepage":"http://homotopytypetheory.org/","size":176310,"stargazers_count":250,"watchers_count":250,"language":"Coq","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":true,"forks_count":54,"mirror_url":null,"open_issues_count":53,"forks":54,"open_issues":53,"watchers":250,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/HoTT/HoTT/pulls/683"},"html":{"href":"https://github.com/HoTT/HoTT/pull/683"},"issue":{"href":"https://api.github.com/repos/HoTT/HoTT/issues/683"},"comments":{"href":"https://api.github.com/repos/HoTT/HoTT/issues/683/comments"},"review_comments":{"href":"https://api.github.com/repos/HoTT/HoTT/pulls/683/comments"},"review_comment":{"href":"https://api.github.com/repos/HoTT/HoTT/pulls/comments/{number}"},"commits":{"href":"https://api.github.com/repos/HoTT/HoTT/pulls/683/commits"},"statuses":{"href":"https://api.github.com/repos/HoTT/HoTT/statuses/de9ba6d5273dca034346f6a2eabba654a9a634e3"}}}}