Rewrite rules for pushouts

Makefile

@@ -4,7 +4,7 @@
 # files, and if these options are pervasive (i.e. they need to be enabled in all
 # modules that include the modules that have them enabled), then they need to be
 # added to the everything file as well.
-everythingOpts := --guardedness --cohesion --flat-split
+everythingOpts := --guardedness --cohesion --flat-split --rewriting
 # use "$ export AGDAVERBOSE=-v20" if you want to see all
 AGDAVERBOSE ?= -v1
 

agda-unimath.agda-lib

@@ -1,3 +1,3 @@
 name: agda-unimath
 include: src
-flags: --without-K --exact-split --no-import-sorts --auto-inline
+flags: --without-K --exact-split --no-import-sorts --auto-inline -WnoWithoutKFlagPrimEraseEquality

src/foundation/constant-type-families.lagda.md

@@ -10,8 +10,10 @@ module foundation.constant-type-families where
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import foundation-core.commuting-squares-of-identifications
 open import foundation-core.dependent-identifications
 open import foundation-core.equivalences
 open import foundation-core.identity-types
@@ -79,6 +81,45 @@ tr-constant-type-family refl b = refl
 ```agda
 apd-constant-type-family :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A} (p : x ＝ y) →
-  apd f p ＝ (tr-constant-type-family p (f x) ∙ ap f p)
+  apd f p ＝ tr-constant-type-family p (f x) ∙ ap f p
 apd-constant-type-family f refl = refl
 ```
+
+### Naturality of transport in constant type families
+
+For every equality `p : x ＝ x'` in `A` and `q : y ＝ y'` in `B` we have a
+commuting square of identifications
+
+```text
+                    ap (tr (λ _ → B) p) q
+          tr (λ _ → B) p y ------> tr (λ _ → B) p y'
+                         |         |
+  tr-constant-family p y |         | tr-constant-family p y'
+                         ∨         ∨
+                         y ------> y'.
+                              q
+```
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  naturality-tr-constant-type-family :
+    {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
+    coherence-square-identifications
+      ( ap (tr (λ _ → B) p) q)
+      ( tr-constant-type-family p y)
+      ( tr-constant-type-family p y')
+      ( q)
+  naturality-tr-constant-type-family p refl = right-unit
+
+  naturality-inv-tr-constant-type-family :
+    {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
+    coherence-square-identifications
+      ( q)
+      ( inv (tr-constant-type-family p y))
+      ( inv (tr-constant-type-family p y'))
+      ( ap (tr (λ _ → B) p) q)
+  naturality-inv-tr-constant-type-family p refl = right-unit
+```

src/foundation/dependent-identifications.lagda.md

@@ -43,7 +43,7 @@ module _
     {x' : B x} {y' : B y}
     (p' : dependent-identification B p x' y')
     (q' : dependent-identification B q x' y') →
-    p' ＝ ((tr² B α _) ∙ q') → dependent-identification² B α p' q'
+    p' ＝ tr² B α x' ∙ q' → dependent-identification² B α p' q'
   map-compute-dependent-identification² refl ._ refl refl =
     refl
 
@@ -52,7 +52,7 @@ module _
     {x' : B x} {y' : B y}
     (p' : dependent-identification B p x' y')
     (q' : dependent-identification B q x' y') →
-    dependent-identification² B α p' q' → p' ＝ ((tr² B α _) ∙ q')
+    dependent-identification² B α p' q' → p' ＝ tr² B α x' ∙ q'
   map-inv-compute-dependent-identification² refl refl ._ refl =
     refl
 
@@ -93,7 +93,7 @@ module _
     {x' : B x} {y' : B y}
     (p' : dependent-identification B p x' y')
     (q' : dependent-identification B q x' y') →
-    (p' ＝ ((tr² B α _) ∙ q')) ≃ dependent-identification² B α p' q'
+    (p' ＝ tr² B α x' ∙ q') ≃ dependent-identification² B α p' q'
   pr1 (compute-dependent-identification² α p' q') =
     map-compute-dependent-identification² α p' q'
   pr2 (compute-dependent-identification² α p' q') =

src/foundation/transport-along-identifications.lagda.md

@@ -75,7 +75,7 @@ equiv-tr-refl B = refl
 
 ```agda
 tr-loop :
-  {l1 : Level} {A : UU l1} {a0 a1 : A} (p : a0 ＝ a1) (l : a0 ＝ a0) →
-  (tr (λ y → y ＝ y) p l) ＝ ((inv p ∙ l) ∙ p)
-tr-loop refl l = inv right-unit
+  {l1 : Level} {A : UU l1} {a0 a1 : A} (p : a0 ＝ a1) (q : a0 ＝ a0) →
+  tr (λ y → y ＝ y) p q ＝ (inv p ∙ q) ∙ p
+tr-loop refl q = inv right-unit
 ```

src/reflection.lagda.md

@@ -1,5 +1,9 @@
 # Reflection
 
+```agda
+{-# OPTIONS --rewriting #-}
+```
+
 ## Files in the reflection folder
 
 ```agda
@@ -9,12 +13,14 @@ open import reflection.abstractions public
 open import reflection.arguments public
 open import reflection.boolean-reflection public
 open import reflection.definitions public
+open import reflection.erasing-equality public
 open import reflection.fixity public
 open import reflection.group-solver public
 open import reflection.literals public
 open import reflection.metavariables public
 open import reflection.names public
 open import reflection.precategory-solver public
+open import reflection.rewriting public
 open import reflection.terms public
 open import reflection.type-checking-monad public
 ```

src/reflection/erasing-equality.lagda.md

@@ -0,0 +1,47 @@
+# Erasing equality
+
+```agda
+module reflection.erasing-equality where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+Agda's builtin primitive `primEraseEquality` is a special construct on
+[identifications](foundation-core.identity-types.md) that for every
+identification `x ＝ y` gives an identification `x ＝ y` with the following
+reduction behaviour:
+
+- If the two end points `x ＝ y` normalize to the same term, `primEraseEquality`
+  reduces to `refl`.
+
+For example, `primEraseEquality` applied to the loop of the
+[circle](synthetic-homotopy-theory.circle.md) will compute to `refl`, while
+`primEraseEquality` applied to the nontrivial identification in the
+[interval](synthetic-homotopy-theory.interval-type.md) will not reduce.
+
+This primitive is useful for [rewrite rules](reflection.rewriting.md), as it
+ensures that the identification used in defining the rewrite rule also computes
+to `refl`. Concretely, if the identification `β` defines a rewrite rule, and `β`
+is defined via `primEraseEqaulity`, then we have the strict equality `β ≐ refl`.
+
+## Primitives
+
+```agda
+primitive
+  primEraseEquality : {l : Level} {A : UU l} {x y : A} → x ＝ y → x ＝ y
+```
+
+## External links
+
+- [Built-ins#Equality](https://agda.readthedocs.io/en/latest/language/built-ins.html#equality)
+  at Agda's documentation pages

src/reflection/rewriting.lagda.md

@@ -0,0 +1,49 @@
+# Rewriting
+
+```agda
+{-# OPTIONS --rewriting #-}
+
+module reflection.rewriting where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+Agda's rewriting functionality allows us to add new strict equalities to our
+type theory. Given an [identification](foundation-core.identity-types.md)
+`β : x ＝ y`, then adding a rewrite rule for `β` with
+
+```text
+{-# REWRITE β #-}
+```
+
+will make it so `x` rewrites to `y`, i.e., `x ≐ y`.
+
+**Warning.** Rewriting is by nature a very unsafe tool so we advice exercising
+abundant caution when defining such rules.
+
+## Definitions
+
+We declare to Agda that the
+[standard identity relation](foundation.identity-types.md) may be used to define
+rewrite rules.
+
+```agda
+{-# BUILTIN REWRITE _＝_ #-}
+```
+
+## See also
+
+- [Erasing equality](reflection.erasing-equality.md)
+
+## External links
+
+- [Rewriting](https://agda.readthedocs.io/en/latest/language/rewriting.html) at
+  Agda's documentation pages

src/synthetic-homotopy-theory.lagda.md

@@ -1,5 +1,9 @@
 # Synthetic homotopy theory
 
+```agda
+{-# OPTIONS --rewriting #-}
+```
+
 ## Files in the synthetic homotopy theory folder
 
 ```agda
@@ -90,7 +94,9 @@ open import synthetic-homotopy-theory.pullback-property-pushouts public
 open import synthetic-homotopy-theory.pushout-products public
 open import synthetic-homotopy-theory.pushouts public
 open import synthetic-homotopy-theory.pushouts-of-pointed-types public
+open import synthetic-homotopy-theory.recursion-principle-pushouts public
 open import synthetic-homotopy-theory.retracts-of-sequential-diagrams public
+open import synthetic-homotopy-theory.rewriting-pushouts public
 open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.sequential-colimits public
 open import synthetic-homotopy-theory.sequential-diagrams public

src/synthetic-homotopy-theory/cocones-under-spans.lagda.md

@@ -117,15 +117,39 @@ module _
         ( vertical-htpy-cocone)
     coherence-htpy-cocone = pr2 (pr2 H)
 
-  reflexive-htpy-cocone :
+  refl-htpy-cocone :
     (c : cocone f g X) → htpy-cocone c c
-  pr1 (reflexive-htpy-cocone (i , j , H)) = refl-htpy
-  pr1 (pr2 (reflexive-htpy-cocone (i , j , H))) = refl-htpy
-  pr2 (pr2 (reflexive-htpy-cocone (i , j , H))) = right-unit-htpy
+  pr1 (refl-htpy-cocone (i , j , H)) = refl-htpy
+  pr1 (pr2 (refl-htpy-cocone (i , j , H))) = refl-htpy
+  pr2 (pr2 (refl-htpy-cocone (i , j , H))) = right-unit-htpy
 
   htpy-eq-cocone :
     (c c' : cocone f g X) → c ＝ c' → htpy-cocone c c'
-  htpy-eq-cocone c .c refl = reflexive-htpy-cocone c
+  htpy-eq-cocone c .c refl = refl-htpy-cocone c
+
+  module _
+    (c c' : cocone f g X)
+    (p : c ＝ c')
+    where
+
+    horizontal-htpy-eq-cocone :
+      horizontal-map-cocone f g c ~
+      horizontal-map-cocone f g c'
+    horizontal-htpy-eq-cocone =
+      horizontal-htpy-cocone c c' (htpy-eq-cocone c c' p)
+
+    vertical-htpy-eq-cocone :
+      vertical-map-cocone f g c ~
+      vertical-map-cocone f g c'
+    vertical-htpy-eq-cocone =
+      vertical-htpy-cocone c c' (htpy-eq-cocone c c' p)
+
+    coherence-square-htpy-eq-cocone :
+      statement-coherence-htpy-cocone c c'
+        ( horizontal-htpy-eq-cocone)
+        ( vertical-htpy-eq-cocone)
+    coherence-square-htpy-eq-cocone =
+      coherence-htpy-cocone c c' (htpy-eq-cocone c c' p)
 
   is-torsorial-htpy-cocone :
     (c : cocone f g X) → is-torsorial (htpy-cocone c)