Small pointed types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-03-23.
Last modified on 2024-04-11.

module structured-types.small-pointed-types where
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.small-types
open import foundation.universe-levels

open import structured-types.pointed-equivalences
open import structured-types.pointed-types


A pointed type is said to be small is its underlying type is small. Equivalently, we say that a pointed type is pointed small if it comes equipped with an element of type

  Σ (Y : Pointed-Type l), X ≃∗ Y

The difference between small pointed types and pointed small pointed types is that the notion of small pointed type is unpointed, and therefore potentially easier to establish. It is immediate that a pointed small type is small. For the converse, note that if X is small, and Y : 𝒰 comes equipped with an equivalence e : type-Pointed-Type X ≃ Y, then we take e * : Y to be the base point, and it is immediate that e is a pointed equivalence.


Small pointed types

module _
  {l1 : Level} (l2 : Level) (X : Pointed-Type l1)

  is-small-prop-Pointed-Type : Prop (l1  lsuc l2)
  is-small-prop-Pointed-Type = is-small-Prop l2 (type-Pointed-Type X)

  is-small-Pointed-Type : UU (l1  lsuc l2)
  is-small-Pointed-Type = is-small l2 (type-Pointed-Type X)

  is-prop-is-small-Pointed-Type : is-prop is-small-Pointed-Type
  is-prop-is-small-Pointed-Type = is-prop-is-small l2 (type-Pointed-Type X)

Pointedly small types

module _
  {l1 : Level} (l2 : Level) (X : Pointed-Type l1)

  is-pointed-small-Pointed-Type : UU (l1  lsuc l2)
  is-pointed-small-Pointed-Type =
    Σ (Pointed-Type l2)  Y  X ≃∗ Y)

module _
  {l1 l2 : Level} (X : Pointed-Type l1)
  (H : is-pointed-small-Pointed-Type l2 X)

  pointed-type-is-pointed-small-Pointed-Type : Pointed-Type l2
  pointed-type-is-pointed-small-Pointed-Type = pr1 H

  type-is-pointed-small-Pointed-Type : UU l2
  type-is-pointed-small-Pointed-Type =
    type-Pointed-Type pointed-type-is-pointed-small-Pointed-Type

  point-is-pointed-small-Pointed-Type :
  point-is-pointed-small-Pointed-Type =
    point-Pointed-Type pointed-type-is-pointed-small-Pointed-Type

  pointed-equiv-is-pointed-small-Pointed-Type :
    X ≃∗ pointed-type-is-pointed-small-Pointed-Type
  pointed-equiv-is-pointed-small-Pointed-Type = pr2 H

  equiv-is-pointed-small-Pointed-Type :
    type-Pointed-Type X  type-is-pointed-small-Pointed-Type
  equiv-is-pointed-small-Pointed-Type =
    equiv-pointed-equiv pointed-equiv-is-pointed-small-Pointed-Type


Being pointed small is a property

module _
  {l1 l2 : Level} (X : Pointed-Type l1)

  is-prop-is-pointed-small-Pointed-Type :
    is-prop (is-pointed-small-Pointed-Type l2 X)
  is-prop-is-pointed-small-Pointed-Type =
      ( λ (Y , e) 
          ( equiv-tot  Z  equiv-comp-pointed-equiv' e))
          ( is-prop-is-contr (is-torsorial-pointed-equiv Y)))

module _
  {l1 : Level} (l2 : Level) (X : Pointed-Type l1)

  is-pointed-small-prop-Pointed-Type : Prop (l1  lsuc l2)
  pr1 is-pointed-small-prop-Pointed-Type =
    is-pointed-small-Pointed-Type l2 X
  pr2 is-pointed-small-prop-Pointed-Type =
    is-prop-is-pointed-small-Pointed-Type X

A pointed type is small if and only if it is pointed small

module _
  {l1 l2 : Level} (X : Pointed-Type l1)

  is-pointed-small-is-small-Pointed-Type :
    is-small-Pointed-Type l2 X  is-pointed-small-Pointed-Type l2 X
  pr1 (pr1 (is-pointed-small-is-small-Pointed-Type (Y , e))) =
  pr2 (pr1 (is-pointed-small-is-small-Pointed-Type (Y , e))) =
    map-equiv e (point-Pointed-Type X)
  pr1 (pr2 (is-pointed-small-is-small-Pointed-Type (Y , e))) =
  pr2 (pr2 (is-pointed-small-is-small-Pointed-Type (Y , e))) =

  is-small-is-pointed-small-Pointed-Type :
    is-pointed-small-Pointed-Type l2 X  is-small-Pointed-Type l2 X
  pr1 (is-small-is-pointed-small-Pointed-Type (Y , e)) =
    type-Pointed-Type Y
  pr2 (is-small-is-pointed-small-Pointed-Type (Y , e)) =
    equiv-pointed-equiv e

Recent changes