Points of reflexive globular types

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

module globular-types.points-reflexive-globular-types where
Imports 
open import foundation.universe-levels

open import globular-types.points-globular-types
open import globular-types.reflexive-globular-types

Idea

Consider a reflexive globular type G. A point of G is a 0-cell of G. Equivalently, a point of G is a reflexive globular map from the unit reflexive globular type into G.

The definition of points of reflexive globular types is much simpler than the definition of points of ordinary globular types. This is due to the condition that reflexive globular maps preserve reflexivity, and therefore the type of higher cells relating the underlying 0-cell to itself is contractible.

Definitions

Points of reflexive globular types

module _
  {l1 l2 : Level} (G : Reflexive-Globular-Type l1 l2)
  where

  point-Reflexive-Globular-Type : UU l1
  point-Reflexive-Globular-Type = 0-cell-Reflexive-Globular-Type G

The underlying points of the underlying globular type of a reflexive globular type

point-globular-type-point-Reflexive-Globular-Type :
  {l1 l2 : Level} (G : Reflexive-Globular-Type l1 l2) →
  point-Reflexive-Globular-Type G →
  point-Globular-Type (globular-type-Reflexive-Globular-Type G)
0-cell-point-Globular-Type
  ( point-globular-type-point-Reflexive-Globular-Type G x) =
  x
1-cell-point-point-Globular-Type
  ( point-globular-type-point-Reflexive-Globular-Type G x) =
  point-globular-type-point-Reflexive-Globular-Type
    ( 1-cell-reflexive-globular-type-Reflexive-Globular-Type G x x)
    ( refl-1-cell-Reflexive-Globular-Type G)

Recent changes