Globular pasting diagrams #1671
Conversation
| 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). |
There was a problem hiding this comment.
Could you elaborate on what you mean by "internal definition" here?
There was a problem hiding this comment.
Is the following text more clear?
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.
There was a problem hiding this comment.
yes, that's indeed more clear
There was a problem hiding this comment.
This name seems reasonable. A reference you might add is this one, which seems to be the first publication where Batanin uses these systems
It'd be nice if you explained that the term "Batanin system" comes from the fact that it is a model of a batanin tree in a globular type, i.e., a "labeled batanin tree".
I also like the reference
In Proposition 8.1.1 it is demonstrated that batanin trees are equivalent to globular pasting diagrams/*schemes.
| ## Idea | ||
|
|
||
| A | ||
| {{#concept "globular pasting diamgram" Disambiguation="globular types" Agda=pasting-diagram-Globular-Type}} |
There was a problem hiding this comment.
| {{#concept "globular pasting diamgram" Disambiguation="globular types" Agda=pasting-diagram-Globular-Type}} | |
| {{#concept "globular pasting diagram" Disambiguation="globular types" Agda=pasting-diagram-Globular-Type}} |
| ``` | ||
|
|
||
| The | ||
| {{#concept "globular pasting scheme" Disambiguation="globular type" Agda=pasting-scheme-Globular-Type}} |
There was a problem hiding this comment.
In section 8.1 https://arxiv.org/pdf/math/0305049 Leinster refers to these as globular pasting diagrams. Although, I do like your naming choice, since it is transferrable to how we view functors F : C -> D as C-diagrams in D.
| - 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`. |
There was a problem hiding this comment.
I think some information is missing about the connection between S and x₀ and x₁
There was a problem hiding this comment.
and ℓ... I'm struggling to parse what is meant here
| {{#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 |
There was a problem hiding this comment.
| [globular map](globular-types.globular-maps.md) from G to the globular type of | |
| [globular map](globular-types.globular-maps.md) from `G` to the globular type of |
| The | ||
| {{#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). |
There was a problem hiding this comment.
This file presents the standard model of the n-sphere, but it is not the only model and these are not equivalent as globular types. A more accurate name might be "globular binary n-sphere" or "boundary of globular n-disk". I'd also be content with reserving "globular n-sphere" for the present concept, but it would be worthwhile to explain what the intended interpretation is.
fredrik-bakke
left a comment
fredrik-bakke
left a comment
There was a problem hiding this comment.
I'm happy with the naming choices in this PR, but some references are in order. I think we should keep the name "globular pasting scheme", but note the discrepancy with the literature.
| module _ | ||
| where |
There was a problem hiding this comment.
Since this module is empty it can be removed
| ( pasting-scheme-Globular-Type | ||
| ( make-listed-plane-tree (cons S (cons T ℓ)))) | ||
| ( inr x) | ||
| ( inl (inl y)) = empty-Globular-Type |
There was a problem hiding this comment.
| ( inl (inl y)) = empty-Globular-Type | |
| ( inl (inl y)) = | |
| empty-Globular-Type |
2 participants
This pull request adds a tentative definition of pasting diagrams, defined inductively using listed plane trees.