# Descent data for families of dependent pair types over the circle

Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2023-08-28.

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

Imports
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

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


## Idea

Given a family A : 𝕊¹ → U over the circle and a family B : (t : 𝕊¹) → (A t) → U over A, the descent data for the family of dependent pair types λ t → Σ (A t) (B t) is (Σ X R, map-Σ e k), where (X, e) is descent data for A and (R, k) is dependent descent data for B.

## Definitions

### Descent data for families of dependent pair types over the circle

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

descent-data-circle-dependent-pair-type : descent-data-circle (l2 ⊔ l3)
pr1 descent-data-circle-dependent-pair-type =
Σ ( type-family-with-descent-data-circle A)
( type-double-family-with-dependent-descent-data-circle A B)
pr2 descent-data-circle-dependent-pair-type =
equiv-Σ
( type-double-family-with-dependent-descent-data-circle A B)
( aut-family-with-descent-data-circle A)
( dependent-automorphism-double-family-with-dependent-descent-data-circle
( A)
( B))

family-descent-data-circle-dependent-pair-type : S → UU (l2 ⊔ l3)
family-descent-data-circle-dependent-pair-type x =
Σ ( family-family-with-descent-data-circle A x)
( double-family-double-family-with-dependent-descent-data-circle A B x)


## Properties

### Characterization of descent data for families of dependent pair types over the circle

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

eq-descent-data-circle-dependent-pair-type :
equiv-descent-data-circle
( descent-data-circle-dependent-pair-type l A B)
( descent-data-family-circle l
( family-descent-data-circle-dependent-pair-type l A B))
pr1 eq-descent-data-circle-dependent-pair-type =
equiv-Σ
( double-family-double-family-with-dependent-descent-data-circle A B
( base-free-loop l))
( equiv-family-with-descent-data-circle A)
( equiv-double-family-with-dependent-descent-data-circle A B)
pr2 eq-descent-data-circle-dependent-pair-type u =
inv
( tr-Σ
( double-family-double-family-with-dependent-descent-data-circle A B)
( loop-free-loop l)
( map-Σ
( double-family-double-family-with-dependent-descent-data-circle
( A)
( B)
( base-free-loop l))
( map-equiv-family-with-descent-data-circle A)
( map-equiv-double-family-with-dependent-descent-data-circle A B)
( u)) ∙
eq-pair-Σ
( inv (coherence-square-family-with-descent-data-circle A (pr1 u)))
( inv
( coherence-square-double-family-with-dependent-descent-data-circle
( A)
( B)
( pr1 u)
( pr2 u) ∙
tr-eq-pair-Σ
( ind-Σ
( double-family-double-family-with-dependent-descent-data-circle
( A)
( B)))
( loop-free-loop l)
( inv
( coherence-square-family-with-descent-data-circle A (pr1 u)))
( map-equiv-double-family-with-dependent-descent-data-circle A B
( pr1 u)
( pr2 u)))))

family-with-descent-data-circle-dependent-pair-type :
family-with-descent-data-circle l (l2 ⊔ l3)
pr1 family-with-descent-data-circle-dependent-pair-type =
family-descent-data-circle-dependent-pair-type l A B
pr1 (pr2 family-with-descent-data-circle-dependent-pair-type) =
descent-data-circle-dependent-pair-type l A B
pr2 (pr2 family-with-descent-data-circle-dependent-pair-type) =
eq-descent-data-circle-dependent-pair-type