review

UniMath · Dec 3, 2024 · ea25b4b · ea25b4b
1 parent d002909
commit ea25b4b
Show file tree

Hide file tree

Showing 9 changed files with 6 additions and 9 deletions.
diff --git a/src/globular-types/binary-dependent-reflexive-globular-types.lagda.md b/src/globular-types/binary-dependent-reflexive-globular-types.lagda.md
@@ -31,8 +31,8 @@ Consider two
 
 A binary dependent globular type `K` over reflexive globular types `G` and `H`
 is said to be
-{{#concept "reflexive" Disambiguation="binary dependent globular type"}} if it
-comes equipped with
+{{#concept "reflexive" Disambiguation="binary dependent globular type" Agda=is-reflexive-Binary-Dependent-Globular-Type}}
+if it comes equipped with
 
 ```text
   refl K : {x : G₀} {y : H₀} (u : K₀ x y) → K₁ (refl G x) (refl G y) u u,

diff --git a/src/globular-types/composition-structure-globular-types.lagda.md b/src/globular-types/composition-structure-globular-types.lagda.md
@@ -51,13 +51,16 @@ record
     {l1 l2 : Level} (G : Globular-Type l1 l2) : UU (l1 ⊔ l2)
   where
   coinductive
+
   field
     comp-binary-globular-map-composition-Globular-Type :
       {x y z : 0-cell-Globular-Type G} →
       binary-globular-map
         ( 1-cell-globular-type-Globular-Type G y z)
         ( 1-cell-globular-type-Globular-Type G x y)
         ( 1-cell-globular-type-Globular-Type G x z)
+
+  field
     composition-1-cell-globular-type-Globular-Type :
       {x y : 0-cell-Globular-Type G} →
       composition-Globular-Type

diff --git a/src/globular-types/large-colax-reflexive-globular-maps.lagda.md b/src/globular-types/large-colax-reflexive-globular-maps.lagda.md
@@ -70,7 +70,6 @@ record
     (H : Large-Reflexive-Globular-Type α2 β2)
     (f : large-globular-map-Large-Reflexive-Globular-Type γ G H) : UUω
   where
-  coinductive
 
   field
     preserves-refl-1-cell-is-colax-reflexive-large-globular-map :

diff --git a/src/globular-types/large-colax-transitive-globular-maps.lagda.md b/src/globular-types/large-colax-transitive-globular-maps.lagda.md
@@ -58,7 +58,6 @@ record
     (H : Large-Transitive-Globular-Type α2 β2)
     (f : large-globular-map-Large-Transitive-Globular-Type γ G H) : UUω
   where
-  coinductive
 
   field
     preserves-comp-1-cell-is-colax-transitive-large-globular-map :

diff --git a/src/globular-types/large-lax-reflexive-globular-maps.lagda.md b/src/globular-types/large-lax-reflexive-globular-maps.lagda.md
@@ -70,7 +70,6 @@ record
     (H : Large-Reflexive-Globular-Type α2 β2)
     (f : large-globular-map-Large-Reflexive-Globular-Type γ G H) : UUω
   where
-  coinductive
 
   field
     preserves-refl-1-cell-is-lax-reflexive-large-globular-map :

diff --git a/src/globular-types/large-lax-transitive-globular-maps.lagda.md b/src/globular-types/large-lax-transitive-globular-maps.lagda.md
@@ -58,7 +58,6 @@ record
     (H : Large-Transitive-Globular-Type α2 β2)
     (f : large-globular-map-Large-Transitive-Globular-Type γ G H) : UUω
   where
-  coinductive
 
   field
     preserves-comp-1-cell-is-lax-transitive-large-globular-map :

diff --git a/src/globular-types/large-reflexive-globular-maps.lagda.md b/src/globular-types/large-reflexive-globular-maps.lagda.md
@@ -60,7 +60,6 @@ record
     (f : large-globular-map-Large-Reflexive-Globular-Type γ G H) :
     UUω
   where
-  coinductive
 
   field
     preserves-refl-1-cell-preserves-refl-large-globular-map :

diff --git a/src/globular-types/large-transitive-globular-maps.lagda.md b/src/globular-types/large-transitive-globular-maps.lagda.md
@@ -52,7 +52,6 @@ record
     (H : Large-Transitive-Globular-Type α2 β2)
     (f : large-globular-map-Large-Transitive-Globular-Type γ G H) : UUω
   where
-  coinductive
 
   field
     preserves-comp-1-cell-is-transitive-large-globular-map :

diff --git a/src/globular-types/superglobular-types.lagda.md b/src/globular-types/superglobular-types.lagda.md
@@ -70,7 +70,7 @@ The low-dimensional data of a superglobular type is therefore as follows:
   G₃ : {x y : G₀} {s t : G₁ x y} (u v : G₂ s t) → Type
   H₂ : {x x' y y' : G₀} {s s' : G₁ x x'} {t t' : G₁ y y'}
        (p : G₂ s s') (q : G₂ t t') → H₁ s t → H₁ s' t' → Type
-  e₂ : {x y : G₀} {s t : H₀ x y} {u v : H₁
+  e₂ : {x y : G₀} {s t : H₀ x y} {u v : H₁ (refl G x) (refl G y) s t} →
        H₂ (refl G x) (refl G y) u v ≃ G₃ (e₁ u) (e₁ v)
 ```
-Original file line number
+Diff line change
@@ Expand Up / @@ -60,7 +60,6 @@ record @@
         (f : large-globular-map-Large-Reflexive-Globular-Type γ G H) :
         UUω
       where
-      coinductive
       field
         preserves-refl-1-cell-preserves-refl-large-globular-map :
@@ Expand Down @@