Refactor synthetic homotopy theory (#654)

- Hyperlinks throughout `synthetic-homotopy-theory`
- Using `coherence-square-identifications` and
`dependent-identifications` in `interval`
- Changing the order of arguments of `coherence-square-identifications`
to be the same as for maps

This PR builds on #649 and #650, and works toward progressing item 8 of
#195.

---------

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

src/foundation-core.lagda.md

@@ -25,7 +25,6 @@ open import foundation-core.equality-dependent-pair-types public
 open import foundation-core.equivalence-relations public
 open import foundation-core.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/homotopies.lagda.md

@@ -41,7 +41,7 @@ module _
 
   map-compute-dependent-identification-eq-value :
     {x y : X} (p : x ＝ y) (q : eq-value x) (r : eq-value y) →
-    coherence-square-identifications (apd f p) r (ap (tr P p) q) (apd g p) →
+    coherence-square-identifications (ap (tr P p) q) (apd f p) (apd g p) r →
     dependent-identification eq-value p q r
   map-compute-dependent-identification-eq-value refl q r =
     inv ∘ (concat' r (right-unit ∙ ap-id q))
@@ -61,22 +61,22 @@ module _
 
   map-compute-dependent-identification-eq-value-function :
     {x y : X} (p : x ＝ y) (q : eq-value f g x) (r : eq-value f g y) →
-    coherence-square-identifications (ap f p) r q (ap g p) →
+    coherence-square-identifications q (ap f p) (ap g p) r →
     dependent-identification eq-value-function p q r
   map-compute-dependent-identification-eq-value-function refl q r =
     inv ∘ concat' r right-unit
 
 map-compute-dependent-identification-eq-value-id-id :
   {l1 : Level} {A : UU l1} {a b : A} (p : a ＝ b) (q : a ＝ a) (r : b ＝ b) →
-  coherence-square-identifications p r q p →
+  coherence-square-identifications q p p r →
   dependent-identification (eq-value id id) p q r
 map-compute-dependent-identification-eq-value-id-id refl q r s =
   inv (s ∙ right-unit)
 
 map-compute-dependent-identification-eq-value-comp-id :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : B → A) (f : A → B) {a b : A}
   (p : a ＝ b) (q : eq-value (g ∘ f) id a) (r : eq-value (g ∘ f) id b) →
-  coherence-square-identifications (ap g (ap f p)) r q p →
+  coherence-square-identifications q (ap g (ap f p)) p r →
   dependent-identification (eq-value (g ∘ f) id) p q r
 map-compute-dependent-identification-eq-value-comp-id g f refl q r s =
   inv (s ∙ right-unit)
@@ -335,7 +335,7 @@ syntax step-homotopy-reasoning p h q = p ~ h by q
 
 - We postulate that homotopies characterize identifications of (dependent)
   functions in the file
-  [`foundation-core.function-extensionality`](foundation-core.function-extensionality.md).
+  [`foundation.function-extensionality`](foundation.function-extensionality.md).
 - [Multivariable homotopies](foundation.multivariable-homotopies.md).
 - The [whiskering operations](foundation.whiskering-homotopies.md) on
   homotopies.

src/foundation-core/propositions.lagda.md

@@ -8,13 +8,13 @@ module foundation-core.propositions where
 
 ```agda
 open import foundation.dependent-pair-types
+open import foundation.function-extensionality
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
 open import foundation-core.contractible-types
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
-open import foundation-core.function-extensionality
 open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types

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

@@ -7,6 +7,7 @@ module foundation-core.transport-along-identifications where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.universe-levels
 
 open import foundation-core.identity-types
@@ -25,7 +26,7 @@ The fact that `tr B p` is an [equivalence](foundation-core.equivalences.md) is
 recorded in
 [`foundation.transport-along-identifications`](foundation.transport-along-identifications.md).
 
-## Definition
+## Definitions
 
 ### Transport
 
@@ -79,6 +80,17 @@ preserves-tr :
 preserves-tr f refl x = refl
 ```
 
+### Transporting along the action on identifications of a function
+
+```agda
+tr-ap :
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : UU l3} {D : C → UU l4}
+  (f : A → C) (g : (x : A) → B x → D (f x))
+  {x y : A} (p : x ＝ y) (z : B x) →
+  tr D (ap f p) (g x z) ＝ g y (tr B p z)
+tr-ap f g refl z = refl
+```
+
 ### Computing maps out of identity types as transports
 
 ```agda
@@ -91,3 +103,21 @@ module _
     (x : A) (p : a ＝ x) → f x p ＝ tr B p (f a refl)
   compute-map-out-of-identity-type x refl = refl
 ```
+
+### Computing transport in the type family of identifications with a fixed target
+
+```agda
+tr-Id-left :
+  {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : b ＝ a) →
+  tr (_＝ a) q p ＝ ((inv q) ∙ p)
+tr-Id-left refl p = refl
+```
+
+### Computing transport in the type family of identifications with a fixed source
+
+```agda
+tr-Id-right :
+  {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : a ＝ b) →
+  tr (a ＝_) q p ＝ (p ∙ q)
+tr-Id-right refl refl = refl
+```

src/foundation.lagda.md

@@ -83,6 +83,7 @@ open import foundation.decidable-types public
 open import foundation.dependent-binary-homotopies public
 open import foundation.dependent-binomial-theorem public
 open import foundation.dependent-epimorphisms public
+open import foundation.dependent-homotopies public
 open import foundation.dependent-identifications public
 open import foundation.dependent-pair-types public
 open import foundation.dependent-sequences public
@@ -290,6 +291,7 @@ open import foundation.towers public
 open import foundation.transfinite-cocomposition-of-maps public
 open import foundation.transport-along-equivalences public
 open import foundation.transport-along-higher-identifications public
+open import foundation.transport-along-homotopies public
 open import foundation.transport-along-identifications public
 open import foundation.trivial-relaxed-sigma-decompositions public
 open import foundation.trivial-sigma-decompositions public

src/foundation/action-on-identifications-functions.lagda.md

@@ -12,7 +12,6 @@ open import foundation.universe-levels
 open import foundation-core.constant-maps
 open import foundation-core.function-types
 open import foundation-core.identity-types
-open import foundation-core.transport-along-identifications
 ```
 
 </details>
@@ -97,17 +96,6 @@ ap-const :
 ap-const b refl = refl
 ```
 
-### Transporting along the action on identifications of a function
-
-```agda
-tr-ap :
-  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : UU l3} {D : C → UU l4}
-  (f : A → C) (g : (x : A) → B x → D (f x))
-  {x y : A} (p : x ＝ y) (z : B x) →
-  tr D (ap f p) (g x z) ＝ g y (tr B p z)
-tr-ap f g refl z = refl
-```
-
 ### The action on identifications of concatenating by `refl` on the right
 
 Note that `_∙ refl` is only homotopic to the identity function. Therefore we

src/foundation/cantors-diagonal-argument.lagda.md

@@ -8,6 +8,7 @@ module foundation.cantors-diagonal-argument where
 
 ```agda
 open import foundation.dependent-pair-types
+open import foundation.function-extensionality
 open import foundation.logical-equivalences
 open import foundation.negation
 open import foundation.propositional-truncations
@@ -16,7 +17,6 @@ open import foundation.universe-levels
 
 open import foundation-core.empty-types
 open import foundation-core.fibers-of-maps
-open import foundation-core.function-extensionality
 open import foundation-core.propositions
 ```
 

src/foundation/commuting-squares-of-identifications.lagda.md

@@ -42,9 +42,8 @@ module _
   where
 
   coherence-square-identifications :
-    (left : x ＝ z) (bottom : z ＝ w)
-    (top : x ＝ y) (right : y ＝ w) → UU l
-  coherence-square-identifications left bottom top right =
+    (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) → UU l
+  coherence-square-identifications top left right bottom =
     (left ∙ bottom) ＝ (top ∙ right)
 ```
 
@@ -65,10 +64,10 @@ module _
   where
 
   coherence-square-identifications-comp-horizontal :
-    coherence-square-identifications p-left p-bottom p-top middle →
-    coherence-square-identifications middle q-bottom q-top q-right →
+    coherence-square-identifications p-top p-left middle p-bottom →
+    coherence-square-identifications q-top middle q-right q-bottom →
     coherence-square-identifications
-      p-left (p-bottom ∙ q-bottom) (p-top ∙ q-top) q-right
+      (p-top ∙ q-top) p-left q-right (p-bottom ∙ q-bottom)
   coherence-square-identifications-comp-horizontal p q =
     ( ( ( inv (assoc p-left p-bottom q-bottom) ∙
           ap-binary (_∙_) p (refl {x = q-bottom})) ∙
@@ -85,10 +84,10 @@ module _
   where
 
   coherence-square-identifications-comp-vertical :
-    coherence-square-identifications p-left middle p-top p-right →
-    coherence-square-identifications q-left q-bottom middle q-right →
+    coherence-square-identifications p-top p-left p-right middle →
+    coherence-square-identifications middle q-left q-right q-bottom →
     coherence-square-identifications
-      (p-left ∙ q-left) q-bottom p-top (p-right ∙ q-right)
+      p-top (p-left ∙ q-left) (p-right ∙ q-right) q-bottom
   coherence-square-identifications-comp-vertical p q =
     ( assoc p-left q-left q-bottom ∙
       ( ( ap-binary (_∙_) (refl {x = p-left}) q ∙
@@ -111,26 +110,26 @@ module _
 
   coherence-square-identifications-left-paste :
     {left' : x ＝ z} (s : left ＝ left') →
-    coherence-square-identifications left bottom top right →
-    coherence-square-identifications left' bottom top right
+    coherence-square-identifications top left right bottom →
+    coherence-square-identifications top left' right bottom
   coherence-square-identifications-left-paste refl sq = sq
 
   coherence-square-identifications-bottom-paste :
     {bottom' : z ＝ w} (s : bottom ＝ bottom') →
-    coherence-square-identifications left bottom top right →
-    coherence-square-identifications left bottom' top right
+    coherence-square-identifications top left right bottom →
+    coherence-square-identifications top left right bottom'
   coherence-square-identifications-bottom-paste refl sq = sq
 
   coherence-square-identifications-top-paste :
     {top' : x ＝ y} (s : top ＝ top') →
-    coherence-square-identifications left bottom top right →
-    coherence-square-identifications left bottom top' right
+    coherence-square-identifications top left right bottom →
+    coherence-square-identifications top' left right bottom
   coherence-square-identifications-top-paste refl sq = sq
 
   coherence-square-identifications-right-paste :
     {right' : y ＝ w} (s : right ＝ right') →
-    coherence-square-identifications left bottom top right →
-    coherence-square-identifications left bottom top right'
+    coherence-square-identifications top left right bottom →
+    coherence-square-identifications top left right' bottom
   coherence-square-identifications-right-paste refl sq = sq
 ```
 
@@ -147,36 +146,36 @@ module _
 
   coherence-square-identifications-top-left-whisk' :
     {x' : A} (p : x' ＝ x) →
-    coherence-square-identifications left bottom top right →
-    coherence-square-identifications (p ∙ left) bottom (p ∙ top) right
+    coherence-square-identifications top left right bottom →
+    coherence-square-identifications (p ∙ top) (p ∙ left) right bottom
   coherence-square-identifications-top-left-whisk' refl sq = sq
 
   coherence-square-identifications-top-left-whisk :
     {x' : A} (p : x ＝ x') →
-    coherence-square-identifications left bottom top right →
-    coherence-square-identifications (inv p ∙ left) bottom (inv p ∙ top) right
+    coherence-square-identifications top left right bottom →
+    coherence-square-identifications (inv p ∙ top) (inv p ∙ left) right bottom
   coherence-square-identifications-top-left-whisk refl sq = sq
 
   coherence-square-identifications-top-right-whisk :
     {y' : A} (p : y ＝ y') →
-    coherence-square-identifications left bottom top right →
-    coherence-square-identifications left bottom (top ∙ p) (inv p ∙ right)
+    coherence-square-identifications top left right bottom →
+    coherence-square-identifications (top ∙ p) left (inv p ∙ right) bottom
   coherence-square-identifications-top-right-whisk refl =
     coherence-square-identifications-top-paste
       left bottom top right (inv right-unit)
 
   coherence-square-identifications-bottom-left-whisk :
     {z' : A} (p : z ＝ z') →
-    coherence-square-identifications left bottom top right →
-    coherence-square-identifications (left ∙ p) (inv p ∙ bottom) top right
+    coherence-square-identifications top left right bottom →
+    coherence-square-identifications top (left ∙ p) right (inv p ∙ bottom)
   coherence-square-identifications-bottom-left-whisk refl =
     coherence-square-identifications-left-paste
       left bottom top right (inv right-unit)
 
   coherence-square-identifications-bottom-right-whisk :
     {w' : A} (p : w ＝ w') →
-    coherence-square-identifications left bottom top right →
-    coherence-square-identifications left (bottom ∙ p) top (right ∙ p)
+    coherence-square-identifications top left right bottom →
+    coherence-square-identifications top left (right ∙ p) (bottom ∙ p)
   coherence-square-identifications-bottom-right-whisk refl =
     ( coherence-square-identifications-bottom-paste
       left bottom top (right ∙ refl) (inv right-unit)) ∘