# Large transitive globular types

```agda
{-# OPTIONS --guardedness #-}

module structured-types.large-transitive-globular-types where
```

<details><summary>Imports</summary>

```agda
open import foundation.universe-levels

open import structured-types.large-globular-types
open import structured-types.transitive-globular-types
```

</details>

## Idea

A
{{#concept "large transitive globular type" Agda=Large-Transitive-Globular-Type}}
is a [large globular type](structured-types.large-globular-types.md) `A`
[equipped](foundation.structure.md) with a binary operator

```text
  - * - : (š‘›+1)-Cell A y z ā†’ (š‘›+1)-Cell A x y ā†’ (š‘›+1)-Cell A x z
```

at every level $n$.

## Definition

### The structure transitivitiy on a large globular type

```agda
record
  is-transitive-large-globular-structure
  {Ī± : Level ā†’ Level} {Ī² : Level ā†’ Level ā†’ Level}
  {A : (l : Level) ā†’ UU (Ī± l)}
  (G : large-globular-structure Ī² A) : UUĻ‰
  where

  field
    comp-1-cell-is-transitive-large-globular-structure :
      {l1 l2 l3 : Level} {x : A l1} {y : A l2} {z : A l3} ā†’
      1-cell-large-globular-structure G y z ā†’
      1-cell-large-globular-structure G x y ā†’
      1-cell-large-globular-structure G x z

    is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure :
      {l1 l2 : Level} (x : A l1) (y : A l2) ā†’
      is-transitive-globular-structure
        ( globular-structure-1-cell-large-globular-structure G x y)

open is-transitive-large-globular-structure public

module _
  {Ī± : Level ā†’ Level} {Ī² : Level ā†’ Level ā†’ Level}
  {A : (l : Level) ā†’ UU (Ī± l)}
  {G : large-globular-structure Ī² A}
  (r : is-transitive-large-globular-structure G)
  where

  comp-2-cell-is-transitive-large-globular-structure :
    {l1 l2 : Level} {x : A l1} {y : A l2}
    {f g h : 1-cell-large-globular-structure G x y} ā†’
    2-cell-large-globular-structure G g h ā†’
    2-cell-large-globular-structure G f g ā†’
    2-cell-large-globular-structure G f h
  comp-2-cell-is-transitive-large-globular-structure {x = x} {y} =
    comp-1-cell-is-transitive-globular-structure
      ( is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure
        ( r)
        ( x)
        ( y))

  comp-3-cell-is-transitive-large-globular-structure :
    {l1 l2 : Level} {x : A l1} {y : A l2}
    {f g : 1-cell-large-globular-structure G x y}
    {H K L : 2-cell-large-globular-structure G f g} ā†’
    3-cell-large-globular-structure G K L ā†’
    3-cell-large-globular-structure G H K ā†’
    3-cell-large-globular-structure G H L
  comp-3-cell-is-transitive-large-globular-structure {x = x} {y} =
    comp-2-cell-is-transitive-globular-structure
      ( is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure
        ( r)
        ( x)
        ( y))
```

### The type of transitive globular structures on a large type

```agda
record
  large-transitive-globular-structure
  {Ī± : Level ā†’ Level} (Ī² : Level ā†’ Level ā†’ Level) (A : (l : Level) ā†’ UU (Ī± l))
  : UUĻ‰
  where

  field
    large-globular-structure-large-transitive-globular-structure :
      large-globular-structure Ī² A

    is-transitive-large-globular-structure-large-transitive-globular-structure :
      is-transitive-large-globular-structure
        ( large-globular-structure-large-transitive-globular-structure)

open large-transitive-globular-structure public
```

### The type of large transitive globular types

```agda
record
  Large-Transitive-Globular-Type
  (Ī± : Level ā†’ Level) (Ī² : Level ā†’ Level ā†’ Level) : UUĻ‰
  where

  field
    0-cell-Large-Transitive-Globular-Type : (l : Level) ā†’ UU (Ī± l)

    transitive-globular-structure-0-cell-Large-Transitive-Globular-Type :
      large-transitive-globular-structure
        ( Ī²)
        ( 0-cell-Large-Transitive-Globular-Type)

open Large-Transitive-Globular-Type public
```