Fibers of globular maps

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

module globular-types.fibers-globular-maps where
Imports 
open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.identity-types
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 globular map f : H → G between two globular types H and G. The fiber of f is a dependent globular type fib_f given by

  (fib_f)₀ x := fib f₀ x
  (fib_f)' (y , refl) (y' , refl) := fib_f'.

Definitions

The fiber of a globular map

fiber-globular-map :
  {l1 l2 l3 l4 : Level}
  (H : Globular-Type l1 l2) (G : Globular-Type l3 l4)
  (f : globular-map H G) →
  Dependent-Globular-Type (l1 ⊔ l3) (l2 ⊔ l4) G
0-cell-Dependent-Globular-Type
  ( fiber-globular-map H G f) =
  fiber (0-cell-globular-map f)
1-cell-dependent-globular-type-Dependent-Globular-Type
  ( fiber-globular-map H G f) {x} {x'} (y , refl) (y' , refl) =
  fiber-globular-map
    ( 1-cell-globular-type-Globular-Type H y y')
    ( 1-cell-globular-type-Globular-Type G _ _)
    ( 1-cell-globular-map-globular-map f)

Recent changes