Discrete globular types

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

module globular-types.discrete-globular-types where

Imports

open import foundation.dependent-pair-types
open import foundation.discrete-binary-relations
open import foundation.propositions
open import foundation.universe-levels

open import globular-types.empty-globular-types
open import globular-types.globular-types

Idea

A globular type G is said to be discrete^¶ if it has no 1-cells, i.e., if the type G₁ x y of 1-cells from x to y in G is empty for any two 0-cells x y : G₀. In other words, a globular type is discrete if its binary relation is discrete.

The forgetful functor from globular types to types given by G ↦ G₀ has a left adjoint, mapping a type A to the globular type with the type A as its 0-cells and no edges. The image of this left adjoint is precisely the type of discrete globular types.

Note that the globular type obtained from a type and its iterated identity types is the standard discrete reflexive globular type.

Definitions

The predicate on globular types of being discrete

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

  is-discrete-prop-Globular-Type : Prop (l1 ⊔ l2)
  is-discrete-prop-Globular-Type =
    is-discrete-prop-Relation (1-cell-Globular-Type G)

  is-discrete-Globular-Type : UU (l1 ⊔ l2)
  is-discrete-Globular-Type = is-discrete-Relation (1-cell-Globular-Type G)

  is-prop-is-discrete-Globular-Type : is-prop is-discrete-Globular-Type
  is-prop-is-discrete-Globular-Type =
    is-prop-is-discrete-Relation (1-cell-Globular-Type G)