Reflexive globular types

Content created by Fredrik Bakke.

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

{-# OPTIONS --guardedness #-}

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

open import structured-types.globular-types

Idea

A globular type is reflexive if every -cell x comes with a choice of -cell from x to x.

Definition

Reflexivity structure on a globular structure

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

open is-reflexive-globular-structure public

module _
  {l : Level} {A : UU l} {G : globular-structure A}
  (r : is-reflexive-globular-structure G)
  where

  refl-1-cell-is-reflexive-globular-structure :
    {x : A} → 1-cell-globular-structure G x x
  refl-1-cell-is-reflexive-globular-structure {x} =
    is-reflexive-1-cell-is-reflexive-globular-structure r x

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

The type of reflexive globular structures

reflexive-globular-structure : {l : Level} (A : UU l) → UU (lsuc l)
reflexive-globular-structure A =
  Σ (globular-structure A) (is-reflexive-globular-structure)

Examples

The reflexive globular structure on a type given by its identity types

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

Recent changes