Lifts of types

Content created by Egbert Rijke and Fredrik Bakke.

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

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

Idea

Consider a type X. A lift of X is an object in the slice over X, i.e., it consists of a type Y and a map f : Y → X.

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

Definitions

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

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

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

  projection-lift-type : type-lift-type → X
  projection-lift-type = pr2 Y

Recent changes