Sequential limits

scripts/generate_main_index_file.py

@@ -67,7 +67,7 @@ def generate_index(root, header):
     namespaces = sorted(set(utils.get_subdirectories_recursive(root)))
 
     for namespace in namespaces:
-        if namespace == 'temp':
+        if namespace == 'temp' or 'MAlonzo' in namespace:
             continue
         entry_list, s = generate_namespace_entry_list(namespace)
         entry_lists.append(entry_list)

scripts/generate_namespace_index_modules.py

@@ -45,7 +45,7 @@ def generate_agda_block(root, namespace):
     root = 'src'
 
     for namespace in utils.get_subdirectories_recursive(root):
-        if namespace == 'temp':
+        if namespace == 'temp' or 'MAlonzo' in namespace:
             continue
 
         namespace_filename = os.path.join(root, namespace) + '.lagda.md'

src/foundation-core/commuting-triangles-of-maps.lagda.md

@@ -22,15 +22,20 @@ open import foundation-core.whiskering-homotopies
 A triangle of maps
 
 ```text
- A ----> B
-  \     /
-   \   /
-    V V
-     X
+      top
+   A ----> B
+    \     /
+left \   / right
+      V V
+       X
 ```
 
 is said to commute if there is a homotopy between the map on the left and the
-composite map.
+composite map
+
+```text
+  left ~ right ∘ top.
+```
 
 ## Definitions
 
@@ -43,11 +48,11 @@ module _
 
   coherence-triangle-maps :
     (left : A → X) (right : B → X) (top : A → B) → UU (l1 ⊔ l2)
-  coherence-triangle-maps left right top = left ~ (right ∘ top)
+  coherence-triangle-maps left right top = left ~ right ∘ top
 
   coherence-triangle-maps' :
     (left : A → X) (right : B → X) (top : A → B) → UU (l1 ⊔ l2)
-  coherence-triangle-maps' left right top = (right ∘ top) ~ left
+  coherence-triangle-maps' left right top = right ∘ top ~ left
 ```
 
 ### Concatenation of commuting triangles of maps
@@ -92,3 +97,17 @@ module _
       ( precomp right W)
   precomp-coherence-triangle-maps' H W = htpy-precomp H W
 ```
+
+### Coherences of commuting triangles of maps with fixed vertices
+
+```agda
+coherence-coherence-triangle-maps :
+  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
+  (left : A → X) (right : B → X) (top : A → B)
+  (left' : A → X) (right' : B → X) (top' : A → B) →
+  coherence-triangle-maps left right top →
+  coherence-triangle-maps left' right' top' →
+  left ~ left' → right ~ right' → top ~ top' → UU (l1 ⊔ l2)
+coherence-coherence-triangle-maps left right top left' right' top' c c' L R T =
+  c ∙h htpy-comp-horizontal T R ~ L ∙h c'
+```

src/foundation-core/equality-dependent-pair-types.lagda.md

@@ -7,6 +7,7 @@ module foundation-core.equality-dependent-pair-types where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.universe-levels
 
@@ -51,13 +52,26 @@ module _
   pair-eq-Σ {s} refl = refl-Eq-Σ s
 
   eq-pair-Σ :
-    {s t : Σ A B} (α : pr1 s ＝ pr1 t) →
+    {s t : Σ A B}
+    (α : pr1 s ＝ pr1 t) →
     dependent-identification B α (pr2 s) (pr2 t) → s ＝ t
-  eq-pair-Σ {pair x y} {pair .x .y} refl refl = refl
+  eq-pair-Σ refl refl = refl
 
   eq-pair-Σ' : {s t : Σ A B} → Eq-Σ s t → s ＝ t
   eq-pair-Σ' p = eq-pair-Σ (pr1 p) (pr2 p)
 
+  eq-pair-Σ-eq-pr1 :
+    {x y : A} {s : B x} (p : x ＝ y) → (x , s) ＝ (y , tr B p s)
+  eq-pair-Σ-eq-pr1 refl = refl
+
+  eq-pair-Σ-eq-pr1' :
+    {x y : A} {t : B y} (p : x ＝ y) → (x , tr B (inv p) t) ＝ (y , t)
+  eq-pair-Σ-eq-pr1' refl = refl
+
+  eq-pair-Σ-eq-pr2 :
+    {x : A} {s t : B x} → s ＝ t → (x , s) ＝ (x , t)
+  eq-pair-Σ-eq-pr2 {x} = ap {B = Σ A B} (x ,_)
+
   is-retraction-pair-eq-Σ :
     (s t : Σ A B) →
     ((pair-eq-Σ {s} {t}) ∘ (eq-pair-Σ' {s} {t})) ~ id {A = Eq-Σ s t}

src/foundation-core/equivalences.lagda.md

@@ -402,7 +402,7 @@ abstract
 abstract
   is-equiv-is-section :
     {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A} →
-    is-equiv f → (f ∘ g) ~ id → is-equiv g
+    is-equiv f → f ∘ g ~ id → is-equiv g
   is-equiv-is-section {B = B} {f = f} {g = g} is-equiv-f H =
     is-equiv-right-factor-htpy id f g (inv-htpy H) is-equiv-f is-equiv-id
 ```

src/foundation-core/homotopies.lagda.md

@@ -7,7 +7,6 @@ module foundation-core.homotopies where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-squares-of-identifications
@@ -334,8 +333,8 @@ syntax step-homotopy-reasoning p h q = p ~ h by q
 
 ## See also
 
-- We postulate that homotopies characterize identifications in (dependent)
-  function types in the file
+- We postulate that homotopies characterize identifications of (dependent)
+  functions in the file
   [`foundation-core.function-extensionality`](foundation-core.function-extensionality.md).
 - The whiskering operations on homotopies are defined in the file
   [`foundation.whiskering-homotopies`](foundation.whiskering-homotopies.md).