Finish draft of the style guide

.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",

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

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

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:

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:

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:
 

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:

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