Empty globular types

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

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

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

Idea

A globular type is said to be empty if its type of 0-cells is empty.

The standard empty globular type is defined to be the constant globular type at the empty type. That is, the standard empty globular type is the globular type 𝟎 given by

  𝟎₀ := ∅
  𝟎' x y := 𝟎.

Definitions

The predicate of being an empty globular type

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

  is-empty-Globular-Type : UU l1
  is-empty-Globular-Type = is-empty (0-cell-Globular-Type G)

The standard empty globular type

empty-Globular-Type : Globular-Type lzero lzero
empty-Globular-Type = constant-Globular-Type empty

Recent changes