Computational identity types (#1015)

### Summary
Adds
- the strictly right unital concatenation operation on identity types.
- the _strictly involutive identity types_. They satisfy the judgmental
laws
  1. `inv (inv p) ≐ p`
  2. `inv refl ≐ refl`
  3. `refl ∙ p ≐ p` or `p ∙ refl ≐ p`
  4. `ind-Id B f refl ≐ f refl`
-  the _Yoneda identity types_. They satisfy the judgmental laws
    1. `(p ∙ q) ∙ r ≐ p ∙ (q ∙ r)`
    2. `refl ∙ p ≐ p`
    3. `p ∙ refl ≐ p`
    4. `inv refl ≐ refl`
    5.   `rec-Id f refl ≐ f refl`
- the _computational identity types_. They satisfy the judgmental laws
  1.  `inv (inv p) ≐ p`
  2. `inv refl ≐ refl`
  3. `refl ∙ p ≐ p` or `p ∙ refl ≐ p`
  4. `(p ∙ q) ∙ r ≐ p ∙ (q ∙ r)`
  5.   `rec-Id f refl ≐ f refl`

### References
-
https://groups.google.com/g/homotopytypetheory/c/FfiZj1vrkmQ/m/GJETdy0AAgAJ

.vscode/agda.code-snippets

@@ -8,11 +8,27 @@
   "Full width equals sign (＝)": {
     "body": ["＝"],
     "description": "Full width equals sign",
-    "prefix": ["Id", "equals"]
+    "prefix": ["Id"]
   },
   "Yoneda embedding (ょ)": {
     "body": ["ょ"],
     "description": "Yoneda embedding",
     "prefix": ["yoneda"]
+  },
+
+  "Equational reasoning": {
+    "body": ["equational-reasoning ? ＝ ? by ?"],
+    "description": "Equational reasoning",
+    "prefix": ["equational-reasoning"]
+  },
+  "Homotopy-reasoning": {
+    "body": ["homotopy-reasoning ? ~ ? by ?"],
+    "description": "Homotopy-reasoning",
+    "prefix": ["homotopy-reasoning"]
+  },
+  "Equivalence-reasoning": {
+    "body": ["equivalence-reasoning ? ≃ ? by ?"],
+    "description": "Equivalence-reasoning",
+    "prefix": ["equivalence-reasoning"]
   }
 }

HOWTO-INSTALL.md

@@ -259,7 +259,7 @@ To insert these symbols in the editor, follow these steps:
 2. When the symbol appears as a greyed-out character in your editor, press `TAB`
    to insert it.
 
-- `＝`: Type `Id` or `equals`
+- `＝`: Type `Id`
 - `ょ`: Type `yoneda`
 - `⧄`: Type `diagonal` or `lifting`
 

MIXFIX-OPERATORS.md

@@ -121,7 +121,7 @@ operators, so that expressions like `a - b + c` are parsed as `(a - b) + c`.
 
 Below, we outline a list of general rules when assigning associativities.
 
-- **Definitionally associative operators**, e.g.
+- **Strictly associative operators**, e.g.
   [function composition `_∘_`](foundation-core.function-types.md), can be
   assigned _any associativity_.
 

src/category-theory/yoneda-lemma-categories.lagda.md

@@ -47,7 +47,7 @@ equivalence.
 
 ## Theorem
 
-### The yoneda lemma into the large category of sets
+### The Yoneda lemma into the large category of sets
 
 ```agda
 module _

src/category-theory/yoneda-lemma-precategories.lagda.md

@@ -54,7 +54,7 @@ equivalence.
 
 ## Theorem
 
-### The yoneda lemma into the large category of sets
+### The Yoneda lemma into the large category of sets
 
 ```agda
 module _

src/foundation-core.lagda.md

@@ -28,7 +28,6 @@ open import foundation-core.equivalence-relations public
 open import foundation-core.equivalences public
 open import foundation-core.families-of-equivalences public
 open import foundation-core.fibers-of-maps public
-open import foundation-core.function-extensionality public
 open import foundation-core.function-types public
 open import foundation-core.functoriality-dependent-function-types public
 open import foundation-core.functoriality-dependent-pair-types public

src/foundation-core/identity-types.lagda.md

@@ -139,6 +139,35 @@ table given above.
 
 ### Concatenation of identifications
 
+The
+{{#concept "concatenation operation on identifications" Agda=_∙_ Agda=_∙'_ Agda=concat}}
+is a family of binary operations
+
+```text
+  _∙_ : x ＝ y → y ＝ z → x ＝ z
+```
+
+indexed by `x y z : A`. However, there are essentially three different ways we
+can define concatenation of identifications, all with different computational
+behaviours.
+
+1. We can define concatenation by induction on the equality `x ＝ y`. This gives
+   us the computation rule `refl ∙ q ≐ q`.
+2. We can define concatenation by induction on the equality `y ＝ z`. This gives
+   us the computation rule `p ∙ refl ≐ p`.
+3. We can define concatenation by induction on both `x ＝ y` and `y ＝ z`. This
+   only gives us the computation rule `refl ∙ refl ≐ refl`.
+
+While the third option may be preferred by some for its symmetry, for practical
+reasons, we prefer one of the first two, and by convention we use the first
+alternative.
+
+The second option is considered in
+[`foundation.strictly-right-unital-concatenation-identifications`](foundation.strictly-right-unital-concatenation-identifications.md),
+and in [`foundation.yoneda-identity-types`](foundation.yoneda-identity-types.md)
+we construct an identity type which satisfies both computation rules among
+others.
+
 ```agda
 module _
   {l : Level} {A : UU l}
@@ -432,11 +461,11 @@ module _
   where
 
   is-injective-concat :
-    {x y z : A} (p : x ＝ y) {q r : y ＝ z} → (p ∙ q) ＝ (p ∙ r) → q ＝ r
+    {x y z : A} (p : x ＝ y) {q r : y ＝ z} → p ∙ q ＝ p ∙ r → q ＝ r
   is-injective-concat refl s = s
 
   is-injective-concat' :
-    {x y z : A} (r : y ＝ z) {p q : x ＝ y} → (p ∙ r) ＝ (q ∙ r) → p ＝ q
+    {x y z : A} (r : y ＝ z) {p q : x ＝ y} → p ∙ r ＝ q ∙ r → p ＝ q
   is-injective-concat' refl s = (inv right-unit) ∙ (s ∙ right-unit)
 ```
 

src/foundation.lagda.md

@@ -62,6 +62,7 @@ open import foundation.complements public
 open import foundation.complements-subtypes public
 open import foundation.composite-maps-in-inverse-sequential-diagrams public
 open import foundation.composition-algebra public
+open import foundation.computational-identity-types public
 open import foundation.cones-over-cospan-diagrams public
 open import foundation.cones-over-inverse-sequential-diagrams public
 open import foundation.conjunction public
@@ -331,6 +332,8 @@ open import foundation.spans public
 open import foundation.spans-families-of-types public
 open import foundation.split-surjective-maps public
 open import foundation.standard-apartness-relations public
+open import foundation.strictly-involutive-identity-types public
+open import foundation.strictly-right-unital-concatenation-identifications public
 open import foundation.strongly-extensional-maps public
 open import foundation.structure public
 open import foundation.structure-identity-principle public
@@ -428,4 +431,5 @@ open import foundation.whiskering-homotopies-composition public
 open import foundation.whiskering-homotopies-concatenation public
 open import foundation.whiskering-identifications-concatenation public
 open import foundation.whiskering-operations public
+open import foundation.yoneda-identity-types public
 ```