From 7b26b2ca83753da4dc8b474ff742118027130c93 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 09:13:43 +0200 Subject: [PATCH 01/19] #885: replace maintainer section in readme by a review-section also: remove gitter-link, add a link with an overview of the PRs that need reviewing --- README.md | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 9ba817846e..f61538360b 100644 --- a/README.md +++ b/README.md @@ -48,15 +48,23 @@ Huber, Anders Mörtberg. This makes it possible to directly represent higher inductive types. -Maintainers ------------ -* [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) +Reviewing of pull requests +-------------------------- +If you switch your draft pull request (PR) to 'ready to merge', +or directly create an open PR, +we should request a review, by one of the reviewers below. +If that doesn't happen, you can also request a review yourself, +to make us aware of the open PR. -* [Andrea Vezzosi](http://saizan.github.io/) +* [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) * [Evan Cavallo](https://staff.math.su.se/evan.cavallo/) -[![Build Status](https://travis-ci.org/agda/cubical.svg?branch=master)](https://travis-ci.org/agda/cubical) +* [Andrea Vezzosi](http://saizan.github.io/) (*inactive*) -[![Gitter](https://badges.gitter.im/agda/cubical.svg)](https://gitter.im/agda/cubical?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge) +* [Felix Cherubini](https://felix-cherubini.de) (*Limited roughly to algebra related topics*) + +[Overview of the current open PRs, descending time since last action](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse) + +[![Build Status](https://travis-ci.org/agda/cubical.svg?branch=master)](https://travis-ci.org/agda/cubical) From b7e55d012031d28037d40f7296592aebb7e25374 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 10:27:13 +0200 Subject: [PATCH 02/19] better grammar MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Anders Mörtberg --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index f61538360b..5d61deb32c 100644 --- a/README.md +++ b/README.md @@ -54,7 +54,7 @@ Reviewing of pull requests If you switch your draft pull request (PR) to 'ready to merge', or directly create an open PR, we should request a review, by one of the reviewers below. -If that doesn't happen, you can also request a review yourself, +If that doesn't happen, you can also request a reviewer yourself, to make us aware of the open PR. * [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) From 895e5dbcf13b7f5ed328010767c948054b7980dd Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 10:27:52 +0200 Subject: [PATCH 03/19] Better description MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Anders Mörtberg --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 5d61deb32c..7743f9e711 100644 --- a/README.md +++ b/README.md @@ -63,7 +63,7 @@ to make us aware of the open PR. * [Andrea Vezzosi](http://saizan.github.io/) (*inactive*) -* [Felix Cherubini](https://felix-cherubini.de) (*Limited roughly to algebra related topics*) +* [Felix Cherubini](https://felix-cherubini.de) (*Mainly algebra related topics*) [Overview of the current open PRs, descending time since last action](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse) From cc410973b01ec5f18f0196aaaeb7bc651013618c Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 10:28:55 +0200 Subject: [PATCH 04/19] more info on reviewer Anders MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Anders Mörtberg --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 7743f9e711..0fe1e1cd2c 100644 --- a/README.md +++ b/README.md @@ -57,7 +57,7 @@ we should request a review, by one of the reviewers below. If that doesn't happen, you can also request a reviewer yourself, to make us aware of the open PR. -* [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) +* [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) (*Most topics*) * [Evan Cavallo](https://staff.math.su.se/evan.cavallo/) From 496677e8193d33c8f32ea76038bb7fc810bce12c Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 11:06:10 +0200 Subject: [PATCH 05/19] #885: update list of reviewers according to suggestions --- README.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 0fe1e1cd2c..9449e72d39 100644 --- a/README.md +++ b/README.md @@ -61,10 +61,14 @@ to make us aware of the open PR. * [Evan Cavallo](https://staff.math.su.se/evan.cavallo/) -* [Andrea Vezzosi](http://saizan.github.io/) (*inactive*) - * [Felix Cherubini](https://felix-cherubini.de) (*Mainly algebra related topics*) +* [Max Zeuner](https://www.su.se/english/profiles/maze1512-1.450461) + +* [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) + +* [Andrea Vezzosi](http://saizan.github.io/) (*inactive*) + [Overview of the current open PRs, descending time since last action](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse) [![Build Status](https://travis-ci.org/agda/cubical.svg?branch=master)](https://travis-ci.org/agda/cubical) From a4d1941c9f09229f67372549719ac527bfec584c Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 11:14:29 +0200 Subject: [PATCH 06/19] #885: Refer to expertise info in reviewer list --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 9449e72d39..c059800e73 100644 --- a/README.md +++ b/README.md @@ -54,7 +54,7 @@ Reviewing of pull requests If you switch your draft pull request (PR) to 'ready to merge', or directly create an open PR, we should request a review, by one of the reviewers below. -If that doesn't happen, you can also request a reviewer yourself, +If that doesn't happen, you can also request a reviewer yourself (for reviewer expertise see below), to make us aware of the open PR. * [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) (*Most topics*) From 88360a769b09b929cad09df59ed76b086cc1e23c Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 11:16:11 +0200 Subject: [PATCH 07/19] #885: Expertise info for Axel and Max --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index c059800e73..a55bf4f49c 100644 --- a/README.md +++ b/README.md @@ -63,9 +63,9 @@ to make us aware of the open PR. * [Felix Cherubini](https://felix-cherubini.de) (*Mainly algebra related topics*) -* [Max Zeuner](https://www.su.se/english/profiles/maze1512-1.450461) +* [Max Zeuner](https://www.su.se/english/profiles/maze1512-1.450461) (*Algebra related topics*) -* [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) +* [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) (*Synthetic homotopy theory and cohomology*) * [Andrea Vezzosi](http://saizan.github.io/) (*inactive*) From 19525f39c0c43867742f87e9cf5f631ae7385488 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 11:18:01 +0200 Subject: [PATCH 08/19] Grammar --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index a55bf4f49c..3fedd65e70 100644 --- a/README.md +++ b/README.md @@ -67,7 +67,7 @@ to make us aware of the open PR. * [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) (*Synthetic homotopy theory and cohomology*) -* [Andrea Vezzosi](http://saizan.github.io/) (*inactive*) +* [Andrea Vezzosi](http://saizan.github.io/) (*Inactive*) [Overview of the current open PRs, descending time since last action](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse) From 4b63c41de529c22b58ddc3925b65adddff23b1f6 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 11:27:34 +0200 Subject: [PATCH 09/19] #885: Table of reviewers instead of list, with more info --- README.md | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index 3fedd65e70..7fe424ffca 100644 --- a/README.md +++ b/README.md @@ -57,17 +57,14 @@ we should request a review, by one of the reviewers below. If that doesn't happen, you can also request a reviewer yourself (for reviewer expertise see below), to make us aware of the open PR. -* [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) (*Most topics*) - -* [Evan Cavallo](https://staff.math.su.se/evan.cavallo/) - -* [Felix Cherubini](https://felix-cherubini.de) (*Mainly algebra related topics*) - -* [Max Zeuner](https://www.su.se/english/profiles/maze1512-1.450461) (*Algebra related topics*) - -* [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) (*Synthetic homotopy theory and cohomology*) - -* [Andrea Vezzosi](http://saizan.github.io/) (*Inactive*) +| Reviewer | github handle | Area of expertise | +|-------------------------------------------------------------------------|---------------|---------------------------------------------| +| [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) | [mortberg](https://github.com/mortberg) | *Most topics* | +| [Evan Cavallo](https://staff.math.su.se/evan.cavallo/) | [ecavallo](https://github.com/ecavallo) | | +| [Felix Cherubini](https://felix-cherubini.de) | [felixwellen](https://github.com/felixwellen) | *Mainly algebra related topics* | +| [Max Zeuner](https://www.su.se/english/profiles/maze1512-1.450461) | [mzeuner](https://github.com/mzeuner) | *Algebra related topics* | +| [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) | [aljungstrom](https://github.com/aljungstrom) | *Synthetic homotopy theory and cohomology* | +| [Andrea Vezzosi](http://saizan.github.io/) | [Saizan](https://github.com/Saizan) | *Inactive* | [Overview of the current open PRs, descending time since last action](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse) From 81233bba2fbd9871c383de61e574e4d10acbace0 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 11:30:35 +0200 Subject: [PATCH 10/19] Typo --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 7fe424ffca..922fe24c3c 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ can check out the tag `v0.1` of this library. For some introductory lecture notes see the material for the Cubical Agda course of the [EPIT 2021 spring school](https://github.com/HoTT/EPIT-2020/blob/main/04-cubical-type-theory/). -For a paper on with details about Cubical Agda, see [Cubical Agda: a dependently typed +For a paper with details about Cubical Agda, see [Cubical Agda: a dependently typed programming language with univalence and higher inductive types](https://dl.acm.org/doi/10.1145/3341691) by Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. From 94786b021e502b71502bde6ee037d8279ac297b3 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 11:33:23 +0200 Subject: [PATCH 11/19] #885: (Re-)organize README --- README.md | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 922fe24c3c..b30aa1542d 100644 --- a/README.md +++ b/README.md @@ -1,14 +1,16 @@ A standard library for Cubical Agda =================================== +The source code has a glorious clickable [rendered version](https://agda.github.io/cubical/Cubical.README.html). + +Compiling, using and installing +------------------------------- This library compiles with the latest official release of [Agda](https://github.com/agda/agda/). For detailed install instructions see the [INSTALL](https://github.com/agda/cubical/blob/master/INSTALL.md) file. -The source code has a glorious clickable [rendered version](https://agda.github.io/cubical/Cubical.README.html). - If you want to use Agda 2.6.2 instead of the latest release version, you can check out the tag `v0.3` of this library. @@ -18,6 +20,8 @@ can check out the tag `v0.2` of this library. If you want to use Agda 2.6.0.1 instead of the latest release version, you can check out the tag `v0.1` of this library. +Learning materials +------------------ For some introductory lecture notes see the material for the Cubical Agda course of the [EPIT 2021 spring school](https://github.com/HoTT/EPIT-2020/blob/main/04-cubical-type-theory/). @@ -30,6 +34,8 @@ For an introduction to this library, see this [blog post](https://homotopytypetheory.org/2018/12/06/cubical-agda/). Note that many files and results have moved since this blog post was written. +Theoretical background +---------------------- The type theory that Cubical Agda implements is a variation of the cubical type theory of: From f3067079bb0c174dbae60468e5e99273145fc700 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 11:34:33 +0200 Subject: [PATCH 12/19] Less color noise --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index b30aa1542d..c3f191e4e7 100644 --- a/README.md +++ b/README.md @@ -72,6 +72,6 @@ to make us aware of the open PR. | [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) | [aljungstrom](https://github.com/aljungstrom) | *Synthetic homotopy theory and cohomology* | | [Andrea Vezzosi](http://saizan.github.io/) | [Saizan](https://github.com/Saizan) | *Inactive* | -[Overview of the current open PRs, descending time since last action](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse) +[Overview](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse) of the current open PRs, descending time since last action. [![Build Status](https://travis-ci.org/agda/cubical.svg?branch=master)](https://travis-ci.org/agda/cubical) From a01d5af398b7950bc3adab821a394d86da9b0f8c Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 11:36:57 +0200 Subject: [PATCH 13/19] #885: Sort things in README by topic --- README.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index c3f191e4e7..b51ae5927e 100644 --- a/README.md +++ b/README.md @@ -25,17 +25,17 @@ Learning materials For some introductory lecture notes see the material for the Cubical Agda course of the [EPIT 2021 spring school](https://github.com/HoTT/EPIT-2020/blob/main/04-cubical-type-theory/). -For a paper with details about Cubical Agda, see [Cubical Agda: a dependently typed -programming language with univalence and higher inductive -types](https://dl.acm.org/doi/10.1145/3341691) by Andrea Vezzosi, Anders -Mörtberg, and Andreas Abel. - For an introduction to this library, see this [blog post](https://homotopytypetheory.org/2018/12/06/cubical-agda/). Note that many files and results have moved since this blog post was written. Theoretical background ---------------------- +For a paper with details about Cubical Agda, see [Cubical Agda: a dependently typed +programming language with univalence and higher inductive +types](https://dl.acm.org/doi/10.1145/3341691) by Andrea Vezzosi, Anders +Mörtberg, and Andreas Abel. + The type theory that Cubical Agda implements is a variation of the cubical type theory of: From 44ba855272ade2507b8a3f72f868a113672d0d44 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 11 Aug 2022 15:12:50 +0200 Subject: [PATCH 14/19] #885; Links to review queues --- README.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index b51ae5927e..0f86382bd1 100644 --- a/README.md +++ b/README.md @@ -63,14 +63,14 @@ we should request a review, by one of the reviewers below. If that doesn't happen, you can also request a reviewer yourself (for reviewer expertise see below), to make us aware of the open PR. -| Reviewer | github handle | Area of expertise | -|-------------------------------------------------------------------------|---------------|---------------------------------------------| -| [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) | [mortberg](https://github.com/mortberg) | *Most topics* | -| [Evan Cavallo](https://staff.math.su.se/evan.cavallo/) | [ecavallo](https://github.com/ecavallo) | | -| [Felix Cherubini](https://felix-cherubini.de) | [felixwellen](https://github.com/felixwellen) | *Mainly algebra related topics* | -| [Max Zeuner](https://www.su.se/english/profiles/maze1512-1.450461) | [mzeuner](https://github.com/mzeuner) | *Algebra related topics* | -| [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) | [aljungstrom](https://github.com/aljungstrom) | *Synthetic homotopy theory and cohomology* | -| [Andrea Vezzosi](http://saizan.github.io/) | [Saizan](https://github.com/Saizan) | *Inactive* | +| Reviewer | github handle | Area of expertise | Queue | +|-------------------------------------------------------------------------|---------------|---------------------------------------------|------| +| [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) | [mortberg](https://github.com/mortberg) | *Most topics* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Amortberg+) | +| [Evan Cavallo](https://staff.math.su.se/evan.cavallo/) | [ecavallo](https://github.com/ecavallo) | | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Aecavallo+) | +| [Felix Cherubini](https://felix-cherubini.de) | [felixwellen](https://github.com/felixwellen) | *Mainly algebra related topics* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Afelixwellen+) | +| [Max Zeuner](https://www.su.se/english/profiles/maze1512-1.450461) | [mzeuner](https://github.com/mzeuner) | *Algebra related topics* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Amzeuner+) | +| [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) | [aljungstrom](https://github.com/aljungstrom) | *Synthetic homotopy theory and cohomology* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Aaljungstrom+) | +| [Andrea Vezzosi](http://saizan.github.io/) | [Saizan](https://github.com/Saizan) | *Inactive* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3ASaizan+) | [Overview](https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse) of the current open PRs, descending time since last action. From 6d39651d1e21a675abba2bccefb5976e7b01daf3 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Fri, 12 Aug 2022 14:05:42 +0200 Subject: [PATCH 15/19] Add link to discord channel --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 0f86382bd1..ec222c950f 100644 --- a/README.md +++ b/README.md @@ -3,6 +3,8 @@ A standard library for Cubical Agda The source code has a glorious clickable [rendered version](https://agda.github.io/cubical/Cubical.README.html). +[Discord](https://discord.gg/5c7ZDMFn). + Compiling, using and installing ------------------------------- This library compiles with the latest official release of From 590a51745d4d98d57d0a547228e48239dc816101 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Fri, 12 Aug 2022 14:07:07 +0200 Subject: [PATCH 16/19] Add evans area of expertise --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index ec222c950f..8afcc4ddae 100644 --- a/README.md +++ b/README.md @@ -68,7 +68,7 @@ to make us aware of the open PR. | Reviewer | github handle | Area of expertise | Queue | |-------------------------------------------------------------------------|---------------|---------------------------------------------|------| | [Anders Mörtberg](https://staff.math.su.se/anders.mortberg/) | [mortberg](https://github.com/mortberg) | *Most topics* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Amortberg+) | -| [Evan Cavallo](https://staff.math.su.se/evan.cavallo/) | [ecavallo](https://github.com/ecavallo) | | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Aecavallo+) | +| [Evan Cavallo](https://staff.math.su.se/evan.cavallo/) | [ecavallo](https://github.com/ecavallo) | *Most topics* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Aecavallo+) | | [Felix Cherubini](https://felix-cherubini.de) | [felixwellen](https://github.com/felixwellen) | *Mainly algebra related topics* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Afelixwellen+) | | [Max Zeuner](https://www.su.se/english/profiles/maze1512-1.450461) | [mzeuner](https://github.com/mzeuner) | *Algebra related topics* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Amzeuner+) | | [Axel Ljungström](https://www.su.se/english/profiles/axlj4439-1.450268) | [aljungstrom](https://github.com/aljungstrom) | *Synthetic homotopy theory and cohomology* | [link](https://github.com/agda/cubical/pulls?q=is%3Apr+review-requested%3Aaljungstrom+) | From ea3399248b5a2918c82568b973835d15d391697f Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 15 Aug 2022 11:00:46 +0200 Subject: [PATCH 17/19] #885: more details on the discord server --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 8afcc4ddae..7de48d1482 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ A standard library for Cubical Agda The source code has a glorious clickable [rendered version](https://agda.github.io/cubical/Cubical.README.html). -[Discord](https://discord.gg/5c7ZDMFn). +There is also a [discord server](https://discord.gg/5c7ZDMFn), shared with [agda-unimath](https://unimath.github.io/agda-unimath/) and the [1lab](https://1lab.dev/). Compiling, using and installing ------------------------------- From 8feb2c7b54baffd636d229f56f0688554bdb5a93 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Fri, 19 Aug 2022 10:55:17 +0200 Subject: [PATCH 18/19] Update README.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Anders Mörtberg --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 7de48d1482..3e05b39b19 100644 --- a/README.md +++ b/README.md @@ -63,7 +63,7 @@ If you switch your draft pull request (PR) to 'ready to merge', or directly create an open PR, we should request a review, by one of the reviewers below. If that doesn't happen, you can also request a reviewer yourself (for reviewer expertise see below), -to make us aware of the open PR. +to make us aware of the open PR. Feel free to use Discord to get in touch with a reviewer in case reviewing is taking a very long time. | Reviewer | github handle | Area of expertise | Queue | |-------------------------------------------------------------------------|---------------|---------------------------------------------|------| From 9ebaebe8294133a6f7694a7204f599c2488e2250 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Fri, 19 Aug 2022 11:17:51 +0200 Subject: [PATCH 19/19] add material from hottest summer school --- README.md | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 3e05b39b19..4eff1d6952 100644 --- a/README.md +++ b/README.md @@ -24,12 +24,17 @@ can check out the tag `v0.1` of this library. Learning materials ------------------ -For some introductory lecture notes see the material for the Cubical Agda course -of the [EPIT 2021 spring school](https://github.com/HoTT/EPIT-2020/blob/main/04-cubical-type-theory/). +* Introductory material from the HoTTest summer school: + [literate agda files](https://github.com/martinescardo/HoTTEST-Summer-School/tree/main/Agda/Cubical) + [recordings on youtube](https://www.youtube.com/channel/UC-9jDbJ-HegCFuWuam1SfvQ) + +* For an introduction to this library, see this [blog + post](https://homotopytypetheory.org/2018/12/06/cubical-agda/). Note that many + files and results have moved since this blog post was written. + +* For some introductory lecture notes see the material for the Cubical Agda course + of the [EPIT 2021 spring school](https://github.com/HoTT/EPIT-2020/blob/main/04-cubical-type-theory/). -For an introduction to this library, see this [blog -post](https://homotopytypetheory.org/2018/12/06/cubical-agda/). Note that many -files and results have moved since this blog post was written. Theoretical background ----------------------