{"id":55495,"name":"agda-unimath","description":"The agda-unimath library","url":"https://github.com/unimath/agda-unimath","last_synced_at":"2025-09-05T13:55:46.027Z","repository":{"id":37013750,"uuid":"429926544","full_name":"UniMath/agda-unimath","owner":"UniMath","description":"The agda-unimath library","archived":false,"fork":false,"pushed_at":"2025-09-03T05:22:19.000Z","size":30684,"stargazers_count":263,"open_issues_count":161,"forks_count":86,"subscribers_count":12,"default_branch":"master","last_synced_at":"2025-09-03T07:13:34.218Z","etag":null,"topics":["category-theory","commutative-algebra","finite-groups","graph-theory","group-theory","higher-group-theory","homotopy-type-theory","number-theory","order-theory","orthogonal-factorization-systems","ring-theory","species","structured-types","synthetic-homotopy-theory","trees","type-theories","univalent-combinatorics","univalent-foundations","univalent-mathematics","universal-algebra"],"latest_commit_sha":null,"homepage":"https://unimath.github.io/agda-unimath/","language":"Agda","has_issues":true,"has_wiki":null,"has_pages":null,"mirror_url":null,"source_name":null,"license":"mit","status":null,"scm":"git","pull_requests_enabled":true,"icon_url":"https://github.com/UniMath.png","metadata":{"files":{"readme":"README.md","changelog":null,"contributing":"CONTRIBUTING.md","funding":null,"license":"LICENSE.md","code_of_conduct":null,"threat_model":null,"audit":null,"citation":"CITATION.cff","codeowners":null,"security":null,"support":null,"governance":null,"roadmap":null,"authors":null,"dei":null,"publiccode":null,"codemeta":null,"zenodo":null,"notice":null,"maintainers":null,"copyright":null,"agents":null,"dco":null,"cla":null}},"created_at":"2021-11-19T20:31:01.000Z","updated_at":"2025-09-03T05:22:23.000Z","dependencies_parsed_at":"2023-01-17T13:15:48.943Z","dependency_job_id":"3b4cb851-d986-41ef-bf41-133ebbdc4df9","html_url":"https://github.com/UniMath/agda-unimath","commit_stats":{"total_commits":2095,"total_committers":46,"mean_commits":45.54347826086956,"dds":0.4343675417661098,"last_synced_commit":"6e87c58ef71c9a92666ba90c4ad522f137f2c382"},"previous_names":[],"tags_count":0,"template":false,"template_full_name":null,"purl":"pkg:github/UniMath/agda-unimath","repository_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/repositories/UniMath%2Fagda-unimath","tags_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/repositories/UniMath%2Fagda-unimath/tags","releases_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/repositories/UniMath%2Fagda-unimath/releases","manifests_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/repositories/UniMath%2Fagda-unimath/manifests","owner_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/owners/UniMath","download_url":"https://codeload.github.com/UniMath/agda-unimath/tar.gz/refs/heads/master","sbom_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/repositories/UniMath%2Fagda-unimath/sbom","scorecard":null,"host":{"name":"GitHub","url":"https://github.com","kind":"github","repositories_count":273768046,"owners_count":25164464,"icon_url":"https://github.com/github.png","version":null,"created_at":"2022-05-30T11:31:42.601Z","updated_at":"2022-07-04T15:15:14.044Z","status":"online","status_checked_at":"2025-09-05T02:00:09.113Z","response_time":402,"last_error":null,"robots_txt_status":"success","robots_txt_updated_at":"2025-07-24T06:49:26.215Z","robots_txt_url":"https://github.com/robots.txt","online":true,"can_crawl_api":true,"host_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub","repositories_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/repositories","repository_names_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/repository_names","owners_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/owners"}},"owner":{"login":"UniMath","name":"Univalent Mathematics","uuid":"6826454","kind":"organization","description":"A unified approach to formalization of mathematical knowledge based on Univalent Foundations.","email":null,"website":null,"location":null,"twitter":null,"company":null,"icon_url":"https://avatars.githubusercontent.com/u/6826454?v=4","repositories_count":21,"last_synced_at":"2024-04-20T00:47:10.927Z","metadata":{"has_sponsors_listing":false},"html_url":"https://github.com/UniMath","funding_links":[],"total_stars":1957,"followers":72,"following":0,"created_at":"2022-11-06T14:15:22.405Z","updated_at":"2024-04-20T00:47:21.795Z","owner_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/owners/UniMath","repositories_url":"https://repos.ecosyste.ms/api/v1/hosts/GitHub/owners/UniMath/repositories"},"packages":[],"commits":{"id":1359644,"full_name":"UniMath/agda-unimath","default_branch":"master","committers":[{"name":"Egbert Rijke","email":"e.m.rijke@gmail.com","login":null,"count":1185},{"name":"Fredrik Bakke","email":"fredrbak@gmail.com","login":null,"count":281},{"name":"Léo Mangel","email":"leo.mangel.prepa@gmail.com","login":null,"count":110},{"name":"Elisabeth Bonnevier","email":"elisabeth.bonnevier@uib.no","login":null,"count":86},{"name":"Jonathan Cubides","email":"jonathan.cubides@uib.no","login":null,"count":61},{"name":"Vojtěch Štěpančík","email":"vojtechstepancik@outlook.com","login":null,"count":46},{"name":"Raymond Baker","email":"raymondgarethbaker@gmail.com","login":null,"count":35},{"name":"Bryan Lu","email":"bryan.lu3@gmail.com","login":null,"count":34},{"name":"Tom de Jong","email":"43781735+tomdjong","login":"tomdjong","count":30},{"name":"fernando","email":"fernando.churiv@gmail.com","login":null,"count":28},{"name":"ElifUskuplu","email":"77177090+ElifUskuplu","login":"ElifUskuplu","count":25},{"name":"Raymond Baker","email":"96847663+morphismz","login":"morphismz","count":21},{"name":"VictorBlanchi","email":"76261859+VictorBlanchi","login":"VictorBlanchi","count":18},{"name":"Ian Ray","email":"ibray1115@gmail.com","login":null,"count":17},{"name":"Andreas Källberg","email":"anka.213@gmail.com","login":null,"count":16},{"name":"Matej Jazbec","email":"jazbec.matej@outlook.com","login":null,"count":12},{"name":"malarbol","email":"malarbol+git@gmail.com","login":null,"count":11},{"name":"Amélia Liao","email":"me@amelia.how","login":null,"count":10},{"name":"Elisabeth Bonnevier","email":"elisabeth@bonnevier.one","login":null,"count":10},{"name":"Eléonore Mangel","email":"eleonore.mangel@gmail.com","login":null,"count":8},{"name":"Daniel Gratzer","email":"danny.gratzer@gmail.com","login":null,"count":7},{"name":"maybemabeline","email":"142519092+maybemabeline","login":"maybemabeline","count":6},{"name":"Ivan Kobe","email":"ivan.kobe@gmail.com","login":null,"count":5},{"name":"Fernando Chu","email":"17756312+FernandoChu","login":"FernandoChu","count":5},{"name":"Elisabeth Bonnevier","email":"55891497+elisabethbonnevier","login":"elisabethbonnevier","count":2},{"name":"Alec Barreto","email":"108373766+wrest64","login":"wrest64","count":2},{"name":"favonia","email":"favonia@gmail.com","login":null,"count":2},{"name":"Ulrik Buchholtz","email":"ulrikbuchholtz@gmail.com","login":null,"count":2},{"name":"Masa Zaucer","email":"masa.zaucer@student.fmf.uni-lj.si","login":null,"count":2},{"name":"Alice Laroche","email":"aliceetampes@gmail.com","login":null,"count":2},{"name":"Aqissiaq","email":"aqissiaq@gmail.com","login":null,"count":1},{"name":"Dylan Braithwaite","email":"dylanbraithwaite1@gmail.com","login":null,"count":1},{"name":"Emily Riehl","email":"eriehl@math.jhu.edu","login":null,"count":1},{"name":"Erik Schnetter","email":"schnetter@gmail.com","login":null,"count":1},{"name":"szumixie","email":"39803844+szumixie","login":"szumixie","count":1},{"name":"louismntnu","email":"95856133+louismntnu","login":"louismntnu","count":1},{"name":"IanRay11","email":"71675731+IanRay11","login":"IanRay11","count":1},{"name":"Gregor Perčič","email":"102703503+GregorPercic","login":"GregorPercic","count":1},{"name":"Elisabeth Stenholm","email":"55891497+elisabethstenholm","login":"elisabethstenholm","count":1},{"name":"EleonoreMangel","email":"99205250+EleonoreMangel","login":"EleonoreMangel","count":1},{"name":"Håkon Gylterud","email":"hakon.gylterud@uib.no","login":null,"count":1},{"name":"Matthias Hutzler","email":"matthias-hutzler@posteo.net","login":null,"count":1},{"name":"Nathan van Doorn","email":"nvd1234@gmail.com","login":null,"count":1},{"name":"Pierre Cagne","email":"pierre.cagne@gmail.com","login":null,"count":1},{"name":"Szumi Xie","email":"szumixie@gmail.com","login":null,"count":1},{"name":"Tom de Jong","email":"tdejong.ac@gmail.com","login":null,"count":1}],"total_commits":2095,"total_committers":46,"total_bot_commits":0,"total_bot_committers":0,"mean_commits":45.54347826086956,"dds":0.4343675417661098,"past_year_committers":[{"name":"Fredrik Bakke","email":"fredrbak@gmail.com","login":null,"count":276},{"name":"Egbert Rijke","email":"e.m.rijke@gmail.com","login":null,"count":244},{"name":"Vojtěch Štěpančík","email":"vojtechstepancik@outlook.com","login":null,"count":46},{"name":"Jonathan Cubides","email":"jonathan.cubides@uib.no","login":null,"count":31},{"name":"Tom de Jong","email":"43781735+tomdjong","login":"tomdjong","count":30},{"name":"Raymond Baker","email":"96847663+morphismz","login":"morphismz","count":20},{"name":"VictorBlanchi","email":"76261859+VictorBlanchi","login":"VictorBlanchi","count":18},{"name":"Fernando Chu","email":"fernando.churiv@gmail.com","login":null,"count":13},{"name":"Raymond Baker","email":"raymondgarethbaker@gmail.com","login":null,"count":10},{"name":"maybemabeline","email":"142519092+maybemabeline","login":"maybemabeline","count":6},{"name":"Fernando Chu","email":"17756312+FernandoChu","login":"FernandoChu","count":5},{"name":"ElifUskuplu","email":"77177090+ElifUskuplu","login":"ElifUskuplu","count":4},{"name":"Ulrik Buchholtz","email":"ulrikbuchholtz@gmail.com","login":null,"count":2},{"name":"Elisabeth Bonnevier","email":"55891497+elisabethbonnevier","login":"elisabethbonnevier","count":2},{"name":"Alec Barreto","email":"108373766+wrest64","login":"wrest64","count":2},{"name":"EleonoreMangel","email":"99205250+EleonoreMangel","login":"EleonoreMangel","count":1},{"name":"Elisabeth Stenholm","email":"55891497+elisabethstenholm","login":"elisabethstenholm","count":1},{"name":"Gregor Perčič","email":"102703503+GregorPercic","login":"GregorPercic","count":1},{"name":"louismntnu","email":"95856133+louismntnu","login":"louismntnu","count":1},{"name":"Emily Riehl","email":"eriehl@math.jhu.edu","login":null,"count":1},{"name":"Matthias Hutzler","email":"matthias-hutzler@posteo.net","login":null,"count":1}],"past_year_total_commits":715,"past_year_total_committers":21,"past_year_total_bot_commits":0,"past_year_total_bot_committers":0,"past_year_mean_commits":34.04761904761905,"past_year_dds":0.613986013986014,"last_synced_at":"2024-01-26T03:08:33.355Z","last_synced_commit":"6e87c58ef71c9a92666ba90c4ad522f137f2c382","created_at":"2023-09-13T13:26:04.294Z","updated_at":"2024-01-26T03:08:33.356Z","commits_url":"https://commits.ecosyste.ms/api/v1/hosts/GitHub/repositories/UniMath%2Fagda-unimath/commits","host":{"name":"GitHub","url":"https://github.com","kind":"github","last_synced_at":"2025-09-05T00:00:10.343Z","repositories_count":5480019,"commits_count":853389012,"contributors_count":31098138,"owners_count":906558,"icon_url":"https://github.com/github.png","host_url":"https://commits.ecosyste.ms/api/v1/hosts/GitHub","repositories_url":"https://commits.ecosyste.ms/api/v1/hosts/GitHub/repositories"}},"issues_stats":{"full_name":"UniMath/agda-unimath","html_url":"https://github.com/UniMath/agda-unimath","last_synced_at":"2025-09-05T04:36:20.230Z","status":null,"issues_count":139,"pull_requests_count":732,"avg_time_to_close_issue":3517479.933333333,"avg_time_to_close_pull_request":1098311.6421404681,"issues_closed_count":45,"pull_requests_closed_count":598,"pull_request_authors_count":24,"issue_authors_count":12,"avg_comments_per_issue":1.2589928057553956,"avg_comments_per_pull_request":3.2759562841530054,"merged_pull_requests_count":540,"bot_issues_count":0,"bot_pull_requests_count":0,"past_year_issues_count":45,"past_year_pull_requests_count":330,"past_year_avg_time_to_close_issue":498935.6666666667,"past_year_avg_time_to_close_pull_request":627970.2222222222,"past_year_issues_closed_count":6,"past_year_pull_requests_closed_count":234,"past_year_pull_request_authors_count":13,"past_year_issue_authors_count":7,"past_year_avg_comments_per_issue":1.0222222222222221,"past_year_avg_comments_per_pull_request":1.9696969696969697,"past_year_bot_issues_count":0,"past_year_bot_pull_requests_count":0,"past_year_merged_pull_requests_count":200,"created_at":"2023-09-13T13:26:34.480Z","updated_at":"2025-09-05T04:36:20.232Z","repository_url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/repositories/UniMath%2Fagda-unimath","issues_url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/repositories/UniMath%2Fagda-unimath/issues","issue_labels_count":{"website":20,"good first issue":20,"help wanted":15,"bug":15,"synthetic-homotopy-theory":15,"CI":12,"enhancement":11,"refactoring":11,"foundation":11,"formalization-target":8,"documentation":7,"pre-commit":7,"tooling":5,"univalent-combinatorics":5,"category-theory":5,"group-theory":5,"cleanup":4,"real-numbers":4,"repo-maintenance":4,"question":3,"orthogonal-factorization-systems":3,"improve naming":2,"metric-spaces":2,"order-theory":2,"structured-types":2,"elementary-number-theory":2,"ring-theory":2,"1000+ theorems":1,"mathswitch":1,"logic":1,"computational-behavior":1,"fix":1,"set-theory":1,"commutative-algebra":1,"species":1,"guides":1,"organic-chemistry":1},"pull_request_labels_count":{"foundation":158,"synthetic-homotopy-theory":85,"refactoring":77,"real-numbers":53,"elementary-number-theory":53,"website":50,"fix":49,"category-theory":43,"group-theory":31,"order-theory":31,"CI":30,"repo-maintenance":26,"enhancement":26,"documentation":23,"univalent-combinatorics":22,"orthogonal-factorization-systems":19,"improve naming":18,"structured-types":17,"metric-spaces":15,"typo":13,"pre-commit":12,"logic":12,"ring-theory":11,"guides":10,"cleanup":9,"set-theory":9,"tooling":9,"experiment":8,"computational-behavior":8,"higher-group-theory":8,"wild-category-theory":7,"commutative-algebra":7,"bug":7,"100-theorems":6,"graph-theory":6,"do not merge":6,"trees":5,"modal-type-theory":5,"oeis":5,"reflection":5,"art":5,"question":5,"finite-group-theory":5,"formatting":4,"finite-algebra":4,"Wikipedia theorems":4,"100 theorems":3,"literature":3,"linear-algebra":3,"low-priority":3,"cat-sitting":2,"synthetic-category-theory":2,"🏆 milestone 🏆":2,"mage":2,"simplicial-type-theory":2,"formalization-target":2,"globular-types":2,"species":1,"domain-theory":1,"1000+ theorems":1,"type-theories":1,"mathswitch":1,"help wanted":1,"vscode":1,"good first issue":1},"issue_author_associations_count":{"COLLABORATOR":120,"CONTRIBUTOR":16,"NONE":3},"pull_request_author_associations_count":{"COLLABORATOR":491,"CONTRIBUTOR":233,"NONE":8},"issue_authors":{"fredrik-bakke":78,"lowasser":21,"VojtechStep":15,"EgbertRijke":14,"malarbol":3,"jonaprieto":2,"ElifUskuplu":1,"elisabethbonnevier":1,"morphismz":1,"djspacewhale":1,"ncfavier":1,"juhp":1},"pull_request_authors":{"fredrik-bakke":243,"lowasser":154,"EgbertRijke":127,"VojtechStep":85,"tomdjong":33,"malarbol":28,"djspacewhale":14,"morphismz":14,"FernandoChu":6,"maybemabeline":5,"ben-connors":4,"ivankobe":3,"arnoudvanderleer":2,"blu-bird":2,"UlrikBuchholtz":2,"GregorPercic":2,"bjarki781":1,"SimonBrandner":1,"dannypsnl":1,"elisabethstenholm":1,"spcfox":1,"wrest64":1,"ecavallo":1,"pitmonticone":1},"host":{"name":"GitHub","url":"https://github.com","kind":"github","last_synced_at":"2025-09-05T00:00:10.444Z","repositories_count":10098796,"issues_count":31459450,"pull_requests_count":97364286,"authors_count":10701971,"icon_url":"https://github.com/github.png","host_url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub","repositories_url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/repositories","owners_url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/owners","authors_url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors"},"past_year_issue_labels_count":{"website":5,"bug":5,"tooling":4,"CI":3,"real-numbers":3,"help wanted":3,"question":2,"order-theory":2,"improve naming":2,"refactoring":2,"formalization-target":2,"documentation":2,"metric-spaces":2,"pre-commit":1,"fix":1,"1000+ theorems":1,"mathswitch":1,"foundation":1,"repo-maintenance":1,"synthetic-homotopy-theory":1,"enhancement":1},"past_year_pull_request_labels_count":{"real-numbers":51,"foundation":39,"elementary-number-theory":37,"order-theory":25,"website":22,"fix":18,"refactoring":17,"univalent-combinatorics":16,"improve naming":14,"metric-spaces":14,"logic":11,"CI":11,"documentation":9,"enhancement":8,"typo":8,"set-theory":8,"repo-maintenance":7,"ring-theory":7,"category-theory":6,"100-theorems":6,"synthetic-homotopy-theory":6,"art":5,"experiment":5,"group-theory":5,"finite-group-theory":4,"oeis":4,"Wikipedia theorems":4,"orthogonal-factorization-systems":3,"linear-algebra":3,"pre-commit":3,"literature":3,"finite-algebra":3,"100 theorems":3,"wild-category-theory":3,"globular-types":2,"graph-theory":2,"structured-types":2,"reflection":2,"computational-behavior":2,"tooling":2,"commutative-algebra":2,"do not merge":1,"formalization-target":1,"formatting":1,"question":1,"trees":1,"synthetic-category-theory":1,"modal-type-theory":1,"1000+ theorems":1,"domain-theory":1,"species":1},"past_year_issue_author_associations_count":{"COLLABORATOR":32,"CONTRIBUTOR":11,"NONE":2},"past_year_pull_request_author_associations_count":{"COLLABORATOR":181,"CONTRIBUTOR":144,"NONE":4},"past_year_issue_authors":{"lowasser":21,"fredrik-bakke":17,"malarbol":3,"djspacewhale":1,"EgbertRijke":1,"ncfavier":1,"VojtechStep":1},"past_year_pull_request_authors":{"lowasser":154,"fredrik-bakke":92,"malarbol":20,"EgbertRijke":19,"VojtechStep":17,"djspacewhale":13,"ben-connors":4,"ivankobe":3,"blu-bird":2,"arnoudvanderleer":2,"SimonBrandner":1,"FernandoChu":1,"ecavallo":1},"maintainers":[{"login":"fredrik-bakke","count":321,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/fredrik-bakke"},{"login":"EgbertRijke","count":141,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/EgbertRijke"},{"login":"VojtechStep","count":79,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/VojtechStep"},{"login":"lowasser","count":51,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/lowasser"},{"login":"malarbol","count":15,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/malarbol"},{"login":"jonaprieto","count":2,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/jonaprieto"},{"login":"elisabethstenholm","count":1,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/elisabethstenholm"},{"login":"elisabethbonnevier","count":1,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/elisabethbonnevier"}],"active_maintainers":[{"login":"fredrik-bakke","count":109,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/fredrik-bakke"},{"login":"lowasser","count":51,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/lowasser"},{"login":"EgbertRijke","count":20,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/EgbertRijke"},{"login":"VojtechStep","count":18,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/VojtechStep"},{"login":"malarbol","count":15,"url":"https://issues.ecosyste.ms/api/v1/hosts/GitHub/authors/malarbol"}]},"events":null,"keywords":["category-theory","commutative-algebra","finite-groups","graph-theory","group-theory","higher-group-theory","homotopy-type-theory","number-theory","order-theory","orthogonal-factorization-systems","ring-theory","species","structured-types","synthetic-homotopy-theory","trees","type-theories","univalent-combinatorics","univalent-foundations","univalent-mathematics","universal-algebra"],"dependencies":[{"ecosystem":"actions","filepath":".github/workflows/ci.yaml","sha":null,"kind":"manifest","created_at":"2023-01-17T13:15:48.817Z","updated_at":"2023-01-17T13:15:48.817Z","repository_link":"https://github.com/UniMath/agda-unimath/blob/master/.github/workflows/ci.yaml","dependencies":[{"id":6994525025,"package_name":"styfle/cancel-workflow-action","ecosystem":"actions","requirements":"0.9.1","direct":true,"kind":"composite","optional":false},{"id":6994525026,"package_name":"actions/cache","ecosystem":"actions","requirements":"v2","direct":true,"kind":"composite","optional":false},{"id":6994525027,"package_name":"haskell/actions/setup","ecosystem":"actions","requirements":"v1","direct":true,"kind":"composite","optional":false},{"id":6994525028,"package_name":"actions/checkout","ecosystem":"actions","requirements":"v2","direct":true,"kind":"composite","optional":false},{"id":6994525029,"package_name":"r-lib/actions/setup-pandoc","ecosystem":"actions","requirements":"v1","direct":true,"kind":"composite","optional":false},{"id":6994525030,"package_name":"peaceiris/actions-gh-pages","ecosystem":"actions","requirements":"v3","direct":true,"kind":"composite","optional":false}]}],"score":9.878374851721052,"created_at":"2025-09-04T15:51:31.365Z","updated_at":"2025-10-07T08:21:56.581Z","avatar_url":"https://github.com/UniMath.png","language":"Agda","category":null,"sub_category":null,"monthly_downloads":0,"funding_links":[],"readme_doi_urls":[],"works":{},"citation_counts":{},"total_citations":0,"keywords_from_contributors":["agda","programming-language","cubical-type-theory","dependent-types","proof-assistant","type-theory","proof"],"project_url":"https://science.ecosyste.ms/api/v1/projects/55495","html_url":"https://science.ecosyste.ms/projects/55495","bibtex_url":"https://science.ecosyste.ms/projects/55495/export.bibtex","apalike_url":"https://science.ecosyste.ms/projects/55495/export.apalike"}