The unit reflexive globular type

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

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

open import globular-types.reflexive-globular-types
open import globular-types.unit-globular-type

Idea

The unit reflexive globular type is the reflexive globular type 𝟏 given by

  𝟏₀ := unit
  𝟏' x y := 𝟏
  refl 𝟏 x := star.

Definitions

The unit reflexive globular type

is-reflexive-unit-Globular-Type :
  is-reflexive-Globular-Type unit-Globular-Type
is-reflexive-1-cell-is-reflexive-Globular-Type
  is-reflexive-unit-Globular-Type x =
  star
is-reflexive-1-cell-globular-type-is-reflexive-Globular-Type
  is-reflexive-unit-Globular-Type =
  is-reflexive-unit-Globular-Type

unit-Reflexive-Globular-Type : Reflexive-Globular-Type lzero lzero
globular-type-Reflexive-Globular-Type unit-Reflexive-Globular-Type =
  unit-Globular-Type
refl-Reflexive-Globular-Type unit-Reflexive-Globular-Type =
  is-reflexive-unit-Globular-Type

Recent changes