The pointed unit type

Content created by Fredrik Bakke and maybemabeline.

Created on 2023-05-03.
Last modified on 2023-10-31.

module structured-types.pointed-unit-type where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.unit-type
open import foundation.universe-levels

open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types

Idea

The pointed unit type is the initial pointed type.

Definition

unit-Pointed-Type : Pointed-Type lzero
pr1 unit-Pointed-Type = unit
pr2 unit-Pointed-Type = star

Properties

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

  terminal-pointed-map : X →∗ unit-Pointed-Type
  pr1 terminal-pointed-map _ = star
  pr2 terminal-pointed-map = refl

  map-terminal-pointed-map : type-Pointed-Type X → unit
  map-terminal-pointed-map =
    map-pointed-map {A = X} {B = unit-Pointed-Type}
      terminal-pointed-map

  inclusion-point-Pointed-Type :
    unit-Pointed-Type →∗ X
  pr1 inclusion-point-Pointed-Type = point (point-Pointed-Type X)
  pr2 inclusion-point-Pointed-Type = refl

  is-initial-unit-Pointed-Type :
    ( f : unit-Pointed-Type →∗ X) → f ~∗ inclusion-point-Pointed-Type
  pr1 (is-initial-unit-Pointed-Type f) _ = preserves-point-pointed-map f
  pr2 (is-initial-unit-Pointed-Type f) = inv right-unit

Recent changes