Large symmetric globular types

Content created by Fredrik Bakke.

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

{-# OPTIONS --guardedness #-}

module structured-types.large-symmetric-globular-types where
Imports 
open import foundation.large-binary-relations
open import foundation.universe-levels

open import structured-types.large-globular-types
open import structured-types.symmetric-globular-types

Idea

We say a large globular type is symmetric if there is a symmetry action on its -cells for positive , mapping -cells from x to y to -cells from y to x.

Definition

Symmetry structure on a large globular structure

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

open is-symmetric-large-globular-structure public

module _
  {α : Level → Level} {β : Level → Level → Level}
  {A : (l : Level) → UU (α l)}
  (G : large-globular-structure β A)
  (r : is-symmetric-large-globular-structure G)
  where

  sym-1-cell-is-symmetric-large-globular-structure :
    {l1 l2 : Level} {x : A l1} {y : A l2} →
    1-cell-large-globular-structure G x y →
    1-cell-large-globular-structure G y x
  sym-1-cell-is-symmetric-large-globular-structure {x = x} {y} =
    is-symmetric-1-cell-is-symmetric-large-globular-structure r x y

  sym-2-cell-is-symmetric-large-globular-structure :
    {l1 l2 : Level} {x : A l1} {y : A l2}
    {f g : 1-cell-large-globular-structure G x y} →
    2-cell-large-globular-structure G f g →
    2-cell-large-globular-structure G g f
  sym-2-cell-is-symmetric-large-globular-structure {x = x} {y} {f} {g} =
    is-symmetric-1-cell-is-symmetric-globular-structure
      ( is-symmetric-globular-structure-1-cell-is-symmetric-large-globular-structure
        ( r)
        ( x)
        ( y))
      ( f)
      ( g)

Recent changes