Computational identity types

.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`
 

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,33 @@ table given above.
 
 ### Concatenation of identifications
 
+The
+{{#concept "concatenation operation on identifications" Agda=_∙_ Agda=_∙'_ Agda=concat}}
+is a map
+
+```text
+  _∙_ : x ＝ y → y ＝ z → x ＝ z
+```
+
+for all `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 `_∙_` 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 use the first alternative by convention.
+
+See also
+
+- [The definitionally right unital concatenation operation on indentifications](foundation.definitionally-right-unital-concatenation-identifications.md)
+- [The yoneda identity types](foundation.yoneda-identity-types.md)
+
 ```agda
 module _
   {l : Level} {A : UU l}
@@ -432,11 +459,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
@@ -92,6 +93,7 @@ open import foundation.decidable-propositions public
 open import foundation.decidable-relations public
 open import foundation.decidable-subtypes public
 open import foundation.decidable-types public
+open import foundation.definitionally-right-unital-concatenation-identifications public
 open import foundation.dependent-binary-homotopies public
 open import foundation.dependent-binomial-theorem public
 open import foundation.dependent-epimorphisms public
@@ -331,6 +333,7 @@ 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.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
 ```