Hofmann-Streicher universes for graphs and globular types

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

@@ -107,7 +107,7 @@ record
   where
 ```
 
-- The underlying large globular type of a large reflexive globular type
+**The underlying large globular type of a large reflexive globular type**
 
 ```agda
   field
@@ -274,7 +274,7 @@ record
       large-globular-type-Large-Reflexive-Globular-Type
 ```
 
-- The reflexivity structure of a large reflexive globular type
+**The reflexivity structure of a large reflexive globular type**
 
 ```agda
   field

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

@@ -123,7 +123,7 @@ record
   where
 ```
 
-- The underlying globular type of a reflexive globular type
+**The underlying globular type of a reflexive globular type**
 
 ```agda
   field
@@ -158,7 +158,7 @@ record
       ( globular-type-Reflexive-Globular-Type)
 ```
 
-- The reflexivity structure of a reflexive globular type
+**The reflexivity structure of a reflexive globular type**
 
 ```agda
   field
@@ -196,7 +196,7 @@ record
       refl-Reflexive-Globular-Type
 ```
 
-- The reflexive globular type of 1-cells of a reflexive globular type
+**The reflexive globular type of 1-cells of a reflexive globular type**
 
 ```agda
   1-cell-reflexive-globular-type-Reflexive-Globular-Type :

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

@@ -114,7 +114,7 @@ record
     make-Transitive-Globular-Type
 ```
 
-- The underlying globular type of a transitive globular type
+**The underlying globular type of a transitive globular type**
 
 ```agda
   field
@@ -167,7 +167,7 @@ record
       ( globular-type-Transitive-Globular-Type)
 ```
 
-- The composition structure of a transitive globular type
+**The composition structure of a transitive globular type**
 
 ```agda
   field

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

@@ -209,7 +209,7 @@ record
   where
 ```
 
-- The underlying large globular map of a colax functor
+**The underlying large globular map of a colax functor**
 
 ```agda
   field
@@ -268,7 +268,7 @@ record
         ( map-colax-functor-Noncoherent-Large-Wild-Higher-Precategory)
 ```
 
-- Preservation of the identity structure
+**Preservation of the identity structure**
 
 ```agda
   preserves-id-structure-colax-functor-Noncoherent-Large-Wild-Higher-Precategory :
@@ -319,7 +319,7 @@ record
       is-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- Preservation of the composition structure
+**Preservation of the composition structure**
 
 ```agda
   preserves-comp-structure-colax-functor-Noncoherent-Large-Wild-Higher-Precategory :
@@ -375,7 +375,7 @@ record
       is-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The globular map on hom-types is again a colax functor
+**The globular map on hom-types is again a colax functor**
 
 ```agda
   is-colax-functor-hom-colax-functor-colax-functor-Noncoherent-Large-Wild-Higher-Precategory :

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

@@ -192,7 +192,7 @@ colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ =
     ( is-colax-functor-Noncoherent-Wild-Higher-Precategory 𝒜 ℬ)
 ```
 
-- The action of colax functors on objects, morphisms, and higher morphisms
+**The action of colax functors on objects, morphisms, and higher morphisms**
 
 ```agda
 module _
@@ -248,7 +248,7 @@ module _
   is-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory = pr2 F
 ```
 
-- Preservation by colax functors of identity morphisms
+**Preservation by colax functors of identity morphisms**
 
 ```agda
   preserves-id-hom-colax-functor-Noncoherent-Wild-Higher-Precategory :
@@ -275,7 +275,7 @@ module _
       is-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory
 ```
 
-- Preservation by colax functors of composition
+**Preservation by colax functors of composition**
 
 ```agda
   preserves-comp-hom-colax-functor-Noncoherent-Wild-Higher-Precategory :
@@ -305,8 +305,8 @@ module _
       is-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory
 ```
 
-- The induced colax functor on the wild category of morphisms between two
-  objects
+**The induced colax functor on the wild category of morphisms between two **
+**objects**
 
 ```agda
   hom-colax-functor-colax-functor-Noncoherent-Wild-Higher-Precategory :

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

@@ -79,15 +79,15 @@ record
   where
 ```
 
-- The underlying large globular type of a noncoherent large wild precategory
+**The underlying large globular type of a noncoherent large wild precategory**
 
 ```agda
   field
     large-globular-type-Noncoherent-Large-Wild-Higher-Precategory :
       Large-Globular-Type α β
 ```
 
-- The type of objects of a noncoherent large wild higher precategory
+**The type of objects of a noncoherent large wild higher precategory**
 
 ```agda
   obj-Noncoherent-Large-Wild-Higher-Precategory : (l : Level) → UU (α l)
@@ -96,8 +96,8 @@ record
       large-globular-type-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The globular type of morphisms between two objects in a noncoherent large wild
-  higher precategory
+**The globular type of morphisms between two objects in a noncoherent large **
+**wild higher precategory**
 
 ```agda
   hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory :
@@ -119,8 +119,8 @@ record
       large-globular-type-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The globular structure on the type of objects of a noncoherent large wild
-  higher precategory
+**The globular structure on the type of objects of a noncoherent large wild **
+**higher precategory**
 
 ```agda
   globular-structure-obj-Noncoherent-Large-Wild-Higher-Precategory :
@@ -130,8 +130,8 @@ record
       large-globular-type-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The globular type of 2-morphisms is a noncoherent large wild higher
-  precategory
+**The globular type of 2-morphisms is a noncoherent large wild higher **
+**precategory**
 
 ```agda
   2-hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory :
@@ -154,8 +154,8 @@ record
       large-globular-type-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The globular structure on the type of morphisms between two objects in a
-  noncoherent large wild higher precategory
+**The globular structure on the type of morphisms between two objects in a **
+**noncoherent large wild higher precategory**
 
 ```agda
   globular-structure-hom-Noncoherent-Large-Wild-Higher-Precategory :
@@ -170,8 +170,8 @@ record
       large-globular-type-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The globular type of 3-morphisms in a noncoherent large wild higher
-  precategory
+**The globular type of 3-morphisms in a noncoherent large wild higher **
+**precategory**
 
 ```agda
   3-hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory :
@@ -198,8 +198,8 @@ record
       large-globular-type-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The globular structure on the type of 2-morphisms in a noncoherent large wild
-  higher precategory
+**The globular structure on the type of 2-morphisms in a noncoherent large **
+**wild higher precategory**
 
 ```agda
   globular-structure-2-hom-Noncoherent-Large-Wild-Higher-Precategory :
@@ -215,8 +215,8 @@ record
       large-globular-type-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The structure of identity morphisms in a noncoherent large wild higher
-  precategory
+**The structure of identity morphisms in a noncoherent large wild higher **
+**precategory**
 
 ```agda
   field
@@ -264,7 +264,7 @@ record
       id-structure-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The structure of composition in a noncoherent large wild higher precategory
+**The structure of composition in a noncoherent large wild higher precategory**
 
 ```agda
   field
@@ -320,8 +320,8 @@ record
       comp-structure-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The noncoherent wild higher precategory of morphisms between two object in a
-  noncoherent large wild higher precategory
+**The noncoherent wild higher precategory of morphisms between two object in **
+**a noncoherent large wild higher precategory**
 
 ```agda
   hom-noncoherent-wild-higher-precategory-Noncoherent-Large-Wild-Higher-Precategory :
@@ -338,8 +338,8 @@ record
         ( comp-structure-hom-globular-type-Noncoherent-Large-Wild-Higher-Precategory)
 ```
 
-- The underlying reflexive globular type of a noncoherent large wild higher
-  precategory
+**The underlying reflexive globular type of a noncoherent large wild higher **
+**precategory**
 
 ```agda
   large-reflexive-globular-type-Noncoherent-Large-Wild-Higher-Precategory :
@@ -352,8 +352,8 @@ record
     id-structure-Noncoherent-Large-Wild-Higher-Precategory
 ```
 
-- The underlying transitive globular type of a noncoherent large wild higher
-  precategory
+**The underlying transitive globular type of a noncoherent large wild higher **
+**precategory**
 
 ```agda
   large-transitive-globular-type-Noncoherent-Large-Wild-Higher-Precategory :

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

@@ -92,7 +92,7 @@ module _
     0-cell-Globular-Type globular-type-Noncoherent-Wild-Higher-Precategory
 ```
 
-- Morphisms in a noncoherent wild higher precategory
+**Morphisms in a noncoherent wild higher precategory**
 
 ```agda
   hom-globular-type-Noncoherent-Wild-Higher-Precategory :
@@ -110,7 +110,7 @@ module _
     1-cell-Globular-Type globular-type-Noncoherent-Wild-Higher-Precategory
 ```
 
-- Identity morphisms in a noncoherent wild higher precategory
+**Identity morphisms in a noncoherent wild higher precategory**
 
 ```agda
   id-structure-Noncoherent-Wild-Higher-Precategory :
@@ -152,7 +152,7 @@ module _
       ( y)
 ```
 
-- Composition in a noncoherent wild higher precategory
+**Composition in a noncoherent wild higher precategory**
 
 ```agda
   comp-structure-Noncoherent-Wild-Higher-Precategory :
@@ -197,8 +197,8 @@ module _
       ( y)
 ```
 
-- The noncoherent wild higher precategory of morphisms between two objects in a
-  noncoherent wild higher precategory
+**The noncoherent wild higher precategory of morphisms between two objects in **
+**a noncoherent wild higher precategory**
 
 ```agda
   hom-noncoherent-wild-higher-precategory-Noncoherent-Wild-Higher-Precategory :
@@ -212,7 +212,7 @@ module _
       ( comp-structure-hom-globular-type-Noncoherent-Wild-Higher-Precategory)
 ```
 
-- 2-Morphisms in a noncoherent wild higher precategory
+**2-Morphisms in a noncoherent wild higher precategory**
 
 ```agda
   2-hom-Noncoherent-Wild-Higher-Precategory :
@@ -242,7 +242,7 @@ module _
       comp-structure-Noncoherent-Wild-Higher-Precategory
 ```
 
-- 3-Morphisms in a noncoherent wild higher precategory
+**3-Morphisms in a noncoherent wild higher precategory**
 
 ```agda
   3-hom-Noncoherent-Wild-Higher-Precategory :