From 4fe126fd51bb945753cef24928f05ff96a9e3d9d Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 6 Dec 2023 16:02:44 +0100 Subject: [PATCH] The `is-sequential-colimit` predicate (#969) --- .../universal-property-equivalences.lagda.md | 12 ++ ...rsal-property-sequential-colimits.lagda.md | 105 ++++++++++++++++-- .../sequential-colimits.lagda.md | 95 ++++++++++++++++ ...rsal-property-sequential-colimits.lagda.md | 6 +- 4 files changed, 204 insertions(+), 14 deletions(-) diff --git a/src/foundation/universal-property-equivalences.lagda.md b/src/foundation/universal-property-equivalences.lagda.md index 519a9a8bf4..fea8d6c9ce 100644 --- a/src/foundation/universal-property-equivalences.lagda.md +++ b/src/foundation/universal-property-equivalences.lagda.md @@ -105,3 +105,15 @@ module _ ( f) ( λ C → H (pr1 C)) ``` + +#### If dependent precomposition by `f` is an equivalence, then `f` is an equivalence + +```agda +abstract + is-equiv-is-equiv-precomp-Π : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → + dependent-universal-property-equiv f → + is-equiv f + is-equiv-is-equiv-precomp-Π f H = + is-equiv-is-equiv-precomp f (is-equiv-precomp-is-equiv-precomp-Π f H) +``` diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md index 7da1b9e746..3797fd704a 100644 --- a/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md @@ -7,19 +7,30 @@ module synthetic-homotopy-theory.dependent-universal-property-sequential-colimit
Imports ```agda +open import foundation.action-on-identifications-functions +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.equivalences open import foundation.fibers-of-maps +open import foundation.function-types open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.precomposition-dependent-functions +open import foundation.precomposition-functions +open import foundation.subtype-identity-principle +open import foundation.universal-property-equivalences open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-sequential-diagrams +open import synthetic-homotopy-theory.coforks open import synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams open import synthetic-homotopy-theory.dependent-coforks open import synthetic-homotopy-theory.dependent-universal-property-coequalizers open import synthetic-homotopy-theory.sequential-diagrams +open import synthetic-homotopy-theory.universal-property-coequalizers open import synthetic-homotopy-theory.universal-property-sequential-colimits ``` @@ -62,7 +73,7 @@ module _ module _ { l1 l2 l3 : Level} (A : sequential-diagram l1) {X : UU l2} ( c : cocone-sequential-diagram A X) {P : X → UU l3} - ( dup-sequential-colimit : + ( dup-c : dependent-universal-property-sequential-colimit A c) where @@ -70,7 +81,7 @@ module _ dependent-cocone-sequential-diagram A c P → ( x : X) → P x map-dependent-universal-property-sequential-colimit = - map-inv-is-equiv (dup-sequential-colimit P) + map-inv-is-equiv (dup-c P) ``` ## Properties @@ -81,7 +92,7 @@ module _ module _ { l1 l2 l3 : Level} (A : sequential-diagram l1) {X : UU l2} ( c : cocone-sequential-diagram A X) {P : X → UU l3} - ( dup-sequential-colimit : + ( dup-c : dependent-universal-property-sequential-colimit A c) ( d : dependent-cocone-sequential-diagram A c P) where @@ -90,17 +101,17 @@ module _ htpy-dependent-cocone-sequential-diagram A P ( dependent-cocone-map-sequential-diagram A c P ( map-dependent-universal-property-sequential-colimit A c - ( dup-sequential-colimit) + ( dup-c) ( d))) ( d) htpy-dependent-cocone-dependent-universal-property-sequential-colimit = htpy-eq-dependent-cocone-sequential-diagram A P ( dependent-cocone-map-sequential-diagram A c P ( map-dependent-universal-property-sequential-colimit A c - ( dup-sequential-colimit) + ( dup-c) ( d))) ( d) - ( is-section-map-inv-is-equiv (dup-sequential-colimit P) d) + ( is-section-map-inv-is-equiv (dup-c P) d) abstract uniqueness-dependent-universal-property-sequential-colimit : @@ -118,7 +129,7 @@ module _ extensionality-dependent-cocone-sequential-diagram A P ( dependent-cocone-map-sequential-diagram A c P h) ( d))) - ( is-contr-map-is-equiv (dup-sequential-colimit P) d) + ( is-contr-map-is-equiv (dup-c P) d) ``` ### Correspondence between dependent universal properties of sequential colimits and coequalizers @@ -162,7 +173,7 @@ module _ ( top-map-cofork-cocone-sequential-diagram A) ( cofork-cocone-sequential-diagram A c)) dependent-universal-property-coequalizer-dependent-universal-property-sequential-colimit - ( dup-sequential-colimit) + ( dup-c) ( P) = is-equiv-top-map-triangle ( dependent-cocone-map-sequential-diagram A c P) @@ -173,7 +184,7 @@ module _ ( cofork-cocone-sequential-diagram A c)) ( triangle-dependent-cocone-sequential-diagram-dependent-cofork A c P) ( is-equiv-dependent-cocone-sequential-diagram-dependent-cofork A c P) - ( dup-sequential-colimit P) + ( dup-c P) ``` ### The non-dependent and dependent universal properties of sequential colimits are logically equivalent @@ -188,7 +199,7 @@ module _ dependent-universal-property-sequential-colimit A c → universal-property-sequential-colimit A c universal-property-dependent-universal-property-sequential-colimit - ( dup-sequential-colimit) + ( dup-c) ( Y) = is-equiv-left-map-triangle ( cocone-map-sequential-diagram A c) @@ -196,7 +207,7 @@ module _ ( dependent-cocone-map-sequential-diagram A c (λ _ → Y)) ( triangle-compute-dependent-cocone-sequential-diagram-constant-family A c ( Y)) - ( dup-sequential-colimit (λ _ → Y)) + ( dup-c (λ _ → Y)) ( is-equiv-map-equiv ( compute-dependent-cocone-sequential-diagram-constant-family A c Y)) @@ -217,3 +228,75 @@ module _ ( c) ( up-sequential-diagram))) ``` + +### The 3-for-2 property of the dependent universal property of sequential colimits + +Given two cocones under a sequential diagram, one of which has the dependent +universal property of sequential colimits, and a map between their vertices, we +prove that the other has the dependent universal property if and only if the map +is an [equivalence](foundation.equivalences.md). + +```agda +module _ + { l1 l2 l3 : Level} (A : sequential-diagram l1) {X : UU l2} {Y : UU l3} + ( c : cocone-sequential-diagram A X) + ( c' : cocone-sequential-diagram A Y) + ( h : X → Y) + ( H : + htpy-cocone-sequential-diagram A (cocone-map-sequential-diagram A c h) c') + where + + abstract + is-equiv-dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit : + dependent-universal-property-sequential-colimit A c → + dependent-universal-property-sequential-colimit A c' → + is-equiv h + is-equiv-dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit + ( dup-c) + ( dup-c') = + is-equiv-universal-property-sequential-colimit-universal-property-sequential-colimit + ( A) + ( c) + ( c') + ( h) + ( H) + ( universal-property-dependent-universal-property-sequential-colimit + ( A) c dup-c) + ( universal-property-dependent-universal-property-sequential-colimit + ( A) c' dup-c') + + dependent-universal-property-sequential-colimit-is-equiv-dependent-universal-property-sequential-colimit : + dependent-universal-property-sequential-colimit A c → + is-equiv h → + dependent-universal-property-sequential-colimit A c' + dependent-universal-property-sequential-colimit-is-equiv-dependent-universal-property-sequential-colimit + ( dup-c) (is-equiv-h) = + dependent-universal-property-universal-property-sequential-colimit A c' + ( universal-property-sequential-colimit-is-equiv-universal-property-sequential-colimit + ( A) + ( c) + ( c') + ( h) + ( H) + ( universal-property-dependent-universal-property-sequential-colimit + ( A) c dup-c) + ( is-equiv-h)) + + dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit-is-equiv : + is-equiv h → + dependent-universal-property-sequential-colimit A c' → + dependent-universal-property-sequential-colimit A c + dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit-is-equiv + ( is-equiv-h) + ( dup-c') = + dependent-universal-property-universal-property-sequential-colimit A c + ( universal-property-sequential-colimit-universal-property-sequential-colimit-is-equiv + ( A) + ( c) + ( c') + ( h) + ( H) + ( is-equiv-h) + ( universal-property-dependent-universal-property-sequential-colimit + ( A) c' dup-c')) +``` diff --git a/src/synthetic-homotopy-theory/sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/sequential-colimits.lagda.md index 7906598769..04bd41ec62 100644 --- a/src/synthetic-homotopy-theory/sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/sequential-colimits.lagda.md @@ -16,6 +16,7 @@ open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies +open import foundation.propositions open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-sequential-diagrams @@ -160,6 +161,33 @@ module _ map-inv-equiv equiv-dup-standard-sequential-colimit ``` +### The small predicate of being a sequential colimit cocone + +The [proposition](foundation-core.propositions.md) `is-sequential-colimit` is +the assertion that the cogap map is an +[equivalence](foundation-core.equivalences.md). Note that this proposition is +[small](foundation-core.small-types.md), whereas +[the universal property](synthetic-homotopy-theory.universal-property-sequential-colimits.md) +is a large proposition. + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2} + (c : cocone-sequential-diagram A X) + where + + is-sequential-colimit : UU (l1 ⊔ l2) + is-sequential-colimit = is-equiv (cogap-standard-sequential-colimit c) + + is-prop-is-sequential-colimit : is-prop is-sequential-colimit + is-prop-is-sequential-colimit = + is-property-is-equiv (cogap-standard-sequential-colimit c) + + is-sequential-colimit-Prop : Prop (l1 ⊔ l2) + pr1 is-sequential-colimit-Prop = is-sequential-colimit + pr2 is-sequential-colimit-Prop = is-prop-is-sequential-colimit +``` + ### Homotopies between maps from the standard sequential colimit Maps from the standard sequential colimit induce cocones under the sequential @@ -211,3 +239,70 @@ module _ htpy-htpy-out-of-standard-sequential-colimit = map-equiv (equiv-htpy-htpy-out-of-standard-sequential-colimit A f g) H ``` + +### A type satisfies `is-sequential-colimit` if and only if it has the (dependent) universal property of sequential colimits + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2} + (c : cocone-sequential-diagram A X) + where + + universal-property-is-sequential-colimit : + is-sequential-colimit c → universal-property-sequential-colimit A c + universal-property-is-sequential-colimit = + universal-property-sequential-colimit-is-equiv-universal-property-sequential-colimit + ( A) + ( cocone-standard-sequential-colimit A) + ( c) + ( cogap-standard-sequential-colimit c) + ( htpy-cocone-universal-property-sequential-colimit A + ( cocone-standard-sequential-colimit A) + ( up-standard-sequential-colimit) + ( c)) + ( up-standard-sequential-colimit) + + dependent-universal-property-is-sequential-colimit : + is-sequential-colimit c → + dependent-universal-property-sequential-colimit A c + dependent-universal-property-is-sequential-colimit = + dependent-universal-property-sequential-colimit-is-equiv-dependent-universal-property-sequential-colimit + ( A) + ( cocone-standard-sequential-colimit A) + ( c) + ( cogap-standard-sequential-colimit c) + ( htpy-cocone-universal-property-sequential-colimit A + ( cocone-standard-sequential-colimit A) + ( up-standard-sequential-colimit) + ( c)) + ( dup-standard-sequential-colimit) + + is-sequential-colimit-universal-property : + universal-property-sequential-colimit A c → is-sequential-colimit c + is-sequential-colimit-universal-property = + is-equiv-universal-property-sequential-colimit-universal-property-sequential-colimit + ( A) + ( cocone-standard-sequential-colimit A) + ( c) + ( cogap-standard-sequential-colimit c) + ( htpy-cocone-universal-property-sequential-colimit A + ( cocone-standard-sequential-colimit A) + ( up-standard-sequential-colimit) + ( c)) + ( up-standard-sequential-colimit) + + is-sequential-colimit-dependent-universal-property : + dependent-universal-property-sequential-colimit A c → + is-sequential-colimit c + is-sequential-colimit-dependent-universal-property = + is-equiv-dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit + ( A) + ( cocone-standard-sequential-colimit A) + ( c) + ( cogap-standard-sequential-colimit c) + ( htpy-cocone-universal-property-sequential-colimit A + ( cocone-standard-sequential-colimit A) + ( up-standard-sequential-colimit) + ( c)) + ( dup-standard-sequential-colimit) +``` diff --git a/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md index 911d82d7c3..382dbbc023 100644 --- a/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md @@ -189,7 +189,7 @@ module _ ( up-sequential-colimit Y) ``` -### 3-for-2 property of sequential colimits +### The 3-for-2 property of the universal property of sequential colimits Given two cocones under a sequential diagram, one of which has the universal property of sequential colimits, and a map between their vertices, we prove that @@ -248,11 +248,11 @@ module _ ( up-sequential-colimit Z) ( up-sequential-colimit' Z)) - universal-property-sequential-colimit-is-equiv-universal-property-sequential-colomit : + universal-property-sequential-colimit-is-equiv-universal-property-sequential-colimit : universal-property-sequential-colimit A c → is-equiv h → universal-property-sequential-colimit A c' - universal-property-sequential-colimit-is-equiv-universal-property-sequential-colomit + universal-property-sequential-colimit-is-equiv-universal-property-sequential-colimit ( up-sequential-colimit) ( is-equiv-h) ( Z) =