Globular types

Content created by Fredrik Bakke.

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

{-# OPTIONS --guardedness #-}

module structured-types.globular-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

Idea

A globular type is a type equipped with a binary relation valued in globular types.

Thus, a globular type consists of a base type A which is called the type of -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

We follow the conventional approach of the library and start by defining the globular structure on a type, and then define a globular type to be a type equipped with such structure. Note that we could equivalently have started by defining globular types, and then define globular structures on a type as binary families of globular types on it, but this is a special property of globular types.

Definitions

The structure of a globular type

record globular-structure {l : Level} (A : UU l) : UU (lsuc l)
  where
  coinductive
  field
    1-cell-globular-structure :
      (x y : A) → UU l
    globular-structure-1-cell-globular-structure :
      (x y : A) → globular-structure (1-cell-globular-structure x y)

open globular-structure public

Iterated projections for globular structures

module _
  {l : Level} {A : UU l} (G : globular-structure A)
  {x y : A} (f g : 1-cell-globular-structure G x y)
  where

  2-cell-globular-structure : UU l
  2-cell-globular-structure =
    1-cell-globular-structure
      ( globular-structure-1-cell-globular-structure G x y) f g

  globular-structure-2-cell-globular-structure :
    globular-structure 2-cell-globular-structure
  globular-structure-2-cell-globular-structure =
    globular-structure-1-cell-globular-structure
      ( globular-structure-1-cell-globular-structure G x y) f g

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

  3-cell-globular-structure : UU l
  3-cell-globular-structure =
    1-cell-globular-structure
      ( globular-structure-2-cell-globular-structure G f g) p q

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

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

  4-cell-globular-structure : UU l
  4-cell-globular-structure =
    1-cell-globular-structure
      ( globular-structure-3-cell-globular-structure G p q) H K

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

The type of globular types

Globular-Type : (l : Level) → UU (lsuc l)
Globular-Type l = Σ (UU l) globular-structure

module _
  {l : Level} (A : Globular-Type l)
  where

  0-cell-Globular-Type : UU l
  0-cell-Globular-Type = pr1 A

  globular-structure-0-cell-Globular-Type :
    globular-structure 0-cell-Globular-Type
  globular-structure-0-cell-Globular-Type = pr2 A

  1-cell-Globular-Type : (x y : 0-cell-Globular-Type) → UU l
  1-cell-Globular-Type =
    1-cell-globular-structure globular-structure-0-cell-Globular-Type

  globular-structure-1-cell-Globular-Type :
    (x y : 0-cell-Globular-Type) →
    globular-structure (1-cell-Globular-Type x y)
  globular-structure-1-cell-Globular-Type =
    globular-structure-1-cell-globular-structure
      ( globular-structure-0-cell-Globular-Type)

  globular-type-1-cell-Globular-Type :
    (x y : 0-cell-Globular-Type) → Globular-Type l
  globular-type-1-cell-Globular-Type x y =
    ( 1-cell-Globular-Type x y , globular-structure-1-cell-Globular-Type x y)

  2-cell-Globular-Type :
    {x y : 0-cell-Globular-Type} (f g : 1-cell-Globular-Type x y) → UU l
  2-cell-Globular-Type =
    2-cell-globular-structure globular-structure-0-cell-Globular-Type

  globular-structure-2-cell-Globular-Type :
    {x y : 0-cell-Globular-Type} (f g : 1-cell-Globular-Type x y) →
    globular-structure (2-cell-Globular-Type f g)
  globular-structure-2-cell-Globular-Type =
    globular-structure-2-cell-globular-structure
      ( globular-structure-0-cell-Globular-Type)

  globular-type-2-cell-Globular-Type :
    {x y : 0-cell-Globular-Type} (f g : 1-cell-Globular-Type x y) →
    Globular-Type l
  globular-type-2-cell-Globular-Type f g =
    ( 2-cell-Globular-Type f g , globular-structure-2-cell-Globular-Type f g)

Examples

The globular structure on a type given by its identity types

globular-structure-Id : {l : Level} (A : UU l) → globular-structure A
globular-structure-Id A =
  λ where
  .1-cell-globular-structure x y →
    x ＝ y
  .globular-structure-1-cell-globular-structure x y →
    globular-structure-Id (x ＝ y)

Recent changes