The globular type of functions

Content created by Egbert Rijke.

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

{-# 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 wild higher precategory.

The structures defined in this file are used to define the noncoherent large wild higher precategory 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