some review comments

src/graph-theory/fibers-directed-graphs.lagda.md

@@ -39,7 +39,7 @@ nodes consists of vertices `y` equipped with a
 of edges from `(y , w)` to `(z , v)` consist of an edge `e : y → z` such that
 `w ＝ cons e v`.
 
-**Note:** The fiber of a directed graphs should not be confused with the
+**Note:** The fiber of a directed graph should not be confused with the
 [fiber of a morphism of directed graphs](graph-theory.fibers-morphisms-directed-graphs.md),
 which is the
 [dependent directed graph](graph-theory.dependent-directed-graphs.md) consisting

src/graph-theory/universal-directed-graph.lagda.md

@@ -46,7 +46,7 @@ The Hofmann–Streicher universe of presheaves on a category `𝒞` is the presh
 
 where `*` is the terminal object of `𝒞/I`, i.e., the identity morphism on `I`.
 
-We compute a the instances of the slice category `⇉/I`:
+We compute the instances of the slice category `⇉/I`:
 
 - The slice category `⇉/0` is the terminal category.
 - The slice category `⇉/1` is the representing cospan

src/structured-types/binary-globular-maps.lagda.md

@@ -11,6 +11,7 @@ module structured-types.binary-globular-maps where
 ```agda
 open import foundation.universe-levels
 
+open import structured-types.globular-maps
 open import structured-types.globular-types
 ```
 
@@ -60,27 +61,3 @@ record
             ( 0-cell-binary-globular-map x y)
             ( 0-cell-binary-globular-map x' y'))
 ```
-
-### Commuting squares of binary globular maps
-
-Consider three [globular maps](structured-types.globular-maps.md) `g : G → G'`,
-`h : H → H'`, and `k : K → K'`, and consider two binary globular maps
-
-```text
-  μ : G → H → K
-  μ' : G' → H' → K'.
-```
-
-A {{#concept "commuting square of binary globular maps"}}
-
-```text
-             μ
-    G   H  ----> K
-    |   |        |
-  g |   | h      | k
-    ∨   ∨        ∨
-    G'  H' ----> K'
-             μ'
-```
-
-consists of a

src/structured-types/globular-maps.lagda.md

@@ -104,7 +104,6 @@ module _
   (F : globular-map A B)
   where
 
-{-
   3-cell-globular-map-globular-map :
     {x y : 0-cell-Globular-Type A}
     {f g : 1-cell-Globular-Type A x y}
@@ -114,11 +113,10 @@ module _
       ( 3-cell-globular-type-Globular-Type B
         ( 2-cell-globular-map F s)
         ( 2-cell-globular-map F t))
-  3-cell-globular-map-globular-map s t =
+  3-cell-globular-map-globular-map =
     2-cell-globular-map-globular-map
       ( 1-cell-globular-map-globular-map F)
--}
-
+
   3-cell-globular-map :
     {x y : 0-cell-Globular-Type A}
     {f g : 1-cell-Globular-Type A x y} →
@@ -136,11 +134,15 @@ module _
 ```agda
 id-globular-map :
   {l1 l2 : Level} (A : Globular-Type l1 l2) → globular-map A A
-id-globular-map A =
+0-cell-globular-map (id-globular-map A) = id
+1-cell-globular-map-globular-map (id-globular-map A) =
+  id-globular-map (1-cell-globular-type-Globular-Type A _ _)
+
+{-
   λ where
   .0-cell-globular-map → id
   .1-cell-globular-map-globular-map {x} {y} →
-    id-globular-map (1-cell-globular-type-Globular-Type A x y)
+    id-globular-map (1-cell-globular-type-Globular-Type A x y) -}
 ```
 
 ### Composition of maps of globular types

src/structured-types/large-lax-reflexive-globular-maps.lagda.md

@@ -30,7 +30,7 @@ between two
 `f : G → H` equipped with a family of 2-cells
 
 ```text
-  (x : G₀) → H₂ (f₁ (Gᵣ x)) (Hᵣ (f₀ x))
+  (x : G₀) → H₂ (Hᵣ (f₀ x)) (f₁ (Gᵣ x))
 ```
 
 from the image of the reflexivity cell at `x` in `G` to the reflexivity cell at

src/structured-types/large-lax-transitive-globular-maps.lagda.md

@@ -30,7 +30,7 @@ between two
 `f : G → H` equipped with a family of 2-cells
 
 ```text
-  H₂ (f₁ (q ∘G p)) (f₁ q ∘H f₁ p)
+  H₂ (f₁ q ∘H f₁ p) (f₁ (q ∘G p))
 ```
 
 from the image of the composite of two 1-cells `q` and `p` in `G` to the

src/structured-types/lax-transitive-globular-maps.lagda.md

@@ -26,7 +26,7 @@ and `H` is a [globular map](structured-types.globular-maps.md) `f : G → H`
 equipped with a family of 2-cells
 
 ```text
-  H₂ (f₁ (q ∘G p)) (f₁ q ∘H f₁ p)
+  H₂ (f₁ q ∘H f₁ p) (f₁ (q ∘G p))
 ```
 
 from the image of the composite of two 1-cells `q` and `p` in `G` to the