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
Imports 
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

Idea

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.

Definitions

Small pointed types

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

  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)
  where

  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)
  where

  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 :
    type-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

Properties

Being pointed small is a property

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

  is-prop-is-pointed-small-Pointed-Type :
    is-prop (is-pointed-small-Pointed-Type l2 X)
  is-prop-is-pointed-small-Pointed-Type =
    is-prop-has-element
      ( λ (Y , e) →
        is-prop-equiv'
          ( 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)
  where

  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)
  where

  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))) =
    Y
  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))) =
    e
  pr2 (pr2 (is-pointed-small-is-small-Pointed-Type (Y , e))) =
    refl

  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