Discrete dependent reflexive globular types

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

module globular-types.discrete-dependent-reflexive-globular-types where
Imports 
open import foundation.universe-levels

open import globular-types.dependent-reflexive-globular-types
open import globular-types.discrete-reflexive-globular-types
open import globular-types.points-reflexive-globular-types
open import globular-types.reflexive-globular-types

Idea

A dependent reflexive globular type H over a reflexive globular type G is said to be discrete if the reflexive globular type

  ev-point H x

is discrete for every point of G.

Definitions

The predicate of being a discrete dependent reflexive globular type

module _
  {l1 l2 l3 l4 : Level} {G : Reflexive-Globular-Type l1 l2}
  (H : Dependent-Reflexive-Globular-Type l3 l4 G)
  where

  is-discrete-Dependent-Reflexive-Globular-Type : UU (l1 ⊔ l3 ⊔ l4)
  is-discrete-Dependent-Reflexive-Globular-Type =
    (x : point-Reflexive-Globular-Type G) →
    is-discrete-Reflexive-Globular-Type
      ( ev-point-Dependent-Reflexive-Globular-Type H x)

Recent changes