From 4bd946d3ab54ad4f777abcada99c75f9e5256143 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 00:54:10 +0100 Subject: [PATCH 01/13] refactor universal property suspensions --- .../integers.lagda.md | 24 +-- src/foundation/unit-type.lagda.md | 2 +- src/synthetic-homotopy-theory/circle.lagda.md | 2 +- ...nt-universal-property-suspensions.lagda.md | 25 +-- .../suspension-structures.lagda.md | 30 ++-- .../suspensions-of-types.lagda.md | 167 +++++++++++------- .../universal-property-suspensions.lagda.md | 57 +++--- 7 files changed, 170 insertions(+), 137 deletions(-) diff --git a/src/elementary-number-theory/integers.lagda.md b/src/elementary-number-theory/integers.lagda.md index 1ea438eb48..ed178f802d 100644 --- a/src/elementary-number-theory/integers.lagda.md +++ b/src/elementary-number-theory/integers.lagda.md @@ -202,7 +202,7 @@ pr2 equiv-pred-ℤ = is-equiv-pred-ℤ ```agda is-injective-succ-ℤ : is-injective succ-ℤ is-injective-succ-ℤ {x} {y} p = - inv (is-retraction-pred-ℤ x) ∙ (ap pred-ℤ p ∙ is-retraction-pred-ℤ y) + inv (is-retraction-pred-ℤ x) ∙ ap pred-ℤ p ∙ is-retraction-pred-ℤ y has-no-fixed-points-succ-ℤ : (x : ℤ) → succ-ℤ x ≠ x has-no-fixed-points-succ-ℤ (inl zero-ℕ) () @@ -309,7 +309,8 @@ is-set-is-positive-ℤ (inr (inl x)) = is-set-empty is-set-is-positive-ℤ (inr (inr x)) = is-set-unit is-positive-ℤ-Set : ℤ → Set lzero -is-positive-ℤ-Set z = pair (is-positive-ℤ z) (is-set-is-positive-ℤ z) +pr1 (is-positive-ℤ-Set z) = is-positive-ℤ z +pr2 (is-positive-ℤ-Set z) = is-set-is-positive-ℤ z positive-ℤ : UU lzero positive-ℤ = Σ ℤ is-positive-ℤ @@ -409,8 +410,8 @@ pr2 equiv-nonnegative-int-ℕ = is-equiv-nonnegative-int-ℕ is-injective-nonnegative-int-ℕ : is-injective nonnegative-int-ℕ is-injective-nonnegative-int-ℕ {x} {y} p = ( inv (is-retraction-nat-nonnegative-ℤ x)) ∙ - ( ( ap nat-nonnegative-ℤ p) ∙ - ( is-retraction-nat-nonnegative-ℤ y)) + ( ap nat-nonnegative-ℤ p) ∙ + ( is-retraction-nat-nonnegative-ℤ y) decide-is-nonnegative-ℤ : {x : ℤ} → (is-nonnegative-ℤ x) + (is-nonnegative-ℤ (neg-ℤ x)) @@ -431,17 +432,16 @@ succ-int-ℕ (succ-ℕ x) = refl ```agda is-injective-neg-ℤ : is-injective neg-ℤ -is-injective-neg-ℤ {x} {y} p = inv (neg-neg-ℤ x) ∙ (ap neg-ℤ p ∙ neg-neg-ℤ y) +is-injective-neg-ℤ {x} {y} p = inv (neg-neg-ℤ x) ∙ ap neg-ℤ p ∙ neg-neg-ℤ y -is-zero-is-zero-neg-ℤ : - (x : ℤ) → is-zero-ℤ (neg-ℤ x) → is-zero-ℤ x +is-zero-is-zero-neg-ℤ : (x : ℤ) → is-zero-ℤ (neg-ℤ x) → is-zero-ℤ x is-zero-is-zero-neg-ℤ (inr (inl star)) H = refl ``` ## See also -1. We show in - [`structured-types.initial-pointed-type-equipped-with-automorphism`](structured-types.initial-pointed-type-equipped-with-automorphism.md) - that ℤ is the initial pointed type equipped with an automorphism. -2. The group of integers is constructed in - [`elementary-number-theory.group-of-integers`](elementary-number-theory.group-of-integers.md). +- We show in + [`structured-types.initial-pointed-type-equipped-with-automorphism`](structured-types.initial-pointed-type-equipped-with-automorphism.md) + that ℤ is the initial pointed type equipped with an automorphism. +- The group of integers is constructed in + [`elementary-number-theory.group-of-integers`](elementary-number-theory.group-of-integers.md). diff --git a/src/foundation/unit-type.lagda.md b/src/foundation/unit-type.lagda.md index f8cfedf850..54127d2476 100644 --- a/src/foundation/unit-type.lagda.md +++ b/src/foundation/unit-type.lagda.md @@ -49,7 +49,7 @@ ind-unit p star = p ```agda terminal-map : {l : Level} {A : UU l} → A → unit -terminal-map = const _ unit star +terminal-map {A = A} = const A unit star ``` ### Points as maps out of the unit type diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md index 469a67856c..390db0d3c5 100644 --- a/src/synthetic-homotopy-theory/circle.lagda.md +++ b/src/synthetic-homotopy-theory/circle.lagda.md @@ -433,7 +433,7 @@ pr2 (pr2 dependent-suspension-structure-sphere-1-circle-sphere-1) = sphere-1-circle-sphere-1 : section sphere-1-circle pr1 sphere-1-circle-sphere-1 = circle-sphere-1 pr2 sphere-1-circle-sphere-1 = - map-inv-dependent-up-suspension + map-inv-dup-suspension ( λ x → (sphere-1-circle (circle-sphere-1 x)) = x) ( dependent-suspension-structure-sphere-1-circle-sphere-1) ``` diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md index 99f5716b12..afb61ece1c 100644 --- a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md @@ -43,16 +43,21 @@ pr1 (dependent-ev-suspension s B f) = pr1 (pr2 (dependent-ev-suspension s B f)) = f (south-suspension-structure s) pr2 (pr2 (dependent-ev-suspension s B f)) = - (apd f) ∘ (meridian-suspension-structure s) + apd f ∘ meridian-suspension-structure s module _ - (l : Level) {l1 l2 : Level} {X : UU l1} {Y : UU l2} + {l1 l2 : Level} {X : UU l1} {Y : UU l2} (s : suspension-structure X Y) where - dependent-universal-property-suspension : UU (l1 ⊔ l2 ⊔ lsuc l) - dependent-universal-property-suspension = + dependent-universal-property-suspension-Level : + (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l) + dependent-universal-property-suspension-Level l = (B : Y → UU l) → is-equiv (dependent-ev-suspension s B) + + dependent-universal-property-suspension : UUω + dependent-universal-property-suspension = + {l : Level} → dependent-universal-property-suspension-Level l ``` #### Coherence between `dependent-ev-suspension` and `dependent-cocone-map` @@ -66,12 +71,12 @@ module _ (s : suspension-structure X Y) → (B : Y → UU l3) → ( ( map-equiv - ( equiv-dependent-suspension-structure-suspension-cocone s B)) ∘ - ( dependent-cocone-map - ( const X unit star) - ( const X unit star) - ( cocone-suspension-structure X Y s) - ( B))) ~ + ( equiv-dependent-suspension-structure-suspension-cocone s B)) ∘ + ( dependent-cocone-map + ( const X unit star) + ( const X unit star) + ( cocone-suspension-structure X Y s) + ( B))) ~ ( dependent-ev-suspension s B) triangle-dependent-ev-suspension s B = refl-htpy ``` diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md index 4057d6ebee..98a7fb11d8 100644 --- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md @@ -51,9 +51,9 @@ h : (x : X) → (f ∘ (const X unit star)) x = (g ∘ (const X unit star)) x ``` Using the -[universal property of `unit`](foundation.universal-property-unit-type.md), we -can characterize suspension cocones as equivalent to a selection of "north" and -"south" poles +[universal property of the unit type](foundation.universal-property-unit-type.md), +we can characterize suspension cocones as equivalent to a selection of "north" +and "south" poles ```text north , south : Y @@ -74,7 +74,7 @@ We call this type of structure `suspension-structure`. ```agda suspension-cocone : {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (l1 ⊔ l2) -suspension-cocone X Y = cocone (const X unit star) (const X unit star) Y +suspension-cocone X Y = cocone (terminal-map {A = X}) (terminal-map {A = X}) Y ``` ### Suspension structures on a type @@ -154,13 +154,9 @@ is-equiv-map-inv-equiv-suspension-structure-suspension-cocone X Z = htpy-comparison-suspension-cocone-suspension-structure : {l1 l2 : Level} (X : UU l1) (Z : UU l2) → - ( map-inv-equiv-suspension-structure-suspension-cocone X Z) - ~ - ( cocone-suspension-structure X Z) -htpy-comparison-suspension-cocone-suspension-structure - ( X) - ( Z) - ( s) = + ( map-inv-equiv-suspension-structure-suspension-cocone X Z) ~ + ( cocone-suspension-structure X Z) +htpy-comparison-suspension-cocone-suspension-structure X Z s = is-injective-map-equiv ( equiv-suspension-structure-suspension-cocone X Z) ( is-section-map-inv-equiv @@ -178,9 +174,9 @@ module _ htpy-suspension-structure : (c c' : suspension-structure X Z) → UU (l1 ⊔ l2) htpy-suspension-structure c c' = - Σ ( (north-suspension-structure c) = (north-suspension-structure c')) + Σ ( north-suspension-structure c = north-suspension-structure c') ( λ p → - Σ ( ( south-suspension-structure c) = ( south-suspension-structure c')) + Σ ( south-suspension-structure c = south-suspension-structure c') ( λ q → ( x : X) → ( meridian-suspension-structure c x ∙ q) = @@ -267,9 +263,7 @@ module _ ind-htpy-suspension-structure : { l : Level} ( P : - ( c' : suspension-structure X Z) → - ( htpy-suspension-structure c c') → - UU l) → + (c' : suspension-structure X Z) → htpy-suspension-structure c c' → UU l) → ( P c refl-htpy-suspension-structure) → ( c' : suspension-structure X Z) ( H : htpy-suspension-structure c c') → @@ -300,11 +294,11 @@ module _ ap-pr1-eq-htpy-suspension-structure = ind-htpy-suspension-structure ( λ c' H → (ap (pr1) (eq-htpy-suspension-structure H)) = (pr1 H)) - ( (ap + ( ap ( ap pr1) ( is-retraction-map-inv-equiv ( extensionality-suspension-structure c c) - ( refl)))) + ( refl))) ap-pr1∘pr2-eq-htpy-suspension-structure : (c' : suspension-structure X Z) (H : htpy-suspension-structure c c') → diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index f20e1393d5..39b2091760 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -32,6 +32,7 @@ open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universe-levels +open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.dependent-suspension-structures open import synthetic-homotopy-theory.dependent-universal-property-suspensions @@ -57,9 +58,9 @@ Suspensions play an important role in synthetic homotopy theory. For example, they star in the freudenthal suspension theorem and give us a definition of [the spheres](synthetic-homotopy-theory.spheres.md). -## Definition +## Definitions -### The suspension of an ordinary type `X` +### The suspension of a type ```agda suspension : @@ -78,7 +79,7 @@ south-suspension {X = X} = meridian-suspension : {l : Level} {X : UU l} → X → - Id (north-suspension {X = X}) (south-suspension {X = X}) + north-suspension {X = X} = south-suspension {X = X} meridian-suspension {X = X} = glue-pushout terminal-map terminal-map @@ -87,11 +88,50 @@ suspension-structure-suspension : pr1 (suspension-structure-suspension X) = north-suspension pr1 (pr2 (suspension-structure-suspension X)) = south-suspension pr2 (pr2 (suspension-structure-suspension X)) = meridian-suspension + +cocone-suspension : + {l : Level} (X : UU l) → + cocone terminal-map terminal-map (pushout terminal-map terminal-map) +cocone-suspension X = + cocone-pushout (terminal-map {A = X}) (terminal-map {A = X}) + +cogap-suspension : + {l1 l2 : Level} {X : UU l1} {Y : UU l2} → + cocone terminal-map terminal-map Y → pushout terminal-map terminal-map → Y +cogap-suspension {X = X} = cogap (terminal-map {A = X}) (terminal-map {A = X}) +``` + +### The cogap map of a suspension structure + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {Y : UU l2} (s : suspension-structure X Y) + where + + cogap-suspension-structure-suspension : suspension X → Y + cogap-suspension-structure-suspension = + cogap-suspension (cocone-suspension-structure X Y s) +``` + +### The property of being a suspension + +The [proposition](foundation-core.propositions.md) `is-suspension` 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](foundation-core.universal-property-pullbacks.md) is a +large proposition. + +```agda +is-suspension : + {l1 l2 : Level} {X : UU l1} {Y : UU l2} → + suspension-structure X Y → UU (l1 ⊔ l2) +is-suspension s = is-equiv (cogap-suspension-structure-suspension s) ``` ## Properties -### The suspension of X has the universal property of suspensions +### The suspension of `X` has the universal property of suspensions ```agda module _ @@ -99,10 +139,7 @@ module _ where up-suspension : - {l : Level} → - universal-property-suspension l X - ( suspension X) - ( suspension-structure-suspension X) + universal-property-suspension (suspension-structure-suspension X) up-suspension Z = is-equiv-htpy ( ev-suspension (suspension-structure-suspension X) Z) @@ -180,15 +217,13 @@ module _ ( up-suspension-meridian-suspension Z c)) ``` -### The suspension of X has the dependent universal property of suspensions +### The suspension of `X` has the dependent universal property of suspensions ```agda -dependent-up-suspension : - (l : Level) {l1 : Level} {X : UU l1} → - dependent-universal-property-suspension - ( l) - ( suspension-structure-suspension X) -dependent-up-suspension l {X = X} B = +dup-suspension : + {l1 : Level} {X : UU l1} → + dependent-universal-property-suspension (suspension-structure-suspension X) +dup-suspension {X = X} B = is-equiv-htpy ( map-equiv ( equiv-dependent-suspension-structure-suspension-cocone @@ -224,83 +259,83 @@ dependent-up-suspension l {X = X} B = ( suspension-structure-suspension X) ( B)))) -equiv-dependent-up-suspension : - {l1 l2 : Level} {X : UU l1} (B : suspension X → UU l2) → - ((x : suspension X) → B x) ≃ - ( dependent-suspension-structure B (suspension-structure-suspension X)) -pr1 (equiv-dependent-up-suspension {l2 = l2} {X = X} B) = - (dependent-ev-suspension (suspension-structure-suspension X) B) -pr2 (equiv-dependent-up-suspension {l2 = l2} B) = - dependent-up-suspension l2 B +equiv-dup-suspension : + {l1 l2 : Level} {X : UU l1} (B : suspension X → UU l2) → + (( x : suspension X) → B x) ≃ + ( dependent-suspension-structure B (suspension-structure-suspension X)) +pr1 (equiv-dup-suspension {l2 = l2} {X = X} B) = + dependent-ev-suspension (suspension-structure-suspension X) B +pr2 (equiv-dup-suspension {l2 = l2} B) = + dup-suspension B module _ {l1 l2 : Level} {X : UU l1} (B : suspension X → UU l2) where - map-inv-dependent-up-suspension : + map-inv-dup-suspension : dependent-suspension-structure B (suspension-structure-suspension X) → (x : suspension X) → B x - map-inv-dependent-up-suspension = - map-inv-is-equiv (dependent-up-suspension l2 B) + map-inv-dup-suspension = + map-inv-is-equiv (dup-suspension B) - is-section-map-inv-dependent-up-suspension : + is-section-map-inv-dup-suspension : ( ( dependent-ev-suspension (suspension-structure-suspension X) B) ∘ - ( map-inv-dependent-up-suspension)) ~ id - is-section-map-inv-dependent-up-suspension = - is-section-map-inv-is-equiv (dependent-up-suspension l2 B) + ( map-inv-dup-suspension)) ~ id + is-section-map-inv-dup-suspension = + is-section-map-inv-is-equiv (dup-suspension B) - is-retraction-map-inv-dependent-up-suspension : - ( ( map-inv-dependent-up-suspension) ∘ + is-retraction-map-inv-dup-suspension : + ( ( map-inv-dup-suspension) ∘ ( dependent-ev-suspension (suspension-structure-suspension X) B)) ~ id - is-retraction-map-inv-dependent-up-suspension = - is-retraction-map-inv-is-equiv (dependent-up-suspension l2 B) + is-retraction-map-inv-dup-suspension = + is-retraction-map-inv-is-equiv (dup-suspension B) - dependent-up-suspension-north-suspension : + dup-suspension-north-suspension : (d : dependent-suspension-structure ( B) ( suspension-structure-suspension X)) → - ( map-inv-dependent-up-suspension d north-suspension) = + ( map-inv-dup-suspension d north-suspension) = ( north-dependent-suspension-structure d) - dependent-up-suspension-north-suspension d = + dup-suspension-north-suspension d = north-htpy-dependent-suspension-structure ( B) ( htpy-eq-dependent-suspension-structure ( B) - ( is-section-map-inv-dependent-up-suspension d)) + ( is-section-map-inv-dup-suspension d)) - dependent-up-suspension-south-suspension : + dup-suspension-south-suspension : (d : dependent-suspension-structure ( B) ( suspension-structure-suspension X)) → - ( map-inv-dependent-up-suspension d south-suspension) = + ( map-inv-dup-suspension d south-suspension) = ( south-dependent-suspension-structure d) - dependent-up-suspension-south-suspension d = + dup-suspension-south-suspension d = south-htpy-dependent-suspension-structure ( B) ( htpy-eq-dependent-suspension-structure ( B) - ( is-section-map-inv-dependent-up-suspension d)) + ( is-section-map-inv-dup-suspension d)) - dependent-up-suspension-meridian-suspension : + dup-suspension-meridian-suspension : (d : dependent-suspension-structure ( B) ( suspension-structure-suspension X)) (x : X) → - coherence-square-identifications - ( ap - ( tr B (meridian-suspension x)) - ( dependent-up-suspension-north-suspension d)) - ( apd - ( map-inv-dependent-up-suspension d) - ( meridian-suspension x)) - ( meridian-dependent-suspension-structure d x) - ( dependent-up-suspension-south-suspension d) - dependent-up-suspension-meridian-suspension d = + coherence-square-identifications + ( ap + ( tr B (meridian-suspension x)) + ( dup-suspension-north-suspension d)) + ( apd + ( map-inv-dup-suspension d) + ( meridian-suspension x)) + ( meridian-dependent-suspension-structure d x) + ( dup-suspension-south-suspension d) + dup-suspension-meridian-suspension d = meridian-htpy-dependent-suspension-structure ( B) ( htpy-eq-dependent-suspension-structure ( B) - ( is-section-map-inv-dependent-up-suspension d)) + ( is-section-map-inv-dup-suspension d)) ``` ### Characterization of homotopies between functions with domain a suspension @@ -403,7 +438,7 @@ module _ ( q)))))) ∙h ( tot-htpy ( λ p → - compute-inv-equiv-tot + ( compute-inv-equiv-tot ( λ q → equiv-Π-equiv-family ( λ x → @@ -415,9 +450,7 @@ module _ ( suspension-structure-suspension X) ( x)) ( p) - ( q)))))) ∙h - ( tot-htpy - ( λ p → + ( q))))) ∙h ( tot-htpy ( λ q → compute-inv-equiv-Π-equiv-family @@ -436,7 +469,7 @@ module _ (f ~ g) ≃ htpy-function-out-of-suspension equiv-htpy-function-out-of-suspension-htpy = ( equiv-htpy-function-out-of-suspension-dependent-suspension-structure) ∘e - ( equiv-dependent-up-suspension (eq-value f g)) + ( equiv-dup-suspension (eq-value f g)) htpy-function-out-of-suspension-htpy : (f ~ g) → htpy-function-out-of-suspension @@ -446,7 +479,7 @@ module _ equiv-htpy-htpy-function-out-of-suspension : htpy-function-out-of-suspension ≃ (f ~ g) equiv-htpy-htpy-function-out-of-suspension = - ( inv-equiv (equiv-dependent-up-suspension (eq-value f g))) ∘e + ( inv-equiv (equiv-dup-suspension (eq-value f g))) ∘e ( equiv-dependent-suspension-structure-htpy-function-out-of-suspension) htpy-htpy-function-out-of-suspension : @@ -461,17 +494,17 @@ module _ compute-inv-equiv-htpy-function-out-of-suspension-htpy c = ( htpy-eq-equiv ( distributive-inv-comp-equiv - ( equiv-dependent-up-suspension (eq-value f g)) + ( equiv-dup-suspension (eq-value f g)) ( equiv-htpy-function-out-of-suspension-dependent-suspension-structure)) ( c)) ∙ ( ap - ( map-inv-equiv (equiv-dependent-up-suspension (eq-value-function f g))) + ( map-inv-equiv (equiv-dup-suspension (eq-value-function f g))) ( compute-inv-equiv-htpy-function-out-of-suspension-dependent-suspension-structure ( c))) is-section-htpy-htpy-function-out-of-suspension : ( ( htpy-function-out-of-suspension-htpy) ∘ - ( htpy-htpy-function-out-of-suspension)) ~ + ( htpy-htpy-function-out-of-suspension)) ~ ( id) is-section-htpy-htpy-function-out-of-suspension c = ( ap @@ -481,8 +514,8 @@ module _ equiv-htpy-function-out-of-suspension-htpy-north-suspension : (c : htpy-function-out-of-suspension) → - ( htpy-htpy-function-out-of-suspension c north-suspension) = - ( north-htpy-function-out-of-suspension c) + ( htpy-htpy-function-out-of-suspension c north-suspension) = + ( north-htpy-function-out-of-suspension c) equiv-htpy-function-out-of-suspension-htpy-north-suspension c = north-htpy-in-htpy-suspension-structure ( htpy-eq-htpy-suspension-structure @@ -490,8 +523,8 @@ module _ equiv-htpy-function-out-of-suspension-htpy-south-suspension : (c : htpy-function-out-of-suspension) → - ( htpy-htpy-function-out-of-suspension c south-suspension) = - ( south-htpy-function-out-of-suspension c) + ( htpy-htpy-function-out-of-suspension c south-suspension) = + ( south-htpy-function-out-of-suspension c) equiv-htpy-function-out-of-suspension-htpy-south-suspension c = south-htpy-in-htpy-suspension-structure ( htpy-eq-htpy-suspension-structure diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md index 5237a4aa66..12e4296820 100644 --- a/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md @@ -30,46 +30,47 @@ Since suspensions are just [pushouts](synthetic-homotopy-theory.pushouts.md), they retain the expected [universal property](synthetic-homotopy-theory.universal-property-pushouts.md), which states that the map `cocone-map` is a equivalence. We denote this -universal property by `universal-property-suspension'`. But, due to the special -nature of the span being pushed out, the suspension of a type enjoys an +universal property by `universal-property-pushout-suspension`. But, due to the +special nature of the span being pushed out, the suspension of a type enjoys an equivalent universal property, here denoted by `universal-property-suspension`. This universal property states that the map `ev-suspension` is an equivalence. -## Definition +## Definitions + +### The universal property of the suspension + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {Y : UU l2} + (s : suspension-structure X Y) + where + + ev-suspension : + {l3 : Level} (Z : UU l3) → (Y → Z) → suspension-structure X Z + pr1 (ev-suspension Z h) = h (north-suspension-structure s) + pr1 (pr2 (ev-suspension Z h)) = h (south-suspension-structure s) + pr2 (pr2 (ev-suspension Z h)) = h ·l (meridian-suspension-structure s) + + universal-property-suspension-Level : (l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) + universal-property-suspension-Level l = + (Z : UU l) → is-equiv (ev-suspension Z) + + universal-property-suspension : UUω + universal-property-suspension = + {l : Level} → universal-property-suspension-Level l +``` ### The universal property of the suspension as a pushout ```agda -universal-property-suspension' : +universal-property-pushout-suspension : (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) (s : suspension-structure X Y) → UU (lsuc l ⊔ l1 ⊔ l2) -universal-property-suspension' l X Y s = +universal-property-pushout-suspension l X Y s = universal-property-pushout l ( const X unit star) ( const X unit star) ( cocone-suspension-structure X Y s) - -is-suspension : - (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (lsuc l ⊔ l1 ⊔ l2) -is-suspension l X Y = - Σ (suspension-structure X Y) (universal-property-suspension' l X Y) -``` - -### The universal property of the suspension reforum - -```agda -ev-suspension : - {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} → - (s : suspension-structure X Y) → - (Z : UU l3) → (Y → Z) → suspension-structure X Z -ev-suspension (pair N (pair S merid)) Z h = - pair (h N) (pair (h S) (h ·l merid)) - -universal-property-suspension : - (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) → - suspension-structure X Y → UU (lsuc l ⊔ l1 ⊔ l2) -universal-property-suspension l X Y s = - (Z : UU l) → is-equiv (ev-suspension s Z) ``` ## Properties @@ -90,7 +91,7 @@ triangle-ev-suspension (pair N (pair S merid)) Z h = refl is-equiv-ev-suspension : { l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} → ( s : suspension-structure X Y) → - ( up-Y : universal-property-suspension' l3 X Y s) → + ( up-Y : universal-property-pushout-suspension l3 X Y s) → ( Z : UU l3) → is-equiv (ev-suspension s Z) is-equiv-ev-suspension {X = X} s up-Y Z = is-equiv-left-map-triangle From 06c000ee3503eec6dda713a98fd0401340903e9c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 01:03:34 +0100 Subject: [PATCH 02/13] `up-product` (I don't want to touch this too much) --- .../products-of-tuples-of-types.lagda.md | 9 --------- ...-property-cartesian-product-types.lagda.md | 20 ++++++++++++------- ...on-cauchy-series-species-of-types.lagda.md | 3 +-- ...-species-of-types-in-subuniverses.lagda.md | 3 +-- ...dirichlet-series-species-of-types.lagda.md | 3 +-- 5 files changed, 16 insertions(+), 22 deletions(-) diff --git a/src/foundation/products-of-tuples-of-types.lagda.md b/src/foundation/products-of-tuples-of-types.lagda.md index 93d246a60c..0fc4d95508 100644 --- a/src/foundation/products-of-tuples-of-types.lagda.md +++ b/src/foundation/products-of-tuples-of-types.lagda.md @@ -38,13 +38,4 @@ pr-product-tuple-types : {l : Level} {n : ℕ} (A : tuple-types l n) (i : Fin n) → product-tuple-types n A → A i pr-product-tuple-types A i f = f i - -{- -equiv-universal-property-product-tuple-types : - {l : Level} {n : ℕ} (A : tuple-types l (succ-ℕ n)) (i : Fin (succ-ℕ n)) → - ( product-tuple-types (succ-ℕ n) A) ≃ - ( ( product-tuple-types n {!!}) × A i) -equiv-universal-property-product-tuple-types A i = - {!!} - -} ``` diff --git a/src/foundation/universal-property-cartesian-product-types.lagda.md b/src/foundation/universal-property-cartesian-product-types.lagda.md index 4cba37f1d2..aad646035d 100644 --- a/src/foundation/universal-property-cartesian-product-types.lagda.md +++ b/src/foundation/universal-property-cartesian-product-types.lagda.md @@ -36,24 +36,30 @@ product ### The universal property of cartesian products as pullbacks ```agda -universal-property-product : +map-up-product : + {l1 l2 l3 : Level} {X : UU l1} {A : X → UU l2} {B : X → UU l3} → + ((x : X) → A x × B x) → (((x : X) → A x) × ((x : X) → B x)) +pr1 (map-up-product f) x = pr1 (f x) +pr2 (map-up-product f) x = pr2 (f x) + +up-product : {l1 l2 l3 : Level} {X : UU l1} {A : X → UU l2} {B : X → UU l3} → ((x : X) → A x × B x) ≃ (((x : X) → A x) × ((x : X) → B x)) -pr1 universal-property-product f = (λ x → pr1 (f x)) , (λ x → pr2 (f x)) -pr2 universal-property-product = +pr1 up-product = map-up-product +pr2 up-product = is-equiv-is-invertible ( λ (f , g) → (λ x → (f x , g x))) ( refl-htpy) ( refl-htpy) - -module _ - {l1 l2 : Level} (A : UU l1) (B : UU l2) - where ``` We construct the cone for two maps into the unit type. ```agda +module _ + {l1 l2 : Level} (A : UU l1) (B : UU l2) + where + cone-prod : cone (const A unit star) (const B unit star) (A × B) pr1 cone-prod = pr1 pr1 (pr2 cone-prod) = pr2 diff --git a/src/species/composition-cauchy-series-species-of-types.lagda.md b/src/species/composition-cauchy-series-species-of-types.lagda.md index 093cd17a22..f3304a68cb 100644 --- a/src/species/composition-cauchy-series-species-of-types.lagda.md +++ b/src/species/composition-cauchy-series-species-of-types.lagda.md @@ -88,8 +88,7 @@ module _ ( λ V → ( equiv-prod ( id-equiv) - ( ( inv-equiv universal-property-product) ∘e - ( equiv-prod id-equiv equiv-ev-pair))) ∘e + ( inv-equiv up-product ∘e equiv-prod id-equiv equiv-ev-pair)) ∘e ( left-unit-law-Σ-is-contr ( is-torsorial-equiv' (Σ U V)) ( Σ U V , id-equiv))))))) ∘e diff --git a/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md b/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md index 9d725e023f..af73cc4fc8 100644 --- a/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md +++ b/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md @@ -159,8 +159,7 @@ module _ ( λ B → ( equiv-prod ( id-equiv) - ( universal-property-product ∘e - equiv-postcomp X (C2 A B))) ∘e + ( up-product ∘e equiv-postcomp X (C2 A B))) ∘e left-unit-law-Σ-is-contr ( is-torsorial-equiv-subuniverse' ( P) diff --git a/src/species/products-dirichlet-series-species-of-types.lagda.md b/src/species/products-dirichlet-series-species-of-types.lagda.md index 8f5b451ac9..d7138beb86 100644 --- a/src/species/products-dirichlet-series-species-of-types.lagda.md +++ b/src/species/products-dirichlet-series-species-of-types.lagda.md @@ -110,8 +110,7 @@ module _ ( λ B → ( equiv-prod ( id-equiv) - ( universal-property-product ∘e - equiv-postcomp X (C1 A B))) ∘e + ( up-product ∘e equiv-postcomp X (C1 A B))) ∘e ( left-unit-law-Σ-is-contr ( is-torsorial-equiv' (A × B)) ( A × B , id-equiv))))) ∘e From 0a00783a8ff1af72b138654926e1f30d6164e241 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 01:35:16 +0100 Subject: [PATCH 03/13] module `terminal-map` --- src/foundation/unit-type.lagda.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/foundation/unit-type.lagda.md b/src/foundation/unit-type.lagda.md index 54127d2476..af60f6353e 100644 --- a/src/foundation/unit-type.lagda.md +++ b/src/foundation/unit-type.lagda.md @@ -48,8 +48,12 @@ ind-unit p star = p ### The terminal map out of a type ```agda -terminal-map : {l : Level} {A : UU l} → A → unit -terminal-map {A = A} = const A unit star +module _ + {l : Level} {A : UU l} + where + + terminal-map : A → unit + terminal-map = const A unit star ``` ### Points as maps out of the unit type From d91220848d1b6bdab4887b66d54a8468cdfbbd29 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 02:38:46 +0100 Subject: [PATCH 04/13] final things --- src/foundation/unit-type.lagda.md | 12 ++++++++---- .../suspensions-of-types.lagda.md | 5 ++--- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/foundation/unit-type.lagda.md b/src/foundation/unit-type.lagda.md index af60f6353e..f3d04ae982 100644 --- a/src/foundation/unit-type.lagda.md +++ b/src/foundation/unit-type.lagda.md @@ -25,7 +25,7 @@ open import foundation-core.truncation-levels ## Idea -The unit type is inductively generated by one point. +The **unit type** is a type inductively generated by a single point. ## Definition @@ -41,7 +41,7 @@ record unit : UU lzero where ### The induction principle of the unit type ```agda -ind-unit : {l : Level} {P : unit → UU l} → P star → ((x : unit) → P x) +ind-unit : {l : Level} {P : unit → UU l} → P star → (x : unit) → P x ind-unit p star = p ``` @@ -59,8 +59,12 @@ module _ ### Points as maps out of the unit type ```agda -point : {l : Level} {A : UU l} → A → (unit → A) -point a = const unit _ a +module _ + {l : Level} {A : UU l} + where + + point : A → (unit → A) + point = const unit A ``` ### Raising the universe level of the unit type diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 39b2091760..0425af9088 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -160,8 +160,7 @@ module _ map-inv-up-suspension : {l : Level} (Z : UU l) → suspension-structure X Z → suspension X → Z - map-inv-up-suspension Z = - map-inv-equiv (equiv-up-suspension Z) + map-inv-up-suspension Z = map-inv-equiv (equiv-up-suspension Z) is-section-map-inv-up-suspension : {l : Level} (Z : UU l) → @@ -173,7 +172,7 @@ module _ is-retraction-map-inv-up-suspension : {l : Level} (Z : UU l) → ( ( map-inv-up-suspension Z) ∘ - ( ev-suspension ((suspension-structure-suspension X)) Z)) ~ id + ( ev-suspension (suspension-structure-suspension X) Z)) ~ id is-retraction-map-inv-up-suspension Z = is-retraction-map-inv-is-equiv (up-suspension Z) From 1e7c7e5b6dd9212186e304f76b65234b8791aee4 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 02:45:00 +0100 Subject: [PATCH 05/13] final changes --- .../dependent-universal-property-suspensions.lagda.md | 7 +------ .../universal-property-suspensions.lagda.md | 6 +----- 2 files changed, 2 insertions(+), 11 deletions(-) diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md index afb61ece1c..21bf24396e 100644 --- a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md @@ -50,14 +50,9 @@ module _ (s : suspension-structure X Y) where - dependent-universal-property-suspension-Level : - (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l) - dependent-universal-property-suspension-Level l = - (B : Y → UU l) → is-equiv (dependent-ev-suspension s B) - dependent-universal-property-suspension : UUω dependent-universal-property-suspension = - {l : Level} → dependent-universal-property-suspension-Level l + {l : Level} (B : Y → UU l) → is-equiv (dependent-ev-suspension s B) ``` #### Coherence between `dependent-ev-suspension` and `dependent-cocone-map` diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md index 12e4296820..c0e98abbf9 100644 --- a/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md @@ -51,13 +51,9 @@ module _ pr1 (pr2 (ev-suspension Z h)) = h (south-suspension-structure s) pr2 (pr2 (ev-suspension Z h)) = h ·l (meridian-suspension-structure s) - universal-property-suspension-Level : (l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) - universal-property-suspension-Level l = - (Z : UU l) → is-equiv (ev-suspension Z) - universal-property-suspension : UUω universal-property-suspension = - {l : Level} → universal-property-suspension-Level l + {l : Level} (Z : UU l) → is-equiv (ev-suspension Z) ``` ### The universal property of the suspension as a pushout From f3f4f94fd5958ec15b9b66fcb81bd07c41609a49 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 02:48:20 +0100 Subject: [PATCH 06/13] final final thing changes --- ...niversal-property-cartesian-product-types.lagda.md | 11 ++++++++--- ...omposition-cauchy-series-species-of-types.lagda.md | 3 ++- ...t-series-species-of-types-in-subuniverses.lagda.md | 2 +- ...roducts-dirichlet-series-species-of-types.lagda.md | 2 +- 4 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/foundation/universal-property-cartesian-product-types.lagda.md b/src/foundation/universal-property-cartesian-product-types.lagda.md index aad646035d..953ce02fed 100644 --- a/src/foundation/universal-property-cartesian-product-types.lagda.md +++ b/src/foundation/universal-property-cartesian-product-types.lagda.md @@ -44,13 +44,18 @@ pr2 (map-up-product f) x = pr2 (f x) up-product : {l1 l2 l3 : Level} {X : UU l1} {A : X → UU l2} {B : X → UU l3} → - ((x : X) → A x × B x) ≃ (((x : X) → A x) × ((x : X) → B x)) -pr1 up-product = map-up-product -pr2 up-product = + is-equiv (map-up-product {A = A} {B}) +up-product = is-equiv-is-invertible ( λ (f , g) → (λ x → (f x , g x))) ( refl-htpy) ( refl-htpy) + +equiv-up-product : + {l1 l2 l3 : Level} {X : UU l1} {A : X → UU l2} {B : X → UU l3} → + ((x : X) → A x × B x) ≃ (((x : X) → A x) × ((x : X) → B x)) +pr1 equiv-up-product = map-up-product +pr2 equiv-up-product = up-product ``` We construct the cone for two maps into the unit type. diff --git a/src/species/composition-cauchy-series-species-of-types.lagda.md b/src/species/composition-cauchy-series-species-of-types.lagda.md index f3304a68cb..e9a9d3e04f 100644 --- a/src/species/composition-cauchy-series-species-of-types.lagda.md +++ b/src/species/composition-cauchy-series-species-of-types.lagda.md @@ -88,7 +88,8 @@ module _ ( λ V → ( equiv-prod ( id-equiv) - ( inv-equiv up-product ∘e equiv-prod id-equiv equiv-ev-pair)) ∘e + ( inv-equiv equiv-up-product ∘e + equiv-prod id-equiv equiv-ev-pair)) ∘e ( left-unit-law-Σ-is-contr ( is-torsorial-equiv' (Σ U V)) ( Σ U V , id-equiv))))))) ∘e diff --git a/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md b/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md index af73cc4fc8..222caf256e 100644 --- a/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md +++ b/src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md @@ -159,7 +159,7 @@ module _ ( λ B → ( equiv-prod ( id-equiv) - ( up-product ∘e equiv-postcomp X (C2 A B))) ∘e + ( equiv-up-product ∘e equiv-postcomp X (C2 A B))) ∘e left-unit-law-Σ-is-contr ( is-torsorial-equiv-subuniverse' ( P) diff --git a/src/species/products-dirichlet-series-species-of-types.lagda.md b/src/species/products-dirichlet-series-species-of-types.lagda.md index d7138beb86..8827da815f 100644 --- a/src/species/products-dirichlet-series-species-of-types.lagda.md +++ b/src/species/products-dirichlet-series-species-of-types.lagda.md @@ -110,7 +110,7 @@ module _ ( λ B → ( equiv-prod ( id-equiv) - ( up-product ∘e equiv-postcomp X (C1 A B))) ∘e + ( equiv-up-product ∘e equiv-postcomp X (C1 A B))) ∘e ( left-unit-law-Σ-is-contr ( is-torsorial-equiv' (A × B)) ( A × B , id-equiv))))) ∘e From bd0f5fb6d0d63c7630eed497dbb6b4febc02047f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 22:44:24 +0100 Subject: [PATCH 07/13] use `cogap` as inverse to `ev-suspension` --- src/foundation-core/equivalences.lagda.md | 4 +- .../universal-property-unit-type.lagda.md | 5 + src/synthetic-homotopy-theory/circle.lagda.md | 19 ++- .../dependent-suspension-structures.lagda.md | 4 +- ...nt-universal-property-suspensions.lagda.md | 2 +- .../functoriality-suspensions.lagda.md | 9 +- .../pushouts.lagda.md | 22 ++- .../suspension-structures.lagda.md | 99 +++++------ .../suspensions-of-types.lagda.md | 157 +++++++++--------- ...erty-suspensions-of-pointed-types.lagda.md | 4 +- .../universal-property-suspensions.lagda.md | 16 +- 11 files changed, 175 insertions(+), 166 deletions(-) diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index d3eeb3f0f0..e68845df72 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/src/foundation-core/equivalences.lagda.md @@ -458,7 +458,7 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where - abstract + opaque is-equiv-htpy : {f : A → B} (g : A → B) → f ~ g → is-equiv g → is-equiv f pr1 (pr1 (is-equiv-htpy g G ((h , H) , (k , K)))) = h @@ -479,7 +479,7 @@ module _ htpy-map-inv-is-equiv : {f g : A → B} (G : f ~ g) (H : is-equiv f) (K : is-equiv g) → - (map-inv-is-equiv H) ~ (map-inv-is-equiv K) + map-inv-is-equiv H ~ map-inv-is-equiv K htpy-map-inv-is-equiv G H K b = ( inv ( is-retraction-map-inv-is-equiv K (map-inv-is-equiv H b))) ∙ diff --git a/src/foundation/universal-property-unit-type.lagda.md b/src/foundation/universal-property-unit-type.lagda.md index 660963fab9..a7ee712ce5 100644 --- a/src/foundation/universal-property-unit-type.lagda.md +++ b/src/foundation/universal-property-unit-type.lagda.md @@ -63,6 +63,11 @@ equiv-universal-property-unit : pr1 (equiv-universal-property-unit Y) = ev-star' Y pr2 (equiv-universal-property-unit Y) = universal-property-unit Y +inv-equiv-universal-property-unit : + {l : Level} (Y : UU l) → Y ≃ (unit → Y) +inv-equiv-universal-property-unit Y = + inv-equiv (equiv-universal-property-unit Y) + abstract is-equiv-point-is-contr : {l1 : Level} {X : UU l1} (x : X) → diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md index 390db0d3c5..2c4667ab1d 100644 --- a/src/synthetic-homotopy-theory/circle.lagda.md +++ b/src/synthetic-homotopy-theory/circle.lagda.md @@ -268,7 +268,7 @@ circle-sphere-1 = circle-sphere-1-north-sphere-1-eq-base-𝕊¹ : Id (circle-sphere-1 (north-sphere 1)) base-𝕊¹ circle-sphere-1-north-sphere-1-eq-base-𝕊¹ = - up-suspension-north-suspension + compute-north-cogap-suspension-structure-suspension ( sphere 0) ( 𝕊¹) ( suspension-structure-sphere-0-𝕊¹) @@ -276,7 +276,7 @@ circle-sphere-1-north-sphere-1-eq-base-𝕊¹ = circle-sphere-1-south-sphere-1-eq-base-𝕊¹ : Id (circle-sphere-1 (south-sphere 1)) base-𝕊¹ circle-sphere-1-south-sphere-1-eq-base-𝕊¹ = - up-suspension-south-suspension + compute-south-cogap-suspension-structure-suspension ( sphere 0) ( 𝕊¹) ( suspension-structure-sphere-0-𝕊¹) @@ -303,7 +303,7 @@ sphere-1-circle-sphere-1-south-sphere-1 = ( ap sphere-1-circle circle-sphere-1-south-sphere-1-eq-base-𝕊¹) ∙ ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1) -apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 : +apply-compute-meridian-cogap-suspension-structure-suspension-sphere-1-circle-sphere-1 : ( n : Fin 2) → coherence-square-identifications ( ap @@ -313,7 +313,8 @@ apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 : ( ap sphere-1-circle (ap circle-sphere-1 (meridian-suspension n))) ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1) ( sphere-1-circle-sphere-1-south-sphere-1) -apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 n = +apply-compute-meridian-cogap-suspension-structure-suspension-sphere-1-circle-sphere-1 + n = ( inv ( assoc ( ap sphere-1-circle (ap circle-sphere-1 (meridian-suspension n))) @@ -330,7 +331,7 @@ apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 n = ( λ x → ( ap sphere-1-circle x) ∙ ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1)) - ( up-suspension-meridian-suspension + ( compute-meridian-cogap-suspension-structure-suspension ( sphere 0) ( 𝕊¹) ( suspension-structure-sphere-0-𝕊¹) @@ -379,7 +380,7 @@ map-sphere-1-circle-sphere-1-meridian (inl (inr n)) = ( meridian-sphere 0 (inl (inr n))) ( sphere-1-circle-sphere-1-north-sphere-1) ( sphere-1-circle-sphere-1-south-sphere-1) - ( ( apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 + ( ( apply-compute-meridian-cogap-suspension-structure-suspension-sphere-1-circle-sphere-1 ( inl (inr n))) ∙ ( identification-right-whisk ( ap-concat @@ -406,7 +407,7 @@ map-sphere-1-circle-sphere-1-meridian (inr n) = ( meridian-sphere 0 (inr n)) ( sphere-1-circle-sphere-1-north-sphere-1) ( sphere-1-circle-sphere-1-south-sphere-1) - ( ( apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 + ( ( apply-compute-meridian-cogap-suspension-structure-suspension-sphere-1-circle-sphere-1 ( inr n)) ∙ ( ap ( λ x → @@ -470,7 +471,7 @@ apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle = ( identification-left-whisk ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1)))) ( inv - ( up-suspension-meridian-suspension + ( compute-meridian-cogap-suspension-structure-suspension (sphere 0) 𝕊¹ suspension-structure-sphere-0-𝕊¹ (one-Fin 1)))) ∙ ( inv ( assoc @@ -501,7 +502,7 @@ apply-up-suspension-meridian-zero-suspension-circle-sphere-1-circle = ( identification-left-whisk ( ap circle-sphere-1 (meridian-suspension (zero-Fin 1))) ( apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle)) ∙ - ( up-suspension-meridian-suspension + ( compute-meridian-cogap-suspension-structure-suspension ( sphere 0) ( 𝕊¹) ( suspension-structure-sphere-0-𝕊¹) diff --git a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md index 8f3ca5a3f0..307726569b 100644 --- a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md @@ -153,7 +153,7 @@ module _ dependent-cocone-dependent-suspension-structure : dependent-suspension-structure B c → - dependent-suspension-cocone B (cocone-suspension-structure X Y c) + dependent-suspension-cocone B (suspension-cocone-suspension-structure c) pr1 (dependent-cocone-dependent-suspension-structure d) t = north-dependent-suspension-structure d pr1 (pr2 (dependent-cocone-dependent-suspension-structure d)) t = @@ -164,7 +164,7 @@ module _ equiv-dependent-suspension-structure-suspension-cocone : ( dependent-suspension-cocone ( B) - ( cocone-suspension-structure X Y c)) ≃ + ( suspension-cocone-suspension-structure c)) ≃ ( dependent-suspension-structure B c) equiv-dependent-suspension-structure-suspension-cocone = ( equiv-Σ diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md index 21bf24396e..620dc4806b 100644 --- a/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md @@ -70,7 +70,7 @@ module _ ( dependent-cocone-map ( const X unit star) ( const X unit star) - ( cocone-suspension-structure X Y s) + ( suspension-cocone-suspension-structure s) ( B))) ~ ( dependent-ev-suspension s B) triangle-dependent-ev-suspension s B = refl-htpy diff --git a/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md b/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md index 6f21d950c8..1cd2fc9919 100644 --- a/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md @@ -50,17 +50,17 @@ module _ map-suspension : suspension A → suspension B map-suspension = - map-inv-up-suspension A (suspension B) map-suspension-structure + cogap-suspension-structure-suspension map-suspension-structure compute-north-map-suspension : map-suspension (north-suspension) = north-suspension compute-north-map-suspension = - up-suspension-north-suspension A (suspension B) map-suspension-structure + compute-north-cogap-suspension-structure-suspension map-suspension-structure compute-south-map-suspension : map-suspension (south-suspension) = south-suspension compute-south-map-suspension = - up-suspension-south-suspension A (suspension B) map-suspension-structure + compute-south-cogap-suspension-structure-suspension map-suspension-structure compute-meridian-map-suspension : (a : A) → @@ -70,8 +70,7 @@ module _ ( meridian-suspension (f a)) ( compute-south-map-suspension) compute-meridian-map-suspension = - up-suspension-meridian-suspension A - ( suspension B) + compute-meridian-cogap-suspension-structure-suspension ( map-suspension-structure) ``` diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md index dafbb62aec..b17dea6d88 100644 --- a/src/synthetic-homotopy-theory/pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pushouts.lagda.md @@ -16,6 +16,8 @@ open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types +open import foundation.retractions +open import foundation.sections open import foundation.universe-levels open import synthetic-homotopy-theory.26-descent @@ -130,11 +132,21 @@ pr2 (equiv-up-pushout f g X) = up-pushout f g X ### The cogap map ```agda -cogap : - { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} - ( f : S → A) (g : S → B) → - { X : UU l4} → cocone f g X → pushout f g → X -cogap f g {X} = map-inv-equiv (equiv-up-pushout f g X) +module _ + {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} + (f : S → A) (g : S → B) { X : UU l4} + where + + cogap : cocone f g X → pushout f g → X + cogap = map-inv-equiv (equiv-up-pushout f g X) + + is-section-cogap : is-section (cocone-map f g (cocone-pushout f g)) cogap + is-section-cogap = is-section-map-inv-equiv (equiv-up-pushout f g X) + + is-retraction-cogap : + is-retraction (cocone-map f g (cocone-pushout f g)) cogap + is-retraction-cogap = + is-retraction-map-inv-equiv (equiv-up-pushout f g X) ``` ### The predicate of being a pushout cocone diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md index 98a7fb11d8..424b77268d 100644 --- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md @@ -108,60 +108,51 @@ module _ ### Equivalence between suspension structures and suspension cocones ```agda -cocone-suspension-structure : - {l1 l2 : Level} (X : UU l1) (Y : UU l2) → - suspension-structure X Y → suspension-cocone X Y -pr1 (cocone-suspension-structure X Y (N , S , merid)) = point N -pr1 (pr2 (cocone-suspension-structure X Y (N , S , merid))) = point S -pr2 (pr2 (cocone-suspension-structure X Y (N , S , merid))) = merid - -equiv-suspension-structure-suspension-cocone : - {l1 l2 : Level} (X : UU l1) (Z : UU l2) → - suspension-cocone X Z ≃ suspension-structure X Z -equiv-suspension-structure-suspension-cocone X Z = - equiv-Σ - ( λ z1 → Σ Z (λ z2 → (x : X) → Id z1 z2)) - ( equiv-universal-property-unit Z) - ( λ z1 → - equiv-Σ - ( λ z2 → (x : X) → Id (z1 star) z2) - ( equiv-universal-property-unit Z) - ( λ z2 → id-equiv)) - -map-equiv-suspension-structure-suspension-cocone : - {l1 l2 : Level} (X : UU l1) (Z : UU l2) → - suspension-cocone X Z → suspension-structure X Z -map-equiv-suspension-structure-suspension-cocone X Z = - map-equiv (equiv-suspension-structure-suspension-cocone X Z) - -is-equiv-map-equiv-suspension-structure-suspension-cocone : - {l1 l2 : Level} (X : UU l1) (Z : UU l2) → - is-equiv (map-equiv-suspension-structure-suspension-cocone X Z) -is-equiv-map-equiv-suspension-structure-suspension-cocone X Z = - is-equiv-map-equiv (equiv-suspension-structure-suspension-cocone X Z) - -map-inv-equiv-suspension-structure-suspension-cocone : - {l1 l2 : Level} (X : UU l1) (Z : UU l2) → - suspension-structure X Z → suspension-cocone X Z -map-inv-equiv-suspension-structure-suspension-cocone X Z = - map-inv-equiv (equiv-suspension-structure-suspension-cocone X Z) - -is-equiv-map-inv-equiv-suspension-structure-suspension-cocone : - {l1 l2 : Level} (X : UU l1) (Z : UU l2) → - is-equiv (map-inv-equiv-suspension-structure-suspension-cocone X Z) -is-equiv-map-inv-equiv-suspension-structure-suspension-cocone X Z = - is-equiv-map-inv-equiv (equiv-suspension-structure-suspension-cocone X Z) - -htpy-comparison-suspension-cocone-suspension-structure : - {l1 l2 : Level} (X : UU l1) (Z : UU l2) → - ( map-inv-equiv-suspension-structure-suspension-cocone X Z) ~ - ( cocone-suspension-structure X Z) -htpy-comparison-suspension-cocone-suspension-structure X Z s = - is-injective-map-equiv - ( equiv-suspension-structure-suspension-cocone X Z) - ( is-section-map-inv-equiv - ( equiv-suspension-structure-suspension-cocone X Z) - ( s)) +module _ + {l1 l2 : Level} {X : UU l1} {Y : UU l2} + where + + suspension-cocone-suspension-structure : + suspension-structure X Y → suspension-cocone X Y + pr1 (suspension-cocone-suspension-structure (N , S , merid)) = point N + pr1 (pr2 (suspension-cocone-suspension-structure (N , S , merid))) = point S + pr2 (pr2 (suspension-cocone-suspension-structure (N , S , merid))) = merid + + suspension-structure-suspension-cocone : + suspension-cocone X Y → suspension-structure X Y + pr1 (suspension-structure-suspension-cocone (N , S , merid)) = N star + pr1 (pr2 (suspension-structure-suspension-cocone (N , S , merid))) = S star + pr2 (pr2 (suspension-structure-suspension-cocone (N , S , merid))) = merid + + is-equiv-suspension-cocone-suspension-structure : + is-equiv suspension-cocone-suspension-structure + is-equiv-suspension-cocone-suspension-structure = + is-equiv-is-invertible + ( suspension-structure-suspension-cocone) + ( refl-htpy) + ( refl-htpy) + + is-equiv-suspension-structure-suspension-cocone : + is-equiv suspension-structure-suspension-cocone + is-equiv-suspension-structure-suspension-cocone = + is-equiv-is-invertible + ( suspension-cocone-suspension-structure) + ( refl-htpy) + ( refl-htpy) + + equiv-suspension-structure-suspension-cocone : + suspension-structure X Y ≃ suspension-cocone X Y + pr1 equiv-suspension-structure-suspension-cocone = + suspension-cocone-suspension-structure + pr2 equiv-suspension-structure-suspension-cocone = + is-equiv-suspension-cocone-suspension-structure + + equiv-suspension-cocone-suspension-structure : + suspension-cocone X Y ≃ suspension-structure X Y + pr1 equiv-suspension-cocone-suspension-structure = + suspension-structure-suspension-cocone + pr2 equiv-suspension-cocone-suspension-structure = + is-equiv-suspension-structure-suspension-cocone ``` #### Characterization of equalities in `suspension-structure` diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 0425af9088..c813ecf849 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -24,6 +24,8 @@ open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.path-algebra +open import foundation.retractions +open import foundation.sections open import foundation.torsorial-type-families open import foundation.transport-along-identifications open import foundation.truncated-types @@ -31,6 +33,7 @@ open import foundation.truncation-levels open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type open import foundation.universe-levels +open import foundation.whiskering-homotopies open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.dependent-cocones-under-spans @@ -110,7 +113,7 @@ module _ cogap-suspension-structure-suspension : suspension X → Y cogap-suspension-structure-suspension = - cogap-suspension (cocone-suspension-structure X Y s) + cogap-suspension (suspension-cocone-suspension-structure s) ``` ### The property of being a suspension @@ -135,85 +138,85 @@ is-suspension s = is-equiv (cogap-suspension-structure-suspension s) ```agda module _ - {l1 : Level} (X : UU l1) + {l1 l2 : Level} {X : UU l1} {Z : UU l2} + where + + is-section-cogap-suspension-structure-suspension : + is-section + ( ev-suspension (suspension-structure-suspension X) Z) + ( cogap-suspension-structure-suspension) + is-section-cogap-suspension-structure-suspension = + ( suspension-structure-suspension-cocone) ·l + ( ( is-section-cogap terminal-map terminal-map) ·r + ( suspension-cocone-suspension-structure)) + + is-retraction-cogap-suspension-structure-suspension : + is-retraction + ( ev-suspension (suspension-structure-suspension X) Z) + ( cogap-suspension-structure-suspension) + is-retraction-cogap-suspension-structure-suspension = + ( is-retraction-cogap terminal-map terminal-map) + +module _ + {l1 l2 : Level} {X : UU l1} {Z : UU l2} where up-suspension : universal-property-suspension (suspension-structure-suspension X) up-suspension Z = - is-equiv-htpy - ( ev-suspension (suspension-structure-suspension X) Z) - ( triangle-ev-suspension - { X = X} - { Y = suspension X} - ( suspension-structure-suspension X) - ( Z)) - ( is-equiv-map-equiv - ( ( equiv-suspension-structure-suspension-cocone X Z) ∘e - ( equiv-up-pushout terminal-map terminal-map Z))) + is-equiv-is-invertible + ( cogap-suspension-structure-suspension) + ( is-section-cogap-suspension-structure-suspension) + ( is-retraction-cogap-suspension-structure-suspension) equiv-up-suspension : - {l : Level} (Z : UU l) → (suspension X → Z) ≃ (suspension-structure X Z) - pr1 (equiv-up-suspension Z) = + (suspension X → Z) ≃ (suspension-structure X Z) + pr1 equiv-up-suspension = ev-suspension (suspension-structure-suspension X) Z - pr2 (equiv-up-suspension Z) = up-suspension Z - - map-inv-up-suspension : - {l : Level} (Z : UU l) → suspension-structure X Z → suspension X → Z - map-inv-up-suspension Z = map-inv-equiv (equiv-up-suspension Z) - - is-section-map-inv-up-suspension : - {l : Level} (Z : UU l) → - ( ( ev-suspension ((suspension-structure-suspension X)) Z) ∘ - ( map-inv-up-suspension Z)) ~ id - is-section-map-inv-up-suspension Z = - is-section-map-inv-is-equiv (up-suspension Z) - - is-retraction-map-inv-up-suspension : - {l : Level} (Z : UU l) → - ( ( map-inv-up-suspension Z) ∘ - ( ev-suspension (suspension-structure-suspension X) Z)) ~ id - is-retraction-map-inv-up-suspension Z = - is-retraction-map-inv-is-equiv (up-suspension Z) - - up-suspension-north-suspension : - {l : Level} (Z : UU l) (c : suspension-structure X Z) → - ( map-inv-up-suspension Z c north-suspension) = + pr2 equiv-up-suspension = up-suspension Z + + compute-north-cogap-suspension-structure-suspension : + (c : suspension-structure X Z) → + ( cogap-suspension-structure-suspension c north-suspension) = ( north-suspension-structure c) - up-suspension-north-suspension Z c = - pr1 (htpy-eq-suspension-structure (is-section-map-inv-up-suspension Z c)) + compute-north-cogap-suspension-structure-suspension c = + pr1 + ( htpy-eq-suspension-structure + ( is-section-cogap-suspension-structure-suspension c)) - up-suspension-south-suspension : - {l : Level} (Z : UU l) (c : suspension-structure X Z) → - ( map-inv-up-suspension Z c south-suspension) = + compute-south-cogap-suspension-structure-suspension : + (c : suspension-structure X Z) → + ( cogap-suspension-structure-suspension c south-suspension) = ( south-suspension-structure c) - up-suspension-south-suspension Z c = + compute-south-cogap-suspension-structure-suspension c = pr1 ( pr2 - ( htpy-eq-suspension-structure (is-section-map-inv-up-suspension Z c))) - - up-suspension-meridian-suspension : - {l : Level} (Z : UU l) (c : suspension-structure X Z) (x : X) → - ( ( ap (map-inv-up-suspension Z c) (meridian-suspension x)) ∙ - ( up-suspension-south-suspension Z c)) = - ( ( up-suspension-north-suspension Z c) ∙ - ( meridian-suspension-structure c x)) - up-suspension-meridian-suspension Z c = + ( htpy-eq-suspension-structure + ( is-section-cogap-suspension-structure-suspension c))) + + compute-meridian-cogap-suspension-structure-suspension : + (c : suspension-structure X Z) (x : X) → + ( ( ap (cogap-suspension-structure-suspension c) (meridian-suspension x)) ∙ + ( compute-south-cogap-suspension-structure-suspension c)) = + ( ( compute-north-cogap-suspension-structure-suspension c) ∙ + ( meridian-suspension-structure c x)) + compute-meridian-cogap-suspension-structure-suspension c = pr2 ( pr2 - ( htpy-eq-suspension-structure (is-section-map-inv-up-suspension Z c))) + ( htpy-eq-suspension-structure + ( is-section-cogap-suspension-structure-suspension c))) ev-suspension-up-suspension : - {l : Level} (Z : UU l) (c : suspension-structure X Z) → + (c : suspension-structure X Z) → ( ev-suspension ( suspension-structure-suspension X) ( Z) - ( map-inv-up-suspension Z c)) = c - ev-suspension-up-suspension {l} Z c = + ( cogap-suspension-structure-suspension c)) = c + ev-suspension-up-suspension c = eq-htpy-suspension-structure - ( ( up-suspension-north-suspension Z c) , - ( up-suspension-south-suspension Z c) , - ( up-suspension-meridian-suspension Z c)) + ( ( compute-north-cogap-suspension-structure-suspension c) , + ( compute-south-cogap-suspension-structure-suspension c) , + ( compute-meridian-cogap-suspension-structure-suspension c)) ``` ### The suspension of `X` has the dependent universal property of suspensions @@ -231,9 +234,7 @@ dup-suspension {X = X} B = ( dependent-cocone-map ( terminal-map) ( terminal-map) - ( cocone-suspension-structure - ( X) - ( suspension X) + ( suspension-cocone-suspension-structure ( suspension-structure-suspension X)) ( B))) ( inv-htpy @@ -248,8 +249,7 @@ dup-suspension {X = X} B = ( dependent-cocone-map ( terminal-map) ( terminal-map) - ( cocone-suspension-structure X - ( suspension X) + ( suspension-cocone-suspension-structure ( suspension-structure-suspension X)) ( B)) ( dependent-up-pushout terminal-map terminal-map B) @@ -262,10 +262,9 @@ equiv-dup-suspension : {l1 l2 : Level} {X : UU l1} (B : suspension X → UU l2) → (( x : suspension X) → B x) ≃ ( dependent-suspension-structure B (suspension-structure-suspension X)) -pr1 (equiv-dup-suspension {l2 = l2} {X = X} B) = +pr1 (equiv-dup-suspension {X = X} B) = dependent-ev-suspension (suspension-structure-suspension X) B -pr2 (equiv-dup-suspension {l2 = l2} B) = - dup-suspension B +pr2 (equiv-dup-suspension B) = dup-suspension B module _ {l1 l2 : Level} {X : UU l1} (B : suspension X → UU l2) @@ -274,8 +273,7 @@ module _ map-inv-dup-suspension : dependent-suspension-structure B (suspension-structure-suspension X) → (x : suspension X) → B x - map-inv-dup-suspension = - map-inv-is-equiv (dup-suspension B) + map-inv-dup-suspension = map-inv-is-equiv (dup-suspension B) is-section-map-inv-dup-suspension : ( ( dependent-ev-suspension (suspension-structure-suspension X) B) ∘ @@ -290,9 +288,10 @@ module _ is-retraction-map-inv-is-equiv (dup-suspension B) dup-suspension-north-suspension : - (d : dependent-suspension-structure - ( B) - ( suspension-structure-suspension X)) → + (d : + dependent-suspension-structure + ( B) + ( suspension-structure-suspension X)) → ( map-inv-dup-suspension d north-suspension) = ( north-dependent-suspension-structure d) dup-suspension-north-suspension d = @@ -303,9 +302,10 @@ module _ ( is-section-map-inv-dup-suspension d)) dup-suspension-south-suspension : - (d : dependent-suspension-structure - ( B) - ( suspension-structure-suspension X)) → + (d : + dependent-suspension-structure + ( B) + ( suspension-structure-suspension X)) → ( map-inv-dup-suspension d south-suspension) = ( south-dependent-suspension-structure d) dup-suspension-south-suspension d = @@ -316,9 +316,10 @@ module _ ( is-section-map-inv-dup-suspension d)) dup-suspension-meridian-suspension : - (d : dependent-suspension-structure - ( B) - ( suspension-structure-suspension X)) + (d : + dependent-suspension-structure + ( B) + ( suspension-structure-suspension X)) (x : X) → coherence-square-identifications ( ap diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md index 173fcc0b33..3d661d9be6 100644 --- a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md @@ -94,7 +94,7 @@ module _ pr1 pointed-map-counit-suspension-loop-adjunction = map-counit-suspension-loop-adjunction pr2 pointed-map-counit-suspension-loop-adjunction = - up-suspension-north-suspension + compute-north-cogap-suspension-structure-suspension ( type-Ω X) ( type-Pointed-Type X) ( point-Pointed-Type X , point-Pointed-Type X , id) @@ -127,7 +127,7 @@ module _ ( Y) ( map-pointed-map f∗)) pr2 (inv-transpose-suspension-loop-adjunction f∗) = - up-suspension-north-suspension + compute-north-cogap-suspension-structure-suspension ( type-Pointed-Type X) ( type-Pointed-Type Y) ( suspension-structure-map-into-Ω diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md index c0e98abbf9..13819ca651 100644 --- a/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-suspensions.lagda.md @@ -49,7 +49,7 @@ module _ {l3 : Level} (Z : UU l3) → (Y → Z) → suspension-structure X Z pr1 (ev-suspension Z h) = h (north-suspension-structure s) pr1 (pr2 (ev-suspension Z h)) = h (south-suspension-structure s) - pr2 (pr2 (ev-suspension Z h)) = h ·l (meridian-suspension-structure s) + pr2 (pr2 (ev-suspension Z h)) = h ·l meridian-suspension-structure s universal-property-suspension : UUω universal-property-suspension = @@ -66,7 +66,7 @@ universal-property-pushout-suspension l X Y s = universal-property-pushout l ( const X unit star) ( const X unit star) - ( cocone-suspension-structure X Y s) + ( suspension-cocone-suspension-structure s) ``` ## Properties @@ -76,13 +76,13 @@ triangle-ev-suspension : {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} → (s : suspension-structure X Y) → (Z : UU l3) → - ( ( map-equiv-suspension-structure-suspension-cocone X Z) ∘ + ( ( suspension-structure-suspension-cocone) ∘ ( cocone-map ( const X unit star) ( const X unit star) - ( cocone-suspension-structure X Y s))) ~ + ( suspension-cocone-suspension-structure s))) ~ ( ev-suspension s Z) -triangle-ev-suspension (pair N (pair S merid)) Z h = refl +triangle-ev-suspension (N , S , merid) Z h = refl is-equiv-ev-suspension : { l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} → @@ -92,12 +92,12 @@ is-equiv-ev-suspension : is-equiv-ev-suspension {X = X} s up-Y Z = is-equiv-left-map-triangle ( ev-suspension s Z) - ( map-equiv-suspension-structure-suspension-cocone X Z) + ( suspension-structure-suspension-cocone) ( cocone-map ( const X unit star) ( const X unit star) - ( cocone-suspension-structure X _ s)) + ( suspension-cocone-suspension-structure s)) ( inv-htpy (triangle-ev-suspension s Z)) ( up-Y Z) - ( is-equiv-map-equiv-suspension-structure-suspension-cocone X Z) + ( is-equiv-suspension-structure-suspension-cocone) ``` From d88f4b74578b24cb09966905583c35ab3b718db0 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 22:52:06 +0100 Subject: [PATCH 08/13] make it typecheck --- src/synthetic-homotopy-theory/circle.lagda.md | 34 ++++----- .../functoriality-suspensions.lagda.md | 8 +-- .../suspensions-of-types.lagda.md | 71 ++++++++++--------- ...erty-suspensions-of-pointed-types.lagda.md | 16 ++--- 4 files changed, 57 insertions(+), 72 deletions(-) diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md index 2c4667ab1d..30547b964b 100644 --- a/src/synthetic-homotopy-theory/circle.lagda.md +++ b/src/synthetic-homotopy-theory/circle.lagda.md @@ -260,25 +260,19 @@ pr2 (pr2 suspension-structure-sphere-0-𝕊¹) = map-sphere-0-eq-base-𝕊¹ circle-sphere-1 : sphere 1 → 𝕊¹ circle-sphere-1 = - map-inv-up-suspension - ( sphere 0) - ( 𝕊¹) + cogap-suspension-structure ( suspension-structure-sphere-0-𝕊¹) circle-sphere-1-north-sphere-1-eq-base-𝕊¹ : - Id (circle-sphere-1 (north-sphere 1)) base-𝕊¹ + circle-sphere-1 (north-sphere 1) = base-𝕊¹ circle-sphere-1-north-sphere-1-eq-base-𝕊¹ = - compute-north-cogap-suspension-structure-suspension - ( sphere 0) - ( 𝕊¹) + compute-north-cogap-suspension-structure ( suspension-structure-sphere-0-𝕊¹) circle-sphere-1-south-sphere-1-eq-base-𝕊¹ : Id (circle-sphere-1 (south-sphere 1)) base-𝕊¹ circle-sphere-1-south-sphere-1-eq-base-𝕊¹ = - compute-south-cogap-suspension-structure-suspension - ( sphere 0) - ( 𝕊¹) + compute-south-cogap-suspension-structure ( suspension-structure-sphere-0-𝕊¹) ``` @@ -303,7 +297,7 @@ sphere-1-circle-sphere-1-south-sphere-1 = ( ap sphere-1-circle circle-sphere-1-south-sphere-1-eq-base-𝕊¹) ∙ ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1) -apply-compute-meridian-cogap-suspension-structure-suspension-sphere-1-circle-sphere-1 : +apply-compute-meridian-cogap-suspension-structure-sphere-1-circle-sphere-1 : ( n : Fin 2) → coherence-square-identifications ( ap @@ -313,7 +307,7 @@ apply-compute-meridian-cogap-suspension-structure-suspension-sphere-1-circle-sph ( ap sphere-1-circle (ap circle-sphere-1 (meridian-suspension n))) ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1) ( sphere-1-circle-sphere-1-south-sphere-1) -apply-compute-meridian-cogap-suspension-structure-suspension-sphere-1-circle-sphere-1 +apply-compute-meridian-cogap-suspension-structure-sphere-1-circle-sphere-1 n = ( inv ( assoc @@ -331,9 +325,7 @@ apply-compute-meridian-cogap-suspension-structure-suspension-sphere-1-circle-sph ( λ x → ( ap sphere-1-circle x) ∙ ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1)) - ( compute-meridian-cogap-suspension-structure-suspension - ( sphere 0) - ( 𝕊¹) + ( compute-meridian-cogap-suspension-structure ( suspension-structure-sphere-0-𝕊¹) ( n))) @@ -380,7 +372,7 @@ map-sphere-1-circle-sphere-1-meridian (inl (inr n)) = ( meridian-sphere 0 (inl (inr n))) ( sphere-1-circle-sphere-1-north-sphere-1) ( sphere-1-circle-sphere-1-south-sphere-1) - ( ( apply-compute-meridian-cogap-suspension-structure-suspension-sphere-1-circle-sphere-1 + ( ( apply-compute-meridian-cogap-suspension-structure-sphere-1-circle-sphere-1 ( inl (inr n))) ∙ ( identification-right-whisk ( ap-concat @@ -407,7 +399,7 @@ map-sphere-1-circle-sphere-1-meridian (inr n) = ( meridian-sphere 0 (inr n)) ( sphere-1-circle-sphere-1-north-sphere-1) ( sphere-1-circle-sphere-1-south-sphere-1) - ( ( apply-compute-meridian-cogap-suspension-structure-suspension-sphere-1-circle-sphere-1 + ( ( apply-compute-meridian-cogap-suspension-structure-sphere-1-circle-sphere-1 ( inr n)) ∙ ( ap ( λ x → @@ -471,8 +463,8 @@ apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle = ( identification-left-whisk ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1)))) ( inv - ( compute-meridian-cogap-suspension-structure-suspension - (sphere 0) 𝕊¹ suspension-structure-sphere-0-𝕊¹ (one-Fin 1)))) ∙ + ( compute-meridian-cogap-suspension-structure + suspension-structure-sphere-0-𝕊¹ (one-Fin 1)))) ∙ ( inv ( assoc ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1)))) @@ -502,9 +494,7 @@ apply-up-suspension-meridian-zero-suspension-circle-sphere-1-circle = ( identification-left-whisk ( ap circle-sphere-1 (meridian-suspension (zero-Fin 1))) ( apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle)) ∙ - ( compute-meridian-cogap-suspension-structure-suspension - ( sphere 0) - ( 𝕊¹) + ( compute-meridian-cogap-suspension-structure ( suspension-structure-sphere-0-𝕊¹) ( zero-Fin 1)) diff --git a/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md b/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md index 1cd2fc9919..b9eb9d22b9 100644 --- a/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md @@ -50,17 +50,17 @@ module _ map-suspension : suspension A → suspension B map-suspension = - cogap-suspension-structure-suspension map-suspension-structure + cogap-suspension-structure map-suspension-structure compute-north-map-suspension : map-suspension (north-suspension) = north-suspension compute-north-map-suspension = - compute-north-cogap-suspension-structure-suspension map-suspension-structure + compute-north-cogap-suspension-structure map-suspension-structure compute-south-map-suspension : map-suspension (south-suspension) = south-suspension compute-south-map-suspension = - compute-south-cogap-suspension-structure-suspension map-suspension-structure + compute-south-cogap-suspension-structure map-suspension-structure compute-meridian-map-suspension : (a : A) → @@ -70,7 +70,7 @@ module _ ( meridian-suspension (f a)) ( compute-south-map-suspension) compute-meridian-map-suspension = - compute-meridian-cogap-suspension-structure-suspension + compute-meridian-cogap-suspension-structure ( map-suspension-structure) ``` diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index c813ecf849..5bbfe8736d 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -111,8 +111,8 @@ module _ {l1 l2 : Level} {X : UU l1} {Y : UU l2} (s : suspension-structure X Y) where - cogap-suspension-structure-suspension : suspension X → Y - cogap-suspension-structure-suspension = + cogap-suspension-structure : suspension X → Y + cogap-suspension-structure = cogap-suspension (suspension-cocone-suspension-structure s) ``` @@ -129,7 +129,7 @@ large proposition. is-suspension : {l1 l2 : Level} {X : UU l1} {Y : UU l2} → suspension-structure X Y → UU (l1 ⊔ l2) -is-suspension s = is-equiv (cogap-suspension-structure-suspension s) +is-suspension s = is-equiv (cogap-suspension-structure s) ``` ## Properties @@ -141,82 +141,83 @@ module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} where - is-section-cogap-suspension-structure-suspension : + is-section-cogap-suspension-structure : is-section ( ev-suspension (suspension-structure-suspension X) Z) - ( cogap-suspension-structure-suspension) - is-section-cogap-suspension-structure-suspension = + ( cogap-suspension-structure) + is-section-cogap-suspension-structure = ( suspension-structure-suspension-cocone) ·l ( ( is-section-cogap terminal-map terminal-map) ·r ( suspension-cocone-suspension-structure)) - is-retraction-cogap-suspension-structure-suspension : + is-retraction-cogap-suspension-structure : is-retraction ( ev-suspension (suspension-structure-suspension X) Z) - ( cogap-suspension-structure-suspension) - is-retraction-cogap-suspension-structure-suspension = + ( cogap-suspension-structure) + is-retraction-cogap-suspension-structure = ( is-retraction-cogap terminal-map terminal-map) +up-suspension : + {l1 : Level} {X : UU l1} → + universal-property-suspension (suspension-structure-suspension X) +up-suspension Z = + is-equiv-is-invertible + ( cogap-suspension-structure) + ( is-section-cogap-suspension-structure) + ( is-retraction-cogap-suspension-structure) + module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} where - up-suspension : - universal-property-suspension (suspension-structure-suspension X) - up-suspension Z = - is-equiv-is-invertible - ( cogap-suspension-structure-suspension) - ( is-section-cogap-suspension-structure-suspension) - ( is-retraction-cogap-suspension-structure-suspension) - equiv-up-suspension : (suspension X → Z) ≃ (suspension-structure X Z) pr1 equiv-up-suspension = ev-suspension (suspension-structure-suspension X) Z pr2 equiv-up-suspension = up-suspension Z - compute-north-cogap-suspension-structure-suspension : + compute-north-cogap-suspension-structure : (c : suspension-structure X Z) → - ( cogap-suspension-structure-suspension c north-suspension) = + ( cogap-suspension-structure c north-suspension) = ( north-suspension-structure c) - compute-north-cogap-suspension-structure-suspension c = + compute-north-cogap-suspension-structure c = pr1 ( htpy-eq-suspension-structure - ( is-section-cogap-suspension-structure-suspension c)) + ( is-section-cogap-suspension-structure c)) - compute-south-cogap-suspension-structure-suspension : + compute-south-cogap-suspension-structure : (c : suspension-structure X Z) → - ( cogap-suspension-structure-suspension c south-suspension) = + ( cogap-suspension-structure c south-suspension) = ( south-suspension-structure c) - compute-south-cogap-suspension-structure-suspension c = + compute-south-cogap-suspension-structure c = pr1 ( pr2 ( htpy-eq-suspension-structure - ( is-section-cogap-suspension-structure-suspension c))) + ( is-section-cogap-suspension-structure c))) - compute-meridian-cogap-suspension-structure-suspension : + compute-meridian-cogap-suspension-structure : (c : suspension-structure X Z) (x : X) → - ( ( ap (cogap-suspension-structure-suspension c) (meridian-suspension x)) ∙ - ( compute-south-cogap-suspension-structure-suspension c)) = - ( ( compute-north-cogap-suspension-structure-suspension c) ∙ + ( ( ap (cogap-suspension-structure c) (meridian-suspension x)) ∙ + ( compute-south-cogap-suspension-structure c)) = + ( ( compute-north-cogap-suspension-structure c) ∙ ( meridian-suspension-structure c x)) - compute-meridian-cogap-suspension-structure-suspension c = + compute-meridian-cogap-suspension-structure c = pr2 ( pr2 ( htpy-eq-suspension-structure - ( is-section-cogap-suspension-structure-suspension c))) + ( is-section-cogap-suspension-structure c))) ev-suspension-up-suspension : (c : suspension-structure X Z) → ( ev-suspension ( suspension-structure-suspension X) ( Z) - ( cogap-suspension-structure-suspension c)) = c + ( cogap-suspension-structure c)) = c ev-suspension-up-suspension c = eq-htpy-suspension-structure - ( ( compute-north-cogap-suspension-structure-suspension c) , - ( compute-south-cogap-suspension-structure-suspension c) , - ( compute-meridian-cogap-suspension-structure-suspension c)) + ( ( compute-north-cogap-suspension-structure c) , + ( compute-south-cogap-suspension-structure c) , + ( compute-meridian-cogap-suspension-structure c)) ``` ### The suspension of `X` has the dependent universal property of suspensions diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md index 3d661d9be6..a6a4ba9420 100644 --- a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md @@ -86,7 +86,7 @@ module _ suspension (type-Ω X) → type-Pointed-Type X map-counit-suspension-loop-adjunction = map-inv-is-equiv - ( up-suspension (type-Ω X) (type-Pointed-Type X)) + ( up-suspension (type-Pointed-Type X)) ( point-Pointed-Type X , point-Pointed-Type X , id) pointed-map-counit-suspension-loop-adjunction : @@ -94,9 +94,7 @@ module _ pr1 pointed-map-counit-suspension-loop-adjunction = map-counit-suspension-loop-adjunction pr2 pointed-map-counit-suspension-loop-adjunction = - compute-north-cogap-suspension-structure-suspension - ( type-Ω X) - ( type-Pointed-Type X) + compute-north-cogap-suspension-structure ( point-Pointed-Type X , point-Pointed-Type X , id) ``` @@ -119,17 +117,13 @@ module _ inv-transpose-suspension-loop-adjunction : (X →∗ Ω Y) → (suspension-Pointed-Type X →∗ Y) pr1 (inv-transpose-suspension-loop-adjunction f∗) = - map-inv-up-suspension - ( type-Pointed-Type X) - ( type-Pointed-Type Y) + cogap-suspension-structure ( suspension-structure-map-into-Ω ( type-Pointed-Type X) ( Y) ( map-pointed-map f∗)) pr2 (inv-transpose-suspension-loop-adjunction f∗) = - compute-north-cogap-suspension-structure-suspension - ( type-Pointed-Type X) - ( type-Pointed-Type Y) + compute-north-cogap-suspension-structure ( suspension-structure-map-into-Ω ( type-Pointed-Type X) ( Y) @@ -172,7 +166,7 @@ module _ ( equiv-right-swap-Σ) ∘e ( equiv-Σ-equiv-base ( λ c → pr1 c = point-Pointed-Type Y) - ( equiv-up-suspension (type-Pointed-Type X) (type-Pointed-Type Y))) + ( equiv-up-suspension)) ``` #### The equivalence in the suspension-loop space adjunction is pointed From 699e9ad9da52bfa1d8d8a75be1f8b30fec076c9f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 22:54:19 +0100 Subject: [PATCH 09/13] revert `opaque` --- src/foundation-core/equivalences.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index e68845df72..43c1596431 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/src/foundation-core/equivalences.lagda.md @@ -458,7 +458,7 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where - opaque + abstract is-equiv-htpy : {f : A → B} (g : A → B) → f ~ g → is-equiv g → is-equiv f pr1 (pr1 (is-equiv-htpy g G ((h , H) , (k , K)))) = h From 39947a540cb927d23154fd174b6c114e4977dc26 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 23:00:37 +0100 Subject: [PATCH 10/13] revert some eroneous renamings --- src/synthetic-homotopy-theory/circle.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md index 30547b964b..c95ab00088 100644 --- a/src/synthetic-homotopy-theory/circle.lagda.md +++ b/src/synthetic-homotopy-theory/circle.lagda.md @@ -297,7 +297,7 @@ sphere-1-circle-sphere-1-south-sphere-1 = ( ap sphere-1-circle circle-sphere-1-south-sphere-1-eq-base-𝕊¹) ∙ ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1) -apply-compute-meridian-cogap-suspension-structure-sphere-1-circle-sphere-1 : +apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 : ( n : Fin 2) → coherence-square-identifications ( ap @@ -307,7 +307,7 @@ apply-compute-meridian-cogap-suspension-structure-sphere-1-circle-sphere-1 : ( ap sphere-1-circle (ap circle-sphere-1 (meridian-suspension n))) ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1) ( sphere-1-circle-sphere-1-south-sphere-1) -apply-compute-meridian-cogap-suspension-structure-sphere-1-circle-sphere-1 +apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 n = ( inv ( assoc @@ -372,7 +372,7 @@ map-sphere-1-circle-sphere-1-meridian (inl (inr n)) = ( meridian-sphere 0 (inl (inr n))) ( sphere-1-circle-sphere-1-north-sphere-1) ( sphere-1-circle-sphere-1-south-sphere-1) - ( ( apply-compute-meridian-cogap-suspension-structure-sphere-1-circle-sphere-1 + ( ( apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 ( inl (inr n))) ∙ ( identification-right-whisk ( ap-concat @@ -399,7 +399,7 @@ map-sphere-1-circle-sphere-1-meridian (inr n) = ( meridian-sphere 0 (inr n)) ( sphere-1-circle-sphere-1-north-sphere-1) ( sphere-1-circle-sphere-1-south-sphere-1) - ( ( apply-compute-meridian-cogap-suspension-structure-sphere-1-circle-sphere-1 + ( ( apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 ( inr n)) ∙ ( ap ( λ x → From 46c6707520e9a0ef1f09733aa54b54f8e9f18d44 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 14:25:56 +0100 Subject: [PATCH 11/13] Update src/species/composition-cauchy-series-species-of-types.lagda.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Vojtěch Štěpančík --- .../composition-cauchy-series-species-of-types.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/species/composition-cauchy-series-species-of-types.lagda.md b/src/species/composition-cauchy-series-species-of-types.lagda.md index e9a9d3e04f..2daa753e6a 100644 --- a/src/species/composition-cauchy-series-species-of-types.lagda.md +++ b/src/species/composition-cauchy-series-species-of-types.lagda.md @@ -88,8 +88,8 @@ module _ ( λ V → ( equiv-prod ( id-equiv) - ( inv-equiv equiv-up-product ∘e - equiv-prod id-equiv equiv-ev-pair)) ∘e + ( ( inv-equiv equiv-up-product) ∘e + ( equiv-prod id-equiv equiv-ev-pair))) ∘e ( left-unit-law-Σ-is-contr ( is-torsorial-equiv' (Σ U V)) ( Σ U V , id-equiv))))))) ∘e From 7bdd9d4638709d85908954c68ff1a6a468143524 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 14:28:38 +0100 Subject: [PATCH 12/13] Update src/synthetic-homotopy-theory/circle.lagda.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Vojtěch Štěpančík --- src/synthetic-homotopy-theory/circle.lagda.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md index c95ab00088..0850b4e851 100644 --- a/src/synthetic-homotopy-theory/circle.lagda.md +++ b/src/synthetic-homotopy-theory/circle.lagda.md @@ -464,7 +464,8 @@ apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle = ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1)))) ( inv ( compute-meridian-cogap-suspension-structure - suspension-structure-sphere-0-𝕊¹ (one-Fin 1)))) ∙ + ( suspension-structure-sphere-0-𝕊¹) + ( one-Fin 1)))) ∙ ( inv ( assoc ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1)))) From ea1c023c77c283e17d815546814da54a16edded4 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 14:52:19 +0100 Subject: [PATCH 13/13] `dependent-cogap-suspension` --- src/synthetic-homotopy-theory/circle.lagda.md | 14 +- .../coequalizers.lagda.md | 2 +- .../functoriality-suspensions.lagda.md | 8 +- .../pushouts.lagda.md | 17 ++- .../suspensions-of-types.lagda.md | 135 +++++++----------- ...erty-suspensions-of-pointed-types.lagda.md | 6 +- 6 files changed, 83 insertions(+), 99 deletions(-) diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md index 0850b4e851..0d3f688f2e 100644 --- a/src/synthetic-homotopy-theory/circle.lagda.md +++ b/src/synthetic-homotopy-theory/circle.lagda.md @@ -260,19 +260,19 @@ pr2 (pr2 suspension-structure-sphere-0-𝕊¹) = map-sphere-0-eq-base-𝕊¹ circle-sphere-1 : sphere 1 → 𝕊¹ circle-sphere-1 = - cogap-suspension-structure + cogap-suspension ( suspension-structure-sphere-0-𝕊¹) circle-sphere-1-north-sphere-1-eq-base-𝕊¹ : circle-sphere-1 (north-sphere 1) = base-𝕊¹ circle-sphere-1-north-sphere-1-eq-base-𝕊¹ = - compute-north-cogap-suspension-structure + compute-north-cogap-suspension ( suspension-structure-sphere-0-𝕊¹) circle-sphere-1-south-sphere-1-eq-base-𝕊¹ : Id (circle-sphere-1 (south-sphere 1)) base-𝕊¹ circle-sphere-1-south-sphere-1-eq-base-𝕊¹ = - compute-south-cogap-suspension-structure + compute-south-cogap-suspension ( suspension-structure-sphere-0-𝕊¹) ``` @@ -325,7 +325,7 @@ apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 ( λ x → ( ap sphere-1-circle x) ∙ ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1)) - ( compute-meridian-cogap-suspension-structure + ( compute-meridian-cogap-suspension ( suspension-structure-sphere-0-𝕊¹) ( n))) @@ -426,7 +426,7 @@ pr2 (pr2 dependent-suspension-structure-sphere-1-circle-sphere-1) = sphere-1-circle-sphere-1 : section sphere-1-circle pr1 sphere-1-circle-sphere-1 = circle-sphere-1 pr2 sphere-1-circle-sphere-1 = - map-inv-dup-suspension + dependent-cogap-suspension ( λ x → (sphere-1-circle (circle-sphere-1 x)) = x) ( dependent-suspension-structure-sphere-1-circle-sphere-1) ``` @@ -463,7 +463,7 @@ apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle = ( identification-left-whisk ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1)))) ( inv - ( compute-meridian-cogap-suspension-structure + ( compute-meridian-cogap-suspension ( suspension-structure-sphere-0-𝕊¹) ( one-Fin 1)))) ∙ ( inv @@ -495,7 +495,7 @@ apply-up-suspension-meridian-zero-suspension-circle-sphere-1-circle = ( identification-left-whisk ( ap circle-sphere-1 (meridian-suspension (zero-Fin 1))) ( apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle)) ∙ - ( compute-meridian-cogap-suspension-structure + ( compute-meridian-cogap-suspension ( suspension-structure-sphere-0-𝕊¹) ( zero-Fin 1)) diff --git a/src/synthetic-homotopy-theory/coequalizers.lagda.md b/src/synthetic-homotopy-theory/coequalizers.lagda.md index 23b837f960..e172509b17 100644 --- a/src/synthetic-homotopy-theory/coequalizers.lagda.md +++ b/src/synthetic-homotopy-theory/coequalizers.lagda.md @@ -96,7 +96,7 @@ module _ ( cocone-pushout ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g)))) - ( dependent-up-pushout + ( dup-pushout ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( P))) diff --git a/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md b/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md index b9eb9d22b9..ee63c9d038 100644 --- a/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md +++ b/src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md @@ -50,17 +50,17 @@ module _ map-suspension : suspension A → suspension B map-suspension = - cogap-suspension-structure map-suspension-structure + cogap-suspension map-suspension-structure compute-north-map-suspension : map-suspension (north-suspension) = north-suspension compute-north-map-suspension = - compute-north-cogap-suspension-structure map-suspension-structure + compute-north-cogap-suspension map-suspension-structure compute-south-map-suspension : map-suspension (south-suspension) = south-suspension compute-south-map-suspension = - compute-south-cogap-suspension-structure map-suspension-structure + compute-south-cogap-suspension map-suspension-structure compute-meridian-map-suspension : (a : A) → @@ -70,7 +70,7 @@ module _ ( meridian-suspension (f a)) ( compute-south-map-suspension) compute-meridian-map-suspension = - compute-meridian-cogap-suspension-structure + compute-meridian-cogap-suspension ( map-suspension-structure) ``` diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md index b17dea6d88..8d9e69a856 100644 --- a/src/synthetic-homotopy-theory/pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pushouts.lagda.md @@ -22,6 +22,7 @@ open import foundation.universe-levels open import synthetic-homotopy-theory.26-descent open import synthetic-homotopy-theory.cocones-under-spans +open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.dependent-universal-property-pushouts open import synthetic-homotopy-theory.flattening-lemma-pushouts open import synthetic-homotopy-theory.universal-property-pushouts @@ -202,17 +203,25 @@ module _ ```agda module _ {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} + (f : S → A) (g : S → B) where - dependent-up-pushout : - (f : S → A) (g : S → B) → + dup-pushout : dependent-universal-property-pushout l4 f g (cocone-pushout f g) - dependent-up-pushout f g = + dup-pushout = dependent-universal-property-universal-property-pushout ( f) ( g) ( cocone-pushout f g) ( up-pushout f g) + + equiv-dup-pushout : + (P : pushout f g → UU l4) → + ((x : pushout f g) → P x) ≃ dependent-cocone f g (cocone-pushout f g) P + pr1 (equiv-dup-pushout P) = + dependent-cocone-map f g (cocone-pushout f g) P + pr2 (equiv-dup-pushout P) = + dup-pushout P ``` ### Computation with the cogap map @@ -378,7 +387,7 @@ square commute (almost) trivially. ( f) ( g) ( cocone-pushout f g) - ( dependent-up-pushout f g)) + ( dup-pushout f g)) ( refl-htpy) ( λ _ → inv diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md index 5bbfe8736d..814bb08cde 100644 --- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md @@ -98,10 +98,10 @@ cocone-suspension : cocone-suspension X = cocone-pushout (terminal-map {A = X}) (terminal-map {A = X}) -cogap-suspension : +cogap-suspension' : {l1 l2 : Level} {X : UU l1} {Y : UU l2} → cocone terminal-map terminal-map Y → pushout terminal-map terminal-map → Y -cogap-suspension {X = X} = cogap (terminal-map {A = X}) (terminal-map {A = X}) +cogap-suspension' {X = X} = cogap (terminal-map {A = X}) (terminal-map {A = X}) ``` ### The cogap map of a suspension structure @@ -111,9 +111,9 @@ module _ {l1 l2 : Level} {X : UU l1} {Y : UU l2} (s : suspension-structure X Y) where - cogap-suspension-structure : suspension X → Y - cogap-suspension-structure = - cogap-suspension (suspension-cocone-suspension-structure s) + cogap-suspension : suspension X → Y + cogap-suspension = + cogap-suspension' (suspension-cocone-suspension-structure s) ``` ### The property of being a suspension @@ -129,7 +129,7 @@ large proposition. is-suspension : {l1 l2 : Level} {X : UU l1} {Y : UU l2} → suspension-structure X Y → UU (l1 ⊔ l2) -is-suspension s = is-equiv (cogap-suspension-structure s) +is-suspension s = is-equiv (cogap-suspension s) ``` ## Properties @@ -141,20 +141,20 @@ module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} where - is-section-cogap-suspension-structure : + is-section-cogap-suspension : is-section ( ev-suspension (suspension-structure-suspension X) Z) - ( cogap-suspension-structure) - is-section-cogap-suspension-structure = + ( cogap-suspension) + is-section-cogap-suspension = ( suspension-structure-suspension-cocone) ·l - ( ( is-section-cogap terminal-map terminal-map) ·r - ( suspension-cocone-suspension-structure)) + ( is-section-cogap terminal-map terminal-map) ·r + ( suspension-cocone-suspension-structure) - is-retraction-cogap-suspension-structure : + is-retraction-cogap-suspension : is-retraction ( ev-suspension (suspension-structure-suspension X) Z) - ( cogap-suspension-structure) - is-retraction-cogap-suspension-structure = + ( cogap-suspension) + is-retraction-cogap-suspension = ( is-retraction-cogap terminal-map terminal-map) up-suspension : @@ -162,9 +162,9 @@ up-suspension : universal-property-suspension (suspension-structure-suspension X) up-suspension Z = is-equiv-is-invertible - ( cogap-suspension-structure) - ( is-section-cogap-suspension-structure) - ( is-retraction-cogap-suspension-structure) + ( cogap-suspension) + ( is-section-cogap-suspension) + ( is-retraction-cogap-suspension) module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} @@ -176,48 +176,48 @@ module _ ev-suspension (suspension-structure-suspension X) Z pr2 equiv-up-suspension = up-suspension Z - compute-north-cogap-suspension-structure : + compute-north-cogap-suspension : (c : suspension-structure X Z) → - ( cogap-suspension-structure c north-suspension) = + ( cogap-suspension c north-suspension) = ( north-suspension-structure c) - compute-north-cogap-suspension-structure c = + compute-north-cogap-suspension c = pr1 ( htpy-eq-suspension-structure - ( is-section-cogap-suspension-structure c)) + ( is-section-cogap-suspension c)) - compute-south-cogap-suspension-structure : + compute-south-cogap-suspension : (c : suspension-structure X Z) → - ( cogap-suspension-structure c south-suspension) = + ( cogap-suspension c south-suspension) = ( south-suspension-structure c) - compute-south-cogap-suspension-structure c = + compute-south-cogap-suspension c = pr1 ( pr2 ( htpy-eq-suspension-structure - ( is-section-cogap-suspension-structure c))) + ( is-section-cogap-suspension c))) - compute-meridian-cogap-suspension-structure : + compute-meridian-cogap-suspension : (c : suspension-structure X Z) (x : X) → - ( ( ap (cogap-suspension-structure c) (meridian-suspension x)) ∙ - ( compute-south-cogap-suspension-structure c)) = - ( ( compute-north-cogap-suspension-structure c) ∙ + ( ( ap (cogap-suspension c) (meridian-suspension x)) ∙ + ( compute-south-cogap-suspension c)) = + ( ( compute-north-cogap-suspension c) ∙ ( meridian-suspension-structure c x)) - compute-meridian-cogap-suspension-structure c = + compute-meridian-cogap-suspension c = pr2 ( pr2 ( htpy-eq-suspension-structure - ( is-section-cogap-suspension-structure c))) + ( is-section-cogap-suspension c))) ev-suspension-up-suspension : (c : suspension-structure X Z) → ( ev-suspension ( suspension-structure-suspension X) ( Z) - ( cogap-suspension-structure c)) = c + ( cogap-suspension c)) = c ev-suspension-up-suspension c = eq-htpy-suspension-structure - ( ( compute-north-cogap-suspension-structure c) , - ( compute-south-cogap-suspension-structure c) , - ( compute-meridian-cogap-suspension-structure c)) + ( ( compute-north-cogap-suspension c) , + ( compute-south-cogap-suspension c) , + ( compute-meridian-cogap-suspension c)) ``` ### The suspension of `X` has the dependent universal property of suspensions @@ -227,41 +227,16 @@ dup-suspension : {l1 : Level} {X : UU l1} → dependent-universal-property-suspension (suspension-structure-suspension X) dup-suspension {X = X} B = - is-equiv-htpy - ( map-equiv - ( equiv-dependent-suspension-structure-suspension-cocone + is-equiv-htpy-equiv' + ( ( equiv-dependent-suspension-structure-suspension-cocone ( suspension-structure-suspension X) - ( B)) ∘ - ( dependent-cocone-map - ( terminal-map) - ( terminal-map) - ( suspension-cocone-suspension-structure - ( suspension-structure-suspension X)) - ( B))) - ( inv-htpy - ( triangle-dependent-ev-suspension - ( suspension-structure-suspension X) - ( B))) - ( is-equiv-comp - ( map-equiv - ( equiv-dependent-suspension-structure-suspension-cocone - ( suspension-structure-suspension X) - ( B))) - ( dependent-cocone-map - ( terminal-map) - ( terminal-map) - ( suspension-cocone-suspension-structure - ( suspension-structure-suspension X)) - ( B)) - ( dependent-up-pushout terminal-map terminal-map B) - ( is-equiv-map-equiv - ( equiv-dependent-suspension-structure-suspension-cocone - ( suspension-structure-suspension X) - ( B)))) + ( B)) ∘e + ( equiv-dup-pushout terminal-map terminal-map B)) + ( triangle-dependent-ev-suspension (suspension-structure-suspension X) B) equiv-dup-suspension : {l1 l2 : Level} {X : UU l1} (B : suspension X → UU l2) → - (( x : suspension X) → B x) ≃ + ( (x : suspension X) → B x) ≃ ( dependent-suspension-structure B (suspension-structure-suspension X)) pr1 (equiv-dup-suspension {X = X} B) = dependent-ev-suspension (suspension-structure-suspension X) B @@ -271,21 +246,21 @@ module _ {l1 l2 : Level} {X : UU l1} (B : suspension X → UU l2) where - map-inv-dup-suspension : + dependent-cogap-suspension : dependent-suspension-structure B (suspension-structure-suspension X) → (x : suspension X) → B x - map-inv-dup-suspension = map-inv-is-equiv (dup-suspension B) + dependent-cogap-suspension = map-inv-is-equiv (dup-suspension B) - is-section-map-inv-dup-suspension : + is-section-dependent-cogap-suspension : ( ( dependent-ev-suspension (suspension-structure-suspension X) B) ∘ - ( map-inv-dup-suspension)) ~ id - is-section-map-inv-dup-suspension = + ( dependent-cogap-suspension)) ~ id + is-section-dependent-cogap-suspension = is-section-map-inv-is-equiv (dup-suspension B) - is-retraction-map-inv-dup-suspension : - ( ( map-inv-dup-suspension) ∘ + is-retraction-dependent-cogap-suspension : + ( ( dependent-cogap-suspension) ∘ ( dependent-ev-suspension (suspension-structure-suspension X) B)) ~ id - is-retraction-map-inv-dup-suspension = + is-retraction-dependent-cogap-suspension = is-retraction-map-inv-is-equiv (dup-suspension B) dup-suspension-north-suspension : @@ -293,28 +268,28 @@ module _ dependent-suspension-structure ( B) ( suspension-structure-suspension X)) → - ( map-inv-dup-suspension d north-suspension) = + ( dependent-cogap-suspension d north-suspension) = ( north-dependent-suspension-structure d) dup-suspension-north-suspension d = north-htpy-dependent-suspension-structure ( B) ( htpy-eq-dependent-suspension-structure ( B) - ( is-section-map-inv-dup-suspension d)) + ( is-section-dependent-cogap-suspension d)) dup-suspension-south-suspension : (d : dependent-suspension-structure ( B) ( suspension-structure-suspension X)) → - ( map-inv-dup-suspension d south-suspension) = + ( dependent-cogap-suspension d south-suspension) = ( south-dependent-suspension-structure d) dup-suspension-south-suspension d = south-htpy-dependent-suspension-structure ( B) ( htpy-eq-dependent-suspension-structure ( B) - ( is-section-map-inv-dup-suspension d)) + ( is-section-dependent-cogap-suspension d)) dup-suspension-meridian-suspension : (d : @@ -327,7 +302,7 @@ module _ ( tr B (meridian-suspension x)) ( dup-suspension-north-suspension d)) ( apd - ( map-inv-dup-suspension d) + ( dependent-cogap-suspension d) ( meridian-suspension x)) ( meridian-dependent-suspension-structure d x) ( dup-suspension-south-suspension d) @@ -336,7 +311,7 @@ module _ ( B) ( htpy-eq-dependent-suspension-structure ( B) - ( is-section-map-inv-dup-suspension d)) + ( is-section-dependent-cogap-suspension d)) ``` ### Characterization of homotopies between functions with domain a suspension diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md index a6a4ba9420..a638e4ea4b 100644 --- a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md @@ -94,7 +94,7 @@ module _ pr1 pointed-map-counit-suspension-loop-adjunction = map-counit-suspension-loop-adjunction pr2 pointed-map-counit-suspension-loop-adjunction = - compute-north-cogap-suspension-structure + compute-north-cogap-suspension ( point-Pointed-Type X , point-Pointed-Type X , id) ``` @@ -117,13 +117,13 @@ module _ inv-transpose-suspension-loop-adjunction : (X →∗ Ω Y) → (suspension-Pointed-Type X →∗ Y) pr1 (inv-transpose-suspension-loop-adjunction f∗) = - cogap-suspension-structure + cogap-suspension ( suspension-structure-map-into-Ω ( type-Pointed-Type X) ( Y) ( map-pointed-map f∗)) pr2 (inv-transpose-suspension-loop-adjunction f∗) = - compute-north-cogap-suspension-structure + compute-north-cogap-suspension ( suspension-structure-map-into-Ω ( type-Pointed-Type X) ( Y)