agda-unimath/src/globular-types/globular-disks.lagda.md at 3422cc5e8b47d7dd8027cdb8ec126950c7770f59 · UniMath/agda-unimath · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
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)
```