Terminal globular types

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

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

open import globular-types.globular-maps
open import globular-types.globular-types

Idea

A globular type G is said to be terminal if for any globular type H the type of globular maps H → G is contractible.

Definitions

The predicate of being a terminal globular type

is-terminal-Globular-Type :
  {l1 l2 : Level} → Globular-Type l1 l2 → UUω
is-terminal-Globular-Type G =
  {l3 l4 : Level} (H : Globular-Type l3 l4) → is-contr (globular-map H G)

Recent changes