# Torsorial type families

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

Created on 2023-06-14.

module foundation.torsorial-type-families where

open import foundation-core.torsorial-type-families public

Imports
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


## Idea

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 → 𝒰).

## Definitions

### 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)
where

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


## Properties

### 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}
where

is-torsorial-fiber-Id :
{a : A} → ((x : A) → (a ＝ x) ≃ B x) → is-torsorial B
is-torsorial-fiber-Id H =
fundamental-theorem-id'
( λ 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)
where
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 =
equiv-iff
( Σ A (λ a → (x : A) → (a ＝ x) ≃ B x) ,
is-prop-total-family-of-equivalences-Id)
( is-contr-Prop (Σ A B))
( λ u → is-torsorial-fiber-Id (pr2 u))
( fiber-Id-is-torsorial)