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 -WnoWithoutKFlagPrimEraseEquality
+flags: --without-K --exact-split --no-import-sorts --auto-inline --confluence-check -WnoWithoutKFlagPrimEraseEquality

references.bib

@@ -338,7 +338,7 @@ @article{MP87
   doi          = {10.1016/0021-8693(87)90046-9}
 }
 
-@online{MR23,
+@online{MR23a,
   title       = {Delooping the Sign Homomorphism in Univalent Mathematics},
   author      = {Mangel, Éléonore and Rijke, Egbert},
   date        = {2023-01-24},
@@ -352,6 +352,19 @@ @online{MR23
   keywords    = {20B30 03B15,Mathematics - Group Theory,Mathematics - Logic}
 }
 
+@online{MR23b,
+  title       = {Commuting {{Cohesions}}},
+  author      = {Myers, David Jaz and Riley, Mitchell},
+  date        = {2023-01-31},
+  month       = {01},
+  year        = {2023},
+  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},
@@ -452,6 +465,25 @@ @online{Rij22draft
   pubstate = {draft}
 }
 
+@misc{RS17,
+  title         = {A type theory for synthetic $\infty$-categories},
+  author        = {Riehl, Emily and Shulman, Michael},
+  year          = {2017},
+  shortjournal  = {High. Struct.},
+  journal       = {Higher Structures},
+  volume        = {1},
+  year          = {2017},
+  number        = {1},
+  pages         = {147--224},
+  issn          = {2209-0606},
+  eprint        = {1705.07442},
+  eprinttype    = {arxiv},
+  eprintclass   = {math},
+  archiveprefix = {arXiv},
+  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

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

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

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

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

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

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

@@ -20,7 +20,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
@@ -75,8 +77,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 :
@@ -121,11 +122,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
@@ -136,7 +137,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 :
@@ -180,6 +181,18 @@ 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))
+```
+
 ### Truncated types are closed under dependent pair types
 
 ```agda
@@ -225,7 +238,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 : 𝕋) →
@@ -236,37 +249,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'))
@@ -334,7 +353,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) →
@@ -402,7 +421,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

@@ -105,8 +105,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

src/foundation/0-connected-types.lagda.md

@@ -39,8 +39,15 @@ open import foundation-core.truncation-levels
 
 ## Idea
 
-A type is said to be connected if its type of connected components, i.e., its
-set truncation, is contractible.
+A type is said to be
+{{#concept "0-connected" Disambiguation="type" Agda=is-0-connected}} if its type
+of [connected components](foundation.connected-components.md), i.e., its
+[set truncation](foundation.set-truncations.md), is
+[contractible](foundation-core.contractible-types.md).
+
+## Definitions
+
+### The predicate on types of being 0-connected
 
 ```agda
 is-0-connected-Prop : {l : Level} → UU l → Prop l
@@ -66,7 +73,13 @@ abstract
     {l : Level} {A : UU l} → is-0-connected A → (x y : A) → mere-eq x y
   mere-eq-is-0-connected {A = A} H x y =
     apply-effectiveness-unit-trunc-Set (eq-is-contr H)
+```
 
+## Properties
+
+### A type is 0-connected if there is an element of that type such that every element is merely equal to it
+
+```agda
 abstract
   is-0-connected-mere-eq :
     {l : Level} {A : UU l} (a : A) →
@@ -77,7 +90,11 @@ abstract
       ( apply-dependent-universal-property-trunc-Set'
         ( λ x → set-Prop (Id-Prop (trunc-Set A) (unit-trunc-Set a) x))
         ( λ x → apply-effectiveness-unit-trunc-Set' (e x)))
+```
+
+### A type is 0-connected if it is inhabited and all elements are merely equal
 
+```agda
 abstract
   is-0-connected-mere-eq-is-inhabited :
     {l : Level} {A : UU l} →
@@ -86,7 +103,11 @@ abstract
     apply-universal-property-trunc-Prop H
       ( is-0-connected-Prop _)
       ( λ a → is-0-connected-mere-eq a (K a))
+```
+
+### A type is is 0-connected iff there is a point inclusion which is surjective
 
+```agda
 is-0-connected-is-surjective-point :
   {l1 : Level} {A : UU l1} (a : A) →
   is-surjective (point a) → is-0-connected A
@@ -107,10 +128,15 @@ abstract
       ( mere-eq-is-0-connected H a x)
       ( trunc-Prop (fiber (point a) x))
       ( λ where refl → unit-trunc-Prop (star , refl))
+```
+
+### The evaluation map at a point of a 0-connected type into a `k+1`-truncated type is `k`-truncated
 
+```agda
 is-trunc-map-ev-point-is-connected :
   {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (a : A) →
-  is-0-connected A → is-trunc (succ-𝕋 k) B →
+  is-0-connected A →
+  is-trunc (succ-𝕋 k) B →
   is-trunc-map k (ev-point' a {B})
 is-trunc-map-ev-point-is-connected k {A} {B} a H K =
   is-trunc-map-comp k
@@ -121,11 +147,14 @@ is-trunc-map-ev-point-is-connected k {A} {B} a H K =
     ( is-trunc-map-precomp-Π-is-surjective k
       ( is-surjective-point-is-0-connected a H)
       ( λ _ → (B , K)))
+```
 
+### 0-connected types satisfy the dependent universal property of 0-connected types
+
+```agda
 equiv-dependent-universal-property-is-0-connected :
   {l1 : Level} {A : UU l1} (a : A) → is-0-connected A →
-  ( {l : Level} (P : A → Prop l) →
-    ((x : A) → type-Prop (P x)) ≃ type-Prop (P a))
+  {l : Level} (P : A → Prop l) → ((x : A) → type-Prop (P x)) ≃ type-Prop (P a)
 equiv-dependent-universal-property-is-0-connected a H P =
   ( equiv-universal-property-unit (type-Prop (P a))) ∘e
   ( equiv-dependent-universal-property-surjection-is-surjective
@@ -167,19 +196,24 @@ abstract
     is-0-connected A
   is-0-connected-is-surjective-fiber-inclusion a H =
     is-0-connected-mere-eq a (mere-eq-is-surjective-fiber-inclusion a H)
+```
 
+### 0-connected types are closed under equivalences
+
+```agda
 is-0-connected-equiv :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} →
-  (A ≃ B) → is-0-connected B → is-0-connected A
-is-0-connected-equiv e = is-contr-equiv _ (equiv-trunc-Set e)
+  A ≃ B → is-0-connected B → is-0-connected A
+is-0-connected-equiv {B = B} e =
+  is-contr-equiv (type-trunc-Set B) (equiv-trunc-Set e)
 
 is-0-connected-equiv' :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} →
-  (A ≃ B) → is-0-connected A → is-0-connected B
+  A ≃ B → is-0-connected A → is-0-connected B
 is-0-connected-equiv' e = is-0-connected-equiv (inv-equiv e)
 ```
 
-### `0-connected` types are closed under cartesian products
+### 0-connected types are closed under cartesian products
 
 ```agda
 module _
@@ -195,12 +229,11 @@ module _
       ( is-contr-product p1 p2)
 ```
 
-### A contractible type is `0`-connected
+### Contractible types are 0-connected
 
 ```agda
 is-0-connected-is-contr :
-  {l : Level} (X : UU l) →
-  is-contr X → is-0-connected X
+  {l : Level} (X : UU l) → is-contr X → is-0-connected X
 is-0-connected-is-contr X p =
   is-contr-equiv X (inv-equiv (equiv-unit-trunc-Set (X , is-set-is-contr p))) p
 ```

src/foundation/action-on-identifications-functions.lagda.md

@@ -100,7 +100,7 @@ ap-inv f refl = refl
 ```agda
 ap-const :
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (b : B) {x y : A}
-  (p : x ＝ y) → (ap (const A b) p) ＝ refl
+  (p : x ＝ y) → ap (const A b) p ＝ refl
 ap-const b refl = refl
 ```