Base change of dependent globular types

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

module globular-types.base-change-dependent-globular-types where
Imports 
open import foundation.universe-levels

open import globular-types.dependent-globular-types
open import globular-types.globular-maps
open import globular-types.globular-types

Idea

Consider a dependent globular type H over G, and consider a globular map f : K → G. The base change of H along f is the dependent globular type f*H given by

  (f*H)₀ x := H₀ (f₀ x)
  (f*H)₁ y y' := H₁.

Definitions

base-change-Dependent-Globular-Type :
  {l1 l2 l3 l4 l5 l6 : Level}
  {G : Globular-Type l1 l2} {K : Globular-Type l3 l4}
  (f : globular-map K G) →
  Dependent-Globular-Type l5 l6 G → Dependent-Globular-Type l5 l6 K
0-cell-Dependent-Globular-Type
  ( base-change-Dependent-Globular-Type f H)
  ( x) =
  0-cell-Dependent-Globular-Type H (0-cell-globular-map f x)
1-cell-dependent-globular-type-Dependent-Globular-Type
  ( base-change-Dependent-Globular-Type f H) y y' =
  base-change-Dependent-Globular-Type
    ( 1-cell-globular-map-globular-map f)
    ( 1-cell-dependent-globular-type-Dependent-Globular-Type H y y')

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  {G : Globular-Type l1 l2} {K : Globular-Type l3 l4}
  (f : globular-map K G) (H : Dependent-Globular-Type l5 l6 G)
  where

  0-cell-base-change-Dependent-Globular-Type :
    0-cell-Globular-Type K → UU l5
  0-cell-base-change-Dependent-Globular-Type =
    0-cell-Dependent-Globular-Type (base-change-Dependent-Globular-Type f H)

  1-cell-dependent-globular-type-base-change-Dependent-Globular-Type :
    {x x' : 0-cell-Globular-Type K}
    (y : 0-cell-base-change-Dependent-Globular-Type x)
    (y' : 0-cell-base-change-Dependent-Globular-Type x') →
    Dependent-Globular-Type l6 l6
      ( 1-cell-globular-type-Globular-Type K x x')
  1-cell-dependent-globular-type-base-change-Dependent-Globular-Type =
    1-cell-dependent-globular-type-Dependent-Globular-Type
      ( base-change-Dependent-Globular-Type f H)

  1-cell-base-change-Dependent-Globular-Type :
    {x x' : 0-cell-Globular-Type K}
    (y : 0-cell-base-change-Dependent-Globular-Type x)
    (y' : 0-cell-base-change-Dependent-Globular-Type x') →
    1-cell-Globular-Type K x x' → UU l6
  1-cell-base-change-Dependent-Globular-Type =
    1-cell-Dependent-Globular-Type (base-change-Dependent-Globular-Type f H)

Recent changes