Torsorial type families

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

Created on 2023-06-14.
Last modified on 2023-11-24.

module foundation.torsorial-type-families where

open import foundation-core.torsorial-type-families public
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.logical-equivalences
open import foundation.universal-property-identity-types
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.type-theoretic-principle-of-choice


A type family E over B is said to be torsorial if its total space is contractible. By the fundamental theorem of identity types it follows that a type family E is torsorial if and only if it is in the image of Id : B → (B → 𝒰).


The predicate of being a torsorial type family over B

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

is-prop-is-torsorial :
  {l1 l2 : Level} {B : UU l1} (E : B  UU l2)  is-prop (is-torsorial E)
is-prop-is-torsorial E = is-prop-type-Prop (is-torsorial-Prop E)

The type of torsorial type families over B

torsorial-family-of-types :
  {l1 : Level} (l2 : Level)  UU l1  UU (l1  lsuc l2)
torsorial-family-of-types l2 B = Σ (B  UU l2) is-torsorial

module _
  {l1 l2 : Level} {B : UU l1} (T : torsorial-family-of-types l2 B)

  type-torsorial-family-of-types : B  UU l2
  type-torsorial-family-of-types = pr1 T

  is-torsorial-torsorial-family-of-types :
    is-torsorial type-torsorial-family-of-types
  is-torsorial-torsorial-family-of-types = pr2 T


fiber Id B ≃ is-torsorial B for any type family B over A

In other words, a type family B over A is in the image of Id : A → (A → 𝒰) if and only if B is torsorial. Since being contractible is a proposition, this observation leads to an alternative proof of the above claim that Id : A → (A → 𝒰) is an embedding. Our previous proof of the fact that Id : A → (A → 𝒰) is an embedding can be found in foundation.universal-property-identity-types.

module _
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2}

  is-torsorial-fiber-Id :
    {a : A}  ((x : A)  (a  x)  B x)  is-torsorial B
  is-torsorial-fiber-Id H =
      ( λ x  map-equiv (H x))
      ( λ x  is-equiv-map-equiv (H x))

  fiber-Id-is-torsorial :
    is-torsorial B  Σ A  a  (x : A)  (a  x)  B x)
  pr1 (fiber-Id-is-torsorial ((a , b) , H)) = a
  pr2 (fiber-Id-is-torsorial ((a , b) , H)) =
    map-inv-distributive-Π-Σ (f , fundamental-theorem-id ((a , b) , H) f)
    f : (x : A)  (a  x)  B x
    f x refl = b

  compute-fiber-Id :
    (Σ A  a  (x : A)  (a  x)  B x))  is-torsorial B
  compute-fiber-Id =
      ( Σ A  a  (x : A)  (a  x)  B x) ,
      ( is-contr-Prop (Σ A B))
      ( λ u  is-torsorial-fiber-Id (pr2 u))
      ( fiber-Id-is-torsorial)

Recent changes