Torsorial type families

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-21.
Last modified on 2024-04-11.

module foundation-core.torsorial-type-families where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.identity-types

Idea

A type family B over A is said to be torsorial if its total space is contractible.

The terminology of torsorial type families is derived from torsors of higher group theory, which are type families X : BG → 𝒰 with contractible total space. In the conventional sense of the word, a torsor is therefore a torsorial type family over a pointed connected type. If we drop the condition that they are defined over a pointed connected type, we get to the notion of ‘torsor-like’, or indeed ‘torsorial’ type families.

The notion of torsoriality of type families is central in many characterizations of identity types. Indeed, the fundamental theorem of identity types shows that for any type family B over A and any a : A, the type family B is torsorial if and only if every family of maps

  (x : A) → a ＝ x → B x

is a family of equivalences. Indeed, the principal example of a torsorial type family is the identity type itself. More generally, any type family in the connected component of the identity type x ↦ a ＝ x is torsorial. These include torsors of higher groups and torsors of concrete groups.

Establishing torsoriality of type families is therefore one of the routine tasks in univalent mathematics. Some files that provide general tools for establishing torsoriality of type families include:

Definition

The predicate of being a torsorial type family

is-torsorial :
  {l1 l2 : Level} {B : UU l1} → (B → UU l2) → UU (l1 ⊔ l2)
is-torsorial E = is-contr (Σ _ E)

Examples

Identity types are torsorial

We prove two variants of the claim that identity types are torsorial:

  • The type family x ↦ a ＝ x is torsorial, and
  • The type family x ↦ x ＝ a is torsorial.
module _
  {l : Level} {A : UU l}
  where

  abstract
    is-torsorial-Id : (a : A) → is-torsorial (λ x → a ＝ x)
    pr1 (pr1 (is-torsorial-Id a)) = a
    pr2 (pr1 (is-torsorial-Id a)) = refl
    pr2 (is-torsorial-Id a) (.a , refl) = refl

  abstract
    is-torsorial-Id' : (a : A) → is-torsorial (λ x → x ＝ a)
    pr1 (pr1 (is-torsorial-Id' a)) = a
    pr2 (pr1 (is-torsorial-Id' a)) = refl
    pr2 (is-torsorial-Id' a) (.a , refl) = refl

See also

Recent changes