Globular pasting diagrams

src/globular-types.lagda.md

@@ -11,6 +11,7 @@ module globular-types where
 
 open import globular-types.base-change-dependent-globular-types public
 open import globular-types.base-change-dependent-reflexive-globular-types public
+open import globular-types.batanin-systems-globular-types public
 open import globular-types.binary-dependent-globular-types public
 open import globular-types.binary-dependent-reflexive-globular-types public
 open import globular-types.binary-globular-maps public
@@ -28,8 +29,13 @@ open import globular-types.empty-globular-types public
 open import globular-types.equality-globular-types public
 open import globular-types.exponentials-globular-types public
 open import globular-types.fibers-globular-maps public
+open import globular-types.globular-disks public
 open import globular-types.globular-equivalences public
 open import globular-types.globular-maps public
+open import globular-types.globular-pasting-diagrams public
+open import globular-types.globular-pasting-schemes public
+open import globular-types.globular-spheres public
+open import globular-types.globular-suspension public
 open import globular-types.globular-types public
 open import globular-types.large-colax-reflexive-globular-maps public
 open import globular-types.large-colax-transitive-globular-maps public

src/globular-types/batanin-systems-globular-types.lagda.md

@@ -0,0 +1,71 @@
+# Batanin systems in globular types
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module globular-types.batanin-systems-globular-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.universe-levels
+
+open import globular-types.globular-types
+
+open import lists.lists
+
+open import trees.plane-trees
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "Batanin system" Disambiguation="globular types" Agda=batanin-system-Globular-Type}}
+is similar to a
+[pasting diagram](globular-types.globular-pasting-diagrams.md) of
+[globular types](globular-types.globular-types.md), but it is defined directly in terms of its cells and not as a [globular map](globular-types.globular-maps.md) from a representing object.
+
+## Definition
+
+### Batanin systems
+
+```agda
+module _
+  {l1 : Level}
+  where
+
+  mutual
+    batanin-system-Globular-Type :
+      (T : listed-plane-tree) (G : Globular-Type l1 l1) → UU l1
+    batanin-system-Globular-Type (make-listed-plane-tree nil) G =
+      0-cell-Globular-Type G
+    batanin-system-Globular-Type (make-listed-plane-tree (cons T ℓ)) G =
+      Σ ( 0-cell-Globular-Type G)
+        ( λ x →
+          Σ ( batanin-system-Globular-Type (make-listed-plane-tree ℓ) G)
+            ( λ B →
+              batanin-system-Globular-Type T
+                ( 1-cell-globular-type-Globular-Type G
+                  ( x)
+                  ( source-cell-batanin-system-Globular-Type
+                    ( make-listed-plane-tree ℓ)
+                    ( G)
+                    ( B)))))
+
+    source-cell-batanin-system-Globular-Type :
+      (T : listed-plane-tree) (G : Globular-Type l1 l1)
+      (B : batanin-system-Globular-Type T G) → 0-cell-Globular-Type G
+    source-cell-batanin-system-Globular-Type (make-listed-plane-tree nil) G B =
+      B
+    source-cell-batanin-system-Globular-Type
+      ( make-listed-plane-tree (cons T ℓ))
+      ( G)
+      ( B) =
+      pr1 B
+```

src/globular-types/empty-globular-types.lagda.md

@@ -54,3 +54,13 @@ module _
 empty-Globular-Type : Globular-Type lzero lzero
 empty-Globular-Type = constant-Globular-Type empty
 ```
+
+### The empty globular type of an arbitrary universe level
+
+```agda
+raise-empty-Globular-Type : (l1 l2 : Level) → Globular-Type l1 l2
+0-cell-Globular-Type (raise-empty-Globular-Type l1 l2) =
+  raise-empty l1
+1-cell-globular-type-Globular-Type (raise-empty-Globular-Type l1 l2) x y =
+  raise-empty-Globular-Type l2 l2
+```

src/globular-types/globular-disks.lagda.md

@@ -0,0 +1,62 @@
+# Globular disks
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module globular-types.globular-disks where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.booleans
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import globular-types.empty-globular-types
+open import globular-types.globular-suspension
+open import globular-types.globular-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "globular `n`-disk" Disambiguation="globular type" Agda=globular-disk}}
+is a [globular type](globular-types.globular-types.md) with the property that
+`n`-cells in an arbitrary globular type `G` are equivalently described as
+[globular maps](globular-types.globular-maps.md) from the globular `n`-disk into
+`G`. In other words, the globular `n`-disk can be thought of as the representing
+`n`-cell.
+
+## Definitions
+
+### The globular `0`-disk
+
+```agda
+0-cell-globular-0-disk : UU lzero
+0-cell-globular-0-disk = unit
+
+1-cell-globular-type-globular-0-disk :
+  (x y : 0-cell-globular-0-disk) → Globular-Type lzero lzero
+1-cell-globular-type-globular-0-disk x y =
+  empty-Globular-Type
+
+globular-0-disk :
+  Globular-Type lzero lzero
+0-cell-Globular-Type globular-0-disk =
+  0-cell-globular-0-disk
+1-cell-globular-type-Globular-Type globular-0-disk =
+  1-cell-globular-type-globular-0-disk
+```
+
+### The globular `n`-disk
+
+```agda
+globular-disk : (n : ℕ) → Globular-Type lzero lzero
+globular-disk zero-ℕ = globular-0-disk
+globular-disk (succ-ℕ n) = suspension-Globular-Type (globular-disk n)
+```

src/globular-types/globular-pasting-diagrams.lagda.md

@@ -0,0 +1,43 @@
+# Globular pasting diagrams
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module globular-types.globular-pasting-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import globular-types.globular-maps
+open import globular-types.globular-pasting-schemes
+open import globular-types.globular-types
+
+open import trees.plane-trees
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "globular pasting diamgram" Disambiguation="globular types" Agda=pasting-diagram-Globular-Type}}
+in a [globular type](globular-types.globular-types.md) `G` is a
+[globular map](globular-types.globular-maps.md) from a
+[globular pasting scheme](globular-types.globular-pasting-schemes.md) into `G`.
+
+## Definitions
+
+### Globular pasting diagrams
+
+```agda
+module _
+  {l1 l2 : Level} (T : listed-plane-tree) (G : Globular-Type l1 l2)
+  where
+
+  pasting-diagram-Globular-Type : UU (l1 ⊔ l2)
+  pasting-diagram-Globular-Type =
+    globular-map (pasting-scheme-Globular-Type T) G
+```

src/globular-types/globular-pasting-schemes.lagda.md

@@ -0,0 +1,142 @@
+# Globular pasting schemes
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module globular-types.globular-pasting-schemes where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.maybe
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import globular-types.empty-globular-types
+open import globular-types.globular-disks
+open import globular-types.globular-types
+
+open import lists.lists
+
+open import trees.plane-trees
+```
+
+</details>
+
+## Idea
+
+Consider a [plane tree](trees.plane-trees.md) `T` such as
+
+```text
+  *       *     *
+   \     /      |
+    \   /       |
+     \ /        |
+      *    *    *
+       \   |   /
+        \  |  /
+         \ | /
+           *
+```
+
+The
+{{#concept "globular pasting scheme" Disambiguation="globular type" Agda=pasting-scheme-Globular-Type}}
+of shape `T` is a [globular type](globular-types.globular-types.md) defined
+inductively on the shape of `T` as follows:
+
+- If `T = nil`, then the pasting scheme of shape `T` is a representing 0-cell.
+  That is, a pasting scheme of shape nil is the
+  [0-disk](globular-types.globular-disks.md).
+- If `T = S ∷ ℓ`, where `ℓ` is a [list](lists.lists.md) of plane trees, then the
+  pasting scheme of shape `T` consists a 0-cell `x₀`, the pasting scheme of
+  shape `ℓ` seen as a plane tree, which has an initial 0-cell `x₁`, and the
+  globular type of `1`-cells between `x₀` and `x₁` is the pasting scheme of
+  shape `T`.
+
+In other words, a globular pasting scheme is a representing object for
+[globular pasting diagrams](globular-types.globular-pasting-diagrams.md) of its
+shape. The example plane tree `T` displayed above gives the following pasting
+scheme:
+
+```text
+     _____
+    /  ∥  \             ______
+   /   ∨   ∨           /  ∥   ∨
+  * ------> * ------> *   ∥    *
+   \   ∥    ∧          \  ∨   ∧
+    \  ∨   /            ------
+     -----
+```
+
+## Definitions
+
+### Pasting schemes
+
+```agda
+module _
+  where
+
+  pasting-scheme-Globular-Type :
+    (T : listed-plane-tree) → Globular-Type lzero lzero
+  pasting-scheme-Globular-Type (make-listed-plane-tree nil) =
+    globular-0-disk
+  0-cell-Globular-Type (pasting-scheme-Globular-Type
+    ( make-listed-plane-tree (cons T ℓ))) =
+    Maybe
+      ( 0-cell-Globular-Type
+        ( pasting-scheme-Globular-Type (make-listed-plane-tree ℓ)))
+  1-cell-globular-type-Globular-Type
+    ( pasting-scheme-Globular-Type (make-listed-plane-tree (cons T nil)))
+    ( inl x)
+    ( inl y) =
+    empty-Globular-Type
+  1-cell-globular-type-Globular-Type
+    ( pasting-scheme-Globular-Type (make-listed-plane-tree (cons T nil)))
+    ( inl x)
+    ( inr y) =
+    empty-Globular-Type
+  1-cell-globular-type-Globular-Type
+    ( pasting-scheme-Globular-Type (make-listed-plane-tree (cons T nil)))
+    ( inr x)
+    ( inl y) =
+    pasting-scheme-Globular-Type T
+  1-cell-globular-type-Globular-Type
+    ( pasting-scheme-Globular-Type (make-listed-plane-tree (cons T nil)))
+    ( inr x)
+    ( inr y) =
+    empty-Globular-Type
+  1-cell-globular-type-Globular-Type
+    ( pasting-scheme-Globular-Type
+      ( make-listed-plane-tree (cons S (cons T ℓ))))
+    ( inl x)
+    ( inl y) =
+    1-cell-globular-type-Globular-Type
+      ( pasting-scheme-Globular-Type (make-listed-plane-tree (cons T ℓ))) x y
+  1-cell-globular-type-Globular-Type
+    ( pasting-scheme-Globular-Type
+      ( make-listed-plane-tree (cons S (cons T ℓ))))
+    ( inl x)
+    ( inr y) =
+    empty-Globular-Type
+  1-cell-globular-type-Globular-Type
+    ( pasting-scheme-Globular-Type
+      ( make-listed-plane-tree (cons S (cons T ℓ))))
+    ( inr x)
+    ( inl (inl y)) = empty-Globular-Type
+  1-cell-globular-type-Globular-Type
+    ( pasting-scheme-Globular-Type
+      ( make-listed-plane-tree (cons S (cons T ℓ))))
+    ( inr x)
+    ( inl (inr y)) =
+    pasting-scheme-Globular-Type S
+  1-cell-globular-type-Globular-Type
+    ( pasting-scheme-Globular-Type
+      ( make-listed-plane-tree (cons S (cons T ℓ))))
+    ( inr x)
+    ( inr y) =
+    empty-Globular-Type
+```