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

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

Idea

Consider two globular types G and H, and a binary family

  K : G₀ → H₀ → Globular-Type

of globular types, indexed over the 0-cells of G and H. Furthermore, consider a binary dependent 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 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 globular types

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

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

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

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

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

Recent changes