# The descent property of the circle

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Vojtěch Štěpančík and Victor Blanchi.

Created on 2023-02-23.

module synthetic-homotopy-theory.descent-circle where

Imports
open import foundation.automorphisms
open import foundation.commuting-squares-of-maps
open import foundation.commuting-triangles-of-maps
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.univalence
open import foundation.universe-levels

open import structured-types.equivalences-types-equipped-with-automorphisms
open import structured-types.types-equipped-with-automorphisms

open import synthetic-homotopy-theory.free-loops
open import synthetic-homotopy-theory.universal-property-circle


## Idea

The descent property of the circle uniquely characterizes type families over the circle.

## Definitions

### Descent data for the circle

By the universal property of the circle and univalence, a type family A : 𝕊¹ → U over the circle is equivalent to a type X : U equipped with an automorphism e : X ≃ X, in a way made precise in further sections of this file. The pair (X, e) is called descent data for the circle.

descent-data-circle :
( l1 : Level) → UU (lsuc l1)
descent-data-circle = Type-With-Automorphism

module _
{ l1 : Level} (P : descent-data-circle l1)
where

type-descent-data-circle : UU l1
type-descent-data-circle = type-Type-With-Automorphism P

aut-descent-data-circle : Aut type-descent-data-circle
aut-descent-data-circle = automorphism-Type-With-Automorphism P

map-descent-data-circle : type-descent-data-circle → type-descent-data-circle
map-descent-data-circle = map-Type-With-Automorphism P


### Canonical descent data for a family over the circle

A type family over the circle gives rise to its canonical descent data, obtained by evaluation at base and transporting along loop.

descent-data-family-circle :
{ l1 l2 : Level} {S : UU l1} (l : free-loop S) →
( S → UU l2) → descent-data-circle l2
pr1 (descent-data-family-circle l A) = A (base-free-loop l)
pr2 (descent-data-family-circle l A) = equiv-tr A (loop-free-loop l)


### The identity type of descent data for the circle

An equivalence between (X, e) and (Y, f) is an equivalence between X and Y which commutes with the automorphisms.

equiv-descent-data-circle :
{ l1 l2 : Level} → descent-data-circle l1 → descent-data-circle l2 →
UU (l1 ⊔ l2)
equiv-descent-data-circle = equiv-Type-With-Automorphism

module _
{ l1 l2 : Level} (P : descent-data-circle l1) (Q : descent-data-circle l2)
( α : equiv-descent-data-circle P Q)
where

equiv-equiv-descent-data-circle :
type-descent-data-circle P ≃ type-descent-data-circle Q
equiv-equiv-descent-data-circle =
equiv-equiv-Type-With-Automorphism P Q α

map-equiv-descent-data-circle :
type-descent-data-circle P → type-descent-data-circle Q
map-equiv-descent-data-circle =
map-equiv-Type-With-Automorphism P Q α

coherence-square-equiv-descent-data-circle :
coherence-square-maps
( map-equiv-descent-data-circle)
( map-descent-data-circle P)
( map-descent-data-circle Q)
( map-equiv-descent-data-circle)
coherence-square-equiv-descent-data-circle =
coherence-square-equiv-Type-With-Automorphism P Q α


### A family over the circle equipped with corresponding descent data

A family for descent data (X, e) is a family over the circle, along with a proof that (X, e) is equivalent to the canonical descent data of the family.

Descent data for a family A : 𝕊¹ → U is descent data with a proof that it's equivalent to the canonical descent data of A.

A family with descent data is a family A : 𝕊¹ → U over the circle, equipped with descent data (X, e), and a proof of their equivalence. This can be described as a diagram

      α
X -----> A base
|         |
e|         | tr A loop
∨         ∨
X -----> A base
α


Ideally, every section characterizing descent data of a particular type family should include an element of type family-with-descent-data-circle, whose type family is the one being described.

Note on naming: a -for- in a name indicates that the particular entry contains a proof that it's somehow equivalent to the structure it's "for".

module _
{ l1 : Level} {S : UU l1} (l : free-loop S)
where

family-for-descent-data-circle :
{ l2 : Level} → descent-data-circle l2 → UU (l1 ⊔ lsuc l2)
family-for-descent-data-circle {l2} P =
Σ ( S → UU l2)
( λ A →
equiv-descent-data-circle
( P)
( descent-data-family-circle l A))

descent-data-circle-for-family :
{ l2 : Level} → (S → UU l2) → UU (lsuc l2)
descent-data-circle-for-family {l2} A =
Σ ( descent-data-circle l2)
( λ P →
equiv-descent-data-circle
( P)
( descent-data-family-circle l A))

family-with-descent-data-circle :
( l2 : Level) → UU (l1 ⊔ lsuc l2)
family-with-descent-data-circle l2 =
Σ ( S → UU l2) descent-data-circle-for-family

module _
{ l1 l2 : Level} {S : UU l1} {l : free-loop S}
( A : family-with-descent-data-circle l l2)
where

family-family-with-descent-data-circle : S → UU l2
family-family-with-descent-data-circle = pr1 A

descent-data-for-family-with-descent-data-circle :
descent-data-circle-for-family l
family-family-with-descent-data-circle
descent-data-for-family-with-descent-data-circle = pr2 A

descent-data-family-with-descent-data-circle : descent-data-circle l2
descent-data-family-with-descent-data-circle =
pr1 descent-data-for-family-with-descent-data-circle

type-family-with-descent-data-circle : UU l2
type-family-with-descent-data-circle =
type-descent-data-circle descent-data-family-with-descent-data-circle

aut-family-with-descent-data-circle : Aut type-family-with-descent-data-circle
aut-family-with-descent-data-circle =
aut-descent-data-circle descent-data-family-with-descent-data-circle

map-aut-family-with-descent-data-circle :
type-family-with-descent-data-circle → type-family-with-descent-data-circle
map-aut-family-with-descent-data-circle =
map-descent-data-circle descent-data-family-with-descent-data-circle

eq-family-with-descent-data-circle :
equiv-descent-data-circle
( descent-data-family-with-descent-data-circle)
( descent-data-family-circle l family-family-with-descent-data-circle)
eq-family-with-descent-data-circle =
pr2 descent-data-for-family-with-descent-data-circle

equiv-family-with-descent-data-circle :
type-family-with-descent-data-circle ≃
family-family-with-descent-data-circle (base-free-loop l)
equiv-family-with-descent-data-circle =
equiv-equiv-descent-data-circle
( descent-data-family-with-descent-data-circle)
( descent-data-family-circle l family-family-with-descent-data-circle)
( eq-family-with-descent-data-circle)

map-equiv-family-with-descent-data-circle :
type-family-with-descent-data-circle →
family-family-with-descent-data-circle (base-free-loop l)
map-equiv-family-with-descent-data-circle =
map-equiv equiv-family-with-descent-data-circle

coherence-square-family-with-descent-data-circle :
coherence-square-maps
( map-equiv-family-with-descent-data-circle)
( map-aut-family-with-descent-data-circle)
( tr family-family-with-descent-data-circle (loop-free-loop l))
( map-equiv-family-with-descent-data-circle)
coherence-square-family-with-descent-data-circle =
coherence-square-equiv-descent-data-circle
( descent-data-family-with-descent-data-circle)
( descent-data-family-circle l family-family-with-descent-data-circle)
( eq-family-with-descent-data-circle)

family-for-family-with-descent-data-circle :
family-for-descent-data-circle l
descent-data-family-with-descent-data-circle
pr1 family-for-family-with-descent-data-circle =
family-family-with-descent-data-circle
pr2 family-for-family-with-descent-data-circle =
eq-family-with-descent-data-circle


## Properties

### Characterization of the identity type of descent data for the circle

id-equiv-descent-data-circle :
{ l1 : Level} (P : descent-data-circle l1) →
equiv-descent-data-circle P P
id-equiv-descent-data-circle =
id-equiv-Type-With-Automorphism

equiv-eq-descent-data-circle :
{ l1 : Level} (P Q : descent-data-circle l1) →
P ＝ Q → equiv-descent-data-circle P Q
equiv-eq-descent-data-circle =
equiv-eq-Type-With-Automorphism

is-torsorial-equiv-descent-data-circle :
{ l1 : Level} (P : descent-data-circle l1) →
is-torsorial (equiv-descent-data-circle P)
is-torsorial-equiv-descent-data-circle =
is-torsorial-equiv-Type-With-Automorphism

is-equiv-equiv-eq-descent-data-circle :
{ l1 : Level} (P Q : descent-data-circle l1) →
is-equiv (equiv-eq-descent-data-circle P Q)
is-equiv-equiv-eq-descent-data-circle =
is-equiv-equiv-eq-Type-With-Automorphism

eq-equiv-descent-data-circle :
{ l1 : Level} (P Q : descent-data-circle l1) →
equiv-descent-data-circle P Q → P ＝ Q
eq-equiv-descent-data-circle =
eq-equiv-Type-With-Automorphism


### Alternative definition of equality of descent data as homomorphisms which are equivalences

module _
{ l1 l2 : Level}
( P : descent-data-circle l1)
( Q : descent-data-circle l2)
where

equiv-descent-data-circle' : UU (l1 ⊔ l2)
equiv-descent-data-circle' = equiv-Type-With-Automorphism' P Q

compute-equiv-descent-data-circle :
equiv-descent-data-circle' ≃ equiv-descent-data-circle P Q
compute-equiv-descent-data-circle = compute-equiv-Type-With-Automorphism P Q


### Uniqueness of descent data characterizing a type family over the circle

Given a type X and an automorphism e : X ≃ X, there is a unique type family 𝓓(X, e) : 𝕊¹ → U for which (X, e) is descent data.

comparison-descent-data-circle :
( l1 : Level) → free-loop (UU l1) → descent-data-circle l1
comparison-descent-data-circle l1 = tot (λ Y → equiv-eq)

is-equiv-comparison-descent-data-circle :
( l1 : Level) → is-equiv (comparison-descent-data-circle l1)
is-equiv-comparison-descent-data-circle l1 =
is-equiv-tot-is-fiberwise-equiv (λ Y → univalence Y Y)

module _
{ l1 l2 : Level} {S : UU l1} (l : free-loop S)
where

triangle-comparison-descent-data-circle :
coherence-triangle-maps
( descent-data-family-circle l)
( comparison-descent-data-circle l2)
( ev-free-loop l (UU l2))
triangle-comparison-descent-data-circle A =
eq-equiv-descent-data-circle
( descent-data-family-circle l A)
( comparison-descent-data-circle l2 (ev-free-loop l (UU l2) A))
( id-equiv , (htpy-eq (inv (compute-map-eq-ap (loop-free-loop l)))))

is-equiv-descent-data-family-circle-universal-property-circle :
( up-circle : universal-property-circle l) →
is-equiv (descent-data-family-circle l)
is-equiv-descent-data-family-circle-universal-property-circle up-circle =
is-equiv-left-map-triangle
( descent-data-family-circle l)
( comparison-descent-data-circle l2)
( ev-free-loop l (UU l2))
( triangle-comparison-descent-data-circle)
( up-circle (UU l2))
( is-equiv-comparison-descent-data-circle l2)

unique-family-property-circle :
{ l1 : Level} (l2 : Level) {S : UU l1} (l : free-loop S) →
UU (l1 ⊔ lsuc l2)
unique-family-property-circle l2 {S} l =
( Q : descent-data-circle l2) → is-contr (family-for-descent-data-circle l Q)

module _
{ l1 l2 : Level} {S : UU l1} (l : free-loop S)
( up-circle : universal-property-circle l)
where

unique-family-property-universal-property-circle :
unique-family-property-circle l2 l
unique-family-property-universal-property-circle Q =
is-contr-is-equiv'
( fiber (descent-data-family-circle l) Q)
( tot
( λ P →
equiv-eq-descent-data-circle Q (descent-data-family-circle l P) ∘
inv))
( is-equiv-tot-is-fiberwise-equiv
( λ P →
is-equiv-comp _ _
( is-equiv-inv _ _)
( is-equiv-equiv-eq-descent-data-circle
( Q)
( descent-data-family-circle l P))))
( is-contr-map-is-equiv
( is-equiv-descent-data-family-circle-universal-property-circle
( l)
( up-circle))
( Q))

family-for-descent-data-circle-descent-data :
( P : descent-data-circle l2) →
family-for-descent-data-circle l P
family-for-descent-data-circle-descent-data P =
center (unique-family-property-universal-property-circle P)

family-with-descent-data-circle-descent-data :
( P : descent-data-circle l2) →
( family-with-descent-data-circle l l2)
pr1 (family-with-descent-data-circle-descent-data P) =
pr1 (family-for-descent-data-circle-descent-data P)
pr1 (pr2 (family-with-descent-data-circle-descent-data P)) = P
pr2 (pr2 (family-with-descent-data-circle-descent-data P)) =
pr2 (family-for-descent-data-circle-descent-data P)