The descent property of the circle
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Vojtěch Štěpančík and Victor Blanchi.
Created on 2023-02-23.
Last modified on 2023-09-11.
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.equality-dependent-function-types open import foundation.equality-dependent-pair-types open import foundation.equivalence-extensionality 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.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.structure-identity-principle open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types open import foundation.univalence open import foundation.universe-levels open import synthetic-homotopy-theory.free-loops open import synthetic-homotopy-theory.universal-property-circle
Idea
The descent property 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 l1 = Σ (UU l1) Aut module _ { l1 : Level} (P : descent-data-circle l1) where type-descent-data-circle : UU l1 type-descent-data-circle = pr1 P aut-descent-data-circle : Aut type-descent-data-circle aut-descent-data-circle = pr2 P map-descent-data-circle : type-descent-data-circle → type-descent-data-circle map-descent-data-circle = map-equiv aut-descent-data-circle
Homomorphisms between descent data for the circle
A homomorphism h
between (X, e)
and (Y, f)
is a map from X
to Y
such
that the obvious square commutes.
h
X -----> Y
| |
e| |f
v v
X -----> Y
h
hom-descent-data-circle : { l1 l2 : Level} ( P : descent-data-circle l1) (Q : descent-data-circle l2) → UU (l1 ⊔ l2) hom-descent-data-circle P Q = Σ ( (type-descent-data-circle P) → (type-descent-data-circle Q)) ( λ h → coherence-square-maps ( h) ( map-descent-data-circle P) ( map-descent-data-circle Q) ( h)) module _ { l1 l2 : Level} (P : descent-data-circle l1) (Q : descent-data-circle l2) ( h : hom-descent-data-circle P Q) where map-hom-descent-data-circle : type-descent-data-circle P → type-descent-data-circle Q map-hom-descent-data-circle = pr1 h coherence-hom-descent-data-circle : coherence-square-maps ( map-hom-descent-data-circle) ( map-descent-data-circle P) ( map-descent-data-circle Q) ( map-hom-descent-data-circle) coherence-hom-descent-data-circle = pr2 h
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
.
ev-descent-data-circle : { l1 l2 : Level} {S : UU l1} (l : free-loop S) → ( S → UU l2) → descent-data-circle l2 pr1 (ev-descent-data-circle l A) = A (base-free-loop l) pr2 (ev-descent-data-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.
Eq-descent-data-circle : { l1 l2 : Level} → descent-data-circle l1 → descent-data-circle l2 → UU (l1 ⊔ l2) Eq-descent-data-circle P Q = Σ ( type-descent-data-circle P ≃ type-descent-data-circle Q) ( λ h → coherence-square-maps ( map-equiv h) ( map-descent-data-circle P) ( map-descent-data-circle Q) ( map-equiv h)) module _ { l1 l2 : Level} (P : descent-data-circle l1) (Q : descent-data-circle l2) ( αH : Eq-descent-data-circle P Q) where equiv-Eq-descent-data-circle : type-descent-data-circle P ≃ type-descent-data-circle Q equiv-Eq-descent-data-circle = pr1 αH map-Eq-descent-data-circle : type-descent-data-circle P → type-descent-data-circle Q map-Eq-descent-data-circle = map-equiv equiv-Eq-descent-data-circle coherence-square-Eq-descent-data-circle : coherence-square-maps ( map-Eq-descent-data-circle) ( map-descent-data-circle P) ( map-descent-data-circle Q) ( map-Eq-descent-data-circle) coherence-square-Eq-descent-data-circle = pr2 αH
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
v v
X -----> A base
α
Ideally, every section characterizing descent data of a particular type family
should include a term 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 term 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 → Eq-descent-data-circle ( P) ( ev-descent-data-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 → Eq-descent-data-circle ( P) ( ev-descent-data-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 : Eq-descent-data-circle ( descent-data-family-with-descent-data-circle) ( ev-descent-data-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-Eq-descent-data-circle ( descent-data-family-with-descent-data-circle) ( ev-descent-data-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-Eq-descent-data-circle ( descent-data-family-with-descent-data-circle) ( ev-descent-data-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
Dependent descent data for the circle
The equivalence extends to the dependent case, where given a type family A
over the circle with descent data (X, e)
, a type family
B : (t : 𝕊¹) → A t → U
is equivalent to a type family R : X → U
equipped
with a family of equivalences k : (x : X) → R(x) ≃ R(e(x))
. The pair (R, k)
is called dependent descent data for the circle over A
. Intuitively, this
states that the types over points of X
belonging to the same connected
component in the total space Σ 𝕊¹ A
are equivalent.
dependent-descent-data-circle : { l1 : Level} → descent-data-circle l1 → ( l2 : Level) → UU (l1 ⊔ lsuc l2) dependent-descent-data-circle P l2 = Σ ( type-descent-data-circle P → UU l2) ( λ R → equiv-fam R (R ∘ (map-descent-data-circle P))) module _ { l1 l2 : Level} (P : descent-data-circle l1) ( Q : dependent-descent-data-circle P l2) where type-dependent-descent-data-circle : type-descent-data-circle P → UU l2 type-dependent-descent-data-circle = pr1 Q pseudo-aut-dependent-descent-data-circle : equiv-fam ( type-dependent-descent-data-circle) ( type-dependent-descent-data-circle ∘ (map-descent-data-circle P)) pseudo-aut-dependent-descent-data-circle = pr2 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 x = map-equiv (pseudo-aut-dependent-descent-data-circle x)
Canonical dependent descent data for a family over a family over the circle
ev-dependent-descent-data-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 ( descent-data-family-with-descent-data-circle A) ( l3) pr1 (ev-dependent-descent-data-circle l A B) x = B (base-free-loop l) (map-equiv-family-with-descent-data-circle A x) pr2 (ev-dependent-descent-data-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 Eq-dependent-descent-data-circle : dependent-descent-data-circle P l2 → dependent-descent-data-circle P l3 → UU (l1 ⊔ l2 ⊔ l3) Eq-dependent-descent-data-circle Q T = Σ ( equiv-fam ( type-dependent-descent-data-circle P Q) ( type-dependent-descent-data-circle P T)) ( λ H → ( x : type-descent-data-circle P) → coherence-square-maps ( map-equiv (H x)) ( map-dependent-descent-data-circle P Q x) ( map-dependent-descent-data-circle P T x) ( map-equiv (H (map-descent-data-circle P x)))) module _ { l1 l2 l3 : Level} (P : descent-data-circle l1) ( Q : dependent-descent-data-circle P l2) ( T : dependent-descent-data-circle P l3) ( αH : Eq-dependent-descent-data-circle P Q T) where equiv-Eq-dependent-descent-data-circle : equiv-fam ( type-dependent-descent-data-circle P Q) ( type-dependent-descent-data-circle P T) equiv-Eq-dependent-descent-data-circle = pr1 αH map-Eq-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-Eq-dependent-descent-data-circle x = map-equiv (equiv-Eq-dependent-descent-data-circle x) coherence-square-Eq-dependent-descent-data-circle : ( x : type-descent-data-circle P) → coherence-square-maps ( map-Eq-dependent-descent-data-circle x) ( map-dependent-descent-data-circle P Q x) ( map-dependent-descent-data-circle P T x) ( map-Eq-dependent-descent-data-circle ( map-descent-data-circle P x)) coherence-square-Eq-dependent-descent-data-circle = pr2 αH
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 family-for-dependent-descent-data-circle : { l3 : Level} → dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( l3) → UU (l1 ⊔ l2 ⊔ lsuc l3) family-for-dependent-descent-data-circle {l3} Q = Σ ( (x : S) → (family-family-with-descent-data-circle A x) → UU l3) ( λ B → Eq-dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( Q) ( ev-dependent-descent-data-circle l A B)) dependent-descent-data-circle-for-family : { l3 : Level} → ( (x : S) → (family-family-with-descent-data-circle A x) → UU l3) → UU (l2 ⊔ lsuc l3) dependent-descent-data-circle-for-family {l3} B = Σ ( dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( l3)) ( λ Q → Eq-dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( Q) ( ev-dependent-descent-data-circle l A B)) family-with-dependent-descent-data-circle : ( l3 : Level) → UU (l1 ⊔ l2 ⊔ lsuc l3) family-with-dependent-descent-data-circle l3 = Σ ( (x : S) → (family-family-with-descent-data-circle A x) → UU l3) dependent-descent-data-circle-for-family module _ { l1 l2 l3 : Level} {S : UU l1} {l : free-loop S} ( A : family-with-descent-data-circle l l2) ( B : family-with-dependent-descent-data-circle l A l3) where family-family-with-dependent-descent-data-circle : ( x : S) → (family-family-with-descent-data-circle A x) → UU l3 family-family-with-dependent-descent-data-circle = pr1 B dependent-descent-data-for-family-with-dependent-descent-data-circle : dependent-descent-data-circle-for-family l A family-family-with-dependent-descent-data-circle dependent-descent-data-for-family-with-dependent-descent-data-circle = pr2 B dependent-descent-data-family-with-dependent-descent-data-circle : dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( l3) dependent-descent-data-family-with-dependent-descent-data-circle = pr1 dependent-descent-data-for-family-with-dependent-descent-data-circle type-family-with-dependent-descent-data-circle : type-family-with-descent-data-circle A → UU l3 type-family-with-dependent-descent-data-circle = type-dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( dependent-descent-data-family-with-dependent-descent-data-circle) pseudo-aut-family-with-dependent-descent-data-circle : equiv-fam ( type-family-with-dependent-descent-data-circle) ( type-family-with-dependent-descent-data-circle ∘ ( map-aut-family-with-descent-data-circle A)) pseudo-aut-family-with-dependent-descent-data-circle = pseudo-aut-dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( dependent-descent-data-family-with-dependent-descent-data-circle) map-pseudo-aut-family-with-dependent-descent-data-circle : ( x : type-family-with-descent-data-circle A) → ( type-family-with-dependent-descent-data-circle x) → ( type-family-with-dependent-descent-data-circle ( map-aut-family-with-descent-data-circle A x)) map-pseudo-aut-family-with-dependent-descent-data-circle = map-dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( dependent-descent-data-family-with-dependent-descent-data-circle) eq-family-with-dependent-descent-data-circle : Eq-dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( dependent-descent-data-family-with-dependent-descent-data-circle) ( ev-dependent-descent-data-circle l A ( family-family-with-dependent-descent-data-circle)) eq-family-with-dependent-descent-data-circle = pr2 dependent-descent-data-for-family-with-dependent-descent-data-circle equiv-family-with-dependent-descent-data-circle : ( x : type-family-with-descent-data-circle A) → ( type-family-with-dependent-descent-data-circle x) ≃ ( family-family-with-dependent-descent-data-circle ( base-free-loop l) ( map-equiv-family-with-descent-data-circle A x)) equiv-family-with-dependent-descent-data-circle = equiv-Eq-dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( dependent-descent-data-family-with-dependent-descent-data-circle) ( ev-dependent-descent-data-circle l A ( family-family-with-dependent-descent-data-circle)) ( eq-family-with-dependent-descent-data-circle) map-equiv-family-with-dependent-descent-data-circle : ( x : type-family-with-descent-data-circle A) → ( type-family-with-dependent-descent-data-circle x) → ( family-family-with-dependent-descent-data-circle ( base-free-loop l) ( map-equiv-family-with-descent-data-circle A x)) map-equiv-family-with-dependent-descent-data-circle x = map-equiv (equiv-family-with-dependent-descent-data-circle x) coherence-square-family-with-dependent-descent-data-circle : ( x : type-family-with-descent-data-circle A) → coherence-square-maps ( map-equiv-family-with-dependent-descent-data-circle x) ( map-pseudo-aut-family-with-dependent-descent-data-circle x) ( tr ( ind-Σ (family-family-with-dependent-descent-data-circle)) ( eq-pair-Σ ( loop-free-loop l) ( inv (coherence-square-family-with-descent-data-circle A x)))) ( map-equiv-family-with-dependent-descent-data-circle ( map-aut-family-with-descent-data-circle A x)) coherence-square-family-with-dependent-descent-data-circle = coherence-square-Eq-dependent-descent-data-circle ( descent-data-family-with-descent-data-circle A) ( dependent-descent-data-family-with-dependent-descent-data-circle) ( ev-dependent-descent-data-circle l A ( family-family-with-dependent-descent-data-circle)) ( eq-family-with-dependent-descent-data-circle) family-for-family-with-dependent-descent-data-circle : family-for-dependent-descent-data-circle l A dependent-descent-data-family-with-dependent-descent-data-circle pr1 family-for-family-with-dependent-descent-data-circle = family-family-with-dependent-descent-data-circle pr2 family-for-family-with-dependent-descent-data-circle = eq-family-with-dependent-descent-data-circle
Properties
Characterization of the identity type of descent data for the circle
refl-Eq-descent-data-circle : { l1 : Level} (P : descent-data-circle l1) → Eq-descent-data-circle P P refl-Eq-descent-data-circle P = id-equiv , refl-htpy Eq-eq-descent-data-circle : { l1 : Level} (P Q : descent-data-circle l1) → P = Q → Eq-descent-data-circle P Q Eq-eq-descent-data-circle P .P refl = refl-Eq-descent-data-circle P is-contr-total-Eq-descent-data-circle : { l1 : Level} (P : descent-data-circle l1) → is-contr (Σ (descent-data-circle l1) (Eq-descent-data-circle P)) is-contr-total-Eq-descent-data-circle P = is-contr-total-Eq-structure ( λ Y f h → coherence-square-maps ( map-equiv h) ( map-descent-data-circle P) ( map-equiv f) ( map-equiv h)) ( is-contr-total-equiv (type-descent-data-circle P)) ( type-descent-data-circle P , id-equiv) ( is-contr-total-htpy-equiv (aut-descent-data-circle P)) is-equiv-Eq-eq-descent-data-circle : { l1 : Level} (P Q : descent-data-circle l1) → is-equiv (Eq-eq-descent-data-circle P Q) is-equiv-Eq-eq-descent-data-circle P = fundamental-theorem-id ( is-contr-total-Eq-descent-data-circle P) ( Eq-eq-descent-data-circle P) eq-Eq-descent-data-circle : { l1 : Level} (P Q : descent-data-circle l1) → Eq-descent-data-circle P Q → P = Q eq-Eq-descent-data-circle P Q = map-inv-is-equiv (is-equiv-Eq-eq-descent-data-circle P Q)
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 Eq-descent-data-circle' : UU (l1 ⊔ l2) Eq-descent-data-circle' = Σ ( hom-descent-data-circle P Q) ( λ h → is-equiv (map-hom-descent-data-circle P Q h)) equiv-Eq-descent-data-circle-hom-is-equiv : Eq-descent-data-circle P Q ≃ Eq-descent-data-circle' equiv-Eq-descent-data-circle-hom-is-equiv = equiv-right-swap-Σ
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 ( ev-descent-data-circle l) ( comparison-descent-data-circle l2) ( ev-free-loop l (UU l2)) triangle-comparison-descent-data-circle A = eq-Eq-descent-data-circle ( ev-descent-data-circle l A) ( comparison-descent-data-circle l2 (ev-free-loop l (UU l2) A)) ( id-equiv , (htpy-eq (inv (compute-equiv-eq-ap (loop-free-loop l))))) is-equiv-ev-descent-data-circle-universal-property-circle : ( up-circle : universal-property-circle (lsuc l2) l) → is-equiv (ev-descent-data-circle l) is-equiv-ev-descent-data-circle-universal-property-circle up-circle = is-equiv-comp-htpy ( ev-descent-data-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 (lsuc l2) 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 (ev-descent-data-circle l) Q) ( tot ( λ P → Eq-eq-descent-data-circle Q (ev-descent-data-circle l P) ∘ inv)) ( is-equiv-tot-is-fiberwise-equiv ( λ P → is-equiv-comp _ _ ( is-equiv-inv _ _) ( is-equiv-Eq-eq-descent-data-circle ( Q) ( ev-descent-data-circle l P)))) ( is-contr-map-is-equiv ( is-equiv-ev-descent-data-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)
Characterization of the identity type of dependent descent data for the circle
module _ { l1 l2 : Level} (P : descent-data-circle l1) where refl-Eq-dependent-descent-data-circle : ( Q : dependent-descent-data-circle P l2) → Eq-dependent-descent-data-circle P Q Q pr1 (refl-Eq-dependent-descent-data-circle Q) = id-equiv-fam (type-dependent-descent-data-circle P Q) pr2 (refl-Eq-dependent-descent-data-circle Q) x = refl-htpy Eq-eq-dependent-descent-data-circle : ( Q T : dependent-descent-data-circle P l2) → Q = T → Eq-dependent-descent-data-circle P Q T Eq-eq-dependent-descent-data-circle Q .Q refl = refl-Eq-dependent-descent-data-circle Q is-contr-total-Eq-dependent-descent-data-circle : ( Q : dependent-descent-data-circle P l2) → is-contr ( Σ ( dependent-descent-data-circle P l2) ( Eq-dependent-descent-data-circle P Q)) is-contr-total-Eq-dependent-descent-data-circle Q = is-contr-total-Eq-structure ( λ R K H → ( x : type-descent-data-circle P) → coherence-square-maps ( map-equiv (H x)) ( map-dependent-descent-data-circle P Q x) ( map-equiv (K x)) ( map-equiv (H (map-descent-data-circle P x)))) ( is-contr-total-equiv-fam (type-dependent-descent-data-circle P Q)) ( type-dependent-descent-data-circle P Q , id-equiv-fam (type-dependent-descent-data-circle P Q)) ( is-contr-total-Eq-Π ( λ x K → ( map-dependent-descent-data-circle P Q x) ~ ( map-equiv K)) ( λ x → is-contr-total-htpy-equiv ( pseudo-aut-dependent-descent-data-circle P Q x))) is-equiv-Eq-eq-dependent-descent-data-circle : ( Q T : dependent-descent-data-circle P l2) → is-equiv (Eq-eq-dependent-descent-data-circle Q T) is-equiv-Eq-eq-dependent-descent-data-circle Q = fundamental-theorem-id ( is-contr-total-Eq-dependent-descent-data-circle Q) ( Eq-eq-dependent-descent-data-circle Q) eq-Eq-dependent-descent-data-circle : ( Q T : dependent-descent-data-circle P l2) → Eq-dependent-descent-data-circle P Q T → Q = T eq-Eq-dependent-descent-data-circle Q T = map-inv-is-equiv (is-equiv-Eq-eq-dependent-descent-data-circle Q T)
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 ( descent-data-family-with-descent-data-circle A) ( l3)) → is-contr (family-for-dependent-descent-data-circle l A Q)
Recent changes
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-09-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-08-28. Vojtěch Štěpančík. Extending infrastructure for working with descent data for the circle (#709).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).