chore: Fix arrowheads in character diagrams (#1124)

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.

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

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

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

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

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

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

src/category-theory/restrictions-functors-cores-precategories.lagda.md

@@ -42,7 +42,7 @@ that fit into a natural diagram
     |               |
     |               |
     |               |
-    v               v
+    ∨               ∨
     C ------------> D.
             F
 ```

src/finite-group-theory/delooping-sign-homomorphism.lagda.md

@@ -94,7 +94,7 @@ commutes :
   |           |
  ≅|           |≅
   |           |
-  v           v
+  ∨           ∨
   BG ------> BH
        ΩBf
 ```

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

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

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

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.
         α₁       β₁       γ₁
 ```

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

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

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

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

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

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

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

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

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

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

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

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