Globular types

Content created by Egbert Rijke.

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

{-# OPTIONS --guardedness #-}

Modules in the globular types namespace

module globular-types where

open import globular-types.base-change-dependent-globular-types public
open import globular-types.base-change-dependent-reflexive-globular-types public
open import globular-types.binary-dependent-globular-types public
open import globular-types.binary-dependent-reflexive-globular-types public
open import globular-types.binary-globular-maps public
open import globular-types.colax-reflexive-globular-maps public
open import globular-types.colax-transitive-globular-maps public
open import globular-types.composition-structure-globular-types public
open import globular-types.constant-globular-types public
open import globular-types.dependent-globular-types public
open import globular-types.dependent-reflexive-globular-types public
open import globular-types.dependent-sums-globular-types public
open import globular-types.discrete-dependent-reflexive-globular-types public
open import globular-types.discrete-globular-types public
open import globular-types.discrete-reflexive-globular-types public
open import globular-types.empty-globular-types public
open import globular-types.equality-globular-types public
open import globular-types.exponentials-globular-types public
open import globular-types.fibers-globular-maps public
open import globular-types.globular-equivalences public
open import globular-types.globular-maps public
open import globular-types.globular-types public
open import globular-types.large-colax-reflexive-globular-maps public
open import globular-types.large-colax-transitive-globular-maps public
open import globular-types.large-globular-maps public
open import globular-types.large-globular-types public
open import globular-types.large-lax-reflexive-globular-maps public
open import globular-types.large-lax-transitive-globular-maps public
open import globular-types.large-reflexive-globular-maps public
open import globular-types.large-reflexive-globular-types public
open import globular-types.large-symmetric-globular-types public
open import globular-types.large-transitive-globular-maps public
open import globular-types.large-transitive-globular-types public
open import globular-types.lax-reflexive-globular-maps public
open import globular-types.lax-transitive-globular-maps public
open import globular-types.points-globular-types public
open import globular-types.points-reflexive-globular-types public
open import globular-types.pointwise-extensions-binary-families-globular-types public
open import globular-types.pointwise-extensions-binary-families-reflexive-globular-types public
open import globular-types.pointwise-extensions-families-globular-types public
open import globular-types.pointwise-extensions-families-reflexive-globular-types public
open import globular-types.products-families-of-globular-types public
open import globular-types.reflexive-globular-equivalences public
open import globular-types.reflexive-globular-maps public
open import globular-types.reflexive-globular-types public
open import globular-types.sections-dependent-globular-types public
open import globular-types.superglobular-types public
open import globular-types.symmetric-globular-types public
open import globular-types.terminal-globular-types public
open import globular-types.transitive-globular-maps public
open import globular-types.transitive-globular-types public
open import globular-types.unit-globular-type public
open import globular-types.unit-reflexive-globular-type public
open import globular-types.universal-globular-type public
open import globular-types.universal-reflexive-globular-type public

Recent changes