Lifts of types (#1001)

In this pull request, dual to #999 I propose a definition of lifts of
types.

---------

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

src/foundation.lagda.md

@@ -201,6 +201,7 @@ open import foundation.large-locale-of-subtypes public
 open import foundation.law-of-excluded-middle public
 open import foundation.lawveres-fixed-point-theorem public
 open import foundation.lesser-limited-principle-of-omniscience public
+open import foundation.lifts-types public
 open import foundation.limited-principle-of-omniscience public
 open import foundation.locally-small-types public
 open import foundation.logical-equivalences public

src/foundation/lifts-types.lagda.md

@@ -0,0 +1,42 @@
+# Lifts of types
+
+```agda
+module foundation.lifts-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a type `X`. A {{#concept "lift" Disambiguation="type" Agda=lift-type}}
+of `X` is an object in the [slice](foundation.slice.md) 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](category-theory.categories.md) we would say that an lift of an object
+`X` consists of an object `Y` equipped with a morphism `f : Y → X`.
+
+## Definitions
+
+```agda
+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
+```