# Torsorial type families

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-21.

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