#1118 except simplicial type theory

agda-unimath.agda-lib

@@ -1,3 +1,3 @@
 name: agda-unimath
 include: src
-flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions -WnoWithoutKFlagPrimEraseEquality --no-postfix-projections
+flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions --confluence-check -WnoWithoutKFlagPrimEraseEquality --no-postfix-projections

docs/DESIGN-PRINCIPLES.md

@@ -23,7 +23,7 @@ makes use of several postulates.
 6. The **truncation operations** are postulated in
    [`foundation.truncations`](foundation.truncations.md)
 7. The **interval** is postulated in
-   [`synthetic-homotopy-theory.interval-type`](synthetic-homotopy-theory.interval-type.md)
+   [`synthetic-homotopy-theory.interval`](synthetic-homotopy-theory.interval.md)
 8. The **circle** is postulated in
    [`synthetic-homotopy-theory.circle`](synthetic-homotopy-theory.circle.md)
 9. **Pushouts** are postulated in
@@ -39,8 +39,8 @@ makes use of several postulates.
 Note that there is some redundancy in the postulates we assume. For example, the
 [univalence axiom implies function extensionality](foundation.univalence-implies-function-extensionality.md),
 but we still assume function extensionality separately. Furthermore,
-[the interval type is contractible](synthetic-homotopy-theory.interval-type.md),
-and the higher inductive types in the agda-unimath library only have computation
+[the interval type is contractible](synthetic-homotopy-theory.interval.md), and
+the higher inductive types in the agda-unimath library only have computation
 rules up to identification, so there is no need at all to postulate it. The
 [circle](synthetic-homotopy-theory.circle.md) can be constructed as the type of
 `ℤ`-[torsors](group-theory.torsors.md), and the

references.bib

@@ -308,6 +308,22 @@ @article{CR21
   keywords      = {algebraic geometry,cohesive homotopy type theory,factorization systems,Homotopy type theory,modal homotopy type theory},
 }
 
+@article{CSY22,
+  title         = {Ambidexterity in chromatic homotopy theory},
+  author        = {Carmeli, Shachar and Schlank, Tomer M. and Yanovski, Lior},
+  year          = 2022,
+  journal       = {Invent. Math.},
+  fjournal      = {Inventiones Mathematicae},
+  volume        = 228,
+  number        = 3,
+  pages         = {1145--1254},
+  doi           = {10.1007/s00222-022-01099-9},
+  issn          = {0020-9910,1432-1297},
+  mrclass       = {55P43 (55P60)},
+  mrnumber      = 4419631,
+  mrreviewer    = {Lennart\ Meier},
+}
+
 @online{DavidJaz/Cohesion,
   title         = {DavidJaz/Cohesion},
   author        = {David Jaz Meyers},
@@ -717,7 +733,7 @@ @article{MP87
   issn          = {0021-8693},
 }
 
-@online{MR23,
+@online{MR23a,
   title         = {Delooping the Sign Homomorphism in Univalent Mathematics},
   author        = {Mangel, Éléonore and Rijke, Egbert},
   year          = 2023,
@@ -731,6 +747,19 @@ @online{MR23
   keywords      = {20B30 03B15,Mathematics - Group Theory,Mathematics - Logic},
 }
 
+@online{MR23b,
+  title         = {Commuting {{Cohesions}}},
+  author        = {Myers, David Jaz and Riley, Mitchell},
+  year          = 2023,
+  month         = {01},
+  date          = {2023-01-31},
+  eprint        = {2301.13780},
+  eprinttype    = {arxiv},
+  eprintclass   = {math},
+  abstract      = {Shulman's spatial type theory internalizes the modalities of Lawvere's axiomatic cohesion in a homotopy type theory, enabling many of the constructions from Schreiber's modal approach to differential cohomology to be carried out synthetically. In spatial type theory, every type carries a spatial cohesion among its points and every function is continuous with respect to this. But in mathematical practice, objects may be spatial in more than one way at the same time; for example, a simplicial space has both topological and simplicial structures. In this paper, we put forward a type theory with "commuting focuses" which allows for types to carry multiple kinds of spatial structure. The theory is a relatively painless extension of spatial type theory, and enables us to give a synthetic account of simplicial, differential, equivariant, and other cohesions carried by the same types. We demonstrate the theory by showing that the homotopy type of any differential stack may be computed from a discrete simplicial set derived from the \textbackslash v\{C\}ech nerve of any good cover. We also give other examples of commuting cohesions, such as differential equivariant types and supergeometric types, laying the groundwork for a synthetic account of Schreiber and Sati's proper orbifold cohomology.},
+  langid        = {english},
+}
+
 @book{MRR88,
   title         = {A {{Course}} in {{Constructive Algebra}}},
   author        = {Mines, Ray and Richman, Fred and Ruitenburg, Wim},
@@ -865,6 +894,24 @@ @online{Rij22draft
   pubstate      = {draft},
 }
 
+@misc{RS17,
+  title         = {A type theory for synthetic $\infty$-categories},
+  author        = {Riehl, Emily and Shulman, Michael},
+  year          = 2017,
+  journal       = {Higher Structures},
+  shortjournal  = {High. Struct.},
+  volume        = 1,
+  number        = 1,
+  pages         = {147--224},
+  issn          = {2209-0606},
+  eprint        = {1705.07442},
+  eprinttype    = {arxiv},
+  archiveprefix = {arXiv},
+  eprintclass   = {math},
+  primaryclass  = {math.CT},
+  url           = {https://emilyriehl.github.io/files/synthetic.pdf},
+}
+
 @article{RSS20,
   title         = {Modalities in Homotopy Type Theory},
   author        = {Rijke, Egbert and Shulman, Michael and Spitters, Bas},

src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md

@@ -205,4 +205,4 @@ module _
 
 ## References
 
-{{#bibliography}} {{#reference MR23}}
+{{#bibliography}} {{#reference MR23a}}

src/finite-group-theory/delooping-sign-homomorphism.lagda.md

@@ -1642,4 +1642,4 @@ module _
 
 ## References
 
-{{#bibliography}} {{#reference MR23}}
+{{#bibliography}} {{#reference MR23a}}

src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md

@@ -825,4 +825,4 @@ module _
 
 ## References
 
-{{#bibliography}} {{#reference MR23}}
+{{#bibliography}} {{#reference MR23a}}

src/foundation-core/truncated-types.lagda.md

@@ -21,7 +21,9 @@ open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
 open import foundation-core.homotopies
 open import foundation-core.identity-types
+open import foundation-core.invertible-maps
 open import foundation-core.propositions
+open import foundation-core.retractions
 open import foundation-core.retracts-of-types
 open import foundation-core.transport-along-identifications
 open import foundation-core.truncation-levels
@@ -76,8 +78,7 @@ module _
 abstract
   is-trunc-succ-is-trunc :
     (k : 𝕋) {l : Level} {A : UU l} → is-trunc k A → is-trunc (succ-𝕋 k) A
-  pr1 (is-trunc-succ-is-trunc neg-two-𝕋 H x y) = eq-is-contr H
-  pr2 (is-trunc-succ-is-trunc neg-two-𝕋 H x .x) refl = left-inv (pr2 H x)
+  is-trunc-succ-is-trunc neg-two-𝕋 = is-prop-is-contr
   is-trunc-succ-is-trunc (succ-𝕋 k) H x y = is-trunc-succ-is-trunc k (H x y)
 
 truncated-type-succ-Truncated-Type :
@@ -122,11 +123,11 @@ module _
   where
 
   is-trunc-retract-of :
-    {k : 𝕋} {A : UU l1} {B : UU l2} →
+    (k : 𝕋) {A : UU l1} {B : UU l2} →
     A retract-of B → is-trunc k B → is-trunc k A
-  is-trunc-retract-of {neg-two-𝕋} = is-contr-retract-of _
-  is-trunc-retract-of {succ-𝕋 k} R H x y =
-    is-trunc-retract-of (retract-eq R x y) (H (pr1 R x) (pr1 R y))
+  is-trunc-retract-of neg-two-𝕋 = is-contr-retract-of _
+  is-trunc-retract-of (succ-𝕋 k) R H x y =
+    is-trunc-retract-of k (retract-eq R x y) (H (pr1 R x) (pr1 R y))
 ```
 
 ### `k`-truncated types are closed under equivalences
@@ -137,7 +138,7 @@ abstract
     {l1 l2 : Level} (k : 𝕋) {A : UU l1} (B : UU l2) (f : A → B) → is-equiv f →
     is-trunc k B → is-trunc k A
   is-trunc-is-equiv k B f is-equiv-f =
-    is-trunc-retract-of (pair f (pr2 is-equiv-f))
+    is-trunc-retract-of k (pair f (pr2 is-equiv-f))
 
 abstract
   is-trunc-equiv :
@@ -181,6 +182,21 @@ abstract
   is-trunc-emb k f = is-trunc-is-emb k (map-emb f) (is-emb-map-emb f)
 ```
 
+In fact, it suffices that the map's action on identifications has a retraction.
+
+```agda
+abstract
+  is-trunc-retraction-ap :
+    {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) →
+    ((x y : A) → retraction (ap f {x} {y})) →
+    is-trunc (succ-𝕋 k) B → is-trunc (succ-𝕋 k) A
+  is-trunc-retraction-ap k f Ef H x y =
+    is-trunc-retract-of k (ap f , Ef x y) (H (f x) (f y))
+```
+
+- See [path-cosplit maps](foundation.path-cosplit-maps.md) for the concept of a
+  map whose action on identifications has a retraction.
+
 ### Truncated types are closed under dependent pair types
 
 ```agda
@@ -244,7 +260,7 @@ abstract
     {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} →
     is-trunc k A → is-trunc k B → is-trunc k (A × B)
   is-trunc-product k is-trunc-A is-trunc-B =
-    is-trunc-Σ is-trunc-A (λ x → is-trunc-B)
+    is-trunc-Σ is-trunc-A (λ _ → is-trunc-B)
 
 product-Truncated-Type :
   {l1 l2 : Level} (k : 𝕋) →
@@ -255,37 +271,43 @@ pr2 (product-Truncated-Type k A B) =
   is-trunc-product k
     ( is-trunc-type-Truncated-Type A)
     ( is-trunc-type-Truncated-Type B)
+```
 
+We need only show that each factor is `k`-truncated given that the opposite
+factor has an element when `k ≥ -1`.
+
+```agda
 is-trunc-product' :
   {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} →
-  (B → is-trunc (succ-𝕋 k) A) → (A → is-trunc (succ-𝕋 k) B) →
+  (B → is-trunc (succ-𝕋 k) A) →
+  (A → is-trunc (succ-𝕋 k) B) →
   is-trunc (succ-𝕋 k) (A × B)
 is-trunc-product' k f g (pair a b) (pair a' b') =
   is-trunc-equiv k
-    ( Eq-product (pair a b) (pair a' b'))
+    ( Eq-product (a , b) (pair a' b'))
     ( equiv-pair-eq (pair a b) (pair a' b'))
     ( is-trunc-product k (f b a a') (g a b b'))
 
-is-trunc-left-factor-product :
+is-trunc-left-factor-product' :
   {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} →
   is-trunc k (A × B) → B → is-trunc k A
-is-trunc-left-factor-product neg-two-𝕋 {A} {B} H b =
+is-trunc-left-factor-product' neg-two-𝕋 {A} {B} H b =
   is-contr-left-factor-product A B H
-is-trunc-left-factor-product (succ-𝕋 k) H b a a' =
-  is-trunc-left-factor-product k {A = (a ＝ a')} {B = (b ＝ b)}
+is-trunc-left-factor-product' (succ-𝕋 k) H b a a' =
+  is-trunc-left-factor-product' k {A = (a ＝ a')} {B = (b ＝ b)}
     ( is-trunc-equiv' k
       ( pair a b ＝ pair a' b)
       ( equiv-pair-eq (pair a b) (pair a' b))
       ( H (pair a b) (pair a' b)))
     ( refl)
 
-is-trunc-right-factor-product :
+is-trunc-right-factor-product' :
   {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} →
   is-trunc k (A × B) → A → is-trunc k B
-is-trunc-right-factor-product neg-two-𝕋 {A} {B} H a =
+is-trunc-right-factor-product' neg-two-𝕋 {A} {B} H a =
   is-contr-right-factor-product A B H
-is-trunc-right-factor-product (succ-𝕋 k) {A} {B} H a b b' =
-  is-trunc-right-factor-product k {A = (a ＝ a)} {B = (b ＝ b')}
+is-trunc-right-factor-product' (succ-𝕋 k) {A} {B} H a b b' =
+  is-trunc-right-factor-product' k {A = (a ＝ a)} {B = (b ＝ b')}
     ( is-trunc-equiv' k
       ( pair a b ＝ pair a b')
       ( equiv-pair-eq (pair a b) (pair a b'))
@@ -353,7 +375,7 @@ abstract
     {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} →
     is-trunc k B → is-trunc k (A → B)
   is-trunc-function-type k {A} {B} is-trunc-B =
-    is-trunc-Π k {B = λ (x : A) → B} (λ x → is-trunc-B)
+    is-trunc-Π k {B = λ (x : A) → B} (λ _ → is-trunc-B)
 
 function-type-Truncated-Type :
   {l1 l2 : Level} {k : 𝕋} (A : UU l1) (B : Truncated-Type l2 k) →
@@ -421,7 +443,12 @@ module _
               ( is-trunc-function-type k H)
               ( λ h →
                 is-trunc-Π k (λ x → is-trunc-Id H (h (f x)) x))))
+```
+
+Alternatively, this follows from the fact that equivalences embed into function
+types, and function types between `k`-truncated types are `k`-truncated.
 
+```agda
 type-equiv-Truncated-Type :
   {l1 l2 : Level} {k : 𝕋} (A : Truncated-Type l1 k) (B : Truncated-Type l2 k) →
   UU (l1 ⊔ l2)

src/foundation-core/univalence.lagda.md

@@ -108,8 +108,8 @@ abstract
   is-torsorial-equiv-based-univalence :
     {l : Level} (A : UU l) →
     based-univalence-axiom A → is-torsorial (λ (B : UU l) → A ≃ B)
-  is-torsorial-equiv-based-univalence A UA =
-    fundamental-theorem-id' (λ B → equiv-eq) UA
+  is-torsorial-equiv-based-univalence A =
+    fundamental-theorem-id' (λ B → equiv-eq)
 ```
 
 ### Contractibility of the total space of equivalences implies univalence