# Dependent descent for the circle

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-08.

module synthetic-homotopy-theory.dependent-descent-circle where

Imports
open import foundation.commuting-squares-of-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.function-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.dependent-types-equipped-with-automorphisms

open import synthetic-homotopy-theory.descent-circle
open import synthetic-homotopy-theory.free-loops


## Idea

The dependent descent property of the circle asserts that a family over a family P over the circle is equivalently described by dependent descent data over the descent data of P, which is defined as a dependent type with an automorphism. More precisely, dependent descent data over descent data (X,e) for the circle consists of a type family R : X → U equipped with a family of equivalences k : (x : X) → R(x) ≃ R(e(x)) over e.

## Definitions

### Dependent descent data for the circle

dependent-descent-data-circle :
{l1 : Level} (l2 : Level) →
descent-data-circle l1 → UU (l1 ⊔ lsuc l2)
dependent-descent-data-circle l2 P =
Dependent-Type-With-Automorphism l2 P

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

type-dependent-descent-data-circle : type-descent-data-circle P → UU l2
type-dependent-descent-data-circle =
family-Dependent-Type-With-Automorphism P Q

dependent-automorphism-dependent-descent-data-circle :
equiv-fam
( type-dependent-descent-data-circle)
( type-dependent-descent-data-circle ∘ (map-descent-data-circle P))
dependent-automorphism-dependent-descent-data-circle =
dependent-automorphism-Dependent-Type-With-Automorphism P Q

map-dependent-descent-data-circle :
{ x : type-descent-data-circle P} →
( type-dependent-descent-data-circle x) →
( type-dependent-descent-data-circle (map-descent-data-circle P x))
map-dependent-descent-data-circle =
map-Dependent-Type-With-Automorphism P Q


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

dependent-descent-data-double-family-circle :
{ l1 l2 l3 : Level} {S : UU l1} (l : free-loop S) →
( A : family-with-descent-data-circle l l2) →
( (x : S) → (family-family-with-descent-data-circle A x) → UU l3) →
dependent-descent-data-circle l3
( descent-data-family-with-descent-data-circle A)
pr1 (dependent-descent-data-double-family-circle l A B) x =
B (base-free-loop l) (map-equiv-family-with-descent-data-circle A x)
pr2 (dependent-descent-data-double-family-circle l A B) x =
equiv-tr
( ind-Σ B)
( eq-pair-Σ
( loop-free-loop l)
( inv (coherence-square-family-with-descent-data-circle A x)))


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

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

equiv-dependent-descent-data-circle :
dependent-descent-data-circle l2 P → dependent-descent-data-circle l3 P →
UU (l1 ⊔ l2 ⊔ l3)
equiv-dependent-descent-data-circle =
equiv-Dependent-Type-With-Automorphism P

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

equiv-equiv-dependent-descent-data-circle :
equiv-fam
( type-dependent-descent-data-circle P Q)
( type-dependent-descent-data-circle P T)
equiv-equiv-dependent-descent-data-circle =
equiv-equiv-Dependent-Type-With-Automorphism P Q T α

map-equiv-dependent-descent-data-circle :
{ x : type-descent-data-circle P} →
( type-dependent-descent-data-circle P Q x) →
( type-dependent-descent-data-circle P T x)
map-equiv-dependent-descent-data-circle =
map-equiv-Dependent-Type-With-Automorphism P Q T α

coherence-square-equiv-dependent-descent-data-circle :
( x : type-descent-data-circle P) →
coherence-square-maps
( map-equiv-dependent-descent-data-circle)
( map-dependent-descent-data-circle P Q)
( map-dependent-descent-data-circle P T)
( map-equiv-dependent-descent-data-circle)
coherence-square-equiv-dependent-descent-data-circle =
coherence-square-equiv-Dependent-Type-With-Automorphism P Q T α


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

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

double-family-for-dependent-descent-data-circle :
{ l3 : Level} →
dependent-descent-data-circle l3
( descent-data-family-with-descent-data-circle A) →
UU (l1 ⊔ l2 ⊔ lsuc l3)
double-family-for-dependent-descent-data-circle {l3} Q =
Σ ( (x : S) → (family-family-with-descent-data-circle A x) → UU l3)
( λ B →
equiv-dependent-descent-data-circle
( descent-data-family-with-descent-data-circle A)
( Q)
( dependent-descent-data-double-family-circle l A B))

dependent-descent-data-circle-for-double-family :
{ l3 : Level} →
( (x : S) → (family-family-with-descent-data-circle A x) → UU l3) →
UU (l2 ⊔ lsuc l3)
dependent-descent-data-circle-for-double-family {l3} B =
Σ ( dependent-descent-data-circle l3
( descent-data-family-with-descent-data-circle A))
( λ Q →
equiv-dependent-descent-data-circle
( descent-data-family-with-descent-data-circle A)
( Q)
( dependent-descent-data-double-family-circle l A B))

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

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

double-family-double-family-with-dependent-descent-data-circle :
( x : S) → (family-family-with-descent-data-circle A x) → UU l3
double-family-double-family-with-dependent-descent-data-circle = pr1 B

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

dependent-descent-data-double-family-with-dependent-descent-data-circle :
dependent-descent-data-circle l3
( descent-data-family-with-descent-data-circle A)
dependent-descent-data-double-family-with-dependent-descent-data-circle =
pr1
dependent-descent-data-for-double-family-with-dependent-descent-data-circle

type-double-family-with-dependent-descent-data-circle :
type-family-with-descent-data-circle A → UU l3
type-double-family-with-dependent-descent-data-circle =
type-dependent-descent-data-circle
( descent-data-family-with-descent-data-circle A)
( dependent-descent-data-double-family-with-dependent-descent-data-circle)

dependent-automorphism-double-family-with-dependent-descent-data-circle :
equiv-fam
( type-double-family-with-dependent-descent-data-circle)
( type-double-family-with-dependent-descent-data-circle ∘
( map-aut-family-with-descent-data-circle A))
dependent-automorphism-double-family-with-dependent-descent-data-circle =
dependent-automorphism-dependent-descent-data-circle
( descent-data-family-with-descent-data-circle A)
( dependent-descent-data-double-family-with-dependent-descent-data-circle)

map-dependent-automorphism-double-family-with-dependent-descent-data-circle :
{ x : type-family-with-descent-data-circle A} →
( type-double-family-with-dependent-descent-data-circle x) →
( type-double-family-with-dependent-descent-data-circle
( map-aut-family-with-descent-data-circle A x))
map-dependent-automorphism-double-family-with-dependent-descent-data-circle =
map-dependent-descent-data-circle
( descent-data-family-with-descent-data-circle A)
( dependent-descent-data-double-family-with-dependent-descent-data-circle)

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

equiv-double-family-with-dependent-descent-data-circle :
( x : type-family-with-descent-data-circle A) →
( type-double-family-with-dependent-descent-data-circle x) ≃
( double-family-double-family-with-dependent-descent-data-circle
( base-free-loop l)
( map-equiv-family-with-descent-data-circle A x))
equiv-double-family-with-dependent-descent-data-circle =
equiv-equiv-dependent-descent-data-circle
( descent-data-family-with-descent-data-circle A)
( dependent-descent-data-double-family-with-dependent-descent-data-circle)
( dependent-descent-data-double-family-circle l A
( double-family-double-family-with-dependent-descent-data-circle))
( eq-double-family-with-dependent-descent-data-circle)

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

coherence-square-double-family-with-dependent-descent-data-circle :
( x : type-family-with-descent-data-circle A) →
coherence-square-maps
( map-equiv-double-family-with-dependent-descent-data-circle x)
( map-dependent-automorphism-double-family-with-dependent-descent-data-circle)
( tr
( ind-Σ
( double-family-double-family-with-dependent-descent-data-circle))
( eq-pair-Σ
( loop-free-loop l)
( inv (coherence-square-family-with-descent-data-circle A x))))
( map-equiv-double-family-with-dependent-descent-data-circle
( map-aut-family-with-descent-data-circle A x))
coherence-square-double-family-with-dependent-descent-data-circle =
coherence-square-equiv-dependent-descent-data-circle
( descent-data-family-with-descent-data-circle A)
( dependent-descent-data-double-family-with-dependent-descent-data-circle)
( dependent-descent-data-double-family-circle l A
( double-family-double-family-with-dependent-descent-data-circle))
( eq-double-family-with-dependent-descent-data-circle)

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


## Properties

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

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

id-equiv-dependent-descent-data-circle :
( Q : dependent-descent-data-circle l2 P) →
equiv-dependent-descent-data-circle P Q Q
id-equiv-dependent-descent-data-circle =
id-equiv-Dependent-Type-With-Automorphism P

equiv-eq-dependent-descent-data-circle :
( Q T : dependent-descent-data-circle l2 P) →
Q ＝ T → equiv-dependent-descent-data-circle P Q T
equiv-eq-dependent-descent-data-circle =
equiv-eq-Dependent-Type-With-Automorphism P

is-torsorial-equiv-dependent-descent-data-circle :
( Q : dependent-descent-data-circle l2 P) →
is-torsorial (equiv-dependent-descent-data-circle P Q)
is-torsorial-equiv-dependent-descent-data-circle =
is-torsorial-equiv-Dependent-Type-With-Automorphism P

is-equiv-equiv-eq-dependent-descent-data-circle :
( Q T : dependent-descent-data-circle l2 P) →
is-equiv (equiv-eq-dependent-descent-data-circle Q T)
is-equiv-equiv-eq-dependent-descent-data-circle =
is-equiv-equiv-eq-Dependent-Type-With-Automorphism P

extensionality-dependent-descent-data-circle :
( Q T : dependent-descent-data-circle l2 P) →
(Q ＝ T) ≃ equiv-dependent-descent-data-circle P Q T
extensionality-dependent-descent-data-circle =
extensionality-Dependent-Type-With-Automorphism P

eq-equiv-dependent-descent-data-circle :
( Q T : dependent-descent-data-circle l2 P) →
equiv-dependent-descent-data-circle P Q T → Q ＝ T
eq-equiv-dependent-descent-data-circle =
eq-equiv-Dependent-Type-With-Automorphism P


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

Given a type family A : 𝕊¹ → U with corresponding descent data (X, e), and a type family R : X → U over X invariant under e as witnessed by k, there is a unique family B : (t : 𝕊¹) → A t → U for which (R, k) is dependent descent data over A.

This is so far a conjecture which remains to be shown.

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

unique-dependent-family-property-circle : UU (l1 ⊔ l2 ⊔ lsuc l3)
unique-dependent-family-property-circle =
( Q :
dependent-descent-data-circle l3
( descent-data-family-with-descent-data-circle A)) →
is-contr (double-family-for-dependent-descent-data-circle l A Q)