From c2536c944144c61d501e0c2d373d9f9f975a73c6 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 13:08:25 +0000
Subject: [PATCH 01/10] clean up descent

---
 .../descent-coproduct-types.lagda.md          | 185 +++++++++++-------
 .../descent-dependent-pair-types.lagda.md     |  87 ++++++--
 src/foundation/descent-empty-types.lagda.md   |  17 ++
 src/foundation/descent-equivalences.lagda.md  |  25 +--
 .../dependent-descent-circle.lagda.md         |  20 +-
 .../descent-circle-subtypes.lagda.md          |   4 +-
 .../descent-circle.lagda.md                   |  18 +-
 .../descent-property-pushouts.lagda.md        |   4 +-
 ...cent-property-sequential-colimits.lagda.md |   2 +-
 9 files changed, 236 insertions(+), 126 deletions(-)

diff --git a/src/foundation/descent-coproduct-types.lagda.md b/src/foundation/descent-coproduct-types.lagda.md
index 03c1a582ba5..dbf7559e115 100644
--- a/src/foundation/descent-coproduct-types.lagda.md
+++ b/src/foundation/descent-coproduct-types.lagda.md
@@ -10,10 +10,12 @@ module foundation.descent-coproduct-types where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
 open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-fibers-of-maps
+open import foundation.logical-equivalences
 open import foundation.universe-levels
 open import foundation.whiskering-identifications-concatenation
 
@@ -29,6 +31,33 @@ open import foundation-core.pullbacks
 
 </details>
 
+## Idea
+
+The
+{{#concept "descent property" Disambiguation="of coproduct types" Agda=iff-descent-coproduct}}
+of [coproduct types](foundation-core.coproduct-types.md) states that given a map
+`i : X' → X` and two [cones](foundation.cones-over-cospan-diagrams.md)
+
+```text
+  A' -----> X'     B' -----> X'
+  |         |      |         |
+  |    α    | i    |    β    | i
+  ∨         ∨      ∨         ∨
+  A ------> X      B ------> X
+```
+
+then the coproduct cone
+
+```text
+  A' + B' -----> X'
+     |           |
+     |    α+β    | i
+     ∨           ∨
+   A + B ------> X
+```
+
+is a [pullback](foundation-core.pullbacks.md) if and only if each cone is.
+
 ## Theorem
 
 ```agda
@@ -36,15 +65,15 @@ module _
   {l1 l2 l3 l1' l2' l3' : Level}
   {A : UU l1} {B : UU l2} {X : UU l3}
   {A' : UU l1'} {B' : UU l2'} {X' : UU l3'}
-  (f : A' → A) (g : B' → B) (h : X' → X)
+  (f : A' → A) (g : B' → B) (i : X' → X)
   (αA : A → X) (αB : B → X) (αA' : A' → X') (αB' : B' → X')
-  (HA : αA ∘ f ~ h ∘ αA') (HB : αB ∘ g ~ h ∘ αB')
+  (HA : αA ∘ f ~ i ∘ αA') (HB : αB ∘ g ~ i ∘ αB')
   where
 
   triangle-descent-square-fiber-map-coproduct-inl-fiber :
     (x : A) →
-    ( map-fiber-vertical-map-cone αA h (f , αA' , HA) x) ~
-    ( map-fiber-vertical-map-cone (ind-coproduct _ αA αB) h
+    ( map-fiber-vertical-map-cone αA i (f , αA' , HA) x) ~
+    ( map-fiber-vertical-map-cone (ind-coproduct _ αA αB) i
       ( map-coproduct f g , ind-coproduct _ αA' αB' , ind-coproduct _ HA HB)
       ( inl x)) ∘
     ( fiber-map-coproduct-inl-fiber f g x)
@@ -56,8 +85,8 @@ module _
 
   triangle-descent-square-fiber-map-coproduct-inr-fiber :
     (y : B) →
-    ( map-fiber-vertical-map-cone αB h (g , αB' , HB) y) ~
-    ( map-fiber-vertical-map-cone (ind-coproduct _ αA αB) h
+    ( map-fiber-vertical-map-cone αB i (g , αB' , HB) y) ~
+    ( map-fiber-vertical-map-cone (ind-coproduct _ αA αB) i
       ( map-coproduct f g , ind-coproduct _ αA' αB' , ind-coproduct _ HA HB)
       ( inr y)) ∘
     ( fiber-map-coproduct-inr-fiber f g y)
@@ -71,118 +100,130 @@ module _
   {l1 l2 l3 l1' l2' l3' : Level}
   {A : UU l1} {B : UU l2} {X : UU l3} {A' : UU l1'} {B' : UU l2'} {X' : UU l3'}
   (f : A → X) (g : B → X) (i : X' → X)
+  (α@(h , f' , H) : cone f i A') (β@(k , g' , K) : cone g i B')
   where
 
   cone-descent-coproduct :
-    (cone-A' : cone f i A') (cone-B' : cone g i B') →
-    cone (ind-coproduct _ f g) i (A' + B')
-  pr1 (cone-descent-coproduct (h , f' , H) (k , g' , K)) = map-coproduct h k
-  pr1 (pr2 (cone-descent-coproduct (h , f' , H) (k , g' , K))) (inl a') = f' a'
-  pr1 (pr2 (cone-descent-coproduct (h , f' , H) (k , g' , K))) (inr b') = g' b'
-  pr2 (pr2 (cone-descent-coproduct (h , f' , H) (k , g' , K))) (inl a') = H a'
-  pr2 (pr2 (cone-descent-coproduct (h , f' , H) (k , g' , K))) (inr b') = K b'
+    cone (rec-coproduct f g) i (A' + B')
+  pr1 (cone-descent-coproduct) = map-coproduct h k
+  pr1 (pr2 cone-descent-coproduct) (inl a') = f' a'
+  pr1 (pr2 cone-descent-coproduct) (inr b') = g' b'
+  pr2 (pr2 cone-descent-coproduct) (inl a') = H a'
+  pr2 (pr2 cone-descent-coproduct) (inr b') = K b'
+
+  abstract
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-descent-coproduct :
+      is-pullback f i α →
+      is-pullback g i β →
+      is-fiberwise-equiv
+        ( map-fiber-vertical-map-cone
+          ( rec-coproduct f g)
+          ( i)
+          ( cone-descent-coproduct))
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-descent-coproduct
+      is-pb-α is-pb-β (inl x) =
+      is-equiv-right-map-triangle
+        ( map-fiber-vertical-map-cone f i (h , f' , H) x)
+        ( map-fiber-vertical-map-cone (rec-coproduct f g) i
+          ( cone-descent-coproduct)
+          ( inl x))
+        ( fiber-map-coproduct-inl-fiber h k x)
+        ( triangle-descent-square-fiber-map-coproduct-inl-fiber
+          h k i f g f' g' H K x)
+        ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback f i
+          ( h , f' , H) is-pb-α x)
+        ( is-equiv-fiber-map-coproduct-inl-fiber h k x)
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-descent-coproduct
+      is-pb-α is-pb-β (inr y) =
+      is-equiv-right-map-triangle
+        ( map-fiber-vertical-map-cone g i (k , g' , K) y)
+        ( map-fiber-vertical-map-cone
+          ( rec-coproduct f g) i
+          ( cone-descent-coproduct)
+          ( inr y))
+        ( fiber-map-coproduct-inr-fiber h k y)
+        ( triangle-descent-square-fiber-map-coproduct-inr-fiber
+          h k i f g f' g' H K y)
+        ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback g i
+          ( k , g' , K) is-pb-β y)
+        ( is-equiv-fiber-map-coproduct-inr-fiber h k y)
 
   abstract
     descent-coproduct :
-      (cone-A' : cone f i A') (cone-B' : cone g i B') →
-      is-pullback f i cone-A' →
-      is-pullback g i cone-B' →
+      is-pullback f i α →
+      is-pullback g i β →
       is-pullback
-        ( ind-coproduct _ f g)
+        ( rec-coproduct f g)
         ( i)
-        ( cone-descent-coproduct cone-A' cone-B')
-    descent-coproduct (h , f' , H) (k , g' , K) is-pb-cone-A' is-pb-cone-B' =
+        ( cone-descent-coproduct)
+    descent-coproduct is-pb-α is-pb-β =
       is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone
-        ( ind-coproduct _ f g)
+        ( rec-coproduct f g)
         ( i)
-        ( cone-descent-coproduct (h , f' , H) (k , g' , K))
-        ( α)
-      where
-      α :
-        is-fiberwise-equiv
-          ( map-fiber-vertical-map-cone
-            ( ind-coproduct (λ _ → X) f g)
-            ( i)
-            ( cone-descent-coproduct (h , f' , H) (k , g' , K)))
-      α (inl x) =
-        is-equiv-right-map-triangle
-          ( map-fiber-vertical-map-cone f i (h , f' , H) x)
-          ( map-fiber-vertical-map-cone (ind-coproduct _ f g) i
-            ( cone-descent-coproduct (h , f' , H) (k , g' , K))
-            ( inl x))
-          ( fiber-map-coproduct-inl-fiber h k x)
-          ( triangle-descent-square-fiber-map-coproduct-inl-fiber
-            h k i f g f' g' H K x)
-          ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback f i
-            ( h , f' , H) is-pb-cone-A' x)
-          ( is-equiv-fiber-map-coproduct-inl-fiber h k x)
-      α (inr y) =
-        is-equiv-right-map-triangle
-          ( map-fiber-vertical-map-cone g i (k , g' , K) y)
-          ( map-fiber-vertical-map-cone
-            ( ind-coproduct _ f g) i
-            ( cone-descent-coproduct (h , f' , H) (k , g' , K))
-            ( inr y))
-          ( fiber-map-coproduct-inr-fiber h k y)
-          ( triangle-descent-square-fiber-map-coproduct-inr-fiber
-            h k i f g f' g' H K y)
-          ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback g i
-            ( k , g' , K) is-pb-cone-B' y)
-          ( is-equiv-fiber-map-coproduct-inr-fiber h k y)
+        ( cone-descent-coproduct)
+        ( is-fiberwise-equiv-map-fiber-vertical-map-cone-descent-coproduct
+          ( is-pb-α)
+          ( is-pb-β))
 
   abstract
     descent-coproduct-inl :
-      (cone-A' : cone f i A') (cone-B' : cone g i B') →
       is-pullback
-        ( ind-coproduct _ f g)
+        ( rec-coproduct f g)
         ( i)
-        ( cone-descent-coproduct cone-A' cone-B') →
-      is-pullback f i cone-A'
-    descent-coproduct-inl (h , f' , H) (k , g' , K) is-pb-dsq =
+        ( cone-descent-coproduct) →
+      is-pullback f i α
+    descent-coproduct-inl is-pb-dsq =
       is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone f i
         ( h , f' , H)
         ( λ a →
           is-equiv-left-map-triangle
           ( map-fiber-vertical-map-cone f i (h , f' , H) a)
-          ( map-fiber-vertical-map-cone (ind-coproduct _ f g) i
-            ( cone-descent-coproduct (h , f' , H) (k , g' , K))
+          ( map-fiber-vertical-map-cone (rec-coproduct f g) i
+            ( cone-descent-coproduct)
             ( inl a))
           ( fiber-map-coproduct-inl-fiber h k a)
           ( triangle-descent-square-fiber-map-coproduct-inl-fiber
             h k i f g f' g' H K a)
           ( is-equiv-fiber-map-coproduct-inl-fiber h k a)
           ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
-            ( ind-coproduct _ f g)
+            ( rec-coproduct f g)
             ( i)
-            ( cone-descent-coproduct ( h , f' , H) (k , g' , K))
+            ( cone-descent-coproduct)
             ( is-pb-dsq)
             ( inl a)))
 
   abstract
     descent-coproduct-inr :
-      (cone-A' : cone f i A') (cone-B' : cone g i B') →
       is-pullback
-        ( ind-coproduct _ f g)
+        ( rec-coproduct f g)
         ( i)
-        ( cone-descent-coproduct cone-A' cone-B') →
-      is-pullback g i cone-B'
-    descent-coproduct-inr (h , f' , H) (k , g' , K) is-pb-dsq =
+        ( cone-descent-coproduct) →
+      is-pullback g i β
+    descent-coproduct-inr is-pb-dsq =
       is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone g i
         ( k , g' , K)
         ( λ b →
           is-equiv-left-map-triangle
           ( map-fiber-vertical-map-cone g i (k , g' , K) b)
-          ( map-fiber-vertical-map-cone (ind-coproduct _ f g) i
-            ( cone-descent-coproduct (h , f' , H) (k , g' , K))
+          ( map-fiber-vertical-map-cone (rec-coproduct f g) i
+            ( cone-descent-coproduct)
             ( inr b))
           ( fiber-map-coproduct-inr-fiber h k b)
           ( triangle-descent-square-fiber-map-coproduct-inr-fiber
             h k i f g f' g' H K b)
           ( is-equiv-fiber-map-coproduct-inr-fiber h k b)
           ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
-            ( ind-coproduct _ f g)
+            ( rec-coproduct f g)
             ( i)
-            ( cone-descent-coproduct (h , f' , H) (k , g' , K))
+            ( cone-descent-coproduct)
             ( is-pb-dsq)
             ( inr b)))
+
+  iff-descent-coproduct :
+    is-pullback f i α × is-pullback g i β ↔
+    is-pullback (rec-coproduct f g) i cone-descent-coproduct
+  iff-descent-coproduct =
+    ( ( λ (is-pb-α , is-pb-β) → descent-coproduct is-pb-α is-pb-β) ,
+      ( λ is-pb-dsq →
+        ( descent-coproduct-inl is-pb-dsq , descent-coproduct-inr is-pb-dsq)))
 ```
diff --git a/src/foundation/descent-dependent-pair-types.lagda.md b/src/foundation/descent-dependent-pair-types.lagda.md
index 9f3cdfc1335..9e6a5b6cdb2 100644
--- a/src/foundation/descent-dependent-pair-types.lagda.md
+++ b/src/foundation/descent-dependent-pair-types.lagda.md
@@ -10,6 +10,7 @@ module foundation.descent-dependent-pair-types where
 open import foundation.cones-over-cospan-diagrams
 open import foundation.dependent-pair-types
 open import foundation.functoriality-fibers-of-maps
+open import foundation.logical-equivalences
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
@@ -22,67 +23,111 @@ open import foundation-core.pullbacks
 
 </details>
 
+## Idea
+
+The
+{{#concept "descent property" Disambiguation="of dependent pair types" Agda=iff-descent-Σ}}
+of [dependent pair types](foundation.dependent-pair-types.md) states that, given
+a map `h : Y → X` and a family of maps `f : (i : I) → A i → X` together with a
+family of [cones](foundation.cones-over-cospan-diagrams.md)
+
+```text
+  B i -----> Y
+   |         |
+   |   c i   | h
+   ∨         ∨
+  A i -----> X
+       f i
+```
+
+for every `i`, then the family is a family of
+[pullback](foundation-core.pullbacks.md) cones if and only if the total cone
+
+```text
+  Σ I B -----> Y
+    |          |
+    |    Σc    | h
+    ∨          ∨
+  Σ I A -----> X
+       rec-Σ f
+```
+
+is a pullback cone.
+
 ## Theorem
 
 ```agda
 module _
   {l1 l2 l3 l4 l5 : Level}
-  {I : UU l1} {A : I → UU l2} {A' : I → UU l3} {X : UU l4} {X' : UU l5}
-  (f : (i : I) → A i → X) (h : X' → X)
-  (c : (i : I) → cone (f i) h (A' i))
+  {I : UU l1} {A : I → UU l2} {B : I → UU l3} {X : UU l4} {Y : UU l5}
+  (f : (i : I) → A i → X) (h : Y → X)
+  (c : (i : I) → cone (f i) h (B i))
   where
 
-  cone-descent-Σ : cone (ind-Σ f) h (Σ I A')
+  cone-descent-Σ : cone (rec-Σ f) h (Σ I B)
   cone-descent-Σ =
     triple
-      ( tot (λ i → (pr1 (c i))))
-      ( ind-Σ (λ i → (pr1 (pr2 (c i)))))
-      ( ind-Σ (λ i → (pr2 (pr2 (c i)))))
+      ( tot (λ i → vertical-map-cone (f i) h (c i)))
+      ( ind-Σ (λ i → horizontal-map-cone (f i) h (c i)))
+      ( ind-Σ (λ i → coherence-square-cone (f i) h (c i)))
 
   triangle-descent-Σ :
     (i : I) (a : A i) →
     ( map-fiber-vertical-map-cone (f i) h (c i) a) ~
-    ( ( map-fiber-vertical-map-cone (ind-Σ f) h cone-descent-Σ (pair i a)) ∘
-      ( map-inv-compute-fiber-tot (λ i → (pr1 (c i))) (pair i a)))
-  triangle-descent-Σ i .(pr1 (c i) a') (pair a' refl) = refl
+    ( map-fiber-vertical-map-cone (rec-Σ f) h cone-descent-Σ (i , a)) ∘
+    ( map-inv-compute-fiber-tot (λ i → vertical-map-cone (f i) h (c i)) (i , a))
+  triangle-descent-Σ i .(vertical-map-cone (f i) h (c i) a') (a' , refl) = refl
 
   abstract
     descent-Σ :
       ((i : I) → is-pullback (f i) h (c i)) →
-      is-pullback (ind-Σ f) h cone-descent-Σ
+      is-pullback (rec-Σ f) h cone-descent-Σ
     descent-Σ is-pb-c =
       is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone
-        ( ind-Σ f)
+        ( rec-Σ f)
         ( h)
         ( cone-descent-Σ)
         ( ind-Σ
           ( λ i a →
             is-equiv-right-map-triangle
             ( map-fiber-vertical-map-cone (f i) h (c i) a)
-            ( map-fiber-vertical-map-cone (ind-Σ f) h cone-descent-Σ (pair i a))
-            ( map-inv-compute-fiber-tot (λ i → pr1 (c i)) (pair i a))
+            ( map-fiber-vertical-map-cone (rec-Σ f) h cone-descent-Σ (i , a))
+            ( map-inv-compute-fiber-tot
+              ( λ i → vertical-map-cone (f i) h (c i))
+              ( i , a))
             ( triangle-descent-Σ i a)
             ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
               (f i) h (c i) (is-pb-c i) a)
-            ( is-equiv-map-inv-compute-fiber-tot (λ i → pr1 (c i)) (pair i a))))
+            ( is-equiv-map-inv-compute-fiber-tot
+              ( λ i → vertical-map-cone (f i) h (c i))
+              ( i , a))))
 
   abstract
     descent-Σ' :
-      is-pullback (ind-Σ f) h cone-descent-Σ →
+      is-pullback (rec-Σ f) h cone-descent-Σ →
       ((i : I) → is-pullback (f i) h (c i))
     descent-Σ' is-pb-dsq i =
       is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone (f i) h (c i)
         ( λ a →
           is-equiv-left-map-triangle
           ( map-fiber-vertical-map-cone (f i) h (c i) a)
-          ( map-fiber-vertical-map-cone (ind-Σ f) h cone-descent-Σ (pair i a))
-          ( map-inv-compute-fiber-tot (λ i → pr1 (c i)) (pair i a))
+          ( map-fiber-vertical-map-cone (rec-Σ f) h cone-descent-Σ (i , a))
+          ( map-inv-compute-fiber-tot
+            ( λ i → vertical-map-cone (f i) h (c i))
+            ( i , a))
           ( triangle-descent-Σ i a)
-          ( is-equiv-map-inv-compute-fiber-tot (λ i → pr1 (c i)) (pair i a))
+          ( is-equiv-map-inv-compute-fiber-tot
+            ( λ i → vertical-map-cone (f i) h (c i))
+            ( i , a))
           ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
-            ( ind-Σ f)
+            ( rec-Σ f)
             ( h)
             ( cone-descent-Σ)
             ( is-pb-dsq)
-            ( pair i a)))
+            ( i , a)))
+
+  iff-descent-Σ :
+    ((i : I) → is-pullback (f i) h (c i)) ↔
+    is-pullback (rec-Σ f) h cone-descent-Σ
+  iff-descent-Σ = (descent-Σ , descent-Σ')
 ```
diff --git a/src/foundation/descent-empty-types.lagda.md b/src/foundation/descent-empty-types.lagda.md
index ca408517a6c..d210092e824 100644
--- a/src/foundation/descent-empty-types.lagda.md
+++ b/src/foundation/descent-empty-types.lagda.md
@@ -17,6 +17,23 @@ open import foundation-core.pullbacks
 
 </details>
 
+## Idea
+
+The
+{{#concept "descent property" Disambiguation="of empty types" Agda=descent-empty}}
+of [empty types](foundation-core.empty-types.md) states that every
+[cone](foundation.cones-over-cospan-diagrams.md) of the form
+
+```text
+  C ------> ∅
+  |         |
+  |         |
+  ∨         ∨
+  B ------> X
+```
+
+is a [pullback](foundation-core.pullbacks.md).
+
 ## Theorem
 
 ```agda
diff --git a/src/foundation/descent-equivalences.lagda.md b/src/foundation/descent-equivalences.lagda.md
index 2a2da46991e..ecc84288184 100644
--- a/src/foundation/descent-equivalences.lagda.md
+++ b/src/foundation/descent-equivalences.lagda.md
@@ -21,21 +21,24 @@ open import foundation-core.pullbacks
 
 ## Idea
 
-The descent property of equivalences is a somewhat degenerate form of a descent
-property. It asserts that in a commuting diagram of the form
+The
+{{#concept "descent property" Disambiguation="of equivalences" Agda=descent-is-equiv Agda=descent-equiv}}
+of [equivalences](foundation-core.equivalences.md) is a somewhat degenerate form
+of a descent property. It asserts that in a commuting diagram of the form
 
 ```text
-     p        q
- A -----> B -----> C
- |        |        |
-f|       g|        |h
- ∨        ∨        ∨
- X -----> Y -----> Z,
-     i        j
+       p        q
+   A -----> B -----> C
+   |        |        |
+  f|       g|        |h
+   ∨        ∨        ∨
+   X -----> Y -----> Z,
+       i        j
 ```
 
-if the maps `i` and `p` are equivalences, then the right square is a pullback if
-and only if the outer rectangle is a pullback.
+if the maps `i` and `p` are equivalences, then the right square is a
+[pullback](foundation-core.pullbacks.md) if and only if the outer rectangle is a
+pullback.
 
 ## Theorem
 
diff --git a/src/synthetic-homotopy-theory/dependent-descent-circle.lagda.md b/src/synthetic-homotopy-theory/dependent-descent-circle.lagda.md
index a847a0abfaa..1e4b4150e31 100644
--- a/src/synthetic-homotopy-theory/dependent-descent-circle.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-descent-circle.lagda.md
@@ -29,14 +29,16 @@ 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](synthetic-homotopy-theory.circle.md) is
-[equivalently](foundation-core.equivalences.md) described by **dependent descent
-data** over the [descent data](synthetic-homotopy-theory.descent-circle.md) of
-`P`, which is defined as a
+The {{#concept "dependent descent property" Disambiguation="of the circle"}} of
+the [circle](synthetic-homotopy-theory.circle.md) asserts that a family `P` over
+descent data on the circle is [equivalently](foundation-core.equivalences.md)
+described by
+{{#concept "dependent descent data" Disambiguation="for the circle" Agda=dependent-descent-data-circle}}
+over the [descent data](synthetic-homotopy-theory.descent-circle.md) of `P`,
+which is defined as a
 [dependent type with an automorphism](structured-types.dependent-types-equipped-with-automorphisms.md).
 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
+consists of a type family `R : X → 𝒰` equipped with a family of equivalences
 `k : (x : X) → R(x) ≃ R(e(x))` _over_ `e`.
 
 ## Definitions
@@ -339,9 +341,9 @@ module _
 
 ### 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
+Given a type family `A : 𝕊¹ → 𝒰` with corresponding descent data `(X, e)`, and a
+type family `R : X → 𝒰` over `X` invariant under `e` as witnessed by `k`, there
+is a unique family `B : (t : 𝕊¹) → A t → 𝒰` for which `(R, k)` is dependent
 descent data over `A`.
 
 This is so far a conjecture which remains to be shown.
diff --git a/src/synthetic-homotopy-theory/descent-circle-subtypes.lagda.md b/src/synthetic-homotopy-theory/descent-circle-subtypes.lagda.md
index b08f68dd4cd..c2884f473fb 100644
--- a/src/synthetic-homotopy-theory/descent-circle-subtypes.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-circle-subtypes.lagda.md
@@ -30,9 +30,9 @@ open import synthetic-homotopy-theory.universal-property-circle
 
 ## Idea
 
-Given a family `A : 𝕊¹ → U` over the
+Given a family `A : 𝕊¹ → 𝒰` over the
 [circle](synthetic-homotopy-theory.circle.md) and a family
-`B : (t : 𝕊¹) → (A t) → U` over `A` with corresponding
+`B : (t : 𝕊¹) → (A t) → 𝒰` over `A` with corresponding
 [descent data](synthetic-homotopy-theory.descent-circle.md) `(X, e)` and
 dependent descent data `(R, k)`, where `R` is a
 [subtype](foundation-core.subtypes.md) of `X`, we get that dependent functions
diff --git a/src/synthetic-homotopy-theory/descent-circle.lagda.md b/src/synthetic-homotopy-theory/descent-circle.lagda.md
index 8adc5c7904e..401ca713337 100644
--- a/src/synthetic-homotopy-theory/descent-circle.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-circle.lagda.md
@@ -1,4 +1,4 @@
-# The descent property of the circle
+# Descent for the circle
 
 ```agda
 module synthetic-homotopy-theory.descent-circle where
@@ -35,8 +35,10 @@ open import synthetic-homotopy-theory.universal-property-circle
 
 ## Idea
 
-The **descent property** of the [circle](synthetic-homotopy-theory.circle.md)
-uniquely characterizes type families over the circle.
+The
+{{#concept "descent property" Disambiguation="of the circle" Agda=unique-family-property-universal-property-circle}}
+of the [circle](synthetic-homotopy-theory.circle.md) uniquely characterizes type
+families over the circle.
 
 ## Definitions
 
@@ -44,8 +46,8 @@ uniquely characterizes type families over the circle.
 
 By the
 [universal property of the circle](synthetic-homotopy-theory.universal-property-circle.md)
-and [univalence](foundation.univalence.md), a type family `A : 𝕊¹ → U` over the
-[circle](synthetic-homotopy-theory.circle.md) is equivalent to a type `X : U`
+and [univalence](foundation.univalence.md), a type family `A : 𝕊¹ → 𝒰` over the
+[circle](synthetic-homotopy-theory.circle.md) is equivalent to a type `X : 𝒰`
 equipped with an [automorphism](foundation.automorphisms.md) `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.
@@ -124,10 +126,10 @@ module _
 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
+**Descent data for a family** `A : 𝕊¹ → 𝒰` 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,
+A **family with descent data** is a family `A : 𝕊¹ → 𝒰` over the circle,
 equipped with descent data `(X, e)`, and a proof of their equivalence. This can
 be described as a diagram
 
@@ -305,7 +307,7 @@ module _
 ### 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.
+`𝓓(X, e) : 𝕊¹ → 𝒰` for which `(X, e)` is descent data.
 
 ```agda
 comparison-descent-data-circle :
diff --git a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
index 5d8b09bc77c..fed387b2cb5 100644
--- a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
@@ -1,4 +1,4 @@
-# Descent property of pushouts
+# Descent for pushouts
 
 ```agda
 module synthetic-homotopy-theory.descent-property-pushouts where
@@ -34,7 +34,7 @@ open import synthetic-homotopy-theory.universal-property-pushouts
 ## Idea
 
 The
-{{#concept "descent property" Disambiguation="pushouts" Agda=uniqueness-family-cocone-descent-data-pushout WDID=Q5263725 WD="descent"}}
+{{#concept "descent property" Disambiguation="of pushouts" Agda=uniqueness-family-cocone-descent-data-pushout WDID=Q5263725 WD="descent"}}
 of [pushouts](synthetic-homotopy-theory.pushouts.md) states that given a pushout
 
 ```text
diff --git a/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md
index 20b9c33dc73..8d95c77644a 100644
--- a/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md
@@ -1,4 +1,4 @@
-# Descent property of sequential colimits
+# Descent for sequential colimits
 
 ```agda
 module synthetic-homotopy-theory.descent-property-sequential-colimits where

From 569052f19648c44b0b811834377c038aee45fa38 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 13:11:36 +0000
Subject: [PATCH 02/10] table on descent properties

---
 docs/tables/descent-properties.md                        | 9 +++++++++
 src/foundation/descent-coproduct-types.lagda.md          | 4 ++++
 src/foundation/descent-dependent-pair-types.lagda.md     | 4 ++++
 src/foundation/descent-empty-types.lagda.md              | 4 ++++
 src/foundation/descent-equivalences.lagda.md             | 4 ++++
 src/synthetic-homotopy-theory/descent-circle.lagda.md    | 8 ++++++++
 .../descent-property-pushouts.lagda.md                   | 4 ++++
 .../descent-property-sequential-colimits.lagda.md        | 4 ++++
 8 files changed, 41 insertions(+)
 create mode 100644 docs/tables/descent-properties.md

diff --git a/docs/tables/descent-properties.md b/docs/tables/descent-properties.md
new file mode 100644
index 00000000000..c0c36d21baf
--- /dev/null
+++ b/docs/tables/descent-properties.md
@@ -0,0 +1,9 @@
+| Concept                          | File                                                                                                                                  |
+| -------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------- |
+| Descent for coproduct types      | [`foundation.descent-coproduct-types`](foundation.descent-coproduct-types.md)                                                         |
+| Descent for dependent pair types | [`foundation.descent-dependent-pair-types`](foundation.descent-pair-types.md)                                                         |
+| Descent for empty types          | [`foundation.descent-empty-types`](foundation.descent-empty-types.md)                                                                 |
+| Descent for equivalences         | [`foundation.descent-equivalences`](foundation.descent-equivalences.md)                                                               |
+| Descent for pushouts             | [`synthetic-homotopy-theory.descent-property-pushouts`](synthetic-homotopy-theory.descent-property-pushouts.md)                       |
+| Descent for sequential colimits  | [`synthetic-homotopy-theory.descent-property-sequential-colimits`](synthetic-homotopy-theory.descent-property-sequential-colimits.md) |
+| Descent for the circle           | [`synthetic-homotopy-theory.descent-circle`](synthetic-homotopy-theory.descent-circle.md)                                             |
diff --git a/src/foundation/descent-coproduct-types.lagda.md b/src/foundation/descent-coproduct-types.lagda.md
index dbf7559e115..f7181b651fc 100644
--- a/src/foundation/descent-coproduct-types.lagda.md
+++ b/src/foundation/descent-coproduct-types.lagda.md
@@ -227,3 +227,7 @@ module _
       ( λ is-pb-dsq →
         ( descent-coproduct-inl is-pb-dsq , descent-coproduct-inr is-pb-dsq)))
 ```
+
+## Table of descent properties
+
+{{#include tables/descent-properties.md}}
diff --git a/src/foundation/descent-dependent-pair-types.lagda.md b/src/foundation/descent-dependent-pair-types.lagda.md
index 9e6a5b6cdb2..0fd13c4d6dc 100644
--- a/src/foundation/descent-dependent-pair-types.lagda.md
+++ b/src/foundation/descent-dependent-pair-types.lagda.md
@@ -131,3 +131,7 @@ module _
     is-pullback (rec-Σ f) h cone-descent-Σ
   iff-descent-Σ = (descent-Σ , descent-Σ')
 ```
+
+## Table of descent properties
+
+{{#include tables/descent-properties.md}}
diff --git a/src/foundation/descent-empty-types.lagda.md b/src/foundation/descent-empty-types.lagda.md
index d210092e824..b23c11774ce 100644
--- a/src/foundation/descent-empty-types.lagda.md
+++ b/src/foundation/descent-empty-types.lagda.md
@@ -56,3 +56,7 @@ module _
       (p : C → empty) (q : C → B) → is-pullback ex-falso g (cone-empty p q)
     descent-empty' p q = descent-empty (cone-empty p q)
 ```
+
+## Table of descent properties
+
+{{#include tables/descent-properties.md}}
diff --git a/src/foundation/descent-equivalences.lagda.md b/src/foundation/descent-equivalences.lagda.md
index ecc84288184..13645b92473 100644
--- a/src/foundation/descent-equivalences.lagda.md
+++ b/src/foundation/descent-equivalences.lagda.md
@@ -99,3 +99,7 @@ module _
   descent-equiv i j h c d =
     descent-is-equiv (map-equiv i) j h c d (is-equiv-map-equiv i)
 ```
+
+## Table of descent properties
+
+{{#include tables/descent-properties.md}}
diff --git a/src/synthetic-homotopy-theory/descent-circle.lagda.md b/src/synthetic-homotopy-theory/descent-circle.lagda.md
index 401ca713337..9a27a90e2c9 100644
--- a/src/synthetic-homotopy-theory/descent-circle.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-circle.lagda.md
@@ -394,3 +394,11 @@ module _
   pr2 (pr2 (family-with-descent-data-circle-descent-data P)) =
     pr2 (family-for-descent-data-circle-descent-data P)
 ```
+
+## See also
+
+We also have a series of files for descent on the circle of particular forms.
+
+## Table of descent properties
+
+{{#include tables/descent-properties.md}}
diff --git a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
index fed387b2cb5..e90482fde0b 100644
--- a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
@@ -299,3 +299,7 @@ module _
   pr2 (pr2 family-with-descent-data-pushout-descent-data-pushout) =
     equiv-family-cocone-descent-data-pushout
 ```
+
+## Table of descent properties
+
+{{#include tables/descent-properties.md}}
diff --git a/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md
index 8d95c77644a..83aef9cf461 100644
--- a/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md
@@ -135,3 +135,7 @@ module _
     map-inv-equiv
       ( equiv-descent-data-family-cocone-sequential-diagram)
 ```
+
+## Table of descent properties
+
+{{#include tables/descent-properties.md}}

From 42862bb38f1e32d82b88611e62b718b15d26460a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 13:15:26 +0000
Subject: [PATCH 03/10] rename two files for consistent naming

---
 src/synthetic-homotopy-theory.lagda.md                        | 4 ++--
 ...t-property-pushouts.lagda.md => descent-pushouts.lagda.md} | 0
 ...colimits.lagda.md => descent-sequential-colimits.lagda.md} | 0
 3 files changed, 2 insertions(+), 2 deletions(-)
 rename src/synthetic-homotopy-theory/{descent-property-pushouts.lagda.md => descent-pushouts.lagda.md} (100%)
 rename src/synthetic-homotopy-theory/{descent-property-sequential-colimits.lagda.md => descent-sequential-colimits.lagda.md} (100%)

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 2839f2a8162..2134196f5c5 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -54,8 +54,8 @@ open import synthetic-homotopy-theory.descent-data-function-types-over-pushouts
 open import synthetic-homotopy-theory.descent-data-identity-types-over-pushouts public
 open import synthetic-homotopy-theory.descent-data-pushouts public
 open import synthetic-homotopy-theory.descent-data-sequential-colimits public
-open import synthetic-homotopy-theory.descent-property-pushouts public
-open import synthetic-homotopy-theory.descent-property-sequential-colimits public
+open import synthetic-homotopy-theory.descent-pushouts public
+open import synthetic-homotopy-theory.descent-sequential-colimits public
 open import synthetic-homotopy-theory.double-loop-spaces public
 open import synthetic-homotopy-theory.eckmann-hilton-argument public
 open import synthetic-homotopy-theory.equifibered-sequential-diagrams public
diff --git a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-pushouts.lagda.md
similarity index 100%
rename from src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md
rename to src/synthetic-homotopy-theory/descent-pushouts.lagda.md
diff --git a/src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/descent-sequential-colimits.lagda.md
similarity index 100%
rename from src/synthetic-homotopy-theory/descent-property-sequential-colimits.lagda.md
rename to src/synthetic-homotopy-theory/descent-sequential-colimits.lagda.md

From 8c80965f93c66f958547a626b96d664dc7e89b0a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 13:20:01 +0000
Subject: [PATCH 04/10] edit

---
 src/foundation/descent-coproduct-types.lagda.md | 17 ++++-------------
 1 file changed, 4 insertions(+), 13 deletions(-)

diff --git a/src/foundation/descent-coproduct-types.lagda.md b/src/foundation/descent-coproduct-types.lagda.md
index f7181b651fc..bad6ac5b759 100644
--- a/src/foundation/descent-coproduct-types.lagda.md
+++ b/src/foundation/descent-coproduct-types.lagda.md
@@ -105,7 +105,7 @@ module _
 
   cone-descent-coproduct :
     cone (rec-coproduct f g) i (A' + B')
-  pr1 (cone-descent-coproduct) = map-coproduct h k
+  pr1 cone-descent-coproduct = map-coproduct h k
   pr1 (pr2 cone-descent-coproduct) (inl a') = f' a'
   pr1 (pr2 cone-descent-coproduct) (inr b') = g' b'
   pr2 (pr2 cone-descent-coproduct) (inl a') = H a'
@@ -152,10 +152,7 @@ module _
     descent-coproduct :
       is-pullback f i α →
       is-pullback g i β →
-      is-pullback
-        ( rec-coproduct f g)
-        ( i)
-        ( cone-descent-coproduct)
+      is-pullback (rec-coproduct f g) i cone-descent-coproduct
     descent-coproduct is-pb-α is-pb-β =
       is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone
         ( rec-coproduct f g)
@@ -167,10 +164,7 @@ module _
 
   abstract
     descent-coproduct-inl :
-      is-pullback
-        ( rec-coproduct f g)
-        ( i)
-        ( cone-descent-coproduct) →
+      is-pullback (rec-coproduct f g) i cone-descent-coproduct →
       is-pullback f i α
     descent-coproduct-inl is-pb-dsq =
       is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone f i
@@ -194,10 +188,7 @@ module _
 
   abstract
     descent-coproduct-inr :
-      is-pullback
-        ( rec-coproduct f g)
-        ( i)
-        ( cone-descent-coproduct) →
+      is-pullback (rec-coproduct f g) i cone-descent-coproduct →
       is-pullback g i β
     descent-coproduct-inr is-pb-dsq =
       is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone g i

From 8a8c807fd12b2112f6a80a57c034f38caa3162b5 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 13:21:55 +0000
Subject: [PATCH 05/10] edit

---
 .../descent-circle-dependent-pair-types.lagda.md              | 4 ++--
 .../descent-circle-equivalence-types.lagda.md                 | 2 +-
 .../descent-circle-function-types.lagda.md                    | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/synthetic-homotopy-theory/descent-circle-dependent-pair-types.lagda.md b/src/synthetic-homotopy-theory/descent-circle-dependent-pair-types.lagda.md
index b9abaf71f4c..dca09b7ebe5 100644
--- a/src/synthetic-homotopy-theory/descent-circle-dependent-pair-types.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-circle-dependent-pair-types.lagda.md
@@ -22,9 +22,9 @@ open import synthetic-homotopy-theory.free-loops
 
 ## Idea
 
-Given a family `A : 𝕊¹ → U` over the
+Given a family `A : 𝕊¹ → 𝒰` over the
 [circle](synthetic-homotopy-theory.circle.md) and a family
-`B : (t : 𝕊¹) → (A t) → U` over `A`, the
+`B : (t : 𝕊¹) → (A t) → 𝒰` over `A`, the
 [descent data](synthetic-homotopy-theory.descent-circle.md) for the family of
 [dependent pair types](foundation.dependent-pair-types.md) `λ t → Σ (A t) (B t)`
 is `(Σ X R, map-Σ e k)`, where `(X, e)` is descent data for `A` and `(R, k)` is
diff --git a/src/synthetic-homotopy-theory/descent-circle-equivalence-types.lagda.md b/src/synthetic-homotopy-theory/descent-circle-equivalence-types.lagda.md
index cec4371a5e0..9023ae65f61 100644
--- a/src/synthetic-homotopy-theory/descent-circle-equivalence-types.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-circle-equivalence-types.lagda.md
@@ -28,7 +28,7 @@ open import synthetic-homotopy-theory.universal-property-circle
 
 ## Idea
 
-Given two families `A, B : 𝕊¹ → U` over the
+Given two families `A, B : 𝕊¹ → 𝒰` over the
 [circle](synthetic-homotopy-theory.circle.md), to show that they are
 [equivalent](foundation.equivalences.md) is the same as showing that their
 [descent data](synthetic-homotopy-theory.descent-circle.md) is equivalent.
diff --git a/src/synthetic-homotopy-theory/descent-circle-function-types.lagda.md b/src/synthetic-homotopy-theory/descent-circle-function-types.lagda.md
index 447911b4677..54e6fb7f078 100644
--- a/src/synthetic-homotopy-theory/descent-circle-function-types.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-circle-function-types.lagda.md
@@ -35,7 +35,7 @@ open import synthetic-homotopy-theory.universal-property-circle
 
 ## Idea
 
-Given two families `A, B : 𝕊¹ → U` over the
+Given two families `A, B : 𝕊¹ → 𝒰` over the
 [circle](synthetic-homotopy-theory.circle.md), the
 [descent data](synthetic-homotopy-theory.descent-circle.md) for the family of
 function types `λ t → (A t → B t)` is `(X → Y, λ h → f ∘ h ∘ e⁻¹)`, where

From 985a6018dfce0ef5acd6d3120923b01d5cd6721a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 13:31:47 +0000
Subject: [PATCH 06/10] fix links

---
 docs/tables/descent-properties.md              | 18 +++++++++---------
 .../descent-data-pushouts.lagda.md             |  3 +--
 .../descent-data-sequential-colimits.lagda.md  |  2 +-
 .../descent-pushouts.lagda.md                  |  2 +-
 .../descent-sequential-colimits.lagda.md       |  2 +-
 .../families-descent-data-pushouts.lagda.md    |  3 +--
 ...s-descent-data-sequential-colimits.lagda.md |  2 +-
 ...tity-systems-descent-data-pushouts.lagda.md |  7 +++----
 .../mathers-second-cube-theorem.lagda.md       |  2 +-
 9 files changed, 19 insertions(+), 22 deletions(-)

diff --git a/docs/tables/descent-properties.md b/docs/tables/descent-properties.md
index c0c36d21baf..35457fdd55c 100644
--- a/docs/tables/descent-properties.md
+++ b/docs/tables/descent-properties.md
@@ -1,9 +1,9 @@
-| Concept                          | File                                                                                                                                  |
-| -------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------- |
-| Descent for coproduct types      | [`foundation.descent-coproduct-types`](foundation.descent-coproduct-types.md)                                                         |
-| Descent for dependent pair types | [`foundation.descent-dependent-pair-types`](foundation.descent-pair-types.md)                                                         |
-| Descent for empty types          | [`foundation.descent-empty-types`](foundation.descent-empty-types.md)                                                                 |
-| Descent for equivalences         | [`foundation.descent-equivalences`](foundation.descent-equivalences.md)                                                               |
-| Descent for pushouts             | [`synthetic-homotopy-theory.descent-property-pushouts`](synthetic-homotopy-theory.descent-property-pushouts.md)                       |
-| Descent for sequential colimits  | [`synthetic-homotopy-theory.descent-property-sequential-colimits`](synthetic-homotopy-theory.descent-property-sequential-colimits.md) |
-| Descent for the circle           | [`synthetic-homotopy-theory.descent-circle`](synthetic-homotopy-theory.descent-circle.md)                                             |
+| Concept                          | File                                                                                                                |
+| -------------------------------- | ------------------------------------------------------------------------------------------------------------------- |
+| Descent for coproduct types      | [`foundation.descent-coproduct-types`](foundation.descent-coproduct-types.md)                                       |
+| Descent for dependent pair types | [`foundation.descent-dependent-pair-types`](foundation.descent-dependent-pair-types.md)                             |
+| Descent for empty types          | [`foundation.descent-empty-types`](foundation.descent-empty-types.md)                                               |
+| Descent for equivalences         | [`foundation.descent-equivalences`](foundation.descent-equivalences.md)                                             |
+| Descent for pushouts             | [`synthetic-homotopy-theory.descent-pushouts`](synthetic-homotopy-theory.descent-pushouts.md)                       |
+| Descent for sequential colimits  | [`synthetic-homotopy-theory.descent-sequential-colimits`](synthetic-homotopy-theory.descent-sequential-colimits.md) |
+| Descent for the circle           | [`synthetic-homotopy-theory.descent-circle`](synthetic-homotopy-theory.descent-circle.md)                           |
diff --git a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
index 0b9cb64d427..4319d3ad7e9 100644
--- a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
@@ -39,8 +39,7 @@ is a triple `(PA, PB, PS)`, where `PA : A → 𝒰` is a type family over `A`,
   PS : (s : S) → PA (f a) ≃ PB (g a).
 ```
 
-In
-[`descent-property-pushouts`](synthetic-homotopy-theory.descent-property-pushouts.md),
+In [`descent-property-pushouts`](synthetic-homotopy-theory.descent-pushouts.md),
 we show that this is exactly the data one needs to "glue together" a type family
 `P : X → 𝒰` over the pushout `X` of `𝒮`.
 
diff --git a/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md
index 96d19a16e03..53c249daf4e 100644
--- a/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md
@@ -36,7 +36,7 @@ for sequential colimits, and it is exactly an
 
 The fact that the type of descent data for a sequential diagram is equivalent to
 the type of type families over its colimit is recorded in
-[`descent-property-sequential-colimits`](synthetic-homotopy-theory.descent-property-sequential-colimits.md).
+[`descent-property-sequential-colimits`](synthetic-homotopy-theory.descent-sequential-colimits.md).
 
 ## Definitions
 
diff --git a/src/synthetic-homotopy-theory/descent-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-pushouts.lagda.md
index e90482fde0b..d0af17043be 100644
--- a/src/synthetic-homotopy-theory/descent-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-pushouts.lagda.md
@@ -1,7 +1,7 @@
 # Descent for pushouts
 
 ```agda
-module synthetic-homotopy-theory.descent-property-pushouts where
+module synthetic-homotopy-theory.descent-pushouts where
 ```
 
 <details><summary>Imports</summary>
diff --git a/src/synthetic-homotopy-theory/descent-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/descent-sequential-colimits.lagda.md
index 83aef9cf461..e4c07465a85 100644
--- a/src/synthetic-homotopy-theory/descent-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-sequential-colimits.lagda.md
@@ -1,7 +1,7 @@
 # Descent for sequential colimits
 
 ```agda
-module synthetic-homotopy-theory.descent-property-sequential-colimits where
+module synthetic-homotopy-theory.descent-sequential-colimits where
 ```
 
 <details><summary>Imports</summary>
diff --git a/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
index 62d678d3b20..cebfceb1cc8 100644
--- a/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
@@ -23,8 +23,7 @@ open import synthetic-homotopy-theory.equivalences-descent-data-pushouts
 
 ## Idea
 
-In
-[`descent-property-pushouts`](synthetic-homotopy-theory.descent-property-pushouts.md)
+In [`descent-property-pushouts`](synthetic-homotopy-theory.descent-pushouts.md)
 we show that given
 [descent data](synthetic-homotopy-theory.descent-data-pushouts.md)
 `(PA, PB, PS)` over a [span diagram](foundation.span-diagrams.md) `𝒮`, there is
diff --git a/src/synthetic-homotopy-theory/families-descent-data-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/families-descent-data-sequential-colimits.lagda.md
index 4343695a692..0033a4bf337 100644
--- a/src/synthetic-homotopy-theory/families-descent-data-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/families-descent-data-sequential-colimits.lagda.md
@@ -26,7 +26,7 @@ open import synthetic-homotopy-theory.sequential-diagrams
 ## Idea
 
 As shown in
-[`descent-property-sequential-colimits`](synthetic-homotopy-theory.descent-property-sequential-colimits.md),
+[`descent-property-sequential-colimits`](synthetic-homotopy-theory.descent-sequential-colimits.md),
 the type of type families over
 [sequential colimits](synthetic-homotopy-theory.universal-property-sequential-colimits.md)
 is [equivalent](foundation-core.equivalences.md) to
diff --git a/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md
index d6b2c7d3f50..682977273ca 100644
--- a/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md
@@ -33,7 +33,7 @@ open import synthetic-homotopy-theory.dependent-universal-property-pushouts
 open import synthetic-homotopy-theory.descent-data-equivalence-types-over-pushouts
 open import synthetic-homotopy-theory.descent-data-identity-types-over-pushouts
 open import synthetic-homotopy-theory.descent-data-pushouts
-open import synthetic-homotopy-theory.descent-property-pushouts
+open import synthetic-homotopy-theory.descent-pushouts
 open import synthetic-homotopy-theory.equivalences-descent-data-pushouts
 open import synthetic-homotopy-theory.families-descent-data-pushouts
 open import synthetic-homotopy-theory.flattening-lemma-pushouts
@@ -71,9 +71,8 @@ and a point `p₀ : PA a₀` over a basepoint `a₀ : A`, we would like to mirro
 definition of identity systems. A naïve translation would lead us to define
 dependent descent data and its sections. We choose to sidestep building that
 technical infrastructure. By the
-[descent property](synthetic-homotopy-theory.descent-property-pushouts.md),
-there is a [unique](foundation-core.contractible-types.md) type family
-`P : X → 𝒰`
+[descent property](synthetic-homotopy-theory.descent-pushouts.md), there is a
+[unique](foundation-core.contractible-types.md) type family `P : X → 𝒰`
 [corresponding](synthetic-homotopy-theory.families-descent-data-pushouts.md) to
 `(PA, PB, PS)`. Observe that the type of dependent type families
 `(x : X) → (p : P x) → 𝒰` is [equivalent](foundation-core.equivalences.md) to
diff --git a/src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md b/src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md
index cb7ed902260..30e6f780489 100644
--- a/src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md
+++ b/src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md
@@ -148,7 +148,7 @@ module _
   [unstraightened](foundation.type-duality.md) version of the
   [flattening lemma for pushouts](synthetic-homotopy-theory.flattening-lemma-pushouts.md)
 - The
-  [descent property for pushouts](synthetic-homotopy-theory.descent-property-pushouts.md).
+  [descent property for pushouts](synthetic-homotopy-theory.descent-pushouts.md).
 
 ## External links
 

From 450dc41483be9004f51892b371140edcec426fea Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 13:31:59 +0000
Subject: [PATCH 07/10] see also section `descent-circle`

---
 src/synthetic-homotopy-theory/descent-circle.lagda.md | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/descent-circle.lagda.md b/src/synthetic-homotopy-theory/descent-circle.lagda.md
index 9a27a90e2c9..fc09848fbc9 100644
--- a/src/synthetic-homotopy-theory/descent-circle.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-circle.lagda.md
@@ -397,7 +397,13 @@ module _
 
 ## See also
 
-We also have a series of files for descent on the circle of particular forms.
+- [Dependent descent for the circle](synthetic-homotopy-theory.dependent-descent-circle.md)
+- [Descent data for constant type families over the circle](synthetic-homotopy-theory.descent-circle-constant-families.md)
+- [Descent data for families of dependent pair types over the circle](synthetic-homotopy-theory.descent-circle-dependent-pair-types.md)
+- [Descent data for families of equivalence types over the circle](synthetic-homotopy-theory.descent-circle-equivalence-types.md)
+- [Descent data for families of function types over the circle](synthetic-homotopy-theory.descent-circle-function-types.md)
+- [Sections of families over the circle](synthetic-homotopy-theory.sections-descent-circle.md)
+- [Subtypes of descent data for the circle](synthetic-homotopy-theory.descent-circle-subtypes.md)
 
 ## Table of descent properties
 

From fa9d309b6787323367517655cecddecc23e90aa0 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 14:29:40 +0000
Subject: [PATCH 08/10] fix link text

---
 src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md | 4 ++--
 .../families-descent-data-pushouts.lagda.md                  | 5 ++---
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
index 4319d3ad7e9..a67082088f7 100644
--- a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md
@@ -39,8 +39,8 @@ is a triple `(PA, PB, PS)`, where `PA : A → 𝒰` is a type family over `A`,
   PS : (s : S) → PA (f a) ≃ PB (g a).
 ```
 
-In [`descent-property-pushouts`](synthetic-homotopy-theory.descent-pushouts.md),
-we show that this is exactly the data one needs to "glue together" a type family
+In [`descent-pushouts`](synthetic-homotopy-theory.descent-pushouts.md), we show
+that this is exactly the data one needs to "glue together" a type family
 `P : X → 𝒰` over the pushout `X` of `𝒮`.
 
 The [identity type](foundation-core.identity-types.md) of descent data is
diff --git a/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
index cebfceb1cc8..488b6f5f058 100644
--- a/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md
@@ -23,9 +23,8 @@ open import synthetic-homotopy-theory.equivalences-descent-data-pushouts
 
 ## Idea
 
-In [`descent-property-pushouts`](synthetic-homotopy-theory.descent-pushouts.md)
-we show that given
-[descent data](synthetic-homotopy-theory.descent-data-pushouts.md)
+In [`descent-pushouts`](synthetic-homotopy-theory.descent-pushouts.md) we show
+that given [descent data](synthetic-homotopy-theory.descent-data-pushouts.md)
 `(PA, PB, PS)` over a [span diagram](foundation.span-diagrams.md) `𝒮`, there is
 a unique type family `P` over its
 [pushout](synthetic-homotopy-theory.pushouts.md) such that its induced descent

From 6cc73b69cd49b78e82412294dc99daa39b23cc2c Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 27 Nov 2025 15:12:09 +0000
Subject: [PATCH 09/10] edits descent

---
 .../descent-dependent-pair-types.lagda.md     |   6 +
 src/foundation/descent-equivalences.lagda.md  | 106 ++++++++++++------
 2 files changed, 79 insertions(+), 33 deletions(-)

diff --git a/src/foundation/descent-dependent-pair-types.lagda.md b/src/foundation/descent-dependent-pair-types.lagda.md
index 0fd13c4d6dc..a4952f250e4 100644
--- a/src/foundation/descent-dependent-pair-types.lagda.md
+++ b/src/foundation/descent-dependent-pair-types.lagda.md
@@ -54,6 +54,8 @@ for every `i`, then the family is a family of
 
 is a pullback cone.
 
+This descent property appears as Theorem 2.2 in {{#cite CR21}}.
+
 ## Theorem
 
 ```agda
@@ -132,6 +134,10 @@ module _
   iff-descent-Σ = (descent-Σ , descent-Σ')
 ```
 
+## References
+
+{{#bibliography}}
+
 ## Table of descent properties
 
 {{#include tables/descent-properties.md}}
diff --git a/src/foundation/descent-equivalences.lagda.md b/src/foundation/descent-equivalences.lagda.md
index 13645b92473..308757ef747 100644
--- a/src/foundation/descent-equivalences.lagda.md
+++ b/src/foundation/descent-equivalences.lagda.md
@@ -8,9 +8,11 @@ module foundation.descent-equivalences where
 
 ```agda
 open import foundation.cones-over-cospan-diagrams
+open import foundation.dependent-pair-types
 open import foundation.dependent-universal-property-equivalences
 open import foundation.equivalences
 open import foundation.functoriality-fibers-of-maps
+open import foundation.logical-equivalences
 open import foundation.universe-levels
 
 open import foundation-core.function-types
@@ -22,18 +24,18 @@ open import foundation-core.pullbacks
 ## Idea
 
 The
-{{#concept "descent property" Disambiguation="of equivalences" Agda=descent-is-equiv Agda=descent-equiv}}
+{{#concept "descent property" Disambiguation="of equivalences" Agda=iff-descent-equiv}}
 of [equivalences](foundation-core.equivalences.md) is a somewhat degenerate form
 of a descent property. It asserts that in a commuting diagram of the form
 
 ```text
-       p        q
-   A -----> B -----> C
-   |        |        |
-  f|       g|        |h
-   ∨        ∨        ∨
-   X -----> Y -----> Z,
-       i        j
+        p         q
+   A ------> B ------> C
+   |         |         |
+  f|        g|         |h
+   ∨         ∨         ∨
+   X ------> Y ------> Z,
+        i         j
 ```
 
 if the maps `i` and `p` are equivalences, then the right square is a
@@ -50,8 +52,10 @@ module _
 
   descent-is-equiv :
     (i : X → Y) (j : Y → Z) (h : C → Z)
-    (c : cone j h B) (d : cone i (vertical-map-cone j h c) A) →
-    is-equiv i → is-equiv (horizontal-map-cone i (vertical-map-cone j h c) d) →
+    (c : cone j h B)
+    (d : cone i (vertical-map-cone j h c) A) →
+    is-equiv i →
+    is-equiv (horizontal-map-cone i (vertical-map-cone j h c) d) →
     is-pullback (j ∘ i) h (pasting-horizontal-cone i j h c d) →
     is-pullback j h c
   descent-is-equiv i j h c d
@@ -62,34 +66,40 @@ module _
         ( λ y → is-equiv (map-fiber-vertical-map-cone j h c y))
         ( λ x →
           is-equiv-right-map-triangle
-          ( map-fiber-vertical-map-cone (j ∘ i) h
-            ( pasting-horizontal-cone i j h c d) x)
-          ( map-fiber-vertical-map-cone j h c (i x))
-          ( map-fiber-vertical-map-cone i (vertical-map-cone j h c) d x)
-          ( preserves-pasting-horizontal-map-fiber-vertical-map-cone
-            ( i)
-            ( j)
-            ( h)
-            ( c)
-            ( d)
-            ( x))
-          ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback (j ∘ i) h
-            ( pasting-horizontal-cone i j h c d)
-            ( is-pb-rectangle)
-            ( x))
-          ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback i
-            ( vertical-map-cone j h c)
-            ( d)
-            ( is-pullback-is-equiv-horizontal-maps i
+            ( map-fiber-vertical-map-cone (j ∘ i) h
+              ( pasting-horizontal-cone i j h c d)
+              ( x))
+            ( map-fiber-vertical-map-cone j h c (i x))
+            ( map-fiber-vertical-map-cone i (vertical-map-cone j h c) d x)
+            ( preserves-pasting-horizontal-map-fiber-vertical-map-cone
+              ( i)
+              ( j)
+              ( h)
+              ( c)
+              ( d)
+              ( x))
+            ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
+              ( j ∘ i)
+              ( h)
+              ( pasting-horizontal-cone i j h c d)
+              ( is-pb-rectangle)
+              ( x))
+            ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
+              ( i)
               ( vertical-map-cone j h c)
               ( d)
-              ( is-equiv-i)
-              ( is-equiv-k))
-            ( x))))
+              ( is-pullback-is-equiv-horizontal-maps
+                ( i)
+                ( vertical-map-cone j h c)
+                ( d)
+                ( is-equiv-i)
+                ( is-equiv-k))
+              ( x))))
 
   descent-equiv :
     (i : X ≃ Y) (j : Y → Z) (h : C → Z)
-    (c : cone j h B) (d : cone (map-equiv i) (vertical-map-cone j h c) A) →
+    (c : cone j h B)
+    (d : cone (map-equiv i) (vertical-map-cone j h c) A) →
     is-equiv (horizontal-map-cone (map-equiv i) (vertical-map-cone j h c) d) →
     is-pullback
       ( j ∘ map-equiv i)
@@ -98,6 +108,36 @@ module _
     is-pullback j h c
   descent-equiv i j h c d =
     descent-is-equiv (map-equiv i) j h c d (is-equiv-map-equiv i)
+
+  iff-descent-is-equiv :
+    (i : X → Y) (j : Y → Z) (h : C → Z)
+    (c : cone j h B)
+    (d : cone i (vertical-map-cone j h c) A) →
+    is-equiv i →
+    is-equiv (horizontal-map-cone i (vertical-map-cone j h c) d) →
+    is-pullback (j ∘ i) h (pasting-horizontal-cone i j h c d) ↔
+    is-pullback j h c
+  iff-descent-is-equiv i j h c d I P =
+    ( descent-is-equiv i j h c d I P ,
+      λ C →
+      is-pullback-rectangle-is-pullback-left-square i j h c d
+        ( C)
+        ( is-pullback-is-equiv-horizontal-maps i (vertical-map-cone j h c) d
+          ( I)
+          ( P)))
+
+  iff-descent-equiv :
+    (i : X ≃ Y) (j : Y → Z) (h : C → Z)
+    (c : cone j h B)
+    (d : cone (map-equiv i) (vertical-map-cone j h c) A) →
+    is-equiv (horizontal-map-cone (map-equiv i) (vertical-map-cone j h c) d) →
+    is-pullback
+      ( j ∘ map-equiv i)
+      ( h)
+      ( pasting-horizontal-cone (map-equiv i) j h c d) ↔
+    is-pullback j h c
+  iff-descent-equiv (i , I) j h c d =
+    iff-descent-is-equiv i j h c d I
 ```
 
 ## Table of descent properties

From c71297da73c8ac98d95f2fae1d741d3c8ee4c8b2 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sat, 29 Nov 2025 19:37:19 +0000
Subject: [PATCH 10/10] Fix formatting in descent-coproduct-types.lagda.md

---
 src/foundation/descent-coproduct-types.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/descent-coproduct-types.lagda.md b/src/foundation/descent-coproduct-types.lagda.md
index bad6ac5b759..5df7301727d 100644
--- a/src/foundation/descent-coproduct-types.lagda.md
+++ b/src/foundation/descent-coproduct-types.lagda.md
@@ -51,7 +51,7 @@ then the coproduct cone
 ```text
   A' + B' -----> X'
      |           |
-     |    α+β    | i
+     |   [α,β]   | i
      ∨           ∨
    A + B ------> X
 ```