The unit globular type

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

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

open import globular-types.constant-globular-types
open import globular-types.globular-types

Idea

The unit globular type is the constant globular type at the unit type. That is, the unit globular type is the globular type 𝟏 given by

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

Definitions

The unit globular type

unit-Globular-Type : Globular-Type lzero lzero
unit-Globular-Type = constant-Globular-Type unit

Recent changes