Composition structure on globular types

Content created by Egbert Rijke.

Created on 2024-12-03.
Last modified on 2024-12-03.

{-# OPTIONS --guardedness #-}

module globular-types.composition-structure-globular-types where
Imports 
open import foundation.universe-levels

open import globular-types.binary-globular-maps
open import globular-types.globular-types

Idea

A composition structure on a globular type G consists of a binary globular map

  - ∘ - : G' y z → G' x y → G' x z,

and for any two 0-cells x y : G₀ a composition structure on the globular type G' x y of 1-cells of G. More explicitly, a composition structure consists of binary operations

  - ∘ - : (𝑛+1)-Cell G y z → (𝑛+1)-Cell G x y → (𝑛+1)-Cell G x z,

each of which preserve all higher cells of the globular type G. Globular composition structure is therefore a strengthening of the transitivity structure on globular types.

Definitions

Globular composition structure

record
  composition-Globular-Type
    {l1 l2 : Level} (G : Globular-Type l1 l2) : UU (l1 ⊔ l2)
  where
  coinductive

  field
    comp-binary-globular-map-composition-Globular-Type :
      {x y z : 0-cell-Globular-Type G} →
      binary-globular-map
        ( 1-cell-globular-type-Globular-Type G y z)
        ( 1-cell-globular-type-Globular-Type G x y)
        ( 1-cell-globular-type-Globular-Type G x z)

  field
    composition-1-cell-globular-type-Globular-Type :
      {x y : 0-cell-Globular-Type G} →
      composition-Globular-Type
        ( 1-cell-globular-type-Globular-Type G x y)

open composition-Globular-Type public

Recent changes