The globular type of 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-functions where
Imports 
open import foundation.globular-type-of-dependent-functions
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 functions is the globular type consisting of functions and homotopies between them. Since functions are dependent functions of constant type families, we define the globular type of functions in terms of the globular type of dependent functions.

The globular type of 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 large category of types.

Definitions

The globular type of functions

function-type-Globular-Type :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) →
  Globular-Type (l1 ⊔ l2) (l1 ⊔ l2)
function-type-Globular-Type A B =
  dependent-function-type-Globular-Type A (λ _ → B)

Properties

The globular type of functions is reflexive

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

function-type-Reflexive-Globular-Type :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) →
  Reflexive-Globular-Type (l1 ⊔ l2) (l1 ⊔ l2)
function-type-Reflexive-Globular-Type A B =
  dependent-function-type-Reflexive-Globular-Type A (λ _ → B)

The globular type of functions is transitive

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

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

See also

Recent changes