Pointed types

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-05-07.
Last modified on 2023-09-13.

module structured-types.pointed-types where
open import foundation.dependent-pair-types
open import foundation.universe-levels


A pointed type is a type A equipped with an element a : A.


The universe of pointed types

Pointed-Type : (l : Level)  UU (lsuc l)
Pointed-Type l = Σ (UU l)  X  X)

module _
  {l : Level} (A : Pointed-Type l)

  type-Pointed-Type : UU l
  type-Pointed-Type = pr1 A

  point-Pointed-Type : type-Pointed-Type
  point-Pointed-Type = pr2 A

Evaluation at the base point

ev-point-Pointed-Type :
  {l1 l2 : Level} (A : Pointed-Type l1) {B : UU l2} 
  (type-Pointed-Type A  B)  B
ev-point-Pointed-Type A f = f (point-Pointed-Type A)

See also

Recent changes