The globular type of dependent functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-12-03.
Last modified on 2025-02-04.

{-# OPTIONS --guardedness #-}

module foundation.globular-type-of-dependent-functions where
Imports 
open import foundation.universe-levels

open import foundation-core.homotopies

open import globular-types.globular-types
open import globular-types.reflexive-globular-types
open import globular-types.transitive-globular-types

Idea

The globular type of dependent functions is the globular type consisting of dependent functions and homotopies between them. Since homotopies are themselves defined to be certain dependent functions, they directly provide a globular structure on dependent function types.

The globular type of dependent functions of a type family B over A is reflexive and transitive, so it is a noncoherent ω-precategory.

The structures defined in this file are used to define the wild category of types.

Definitions

The globular type of dependent functions

dependent-function-type-Globular-Type :
  {l1 l2 : Level} (A : UU l1) (B : A → UU l2) →
  Globular-Type (l1 ⊔ l2) (l1 ⊔ l2)
0-cell-Globular-Type (dependent-function-type-Globular-Type A B) =
  (x : A) → B x
1-cell-globular-type-Globular-Type
  ( dependent-function-type-Globular-Type A B) f g =
  dependent-function-type-Globular-Type A (eq-value f g)

Properties

The globular type of dependent functions is reflexive

is-reflexive-dependent-function-type-Globular-Type :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
  is-reflexive-Globular-Type (dependent-function-type-Globular-Type A B)
is-reflexive-1-cell-is-reflexive-Globular-Type
  is-reflexive-dependent-function-type-Globular-Type f =
  refl-htpy
is-reflexive-1-cell-globular-type-is-reflexive-Globular-Type
  is-reflexive-dependent-function-type-Globular-Type =
  is-reflexive-dependent-function-type-Globular-Type

dependent-function-type-Reflexive-Globular-Type :
  {l1 l2 : Level} (A : UU l1) (B : A → UU l2) →
  Reflexive-Globular-Type (l1 ⊔ l2) (l1 ⊔ l2)
globular-type-Reflexive-Globular-Type
  ( dependent-function-type-Reflexive-Globular-Type A B) =
  dependent-function-type-Globular-Type A B
refl-Reflexive-Globular-Type
  ( dependent-function-type-Reflexive-Globular-Type A B) =
  is-reflexive-dependent-function-type-Globular-Type

The globular type of dependent functions is transitive

is-transitive-dependent-function-type-Globular-Type :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
  is-transitive-Globular-Type (dependent-function-type-Globular-Type A B)
comp-1-cell-is-transitive-Globular-Type
  is-transitive-dependent-function-type-Globular-Type K H =
  H ∙h K
is-transitive-1-cell-globular-type-is-transitive-Globular-Type
  is-transitive-dependent-function-type-Globular-Type =
  is-transitive-dependent-function-type-Globular-Type

dependent-function-type-Transitive-Globular-Type :
  {l1 l2 : Level} (A : UU l1) (B : A → UU l2) →
  Transitive-Globular-Type (l1 ⊔ l2) (l1 ⊔ l2)
globular-type-Transitive-Globular-Type
  ( dependent-function-type-Transitive-Globular-Type A B) =
  dependent-function-type-Globular-Type A B
is-transitive-Transitive-Globular-Type
  ( dependent-function-type-Transitive-Globular-Type A B) =
  is-transitive-dependent-function-type-Globular-Type

See also

Recent changes