Extensions of types

Content created by Egbert Rijke.

Created on 2024-01-23.
Last modified on 2024-01-23.

module foundation.extensions-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

Idea

Consider a type X. An extension of X is an object in the coslice under X, i.e., it consists of a type Y and a map f : X → Y.

In the above definition of extensions of types our aim is to capture the most general concept of what it means to be an extension of a type. Similarly, in any category we would say that an extension of an object X consists of an object Y equipped with a morphism f : X → Y.

Our notion of extensions of types are not to be confused with extension types of cubical type theory or extension types of simplicial type theory.

Definitions

Extensions of types

extension-type : {l1 : Level} (l2 : Level) (X : UU l1) → UU (l1 ⊔ lsuc l2)
extension-type l2 X = Σ (UU l2) (λ Y → X → Y)

module _
  {l1 l2 : Level} {X : UU l1} (Y : extension-type l2 X)
  where

  type-extension-type : UU l2
  type-extension-type = pr1 Y

  inclusion-extension-type : X → type-extension-type
  inclusion-extension-type = pr2 Y

Recent changes