Pointed torsorial type families

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, fernabnor and louismntnu.

Created on 2023-06-14.
Last modified on 2023-10-21.

module foundation.pointed-torsorial-type-families where
Imports 
open import foundation.0-connected-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.locally-small-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.sorial-type-families
open import foundation.transport-along-identifications
open import foundation.type-theoretic-principle-of-choice
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.small-types
open import foundation-core.torsorial-type-families

open import structured-types.pointed-types

Idea

A type family E over a pointed type B is said to be pointed torsorial if it comes equipped with a family of equivalences

  E x ≃ (pt ＝ x)

indexed by x : B. Note that the type of such a torsorial structure on the type family E is equivalent to the type

  E pt × is-torsorial E

Indeed, if E is pointed torsorial, then refl : pt ＝ pt induces an element in E pt, and the total space of E is contractible by the fundamental theorem of identity types. Conversely, if we are given an element y : E pt and the total space of E is contractible, then the unique family of maps (pt ＝ x) → E x mapping refl to y is a family of equivalences.

Definitions

The predicate of being a pointed torsorial type family

module _
  {l1 l2 : Level} (B : Pointed-Type l1) (E : type-Pointed-Type B → UU l2)
  where

  is-pointed-torsorial-family-of-types : UU (l1 ⊔ l2)
  is-pointed-torsorial-family-of-types =
    (x : type-Pointed-Type B) → E x ≃ (point-Pointed-Type B ＝ x)

module _
  {l1 l2 : Level} (B : Pointed-Type l1) {E : type-Pointed-Type B → UU l2}
  (T : is-pointed-torsorial-family-of-types B E)
  where

  point-is-pointed-torsorial-family-of-types : E (point-Pointed-Type B)
  point-is-pointed-torsorial-family-of-types =
    map-inv-equiv (T (point-Pointed-Type B)) refl

  is-torsorial-space-is-pointed-torsorial-family-of-types :
    is-torsorial E
  is-torsorial-space-is-pointed-torsorial-family-of-types =
    fundamental-theorem-id'
      ( λ x → map-inv-equiv (T x))
      ( λ x → is-equiv-map-inv-equiv (T x))

Torsorial families of types

pointed-torsorial-family-of-types :
  {l1 : Level} (l2 : Level) (B : Pointed-Type l1) → UU (l1 ⊔ lsuc l2)
pointed-torsorial-family-of-types l2 B =
  Σ (type-Pointed-Type B → UU l2) (is-pointed-torsorial-family-of-types B)

Properties

Any torsorial type family is sorial

is-sorial-is-pointed-torsorial-family-of-types :
  {l1 l2 : Level} (B : Pointed-Type l1) {E : type-Pointed-Type B → UU l2} →
  is-pointed-torsorial-family-of-types B E → is-sorial-family-of-types B E
is-sorial-is-pointed-torsorial-family-of-types B {E} H x y =
  equiv-tr E (map-equiv (H x) y)

Being pointed torsorial is equivalent to being pointed and having contractible total space

module _
  {l1 l2 : Level} (B : Pointed-Type l1) {E : type-Pointed-Type B → UU l2}
  where

  point-and-contractible-total-space-is-pointed-torsorial-family-of-types :
    is-pointed-torsorial-family-of-types B E →
    E (point-Pointed-Type B) × is-contr (Σ (type-Pointed-Type B) E)
  pr1
    ( point-and-contractible-total-space-is-pointed-torsorial-family-of-types H)
    =
    point-is-pointed-torsorial-family-of-types B H
  pr2
    ( point-and-contractible-total-space-is-pointed-torsorial-family-of-types H)
    =
    is-torsorial-space-is-pointed-torsorial-family-of-types B H

Pointed connected types equipped with a pointed torsorial family of types of universe level l are locally l-small

module _
  {l1 l2 : Level} (B : Pointed-Type l1) {E : type-Pointed-Type B → UU l2}
  (T : is-pointed-torsorial-family-of-types B E)
  where

  abstract
    is-locally-small-is-pointed-torsorial-family-of-types :
      is-0-connected (type-Pointed-Type B) →
      is-locally-small l2 (type-Pointed-Type B)
    is-locally-small-is-pointed-torsorial-family-of-types H x y =
      apply-universal-property-trunc-Prop
        ( mere-eq-is-0-connected H (point-Pointed-Type B) x)
        ( is-small-Prop l2 (x ＝ y))
        ( λ where refl → (E y , inv-equiv (T y)))

The type of pointed torsorial type families of universe level l over a pointed connected type is equivalent to the proposition that B is locally l-small

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

  is-locally-small-pointed-torsorial-family-of-types :
    is-0-connected (type-Pointed-Type B) →
    pointed-torsorial-family-of-types l2 B →
    is-locally-small l2 (type-Pointed-Type B)
  is-locally-small-pointed-torsorial-family-of-types H (E , T) =
    is-locally-small-is-pointed-torsorial-family-of-types B T H

  pointed-torsorial-family-of-types-is-locally-small :
    is-locally-small l2 (type-Pointed-Type B) →
    pointed-torsorial-family-of-types l2 B
  pr1 (pointed-torsorial-family-of-types-is-locally-small H) x =
    type-is-small (H (point-Pointed-Type B) x)
  pr2 (pointed-torsorial-family-of-types-is-locally-small H) x =
    inv-equiv-is-small (H (point-Pointed-Type B) x)

  is-prop-pointed-torsorial-family-of-types :
    is-prop (pointed-torsorial-family-of-types l2 B)
  is-prop-pointed-torsorial-family-of-types =
    is-prop-equiv'
      ( distributive-Π-Σ)
      ( is-prop-Π
        ( λ x →
          is-prop-equiv
            ( equiv-tot (λ X → equiv-inv-equiv))
            ( is-prop-is-small l2 (point-Pointed-Type B ＝ x))))

  compute-pointed-torsorial-family-of-types-is-0-connected :
    is-0-connected (type-Pointed-Type B) →
    is-locally-small l2 (type-Pointed-Type B) ≃
    pointed-torsorial-family-of-types l2 B
  compute-pointed-torsorial-family-of-types-is-0-connected H =
    equiv-iff
      ( is-locally-small-Prop l2 (type-Pointed-Type B))
      ( pointed-torsorial-family-of-types l2 B ,
        is-prop-pointed-torsorial-family-of-types)
      ( pointed-torsorial-family-of-types-is-locally-small)
      ( is-locally-small-pointed-torsorial-family-of-types H)

  is-contr-pointed-torsorial-family-of-types :
    is-locally-small l2 (type-Pointed-Type B) →
    is-contr (pointed-torsorial-family-of-types l2 B)
  is-contr-pointed-torsorial-family-of-types H =
    is-proof-irrelevant-is-prop
      ( is-prop-pointed-torsorial-family-of-types)
      ( pointed-torsorial-family-of-types-is-locally-small H)

Recent changes