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
- 2024-03-20. Fredrik Bakke. Globular types (#1084).