From e506e4c148db380695af4176c675f1a1995ae5b0 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Wed, 5 Nov 2025 15:27:25 -0500 Subject: [PATCH 1/5] globular disks and spheres --- src/globular-types/empty-globular-types.lagda.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/globular-types/empty-globular-types.lagda.md b/src/globular-types/empty-globular-types.lagda.md index 9e19f67f78..aadd187a68 100644 --- a/src/globular-types/empty-globular-types.lagda.md +++ 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 +``` From 27fde1ac81c64520104699baa637bc2446c54101 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 6 Nov 2025 14:24:54 -0500 Subject: [PATCH 2/5] globular pasting diagrams --- src/globular-types.lagda.md | 6 + .../batanin-systems-globular-types.lagda.md | 71 +++++++++ src/globular-types/globular-disks.lagda.md | 62 ++++++++ .../globular-pasting-diagrams.lagda.md | 43 ++++++ .../globular-pasting-schemes.lagda.md | 142 ++++++++++++++++++ src/globular-types/globular-spheres.lagda.md | 49 ++++++ .../globular-suspension.lagda.md | 68 +++++++++ 7 files changed, 441 insertions(+) create mode 100644 src/globular-types/batanin-systems-globular-types.lagda.md create mode 100644 src/globular-types/globular-disks.lagda.md create mode 100644 src/globular-types/globular-pasting-diagrams.lagda.md create mode 100644 src/globular-types/globular-pasting-schemes.lagda.md create mode 100644 src/globular-types/globular-spheres.lagda.md create mode 100644 src/globular-types/globular-suspension.lagda.md diff --git a/src/globular-types.lagda.md b/src/globular-types.lagda.md index 260995b614..dbd4aeeb15 100644 --- a/src/globular-types.lagda.md +++ b/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 diff --git a/src/globular-types/batanin-systems-globular-types.lagda.md b/src/globular-types/batanin-systems-globular-types.lagda.md new file mode 100644 index 0000000000..a8ca1f8791 --- /dev/null +++ b/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 +``` + +
Imports + +```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 +``` + +
+ +## Idea + +A +{{#concept "Batanin system" Disambiguation="globular types" Agda=batanin-system-Globular-Type}} +is an internal definition of a +[pasting diagram](globular-types.globular-pasting-diagrams.md) of +[globular types](globular-types.globular-types.md). + +## 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 +``` diff --git a/src/globular-types/globular-disks.lagda.md b/src/globular-types/globular-disks.lagda.md new file mode 100644 index 0000000000..a4ee5edaaa --- /dev/null +++ b/src/globular-types/globular-disks.lagda.md @@ -0,0 +1,62 @@ +# Globular disks + +```agda +{-# OPTIONS --guardedness #-} + +module globular-types.globular-disks where +``` + +
Imports + +```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 +``` + +
+ +## 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) +``` diff --git a/src/globular-types/globular-pasting-diagrams.lagda.md b/src/globular-types/globular-pasting-diagrams.lagda.md new file mode 100644 index 0000000000..b5752f35dd --- /dev/null +++ b/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 +``` + +
Imports + +```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 +``` + +
+ +## 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 +``` diff --git a/src/globular-types/globular-pasting-schemes.lagda.md b/src/globular-types/globular-pasting-schemes.lagda.md new file mode 100644 index 0000000000..f359ad4027 --- /dev/null +++ b/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 +``` + +
Imports + +```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 +``` + +
+ +## 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 +``` diff --git a/src/globular-types/globular-spheres.lagda.md b/src/globular-types/globular-spheres.lagda.md new file mode 100644 index 0000000000..ee00c0b597 --- /dev/null +++ b/src/globular-types/globular-spheres.lagda.md @@ -0,0 +1,49 @@ +# Globular spheres + +```agda +{-# OPTIONS --guardedness #-} + +module globular-types.globular-spheres where +``` + +
Imports + +```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 +``` + +
+ +## Idea + +The +{{#concept "globular `n`-sphere" Disambiguation="globular type" Agda=globular-disk}} +is a [globular type](globular-types.globular-types.md) defined by iterated +[globular suspension](globular-types.globular-suspension.md) of the +[empty globular type](globular-types.empty-globular-types.md). + +## Definitions + +### The globular `0`-sphere + +```agda +globular-0-sphere : + Globular-Type lzero lzero +globular-0-sphere = suspension-Globular-Type empty-Globular-Type +``` + +### The globular `n`-sphere + +```agda +globular-sphere : (n : ℕ) → Globular-Type lzero lzero +globular-sphere zero-ℕ = globular-0-sphere +globular-sphere (succ-ℕ n) = suspension-Globular-Type (globular-sphere n) +``` diff --git a/src/globular-types/globular-suspension.lagda.md b/src/globular-types/globular-suspension.lagda.md new file mode 100644 index 0000000000..07a378f7d9 --- /dev/null +++ b/src/globular-types/globular-suspension.lagda.md @@ -0,0 +1,68 @@ +# Globular suspension + +```agda +{-# OPTIONS --guardedness #-} + +module globular-types.globular-suspension where +``` + +
Imports + +```agda +open import foundation.universe-levels + +open import globular-types.empty-globular-types +open import globular-types.globular-types +``` + +
+ +## Idea + +The +{{#concept "globular suspension" Disambiguation="globular type" Agda="suspension-Globular-Type}} +of a [globular type](globular-types.globular-types.md) `G` is a globular type +`ΣG` with exactly two `0`-cells called north and south, and a +[globular map](globular-types.globular-maps.md) from G to the globular type of +`1`-cells from north to south in `ΣG`. + +## Definition + +### The suspension of globular sets of a fixed universe level `l1` + +Note: Allowing globular types with separate universe levels for 0-cells and +higher cells complicates the definition of suspension. + +```agda +module _ + {l1 : Level} (G : Globular-Type l1 l1) + where + + data 0-cell-suspension-Globular-Type : UU lzero where + north-suspension-Globular-Type : 0-cell-suspension-Globular-Type + south-suspension-Globular-Type : 0-cell-suspension-Globular-Type + + suspension-Globular-Type : Globular-Type lzero l1 + 0-cell-Globular-Type suspension-Globular-Type = + 0-cell-suspension-Globular-Type + 1-cell-globular-type-Globular-Type + suspension-Globular-Type + north-suspension-Globular-Type + north-suspension-Globular-Type = + raise-empty-Globular-Type l1 l1 + 1-cell-globular-type-Globular-Type + suspension-Globular-Type + north-suspension-Globular-Type + south-suspension-Globular-Type = + G + 1-cell-globular-type-Globular-Type + suspension-Globular-Type + south-suspension-Globular-Type + north-suspension-Globular-Type = + raise-empty-Globular-Type l1 l1 + 1-cell-globular-type-Globular-Type + suspension-Globular-Type + south-suspension-Globular-Type + south-suspension-Globular-Type = + raise-empty-Globular-Type l1 l1 +``` From d43933de96e74d3c1679aa3f84a1f74b929b3b91 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 6 Nov 2025 15:29:06 -0500 Subject: [PATCH 3/5] bugs --- src/globular-types/globular-spheres.lagda.md | 2 +- src/globular-types/globular-suspension.lagda.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/globular-types/globular-spheres.lagda.md b/src/globular-types/globular-spheres.lagda.md index ee00c0b597..0984a96b19 100644 --- a/src/globular-types/globular-spheres.lagda.md +++ b/src/globular-types/globular-spheres.lagda.md @@ -25,7 +25,7 @@ open import globular-types.globular-types ## Idea The -{{#concept "globular `n`-sphere" Disambiguation="globular type" Agda=globular-disk}} +{{#concept "globular `n`-sphere" Disambiguation="globular type" Agda=globular-sphere}} is a [globular type](globular-types.globular-types.md) defined by iterated [globular suspension](globular-types.globular-suspension.md) of the [empty globular type](globular-types.empty-globular-types.md). diff --git a/src/globular-types/globular-suspension.lagda.md b/src/globular-types/globular-suspension.lagda.md index 07a378f7d9..f2e45f664c 100644 --- a/src/globular-types/globular-suspension.lagda.md +++ b/src/globular-types/globular-suspension.lagda.md @@ -20,7 +20,7 @@ open import globular-types.globular-types ## Idea The -{{#concept "globular suspension" Disambiguation="globular type" Agda="suspension-Globular-Type}} +{{#concept "globular suspension" Disambiguation="globular type" Agda=suspension-Globular-Type}} of a [globular type](globular-types.globular-types.md) `G` is a globular type `ΣG` with exactly two `0`-cells called north and south, and a [globular map](globular-types.globular-maps.md) from G to the globular type of From f1970a0e78a22330fed618990a157010aeb0da0c Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 6 Nov 2025 15:29:46 -0500 Subject: [PATCH 4/5] types --- src/globular-types/globular-suspension.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/globular-types/globular-suspension.lagda.md b/src/globular-types/globular-suspension.lagda.md index f2e45f664c..6dfa4218f7 100644 --- a/src/globular-types/globular-suspension.lagda.md +++ b/src/globular-types/globular-suspension.lagda.md @@ -28,7 +28,7 @@ of a [globular type](globular-types.globular-types.md) `G` is a globular type ## Definition -### The suspension of globular sets of a fixed universe level `l1` +### The suspension of globular types of a fixed universe level `l1` Note: Allowing globular types with separate universe levels for 0-cells and higher cells complicates the definition of suspension. From 3422cc5e8b47d7dd8027cdb8ec126950c7770f59 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 6 Nov 2025 19:31:05 -0500 Subject: [PATCH 5/5] work --- src/globular-types/batanin-systems-globular-types.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/globular-types/batanin-systems-globular-types.lagda.md b/src/globular-types/batanin-systems-globular-types.lagda.md index a8ca1f8791..b3bdb3bd9e 100644 --- a/src/globular-types/batanin-systems-globular-types.lagda.md +++ b/src/globular-types/batanin-systems-globular-types.lagda.md @@ -27,9 +27,9 @@ open import trees.plane-trees A {{#concept "Batanin system" Disambiguation="globular types" Agda=batanin-system-Globular-Type}} -is an internal definition of a +is similar to a [pasting diagram](globular-types.globular-pasting-diagrams.md) of -[globular types](globular-types.globular-types.md). +[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