From aa95b6e29ad252904e9e6e33f6ca82985822428c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 25 Apr 2024 14:48:48 +0200 Subject: [PATCH] chore: Fix arrowheads in character diagrams (#1124) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replaces capital and lower-case `V` arrowheads in character diagrams with the logical or character `∨`, and the caret arrowheads `^` with logical and `∧`. Also fixes a couple of miscellaneous issues with some diagrams like lacking indentation and whitespace. --- .../adjunctions-large-categories.lagda.md | 2 +- .../adjunctions-large-precategories.lagda.md | 2 +- ...-morphisms-in-large-precategories.lagda.md | 2 +- ...res-of-morphisms-in-precategories.lagda.md | 2 +- ...ares-of-morphisms-in-set-magmoids.lagda.md | 2 +- src/category-theory/gaunt-categories.lagda.md | 6 +- ...ions-functors-cores-precategories.lagda.md | 2 +- .../delooping-sign-homomorphism.lagda.md | 2 +- .../coherently-invertible-maps.lagda.md | 2 +- .../commuting-prisms-of-maps.lagda.md | 14 +-- .../commuting-squares-of-homotopies.lagda.md | 2 +- .../commuting-squares-of-maps.lagda.md | 2 +- .../commuting-triangles-of-maps.lagda.md | 6 +- src/foundation-core/equivalences.lagda.md | 4 +- .../operations-span-diagrams.lagda.md | 4 +- src/foundation-core/operations-spans.lagda.md | 4 +- src/foundation-core/pullbacks.lagda.md | 10 +- src/foundation-core/retractions.lagda.md | 4 +- src/foundation-core/sections.lagda.md | 4 +- ...ces-functions-out-of-subuniverses.lagda.md | 2 +- ...s-type-families-over-subuniverses.lagda.md | 2 +- ...ion-on-equivalences-type-families.lagda.md | 4 +- ...-identifications-binary-functions.lagda.md | 2 +- .../cartesian-morphisms-arrows.lagda.md | 6 +- .../commuting-prisms-of-maps.lagda.md | 40 +++---- .../commuting-squares-of-maps.lagda.md | 59 +++++----- .../commuting-tetrahedra-of-maps.lagda.md | 4 +- .../commuting-triangles-of-maps.lagda.md | 10 +- src/foundation/composition-algebra.lagda.md | 2 +- ...-over-inverse-sequential-diagrams.lagda.md | 2 +- src/foundation/copartial-elements.lagda.md | 8 +- src/foundation/copartial-functions.lagda.md | 4 +- src/foundation/coslice.lagda.md | 4 +- ...ndent-inverse-sequential-diagrams.lagda.md | 2 +- .../dependent-sums-pullbacks.lagda.md | 4 +- src/foundation/descent-equivalences.lagda.md | 2 +- .../diagonals-of-morphisms-arrows.lagda.md | 4 +- ...s-with-respect-to-truncated-types.lagda.md | 4 +- src/foundation/epimorphisms.lagda.md | 2 +- src/foundation/equivalences-arrows.lagda.md | 2 +- src/foundation/equivalences-cospans.lagda.md | 2 +- ...ences-inverse-sequential-diagrams.lagda.md | 2 +- ...s-span-diagrams-families-of-types.lagda.md | 2 +- .../equivalences-span-diagrams.lagda.md | 2 +- ...ivalences-spans-families-of-types.lagda.md | 2 +- src/foundation/fibered-equivalences.lagda.md | 2 +- src/foundation/fibered-involutions.lagda.md | 2 +- src/foundation/fibered-maps.lagda.md | 39 +++---- ...toriality-cartesian-product-types.lagda.md | 2 +- ...unctoriality-dependent-pair-types.lagda.md | 2 +- .../functoriality-fibers-of-maps.lagda.md | 12 +- .../homotopies-morphisms-arrows.lagda.md | 4 +- src/foundation/morphisms-arrows.lagda.md | 12 +- .../morphisms-cospan-diagrams.lagda.md | 2 +- src/foundation/morphisms-cospans.lagda.md | 2 +- ...hisms-inverse-sequential-diagrams.lagda.md | 2 +- .../morphisms-span-diagrams.lagda.md | 6 +- src/foundation/morphisms-spans.lagda.md | 4 +- .../morphisms-twisted-arrows.lagda.md | 2 +- .../operations-span-diagrams.lagda.md | 4 +- src/foundation/operations-spans.lagda.md | 4 +- src/foundation/partial-elements.lagda.md | 2 +- src/foundation/partial-functions.lagda.md | 2 +- ...stcomposition-dependent-functions.lagda.md | 4 +- ...recomposition-dependent-functions.lagda.md | 2 +- .../precomposition-functions.lagda.md | 2 +- .../preunivalent-type-families.lagda.md | 2 +- src/foundation/pullbacks-subtypes.lagda.md | 2 +- src/foundation/pullbacks.lagda.md | 2 +- src/foundation/retracts-of-maps.lagda.md | 20 ++-- src/foundation/standard-pullbacks.lagda.md | 6 +- .../univalent-type-families.lagda.md | 2 +- .../universal-property-pullbacks.lagda.md | 6 +- ...ng-squares-of-group-homomorphisms.lagda.md | 2 +- .../functoriality-quotient-groups.lagda.md | 2 +- .../homomorphisms-group-actions.lagda.md | 2 +- src/group-theory/pullbacks-subgroups.lagda.md | 2 +- .../pullbacks-subsemigroups.lagda.md | 2 +- src/group-theory/quotient-groups.lagda.md | 2 +- ...roups-generated-by-subsets-groups.lagda.md | 2 +- src/group-theory/torsion-free-groups.lagda.md | 2 +- ...rder-preserving-maps-large-posets.lagda.md | 2 +- .../cd-structures.lagda.md | 2 +- ...nsions-lifts-families-of-elements.lagda.md | 2 +- .../extensions-of-maps.lagda.md | 14 +-- ...ation-operations-function-classes.lagda.md | 4 +- ...perations-global-function-classes.lagda.md | 4 +- .../factorization-operations.lagda.md | 4 +- ...izations-of-maps-function-classes.lagda.md | 4 +- ...s-of-maps-global-function-classes.lagda.md | 4 +- .../factorizations-of-maps.lagda.md | 4 +- .../functoriality-higher-modalities.lagda.md | 4 +- .../lifting-operations.lagda.md | 2 +- .../lifts-families-of-elements.lagda.md | 2 +- .../lifts-of-maps.lagda.md | 20 ++-- .../modal-induction.lagda.md | 2 +- .../orthogonal-maps.lagda.md | 26 ++--- ...sition-lifts-families-of-elements.lagda.md | 12 +- .../pullback-hom.lagda.md | 2 +- .../regular-cd-structures.lagda.md | 2 +- ...ing-squares-of-pointed-homotopies.lagda.md | 2 +- .../equivalences-pointed-arrows.lagda.md | 2 +- .../morphisms-pointed-arrows.lagda.md | 14 +-- .../morphisms-twisted-pointed-arrows.lagda.md | 2 +- ...types-equipped-with-automorphisms.lagda.md | 2 +- ...types-equipped-with-endomorphisms.lagda.md | 2 +- src/structured-types/wild-monoids.lagda.md | 4 +- .../acyclic-maps.lagda.md | 2 +- .../cocartesian-morphisms-arrows.lagda.md | 2 +- ...cocones-under-sequential-diagrams.lagda.md | 2 +- .../cocones-under-spans.lagda.md | 110 +++++++++--------- ...endent-pullback-property-pushouts.lagda.md | 10 +- .../dependent-pushout-products.lagda.md | 2 +- .../dependent-sequential-diagrams.lagda.md | 2 +- .../descent-circle.lagda.md | 2 +- .../flattening-lemma-pushouts.lagda.md | 6 +- ...ttening-lemma-sequential-colimits.lagda.md | 2 +- ...functoriality-sequential-colimits.lagda.md | 18 +-- .../joins-of-maps.lagda.md | 10 +- .../maps-of-prespectra.lagda.md | 2 +- .../morphisms-descent-data-circle.lagda.md | 2 +- .../morphisms-sequential-diagrams.lagda.md | 2 +- .../pullback-property-pushouts.lagda.md | 2 +- .../pushout-products.lagda.md | 4 +- .../pushouts.lagda.md | 10 +- .../smash-products-of-pointed-types.lagda.md | 2 +- .../suspensions-of-types.lagda.md | 4 +- .../tangent-spheres.lagda.md | 2 +- .../truncated-acyclic-maps.lagda.md | 4 +- .../universal-property-pushouts.lagda.md | 97 ++++++++------- ...rsal-property-sequential-colimits.lagda.md | 6 +- .../wedges-of-pointed-types.lagda.md | 2 +- ...-algebras-polynomial-endofunctors.lagda.md | 2 +- ...oalgebras-polynomial-endofunctors.lagda.md | 2 +- .../dependent-type-theories.lagda.md | 2 +- 135 files changed, 437 insertions(+), 444 deletions(-) diff --git a/src/category-theory/adjunctions-large-categories.lagda.md b/src/category-theory/adjunctions-large-categories.lagda.md index 4e1b492cb3..a8adbd3bcd 100644 --- a/src/category-theory/adjunctions-large-categories.lagda.md +++ b/src/category-theory/adjunctions-large-categories.lagda.md @@ -38,7 +38,7 @@ Two [functors](category-theory.functors-large-categories.md) `F : C → D` and | | g ∘ - ∘ F f | | G g ∘ - ∘ f | | - v v + ∨ ∨ hom (F X₂) Y₂ --------> hom X₂ (G Y₂) ϕ X₂ Y₂ ``` diff --git a/src/category-theory/adjunctions-large-precategories.lagda.md b/src/category-theory/adjunctions-large-precategories.lagda.md index d98a4ff347..ac473c743e 100644 --- a/src/category-theory/adjunctions-large-precategories.lagda.md +++ b/src/category-theory/adjunctions-large-precategories.lagda.md @@ -39,7 +39,7 @@ Let `C` and `D` be two | | g ∘ - ∘ F f | | G g ∘ - ∘ f | | - v v + ∨ ∨ hom (F X₂) Y₂ --------> hom X₂ (G Y₂) ϕ X₂ Y₂ ``` diff --git a/src/category-theory/commuting-squares-of-morphisms-in-large-precategories.lagda.md b/src/category-theory/commuting-squares-of-morphisms-in-large-precategories.lagda.md index 838a774e93..3e6f636e0b 100644 --- a/src/category-theory/commuting-squares-of-morphisms-in-large-precategories.lagda.md +++ b/src/category-theory/commuting-squares-of-morphisms-in-large-precategories.lagda.md @@ -23,7 +23,7 @@ A square of morphisms x ------> y | | | | - V V + ∨ ∨ z ------> w ``` diff --git a/src/category-theory/commuting-squares-of-morphisms-in-precategories.lagda.md b/src/category-theory/commuting-squares-of-morphisms-in-precategories.lagda.md index a0ffd99bb9..9fce14c311 100644 --- a/src/category-theory/commuting-squares-of-morphisms-in-precategories.lagda.md +++ b/src/category-theory/commuting-squares-of-morphisms-in-precategories.lagda.md @@ -23,7 +23,7 @@ A square of morphisms x ------> y | | | | - V V + ∨ ∨ z ------> w ``` diff --git a/src/category-theory/commuting-squares-of-morphisms-in-set-magmoids.lagda.md b/src/category-theory/commuting-squares-of-morphisms-in-set-magmoids.lagda.md index 3d5e86b8c9..9bcce6ed57 100644 --- a/src/category-theory/commuting-squares-of-morphisms-in-set-magmoids.lagda.md +++ b/src/category-theory/commuting-squares-of-morphisms-in-set-magmoids.lagda.md @@ -23,7 +23,7 @@ A square of morphisms x ------> y | | | | - V V + ∨ ∨ z ------> w ``` diff --git a/src/category-theory/gaunt-categories.lagda.md b/src/category-theory/gaunt-categories.lagda.md index 8235795ebe..20ed849c28 100644 --- a/src/category-theory/gaunt-categories.lagda.md +++ b/src/category-theory/gaunt-categories.lagda.md @@ -50,15 +50,15 @@ diagram relating the different notions of "category": Gaunt categories / \ / \ - v v + ∨ ∨ Categories Strict categories \ / \ / - v v + ∨ ∨ Preunivalent categories | | - v + ∨ Precategories ``` diff --git a/src/category-theory/restrictions-functors-cores-precategories.lagda.md b/src/category-theory/restrictions-functors-cores-precategories.lagda.md index ca34e5f283..1463265b07 100644 --- a/src/category-theory/restrictions-functors-cores-precategories.lagda.md +++ b/src/category-theory/restrictions-functors-cores-precategories.lagda.md @@ -42,7 +42,7 @@ that fit into a natural diagram | | | | | | - v v + ∨ ∨ C ------------> D. F ``` diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md index 3de1b68a34..f9be0f8f1b 100644 --- a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md @@ -94,7 +94,7 @@ commutes : | | ≅| |≅ | | - v v + ∨ ∨ BG ------> BH ΩBf ``` diff --git a/src/foundation-core/coherently-invertible-maps.lagda.md b/src/foundation-core/coherently-invertible-maps.lagda.md index dca846c82f..e33abe7e30 100644 --- a/src/foundation-core/coherently-invertible-maps.lagda.md +++ b/src/foundation-core/coherently-invertible-maps.lagda.md @@ -1176,7 +1176,7 @@ of coherently invertible maps asserts that for any \ / f\ /g \ / - V V + ∨ ∨ X, ``` diff --git a/src/foundation-core/commuting-prisms-of-maps.lagda.md b/src/foundation-core/commuting-prisms-of-maps.lagda.md index 54ae44233f..68a2637fd1 100644 --- a/src/foundation-core/commuting-prisms-of-maps.lagda.md +++ b/src/foundation-core/commuting-prisms-of-maps.lagda.md @@ -31,12 +31,12 @@ Consider an arrangment of maps composable into a diagram as follows: |\ |\ | \ h ⇗ | \ h' | \ f' | \ - | V | V + | ∨ | ∨ f | ⇐ B ------ | -> B' | / hB | ⇐ / | / g | / g' | / ⇗ | / - VV VV + ∨∨ ∨∨ C ---------> C' , hC ``` @@ -57,16 +57,16 @@ We may also arrange the maps into a more vertical shape, like so: ```text B - h ^| \ g + h ∧| \ g / | \ - / f | ⇑ V + / f | ⇑ ∨ A ---------> C | | hB | - | ⇗ V ⇗ | + | ⇗ ∨ ⇗ | hA | B' | hC - | h' ^ \ g' | + | h' ∧ \ g' | | / ⇑ \ | - V/ VV + ∨/ ∨∨ A' --------> C' . f' ``` diff --git a/src/foundation-core/commuting-squares-of-homotopies.lagda.md b/src/foundation-core/commuting-squares-of-homotopies.lagda.md index 27936d2400..a19b3297ec 100644 --- a/src/foundation-core/commuting-squares-of-homotopies.lagda.md +++ b/src/foundation-core/commuting-squares-of-homotopies.lagda.md @@ -26,7 +26,7 @@ A square of [homotopies](foundation-core.homotopies.md) f ------> g | | left | | right - v v + ∨ ∨ h ------> i bottom ``` diff --git a/src/foundation-core/commuting-squares-of-maps.lagda.md b/src/foundation-core/commuting-squares-of-maps.lagda.md index 92e9ba73f6..6cce4fb386 100644 --- a/src/foundation-core/commuting-squares-of-maps.lagda.md +++ b/src/foundation-core/commuting-squares-of-maps.lagda.md @@ -137,7 +137,7 @@ module _ A -----> X -----> U -----> K | | | | f | α g | β h | γ | i - V V V V + ∨ ∨ ∨ ∨ B -----> Y -----> V -----> L. α₁ β₁ γ₁ ``` diff --git a/src/foundation-core/commuting-triangles-of-maps.lagda.md b/src/foundation-core/commuting-triangles-of-maps.lagda.md index 610e4cd7c2..737a612750 100644 --- a/src/foundation-core/commuting-triangles-of-maps.lagda.md +++ b/src/foundation-core/commuting-triangles-of-maps.lagda.md @@ -27,7 +27,7 @@ A triangle of maps A ----> B \ / left \ / right - V V + ∨ ∨ X ``` @@ -85,7 +85,7 @@ then the triangle \ / g\ /f \ / - V V + ∨ ∨ X ``` @@ -117,7 +117,7 @@ then the triangle \ / h\ /r \ / - V V + ∨ ∨ B ``` diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index d164003b00..1f9549ab3a 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/src/foundation-core/equivalences.lagda.md @@ -311,7 +311,7 @@ The **3-for-2 property** of equivalences asserts that for any \ / f\ /g \ / - V V + ∨ ∨ X, ``` @@ -622,7 +622,7 @@ We will assume a commuting square A -----> C | | f | | g - V V + ∨ ∨ B -----> D i ``` diff --git a/src/foundation-core/operations-span-diagrams.lagda.md b/src/foundation-core/operations-span-diagrams.lagda.md index d80e62f1a5..78b68e8722 100644 --- a/src/foundation-core/operations-span-diagrams.lagda.md +++ b/src/foundation-core/operations-span-diagrams.lagda.md @@ -138,7 +138,7 @@ as indicated in the diagram A' <---- S' | | h₀ | | h₁ - V V + ∨ ∨ A <----- S -----> B. f g ``` @@ -210,7 +210,7 @@ as indicated in the diagram S' ----> B' | | h₀ | | h₁ - V V + ∨ ∨ A <----- S -----> B. f g ``` diff --git a/src/foundation-core/operations-spans.lagda.md b/src/foundation-core/operations-spans.lagda.md index 33d70af2cf..47e60de4d7 100644 --- a/src/foundation-core/operations-spans.lagda.md +++ b/src/foundation-core/operations-spans.lagda.md @@ -130,7 +130,7 @@ as indicated in the diagram A' <---- S' | | h₀ | | h₁ - V V + ∨ ∨ A <----- S -----> B. f g ``` @@ -178,7 +178,7 @@ as indicated in the diagram S' ----> B' | | h₀ | | h₁ - V V + ∨ ∨ A <----- S -----> B. f g ``` diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md index 7711113bb2..ca48ba96ed 100644 --- a/src/foundation-core/pullbacks.lagda.md +++ b/src/foundation-core/pullbacks.lagda.md @@ -340,7 +340,7 @@ Given a diagram as follows where the right-hand square is a pullback ∙ -------> ∙ -------> ∙ | | ⌟ | | | | - v v v + ∨ ∨ ∨ ∙ -------> ∙ -------> ∙, ``` @@ -431,11 +431,11 @@ Given a diagram as follows where the lower square is a pullback ∙ -------> ∙ | | | | - v v + ∨ ∨ ∙ -------> ∙ | ⌟ | | | - v v + ∨ ∨ ∙ -------> ∙, ``` @@ -672,7 +672,7 @@ Given a pullback square C -------> B | ⌟ | g'| | g - v v + ∨ ∨ A -------> X f ``` @@ -684,7 +684,7 @@ square C ---------> X | ⌟ | (f' , g') | | - v v + ∨ ∨ A × B -----> X × X, f × g ``` diff --git a/src/foundation-core/retractions.lagda.md b/src/foundation-core/retractions.lagda.md index 7ba3ebc1f4..56c9238c34 100644 --- a/src/foundation-core/retractions.lagda.md +++ b/src/foundation-core/retractions.lagda.md @@ -162,7 +162,7 @@ In a commuting triangle of the form \ / f\ /g \ / - V V + ∨ ∨ X, ``` @@ -206,7 +206,7 @@ In a commuting triangle of the form \ / f\ /g \ / - V V + ∨ ∨ X, ``` diff --git a/src/foundation-core/sections.lagda.md b/src/foundation-core/sections.lagda.md index a661fbfc70..1a1948ba65 100644 --- a/src/foundation-core/sections.lagda.md +++ b/src/foundation-core/sections.lagda.md @@ -115,7 +115,7 @@ In a commuting triangle of the form \ / f\ /g \ / - V V + ∨ ∨ X, ``` @@ -188,7 +188,7 @@ In a commuting triangle of the form \ / f\ /g \ / - V V + ∨ ∨ X, ``` diff --git a/src/foundation/action-on-equivalences-functions-out-of-subuniverses.lagda.md b/src/foundation/action-on-equivalences-functions-out-of-subuniverses.lagda.md index 7aaf843921..77d4813bf5 100644 --- a/src/foundation/action-on-equivalences-functions-out-of-subuniverses.lagda.md +++ b/src/foundation/action-on-equivalences-functions-out-of-subuniverses.lagda.md @@ -42,7 +42,7 @@ which is uniquely determined by the (X = Y) ---------------> (f X = f Y) | | equiv-eq | | id - V V + ∨ ∨ (X ≃ Y) ---------------> (f X = f Y) action-equiv f ``` diff --git a/src/foundation/action-on-equivalences-type-families-over-subuniverses.lagda.md b/src/foundation/action-on-equivalences-type-families-over-subuniverses.lagda.md index 867e44a659..9285de702a 100644 --- a/src/foundation/action-on-equivalences-type-families-over-subuniverses.lagda.md +++ b/src/foundation/action-on-equivalences-type-families-over-subuniverses.lagda.md @@ -72,7 +72,7 @@ We claim that the square (X ＝ Y) --------> (B X ＝ B Y) | | equiv-eq | | equiv-eq - V V + ∨ ∨ (X ≃ Y) ---------> (B X ≃ B Y). B ``` diff --git a/src/foundation/action-on-equivalences-type-families.lagda.md b/src/foundation/action-on-equivalences-type-families.lagda.md index caf1cd9269..909f4c4011 100644 --- a/src/foundation/action-on-equivalences-type-families.lagda.md +++ b/src/foundation/action-on-equivalences-type-families.lagda.md @@ -45,7 +45,7 @@ determined by the identification `B id-equiv ＝ id-equiv`, and fits in a (X ＝ Y) --------> (B X ＝ B Y) | | equiv-eq | | equiv-eq - V V + ∨ ∨ (X ≃ Y) ---------> (B X ≃ B Y). B ``` @@ -98,7 +98,7 @@ We claim that the square (X ＝ Y) --------> (B X ＝ B Y) | | equiv-eq | | equiv-eq - V V + ∨ ∨ (X ≃ Y) ---------> (B X ≃ B Y). B ``` diff --git a/src/foundation/action-on-identifications-binary-functions.lagda.md b/src/foundation/action-on-identifications-binary-functions.lagda.md index d9d2b1d339..626856cd0b 100644 --- a/src/foundation/action-on-identifications-binary-functions.lagda.md +++ b/src/foundation/action-on-identifications-binary-functions.lagda.md @@ -126,7 +126,7 @@ uncurried [commuting square](foundation-core.commuting-squares-of-maps.md) | | 1 × Δ | | ap | | - v v + ∨ ∨ (A × A → B) × Path A × Path A ----------> Path B. ap-binary ``` diff --git a/src/foundation/cartesian-morphisms-arrows.lagda.md b/src/foundation/cartesian-morphisms-arrows.lagda.md index 4c74b2d08a..8750d63496 100644 --- a/src/foundation/cartesian-morphisms-arrows.lagda.md +++ b/src/foundation/cartesian-morphisms-arrows.lagda.md @@ -53,7 +53,7 @@ if the [commuting square](foundation-core.commuting-squares-of-maps.md) A -----> X | | f | h | g - V V + ∨ ∨ B -----> Y j ``` @@ -184,7 +184,7 @@ of a cartesian morphism of arrows A -----> X | ⌟ | f | | g - V V + ∨ ∨ B -----> Y j ``` @@ -196,7 +196,7 @@ is the cartesian morphism of arrows A -----> B | ⌟ | i | | j - V V + ∨ ∨ X -----> Y. g ``` diff --git a/src/foundation/commuting-prisms-of-maps.lagda.md b/src/foundation/commuting-prisms-of-maps.lagda.md index c8567bf6b6..1abe1edc03 100644 --- a/src/foundation/commuting-prisms-of-maps.lagda.md +++ b/src/foundation/commuting-prisms-of-maps.lagda.md @@ -198,16 +198,16 @@ The basic set-up is that, given a commuting prism of maps ```text B - h ^| \ g + h ∧| \ g / | \ - / f | ⇑ v + / f | ⇑ ∨ A ---------> C | | hB | - | ⇗ v ⇗ | + | ⇗ ∨ ⇗ | hA | B' | hC - | h' ^ \ g' | + | h' ∧ \ g' | | / ⇑ \ | - v/ vv + ∨/ ∨∨ A' --------> C' f' ``` @@ -217,17 +217,17 @@ we have commuting prisms of ```text (B' → S) - (- ∘ g') ^ | \ (- ∘ h') + (- ∘ g') ∧ | \ (- ∘ h') / | \ - / (- ∘ f')| ⇑ v + / (- ∘ f')| ⇑ ∨ (C' → S) ---------------> (A' → S) | | | | | (- ∘ hB) | - | ⇙ v ⇙ | + | ⇙ ∨ ⇙ | (- ∘ hC) | (B → S) | (- ∘ hA) - | (- ∘ g) ^ \ (- ∘ h) | + | (- ∘ g) ∧ \ (- ∘ h) | | / ⇑ \ | - v / v v + ∨ / ∨ ∨ (C → S) ----------------> (A → S). (- ∘ f) ``` @@ -424,16 +424,16 @@ Given a commuting prism of maps ```text B - h ^| \ g + h ∧| \ g / | \ - / f | ⇑ v + / f | ⇑ ∨ A ---------> C | | hB | - | ⇗ v ⇗ | + | ⇗ ∨ ⇗ | hA | B' | hC - | h' ^ \ g' | + | h' ∧ \ g' | | / ⇑ \ | - v/ vv + ∨/ ∨∨ A' --------> C' f' ``` @@ -443,17 +443,17 @@ we have commuting prisms of ```text (S → B) - (h ∘ -) ^ | \ (g ∘ -) + (h ∘ -) ∧ | \ (g ∘ -) / | \ - / (f ∘ -)| ⇑ v + / (f ∘ -)| ⇑ ∨ (S → A) ----------------> (S → C) | | | | | (hB ∘ -) | - | ⇗ v ⇗ | + | ⇗ ∨ ⇗ | (hA ∘ -) | (S → B') | (hC ∘ -) - | (h' ∘ -) ^ \ (g' ∘ -) | + | (h' ∘ -) ∧ \ (g' ∘ -) | | / ⇑ \ | - v / v v + ∨ / ∨ ∨ (S → A') ---------------> (S → C'). (f' ∘ -) ``` diff --git a/src/foundation/commuting-squares-of-maps.lagda.md b/src/foundation/commuting-squares-of-maps.lagda.md index cb2b53f6f1..12fbe4c18f 100644 --- a/src/foundation/commuting-squares-of-maps.lagda.md +++ b/src/foundation/commuting-squares-of-maps.lagda.md @@ -425,11 +425,11 @@ As a corollary, whenever we have two coherence squares touching at a vertex: A -----> B | | | H ⇗ | - V V + ∨ ∨ C -----> D -----> X | | | K ⇗ | - V V + ∨ ∨ Y -----> Z , ``` @@ -465,11 +465,11 @@ Given a square of commuting squares, like so: A -----> B -----> C | | | | ⇗ | ⇗ | - V V V + ∨ ∨ ∨ X -----> Y -----> Z | | | | ⇗ | ⇗ | - V V V + ∨ ∨ ∨ M -----> N -----> O , ``` @@ -603,32 +603,27 @@ homotopy that is homotopic to first transposing the squares and then composing them. ```text - tl tr tr ∘ tl - A -----> B -----> C A --------> C - | | | | | -l | m| | r ↦ l| r| - | H | K | | H | K | - ∨ ∨ ∨ ∨ ∨ - X -----> Y -----> Z X --------> Z - bl br br ∘ bl - - - - - | | - ∨ ∨ - - -∘r - W^Z ------> W^C - | | --∘br | W^K | -∘tr W^(H | K) - | | - ∨ -∘m ∨ ~ - W^Y ------> W^B |-> - | | W^K --∘bl | W^H | -∘tl --- - | | W^H - ∨ ∨ - W^X ------> W^A - -∘l + tl tr tr ∘ tl + A -----> B -----> C A --------> C + | | | | | + l | H m | K | r ↦ l | H | K | r + ∨ ∨ ∨ ∨ ∨ + X -----> Y -----> Z X --------> Z + bl br br ∘ bl + + ↧ ↧ + + - ∘ r + W^Z ------> W^C + | | + - ∘ br | W^K | - ∘ tr W^(H | K) + ∨ - ∘ m ∨ ~ + W^Y ------> W^B ↦ + | | W^K + - ∘ bl | W^H | - ∘ tl --- + ∨ ∨ W^H + W^X ------> W^A + - ∘ l ``` ```agda @@ -821,7 +816,7 @@ Taking a square of the form X -----> A -----> B | | left | H | right - v v + ∨ ∨ C -----> D bottom ``` @@ -832,7 +827,7 @@ and transposing it by precomposition results in the square W^D -----> W^B | | | W^H | - v v -∘f + ∨ ∨ - ∘ f W^C -----> W^A -----> W^X ``` diff --git a/src/foundation/commuting-tetrahedra-of-maps.lagda.md b/src/foundation/commuting-tetrahedra-of-maps.lagda.md index fe188d92cf..6adcbb657d 100644 --- a/src/foundation/commuting-tetrahedra-of-maps.lagda.md +++ b/src/foundation/commuting-tetrahedra-of-maps.lagda.md @@ -23,11 +23,11 @@ is a commuting diagram of the form ```text A ----------> B - | \ ^ | + | \ ∧ | | \ / | | / | | / \ | - V / v V + ∨ / ∨ ∨ X ----------> Y. ``` diff --git a/src/foundation/commuting-triangles-of-maps.lagda.md b/src/foundation/commuting-triangles-of-maps.lagda.md index 742618605e..55d8859dee 100644 --- a/src/foundation/commuting-triangles-of-maps.lagda.md +++ b/src/foundation/commuting-triangles-of-maps.lagda.md @@ -34,7 +34,7 @@ A triangle of maps A ----> B \ / \ / - V V + ∨ ∨ X ``` @@ -86,7 +86,7 @@ Given a commuting triangle of maps A ----> B \ ⇗ / h \ / g - V V + ∨ ∨ X ``` @@ -98,7 +98,7 @@ there is an induced commuting triangle of (X → S) ----> (B → S) \ ⇗ / (- ∘ h) \ / (- ∘ f) - V V + ∨ ∨ (A → S). ``` @@ -138,7 +138,7 @@ Given a commuting triangle of maps A ----> B \ ⇗ / h \ / g - V V + ∨ ∨ X ``` @@ -150,7 +150,7 @@ there is an induced commuting triangle of (S → A) ----> (S → B) \ ⇗ / (h ∘ -) \ / (g ∘ -) - V V + ∨ ∨ (S → X). ``` diff --git a/src/foundation/composition-algebra.lagda.md b/src/foundation/composition-algebra.lagda.md index 515ca2b985..e98e9e0260 100644 --- a/src/foundation/composition-algebra.lagda.md +++ b/src/foundation/composition-algebra.lagda.md @@ -253,7 +253,7 @@ homotopies precomp f Y ·l htpy-postcomp B G htpy-postcomp A G ·r precomp f' X | | | | - v v + ∨ ∨ (g' ∘ - ∘ f) --------------------------------> (g' ∘ - ∘ f'). htpy-precomp F Y ·r postcomp B g' ``` diff --git a/src/foundation/cones-over-inverse-sequential-diagrams.lagda.md b/src/foundation/cones-over-inverse-sequential-diagrams.lagda.md index ba3b8087f4..a062c7b9d4 100644 --- a/src/foundation/cones-over-inverse-sequential-diagrams.lagda.md +++ b/src/foundation/cones-over-inverse-sequential-diagrams.lagda.md @@ -40,7 +40,7 @@ from `X` into the sequence of types of `A` such that the triangles X / \ / \ - v v + ∨ ∨ Aₙ₊₁ -> Aₙ ``` diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md index 7d4c7b1739..857e423d5b 100644 --- a/src/foundation/copartial-elements.lagda.md +++ b/src/foundation/copartial-elements.lagda.md @@ -45,14 +45,14 @@ following [pullback](foundation.pullbacks.md) squares A -----> Σ (Q : Prop), A * Q 1 -----> Σ (P : Prop), (P → A) | ⌟ | | ⌟ | | | | | - V V V V + ∨ ∨ ∨ ∨ 1 -----------> Prop 1 -----------> Prop F F 1 -----> Σ (Q : Prop), A * Q A -----> Σ (P : Prop), (P → A) | ⌟ | | ⌟ | | | | | - V V V V + ∨ ∨ ∨ ∨ 1 -----------> Prop 1 -----------> Prop T T ``` @@ -71,7 +71,7 @@ the [pushout-product](synthetic-homotopy-theory.pushout-products.md) A 1 | | ! | □ | T - V V + ∨ ∨ 1 Prop ``` @@ -85,7 +85,7 @@ copartial elements induce copartial elements. Indeed, note that 1 1 Σ (P Q : Prop), P * Q ---------------------> 1 | | | | T | □ | T = T □ T | | - V V V V + ∨ ∨ ∨ ∨ Prop Prop Prop² ------------------------------> Prop P Q ↦ P * Q ``` diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md index 0800b92252..6b5c611c47 100644 --- a/src/foundation/copartial-functions.lagda.md +++ b/src/foundation/copartial-functions.lagda.md @@ -41,7 +41,7 @@ described as a [morphism of arrows](foundation.morphisms-arrows.md) A B 1 | | | id | ⇒ | □ | T - V V V + ∨ ∨ ∨ A 1 Prop ``` @@ -56,7 +56,7 @@ functions can be defined by copartial-element (copartial-element C) ∧ | map-copartial-element g / | join-copartial-element - / V + / ∨ A ----> copartial-element B copartial-element C f ``` diff --git a/src/foundation/coslice.lagda.md b/src/foundation/coslice.lagda.md index 6533ee227b..20e4829866 100644 --- a/src/foundation/coslice.lagda.md +++ b/src/foundation/coslice.lagda.md @@ -30,7 +30,7 @@ Given a span of maps X / \ f / \ g - v v + ∨ ∨ A B, ``` @@ -41,7 +41,7 @@ map `h : A → B` together with a coherence triangle `(h ∘ f) ~ g`: X / \ f / \ g - v v + ∨ ∨ A ----> B. h ``` diff --git a/src/foundation/dependent-inverse-sequential-diagrams.lagda.md b/src/foundation/dependent-inverse-sequential-diagrams.lagda.md index 25e5bc7fd8..962e766c42 100644 --- a/src/foundation/dependent-inverse-sequential-diagrams.lagda.md +++ b/src/foundation/dependent-inverse-sequential-diagrams.lagda.md @@ -96,7 +96,7 @@ we mean that the diagrams ```text gₙ Bₙ₊₁ ---> Bₙ - ^ ^ + ∧ ∧ hₙ₊₁| | hₙ | | Aₙ₊₁ ---> Aₙ diff --git a/src/foundation/dependent-sums-pullbacks.lagda.md b/src/foundation/dependent-sums-pullbacks.lagda.md index a8533677f9..406b3de694 100644 --- a/src/foundation/dependent-sums-pullbacks.lagda.md +++ b/src/foundation/dependent-sums-pullbacks.lagda.md @@ -41,7 +41,7 @@ Squares of the form | | pr1 | | pr1 | | - V V + ∨ ∨ A -----------------------> B f ``` @@ -105,7 +105,7 @@ Given a map `f : A → B` with a family of maps over it Σ A P ----------> Σ B Q | | | | - v v + ∨ ∨ A -------------> B f ``` diff --git a/src/foundation/descent-equivalences.lagda.md b/src/foundation/descent-equivalences.lagda.md index 108a879578..2a2da46991 100644 --- a/src/foundation/descent-equivalences.lagda.md +++ b/src/foundation/descent-equivalences.lagda.md @@ -29,7 +29,7 @@ property. It asserts that in a commuting diagram of the form A -----> B -----> C | | | f| g| |h - V V V + ∨ ∨ ∨ X -----> Y -----> Z, i j ``` diff --git a/src/foundation/diagonals-of-morphisms-arrows.lagda.md b/src/foundation/diagonals-of-morphisms-arrows.lagda.md index 86887ec613..01f3f27480 100644 --- a/src/foundation/diagonals-of-morphisms-arrows.lagda.md +++ b/src/foundation/diagonals-of-morphisms-arrows.lagda.md @@ -22,7 +22,7 @@ The {{#concept "diagonal" Disambiguation="morphism of arrows"}} of a A -----> X | | f | | g - V V + ∨ ∨ B -----> Y j ``` @@ -35,7 +35,7 @@ maps `i` and `j`, which fit in a naturality square A -----> A ×_X A | | f | | functoriality Δ g - V V + ∨ ∨ B -----> B ×_Y B. Δ j ``` diff --git a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md index 4cb8a7e747..e5ff5b16a5 100644 --- a/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md +++ b/src/foundation/epimorphisms-with-respect-to-truncated-types.lagda.md @@ -265,9 +265,9 @@ We consider the commutative diagram for any `k`-type `X`: ```text horizontal-map-cocone (B → X) <---------------------------- cocone f f X - | ≃ ^ + | ≃ ∧ id | ≃ ≃ | (universal property) - v | + ∨ | (B → X) ------------------------> (pushout f f → X) precomp (codiagonal f) ``` diff --git a/src/foundation/epimorphisms.lagda.md b/src/foundation/epimorphisms.lagda.md index 2d8775edd7..b7c5bb9ab4 100644 --- a/src/foundation/epimorphisms.lagda.md +++ b/src/foundation/epimorphisms.lagda.md @@ -71,7 +71,7 @@ If the map `f : A → B` is epi, then the commutative square A -----> B | | f | | id - V ⌜ V + ∨ ⌜ ∨ B -----> B id ``` diff --git a/src/foundation/equivalences-arrows.lagda.md b/src/foundation/equivalences-arrows.lagda.md index 1f40d8cb42..ae942fce9a 100644 --- a/src/foundation/equivalences-arrows.lagda.md +++ b/src/foundation/equivalences-arrows.lagda.md @@ -32,7 +32,7 @@ function `g : X → Y` is a [morphism of arrows](foundation.morphisms-arrows.md) A -----> X | ≃ | f | | g - V ≃ V + ∨ ≃ ∨ B -----> Y j ``` diff --git a/src/foundation/equivalences-cospans.lagda.md b/src/foundation/equivalences-cospans.lagda.md index aea864d493..a44b7e3b11 100644 --- a/src/foundation/equivalences-cospans.lagda.md +++ b/src/foundation/equivalences-cospans.lagda.md @@ -36,7 +36,7 @@ An {{#concept "equivalence of cospans" Agda=equiv-cospan}} from X ----> Y X ----> Y \ / \ / f \ / h g \ / k - V V V V + ∨ ∨ ∨ ∨ A B ``` diff --git a/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md b/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md index b6abd40a7e..c7439c75b1 100644 --- a/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md +++ b/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md @@ -38,7 +38,7 @@ An ⋯ ----> Aₙ₊₁ ----> Aₙ ----> ⋯ ----> A₁ ----> A₀ | | | | | ⋯ | | ⋯ | | - v v v v v + ∨ ∨ ∨ ∨ ∨ ⋯ ----> Bₙ₊₁ ----> Bₙ ----> ⋯ ----> B₁ ----> B₀. ``` diff --git a/src/foundation/equivalences-span-diagrams-families-of-types.lagda.md b/src/foundation/equivalences-span-diagrams-families-of-types.lagda.md index f7f3f6fd3c..05c24bbdad 100644 --- a/src/foundation/equivalences-span-diagrams-families-of-types.lagda.md +++ b/src/foundation/equivalences-span-diagrams-families-of-types.lagda.md @@ -35,7 +35,7 @@ types indexed by a type `I` to a span `(B , t)` indexed by `I` consists of a S -----> T | | fᵢ | | gᵢ - V V + ∨ ∨ Aᵢ ----> Bᵢ h ``` diff --git a/src/foundation/equivalences-span-diagrams.lagda.md b/src/foundation/equivalences-span-diagrams.lagda.md index 05e26311db..92238d6cff 100644 --- a/src/foundation/equivalences-span-diagrams.lagda.md +++ b/src/foundation/equivalences-span-diagrams.lagda.md @@ -44,7 +44,7 @@ with two [homotopies](foundation-core.homotopies.md) witnessing that the diagram A <----- S -----> B | | | u | | w | v - V V V + ∨ ∨ ∨ C <----- T -----> D h k ``` diff --git a/src/foundation/equivalences-spans-families-of-types.lagda.md b/src/foundation/equivalences-spans-families-of-types.lagda.md index 0d6c5ebc6c..f76bbf5f10 100644 --- a/src/foundation/equivalences-spans-families-of-types.lagda.md +++ b/src/foundation/equivalences-spans-families-of-types.lagda.md @@ -40,7 +40,7 @@ span `t` on `A` consists of an [equivalence](foundation-core.equivalences.md) S ----> T \ / \ / - V V + ∨ ∨ Aᵢ ``` diff --git a/src/foundation/fibered-equivalences.lagda.md b/src/foundation/fibered-equivalences.lagda.md index 2b90a61064..3d899df149 100644 --- a/src/foundation/fibered-equivalences.lagda.md +++ b/src/foundation/fibered-equivalences.lagda.md @@ -38,7 +38,7 @@ A fibered equivalence is a fibered map | | f| |g | | - V V + ∨ ∨ X -------> Y i ``` diff --git a/src/foundation/fibered-involutions.lagda.md b/src/foundation/fibered-involutions.lagda.md index 7ac675eebc..e00fab4ca6 100644 --- a/src/foundation/fibered-involutions.lagda.md +++ b/src/foundation/fibered-involutions.lagda.md @@ -30,7 +30,7 @@ A fibered involution is a fibered map | | f| |g | | - V V + ∨ ∨ X -------> X i ``` diff --git a/src/foundation/fibered-maps.lagda.md b/src/foundation/fibered-maps.lagda.md index 0cd36bbb43..686a7b601f 100644 --- a/src/foundation/fibered-maps.lagda.md +++ b/src/foundation/fibered-maps.lagda.md @@ -42,13 +42,12 @@ open import foundation-core.truncation-levels Consider a diagram of the form ```text - A B - | | - f| |g - | | - V V - X ------> Y - i + A B + | | + f | | g + ∨ ∨ + X ------> Y + i ``` A **fibered map** from `f` to `g` over `i` is a map `h : A → B` such that the @@ -433,13 +432,13 @@ module _ ### If the top left corner is empty, the type of fibered maps is equivalent to maps `X → Y` ```text - ! -empty ---> B - | | - !| |g - V V - X -----> Y - i + ! + empty ---> B + | | + ! | | g + ∨ ∨ + X -----> Y + i ``` ```agda @@ -476,12 +475,12 @@ module _ ### If the bottom right corner is contractible, the type of fibered maps is equivalent to maps `A → B` ```text - A -----> B - | | - f| |! - V V - X ---> unit - ! + A -----> B + | | + f | | ! + ∨ ∨ + X ---> unit + ! ``` ```agda diff --git a/src/foundation/functoriality-cartesian-product-types.lagda.md b/src/foundation/functoriality-cartesian-product-types.lagda.md index ab46e822fa..6b853ac770 100644 --- a/src/foundation/functoriality-cartesian-product-types.lagda.md +++ b/src/foundation/functoriality-cartesian-product-types.lagda.md @@ -44,7 +44,7 @@ the sense that for any two maps `f : A → B` and `g : C → D` the diagram | \ | 1×g | \f×g | 1×g | \ | - V > V + ∨ ∨ ∨ A × D ---> B × D f×1 ``` diff --git a/src/foundation/functoriality-dependent-pair-types.lagda.md b/src/foundation/functoriality-dependent-pair-types.lagda.md index a35a9726ef..86a2912fa7 100644 --- a/src/foundation/functoriality-dependent-pair-types.lagda.md +++ b/src/foundation/functoriality-dependent-pair-types.lagda.md @@ -49,7 +49,7 @@ over `H`, expressed as C a -----> D (f a) \ / g' a \ / tr D (H a) - V V + ∨ ∨ D (f' a) , ``` diff --git a/src/foundation/functoriality-fibers-of-maps.lagda.md b/src/foundation/functoriality-fibers-of-maps.lagda.md index 6e821ccd82..8566e6620f 100644 --- a/src/foundation/functoriality-fibers-of-maps.lagda.md +++ b/src/foundation/functoriality-fibers-of-maps.lagda.md @@ -38,7 +38,7 @@ to `g` A -----> X | | f | | g - v v + ∨ ∨ B -----> Y j ``` @@ -51,7 +51,7 @@ induces a morphism of arrows between the fiber f b -----> fiber g (j b) | | | | - V V + ∨ ∨ A ---------------> X. ``` @@ -254,7 +254,7 @@ Given two morphisms of arrows | | f | α β | g | | - V α₁ V + ∨ α₁ ∨ B ------> Y ------> β₁ @@ -268,13 +268,13 @@ diagram of the form ∧ | \ / | \ (x , q) ↦ (x , q ∙ γ₁ b) / | \ - / | V + / | ∨ fiber f b --------> fiber g (β₁ b) | | / | | / | | / | | / - V V V + ∨ ∨ ∨ A -------> X ``` @@ -338,7 +338,7 @@ Now it remains to fill a coherence for the square of homotopies | | coh (tr ∘ α b) | | coh-hom-arrow-fiber f g β b ≐ refl-htpy | | ≐ refl-htpy - V V + ∨ ∨ · ---------> · i ·r H ``` diff --git a/src/foundation/homotopies-morphisms-arrows.lagda.md b/src/foundation/homotopies-morphisms-arrows.lagda.md index a49b039cfd..4eb4eeead5 100644 --- a/src/foundation/homotopies-morphisms-arrows.lagda.md +++ b/src/foundation/homotopies-morphisms-arrows.lagda.md @@ -59,7 +59,7 @@ and `J : j ~ j'` and a homotopy `K` witnessing that the (j ∘ f) --------> (j' ∘ f) | | H | | H' - V V + ∨ ∨ (g ∘ i) --------> (g ∘ i') g ·l I ``` @@ -467,7 +467,7 @@ Consider a commuting diagram of the form A -----> X -----> U -----> K | | | | f | α g | β h | γ | i - V V V V + ∨ ∨ ∨ ∨ B -----> Y -----> V -----> L α₁ β₁ γ₁ ``` diff --git a/src/foundation/morphisms-arrows.lagda.md b/src/foundation/morphisms-arrows.lagda.md index 83dae01537..7b85cd1c07 100644 --- a/src/foundation/morphisms-arrows.lagda.md +++ b/src/foundation/morphisms-arrows.lagda.md @@ -38,7 +38,7 @@ the square A -----> X | | f | | g - V V + ∨ ∨ B -----> Y j ``` @@ -85,7 +85,7 @@ The identity morphism of arrows is defined as A -----> A | | f | | f - V V + ∨ ∨ B -----> B id ``` @@ -112,7 +112,7 @@ Consider a commuting diagram of the form A -----> X -----> U | | | f | α g | β | h - V V V + ∨ ∨ ∨ B -----> Y -----> V. α₁ β₁ ``` @@ -126,7 +126,7 @@ maps. The {{#concept "composition" Disambiguation="morphism of arrows"}} of A ----------> U | | f | α □ β | h - V V + ∨ ∨ B ----------> V. β₁ ∘ α₁ ``` @@ -185,7 +185,7 @@ morphism of arrows A -----> X | | f | | g - V V + ∨ ∨ B -----> Y j ``` @@ -197,7 +197,7 @@ is the morphism of arrows A -----> B | | i | | j - V V + ∨ ∨ X -----> Y. g ``` diff --git a/src/foundation/morphisms-cospan-diagrams.lagda.md b/src/foundation/morphisms-cospan-diagrams.lagda.md index f5a8a9339a..d576b35813 100644 --- a/src/foundation/morphisms-cospan-diagrams.lagda.md +++ b/src/foundation/morphisms-cospan-diagrams.lagda.md @@ -26,7 +26,7 @@ commuting diagram of the form A -----> X <----- B | | | | | | - V V V + ∨ ∨ ∨ A' ----> X' <---- B'. ``` diff --git a/src/foundation/morphisms-cospans.lagda.md b/src/foundation/morphisms-cospans.lagda.md index f90a01e478..b3cdf33eb6 100644 --- a/src/foundation/morphisms-cospans.lagda.md +++ b/src/foundation/morphisms-cospans.lagda.md @@ -30,7 +30,7 @@ witnessing that the two triangles X ----> Y X ----> Y \ / \ / f \ / h g \ / k - V V V V + ∨ ∨ ∨ ∨ A B ``` diff --git a/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md b/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md index 0f260a9039..794b939f5a 100644 --- a/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md +++ b/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md @@ -39,7 +39,7 @@ the form ⋯ ----> Aₙ₊₁ ----> Aₙ ----> ⋯ ----> A₁ ----> A₀ | | | | | ⋯ | | ⋯ | | - v v v v v + ∨ ∨ ∨ ∨ ∨ ⋯ ----> Bₙ₊₁ ----> Bₙ ----> ⋯ ----> B₁ ----> B₀. ``` diff --git a/src/foundation/morphisms-span-diagrams.lagda.md b/src/foundation/morphisms-span-diagrams.lagda.md index 7b5ba197e5..604d0c6d6e 100644 --- a/src/foundation/morphisms-span-diagrams.lagda.md +++ b/src/foundation/morphisms-span-diagrams.lagda.md @@ -32,7 +32,7 @@ A {{#concept "morphism of span diagrams" Agda=hom-span-diagram}} from a A <----- S -----> B | | | u | | w | v - V V V + ∨ ∨ ∨ C <----- T -----> D h k ``` @@ -52,7 +52,7 @@ squares of morphisms of spans are oriented in the following way: S ----------------------> T | | left-map-span s | | left-map-span t - V V + ∨ ∨ A ----------------------> C map-domain-hom-span ``` @@ -68,7 +68,7 @@ squares of morphisms of spans are oriented in the following way: S ----------------------> T | | right-map-span s | | right-map-span t - V V + ∨ ∨ B ----------------------> D map-codomain-hom-span ``` diff --git a/src/foundation/morphisms-spans.lagda.md b/src/foundation/morphisms-spans.lagda.md index 700e1f771b..0632d4ed00 100644 --- a/src/foundation/morphisms-spans.lagda.md +++ b/src/foundation/morphisms-spans.lagda.md @@ -30,11 +30,11 @@ consists of a map `w : S → T` [equipped](foundation.structure.md) with two S / | \ f / | \ h - V | V + ∨ | ∨ A |w B ∧ | ∧ h \ | / k - \ V / + \ ∨ / T ``` diff --git a/src/foundation/morphisms-twisted-arrows.lagda.md b/src/foundation/morphisms-twisted-arrows.lagda.md index 0a7a0dd0fb..a5d63757b3 100644 --- a/src/foundation/morphisms-twisted-arrows.lagda.md +++ b/src/foundation/morphisms-twisted-arrows.lagda.md @@ -31,7 +31,7 @@ A **morphism of twisted arrows** from `f : A → B` to `g : X → Y` is a triple A <----- X | | f | | g - V V + ∨ ∨ B -----> Y j ``` diff --git a/src/foundation/operations-span-diagrams.lagda.md b/src/foundation/operations-span-diagrams.lagda.md index f162990c4a..9337e9f12a 100644 --- a/src/foundation/operations-span-diagrams.lagda.md +++ b/src/foundation/operations-span-diagrams.lagda.md @@ -46,7 +46,7 @@ and an [equivalence of arrows](foundation.equivalences-arrows.md) A' <---- S' | | h₀ | ≃ ≃ | h₁ - V V + ∨ ∨ A <----- S -----> B. f g ``` @@ -115,7 +115,7 @@ and a [equivalence of arrows](foundation.equivalences-arrows.md) S' ----> B' | | h₀ | ≃ ≃ | h₁ - V V + ∨ ∨ A <----- S -----> B. f g ``` diff --git a/src/foundation/operations-spans.lagda.md b/src/foundation/operations-spans.lagda.md index 2963f46eae..9037d78969 100644 --- a/src/foundation/operations-spans.lagda.md +++ b/src/foundation/operations-spans.lagda.md @@ -46,7 +46,7 @@ and an [equivalence of arrows](foundation.equivalences-arrows.md) A' <---- S' | | h₀ | ≃ ≃ | h₁ - V V + ∨ ∨ A <----- S -----> B. f g ``` @@ -101,7 +101,7 @@ as indicated in the diagram S' ----> B' | | h₀ | ≃ ≃ | h₁ - V V + ∨ ∨ A <----- S -----> B. f g ``` diff --git a/src/foundation/partial-elements.lagda.md b/src/foundation/partial-elements.lagda.md index ca67ef0cb8..55625c0785 100644 --- a/src/foundation/partial-elements.lagda.md +++ b/src/foundation/partial-elements.lagda.md @@ -38,7 +38,7 @@ codomain of the 1 ∅ ∅ | | | T | ∘ | = | - V V V + ∨ ∨ ∨ Prop X P T X ``` diff --git a/src/foundation/partial-functions.lagda.md b/src/foundation/partial-functions.lagda.md index d11bd0d4ac..9b23765ad7 100644 --- a/src/foundation/partial-functions.lagda.md +++ b/src/foundation/partial-functions.lagda.md @@ -38,7 +38,7 @@ Partial functions can be described ∅ 1 ∅ | | | | ⇒ | ∘ | - V V V + ∨ ∨ ∨ A Prop B ``` diff --git a/src/foundation/postcomposition-dependent-functions.lagda.md b/src/foundation/postcomposition-dependent-functions.lagda.md index fdf640a652..af9cd90fde 100644 --- a/src/foundation/postcomposition-dependent-functions.lagda.md +++ b/src/foundation/postcomposition-dependent-functions.lagda.md @@ -58,7 +58,7 @@ Consider a map `f : {x : A} → B x → C x` and two functions (g ＝ h) -------------------------> (f ∘ g ＝ f ∘ h) | | htpy-eq | | htpy-eq - V V + ∨ ∨ (g ~ h) --------------------------> (f ∘ g ~ f ∘ h). f ·l_ ``` @@ -69,7 +69,7 @@ commuting square ```text ap (postcomp-Π A f) (g ＝ h) -------------------------> (f ∘ g ＝ f ∘ h) - ^ ^ + ∧ ∧ eq-htpy | | eq-htpy | | (g ~ h) --------------------------> (f ∘ g ~ f ∘ h). diff --git a/src/foundation/precomposition-dependent-functions.lagda.md b/src/foundation/precomposition-dependent-functions.lagda.md index a4ef43be00..0e1b1294b1 100644 --- a/src/foundation/precomposition-dependent-functions.lagda.md +++ b/src/foundation/precomposition-dependent-functions.lagda.md @@ -51,7 +51,7 @@ Then the square (g ＝ h) ---------------------------> (g ∘ f ＝ h ∘ f) | | htpy-eq | | htpy-eq - V V + ∨ ∨ (g ~ h) ----------------------------> (g ∘ f ~ h ∘ f) precomp-Π f (eq-value g h) ``` diff --git a/src/foundation/precomposition-functions.lagda.md b/src/foundation/precomposition-functions.lagda.md index eba63757e6..720c665b0e 100644 --- a/src/foundation/precomposition-functions.lagda.md +++ b/src/foundation/precomposition-functions.lagda.md @@ -113,7 +113,7 @@ type of maps `h : B → X` equipped with a homotopy witnessing that the square A -----> B | | f | | h - V V + ∨ ∨ B -----> X g ``` diff --git a/src/foundation/preunivalent-type-families.lagda.md b/src/foundation/preunivalent-type-families.lagda.md index 0a71d755dd..96fb37312b 100644 --- a/src/foundation/preunivalent-type-families.lagda.md +++ b/src/foundation/preunivalent-type-families.lagda.md @@ -70,7 +70,7 @@ is-preunivalent-UU l = preunivalence \ / \ / equiv-tr B \ / equiv-eq - v v + ∨ ∨ (B x ≃ B y) ``` diff --git a/src/foundation/pullbacks-subtypes.lagda.md b/src/foundation/pullbacks-subtypes.lagda.md index 816963473b..f2f6b26b72 100644 --- a/src/foundation/pullbacks-subtypes.lagda.md +++ b/src/foundation/pullbacks-subtypes.lagda.md @@ -34,7 +34,7 @@ Consider a [subtype](foundation-core.subtypes.md) `T` of a type `B` and a map | ⌟ | π₁ | | i | | - V V + ∨ ∨ A -----------> B f ``` diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md index 6eb3956b41..7da824f4bb 100644 --- a/src/foundation/pullbacks.lagda.md +++ b/src/foundation/pullbacks.lagda.md @@ -332,7 +332,7 @@ Given a pullback square C -------> B | ⌟ | g'| | g - v v + ∨ ∨ A -------> X f ``` diff --git a/src/foundation/retracts-of-maps.lagda.md b/src/foundation/retracts-of-maps.lagda.md index 1ab6ec6ad7..d79a6ea065 100644 --- a/src/foundation/retracts-of-maps.lagda.md +++ b/src/foundation/retracts-of-maps.lagda.md @@ -48,7 +48,7 @@ of `X` and `B` of `Y` that fit into a commutative diagram A ------> X ------> A | | | f | i | g r | f - v v v + ∨ ∨ ∨ B ------> Y ------> B i₁ r₁ ``` @@ -70,7 +70,7 @@ coherence | | r₁ ·l i⁻¹ | L | f ·l H₀ | | - V V + ∨ ∨ r₁ ∘ i₁ ∘ f ---------------> f H₁ ·r f ``` @@ -88,7 +88,7 @@ the square A ========= A | | f | refl-htpy | f - v v + ∨ ∨ B ========= B, ``` @@ -291,7 +291,7 @@ In fact, we only need the following data to show this: X ------> A | | g | r | f - v v + ∨ ∨ B ------> Y ------> B. i₁ H₁ r₁ ``` @@ -304,7 +304,7 @@ In fact, we only need the following data to show this: \ / r₁ ∘ g \ / f \ / - V V + ∨ ∨ B. ``` @@ -351,7 +351,7 @@ In fact, we only need the following data to show this: A ------> X ------> A | | f | i | g - v v + ∨ ∨ B ------> Y. i₁ ``` @@ -364,7 +364,7 @@ In fact, we only need the following data to show this: \ / g ∘ i₀ \ / i₁ \ / - V V + ∨ ∨ Y. ``` @@ -461,11 +461,11 @@ row of squares in the diagram below. fiber f b -----> fiber g (i₁ b) -----> fiber f b | | | | i' | r' | - v v v + ∨ ∨ ∨ A ----- i₀ -----> X ------- r₀ ------> A | | | f | i | g r | f - v v v + ∨ ∨ ∨ B --------------> Y -----------------> B i₁ r₁ ``` @@ -482,7 +482,7 @@ obtain a commuting diagram fiber f b -----> fiber g (i₁ b) -----> fiber f (r₀ (i₀ b)) -----> fiber f b | | | | | i' | r' | | - v v v V + ∨ ∨ ∨ ∨ A --------------> X --------------------> A ---------------------> A i₀ r₀ id ``` diff --git a/src/foundation/standard-pullbacks.lagda.md b/src/foundation/standard-pullbacks.lagda.md index 825b7f3264..9cf5905aa3 100644 --- a/src/foundation/standard-pullbacks.lagda.md +++ b/src/foundation/standard-pullbacks.lagda.md @@ -52,7 +52,7 @@ of the cospan, completing the diagram | ⌟ | | | g | | - v v + ∨ ∨ A ---------> X. f ``` @@ -478,7 +478,7 @@ Given a standard pullback square C -------> B | ⌟ | g'| | g - v v + ∨ ∨ A -------> X f ``` @@ -490,7 +490,7 @@ square C ---------> X | ⌟ | (f' , g') | | - v v + ∨ ∨ A × B -----> X × X, f × g ``` diff --git a/src/foundation/univalent-type-families.lagda.md b/src/foundation/univalent-type-families.lagda.md index bf200504ea..129dfaf7be 100644 --- a/src/foundation/univalent-type-families.lagda.md +++ b/src/foundation/univalent-type-families.lagda.md @@ -96,7 +96,7 @@ is-univalent-UU l = univalence \ / \ / equiv-tr B \ / equiv-eq - v v + ∨ ∨ (B x ≃ B y) ``` diff --git a/src/foundation/universal-property-pullbacks.lagda.md b/src/foundation/universal-property-pullbacks.lagda.md index cd17827ad2..0b97e575fa 100644 --- a/src/foundation/universal-property-pullbacks.lagda.md +++ b/src/foundation/universal-property-pullbacks.lagda.md @@ -82,7 +82,7 @@ Given a diagram ∙ -------> ∙ -------> ∙ | | ⌟ | | | | - v v v + ∨ ∨ ∨ ∙ -------> ∙ -------> ∙ ``` @@ -138,11 +138,11 @@ Given a diagram ∙ -------> ∙ | | | | - v v + ∨ ∨ ∙ -------> ∙ | ⌟ | | | - v v + ∨ ∨ ∙ -------> ∙ ``` diff --git a/src/group-theory/commuting-squares-of-group-homomorphisms.lagda.md b/src/group-theory/commuting-squares-of-group-homomorphisms.lagda.md index 13d20483a4..e8e02a54ec 100644 --- a/src/group-theory/commuting-squares-of-group-homomorphisms.lagda.md +++ b/src/group-theory/commuting-squares-of-group-homomorphisms.lagda.md @@ -25,7 +25,7 @@ A square of [group homomorphisms](group-theory.homomorphisms-groups.md) G -----> H | | g | | h - V V + ∨ ∨ K -----> L k ``` diff --git a/src/group-theory/functoriality-quotient-groups.lagda.md b/src/group-theory/functoriality-quotient-groups.lagda.md index 91f0b9d98b..6b48fc225f 100644 --- a/src/group-theory/functoriality-quotient-groups.lagda.md +++ b/src/group-theory/functoriality-quotient-groups.lagda.md @@ -41,7 +41,7 @@ satisfying the property that `x ∈ N ⇒ f x ∈ M` induces a group homomorphis G -------> H | | q | | q - V V + ∨ ∨ G/N -----> H/M g ``` diff --git a/src/group-theory/homomorphisms-group-actions.lagda.md b/src/group-theory/homomorphisms-group-actions.lagda.md index d615116603..b9f76c3392 100644 --- a/src/group-theory/homomorphisms-group-actions.lagda.md +++ b/src/group-theory/homomorphisms-group-actions.lagda.md @@ -40,7 +40,7 @@ that for any element `g` of the [group](group-theory.groups.md) `G` the square X -----> Y | | μ g | | μ g - V V + ∨ ∨ X -----> Y f ``` diff --git a/src/group-theory/pullbacks-subgroups.lagda.md b/src/group-theory/pullbacks-subgroups.lagda.md index 46578fdb29..8ac1c10168 100644 --- a/src/group-theory/pullbacks-subgroups.lagda.md +++ b/src/group-theory/pullbacks-subgroups.lagda.md @@ -170,7 +170,7 @@ The square | | K ↦ UK | | K ↦ UK | | - V V + ∨ ∨ subset-Group H ------------> subset-Group G pullback f ``` diff --git a/src/group-theory/pullbacks-subsemigroups.lagda.md b/src/group-theory/pullbacks-subsemigroups.lagda.md index c5718c895f..cfefc2061d 100644 --- a/src/group-theory/pullbacks-subsemigroups.lagda.md +++ b/src/group-theory/pullbacks-subsemigroups.lagda.md @@ -123,7 +123,7 @@ The square | | K ↦ UK | | K ↦ UK | | - V V + ∨ ∨ subset-Semigroup H ------------> subset-Semigroup G pullback f ``` diff --git a/src/group-theory/quotient-groups.lagda.md b/src/group-theory/quotient-groups.lagda.md index 0f695c97ba..d109a8292d 100644 --- a/src/group-theory/quotient-groups.lagda.md +++ b/src/group-theory/quotient-groups.lagda.md @@ -628,7 +628,7 @@ along `q`: | \ q | \ f | \ - V V + ∨ ∨ G/N -> H. ∃! ``` diff --git a/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md b/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md index d4f6728889..bdcb3c854f 100644 --- a/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md +++ b/src/group-theory/subgroups-generated-by-subsets-groups.lagda.md @@ -521,7 +521,7 @@ implies that the square | | S ↦ ⟨S⟩ | | S ↦ ⟨S⟩ | | - V V + ∨ ∨ Subgroup G ----------> Subgroup H im f ``` diff --git a/src/group-theory/torsion-free-groups.lagda.md b/src/group-theory/torsion-free-groups.lagda.md index f207fffb76..d7e4ed6170 100644 --- a/src/group-theory/torsion-free-groups.lagda.md +++ b/src/group-theory/torsion-free-groups.lagda.md @@ -57,7 +57,7 @@ holds for all elements `x : G`. This condition can be formulated in several · ---------> Prop | ⌟ | p| | P ↦ {k : ℤ ∣ (k ＝ 0) ∨ P} - V V + ∨ ∨ G -------> Subgroup ℤ order ``` diff --git a/src/order-theory/commuting-squares-of-order-preserving-maps-large-posets.lagda.md b/src/order-theory/commuting-squares-of-order-preserving-maps-large-posets.lagda.md index 757d613c0d..42b32bdb2f 100644 --- a/src/order-theory/commuting-squares-of-order-preserving-maps-large-posets.lagda.md +++ b/src/order-theory/commuting-squares-of-order-preserving-maps-large-posets.lagda.md @@ -29,7 +29,7 @@ A square P -----> U | | f | | g - V V + ∨ ∨ Q -----> V j ``` diff --git a/src/orthogonal-factorization-systems/cd-structures.lagda.md b/src/orthogonal-factorization-systems/cd-structures.lagda.md index 3fcfbb6f4c..d33d5a3d4a 100644 --- a/src/orthogonal-factorization-systems/cd-structures.lagda.md +++ b/src/orthogonal-factorization-systems/cd-structures.lagda.md @@ -26,7 +26,7 @@ class `𝒟` of A -----> X | | f | | g - V V + ∨ ∨ B -----> Y. j ``` diff --git a/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md index 5c8a20cb5d..54bbaced86 100644 --- a/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md @@ -264,7 +264,7 @@ diagram / | \ a/ | \c / |b \ - V V V + ∨ ∨ ∨ A --> B --> C f g ``` diff --git a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md index 440844254f..02e43793b1 100644 --- a/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-of-maps.lagda.md @@ -54,7 +54,7 @@ along `i` to `f`. | \ i f | \ - v v + ∨ ∨ B - g -> P ``` @@ -110,12 +110,12 @@ module _ | \ i f | \ - v v + ∨ ∨ B - g -> P - | ^ + | ∧ j / | h - v / + ∨ / C ``` @@ -138,7 +138,7 @@ module _ / | \ f g h / | \ - v v v + ∨ ∨ ∨ B - i -> C - j -> P ``` @@ -179,7 +179,7 @@ module _ | \ i f | \ - v v + ∨ ∨ B - g -> C - h -> P ``` @@ -202,7 +202,7 @@ module _ | \ i f | \ - v v + ∨ ∨ B - g -> P ``` diff --git a/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md b/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md index aa145fda24..4f01d8a991 100644 --- a/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md +++ b/src/orthogonal-factorization-systems/factorization-operations-function-classes.lagda.md @@ -45,9 +45,9 @@ in `L`, and the right map is in `R`. ```text ∙ - ^ \ + ∧ \ L ∋ / \ ∈ R - / v + / ∨ A -----> B ``` diff --git a/src/orthogonal-factorization-systems/factorization-operations-global-function-classes.lagda.md b/src/orthogonal-factorization-systems/factorization-operations-global-function-classes.lagda.md index 1b1358fa3a..a372c14a56 100644 --- a/src/orthogonal-factorization-systems/factorization-operations-global-function-classes.lagda.md +++ b/src/orthogonal-factorization-systems/factorization-operations-global-function-classes.lagda.md @@ -27,9 +27,9 @@ in `L`, and the right map is in `R`. ```text Im f - ^ \ + ∧ \ L ∋ / \ ∈ R - / v + / ∨ A ------> B f ``` diff --git a/src/orthogonal-factorization-systems/factorization-operations.lagda.md b/src/orthogonal-factorization-systems/factorization-operations.lagda.md index ef97591565..9262dfd081 100644 --- a/src/orthogonal-factorization-systems/factorization-operations.lagda.md +++ b/src/orthogonal-factorization-systems/factorization-operations.lagda.md @@ -22,9 +22,9 @@ every map `f` in `A → B`. ```text Im f - ^ \ + ∧ \ / \ - / v + / ∨ A ------> B f ``` diff --git a/src/orthogonal-factorization-systems/factorizations-of-maps-function-classes.lagda.md b/src/orthogonal-factorization-systems/factorizations-of-maps-function-classes.lagda.md index 31bf354643..f4eee03050 100644 --- a/src/orthogonal-factorization-systems/factorizations-of-maps-function-classes.lagda.md +++ b/src/orthogonal-factorization-systems/factorizations-of-maps-function-classes.lagda.md @@ -42,9 +42,9 @@ such that their composite `r ∘ l` is `f`. ```text X - ^ \ + ∧ \ L ∋ l / \ r ∈ R - / v + / ∨ A -----> B f ``` diff --git a/src/orthogonal-factorization-systems/factorizations-of-maps-global-function-classes.lagda.md b/src/orthogonal-factorization-systems/factorizations-of-maps-global-function-classes.lagda.md index 49d6546998..9945116577 100644 --- a/src/orthogonal-factorization-systems/factorizations-of-maps-global-function-classes.lagda.md +++ b/src/orthogonal-factorization-systems/factorizations-of-maps-global-function-classes.lagda.md @@ -43,9 +43,9 @@ classes `L` and `R`** of a map `f : A → B` is a pair of maps `l : A → X` and ```text X - ^ \ + ∧ \ L ∋ l / \ r ∈ R - / v + / ∨ A -----> B f ``` diff --git a/src/orthogonal-factorization-systems/factorizations-of-maps.lagda.md b/src/orthogonal-factorization-systems/factorizations-of-maps.lagda.md index 8dc962ca58..a4266abdd5 100644 --- a/src/orthogonal-factorization-systems/factorizations-of-maps.lagda.md +++ b/src/orthogonal-factorization-systems/factorizations-of-maps.lagda.md @@ -32,9 +32,9 @@ A **factorization** of a map `f : A → B` is a pair of maps `g : X → B` and ```text X - ^ \ + ∧ \ h / \ g - / v + / ∨ A -----> B f ``` diff --git a/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md b/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md index 4ff943dd58..5bf2870bfe 100644 --- a/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/functoriality-higher-modalities.lagda.md @@ -40,7 +40,7 @@ into a [natural square](foundation-core.commuting-squares-of-maps.md) X ------> Y | | | | - v v + ∨ ∨ ○ X ----> ○ Y. ○ f ``` @@ -101,7 +101,7 @@ For every map `f : X → Y` there is a naturality square X ------> Y | | | | - v v + ∨ ∨ ○ X ----> ○ Y. ○ f ``` diff --git a/src/orthogonal-factorization-systems/lifting-operations.lagda.md b/src/orthogonal-factorization-systems/lifting-operations.lagda.md index 6acf6a8485..35f437fa9b 100644 --- a/src/orthogonal-factorization-systems/lifting-operations.lagda.md +++ b/src/orthogonal-factorization-systems/lifting-operations.lagda.md @@ -28,7 +28,7 @@ and `g`_ is a choice of lifting square for every commuting square A ------> B | | f| |g - V V + ∨ ∨ X ------> Y. ``` diff --git a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md index 9df8289124..5b83a70324 100644 --- a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md +++ b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md @@ -61,7 +61,7 @@ lifting diagram | | pr1 | - v + ∨ I ------> A . a ``` diff --git a/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md b/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md index a8cc6f74dc..779ab60222 100644 --- a/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md +++ b/src/orthogonal-factorization-systems/lifts-of-maps.lagda.md @@ -37,10 +37,10 @@ such that the composition `i ∘ g` is `f`. ```text A - ^| + ∧| / i g | - / v + / ∨ X - f -> B ``` @@ -78,15 +78,15 @@ module _ ```text A - ^| + ∧| / i g | - / v + / ∨ X - f -> B \ | h j \ | - v v + ∨ ∨ C ``` @@ -107,7 +107,7 @@ module _ \ | / h i j \ | / - v v v + ∨ ∨ ∨ X ``` @@ -126,10 +126,10 @@ module _ ```text A - ^| + ∧| / i g | - / v + / ∨ X - f -> B - h -> S ``` @@ -147,10 +147,10 @@ module _ ```text A - ^| + ∧| / i g | - / v + / ∨ S - h -> X - f -> B ``` diff --git a/src/orthogonal-factorization-systems/modal-induction.lagda.md b/src/orthogonal-factorization-systems/modal-induction.lagda.md index 150e807411..207aa7c89a 100644 --- a/src/orthogonal-factorization-systems/modal-induction.lagda.md +++ b/src/orthogonal-factorization-systems/modal-induction.lagda.md @@ -263,7 +263,7 @@ For every `f : X → Y` there is an associated X ------> Y | | | | - v v + ∨ ∨ ○ X ----> ○ Y. ○ f ``` diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md index 9c1d91990e..b00240504a 100644 --- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md +++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md @@ -71,7 +71,7 @@ The map `f : A → B` is said to be B → X -------> A → X | | g ∘ - | | g ∘ - - V V + ∨ ∨ B → Y -------> A → Y. - ∘ f ``` @@ -139,7 +139,7 @@ The maps `f` and `g` are orthogonal if and only if the square B → X -------> A → X | | g ∘ - | | g ∘ - - V V + ∨ ∨ B → Y -------> A → Y. - ∘ f ``` @@ -397,11 +397,11 @@ below diagram is a pullback precisely when `g` is right orthogonal to `f`: B → X -------> A → X | | g ∘ - | | g ∘ - - V V + ∨ ∨ B → Y -------> A → Y | ⌟ | h ∘ - | | h ∘ - - V V + ∨ ∨ B → Z -------> A → Z. - ∘ f ``` @@ -493,7 +493,7 @@ below diagram is a pullback precisely when `f` is left orthogonal to `g`: C → X -------> B → X -------> A → X | | ⌟ | g ∘ - | | | g ∘ - - V V V + ∨ ∨ ∨ C → Y -------> B → Y -------> A → Y - ∘ h - ∘ f ``` @@ -585,7 +585,7 @@ If `f ⊥ gᵢ`, for each `i : I`, then `f ⊥ (map-Π g)`. | | map-Π g ∘ - | | map-Π g ∘ - | | - v v + ∨ ∨ (B → Πᵢ Yᵢ) ---------------> (A → Πᵢ Yᵢ) - ∘ f ``` @@ -600,7 +600,7 @@ equivalent to | | map-Π (gᵢ ∘ -) | | map-Π (gᵢ ∘ -) | | - v v + ∨ ∨ (Πᵢ B → Yᵢ) ---------------> (Πᵢ A → Yᵢ) map-Π (- ∘ f) ``` @@ -756,7 +756,7 @@ If `fᵢ ⊥ g` for every `i`, then `(tot f) ⊥ g`. | | g ∘ - | | g ∘ - | | - v v + ∨ ∨ ((Σ I B) → Y) ---------------> ((Σ I A) → Y) - ∘ (tot f) ``` @@ -771,7 +771,7 @@ square is equivalent to | | Πᵢ (g ∘ -) | | Πᵢ (g ∘ -) | | - v v + ∨ ∨ Πᵢ (Bᵢ → Y) -----------> Πᵢ (Aᵢ → Y), Πᵢ (- ∘ fᵢ) ``` @@ -846,7 +846,7 @@ If `f ⊥ g` and `f' ⊥ g`, then `(f + f') ⊥ g`. | | g ∘ - | | g ∘ - | | - v v + ∨ ∨ ((B + B') → Y) ---------------> ((A + A') → Y) - ∘ (f + f') ``` @@ -861,7 +861,7 @@ equivalent to | | (g ∘ -) × (g ∘ -) | | (g ∘ -) × (g ∘ -) | | - v v + ∨ ∨ (B → Y) × (B' → Y) -----------> (A → Y) × (A' → Y), (- ∘ f) × (- ∘ f') ``` @@ -938,7 +938,7 @@ Given a pullback square X' -----> X | ⌟ | g'| | g - v v + ∨ ∨ Y' -----> Y, ``` @@ -998,7 +998,7 @@ that means we have a pullback square B → X -----> A → X | ⌟ | ! ∘ - | | ! ∘ - - v v + ∨ ∨ B → 1 -----> A → 1. - ∘ f ``` diff --git a/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md index db85888742..c197c952bc 100644 --- a/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md +++ b/src/orthogonal-factorization-systems/precomposition-lifts-families-of-elements.lagda.md @@ -45,7 +45,7 @@ In other words, given a diagram | | pr1 | - v + ∨ J ------> I ------> A , f a ``` @@ -111,7 +111,7 @@ different codomains, namely `lift-family-of-elements B (a ∘ f)` and \ / precomp-lift B g a \ / tr (lift-family-of-elements B) (htpy-precomp H A a) \ / - V V + ∨ ∨ lift-family-of-elements B (a ∘ g) ``` @@ -215,7 +215,7 @@ We have a [commuting square](foundation.commuting-squares-of-maps.md) like this: | | | map-inv-distributive-Π-Σ ⇗ map-inv-distributive-Π-Σ | | | - V V + ∨ ∨ I → Σ A B ------------------------------------------------> J → Σ A B , - ∘ f ``` @@ -284,13 +284,13 @@ and `precomp-lifted-family-of-elements g`. One factors through ----------------------------------- / \ / ⇗ htpy-precomp-lifted-family H \ - / V + / ∨ Σ (a : I → A) ((i : I) → B (a i)) ------------------------> Σ (a : J → A) ((j : J) → B (a j)) | precomp-lifted-family f | | | | ⇗ | | map-inv-distributive-Π-Σ map-inv-distributive-Π-Σ | - V V + ∨ ∨ I → Σ A B ------------------------------------------------> J → Σ A B , - ∘ f ``` @@ -304,7 +304,7 @@ while the other factors through `- ∘ g`: | | | map-inv-distributive-Π-Σ ⇗ map-inv-distributive-Π-Σ | | | - V - ∘ g V + ∨ - ∘ g ∨ I → Σ A B ------------------------------------------------> J → Σ A B . \ > \ ⇗ htpy-precomp H / diff --git a/src/orthogonal-factorization-systems/pullback-hom.lagda.md b/src/orthogonal-factorization-systems/pullback-hom.lagda.md index 5bebc74e00..7719fa3e96 100644 --- a/src/orthogonal-factorization-systems/pullback-hom.lagda.md +++ b/src/orthogonal-factorization-systems/pullback-hom.lagda.md @@ -53,7 +53,7 @@ The {{#concept "pullback-hom" Agda=pullback-hom}} or B → X -------> A → X | | g ∘ - | | g ∘ - - V V + ∨ ∨ B → Y -------> A → Y. - ∘ f ``` diff --git a/src/orthogonal-factorization-systems/regular-cd-structures.lagda.md b/src/orthogonal-factorization-systems/regular-cd-structures.lagda.md index 3760dc0dbd..fb4eb45feb 100644 --- a/src/orthogonal-factorization-systems/regular-cd-structures.lagda.md +++ b/src/orthogonal-factorization-systems/regular-cd-structures.lagda.md @@ -28,7 +28,7 @@ satisfies the following three axioms: A -----> A ×_X A | | f | | functoriality Δ g - V V + ∨ ∨ B -----> B ×_Y B. Δ j ``` diff --git a/src/structured-types/commuting-squares-of-pointed-homotopies.lagda.md b/src/structured-types/commuting-squares-of-pointed-homotopies.lagda.md index 450d973a09..0bd38407d8 100644 --- a/src/structured-types/commuting-squares-of-pointed-homotopies.lagda.md +++ b/src/structured-types/commuting-squares-of-pointed-homotopies.lagda.md @@ -27,7 +27,7 @@ A square of [pointed homotopies](structured-types.pointed-homotopies.md) f ------> g | | left | | right - v v + ∨ ∨ h ------> i bottom ``` diff --git a/src/structured-types/equivalences-pointed-arrows.lagda.md b/src/structured-types/equivalences-pointed-arrows.lagda.md index febdc24bdb..0d1aacbfd7 100644 --- a/src/structured-types/equivalences-pointed-arrows.lagda.md +++ b/src/structured-types/equivalences-pointed-arrows.lagda.md @@ -38,7 +38,7 @@ consisting of [pointed equivalences](structured-types.pointed-equivalences.md) A -----> X | | f | | g - V V + ∨ ∨ B -----> Y j ``` diff --git a/src/structured-types/morphisms-pointed-arrows.lagda.md b/src/structured-types/morphisms-pointed-arrows.lagda.md index d86af9b863..a7f8e2d3fe 100644 --- a/src/structured-types/morphisms-pointed-arrows.lagda.md +++ b/src/structured-types/morphisms-pointed-arrows.lagda.md @@ -55,7 +55,7 @@ consisting of pointed maps `i : A →∗ X` and `j : B →∗ Y` and a A -----> X | | f | | g - V V + ∨ ∨ B -----> Y j ``` @@ -144,7 +144,7 @@ of a morphism of pointed arrows A -----> X | | f | | g - V V + ∨ ∨ B -----> Y j ``` @@ -156,7 +156,7 @@ is the morphism of pointed arrows A -----> B | | i | | j - V V + ∨ ∨ X -----> Y. g ``` @@ -204,7 +204,7 @@ The identity morphism of pointed arrows is defined as A -----> A | | f | | f - V V + ∨ ∨ B -----> B id ``` @@ -236,7 +236,7 @@ Consider a commuting diagram of the form A -----> X -----> U | | | f | α g | β | h - V V V + ∨ ∨ ∨ B -----> Y -----> V. α₁ β₁ ``` @@ -251,7 +251,7 @@ of `β : g → h` with `α : f → g` is therefore defined to be A ----------> U | | f | α □ β | h - V V + ∨ ∨ B ----------> V. β₁ ∘ α₁ ``` @@ -424,7 +424,7 @@ and a pointed `2`-homotopy `r₂` witnessing that the square of pointed homotopi (α₁ ∘ f) --------> (α₁ ∘ f) | | α₂ | | α₂ - V V + ∨ ∨ (g ∘ α₀) --------> (g ∘ α₀) g ·l r₀ ``` diff --git a/src/structured-types/morphisms-twisted-pointed-arrows.lagda.md b/src/structured-types/morphisms-twisted-pointed-arrows.lagda.md index 16616f1516..42373c4872 100644 --- a/src/structured-types/morphisms-twisted-pointed-arrows.lagda.md +++ b/src/structured-types/morphisms-twisted-pointed-arrows.lagda.md @@ -33,7 +33,7 @@ consisting of pointed maps `i : X →∗ A` and `j : B →∗ Y` and a A <----- X | | f | | g - V V + ∨ ∨ B -----> Y j ``` diff --git a/src/structured-types/morphisms-types-equipped-with-automorphisms.lagda.md b/src/structured-types/morphisms-types-equipped-with-automorphisms.lagda.md index 109088b2d0..2f74c32b78 100644 --- a/src/structured-types/morphisms-types-equipped-with-automorphisms.lagda.md +++ b/src/structured-types/morphisms-types-equipped-with-automorphisms.lagda.md @@ -32,7 +32,7 @@ that the square X -----> Y | | e| |f - V V + ∨ ∨ X -----> Y h ``` diff --git a/src/structured-types/morphisms-types-equipped-with-endomorphisms.lagda.md b/src/structured-types/morphisms-types-equipped-with-endomorphisms.lagda.md index d5d0626781..3215246b06 100644 --- a/src/structured-types/morphisms-types-equipped-with-endomorphisms.lagda.md +++ b/src/structured-types/morphisms-types-equipped-with-endomorphisms.lagda.md @@ -39,7 +39,7 @@ that the square X -----> Y | | f| |g - V V + ∨ ∨ X -----> Y h ``` diff --git a/src/structured-types/wild-monoids.lagda.md b/src/structured-types/wild-monoids.lagda.md index d0caf2462f..250cabb823 100644 --- a/src/structured-types/wild-monoids.lagda.md +++ b/src/structured-types/wild-monoids.lagda.md @@ -43,11 +43,11 @@ following diagram (A × A) × A ----> A × (A × A) | | (_*_ , id) | | (id, _*_) - v v + ∨ ∨ A × A A × A \ / (_*_) \ / (_*_) - v v + ∨ ∨ A ``` diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index 832bb7d71b..60423d0894 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -320,7 +320,7 @@ module _ | | | f | | j | id | | | - v ⌜ v v + ∨ ⌜ ∨ ∨ A -------> C -------> C i id ``` diff --git a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md index 5e0b0f71b5..9e34713e9c 100644 --- a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md +++ b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md @@ -31,7 +31,7 @@ if the [commuting square](foundation-core.commuting-squares-of-maps.md) A -----> X | | f | h | g - V V + ∨ ∨ B -----> Y j ``` diff --git a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md index 5f4d6c625b..72a7892f98 100644 --- a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md @@ -47,7 +47,7 @@ triangles \ / \ / iₙ \ / iₙ₊₁ - V V + ∨ ∨ X ``` diff --git a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md index daaa5bd191..a8570bc383 100644 --- a/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md +++ b/src/synthetic-homotopy-theory/cocones-under-spans.lagda.md @@ -37,13 +37,13 @@ A **cocone under a [span](foundation.spans.md)** `A <-f- S -g-> B` with codomain [homotopy](foundation.homotopies.md) witnessing that the square ```text - g - S -----> B - | | - f| |j - V V - A -----> X - i + g + S -----> B + | | + f | |j + ∨ ∨ + A -----> X + i ``` [commutes](foundation.commuting-squares-of-maps.md). @@ -215,12 +215,12 @@ cocone-map-comp f g (i , j , H) h k = ### Horizontal composition of cocones ```text - i k - A ----> B ----> C - | | | - f| | | - v v v - X ----> Y ----> Z + i k + A ----> B ----> C + | | | + f | | | + ∨ ∨ ∨ + X ----> Y ----> Z ``` ```agda @@ -250,13 +250,13 @@ pr2 (pr2 (cocone-comp-horizontal f i k c d)) = A variation on the above: ```text - i k - A ----> B ----> C - | | | - f | g | | - v v v - X ----> Y ----> Z - j + i k + A ----> B ----> C + | | | + f | g | | + ∨ ∨ ∨ + X ----> Y ----> Z + j ``` ```agda @@ -273,16 +273,16 @@ cocone-comp-horizontal' f i k g j c coh = ### Vertical composition of cocones ```text - i - A -----> X - | | -f| | - v v - B -----> Y - | | -k| | - v v - C -----> Z + i + A -----> X + | | + f | | + ∨ ∨ + B -----> Y + | | + k | | + ∨ ∨ + C -----> Z ``` ```agda @@ -312,16 +312,16 @@ pr2 (pr2 (cocone-comp-vertical f i k c d)) = A variation on the above: ```text - i - A -----> X - | | -f| |g - v j v - B -----> Y - | | -k| | - v v - C -----> Z + i + A -----> X + | | + f | |g + ∨ j ∨ + B -----> Y + | | + k | | + ∨ ∨ + C -----> Z ``` ```agda @@ -338,26 +338,26 @@ cocone-comp-vertical' f i g j k c coh = Given a commutative diagram like this, ```text - g' - S' ---> B' - / \ \ - f' / \ k \ j - / v g v - A' S ----> B - \ | | - i \ | f | - \ v v - > A ----> X + g' + S' ---> B' + / \ \ + f' / \ k \ j + / ∨ g ∨ + A' S ----> B + \ | | + i \ | f | + \ ∨ ∨ + > A ----> X ``` we can compose both vertically and horizontally to get the following cocone: ```text - S' ---> B' - | | - | | - v v - A' ---> X + S' ---> B' + | | + | | + ∨ ∨ + A' ---> X ``` Notice that the triple `(i,j,k)` is really a morphism of spans. So the resulting diff --git a/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md index ea5a3b5b4e..977930ff08 100644 --- a/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md @@ -90,7 +90,7 @@ Consider a [cocone](synthetic-homotopy-theory.cocones-under-spans.md) S -----> B | | f | | j - V V + ∨ ∨ A -----> X . i ``` @@ -154,7 +154,7 @@ allow us to construct the following / | \ / | \ / | \ - V V V + ∨ ∨ ∨ Σ (h : A → X) ((a : A) → P (h a)) X → Σ (x : X) (P x) Σ (h : B → X) ((b : B) → P (h b)) |\ / \ /| | \ / \ / | @@ -163,7 +163,7 @@ allow us to construct the following | / \ / \ | | / \ / \ | | / \ / \ | - VV V V VV + ∨∨ ∨ ∨ ∨∨ A → Σ (x : X) (P x) Σ (h : S → X) ((s : S) → P (h s)) B → Σ (x : X) (P x) \ | / \ | / @@ -172,7 +172,7 @@ allow us to construct the following \ | / \ | / \ | / - V V V + ∨ ∨ ∨ S → Σ (x : X) (P x) . ``` @@ -196,7 +196,7 @@ i.e. for every `h : X → X` we have a pullback | | | | | | - V V + ∨ ∨ (a : A) → P (h (i a)) -----> (s : S) → P (h (j (g s))) , ``` diff --git a/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md b/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md index d993f3ec14..265ce6a2c9 100644 --- a/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md @@ -34,7 +34,7 @@ the [commuting square](foundation-core.commuting-squares-of-maps.md) Σ A (B ∘ f) --------> Σ X B | | Σ id (g ∘ f) | | Σ id g - V V + ∨ ∨ Σ A (Y ∘ f) --------> Σ X Y. Σ f id ``` diff --git a/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md index 103dab194a..61821fe585 100644 --- a/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md @@ -111,7 +111,7 @@ the form ```text bₙ(x) Bₙ(x) -------> Bₙ₊₁(aₙ(x)) - ^ ^ + ∧ ∧ sₙ | | sₙ₊₁ | | (x : Aₙ) ---> (aₙ(x) : Aₙ₊₁) diff --git a/src/synthetic-homotopy-theory/descent-circle.lagda.md b/src/synthetic-homotopy-theory/descent-circle.lagda.md index 140c0e3a20..8adc5c7904 100644 --- a/src/synthetic-homotopy-theory/descent-circle.lagda.md +++ b/src/synthetic-homotopy-theory/descent-circle.lagda.md @@ -136,7 +136,7 @@ be described as a diagram X -----> A base | | e| | tr A loop - v v + ∨ ∨ X -----> A base α ``` diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md index 84dc466dfb..01f1b5369a 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md @@ -45,7 +45,7 @@ given a pushout square S -----> B | | f| |j - V ⌜ V + ∨ ⌜ ∨ A -----> X i ``` @@ -57,7 +57,7 @@ commuting square Σ (s : S), P(if(s)) ---> Σ (s : S), P(jg(s)) ---> Σ (b : B), P(j(b)) | | | | - V ⌜ V + ∨ ⌜ ∨ Σ (a : A), P(i(a)) -----------------------------> Σ (x : X), P(x) ``` @@ -306,7 +306,7 @@ map of spans: Σ (a : A) (PA a) <------- Σ (s : S) (PA (f s)) -----> Σ (b : B) (PB b) | | | | | | - v v v + ∨ ∨ ∨ Σ (a : A) (P (i a)) <---- Σ (s : S) (P (i (f s))) ---> Σ (b : B) (P (j b)) ``` diff --git a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md index 83f4f990f3..9dd5911269 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md @@ -92,7 +92,7 @@ so it suffices to invoke the flattening lemma for coequalizers. | | | inv-assoc-Σ | ≃ inv-assoc-Σ | ≃ id | ≃ | | | - V ---------> V V + ∨ ---------> ∨ ∨ Σ ((n, a) : Σ ℕ A) P(iₙ a) ---------> Σ ((n, a) : Σ ℕ A) P(iₙ a) -----> Σ (x : X) P(x) , ``` diff --git a/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md index d4acb85496..6b9da03d0f 100644 --- a/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md @@ -51,7 +51,7 @@ and `(B, b)`, their A₀ ---> A₁ ---> A₂ ---> ⋯ ---> X | | | | f₀ | | f₁ | f₂ | g - V V V V + ∨ ∨ ∨ ∨ B₀ ---> B₁ ---> B₂ ---> ⋯ ---> Y b₀ b₁ b₂ ``` @@ -71,7 +71,7 @@ them to their colimits and maps between them. (A, a) A∞ | | f | ↦ | f∞ - V V + ∨ ∨ (B, b) B∞ . ``` @@ -104,7 +104,7 @@ The unique map `g : X → Y` such that the diagram A₀ ---> A₁ ---> A₂ ---> ⋯ ---> X | | | | f₀ | | f₁ | f₂ | g - V V V V + ∨ ∨ ∨ ∨ B₀ ---> B₁ ---> B₂ ---> ⋯ ---> Y b₀ b₁ b₂ ``` @@ -119,16 +119,16 @@ This homotopy of cocones provides ```text Aₙ₊₁ - ^ | \ + ∧ | \ / | \ - / |fₙ₊₁ V + / |fₙ₊₁ ∨ Aₙ ---------> X | | | - | V | + | ∨ | fₙ | Bₙ₊₁ | g - | ^ \ | + | ∧ \ | | / \ | - V/ VV + ∨/ ∨∨ Bₙ ---------> Y , ``` @@ -502,7 +502,7 @@ diagrams, i.e. it is the unique map `g : Y → X` making the diagram B₀ ---> B₁ ---> B₂ ---> ⋯ ---> Y | | | | e₀⁻¹ | | e₁⁻¹ | e₂⁻¹ | g - V V V V + ∨ ∨ ∨ ∨ A₀ ---> A₁ ---> A₂ ---> ⋯ ---> X a₀ a₁ a₂ ``` diff --git a/src/synthetic-homotopy-theory/joins-of-maps.lagda.md b/src/synthetic-homotopy-theory/joins-of-maps.lagda.md index 583b5c6667..d31b23c331 100644 --- a/src/synthetic-homotopy-theory/joins-of-maps.lagda.md +++ b/src/synthetic-homotopy-theory/joins-of-maps.lagda.md @@ -33,7 +33,7 @@ Consider two maps `f : A → X` and `g : B → X` with a common codomain. The A ×_X B -----> B | ⌟ | π₁ | | g - V V + ∨ ∨ A ---------> X. f ``` @@ -46,7 +46,7 @@ the cogap map of any cartesian square A -----> X | ⌟ | f | | g - V V + ∨ ∨ B -----> Y i ``` @@ -70,7 +70,7 @@ from the [fiber](foundation-core.fibers-of-maps.md) of `f * g` to the \ / \ / \ / - V V + ∨ ∨ X. ``` @@ -82,7 +82,7 @@ fits in a [pullback diagram](foundation.pullbacks.md) A *_X B ------> (X × B) ⊔_{A × B} (A × X) | ⌟ | f * g | | f □ g - V V + ∨ ∨ X ----------------> X × X. Δ ``` @@ -96,7 +96,7 @@ that there is a commuting triangle \ / f □ g \ / (f × id) * (id × g) \ / - V V + ∨ ∨ X × Y ``` diff --git a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md index e8bb0099c2..a3825a6e48 100644 --- a/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md +++ b/src/synthetic-homotopy-theory/maps-of-prespectra.lagda.md @@ -39,7 +39,7 @@ such that the squares | | | | | | - v v + ∨ ∨ ΩAₙ₊₁ -----> ΩBₙ₊₁ Ωfₙ₊₁ ``` diff --git a/src/synthetic-homotopy-theory/morphisms-descent-data-circle.lagda.md b/src/synthetic-homotopy-theory/morphisms-descent-data-circle.lagda.md index 0066152d48..d579804e93 100644 --- a/src/synthetic-homotopy-theory/morphisms-descent-data-circle.lagda.md +++ b/src/synthetic-homotopy-theory/morphisms-descent-data-circle.lagda.md @@ -29,7 +29,7 @@ e)`and`(B, f)`is a map`h`from`A`to`B` such that the square A -----> B | | e| |f - v v + ∨ ∨ A -----> B h ``` diff --git a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md index 47a9948110..28bc2708eb 100644 --- a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md @@ -43,7 +43,7 @@ A **morphism between Aₙ ---> Aₙ₊₁ | | fₙ | | fₙ₊₁ - v v + ∨ ∨ Bₙ ---> Bₙ₊₁ bₙ ``` diff --git a/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md index a89e1eacb9..888f86f5ed 100644 --- a/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md @@ -33,7 +33,7 @@ pushout of `S` if and only if the square Y^X -----> Y^B | ⌟ | | | - V V + ∨ ∨ Y^A -----> Y^S ``` diff --git a/src/synthetic-homotopy-theory/pushout-products.lagda.md b/src/synthetic-homotopy-theory/pushout-products.lagda.md index e4755215af..5756497b68 100644 --- a/src/synthetic-homotopy-theory/pushout-products.lagda.md +++ b/src/synthetic-homotopy-theory/pushout-products.lagda.md @@ -34,7 +34,7 @@ of `f` and `g` is defined as the A × B --------> X × B | | id × g | H ⇗ | id × g - V V + ∨ ∨ A × Y --------> X × Y. f × id ``` @@ -61,7 +61,7 @@ and a homotopy `M` witnessing that the | | (f □ g) ·l glue | | H | | - V V + ∨ ∨ (f □ g) ∘ inr ∘ (f × id) ---------------> (id × g) ∘ (f × id) L ·r (f × id) ``` diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md index 0d1437d0ad..11b54821d0 100644 --- a/src/synthetic-homotopy-theory/pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pushouts.lagda.md @@ -57,7 +57,7 @@ A **pushout** of `𝒮` is an initial type `X` equipped with a S -----> B | | f | H | j - V V + ∨ ∨ A -----> X, i ``` @@ -473,11 +473,11 @@ Given a pushout square with a S ----> B | | \ f | inr| \ n - v ⌜ v \ + ∨ ⌜ ∨ \ A ----> ∙ \ \ inl \ | m \ cogap\ | - \ ∨ v + \ ∨ ∨ \-----> X ``` @@ -487,7 +487,7 @@ we have, for every `x : X`, a pushout square of fibers: fiber (m ∘ f) x ---> fiber (cogap ∘ inr) x | | | | - v ⌜ v + ∨ ⌜ ∨ fiber (cogap ∘ inl) x ----> fiber cogap x ``` @@ -601,7 +601,7 @@ We record the following auxiliary lemma which says that if we have types `T`, T ----------> G | | u | | - v ⌜ v + ∨ ⌜ ∨ F ----> fiber cogap x ``` diff --git a/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md index 9be1a3bf29..486abc8c5d 100644 --- a/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md @@ -42,7 +42,7 @@ we may form their **smash product** as the following A ∨∗ B ----> A ×∗ B | | | | - v ⌜ v + ∨ ⌜ ∨ unit -----> A ∧∗ B ``` diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index f36a85d1f9..b66b91c00a 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -546,9 +546,9 @@ So for any `(k+1)`-type `Y`, we have the commutative diagram ```text Δ Y ----------------------> (suspension X → Y) - ^ | + ∧ | pr1 | ≃ ≃ | ev-suspension - | ≃ v + | ≃ ∨ Σ (y y' : Y) , y ＝ y' <----- suspension-structure Y ≐ Σ (y y' : Y) , X → y ＝ y' ``` diff --git a/src/synthetic-homotopy-theory/tangent-spheres.lagda.md b/src/synthetic-homotopy-theory/tangent-spheres.lagda.md index 10dd57a601..ec35fb7cab 100644 --- a/src/synthetic-homotopy-theory/tangent-spheres.lagda.md +++ b/src/synthetic-homotopy-theory/tangent-spheres.lagda.md @@ -39,7 +39,7 @@ Consider a type `X` and a point `x : X`. We say that `x` **has a tangent T -----> C | | | | i - V ⌜ V + ∨ ⌜ ∨ 1 -----> X x ``` diff --git a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md index cdf2ec27c1..88c1339d10 100644 --- a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md @@ -541,7 +541,7 @@ module _ S -------> B -------> C | | | f | | j | inr - v ⌜ v ⌜ v + ∨ ⌜ ∨ ⌜ ∨ A -------> C -------> ∙ i inl ``` @@ -560,7 +560,7 @@ For this, we use the following commutative diagram | | ≃ | (universal | vertical-map-cocone | property) | (second projection) - v v + ∨ ∨ cocone j j X --------------------------> (C → X) vertical-map-cocone (second projection) diff --git a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md index 1aed8853a9..06f4082d85 100644 --- a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md @@ -413,12 +413,12 @@ If in the following diagram the left square is a pushout, then the outer rectangle is a pushout if and only if the right square is a pushout. ```text - g k - A ----> B ----> C - | | | - f| | | - v v v - X ----> Y ----> Z + g k + A ----> B ----> C + | | | + f | | | + ∨ ∨ ∨ + X ----> Y ----> Z ``` ```agda @@ -561,13 +561,13 @@ map f' : S' → A' making the left square commute, then the outer rectangle is again a pushout. ```text - i g - S' ---> S ----> B - | ≃ | | -f' | | f | - v ≃ v ⌜ v - A' ---> A ----> X - j + i g + S' ---> S ----> B + | ≃ | | + f' | | f | + ∨ ≃ ∨ ⌜ ∨ + A' ---> A ----> X + j ``` ```agda @@ -608,16 +608,16 @@ If in the following diagram the top square is a pushout, then the outer rectangle is a pushout if and only if the bottom square is a pushout. ```text - g - A -----> X - | | - f| | - v ⌜ v - B -----> Y - | | - k| | - v v - C -----> Z + g + A -----> X + | | + f | | + ∨ ⌜ ∨ + B -----> Y + | | + k | | + ∨ ∨ + C -----> Z ``` ```agda @@ -758,17 +758,16 @@ rectangle is again a pushout. This is a special case of the vertical pushout pasting lemma. ```text - g' - S' ---> B' - | | - i | ≃ ≃ | j - | | - v g v - S ----> B - | | - f | | - v ⌜ v - A ----> X + g' + S' ---> B' + | | + i | ≃ ≃ | j + ∨ g ∨ + S ----> B + | | + f | | + ∨ ⌜ ∨ + A ----> X ``` ```agda @@ -808,26 +807,26 @@ module _ Given a commutative diagram where `i`, `j` and `k` are equivalences, ```text - g' - S' ---> B' - / \ \ - f' / \ k \ j - / v g v - A' S ----> B - \ | | - i \ | f | - \ v ⌜ v - > A ----> X + g' + S' ---> B' + / \ \ + f' / \ k \ j + / ∨ g ∨ + A' S ----> B + \ | | + i \ | f | + \ ∨ ⌜ ∨ + > A ----> X ``` the induced square is a pushout: ```text - S' ---> B' - | | - | | - v ⌜ v - A' ---> X. + S' ---> B' + | | + | | + ∨ ⌜ ∨ + A' ---> X. ``` This combines both special cases of the pushout pasting lemmas for equivalences. diff --git a/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md index 12b0183707..8cf231f399 100644 --- a/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md @@ -403,7 +403,7 @@ triangle commute: X → Y ----------> cocone A Y \ / \ / - - ∘ i₀ \ / first-map-cocone-sequential-colimit + - ∘ i₀ \ / first-map-cocone-sequential-colimit \ / ∨ ∨ A₀ → Y . @@ -429,8 +429,8 @@ which to every `f : A₀ → Y` assigns the cocone A₀ ----> A₁ ----> A₂ ----> ⋯ \ | / \ | / - \ f∘a₀⁻¹ / - f \ | / f ∘ a₁⁻¹ ∘ a₀⁻¹ + \ f ∘ a₀⁻¹/ + f \ | / f ∘ a₁⁻¹ ∘ a₀⁻¹ \ | / ∨ ∨ ∨ Y , diff --git a/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md index 81a8394688..2c1bae772a 100644 --- a/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md @@ -36,7 +36,7 @@ defined by the following unit ------> A | | | | - v ⌜ v + ∨ ⌜ ∨ B -----> A ∨∗ B, ``` diff --git a/src/trees/morphisms-algebras-polynomial-endofunctors.lagda.md b/src/trees/morphisms-algebras-polynomial-endofunctors.lagda.md index d9c081ee38..12364a1b34 100644 --- a/src/trees/morphisms-algebras-polynomial-endofunctors.lagda.md +++ b/src/trees/morphisms-algebras-polynomial-endofunctors.lagda.md @@ -39,7 +39,7 @@ that the square P A B X ---------> P A B Y | | | | - V V + ∨ ∨ X -------------> Y f ``` diff --git a/src/trees/morphisms-coalgebras-polynomial-endofunctors.lagda.md b/src/trees/morphisms-coalgebras-polynomial-endofunctors.lagda.md index cf2affdfe0..f6771ba67b 100644 --- a/src/trees/morphisms-coalgebras-polynomial-endofunctors.lagda.md +++ b/src/trees/morphisms-coalgebras-polynomial-endofunctors.lagda.md @@ -39,7 +39,7 @@ witnessing that the square X -------------> Y | | | | - V V + ∨ ∨ P A B X ---------> P A B Y P A B f ``` diff --git a/src/type-theories/dependent-type-theories.lagda.md b/src/type-theories/dependent-type-theories.lagda.md index 3e69e57f60..6f40eba0bc 100644 --- a/src/type-theories/dependent-type-theories.lagda.md +++ b/src/type-theories/dependent-type-theories.lagda.md @@ -40,7 +40,7 @@ built. Ã₀ Ã₁ Ã₂ | | | | | | - V V V + ∨ ∨ ∨ A₀ <---- A₁ <---- A₂ <---- ⋯ ```