# Large globular types

Content created by Fredrik Bakke, Egbert Rijke and Vojtěch Štěpančík.

Created on 2024-03-20.
Last modified on 2024-09-01.

{-# OPTIONS --guardedness #-}

module structured-types.large-globular-types where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import structured-types.globular-types


## Idea

A large globular type is a hierarchy of types indexed by universe levels, equipped with a large binary relation valued in globular types.

Thus, a large globular type consists of a base hierarchy of types indexed by universe levels A called the -cells, and for every pair of -cells, a type of -cells, and for every pair of -cells a type of -cells, and so on ad infinitum. For every pair of -cells s and t, there is a type of -cells from s to t, and we say the -cells have source s and target t.

The standard interpretation of the higher cells of a globular type is as arrows from their source to their target. For instance, given two -cells x and y, two -cells f and g from x to y, two -cells H and K from f to g, and a -cell α from H to K, a common depiction would be

             f
-------------
/   //     \\   \
/   //   α   \\   ∨
x  H|| ≡≡≡≡≡≡> ||K  y.
\   \\       //   ∧
\   V       V   /
-------------
g


## Definitions

### The structure of a large globular type

record
large-globular-structure
{α : Level → Level} (β : Level → Level → Level) (A : (l : Level) → UU (α l))
: UUω
where
field
1-cell-large-globular-structure :
{l1 l2 : Level} (x : A l1) (y : A l2) → UU (β l1 l2)
globular-structure-1-cell-large-globular-structure :
{l1 l2 : Level} (x : A l1) (y : A l2) →
globular-structure (β l1 l2) (1-cell-large-globular-structure x y)

open large-globular-structure public


#### Iterated projections for large globular structures

module _
{α : Level → Level} {β : Level → Level → Level}
{A : (l : Level) → UU (α l)}
(G : large-globular-structure β A)
{l1 l2 : Level} {x : A l1} {y : A l2}
(f g : 1-cell-large-globular-structure G x y)
where

2-cell-large-globular-structure : UU (β l1 l2)
2-cell-large-globular-structure =
1-cell-globular-structure
( globular-structure-1-cell-large-globular-structure G x y) f g

globular-structure-2-cell-large-globular-structure :
globular-structure (β l1 l2) 2-cell-large-globular-structure
globular-structure-2-cell-large-globular-structure =
globular-structure-1-cell-globular-structure
( globular-structure-1-cell-large-globular-structure G x y) f g

module _
{α : Level → Level} {β : Level → Level → Level}
{A : (l : Level) → UU (α l)}
(G : large-globular-structure β A)
{l1 l2 : Level} {x : A l1} {y : A l2}
{f g : 1-cell-large-globular-structure G x y}
(p q : 2-cell-large-globular-structure G f g)
where

3-cell-large-globular-structure : UU (β l1 l2)
3-cell-large-globular-structure =
1-cell-globular-structure
( globular-structure-2-cell-large-globular-structure G f g) p q

globular-structure-3-cell-large-globular-structure :
globular-structure (β l1 l2) 3-cell-large-globular-structure
globular-structure-3-cell-large-globular-structure =
globular-structure-1-cell-globular-structure
( globular-structure-2-cell-large-globular-structure G f g) p q

module _
{α : Level → Level} {β : Level → Level → Level}
{A : (l : Level) → UU (α l)}
(G : large-globular-structure β A)
{l1 l2 : Level} {x : A l1} {y : A l2}
{f g : 1-cell-large-globular-structure G x y}
{p q : 2-cell-large-globular-structure G f g}
(H K : 3-cell-large-globular-structure G p q)
where

4-cell-large-globular-structure : UU (β l1 l2)
4-cell-large-globular-structure =
1-cell-globular-structure
( globular-structure-3-cell-large-globular-structure G p q) H K

globular-structure-4-cell-large-globular-structure :
globular-structure (β l1 l2) 4-cell-large-globular-structure
globular-structure-4-cell-large-globular-structure =
globular-structure-1-cell-globular-structure
( globular-structure-3-cell-large-globular-structure G p q) H K


### The type of large globular types

record
Large-Globular-Type (α : Level → Level) (β : Level → Level → Level) : UUω
where
field
0-cell-Large-Globular-Type :
(l : Level) → UU (α l)
globular-structure-0-cell-Large-Globular-Type :
large-globular-structure β 0-cell-Large-Globular-Type

open Large-Globular-Type public

module _
{α : Level → Level} {β : Level → Level → Level} (A : Large-Globular-Type α β)
where

1-cell-Large-Globular-Type :
{l1 l2 : Level}
(x : 0-cell-Large-Globular-Type A l1)
(y : 0-cell-Large-Globular-Type A l2) →
UU (β l1 l2)
1-cell-Large-Globular-Type =
1-cell-large-globular-structure
( globular-structure-0-cell-Large-Globular-Type A)

globular-structure-1-cell-Large-Globular-Type :
{l1 l2 : Level}
(x : 0-cell-Large-Globular-Type A l1)
(y : 0-cell-Large-Globular-Type A l2) →
globular-structure (β l1 l2) (1-cell-Large-Globular-Type x y)
globular-structure-1-cell-Large-Globular-Type =
globular-structure-1-cell-large-globular-structure
( globular-structure-0-cell-Large-Globular-Type A)

globular-type-1-cell-Large-Globular-Type :
{l1 l2 : Level}
(x : 0-cell-Large-Globular-Type A l1)
(y : 0-cell-Large-Globular-Type A l2) →
Globular-Type (β l1 l2) (β l1 l2)
globular-type-1-cell-Large-Globular-Type x y =
( 1-cell-Large-Globular-Type x y ,
globular-structure-1-cell-Large-Globular-Type x y)

2-cell-Large-Globular-Type :
{l1 l2 : Level}
{x : 0-cell-Large-Globular-Type A l1}
{y : 0-cell-Large-Globular-Type A l2}
(p q : 1-cell-Large-Globular-Type x y) → UU (β l1 l2)
2-cell-Large-Globular-Type {x = x} {y} =
1-cell-globular-structure
( globular-structure-1-cell-Large-Globular-Type x y)

globular-structure-2-cell-Large-Globular-Type :
{l1 l2 : Level}
{x : 0-cell-Large-Globular-Type A l1}
{y : 0-cell-Large-Globular-Type A l2}
(f g : 1-cell-Large-Globular-Type x y) →
globular-structure (β l1 l2) (2-cell-Large-Globular-Type f g)
globular-structure-2-cell-Large-Globular-Type =
globular-structure-2-cell-large-globular-structure
( globular-structure-0-cell-Large-Globular-Type A)

globular-type-2-cell-Large-Globular-Type :
{l1 l2 : Level}
{x : 0-cell-Large-Globular-Type A l1}
{y : 0-cell-Large-Globular-Type A l2}
(f g : 1-cell-Large-Globular-Type x y) →
Globular-Type (β l1 l2) (β l1 l2)
globular-type-2-cell-Large-Globular-Type f g =
( 2-cell-Large-Globular-Type f g ,
globular-structure-2-cell-Large-Globular-Type f g)

3-cell-Large-Globular-Type :
{l1 l2 : Level}
{x : 0-cell-Large-Globular-Type A l1}
{y : 0-cell-Large-Globular-Type A l2}
{p q : 1-cell-Large-Globular-Type x y}
(H K : 2-cell-Large-Globular-Type p q) → UU (β l1 l2)
3-cell-Large-Globular-Type {x = x} {y} =
2-cell-globular-structure
( globular-structure-1-cell-Large-Globular-Type x y)