# Transitive globular types

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

Created on 2024-03-20.

{-# OPTIONS --guardedness #-}

module structured-types.transitive-globular-types where

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

open import structured-types.globular-types


## Idea

A transitive globular type is a globular type A equipped with a binary operator

  - * - : (𝑛+1)-Cell A y z → (𝑛+1)-Cell A x y → (𝑛+1)-Cell A x z


at every level .

Note. This is not established terminology and may change.

## Definition

### Transitivity structure on a globular type

record
is-transitive-globular-structure
{l1 l2 : Level} {A : UU l1} (G : globular-structure l2 A) : UU (l1 ⊔ l2)
where
coinductive
field
comp-1-cell-is-transitive-globular-structure :
{x y z : A} →
1-cell-globular-structure G y z →
1-cell-globular-structure G x y →
1-cell-globular-structure G x z

is-transitive-globular-structure-1-cell-is-transitive-globular-structure :
(x y : A) →
is-transitive-globular-structure
( globular-structure-1-cell-globular-structure G x y)

open is-transitive-globular-structure public

module _
{l1 l2 : Level} {A : UU l1} {G : globular-structure l2 A}
(r : is-transitive-globular-structure G)
where

comp-2-cell-is-transitive-globular-structure :
{x y : A} {f g h : 1-cell-globular-structure G x y} →
2-cell-globular-structure G g h →
2-cell-globular-structure G f g →
2-cell-globular-structure G f h
comp-2-cell-is-transitive-globular-structure {x} {y} =
comp-1-cell-is-transitive-globular-structure
( is-transitive-globular-structure-1-cell-is-transitive-globular-structure
( r)
( x)
( y))

is-transitive-globular-structure-2-cell-is-transitive-globular-structure :
{x y : A} (f g : 1-cell-globular-structure G x y) →
is-transitive-globular-structure
( globular-structure-2-cell-globular-structure G f g)
is-transitive-globular-structure-2-cell-is-transitive-globular-structure
{ x} {y} =
is-transitive-globular-structure-1-cell-is-transitive-globular-structure
( is-transitive-globular-structure-1-cell-is-transitive-globular-structure
( r)
( x)
( y))

comp-3-cell-is-transitive-globular-structure :
{x y : A} {f g : 1-cell-globular-structure G x y}
{H K L : 2-cell-globular-structure G f g} →
3-cell-globular-structure G K L →
3-cell-globular-structure G H K →
3-cell-globular-structure G H L
comp-3-cell-is-transitive-globular-structure {x} {y} {f} {g} =
comp-1-cell-is-transitive-globular-structure
( is-transitive-globular-structure-2-cell-is-transitive-globular-structure
( f)
( g))


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

transitive-globular-structure :
{l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2)
transitive-globular-structure l2 A =
Σ (globular-structure l2 A) (is-transitive-globular-structure)


### The type of transitive globular types

Transitive-Globular-Type : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Transitive-Globular-Type l1 l2 = Σ (UU l1) (transitive-globular-structure l2)


## Examples

### The transitive globular structure on a type given by its identity types

is-transitive-globular-structure-Id :
{l : Level} (A : UU l) →
is-transitive-globular-structure (globular-structure-Id A)
is-transitive-globular-structure-Id A =
λ where
.comp-1-cell-is-transitive-globular-structure
p q →
q ∙ p
.is-transitive-globular-structure-1-cell-is-transitive-globular-structure
x y →
is-transitive-globular-structure-Id (x ＝ y)

transitive-globular-structure-Id :
{l : Level} (A : UU l) → transitive-globular-structure l A
transitive-globular-structure-Id A =
( globular-structure-Id A , is-transitive-globular-structure-Id A)