# Subtypes of descent data for the circle

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

Created on 2023-08-28.

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

Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-dependent-pair-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.descent-circle-dependent-pair-types
open import synthetic-homotopy-theory.free-loops
open import synthetic-homotopy-theory.sections-descent-circle
open import synthetic-homotopy-theory.universal-property-circle


## Idea

Given a family A : 𝕊¹ → U over the circle and a family B : (t : 𝕊¹) → (A t) → U over A with corresponding descent data (X, e) and dependent descent data (R, k), where R is a subtype of X, we get that dependent functions of type (t : 𝕊¹) → Σ (A t) (B t) are exactly the fixpoints of e which belong to R.

## Properties

### Characterization of sections of families of subtypes

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)
( is-subtype-B :
( t : S) →
is-subtype
( double-family-double-family-with-dependent-descent-data-circle A B t))
where

subtype-descent-data-circle-subtype :
subtype l3 (type-family-with-descent-data-circle A)
pr1 (subtype-descent-data-circle-subtype x) =
type-double-family-with-dependent-descent-data-circle A B x
pr2 (subtype-descent-data-circle-subtype x) =
is-prop-equiv
( equiv-double-family-with-dependent-descent-data-circle A B x)
( is-subtype-B
( base-free-loop l)
( map-equiv-family-with-descent-data-circle A x))

equiv-fixpoint-descent-data-circle-subtype-fixpoint-in-subtype :
fixpoint-descent-data-circle
( descent-data-family-with-descent-data-circle
( family-with-descent-data-circle-dependent-pair-type l A B)) ≃
( Σ ( fixpoint-descent-data-circle
( descent-data-family-with-descent-data-circle A))
( λ x → is-in-subtype subtype-descent-data-circle-subtype (pr1 x)))
equiv-fixpoint-descent-data-circle-subtype-fixpoint-in-subtype =
equivalence-reasoning
fixpoint-descent-data-circle
( descent-data-family-with-descent-data-circle
( family-with-descent-data-circle-dependent-pair-type l A B))
≃ Σ ( type-family-with-descent-data-circle A)
( λ x →
Σ ( type-double-family-with-dependent-descent-data-circle A B x)
( λ r →
map-Σ
( type-double-family-with-dependent-descent-data-circle A B)
( map-aut-family-with-descent-data-circle A)
( λ x →
map-dependent-automorphism-double-family-with-dependent-descent-data-circle
( A)
( B))
( x , r) ＝
( x , r)))
by
associative-Σ
( type-family-with-descent-data-circle A)
( type-double-family-with-dependent-descent-data-circle A B)
( λ u →
map-Σ
( type-double-family-with-dependent-descent-data-circle A B)
( map-aut-family-with-descent-data-circle A)
( λ x →
map-dependent-automorphism-double-family-with-dependent-descent-data-circle
( A)
( B))
( u) ＝
u)
≃ Σ ( type-family-with-descent-data-circle A)
( λ x →
( is-in-subtype subtype-descent-data-circle-subtype x) ×
( map-aut-family-with-descent-data-circle A x ＝ x))
by
equiv-tot
( λ x →
equiv-tot
( λ r →
extensionality-type-subtype'
( subtype-descent-data-circle-subtype)
( _)
( x , r)))
≃ Σ ( type-family-with-descent-data-circle A)
( λ x →
( map-aut-family-with-descent-data-circle A x ＝ x) ×
( is-in-subtype subtype-descent-data-circle-subtype x))
by equiv-tot (λ _ → commutative-product)
≃ Σ ( fixpoint-descent-data-circle
( descent-data-family-with-descent-data-circle A))
( λ x → is-in-subtype subtype-descent-data-circle-subtype (pr1 x))
by
inv-associative-Σ
( type-family-with-descent-data-circle A)
( λ x → map-aut-family-with-descent-data-circle A x ＝ x)
( λ x → is-in-subtype subtype-descent-data-circle-subtype (pr1 x))

equiv-section-descent-data-circle-subtype-fixpoint-in-subtype :
dependent-universal-property-circle l →
( (x : S) → family-descent-data-circle-dependent-pair-type l A B x) ≃
( Σ ( fixpoint-descent-data-circle
( descent-data-family-with-descent-data-circle A))
( λ x → is-in-subtype subtype-descent-data-circle-subtype (pr1 x)))
equiv-section-descent-data-circle-subtype-fixpoint-in-subtype dup-circle =
equiv-fixpoint-descent-data-circle-subtype-fixpoint-in-subtype ∘e
( equiv-ev-fixpoint-descent-data-circle
( l)
( family-with-descent-data-circle-dependent-pair-type l A B)
( dup-circle))