From ac1467c4755629aa73d6a2364fd1aacdb041e069 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 6 Oct 2023 14:51:29 +0200 Subject: [PATCH 01/19] update typechecking commands --- .vscode/tasks.json | 4 ++-- README.md | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.vscode/tasks.json b/.vscode/tasks.json index a4ad0809..3642d5f0 100644 --- a/.vscode/tasks.json +++ b/.vscode/tasks.json @@ -5,9 +5,9 @@ "tasks": [ { "label": "typecheck", - "type": "shell", + "type": "process", "command": "rzk", - "args": ["typecheck", "src/hott/*", "src/simplicial-hott/*"], + "args": ["typecheck"], "problemMatcher": [], "group": { "kind": "build", diff --git a/README.md b/README.md index 927c3ecb..8c7fd1ce 100644 --- a/README.md +++ b/README.md @@ -38,7 +38,7 @@ Install the assistant. Then run the following command from the root of this repository: ```sh -rzk typecheck src/hott/* src/simplicial-hott/* +rzk typecheck ``` # References From ba6da6e5c605e999b7ba7c15fbd07d107425f910 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 6 Oct 2023 14:52:00 +0200 Subject: [PATCH 02/19] fix file references --- src/simplicial-hott/05-segal-types.rzk.md | 14 +++++++------- src/simplicial-hott/06-2cat-of-segal-types.rzk.md | 8 ++++---- src/simplicial-hott/07-discrete.rzk.md | 13 +++++++------ src/simplicial-hott/08-covariant.rzk.md | 11 ++++++----- src/simplicial-hott/09-yoneda.rzk.md | 10 +++++----- src/simplicial-hott/12-cocartesian.rzk.md | 14 +++++++------- 6 files changed, 36 insertions(+), 34 deletions(-) diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md index 6f2d33e4..99cedd49 100644 --- a/src/simplicial-hott/05-segal-types.rzk.md +++ b/src/simplicial-hott/05-segal-types.rzk.md @@ -10,14 +10,14 @@ This is a literate `rzk` file: ## Prerequisites -- `hott/1-paths.md` - We require basic path algebra. -- `hott/2-contractible.md` - We require the notion of contractible types and - their data. +- `hott/01-paths.rzk.md` - We require basic path algebra. +- `hott/02-contractible.rzk.md` - We require the notion of contractible types + and their data. - `hott/total-space.md` — We rely on `#!rzk is-equiv-projection-contractible-fibers` and `#!rzk total-space-projection` in the proof of Theorem 5.5. -- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and their - subshapes. +- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and + their subshapes. - `03-extension-types.rzk.md` — We use the fubini theorem and extension extensionality. @@ -1775,8 +1775,8 @@ The cofibration Λ²₁ → Δ² is inner anodyne ## Products of Segal Types -This is an additional section which describes morphisms in products of types as products of morphisms. -It is implicitly stated in Proposition 8.21. +This is an additional section which describes morphisms in products of types as +products of morphisms. It is implicitly stated in Proposition 8.21. ```rzk #section morphisms-of-products-is-products-of-morphisms diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 85ddd775..38fd8f9b 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -10,10 +10,10 @@ This is a literate `rzk` file: ## Prerequisites -- `3-simplicial-type-theory.md` — We rely on definitions of simplicies and their - subshapes. -- `4-extension-types.md` — We use extension extensionality. -- `5-segal-types.md` - We use the notion of hom types. +- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and + their subshapes. +- `04-extension-types.rzk.md` — We use extension extensionality. +- `05-segal-types.rzk.md` - We use the notion of hom types. Some of the definitions in this file rely on function extensionality and extension extensionality: diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md index 89aee5d3..7d3bb27e 100644 --- a/src/simplicial-hott/07-discrete.rzk.md +++ b/src/simplicial-hott/07-discrete.rzk.md @@ -10,12 +10,13 @@ This is a literate `rzk` file: ## Prerequisites -- `hott/1-paths.md` - We require basic path algebra. -- `hott/4-equivalences.md` - We require the notion of equivalence between types. -- `3-simplicial-type-theory.md` — We rely on definitions of simplicies and their - subshapes. -- `4-extension-types.md` — We use extension extensionality. -- `5-segal-types.md` - We use the notion of hom types. +- `hott/01-paths.rzk.md` - We require basic path algebra. +- `hott/04-equivalences.rzk.md` - We require the notion of equivalence between + types. +- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and + their subshapes. +- `04-extension-types.rzk.md` — We use extension extensionality. +- `05-segal-types.rzk.md` - We use the notion of hom types. Some of the definitions in this file rely on function extensionality and extension extensionality: diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index a40c8cb1..e00e4679 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -12,12 +12,13 @@ This is a literate `rzk` file: - `hott/*` - We require various prerequisites from homotopy type theory, for instance the notion of contractible types. -- `3-simplicial-type-theory.md` — We rely on definitions of simplicies and their - subshapes. -- `4-extension-types.md` — We use Theorem 4.1, an equivalence between lifts. -- `5-segal-types.md` - We make use of the notion of Segal types and their +- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and + their subshapes. +- `04-extension-types.rzk.md` — We use Theorem 4.1, an equivalence between + lifts. +- `05-segal-types.rzk.md` - We make use of the notion of Segal types and their structures. -- `6-contractible.md` - We make use of weak function extensionality. +- `06-contractible.rzk.md` - We make use of weak function extensionality. Some of the definitions in this file rely on extension extensionality: diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md index 605065f3..ba2c4140 100644 --- a/src/simplicial-hott/09-yoneda.rzk.md +++ b/src/simplicial-hott/09-yoneda.rzk.md @@ -12,12 +12,12 @@ This is a literate `rzk` file: - `hott/*` - We require various prerequisites from homotopy type theory, for instance the axiom of function extensionality. -- `3-simplicial-type-theory.md` — We rely on definitions of simplicies and their - subshapes. -- `4-extension-types.md` — We use the fubini theorem and extension +- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and + their subshapes. +- `04-extension-types.rzk.md` — We use the fubini theorem and extension extensionality. -- `5-segal-types.md` - We make heavy use of the notion of Segal types -- `8-covariant.md` - We use covariant type families. +- `05-segal-types.rzk.md` - We make heavy use of the notion of Segal types +- `08-covariant.rzk.md` - We use covariant type families. Some of the definitions in this file rely on function extensionality and extension extensionality: diff --git a/src/simplicial-hott/12-cocartesian.rzk.md b/src/simplicial-hott/12-cocartesian.rzk.md index 5b056eb2..6d3d2164 100644 --- a/src/simplicial-hott/12-cocartesian.rzk.md +++ b/src/simplicial-hott/12-cocartesian.rzk.md @@ -16,12 +16,12 @@ This is a literate `rzk` file: - `hott/*` - We require various prerequisites from homotopy type theory, for instance the axiom of function extensionality. -- `3-simplicial-type-theory.md` — We rely on definitions of simplicies and their - subshapes. -- `4-extension-types.md` — We use the fubini theorem and extension +- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and + their subshapes. +- `04-extension-types.rzk.md` — We use the fubini theorem and extension extensionality. -- `5-segal-types.md` - We make heavy use of the notion of Segal types -- `10-rezk-types.md`- We use Rezk types. +- `05-segal-types.rzk.md` - We make heavy use of the notion of Segal types +- `10-rezk-types.rzk.md`- We use Rezk types. ## (Iso-)Inner families @@ -94,8 +94,8 @@ a given starting point in the fiber. ## Cocartesian family -A family over cocartesian if it is isoinner and any arrow in -the has a cocartesian lift, given a point in the fiber over the domain. +A family over cocartesian if it is isoinner and any arrow in the has a +cocartesian lift, given a point in the fiber over the domain. ```rzk title="BW23, Definition 5.2.1" #def has-cocartesian-lifts From 7eb3134e01bddb706b00daf3d4191422a5ef1c7f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 6 Oct 2023 20:38:48 +0200 Subject: [PATCH 03/19] sentence case in headers --- README.md | 6 +++--- src/hott/04-half-adjoint-equivalences.rzk.md | 2 +- src/hott/10-trivial-fibrations.rzk.md | 6 +++--- src/index.md | 2 +- src/simplicial-hott/02-simplicial-type-theory.rzk.md | 2 +- src/simplicial-hott/05-segal-types.rzk.md | 4 ++-- src/simplicial-hott/09-yoneda.rzk.md | 2 +- 7 files changed, 12 insertions(+), 12 deletions(-) diff --git a/README.md b/README.md index 8c7fd1ce..8401aa7d 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ results from the following papers: - "[Limits and colimits of synthetic ∞-categories](https://arxiv.org/abs/2202.12386)" [3] -This formalization project follows the philosophy layed out in the article +This formalization project follows the philosophy laid out in the article "[Could ∞-category theory be taught to undergraduates?](https://www.ams.org/journals/notices/202305/noti2692/noti2692.html)" [4]. @@ -29,9 +29,9 @@ variant of type theory with shapes. See the list of contributors at The formalizations can be viewed as markdown files rendered at [rzk-lang.github.io/sHoTT/](https://rzk-lang.github.io/sHoTT/) using syntax highlighting supplied by -[MkDocs plugin for rzk](https://github.com/rzk-lang/mkdocs-plugin-rzk). +[MkDocs plugin for Rzk](https://github.com/rzk-lang/mkdocs-plugin-rzk). -## Checking the Formalisations Locally +## Checking the formalisations locally Install the [`rzk`](https://rzk-lang.github.io/rzk/latest/getting-started/install/) proof diff --git a/src/hott/04-half-adjoint-equivalences.rzk.md b/src/hott/04-half-adjoint-equivalences.rzk.md index b26e911f..72c15810 100644 --- a/src/hott/04-half-adjoint-equivalences.rzk.md +++ b/src/hott/04-half-adjoint-equivalences.rzk.md @@ -1,4 +1,4 @@ -# 4. Half Adjoint Equivalences +# 4. Half adjoint equivalences This is a literate `rzk` file: diff --git a/src/hott/10-trivial-fibrations.rzk.md b/src/hott/10-trivial-fibrations.rzk.md index 18142338..1aca6edb 100644 --- a/src/hott/10-trivial-fibrations.rzk.md +++ b/src/hott/10-trivial-fibrations.rzk.md @@ -1,4 +1,4 @@ -# 10. Trivial Fibrations +# 10. Trivial fibrations This is a literate `rzk` file: @@ -230,13 +230,13 @@ Finally, we have: #def contractible-fibers-is-equiv-projection ( A : U) ( B : A → U) - ( proj-B-to-A-is-equiv + ( is-equiv-total-space-projection : is-equiv (Σ (x : A) , B x) A (total-space-projection A B)) : contractible-fibers A B := contractible-fibers-is-half-adjoint-equiv-projection A B ( is-half-adjoint-equiv-is-equiv (Σ (x : A) , B x) A - ( total-space-projection A B) proj-B-to-A-is-equiv) + ( total-space-projection A B) is-equiv-total-space-projection) ``` ```rzk title="The main theorem" diff --git a/src/index.md b/src/index.md index 3a94a1bb..8eaaf5d6 100644 --- a/src/index.md +++ b/src/index.md @@ -26,7 +26,7 @@ variant of type theory with shapes. See the list of contributors to this formalisation project at [`CONTRIBUTORS.md`](CONTRIBUTORS.md). -## Checking the Formalisations Locally +## Checking the formalisations locally It is recommended to use [VS Code extension for Rzk](https://rzk-lang.github.io/rzk/v0.6.2/getting-started/install/) diff --git a/src/simplicial-hott/02-simplicial-type-theory.rzk.md b/src/simplicial-hott/02-simplicial-type-theory.rzk.md index 998738c3..24c1d77a 100644 --- a/src/simplicial-hott/02-simplicial-type-theory.rzk.md +++ b/src/simplicial-hott/02-simplicial-type-theory.rzk.md @@ -185,7 +185,7 @@ The union of shapes is defined by disjunction on topes. := \ t → ψ t ∨ χ t ``` -### Connection Squares +### Connection squares diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md index 99cedd49..f9548f84 100644 --- a/src/simplicial-hott/05-segal-types.rzk.md +++ b/src/simplicial-hott/05-segal-types.rzk.md @@ -493,7 +493,7 @@ is exactly `#!rzk horn-restriction A`. ( h))) ( equiv-horn-restriction A)) ( horn-restriction A , is-local-horn-inclusion-A))) - ( horn A x y z f g) + ( horn A x y z f g) ``` We have now proven that both notions of Segal types are logically equivalent. @@ -1773,7 +1773,7 @@ The cofibration Λ²₁ → Δ² is inner anodyne ( h^ A h)) ``` -## Products of Segal Types +## Products of Segal types This is an additional section which describes morphisms in products of types as products of morphisms. It is implicitly stated in Proposition 8.21. diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md index ba2c4140..4e5c3dfd 100644 --- a/src/simplicial-hott/09-yoneda.rzk.md +++ b/src/simplicial-hott/09-yoneda.rzk.md @@ -596,7 +596,7 @@ equivalence. ( contra-yon-evid A is-segal-A a C is-contravariant-C))) ``` -## Contravariant Naturality +## Contravariant naturality The equivalence of the Yoneda lemma is natural in both `#!rzk a : A` and `#!rzk C : A → U`. From 027b9fcfc0590301b6016c7a96344d9a3d22421b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 6 Oct 2023 20:39:08 +0200 Subject: [PATCH 04/19] first additions `STYLEGUIDE.md` --- src/STYLEGUIDE.md | 191 ++++++++++++++++++++++++++-------------------- 1 file changed, 107 insertions(+), 84 deletions(-) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index 2eebd32a..5fc76849 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -1,7 +1,9 @@ # Style guide and design principles This guide provides a set of design principles and guidelines for the `sHoTT` -project. Our style and design principles borrows heavily from +project. + +Our style and design principles borrows heavily from [`agda-unimath`](https://github.com/UniMath/agda-unimath). ## The structure of code @@ -17,7 +19,8 @@ The general format of a definition is as follows: ( p : x = y) ( q : y = z) : (x = z) - := idJ (A , y , \ z' q' → (x = z') , p , z , q) + := + ind-path A y (\ z' q' → (x = z')) p z q ``` - We start with the name, and place every assumption on a new line. @@ -30,24 +33,23 @@ The general format of a definition is as follows: not fit on a single line, we immediately insert a new line after the walrus separator and indent the code an extra level (2 spaces). -(Currently just taken from agda-unimath and adapted to Rzk) In Rzk, every -construction is structured like a tree, where each operation can be seen as a -branching point. We use indentation levels and parentheses to highlight this -structure, which makes the code feel more organized and understandable. For -example, when a definition part extends beyond a line, we introduce line breaks -at the earliest branching point, clearly displaying the tree structure of the -definition. This allows the reader to follow the branches of the tree, and to -visually grasp the scope of each operation and argument. Consider the following -example about Segal types: +In the Rzk language, every construction is structured like a tree, where each +operation can be seen as a branching point. We use indentation levels and +parentheses to highlight this structure, which makes the code more organized and +readable. For example, when part of a definition extends beyond a single line, +we introduce line breaks at the earliest branching point, clearly displaying the +tree structure of the definition. This allows the reader to follow the branches +of the tree, and to visually grasp the scope of each operation and argument. +Consider the following example about Segal types: ```rzk #def is-segal-is-local-horn-inclusion ( A : U) ( is-local-horn-inclusion-A : is-local-horn-inclusion A) - : isSegal A + : is-segal A := \ x y z f g → - projection-equiv-contractible-fibers + contractible-fibers-is-equiv-projection ( Λ → A) ( \ k → Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂))) , @@ -57,8 +59,8 @@ example about Segal types: ( \ t → k (1₂ , t)) ( h))) ( second - ( comp-equiv - ( Σ ( k : Λ → A ) , + ( equiv-comp + ( Σ ( k : Λ → A) , Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂))) , ( hom2 A ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂)) @@ -85,10 +87,10 @@ The root here is the function `projection-equiv-contractible-fibers`. It takes four arguments, each starting on a fresh line and is indented an extra level from the root. The first argument fits neatly on one line, but the second one is too large. In these cases, we add a line break right after the `→`-symbol -following the lambda-abstraction, which is the earliest branching point in this -case. The next node is again `Σ`, with two arguments. The first one fits on a -line, but the second does not, so we add a line break between them. This process -is continued until the definition is complete. +following the lambda-abstraction, which we consider the earliest branching point +in this case. The next node is again `Σ`, with two arguments. The first one fits +on a line, but the second does not, so we add a line break between them. This +process is continued until the definition is complete. Note also that we use parentheses to mark the branches. The extra space after the opening parentheses marking a branch is there to visually emphasize the tree @@ -97,25 +99,38 @@ two-space indentation level increases. ## Naming conventions -- As a main strategy, we strive to keep a tight connection between names of - constructions and their types. Take for instance [...]. - > - Add example - > - prepending assumptions and then conclusion - > - See agda-unimath's description - > - > We start with the initial assumption, then, working our way to the - > > conclusion, prepending every central assumption to the name, and finally - > > the conclusion. So for instance the name `iso-is-initial-is-segal` - > > should read like we get an iso of something which is initial given that - > > something is Segal. The true reading should then be obvious. - > - > > The naming conventions are aimed at improving the readability of the code, - > > not to ensure the shortest possible names, nor to minimize the amount of - > > typing by the implementers of the library. -- We mainly use lower case names with words separated by hyphens. -- Capitalized names are reserved for subuniverses and similar collections. When +Adhering to a good naming convention is essential for keeping the library +navigable and maintainable, and helps you make progress with your formalization +goals. Good names provide concise descriptions of an entry's purpose, and help +making the code in the library readable. + +- Entry names aim to concisely describe their mathematical concept, using + well-known mathematical vocabulary. +- While an entry's name reflects its concept, it avoids relying on the details + of its formalization. This way, a user is not required to know how something + is formalized in order to reference an entry. +- Even with only minimal knowledge of the conventions, readers should be able to + intuitively grasp an entry's purpose from its name. +- The naming conventions should apply regardless of topic or subfield. +- For many common kinds of entries, our naming conventions should offer a + predictable suggestion of what its name should be. +- Ultimately, our goal is for these conventions to support clear and + maintainable code. + +> - Add example +> - prepending assumptions and then conclusion. General format of names +> +> > The naming conventions are aimed at improving the readability of the code, +> > not to ensure the shortest possible names, nor to minimize the amount of +> > typing by the implementers of the library. + +> - We mainly use lower case names with words separated by hyphens. + +- Capitalized names are reserved for subuniverses and similar "namespaces". When a construction is made internally to such a collection, we _append_ its name. - For instance, the subuniverse of Segal types is called `Segal`, and its - internal hom, called `function-type-Segal,` has the following signature: + For instance, the subuniverse of Segal types is called `Segal`, and the + function type formation in that subuniverse , called `function-type-Segal,` + has the following signature: ```rzk #def function-type-Segal @@ -129,70 +144,78 @@ two-space indentation level increases. - For technical lemmas or definitions, where the chance they will be reused is very low, the specific names do not matter as much. In these cases, one may - resort to a simplified naming scheme, like enumeration. Please note, however, - that if you find yourself appealing to this convention frequently, that is a - sign that your code should be refactored. + resort to a simplified naming scheme, like enumeration. Please keep in mind, + however, that if you find yourself appealing to this convention frequently, + that is a sign that your code should be refactored. -- We use Unicode symbols sparingly and only when they align with established - mathematical practice. +- We use Unicode symbols in names very sparingly and only when they align with + established mathematical practice. ## Use of Unicode characters -In the defined names we use Unicode symbols sparingly and only when they align -with established mathematical practice. +In defined names we use Unicode symbols sparingly and only when they align with +established mathematical practice. For the builtin syntactic features of `rzk`, +however, we prefer the following Unicode symbols: -For the builtin syntactic features of `rzk` we use the following Unicode -symbols: +- `→` should be used instead of `->` (`\to`) +- `↦` should be used instead of`|->` (`\mapsto`) +- `≡` should be used instead of `===` (`\equiv`) +- `≤` should be used instead of `<=` (`\<=`) +- `∧` should be used instead of `/\` (`\and`) +- `∨` should be used instead of `\/` (`\or`) +- `0₂` should be used instead of `0_2` (`0\2`) +- `1₂` should be used instead of `1_2` (`1\2`) +- `I × J` should be used instead of `I * J` (`\x` or `\times`) -- `->` should be always replaced with `→` (`\to`) -- `|->` should be always replaced with `↦` (`\mapsto`) -- `===` should be always replaced with `≡` (`\equiv`) -- `<=` should be always replaced with `≤` (`\<=`) -- `/\` should be always replaced with `∧` (`\and`) -- `\/` should be always replaced with `∨` (`\or`) -- `0_2` should be always replaced with `0₂` (`0\2`) -- `1_2` should be always replaced with `1₂` (`1\2`) -- `I * J` should be always replaced with `I × J` (`\x` or `\times`) +!!! info -We use ASCII versions for `TOP` and `BOT` since `⊤` and `⊥` do not read better -in the code. Same for `first` and `second` (`π₁` and `π₂` are not very -readable). For the latter a lot of uses for projections should go away by using -pattern matching (and `let`/`where` in the future). + For `first`, `second`, `TOP` and `BOT`, we prefer the ASCII versions as + opposed to `π₁`, `π₂`, `⊤` and `⊥`, as we find the latter don't read too + well in the code. Please also note that we usually prefer the use of + named projections for special Sigma-types when these are defined. -## Use of Comments +## Use of comments -> We do not explicitly ban code comments, but our other conventions should -> heavily limit their need. -> -> - [ ] Literate file format for prose -> - [ ] Descriptive definition names shouldn't need additional explanation -> - [ ] Strictly organized code to ease reading and understanding -> - [ ] Essential information should be carried by code, not only comments -> -> Still, code annotations may find their uses. -> -> Where to place literature references? +Since we are using literate file formats, the need for comments in the code +should be heavily limited. If you feel the need to comment your code, then +please consider the following: + +- Descriptive names for definitions should make their use self-documenting. If + you are finding that you want to explain an application of a definition, + consider giving it a better name, or creating an intermediate definition with + a name that better describes your current aplication. -- Create and use named projections instead of using the `first` and `second` - projections. In many cases, their meaning is not immediately obvious, and so - one could be tempted to annotate the code with their meaning using comments. + In particular, if a particular family of Sigma types is given a name, we + prefer to also create and use named projections instead of `first` and + `second`. In many cases, their meaning is not immediately obvious, and so one + could be tempted to annotate the code with their meaning using comments. For instance, instead of writing `first (second is-invertible-f)`, we define a named projection `is-section-is-invertible`. This may then be used as - `is-section-is-invertible A B f is-invertible-f` in other places. This way, - the code becomes self-documenting, and much easier to read. + `is-section-is-invertible A B f is-invertible-f` elsewhere. This way, the code + becomes self-documenting, and much easier to read. However, we recognize that in `rzk`, since we do not have the luxury of implicit arguments, this may sometimes cause unnecessarily verbose code. In such cases, you may revert to using `first` and `second`. -## Adapting and Evolving the Style Guide +- Can your code be structured in a way that makes it more readable? Are you + structuring it according to our conventions, or can our conventions be + improved to make it more readable? + +- Can the comments naturally be converted to prose that can be placed outside of + the coding environment in the literate file? + +## Literary conventions + +- We write in US English. +- Headers are written using sentence casing, as opposed to title casing. + +## Adapting and evolving the style guide -This style guide should evolve as Rzk develops and grows. If new features, like -implicit arguments, `let`-expressions, or `where`-blocks are added to the -language, or if there is made changes to the syntax of the language, their use -should be incorporated into this style guide. +This style guide should evolve as Rzk develops and grows. If new features are +added to the language or if there is made changes to the syntax of the language, +their use should be incorporated into this style guide. -At all times, the goal is to have code that is easy to read and navigate, even -for those who are not the authors. We should also ensure that we maintain a -consistent style across the entire repository. +Remember, the goal is at all times is to have code that is easy to read, +navigate and maintain, even for those who are not the original authors. From 14979426c2d97e1f29ea91a64f378428e61e18b7 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 9 Oct 2023 19:33:44 +0200 Subject: [PATCH 05/19] styleguide WIP --- src/STYLEGUIDE.md | 334 ++++++++++++++++++++++++++++++++-------------- 1 file changed, 235 insertions(+), 99 deletions(-) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index 5fc76849..75a4f49f 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -1,26 +1,36 @@ # Style guide and design principles -This guide provides a set of design principles and guidelines for the `sHoTT` -project. +The `sHoTT` project is an evolving community effort, and your participation is +most welcomed! However, to make the library as useful as possible for everyone, +we ask that everyone comply to a common set of style guidelines. -Our style and design principles borrows heavily from -[`agda-unimath`](https://github.com/UniMath/agda-unimath). +Good style conventions don't just serve to homogenize code and make things look +pretty, but they serve to + +- Elucidate the structure of proofs and definitions through proper formatting. +- Effectively summarize definitions and arguments through good naming + conventions. +- Make the formalization base easier to navigate. +- Help us maintain the repository. +- Provide techniques that help you in the formalization process. + +Please note that these conventions will and should change as the project and +language develops. We acknowledge that our code is not always consistent with +our conventions, and appreciate your help keeping the library compliant and +clean. ## The structure of code We enforce strict formatting rules. This formatting allows the type of the defined term to be easily readable, and aids in understanding the structure of -the definition. - -The general format of a definition is as follows: +the definition. The general format of a definition is as follows: ```rzk #def concat ( p : x = y) ( q : y = z) : (x = z) - := - ind-path A y (\ z' q' → (x = z')) p z q + := ind-path A y (\ z' q' → (x = z')) p z q ``` - We start with the name, and place every assumption on a new line. @@ -28,19 +38,23 @@ The general format of a definition is as follows: - The conclusion of the definition is placed on its own line, which starts with a colon (`:`). -- Then, on the next line, the walrus separator (`:=`) is placed, and after it - follows the actual construction of the definition. If the construction does - not fit on a single line, we immediately insert a new line after the walrus - separator and indent the code an extra level (2 spaces). +- On the next line, the walrus separator (`:=`) is placed, and after it follows + the actual construction of the definition. If the construction does not fit on + a single line, we immediately insert a new line after the walrus separator. + Note, in particular, to avoid excessive indentation we do **not** indent the + code an extra level in this case. + +### Trees and your constructions In the Rzk language, every construction is structured like a tree, where each -operation can be seen as a branching point. We use indentation levels and -parentheses to highlight this structure, which makes the code more organized and -readable. For example, when part of a definition extends beyond a single line, -we introduce line breaks at the earliest branching point, clearly displaying the -tree structure of the definition. This allows the reader to follow the branches -of the tree, and to visually grasp the scope of each operation and argument. -Consider the following example about Segal types: +operation can be seen as a branching point. We use indentation and +parenthization conventions to highlight this structure, which makes the code +more organized and readable. For example, when part of a definition extends +beyond a single line, we introduce line breaks at the earliest sensible +branching point, clearly displaying the tree structure of the definition. This +allows the reader to follow the branches of the tree, and to visually grasp the +scope of each operation and argument. Consider the following example about Segal +types: ```rzk #def is-segal-is-local-horn-inclusion @@ -48,61 +62,125 @@ Consider the following example about Segal types: ( is-local-horn-inclusion-A : is-local-horn-inclusion A) : is-segal A := - \ x y z f g → - contractible-fibers-is-equiv-projection - ( Λ → A) - ( \ k → - Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂))) , - ( hom2 A - ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂)) - ( \ t → k (t , 0₂)) - ( \ t → k (1₂ , t)) - ( h))) - ( second - ( equiv-comp - ( Σ ( k : Λ → A) , - Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂))) , - ( hom2 A + \ x y z f g → + contractible-fibers-is-equiv-projection + ( Λ → A) + ( \ k → + Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂))) + , ( hom2 A + ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂)) + ( \ t → k (t , 0₂)) + ( \ t → k (1₂ , t)) + ( h))) + ( second + ( equiv-comp + ( Σ ( k : Λ → A) + , Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂))) + , ( hom2 A + ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂)) + ( \ t → k (t , 0₂)) + ( \ t → k (1₂ , t)) + ( h))) + ( Δ² → A) + ( Λ → A) + ( inv-equiv + ( Δ² → A) + ( Σ ( k : Λ → A) + , Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂))) + , ( hom2 A ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂)) ( \ t → k (t , 0₂)) ( \ t → k (1₂ , t)) ( h))) - ( Δ² → A) - ( Λ → A) - ( inv-equiv - ( Δ² → A) - ( Σ ( k : Λ → A) , - Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂))) , - ( hom2 A - ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂)) - ( \ t → k (t , 0₂)) - ( \ t → k (1₂ , t)) - ( h))) - ( equiv-horn-restriction A)) - ( horn-restriction A , is-local-horn-inclusion-A))) - ( horn A x y z f g) + ( equiv-horn-restriction A)) + ( horn-restriction A , is-local-horn-inclusion-A))) + ( horn A x y z f g) ``` The root here is the function `projection-equiv-contractible-fibers`. It takes -four arguments, each starting on a fresh line and is indented an extra level -from the root. The first argument fits neatly on one line, but the second one is -too large. In these cases, we add a line break right after the `→`-symbol -following the lambda-abstraction, which we consider the earliest branching point -in this case. The next node is again `Σ`, with two arguments. The first one fits -on a line, but the second does not, so we add a line break between them. This -process is continued until the definition is complete. - -Note also that we use parentheses to mark the branches. The extra space after -the opening parentheses marking a branch is there to visually emphasize the tree -structure of the definition, and synergizes with our convention to have +four arguments, each starting on a fresh line and is parenthesized. The first +argument fits neatly on one line, but the second one is too large. In these +cases, we add a line break right after the `→`-symbol following the +lambda-abstraction, which we consider the earliest sensible branching point +here. The next node is again `Σ`, with two arguments. The first one fits on a +line, but the second does not, so we add a line break between them since `Σ` is +only one character. This process is continued until the definition is complete. + +Observe also that we use indentation to highlight the branches. The extra space +after the opening parentheses marking a branch is there to visually emphasize +the tree structure of the definition, and synergizes with our convention to have two-space indentation level increases. +What is generally considered the "earliest branching point" will depend on +context, and we ask that contributors practice common sense when deciding this. +When in doubt, it is usually better to break lines sooner rather than later. + +## Other code conventions + +- We place binary operators/separators at the beginning of a line rather than + the end. When they are a single character wide, this aligns very well with our + parenthization and indentation rules. Consider for instance the following + sample code: + + ```rzk + ( moderately-long-name-of-a-function-A + ( a-very-complicated-term-with-a-very-long-name-or-description-B + , another-long-and-complicated-expression-for-another-term-C)) + ``` + + Our indentation convention has the beautiful feature that we can determine the + structure of the code simply by scanning the left edge of the code block. The + placement of the comma separator in the example above complements this neatly, + since we can immediately see that `function-A` is applied to the pair + `(term-B , term-C)` by scanning the left edge of the code. + + Similarly, consider also + + ```rzk + ( ( a-long-and-complicated-arithmetic-expression-involving-many-operations) + * ( another-complicated-and-long-expression-with-symbols-and-numbers)) + ``` + + By having the multiplication symbol on the start of the line we can + immediately see that we are multiplying the two long expressions together, as + opposed to some other operation. + + Similarly, we also place function type formation arrows at the start of the + next line. E.g. + + ```rzk + #def function + ( parameter-1 : type-1) + ( parameter-2 : type-2) + : type-with-a-name-3 + → type-with-a-longer-name-4 + → short-type-5 + := undefined + ``` + + !!! warning + + This should not be confused with the convention for lambda abstractions, + which should be placed at the end of the line instead. + + When the binary operator/separator is more then a single character wide, e.g. + for the walrus separator (`:=`) and identity type formation with explicitly + defined underlying type (`=_{...}`), we insert a new line directly after the + operator. E.g. + + ```rzk + ( ( a-term-of-a-type) + =_{ the-name-of-the-type} + ( another-term-of-that-type)) + ``` + ## Naming conventions Adhering to a good naming convention is essential for keeping the library navigable and maintainable, and helps you make progress with your formalization goals. Good names provide concise descriptions of an entry's purpose, and help -making the code in the library readable. +making the code in the library readable. The intent of our conventions can be +summarized as follows: - Entry names aim to concisely describe their mathematical concept, using well-known mathematical vocabulary. @@ -114,17 +192,17 @@ making the code in the library readable. - The naming conventions should apply regardless of topic or subfield. - For many common kinds of entries, our naming conventions should offer a predictable suggestion of what its name should be. +- In this way, our conventions should help generate names for definitions. - Ultimately, our goal is for these conventions to support clear and maintainable code. -> - Add example -> - prepending assumptions and then conclusion. General format of names -> -> > The naming conventions are aimed at improving the readability of the code, -> > not to ensure the shortest possible names, nor to minimize the amount of -> > typing by the implementers of the library. +### A naming scheme + +With this in mind + +TODO -> - We mainly use lower case names with words separated by hyphens. +- We mainly use lower case names with words separated by hyphens. - Capitalized names are reserved for subuniverses and similar "namespaces". When a construction is made internally to such a collection, we _append_ its name. @@ -139,33 +217,60 @@ making the code in the library readable. ``` - Use meaningful names that accurately represent the concepts applied. For - example, if a concept is known best by a special name, that name should + instance, if a concept is known best by a special name, that name should probably be used. + For instance, the canonical function with type signature + + ```rzk + (A → B → C) → (A × B → C) + ``` + + should be called `uncurry`, and not for instance + `map-from-product-map-of-maps`. + +### Exceptions and naming practices to avoid + +- We use Unicode symbols in names very sparingly and only when they align with + established mathematical practice. See the next section for more elaboration. + +- We never refer to variables in definition names. The only instance we allow + this is when that variable is available at every possible invoking site. For + instance, we can name the argument of `is-segal-is-local-horn-inclusion` of + type `is-local-horn-inclusion A` as `is-local-horn-inclusion-A`, since + anywhere it can be invoked, the name `A` is also in scope. However, we would + never name `is-segal-is-local-horn-inclusion` as + `is-segal-A-is-local-horn-inclusion`. + - For technical lemmas or definitions, where the chance they will be reused is - very low, the specific names do not matter as much. In these cases, one may + very low, the specific names do not matter as much. In these cases, you may resort to a simplified naming scheme, like enumeration. Please keep in mind, however, that if you find yourself appealing to this convention frequently, that is a sign that your code should be refactored. -- We use Unicode symbols in names very sparingly and only when they align with - established mathematical practice. +In closing, we note that the naming conventions are aimed at improving the +readability of the code, not to ensure the shortest possible names, nor to +minimize the amount of typing by the implementers of the library. ## Use of Unicode characters -In defined names we use Unicode symbols sparingly and only when they align with -established mathematical practice. For the builtin syntactic features of `rzk`, -however, we prefer the following Unicode symbols: +Although using Unicode characters in definition names is entirely permissible, +we recommend practicing restraint to maintain readability. For instance, +although products of shapes can be formed with the `×` binary operator, we +prefer to refer to it as `product` in names. + +When it comes to using builtin syntactic features of `rzk`, however, we use the +following symbols: -- `→` should be used instead of `->` (`\to`) -- `↦` should be used instead of`|->` (`\mapsto`) -- `≡` should be used instead of `===` (`\equiv`) -- `≤` should be used instead of `<=` (`\<=`) -- `∧` should be used instead of `/\` (`\and`) -- `∨` should be used instead of `\/` (`\or`) -- `0₂` should be used instead of `0_2` (`0\2`) -- `1₂` should be used instead of `1_2` (`1\2`) -- `I × J` should be used instead of `I * J` (`\x` or `\times`) +- `→` should be used over `->` (`\to`) +- `↦` should be used over `|->` (`\mapsto`) +- `≡` should be used over `===` (`\equiv`) +- `≤` should be used over `<=` (`\<=`) +- `∧` should be used over `/\` (`\and`) +- `∨` should be used over `\/` (`\or`) +- `0₂` should be used over `0_2` (`0\2`) +- `1₂` should be used over `1_2` (`1\2`) +- `I × J` should be used over `I * J` (`\x` or `\times`) !!! info @@ -185,19 +290,19 @@ please consider the following: consider giving it a better name, or creating an intermediate definition with a name that better describes your current aplication. - In particular, if a particular family of Sigma types is given a name, we - prefer to also create and use named projections instead of `first` and - `second`. In many cases, their meaning is not immediately obvious, and so one - could be tempted to annotate the code with their meaning using comments. + In particular, if some family of Sigma types is given a name, we prefer to + also define and use named projections instead of `first` and `second`. In many + cases, their meaning is not immediately obvious, and so one could be tempted + to annotate the code using comments to explain them. - For instance, instead of writing `first (second is-invertible-f)`, we define a + For example, instead of writing `first (second is-invertible-f)`, we define a named projection `is-section-is-invertible`. This may then be used as `is-section-is-invertible A B f is-invertible-f` elsewhere. This way, the code - becomes self-documenting, and much easier to read. + becomes self-documenting. - However, we recognize that in `rzk`, since we do not have the luxury of - implicit arguments, this may sometimes cause unnecessarily verbose code. In - such cases, you may revert to using `first` and `second`. + However, we recognize that in Rzk, since we do not have the luxury of implicit + arguments, this may sometimes cause overly verbose code. In such cases, you + may revert to using `first` and `second`. - Can your code be structured in a way that makes it more readable? Are you structuring it according to our conventions, or can our conventions be @@ -208,14 +313,45 @@ please consider the following: ## Literary conventions -- We write in US English. +- For consistency, we prefer to write in US English. + - Headers are written using sentence casing, as opposed to title casing. +- If the contents of a code block in some sense captures a section of an + external source, the `title`-field may be used to reference that section. + + For example: + + ````md + ```rzk title="RS17, Definition 10.6" + #def is-rezk + ( A : U) + : U + := + Σ ( is-segal-A : is-segal A) + , ( (x : A) + → (y : A) + → is-equiv (x = y) (Iso A is-segal-A x y) (iso-eq A is-segal-A x y)) + ``` + ```` + + The `title`-field may also be used to give descriptive headers to sections of + your code. + ## Adapting and evolving the style guide -This style guide should evolve as Rzk develops and grows. If new features are -added to the language or if there is made changes to the syntax of the language, -their use should be incorporated into this style guide. +As mentioned in the introduction, we reiterate that this style guide will +necessarily evolve as we learn to use Rzk in new and better ways, and as the +language itself develops. Remember, the goal is at all times is to have code +that is easy to read, navigate and maintain, even for those who are not the +original authors. + +## References + +Our style guide and design principles borrows heavily from +[`agda-unimath`](https://github.com/UniMath/agda-unimath). If you are looking +for more inspiration, have a look at: -Remember, the goal is at all times is to have code that is easy to read, -navigate and maintain, even for those who are not the original authors. +- [The design philosophy of `agda-unimath`](https://unimath.github.io/agda-unimath/DESIGN-PRINCIPLES.html#design-philosophy-of-agda-unimath) +- [The `agda-unimath` library style guide](https://unimath.github.io/agda-unimath/CODINGSTYLE.html) +- [Naming conventions for `agda-unimath`](https://unimath.github.io/agda-unimath/NAMING-CONVENTIONS.html) From 9c02a0506733fa7982fa492cf99915358a916dd6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 9 Oct 2023 19:44:13 +0200 Subject: [PATCH 06/19] adjust some wording `STYLEGUIDE` --- src/STYLEGUIDE.md | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index 75a4f49f..47176f4d 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -12,7 +12,7 @@ pretty, but they serve to conventions. - Make the formalization base easier to navigate. - Help us maintain the repository. -- Provide techniques that help you in the formalization process. +- Provide techniques and habits that help you in the formalization process. Please note that these conventions will and should change as the project and language develops. We acknowledge that our code is not always consistent with @@ -112,8 +112,9 @@ the tree structure of the definition, and synergizes with our convention to have two-space indentation level increases. What is generally considered the "earliest branching point" will depend on -context, and we ask that contributors practice common sense when deciding this. -When in doubt, it is usually better to break lines sooner rather than later. +context, and we ask that contributors practice common sense when determining +this. When in doubt, it is usually better to break lines sooner rather than +later. ## Other code conventions @@ -143,7 +144,7 @@ When in doubt, it is usually better to break lines sooner rather than later. By having the multiplication symbol on the start of the line we can immediately see that we are multiplying the two long expressions together, as - opposed to some other operation. + opposed to performing some other operation. Similarly, we also place function type formation arrows at the start of the next line. E.g. @@ -160,13 +161,14 @@ When in doubt, it is usually better to break lines sooner rather than later. !!! warning - This should not be confused with the convention for lambda abstractions, - which should be placed at the end of the line instead. + This should not be confused with the convention for placement of arrows + for lambda abstractions, which should be placed at the end of the line + instead. - When the binary operator/separator is more then a single character wide, e.g. + When the binary operator/separator is more than a single character wide, e.g. for the walrus separator (`:=`) and identity type formation with explicitly - defined underlying type (`=_{...}`), we insert a new line directly after the - operator. E.g. + passed underlying type (`=_{...}`), we insert a new line directly after the + operator as well. I.e. ```rzk ( ( a-term-of-a-type) @@ -277,7 +279,7 @@ following symbols: For `first`, `second`, `TOP` and `BOT`, we prefer the ASCII versions as opposed to `π₁`, `π₂`, `⊤` and `⊥`, as we find the latter don't read too well in the code. Please also note that we usually prefer the use of - named projections for special Sigma-types when these are defined. + named projections for special `Σ`-types when these are defined. ## Use of comments @@ -290,10 +292,10 @@ please consider the following: consider giving it a better name, or creating an intermediate definition with a name that better describes your current aplication. - In particular, if some family of Sigma types is given a name, we prefer to - also define and use named projections instead of `first` and `second`. In many - cases, their meaning is not immediately obvious, and so one could be tempted - to annotate the code using comments to explain them. + In particular, if some family of `Σ`-types is given a name, we prefer to also + define and use named projections for it instead of `first` and `second`. In + many cases, their meaning is not immediately obvious, and so one could be + tempted to annotate the code using comments to explain them. For example, instead of writing `first (second is-invertible-f)`, we define a named projection `is-section-is-invertible`. This may then be used as From babea46dc3cfe20b9e3135cfd902bf8b22fc6cd6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 9 Oct 2023 23:22:39 +0200 Subject: [PATCH 07/19] style guide naming convention and other additions --- src/STYLEGUIDE.md | 97 +++++++++++++++++++++++++++++++++-------------- 1 file changed, 68 insertions(+), 29 deletions(-) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index 47176f4d..817454f3 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -40,9 +40,10 @@ the definition. The general format of a definition is as follows: - On the next line, the walrus separator (`:=`) is placed, and after it follows the actual construction of the definition. If the construction does not fit on - a single line, we immediately insert a new line after the walrus separator. - Note, in particular, to avoid excessive indentation we do **not** indent the - code an extra level in this case. + a single line, by which we mean fit within our stipulated 80-character limit, + we immediately insert a new line after the walrus separator. Note, in + particular, to avoid excessive indentation we do **not** indent the code an + extra level in this case. ### Trees and your constructions @@ -98,22 +99,23 @@ types: ``` The root here is the function `projection-equiv-contractible-fibers`. It takes -four arguments, each starting on a fresh line and is parenthesized. The first -argument fits neatly on one line, but the second one is too large. In these -cases, we add a line break right after the `→`-symbol following the -lambda-abstraction, which we consider the earliest sensible branching point -here. The next node is again `Σ`, with two arguments. The first one fits on a -line, but the second does not, so we add a line break between them since `Σ` is -only one character. This process is continued until the definition is complete. +four arguments, each starting on a fresh line and is parenthesized. Note that +its parentheses are indented at the same level as its parent node. The first +argument fits neatly on one line, but the second one is too large. In this case, +we add a line break right after the `→`-symbol following the lambda-abstraction, +which we consider the earliest branching point here. The next node is again `Σ`, +with two arguments. The first one fits on a line, but the second does not, so we +add a line break between them since `Σ` is only one character. This process is +continued until the definition is complete. Observe also that we use indentation to highlight the branches. The extra space after the opening parentheses marking a branch is there to visually emphasize the tree structure of the definition, and synergizes with our convention to have two-space indentation level increases. -What is generally considered the "earliest branching point" will depend on -context, and we ask that contributors practice common sense when determining -this. When in doubt, it is usually better to break lines sooner rather than +What is generally considered the "earliest sensible branching point" will depend +on context, and we ask that contributors practice common sense when determining +this. When in doubt, it is generally better to break lines sooner rather than later. ## Other code conventions @@ -176,6 +178,15 @@ later. ( another-term-of-that-type)) ``` +- We employ an 80-character line length limit. This means that lines of code + generally should not be longer than 80 characters. If they exceed this limit, + they should be reformatted to fit within the limit by inserting appropriate + line breaks. We do make some exceptions to this rule: + + - Names can be longer than the line character limit + +- TODO Formatting convention for extension types + ## Naming conventions Adhering to a good naming convention is essential for keeping the library @@ -198,38 +209,60 @@ summarized as follows: - Ultimately, our goal is for these conventions to support clear and maintainable code. -### A naming scheme +### A general naming scheme -With this in mind +With the basic purpose in mind, we present an adapted possible general naming +scheme originally due to Egbert Rijke. -TODO +The general pattern looks as follows: -- We mainly use lower case names with words separated by hyphens. +```text + [descriptor]-[output-type]-[input-types]-[Namespace] +``` -- Capitalized names are reserved for subuniverses and similar "namespaces". When - a construction is made internally to such a collection, we _append_ its name. - For instance, the subuniverse of Segal types is called `Segal`, and the - function type formation in that subuniverse , called `function-type-Segal,` - has the following signature: +Every part of the pattern is optional. However, their order is fixed. The +general naming pattern is broken into the following parts: - ```rzk +- **\[descriptor\]:** A custom descriptive name part for the entry. +- **\[output-type\]:** Refers to the concluding type of the entry. +- **\[input-types\]:** Consists of references to noteworthy input types. +- **\[Namespace\]:** Refers to an overarching concept, a subuniverse which the + construction takes place in, or a general category the entry is about. + +In particular, since Rzk does not currently have a suitable namespace mechanism, +the `[Namespace]` field serves as a reasonable substitute. + +Now, let us consider some examples: + +- ```rzk #def function-type-Segal ( A B : Segal) : Segal ``` -- Use meaningful names that accurately represent the concepts applied. For - instance, if a concept is known best by a special name, that name should - probably be used. + This definition uses the pattern `[output-type]-[Namespace]`. + +- `is-segal-is-local-horn-inclusion` uses the pattern + `[output-type]-[input-types]`. +- `is-equiv-identity` uses the pattern `[output-type]`. - For instance, the canonical function with type signature +The descriptor pattern is by far the most versatile one. It's purpose is to give +special meaningful descriptions that accurately represent some aspect, or +precisely the concept in question. For instance, if a concept is known best by a +special name, that name should probably be used. + +- As an example, the canonical function with type signature ```rzk (A → B → C) → (A × B → C) ``` - should be called `uncurry`, and not for instance - `map-from-product-map-of-maps`. + should be called `uncurry`, using the `descriptor`-pattern. It should not, for + instance, be called `map-from-product-map-of-maps`. + +- Another example is `compute-hom-eq-extension-type-is-discrete`. This uses the + pattern `[descriptor]-[output-type]-[input-types]` + (`(compute)-(hom)-(eq-extension-type-is-discrete)`). ### Exceptions and naming practices to avoid @@ -340,6 +373,12 @@ please consider the following: The `title`-field may also be used to give descriptive headers to sections of your code. +- We use the autoformatting tool [Prettier](https://prettier.io/) to format + markdown code, and we recommend that you install it or an alternative for use + with your editor. Be aware that the formatting rules automated by Prettier are + enforced by our CI workflow, so pull requests cannot be merged without the + proper markdown formatting. + ## Adapting and evolving the style guide As mentioned in the introduction, we reiterate that this style guide will From 219cb92db8945957693d31d1f5088cd36c958eb4 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 9 Oct 2023 23:30:17 +0200 Subject: [PATCH 08/19] add reminder to read style guide --- README.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/README.md b/README.md index 5ca5d3a7..fdb08015 100644 --- a/README.md +++ b/README.md @@ -41,6 +41,9 @@ assistant. Then run the following command from the root of this repository: rzk typecheck ``` +Please also have a look at our [style guide](src/STYLEGUIDE.md) before +submitting your pull request. + # References 1. Emily Riehl & Michael Shulman. A type theory for synthetic ∞-categories. From d6a16ec47feeff6657a5fdd1d7470d66dbd6a085 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 10 Oct 2023 14:39:01 +0200 Subject: [PATCH 09/19] Table of common descriptors --- src/STYLEGUIDE.md | 19 +++++++++++++++++++ src/simplicial-hott/05-segal-types.rzk.md | 20 ++++++++++---------- 2 files changed, 29 insertions(+), 10 deletions(-) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index 817454f3..d4302fd6 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -264,6 +264,25 @@ special name, that name should probably be used. pattern `[descriptor]-[output-type]-[input-types]` (`(compute)-(hom)-(eq-extension-type-is-discrete)`). +### Table of common descriptors + +To give a sense of the kind of general descriptors we use, we list some common +descriptors with examples in the table below. + +| Descriptor | Purpose | Example | +| ---------------- | ------------------------------------------------------------------------------------------------------------------ | --------------------------------------- | +| `coherence` | Used for proofs of coherence | `coherence-is-half-adjoint-equiv` | +| `compute` | Used for proofs of computation, which may be an identification or an element of any other identity system | `compute-postwhisker-homotopy-is-segal` | +| `Eq` | Used for identity systems on types where `htpy` or `equiv` is not an appropriate descriptor of the identity system | | +| `eq` | Used as a descriptor for the identity type | `eq-htpy` | +| `equiv` | Used for equivalences, and also for names of identity systems of universe-like types | `equiv-ap-is-equiv` | +| `extensionality` | Used for computations of identity types | `extensionality-Σ` | +| `homotopy` | Used for constructions of homotopies, and also for names of identity systems of function-like types | `homotopy-section-retraction-is-equiv` | +| `is-property` | Used when `is-prop` is unavailable | | +| `map` | Used in two ways: as the functorial action of a type constructor, but also as the underlying map of a morphism | `map-inverse-has-inverse` | +| `type` | Used for the underlying type of an object | `type-Segal` | +| `statement` | Used for definitions which are statements of things | `statement-homotopy-interchange-law` | + ### Exceptions and naming practices to avoid - We use Unicode symbols in names very sparingly and only when they align with diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md index 301a2bf5..315f651f 100644 --- a/src/simplicial-hott/05-segal-types.rzk.md +++ b/src/simplicial-hott/05-segal-types.rzk.md @@ -16,8 +16,8 @@ This is a literate `rzk` file: - `hott/total-space.md` — We rely on `#!rzk is-equiv-projection-contractible-fibers` and `#!rzk projection-total-type` in the proof of Theorem 5.5. -- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and their - subshapes. +- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and + their subshapes. - `03-extension-types.rzk.md` — We use the fubini theorem and extension extensionality. @@ -1546,7 +1546,7 @@ Interchange law #variable is-segal-A : is-segal A #variables x y z : A -#def homotopy-interchange-law-statement +#def statement-homotopy-interchange-law ( f1 f2 f3 : hom A x y) ( h1 h2 h3 : hom A y z) ( p : f1 = f2) @@ -1574,25 +1574,25 @@ Interchange law ( q : f2 = f3) ( p' : h1 = h2) ( q' : h2 = h3) - : homotopy-interchange-law-statement f1 f2 f3 h1 h2 h3 p q p' q' + : statement-homotopy-interchange-law f1 f2 f3 h1 h2 h3 p q p' q' := ind-path ( hom A x y) ( f2) - ( \ f3 q -> homotopy-interchange-law-statement f1 f2 f3 h1 h2 h3 p q p' q') + ( \ f3 q -> statement-homotopy-interchange-law f1 f2 f3 h1 h2 h3 p q p' q') ( ind-path ( hom A x y) ( f1) - ( \ f2 p -> homotopy-interchange-law-statement f1 f2 f2 h1 h2 h3 + ( \ f2 p -> statement-homotopy-interchange-law f1 f2 f2 h1 h2 h3 p refl p' q') ( ind-path ( hom A y z) ( h2) - ( \ h3 q' -> homotopy-interchange-law-statement f1 f1 f1 h1 h2 h3 + ( \ h3 q' -> statement-homotopy-interchange-law f1 f1 f1 h1 h2 h3 refl refl p' q') ( ind-path ( hom A y z) ( h1) - ( \ h2 p' -> homotopy-interchange-law-statement f1 f1 f1 h1 h2 h2 + ( \ h2 p' -> statement-homotopy-interchange-law f1 f1 f1 h1 h2 h2 refl refl p' refl) ( refl) ( h2) @@ -1779,8 +1779,8 @@ The cofibration Λ²₁ → Δ² is inner anodyne ## Inner fibrations -An inner fibration is a map `α : A' → A` which is right orthogonal -to `Λ ⊂ Δ²`. This is the relative notion of a Segal type. +An inner fibration is a map `α : A' → A` which is right orthogonal to `Λ ⊂ Δ²`. +This is the relative notion of a Segal type. ```rzk #def is-inner-fibration From a2fbdd7815615d830ea959c29fc523dbcf5fdbfc Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 10 Oct 2023 14:39:35 +0200 Subject: [PATCH 10/19] =?UTF-8?q?example=20`Eq-=CE=A3`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/STYLEGUIDE.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index d4302fd6..d5995381 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -273,7 +273,7 @@ descriptors with examples in the table below. | ---------------- | ------------------------------------------------------------------------------------------------------------------ | --------------------------------------- | | `coherence` | Used for proofs of coherence | `coherence-is-half-adjoint-equiv` | | `compute` | Used for proofs of computation, which may be an identification or an element of any other identity system | `compute-postwhisker-homotopy-is-segal` | -| `Eq` | Used for identity systems on types where `htpy` or `equiv` is not an appropriate descriptor of the identity system | | +| `Eq` | Used for identity systems on types where `htpy` or `equiv` is not an appropriate descriptor of the identity system | `Eq-Σ` | | `eq` | Used as a descriptor for the identity type | `eq-htpy` | | `equiv` | Used for equivalences, and also for names of identity systems of universe-like types | `equiv-ap-is-equiv` | | `extensionality` | Used for computations of identity types | `extensionality-Σ` | From db211c8d437f02b6e00f9b5ee8568e61c1ae0e3b Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 19 Oct 2023 16:42:57 +0200 Subject: [PATCH 11/19] total fibers --- src/hott/10-trivial-fibrations.rzk.md | 20 ++- src/hott/11-homotopy-pullbacks.rzk.md | 232 +++++++++++++++++++++++++- 2 files changed, 242 insertions(+), 10 deletions(-) diff --git a/src/hott/10-trivial-fibrations.rzk.md b/src/hott/10-trivial-fibrations.rzk.md index 38cee14a..619234eb 100644 --- a/src/hott/10-trivial-fibrations.rzk.md +++ b/src/hott/10-trivial-fibrations.rzk.md @@ -251,10 +251,9 @@ For any map `#!rzk f : A → B` the domain `#!rzk A` is equivalent to the sum of the fibers. ```rzk - -#def equiv-domain-sum-of-fibers - (A B : U) - (f : A → B) +#def equiv-sum-of-fibers-domain + ( A B : U) + ( f : A → B) : Equiv A (Σ (b : B), fib A B f b) := equiv-left-cancel @@ -268,6 +267,19 @@ the fibers. ( fubini-Σ A B (\ a b → f a = b)) ``` +The inverse map is just the canonical projection to `A`. + +```rzk +#def is-equiv-domain-sum-of-fibers + ( A B : U) + ( f : A → B) + : is-equiv (Σ (b : B), fib A B f b) A ( \ (_ , (a , _)) → a) + := + second + ( inv-equiv A (Σ (b : B) , fib A B f b) + ( equiv-sum-of-fibers-domain A B f)) +``` + ## Equivalence between fibers in equivalent domains As an application of the main theorem, we show that precomposing with an diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 3a2839af..70b82d4b 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -142,7 +142,7 @@ always do this (whether the square is homotopy-cartesian or not). := (first ĉ', first-path-Σ A C (temp-uBDx-Σαγ ĉ') ĉ q̂) -#def temp-uBDx-helper-type uses (γ C') +#def temp-uBDx-helper-IkCK-type uses (γ C') ( ((s', s) , η) : has-section-family-over-map) ( a : A ) ( (a', p) : fib A' A α a ) @@ -151,14 +151,14 @@ always do this (whether the square is homotopy-cartesian or not). Σ ( q̂ : temp-uBDx-Σαγ (a', s' a') = (a, s a)), ( induced-map-on-fibers-Σ (a, s a) ((a', s' a'), q̂) = (a', p)) -#def temp-uBDx-helper uses (γ C') +#def temp-uBDx-helper-IkCK uses (γ C') ( ((s', s) , η) : has-section-family-over-map) : ( a : A) → ( (a', p) : fib A' A α a ) → - temp-uBDx-helper-type ((s',s), η) a (a', p) + temp-uBDx-helper-IkCK-type ((s',s), η) a (a', p) := ind-fib A' A α - ( temp-uBDx-helper-type ((s',s), η)) + ( temp-uBDx-helper-IkCK-type ((s',s), η)) ( \ a' → ( eq-pair A C (α a', γ a' (s' a')) (α a', s (α a')) ( refl, η a' ) , eq-pair @@ -185,9 +185,9 @@ always do this (whether the square is homotopy-cartesian or not). ( \ (a', c') → (α a', γ a' c')) ( a, s a))) := - ( \ (a', p) → ( (a', s' a'), first (temp-uBDx-helper ((s',s),η) a (a',p))), + ( \ (a', p) → ( (a', s' a'), first (temp-uBDx-helper-IkCK ((s',s),η) a (a',p))), ( induced-map-on-fibers-Σ (a, s a) , - \ (a', p) → second (temp-uBDx-helper ((s',s),η) a (a',p)))) + \ (a', p) → second (temp-uBDx-helper-IkCK ((s',s),η) a (a',p)))) #def push-down-equiv-with-section uses (γ) ( ((s',s),η) : has-section-family-over-map) @@ -502,6 +502,10 @@ Given two maps `B → A` and `C → A`, we can form the **relative product** ove : relative-product → C := \ ((_ , c), _) → c +#def projection-relative-product uses (A B β C) + : relative-product → A + := \ ((_ , c) , _) → γ c + #def homotopy-relative-product uses (A B C) ( (bc, p) : relative-product ) : β (first-relative-product (bc,p)) = γ (second-relative-product (bc,p)) @@ -529,6 +533,10 @@ product of all fibers. : fiber-product → C := \ (_, (_, (c, _))) → c +#def projection-fiber-product uses (A B β C γ) + : fiber-product → A + := \ (a, (_, (_, _))) → a + #def homotopy-fiber-product uses (A B C) : ( abpcq : fiber-product ) → β (first-fiber-product abpcq) = γ (second-fiber-product abpcq) @@ -546,6 +554,17 @@ product of all fibers. : fiber-product := ( γ c , ( (b , e) , (c , refl))) +#def compatible-projection-fiber-relative-product uses (A B β C γ) + ( x : relative-product) + : projection-relative-product x = projection-fiber-product (fiber-relative-product x) + := refl + +#def compatible-projection-relative-fiber-product uses (A B β C γ) + ( abpcq : fiber-product) + : ( projection-relative-product (relative-fiber-product abpcq) + = projection-fiber-product abpcq) + := second (second (second abpcq)) -- evaluates to q + #def is-id-relative-fiber-relative-product ( bce : relative-product) : relative-fiber-product (fiber-relative-product bce) = bce @@ -615,5 +634,206 @@ The relative product of `f : B → A` with a map `Unit → A` corresponding to , \ _ → refl) , ( second (compute-pullback-to-Unit B A f a) , is-equiv-identity Unit)) +``` + +### Total fibers of a square + +We consider a commutative square + +``` +T → B +↓ ↓ +C → A +``` + +given by the following data: + +```rzk +#section fibers-comm-square + +-- the data of a comm square +#variable A : U +#variable B : U +#variable β : B → A +#variable C : U +#variable γ : C → A +#variable T : U +#variable β' : T → B +#variable γ' : T → C +#variable η : (t : T) → β (β' t) = γ (γ' t) +``` + +We define the canonical **gap map** from `T` to the relative product over `A`. +The fibers of this gap map are called the **total-fibers** of the commutative +square. + +```rzk +#def gap-map-comm-square + : T → relative-product A B β C γ + := \ t → ((β' t , γ' t) , η t) + +#def tot-fib-comm-square uses (β' γ' η) + ( bcp : relative-product A B β C γ) + : U + := fib T (relative-product A B β C γ) gap-map-comm-square bcp +-- t , ((β' t , γ' t) , η t) = ((b , c) , p) +``` + +We aim to show that one can compute these total fibers of the commutative square +in two steps: first, one takes the fibers in the vertical direction and obtains +an induced map `fib T C γ c → fib B A β (γ c)`; second, one takes the fibers of +these maps. + +We define the induced maps on fibers the resulting fibers between fibers. + +```rzk +#def map-vertical-fibs-comm-square + ( c : C) + : fib T C γ' c → fib B A β (γ c) + := \ (t , q) → + ( (β' t) + , ( concat A (β (β' t)) (γ (γ' t)) (γ c) + (η t) (ap C A (γ' t) c γ q))) + +#def fib-vertical-fibs-comm-square uses (β' γ' η) + ( c : C) + ( bp : fib B A β (γ c)) + : U + := fib (fib T C γ' c) (fib B A β (γ c)) + ( map-vertical-fibs-comm-square c) + ( bp) +-- (t, q : γ' t = c) , (β' t, concat (η t) (ap γ q)) = (b, p : β b = γ c) +``` + +Then we use a helper term to construct a comparison map from the total fibers to +the fiber fibers. + +```rzk +-- We append the random suffix IkCK to terms +-- that are only meant to be used locally in this section + +#def helper-IkCK uses (β' η) + ( ((b , c) , p) : relative-product A B β C γ) + ( t : T) + : U + := Σ ( q : γ' t = c) , map-vertical-fibs-comm-square c (t , q) = (b , p) + +#def fib-vertical-fibs-helper-IkCK uses (β' γ' η) + ( ((b , c) , p) : relative-product A B β C γ) + ( t : T) + ( (q , e) : helper-IkCK ((b,c),p) t) + : fib-vertical-fibs-comm-square c (b,p) + := ((t , q) , e) + + +#def fib-vertical-fibs-tot-fib-comm-square uses (η β' γ') + : ( ((b,c),p) : relative-product A B β C γ) + → ( (t , h) : tot-fib-comm-square ((b,c),p)) + → fib-vertical-fibs-comm-square c (b,p) + := + ( fib-vertical-fibs-helper-IkCK ((b,c),p) t) + ( ind-fib T (relative-product A B β C γ) + ( gap-map-comm-square) + ( \ bcp' (t, h') → helper-IkCK bcp' t) + ( \ t → (refl, refl)) + ( ((b,c),p)) + ( t , h)) +``` + +Note that we could have defined this comparison map without the helper by a +direct fiber induction, but this would leave it with worse definitional +computation properties on which the rest of our construction relies. + +```rzk +#def fib-vertical-fibs-tot-fib-comm-square' uses (η β' γ') +-- worse computation than fib-vertical-fibs-tot-fib-comm-square + : ( ((b,c),p) : relative-product A B β C γ) + → ( (t , h) : tot-fib-comm-square ((b,c),p)) + → fib-vertical-fibs-comm-square c (b,p) + := + ind-fib T (relative-product A B β C γ) (gap-map-comm-square) + ( \ ((b,c),p) _ → fib-vertical-fibs-comm-square c (b,p)) + ( \ t → ((t , refl) , refl)) +``` + +Finally, we show that these comparison maps are equivalences by summing over all +of them. Indeed, by applications of `is-equiv-domain-sum-of-fibers`, the total +sum of each is just equivalent to `T`. + +```rzk +#def is-equiv-projection-fib-vertical-fibs-comm-square uses (η β') + : is-equiv + ( Σ (((b,c),p) : relative-product A B β C γ) + , fib-vertical-fibs-comm-square c (b,p)) + ( T) + ( \ (_ , ((t , _) , _)) → t) + := + is-equiv-triple-comp + ( Σ (((b,c),p) : relative-product A B β C γ) + , fib-vertical-fibs-comm-square c (b,p)) + ( Σ ( c : C) + , ( Σ (bp : fib B A β (γ c)) + , fib-vertical-fibs-comm-square c bp)) + ( Σ (c : C) , fib T C γ' c) + ( T) + ( \ (((b , c) , p) , tqe) → (c , ((b , p) , tqe))) + ( ( \ (c , ((b , p) , tqe)) → (((b , c) , p) , tqe) , \ _ → refl) + , ( \ (c , ((b , p) , tqe)) → (((b , c) , p) , tqe) , \ _ → refl)) + ( \ (c , (_ , (tq , _))) → (c , tq)) + ( is-equiv-total-is-equiv-fiberwise C + ( \ c → Σ (bp : fib B A β (γ c)) , fib-vertical-fibs-comm-square c bp) + ( \ c → fib T C γ' c) + ( \ c (_ , (tq , _)) → tq) + ( \ c → + is-equiv-domain-sum-of-fibers + ( fib T C γ' c) (fib B A β (γ c)) + ( map-vertical-fibs-comm-square c))) + ( \ (_ , (t , _)) → t) + ( is-equiv-domain-sum-of-fibers T C γ') + +#def is-equiv-fib-vertical-fibs-tot-fib-comm-square uses (η β' γ') + : (((b,c),p) : relative-product A B β C γ) + → is-equiv + ( tot-fib-comm-square ((b,c),p)) + ( fib-vertical-fibs-comm-square c (b,p)) + ( fib-vertical-fibs-tot-fib-comm-square ((b,c),p)) + := + is-equiv-fiberwise-is-equiv-total + ( relative-product A B β C γ) + ( \ bcp → tot-fib-comm-square bcp) + ( \ ((b,c),p) → fib-vertical-fibs-comm-square c (b,p)) + ( \ bcp → fib-vertical-fibs-tot-fib-comm-square bcp) + ( is-equiv-right-factor + ( Σ (bcp : relative-product A B β C γ) + , tot-fib-comm-square bcp) + ( Σ (((b,c),p) : relative-product A B β C γ) + , fib-vertical-fibs-comm-square c (b,p)) + ( T) + ( total-map + ( relative-product A B β C γ) + ( \ bcp → tot-fib-comm-square bcp) + ( \ ((b,c),p) → fib-vertical-fibs-comm-square c (b,p)) + ( \ bcp → fib-vertical-fibs-tot-fib-comm-square bcp)) + ( \ (_ , ((t , _) , _)) → t) + ( is-equiv-projection-fib-vertical-fibs-comm-square) + ( is-equiv-domain-sum-of-fibers + ( T) ( relative-product A B β C γ) + ( gap-map-comm-square))) +``` + +We summarize the result as the following equivalence: + +```rzk +#def equiv-fib-vertical-fibs-tot-fib-comm-square uses (A B C β γ T β' γ' η) + ( b : B) + ( c : C) + ( p : β b = γ c) + : Equiv + ( tot-fib-comm-square ((b , c) , p)) + ( fib-vertical-fibs-comm-square c (b , p)) + := + ( fib-vertical-fibs-tot-fib-comm-square ((b , c) , p) + , is-equiv-fib-vertical-fibs-tot-fib-comm-square ((b , c) , p)) +#end fibers-comm-square ``` From 2d390c7931a544db72d767283edaed6da9c3da2a Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 19 Oct 2023 16:56:35 +0200 Subject: [PATCH 12/19] explain compute --- src/hott/11-homotopy-pullbacks.rzk.md | 31 ++++++++++++--------------- 1 file changed, 14 insertions(+), 17 deletions(-) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 70b82d4b..2fe59282 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -725,11 +725,10 @@ the fiber fibers. : fib-vertical-fibs-comm-square c (b,p) := ((t , q) , e) - #def fib-vertical-fibs-tot-fib-comm-square uses (η β' γ') - : ( ((b,c),p) : relative-product A B β C γ) - → ( (t , h) : tot-fib-comm-square ((b,c),p)) - → fib-vertical-fibs-comm-square c (b,p) + ( ((b,c),p) : relative-product A B β C γ) + ( (t , h) : tot-fib-comm-square ((b,c),p)) + : fib-vertical-fibs-comm-square c (b,p) := ( fib-vertical-fibs-helper-IkCK ((b,c),p) t) ( ind-fib T (relative-product A B β C γ) @@ -740,25 +739,23 @@ the fiber fibers. ( t , h)) ``` -Note that we could have defined this comparison map without the helper by a -direct fiber induction, but this would leave it with worse definitional -computation properties on which the rest of our construction relies. +We could have defined this comparison map without the helper by a direct fiber +induction, but in this case it would not commute definitionally with the +canonical projection to `T`. ```rzk -#def fib-vertical-fibs-tot-fib-comm-square' uses (η β' γ') --- worse computation than fib-vertical-fibs-tot-fib-comm-square - : ( ((b,c),p) : relative-product A B β C γ) - → ( (t , h) : tot-fib-comm-square ((b,c),p)) - → fib-vertical-fibs-comm-square c (b,p) - := - ind-fib T (relative-product A B β C γ) (gap-map-comm-square) - ( \ ((b,c),p) _ → fib-vertical-fibs-comm-square c (b,p)) - ( \ t → ((t , refl) , refl)) +#def compute-fib-vertical-fibs-tot-fib-comm-square uses (η β' γ') + ( bcp : relative-product A B β C γ) + ( (t , h) : tot-fib-comm-square bcp) + : + ( first (first (fib-vertical-fibs-tot-fib-comm-square bcp (t , h))) + = t) + := refl ``` Finally, we show that these comparison maps are equivalences by summing over all of them. Indeed, by applications of `is-equiv-domain-sum-of-fibers`, the total -sum of each is just equivalent to `T`. +type on each side is just equivalent to `T`. ```rzk #def is-equiv-projection-fib-vertical-fibs-comm-square uses (η β') From 832b25fd34aaa2b98a86d612dedf5725264be5dc Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Thu, 19 Oct 2023 17:04:43 +0200 Subject: [PATCH 13/19] reverse accidental search-and-replace error --- src/hott/11-homotopy-pullbacks.rzk.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 2fe59282..e97987fe 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -142,7 +142,7 @@ always do this (whether the square is homotopy-cartesian or not). := (first ĉ', first-path-Σ A C (temp-uBDx-Σαγ ĉ') ĉ q̂) -#def temp-uBDx-helper-IkCK-type uses (γ C') +#def temp-uBDx-helper-type uses (γ C') ( ((s', s) , η) : has-section-family-over-map) ( a : A ) ( (a', p) : fib A' A α a ) @@ -151,14 +151,14 @@ always do this (whether the square is homotopy-cartesian or not). Σ ( q̂ : temp-uBDx-Σαγ (a', s' a') = (a, s a)), ( induced-map-on-fibers-Σ (a, s a) ((a', s' a'), q̂) = (a', p)) -#def temp-uBDx-helper-IkCK uses (γ C') +#def temp-uBDx-helper uses (γ C') ( ((s', s) , η) : has-section-family-over-map) : ( a : A) → ( (a', p) : fib A' A α a ) → - temp-uBDx-helper-IkCK-type ((s',s), η) a (a', p) + temp-uBDx-helper-type ((s',s), η) a (a', p) := ind-fib A' A α - ( temp-uBDx-helper-IkCK-type ((s',s), η)) + ( temp-uBDx-helper-type ((s',s), η)) ( \ a' → ( eq-pair A C (α a', γ a' (s' a')) (α a', s (α a')) ( refl, η a' ) , eq-pair @@ -185,9 +185,9 @@ always do this (whether the square is homotopy-cartesian or not). ( \ (a', c') → (α a', γ a' c')) ( a, s a))) := - ( \ (a', p) → ( (a', s' a'), first (temp-uBDx-helper-IkCK ((s',s),η) a (a',p))), + ( \ (a', p) → ( (a', s' a'), first (temp-uBDx-helper ((s',s),η) a (a',p))), ( induced-map-on-fibers-Σ (a, s a) , - \ (a', p) → second (temp-uBDx-helper-IkCK ((s',s),η) a (a',p)))) + \ (a', p) → second (temp-uBDx-helper ((s',s),η) a (a',p)))) #def push-down-equiv-with-section uses (γ) ( ((s',s),η) : has-section-family-over-map) From bb773b8b5a01110c0de4d04b34fad491c1b6ac2d Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Mon, 23 Oct 2023 12:43:58 +0200 Subject: [PATCH 14/19] fix code broken by merge --- src/hott/11-homotopy-pullbacks.rzk.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 46fbe032..c902f049 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -900,10 +900,10 @@ that an equivalence of maps induces an equivalence of fibers at each base point. ( sums-of-fibers-to-domains-map-of-maps) ( second ( ( inv-equiv A' (Σ (a : A), fib A' A α a)) - ( equiv-domain-sum-of-fibers A' A α))) + ( equiv-sum-of-fibers-domain A' A α))) ( second ( ( inv-equiv B' (Σ (b : B), fib B' B β b)) - ( equiv-domain-sum-of-fibers B' B β))) + ( equiv-sum-of-fibers-domain B' B β))) ( is-equiv-s') #variable is-equiv-s : is-equiv A B s-c4XT From abbdde1bdf3fe449c432b4a742b583118ca6ce8e Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 23 Oct 2023 18:23:20 +0200 Subject: [PATCH 15/19] Conclusions first! --- src/STYLEGUIDE.md | 83 ++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 67 insertions(+), 16 deletions(-) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index d5995381..820b96e2 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -185,8 +185,6 @@ later. - Names can be longer than the line character limit -- TODO Formatting convention for extension types - ## Naming conventions Adhering to a good naming convention is essential for keeping the library @@ -246,7 +244,7 @@ Now, let us consider some examples: `[output-type]-[input-types]`. - `is-equiv-identity` uses the pattern `[output-type]`. -The descriptor pattern is by far the most versatile one. It's purpose is to give +The descriptor pattern is by far the most versatile one. Its purpose is to give special meaningful descriptions that accurately represent some aspect, or precisely the concept in question. For instance, if a concept is known best by a special name, that name should probably be used. @@ -264,24 +262,77 @@ special name, that name should probably be used. pattern `[descriptor]-[output-type]-[input-types]` (`(compute)-(hom)-(eq-extension-type-is-discrete)`). +### Conclusions first! + +One of the most noteworthy aspects of our general naming scheme is that +conclusions always end up at the start of the name. This has the benefit that +the most important aspect of a definition is what is mentioned first in its +name. Although it can take a little while to get used to this scheme as +everything is written in the opposite order you may be used to, it offers the +following central benefit: the name summarizes the entry's meaning efficiently, +even if only part of it is read. This means that when a reader is scanning the +application of a definition in a larger proof, they can get an overview by only +scanning the first few words at each branching point/line. + +Hence, if you are at a loss for naming a definition, we offer you the following +simplified naming scheme: start with the first important assumption in your +definition statement, and to it, _prepend_ every subsequent important assumption +that is made. Finally, prepend the concluding type. + +- For example, consider an entry with the following signature + + ```rzk + #def ????? + ( A B : U) + ( is-prop-A : is-prop A) + ( is-prop-B : is-prop B) + ( (f , g) : iff A B) + : is-equiv A B f + := ... + ``` + + applying the scheme we get + + 1. `is-prop`, noting the assumption that `A` is a proposition. Remember, we do + not include variable names in the entry's name. + 2. `is-prop-is-prop`, noting the assumption that `B` is a proposition. + 3. `iff-is-prop-is-prop`, noting the assumption that we have a logical + equivalence between `A` and `B`. + 4. `is-equiv-iff-is-prop-is-prop`, finally prepending the concluding type. + + Hence our final definition will be + + ```rzk + #def is-equiv-iff-is-prop-is-prop + ( A B : U) + ( is-prop-A : is-prop A) + ( is-prop-B : is-prop B) + ( (f , g) : iff A B) + : is-equiv A B f + := ... + ``` + + Observe how it is immediately clear what the elements that go into the entry + are, in which order they go, and what you get out if applying it! + ### Table of common descriptors To give a sense of the kind of general descriptors we use, we list some common descriptors with examples in the table below. -| Descriptor | Purpose | Example | -| ---------------- | ------------------------------------------------------------------------------------------------------------------ | --------------------------------------- | -| `coherence` | Used for proofs of coherence | `coherence-is-half-adjoint-equiv` | -| `compute` | Used for proofs of computation, which may be an identification or an element of any other identity system | `compute-postwhisker-homotopy-is-segal` | -| `Eq` | Used for identity systems on types where `htpy` or `equiv` is not an appropriate descriptor of the identity system | `Eq-Σ` | -| `eq` | Used as a descriptor for the identity type | `eq-htpy` | -| `equiv` | Used for equivalences, and also for names of identity systems of universe-like types | `equiv-ap-is-equiv` | -| `extensionality` | Used for computations of identity types | `extensionality-Σ` | -| `homotopy` | Used for constructions of homotopies, and also for names of identity systems of function-like types | `homotopy-section-retraction-is-equiv` | -| `is-property` | Used when `is-prop` is unavailable | | -| `map` | Used in two ways: as the functorial action of a type constructor, but also as the underlying map of a morphism | `map-inverse-has-inverse` | -| `type` | Used for the underlying type of an object | `type-Segal` | -| `statement` | Used for definitions which are statements of things | `statement-homotopy-interchange-law` | +| Descriptor | Purpose | Example | +| -------------------- | ------------------------------------------------------------------------------------------------------------------- | --------------------------------------- | +| `coherence` | Used for proofs of coherence. | `coherence-is-half-adjoint-equiv` | +| `compute` | Used for proofs of computation, which may be an identification or an element of any other identity system. | `compute-postwhisker-homotopy-is-segal` | +| `Eq` | Used for identity systems on types where `htpy` or `equiv` is not an appropriate descriptor of the identity system. | `Eq-Σ` | +| `eq` | Used as a descriptor for the identity type. | `eq-htpy` | +| `equiv` | Used for equivalences, and also for names of identity systems of universe-like types. | `equiv-ap-is-equiv` | +| `extensionality` | Used for computations of identity types. | `extensionality-Σ` | +| `homotopy` or `htpy` | Used for constructions of homotopies, and also for names of identity systems of function-like types. | `homotopy-section-retraction-is-equiv` | +| `is-property` | Used when `is-prop` is unavailable. | `is-property-is-contr` | +| `map` | Used in two ways: as the functorial action of a type constructor, but also as the underlying map of a morphism. | `map-inverse-has-inverse` | +| `type` | Used for the underlying type of an object. | `type-Segal` | +| `statement` | Used for definitions which are statements of things. | `statement-homotopy-interchange-law` | ### Exceptions and naming practices to avoid From b4edfd9f9bc33991ecb806e9855e4b21aa1da15d Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 23 Oct 2023 18:29:12 +0200 Subject: [PATCH 16/19] `uses` convention --- src/STYLEGUIDE.md | 51 ++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 46 insertions(+), 5 deletions(-) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index 820b96e2..67c30981 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -120,6 +120,15 @@ later. ## Other code conventions +- We employ an 80-character line length limit. This means that lines of code + generally should not be longer than 80 characters. If they exceed this limit, + they should be reformatted to fit within the limit by inserting appropriate + line breaks. + + !!! info + + Names can be longer than the line character limit. + - We place binary operators/separators at the beginning of a line rather than the end. When they are a single character wide, this aligns very well with our parenthization and indentation rules. Consider for instance the following @@ -178,12 +187,44 @@ later. ( another-term-of-that-type)) ``` -- We employ an 80-character line length limit. This means that lines of code - generally should not be longer than 80 characters. If they exceed this limit, - they should be reformatted to fit within the limit by inserting appropriate - line breaks. We do make some exceptions to this rule: +- The `uses`-keyword and the accompanying list of variables is placed on their + own lines. - - Names can be longer than the line character limit + In the base case, write + + ```rzk + #define my-name + uses (my-variable-1 my-variable-2 ...) + ( A : U) + ... + ``` + + If the variable list (`(my-variable-1 my-variable-2 ...)`) does not fit on the + first line together with `uses`, insert a line break directly after `uses` and + write: + + ```rzk + #define my-name + uses + ( my-variable-1 my-variable-2 ...) + ( A : U) + ... + ``` + + If the list still does not fit on a single line, start insert line breaks + between variables. Here, there is some room for common sense in where the line + breaks should be inserted, allowing for certain variable names to be grouped + together: + + ```rzk + #define my-name + uses + ( my-variable-1 + my-variable-2 + ...) + ( A : U) + ... + ``` ## Naming conventions From fb1a34164c3978bdb586e2f5340730a98dd146f6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 23 Oct 2023 18:37:56 +0200 Subject: [PATCH 17/19] minor fixes --- src/STYLEGUIDE.md | 51 ++++++++++++++++++++++++----------------------- 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index 67c30981..de58951e 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -21,9 +21,9 @@ clean. ## The structure of code -We enforce strict formatting rules. This formatting allows the type of the -defined term to be easily readable, and aids in understanding the structure of -the definition. The general format of a definition is as follows: +We enforce strict formatting rules. These rules facilitate better readability of +the code and aids in understanding the structure of every. The general format of +a definition is as follows: ```rzk #def concat @@ -42,10 +42,10 @@ the definition. The general format of a definition is as follows: the actual construction of the definition. If the construction does not fit on a single line, by which we mean fit within our stipulated 80-character limit, we immediately insert a new line after the walrus separator. Note, in - particular, to avoid excessive indentation we do **not** indent the code an - extra level in this case. + particular, to avoid excessive indentation we do not indent the code an extra + level in this particular case. -### Trees and your constructions +### The tree structure of constructions In the Rzk language, every construction is structured like a tree, where each operation can be seen as a branching point. We use indentation and @@ -98,15 +98,16 @@ types: ( horn A x y z f g) ``` -The root here is the function `projection-equiv-contractible-fibers`. It takes -four arguments, each starting on a fresh line and is parenthesized. Note that -its parentheses are indented at the same level as its parent node. The first -argument fits neatly on one line, but the second one is too large. In this case, -we add a line break right after the `→`-symbol following the lambda-abstraction, -which we consider the earliest branching point here. The next node is again `Σ`, -with two arguments. The first one fits on a line, but the second does not, so we -add a line break between them since `Σ` is only one character. This process is -continued until the definition is complete. +The root in this instance is the function +`projection-equiv-contractible-fibers`. It takes four arguments, each starting +on a fresh line and is parenthesized. Note that its parentheses are indented at +the same level as its parent node. The first argument fits neatly on one line, +but the second one is too large. In this case, we add a line break right after +the `→`-symbol following the lambda-abstraction, which we consider the earliest +branching point in this case. The next node is again `Σ`, with two arguments. +The first one fits on a line, but the second does not, so we add a line break +between them since `Σ` is only one character. This process is continued until +the definition is complete. Observe also that we use indentation to highlight the branches. The extra space after the opening parentheses marking a branch is there to visually emphasize @@ -305,13 +306,13 @@ special name, that name should probably be used. ### Conclusions first! -One of the most noteworthy aspects of our general naming scheme is that -conclusions always end up at the start of the name. This has the benefit that -the most important aspect of a definition is what is mentioned first in its -name. Although it can take a little while to get used to this scheme as -everything is written in the opposite order you may be used to, it offers the -following central benefit: the name summarizes the entry's meaning efficiently, -even if only part of it is read. This means that when a reader is scanning the +The most noteworthy aspect of our general naming scheme is that conclusions +always end up at the start of the name. This has the benefit that the most +important aspect of a definition is what is mentioned first in its name. +Although it can take a little while to get used to this scheme as everything is +written in the opposite order you may be used to, it offers the following +central benefit: the name summarizes the entry's meaning efficiently, even if +only part of it is read. This means that when a reader is scanning the application of a definition in a larger proof, they can get an overview by only scanning the first few words at each branching point/line. @@ -334,8 +335,8 @@ that is made. Finally, prepend the concluding type. applying the scheme we get - 1. `is-prop`, noting the assumption that `A` is a proposition. Remember, we do - not include variable names in the entry's name. + 1. `is-prop`, noting the assumption that `A` is a proposition. We do not + include variable names in the entry's name. 2. `is-prop-is-prop`, noting the assumption that `B` is a proposition. 3. `iff-is-prop-is-prop`, noting the assumption that we have a logical equivalence between `A` and `B`. @@ -500,7 +501,7 @@ original authors. ## References -Our style guide and design principles borrows heavily from +Our style guide and design principles borrow heavily from [`agda-unimath`](https://github.com/UniMath/agda-unimath). If you are looking for more inspiration, have a look at: From ae5c4a4094f937bfefdb934de2d1d2d437c93f15 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 23 Oct 2023 18:41:33 +0200 Subject: [PATCH 18/19] convention for additional line break after `:=` --- src/STYLEGUIDE.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index de58951e..5ad38881 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -227,6 +227,10 @@ later. ... ``` +- If you find that the separation between the type signature of a definition and + its construction is not visually clear, we permit the insertion of an + additional line break after the walrus separator (`:=`). + ## Naming conventions Adhering to a good naming convention is essential for keeping the library From 36724eb731e17f8a21b31bcf8740ae1e93ae6727 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 23 Oct 2023 22:34:29 +0200 Subject: [PATCH 19/19] some words on grouping --- src/STYLEGUIDE.md | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/src/STYLEGUIDE.md b/src/STYLEGUIDE.md index 5ad38881..acdec986 100644 --- a/src/STYLEGUIDE.md +++ b/src/STYLEGUIDE.md @@ -114,10 +114,22 @@ after the opening parentheses marking a branch is there to visually emphasize the tree structure of the definition, and synergizes with our convention to have two-space indentation level increases. -What is generally considered the "earliest sensible branching point" will depend -on context, and we ask that contributors practice common sense when determining -this. When in doubt, it is generally better to break lines sooner rather than -later. +What is generally considered the "earliest _sensible_ branching point" will +depend on context, and we ask that contributors practice common sense when +determining this. For instance, it may be sensible to group some arguments +together on a line. Already in our example above we wrote + +```rzk + hom2 A + ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂)) + ( \ t → k (t , 0₂)) + ( \ t → k (1₂ , t)) + ( h) +``` + +visually grouping together `hom2` and `A`, and again the next three arguments, +emphasizing their connection to eachother. When in doubt, it is generally better +to break lines sooner rather than later. ## Other code conventions