Descent data for constant type families 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-constant-families where

Imports
open import foundation.constant-type-families
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.universe-levels

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


Idea

Descent data for the circle for a constant type family is the type it evaluates to, together with the identity.

Definitions

Descent data for constant type families over the circle

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

descent-data-circle-constant-type : descent-data-circle l2
pr1 descent-data-circle-constant-type = X
pr2 descent-data-circle-constant-type = id-equiv

family-descent-data-circle-constant-type : S → UU l2
family-descent-data-circle-constant-type x = X


Properties

Characterization of descent data for constant type families over the circle

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

eq-descent-data-circle-constant-type :
equiv-descent-data-circle
( descent-data-circle-constant-type l X)
( descent-data-family-circle l
( family-descent-data-circle-constant-type l X))
pr1 eq-descent-data-circle-constant-type = id-equiv
pr2 eq-descent-data-circle-constant-type x =
inv (tr-constant-type-family (loop-free-loop l) x)

family-with-descent-data-constant-type :
family-with-descent-data-circle l l2
pr1 family-with-descent-data-constant-type =
family-descent-data-circle-constant-type l X
pr1 (pr2 family-with-descent-data-constant-type) =
descent-data-circle-constant-type l X
pr2 (pr2 family-with-descent-data-constant-type) =
eq-descent-data-circle-constant-type