make pre-commit

src/structured-types/wild-category-of-pointed-types.lagda.md

@@ -21,14 +21,15 @@ open import globular-types.globular-types
 open import globular-types.large-globular-types
 open import globular-types.large-reflexive-globular-types
 open import globular-types.large-transitive-globular-types
+open import globular-types.reflexive-globular-types
+open import globular-types.transitive-globular-types
+
 open import structured-types.pointed-2-homotopies
 open import structured-types.pointed-dependent-functions
 open import structured-types.pointed-families-of-types
 open import structured-types.pointed-homotopies
 open import structured-types.pointed-maps
 open import structured-types.pointed-types
-open import globular-types.reflexive-globular-types
-open import globular-types.transitive-globular-types
 open import structured-types.uniform-pointed-homotopies
 
 open import wild-category-theory.noncoherent-large-wild-higher-precategories

src/wild-category-theory/colax-functors-noncoherent-wild-higher-precategories.lagda.md

@@ -34,9 +34,9 @@ A
 [noncoherent wild higher precategories](wild-category-theory.noncoherent-wild-higher-precategories.md)
 `𝒜` and `ℬ` is a
 [map of noncoherent wild higher precategories](wild-category-theory.maps-noncoherent-wild-higher-precategories.md)
-which is [colax reflexive](globular-types.colax-reflexive-globular-maps.md)
-and [colax transitive](globular-types.colax-transitive-globular-maps.md). This
-means that for every $n$-morphism `f` in `𝒜`, where we take $0$-morphisms to be
+which is [colax reflexive](globular-types.colax-reflexive-globular-maps.md) and
+[colax transitive](globular-types.colax-transitive-globular-maps.md). This means
+that for every $n$-morphism `f` in `𝒜`, where we take $0$-morphisms to be
 objects, there is an $(n+1)$-morphism
 
 ```text

src/wild-category-theory/noncoherent-wild-higher-precategories.lagda.md

@@ -40,8 +40,8 @@ A _noncoherent wild higher precategory_ `𝒞` is a structure that attempts at
 capturing the structure of a higher precategory to the $0$'th order. It consists
 of in some sense all of the operations and none of the coherence of a higher
 precategory. Thus, it is defined as a
-[globular type](globular-types.globular-types.md) with families of
-$n$-morphisms labeled as "identities"
+[globular type](globular-types.globular-types.md) with families of $n$-morphisms
+labeled as "identities"
 
 ```text
   id-hom : (x : 𝑛-Cell 𝒞) → (𝑛+1)-Cell 𝒞 x x
@@ -57,10 +57,10 @@ and a composition operation at every dimension
 Entirely concretely, we define a
 {{#concept "noncoherent wild higher precategory" Agda=Noncoherent-Wild-Higher-Precategory}}
 to be a [reflexive](globular-types.reflexive-globular-types.md) and
-[transitive](globular-types.transitive-globular-types.md) globular type. We
-call the 0-cells the _objects_, the 1-cells the _morphisms_ and the higher cells
-the _$n$-morphisms_. The reflexivities are called the _identity morphisms_, and
-the transitivity operations are branded as _composition of morphisms_.
+[transitive](globular-types.transitive-globular-types.md) globular type. We call
+the 0-cells the _objects_, the 1-cells the _morphisms_ and the higher cells the
+_$n$-morphisms_. The reflexivities are called the _identity morphisms_, and the
+transitivity operations are branded as _composition of morphisms_.
 
 ## Definitions