Pointwise extensions of families of reflexive globular types

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

module
  globular-types.pointwise-extensions-families-reflexive-globular-types
  where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

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

Idea

Consider a family of reflexive globular types H : G₀ → Reflexive-Globular-Type indexed by the 0-cells of a reflexive globular type G and consider a dependent reflexive globular type K over G. We say that K is a pointwise extension of H if it comes equipped with a family of reflexive globular equivalences

  ev-point K x ≃ H x₀

indexed by the points of G.

Definitions

The predicate of being a pointwise extension of a family of reflexive globular types

module _
  {l1 l2 l3 l4 l5 l6 : Level} {G : Reflexive-Globular-Type l1 l2}
  (H : 0-cell-Reflexive-Globular-Type G → Reflexive-Globular-Type l3 l4)
  (K : Dependent-Reflexive-Globular-Type l5 l6 G)
  where

  is-pointwise-extension-family-of-reflexive-globular-types-Dependent-Reflexive-Globular-Type :
    UU (l1 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
  is-pointwise-extension-family-of-reflexive-globular-types-Dependent-Reflexive-Globular-Type =
    (x : point-Reflexive-Globular-Type G) →
    reflexive-globular-equiv
      ( ev-point-Dependent-Reflexive-Globular-Type K x)
      ( H x)

The type of pointwise extensions of a family of reflexive globular types

module _
  {l1 l2 l3 l4 : Level} (l5 l6 : Level) (G : Reflexive-Globular-Type l1 l2)
  (H : 0-cell-Reflexive-Globular-Type G → Reflexive-Globular-Type l3 l4)
  where

  pointwise-extension-family-of-reflexive-globular-types :
    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6)
  pointwise-extension-family-of-reflexive-globular-types =
    Σ ( Dependent-Reflexive-Globular-Type l5 l6 G)
      ( is-pointwise-extension-family-of-reflexive-globular-types-Dependent-Reflexive-Globular-Type
        H)

Recent changes