Constant globular types

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

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

open import globular-types.globular-types

Idea

Consider a type A. The constant globular type at A is the globular type 𝐀 given by

  𝐀₀ := A
  𝐀₁ x y := 𝐀.

Definitions

The constant globular type at a type

module _
  {l : Level} (A : UU l)
  where

  constant-Globular-Type : Globular-Type l l
  0-cell-Globular-Type constant-Globular-Type =
    A
  1-cell-globular-type-Globular-Type constant-Globular-Type x y =
    constant-Globular-Type

Recent changes