{"action":"created","issue":{"url":"https://api.github.com/repos/JonPRL/sml-dependent-lcf/issues/3","repository_url":"https://api.github.com/repos/JonPRL/sml-dependent-lcf","labels_url":"https://api.github.com/repos/JonPRL/sml-dependent-lcf/issues/3/labels{/name}","comments_url":"https://api.github.com/repos/JonPRL/sml-dependent-lcf/issues/3/comments","events_url":"https://api.github.com/repos/JonPRL/sml-dependent-lcf/issues/3/events","html_url":"https://github.com/JonPRL/sml-dependent-lcf/issues/3","id":135246729,"number":3,"title":"[agda] define model","user":{"login":"jonsterling","id":55057,"avatar_url":"https://avatars.githubusercontent.com/u/55057?v=3","gravatar_id":"","url":"https://api.github.com/users/jonsterling","html_url":"https://github.com/jonsterling","followers_url":"https://api.github.com/users/jonsterling/followers","following_url":"https://api.github.com/users/jonsterling/following{/other_user}","gists_url":"https://api.github.com/users/jonsterling/gists{/gist_id}","starred_url":"https://api.github.com/users/jonsterling/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonsterling/subscriptions","organizations_url":"https://api.github.com/users/jonsterling/orgs","repos_url":"https://api.github.com/users/jonsterling/repos","events_url":"https://api.github.com/users/jonsterling/events{/privacy}","received_events_url":"https://api.github.com/users/jonsterling/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2016-02-21T19:21:35Z","updated_at":"2016-02-21T19:25:19Z","closed_at":null,"body":"- [ ] relative monads\r\n- [ ] category of containers\r\n- [ ] telescopes\r\n- [ ] logical signature == container `Valence :> Sort`, with a distinguished sort `jdg` of judgments\r\n- [ ] category of logical signatures\r\n- [ ] functor `J` from a logical signature `L` to the set of `L`-judgments\r\n- [ ] functor `T` from a logical signature `L` to the set of proof states for `L`\r\n- [ ] show that `T` is a relative monad on `J`"},"comment":{"url":"https://api.github.com/repos/JonPRL/sml-dependent-lcf/issues/comments/186894997","html_url":"https://github.com/JonPRL/sml-dependent-lcf/issues/3#issuecomment-186894997","issue_url":"https://api.github.com/repos/JonPRL/sml-dependent-lcf/issues/3","id":186894997,"user":{"login":"jonsterling","id":55057,"avatar_url":"https://avatars.githubusercontent.com/u/55057?v=3","gravatar_id":"","url":"https://api.github.com/users/jonsterling","html_url":"https://github.com/jonsterling","followers_url":"https://api.github.com/users/jonsterling/followers","following_url":"https://api.github.com/users/jonsterling/following{/other_user}","gists_url":"https://api.github.com/users/jonsterling/gists{/gist_id}","starred_url":"https://api.github.com/users/jonsterling/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonsterling/subscriptions","organizations_url":"https://api.github.com/users/jonsterling/orgs","repos_url":"https://api.github.com/users/jonsterling/repos","events_url":"https://api.github.com/users/jonsterling/events{/privacy}","received_events_url":"https://api.github.com/users/jonsterling/received_events","type":"User","site_admin":false},"created_at":"2016-02-21T19:25:18Z","updated_at":"2016-02-21T19:25:18Z","body":"Note: I have not yet convinced myself that the `subst` operation for dependent tactic trees actually obeys the (relative) monad laws. I hope it does, or if it doesn't, can be replaced with something that does."}}