Exponentials of globular types

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

module globular-types.exponentials-globular-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import globular-types.globular-maps
open import globular-types.globular-types
open import globular-types.products-families-of-globular-types

Idea

Consider a family G : I → Globular-Type of globular types indexed by a type I. We construct a globular type Π_I G.

Definitions

Exponentials of globular types

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

  0-cell-exponential-Globular-Type : UU (l1 ⊔ l2)
  0-cell-exponential-Globular-Type =
    0-cell-indexed-product-Globular-Type (λ (x : A) → G)

  1-cell-exponential-Globular-Type :
    (x y : 0-cell-exponential-Globular-Type) → UU (l1 ⊔ l3)
  1-cell-exponential-Globular-Type =
    1-cell-indexed-product-Globular-Type (λ (x : A) → G)

  exponential-Globular-Type : Globular-Type (l1 ⊔ l2) (l1 ⊔ l3)
  exponential-Globular-Type = indexed-product-Globular-Type (λ (x : A) → G)

Double exponentials of globular types

module _
  {l1 l2 l3 l4 : Level} (A : UU l1) (B : UU l2) (G : Globular-Type l3 l4)
  where

  0-cell-double-exponential-Globular-Type : UU (l1 ⊔ l2 ⊔ l3)
  0-cell-double-exponential-Globular-Type =
    0-cell-double-indexed-product-Globular-Type (λ (x : A) (y : B) → G)

  1-cell-double-exponential-Globular-Type :
    (x y : 0-cell-double-exponential-Globular-Type) → UU (l1 ⊔ l2 ⊔ l4)
  1-cell-double-exponential-Globular-Type =
    1-cell-double-indexed-product-Globular-Type (λ (x : A) (y : B) → G)

  double-exponential-Globular-Type : Globular-Type (l1 ⊔ l2 ⊔ l3) (l1 ⊔ l2 ⊔ l4)
  double-exponential-Globular-Type =
    double-indexed-product-Globular-Type (λ (x : A) (y : B) → G)

Evaluating globular maps into exponentials of globular types

ev-hom-exponential-Globular-Type :
  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
  {G : Globular-Type l2 l3} {H : Globular-Type l4 l5}
  (f : globular-map G (exponential-Globular-Type I H)) →
  I → globular-map G H
ev-hom-exponential-Globular-Type = ev-hom-indexed-product-Globular-Type

Binding families of globular maps

bind-family-globular-maps :
  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
  {G : Globular-Type l2 l3} {H : Globular-Type l4 l5}
  (f : I → globular-map G H) → globular-map G (exponential-Globular-Type I H)
bind-family-globular-maps = bind-indexed-family-globular-maps

Recent changes