Pointwise extensions of binary 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-binary-families-reflexive-globular-types
  where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import globular-types.binary-dependent-reflexive-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 two reflexive globular types G and H, and a binary family

  K : G₀ → H₀ → Reflexive-Globular-Type

of reflexive globular types, indexed over the 0-cells of G and H. Furthermore, consider a binary dependent reflexive globular type L over G and H. We say that L is a pointwise extension of K if it comes equipped with a family of reflexive globular equivalences

  (x : point G) (y : point H) → ev-point L x y ≃ K x₀ y₀.

Definitions

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

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

  is-pointwise-extension-binary-family-reflexive-globular-types :
    UU (l1 ⊔ l3 ⊔ l5 ⊔ l6 ⊔ l7 ⊔ l8)
  is-pointwise-extension-binary-family-reflexive-globular-types =
    (x : point-Reflexive-Globular-Type G)
    (y : point-Reflexive-Globular-Type H) →
    reflexive-globular-equiv
      ( ev-point-Binary-Dependent-Reflexive-Globular-Type G H L x y)
      ( K x y)

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

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

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

Recent changes