Torsorial type families

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-21.
Last modified 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

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.

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)

Recent changes