# Pointed torsorial type families

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

Created on 2023-06-14.

module foundation.pointed-torsorial-type-families where

Imports
open import foundation.0-connected-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.locally-small-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.sorial-type-families
open import foundation.transport-along-identifications
open import foundation.type-theoretic-principle-of-choice
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.small-types
open import foundation-core.torsorial-type-families

open import structured-types.pointed-types


## Idea

A type family E over a pointed type B is said to be pointed torsorial if it comes equipped with a family of equivalences

  E x ≃ (pt ＝ x)


indexed by x : B. Note that the type of such a torsorial structure on the type family E is equivalent to the type

  E pt × is-torsorial E


Indeed, if E is pointed torsorial, then refl : pt ＝ pt induces an element in E pt, and the total space of E is contractible by the fundamental theorem of identity types. Conversely, if we are given an element y : E pt and the total space of E is contractible, then the unique family of maps (pt ＝ x) → E x mapping refl to y is a family of equivalences.

## Definitions

### The predicate of being a pointed torsorial type family

module _
{l1 l2 : Level} (B : Pointed-Type l1) (E : type-Pointed-Type B → UU l2)
where

is-pointed-torsorial-family-of-types : UU (l1 ⊔ l2)
is-pointed-torsorial-family-of-types =
(x : type-Pointed-Type B) → E x ≃ (point-Pointed-Type B ＝ x)

module _
{l1 l2 : Level} (B : Pointed-Type l1) {E : type-Pointed-Type B → UU l2}
(T : is-pointed-torsorial-family-of-types B E)
where

point-is-pointed-torsorial-family-of-types : E (point-Pointed-Type B)
point-is-pointed-torsorial-family-of-types =
map-inv-equiv (T (point-Pointed-Type B)) refl

is-torsorial-space-is-pointed-torsorial-family-of-types :
is-torsorial E
is-torsorial-space-is-pointed-torsorial-family-of-types =
fundamental-theorem-id'
( λ x → map-inv-equiv (T x))
( λ x → is-equiv-map-inv-equiv (T x))


### Torsorial families of types

pointed-torsorial-family-of-types :
{l1 : Level} (l2 : Level) (B : Pointed-Type l1) → UU (l1 ⊔ lsuc l2)
pointed-torsorial-family-of-types l2 B =
Σ (type-Pointed-Type B → UU l2) (is-pointed-torsorial-family-of-types B)


## Properties

### Any torsorial type family is sorial

is-sorial-is-pointed-torsorial-family-of-types :
{l1 l2 : Level} (B : Pointed-Type l1) {E : type-Pointed-Type B → UU l2} →
is-pointed-torsorial-family-of-types B E → is-sorial-family-of-types B E
is-sorial-is-pointed-torsorial-family-of-types B {E} H x y =
equiv-tr E (map-equiv (H x) y)


### Being pointed torsorial is equivalent to being pointed and having contractible total space

module _
{l1 l2 : Level} (B : Pointed-Type l1) {E : type-Pointed-Type B → UU l2}
where

point-and-contractible-total-space-is-pointed-torsorial-family-of-types :
is-pointed-torsorial-family-of-types B E →
E (point-Pointed-Type B) × is-contr (Σ (type-Pointed-Type B) E)
pr1
( point-and-contractible-total-space-is-pointed-torsorial-family-of-types H)
=
point-is-pointed-torsorial-family-of-types B H
pr2
( point-and-contractible-total-space-is-pointed-torsorial-family-of-types H)
=
is-torsorial-space-is-pointed-torsorial-family-of-types B H


### Pointed connected types equipped with a pointed torsorial family of types of universe level l are locally l-small

module _
{l1 l2 : Level} (B : Pointed-Type l1) {E : type-Pointed-Type B → UU l2}
(T : is-pointed-torsorial-family-of-types B E)
where

abstract
is-locally-small-is-pointed-torsorial-family-of-types :
is-0-connected (type-Pointed-Type B) →
is-locally-small l2 (type-Pointed-Type B)
is-locally-small-is-pointed-torsorial-family-of-types H x y =
apply-universal-property-trunc-Prop
( mere-eq-is-0-connected H (point-Pointed-Type B) x)
( is-small-Prop l2 (x ＝ y))
( λ where refl → (E y , inv-equiv (T y)))


### The type of pointed torsorial type families of universe level l over a pointed connected type is equivalent to the proposition that B is locally l-small

module _
{l1 l2 : Level} (B : Pointed-Type l1)
where

is-locally-small-pointed-torsorial-family-of-types :
is-0-connected (type-Pointed-Type B) →
pointed-torsorial-family-of-types l2 B →
is-locally-small l2 (type-Pointed-Type B)
is-locally-small-pointed-torsorial-family-of-types H (E , T) =
is-locally-small-is-pointed-torsorial-family-of-types B T H

pointed-torsorial-family-of-types-is-locally-small :
is-locally-small l2 (type-Pointed-Type B) →
pointed-torsorial-family-of-types l2 B
pr1 (pointed-torsorial-family-of-types-is-locally-small H) x =
type-is-small (H (point-Pointed-Type B) x)
pr2 (pointed-torsorial-family-of-types-is-locally-small H) x =
inv-equiv-is-small (H (point-Pointed-Type B) x)

is-prop-pointed-torsorial-family-of-types :
is-prop (pointed-torsorial-family-of-types l2 B)
is-prop-pointed-torsorial-family-of-types =
is-prop-equiv'
( distributive-Π-Σ)
( is-prop-Π
( λ x →
is-prop-equiv
( equiv-tot (λ X → equiv-inv-equiv))
( is-prop-is-small l2 (point-Pointed-Type B ＝ x))))

compute-pointed-torsorial-family-of-types-is-0-connected :
is-0-connected (type-Pointed-Type B) →
is-locally-small l2 (type-Pointed-Type B) ≃
pointed-torsorial-family-of-types l2 B
compute-pointed-torsorial-family-of-types-is-0-connected H =
equiv-iff
( is-locally-small-Prop l2 (type-Pointed-Type B))
( pointed-torsorial-family-of-types l2 B ,
is-prop-pointed-torsorial-family-of-types)
( pointed-torsorial-family-of-types-is-locally-small)
( is-locally-small-pointed-torsorial-family-of-types H)

is-contr-pointed-torsorial-family-of-types :
is-locally-small l2 (type-Pointed-Type B) →
is-contr (pointed-torsorial-family-of-types l2 B)
is-contr-pointed-torsorial-family-of-types H =
is-proof-irrelevant-is-prop
( is-prop-pointed-torsorial-family-of-types)
( pointed-torsorial-family-of-types-is-locally-small H)