diff --git a/agda-unimath.agda-lib b/agda-unimath.agda-lib index 44045614215..4f49cf98cd9 100644 --- a/agda-unimath.agda-lib +++ b/agda-unimath.agda-lib @@ -1,3 +1,3 @@ name: agda-unimath include: src -flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions -WnoWithoutKFlagPrimEraseEquality --no-postfix-projections +flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions --confluence-check -WnoWithoutKFlagPrimEraseEquality --no-postfix-projections diff --git a/docs/DESIGN-PRINCIPLES.md b/docs/DESIGN-PRINCIPLES.md index d66229a164e..b29492deb22 100644 --- a/docs/DESIGN-PRINCIPLES.md +++ b/docs/DESIGN-PRINCIPLES.md @@ -23,7 +23,7 @@ makes use of several postulates. 6. The **truncation operations** are postulated in [`foundation.truncations`](foundation.truncations.md) 7. The **interval** is postulated in - [`synthetic-homotopy-theory.interval-type`](synthetic-homotopy-theory.interval-type.md) + [`synthetic-homotopy-theory.interval`](synthetic-homotopy-theory.interval.md) 8. The **circle** is postulated in [`synthetic-homotopy-theory.circle`](synthetic-homotopy-theory.circle.md) 9. **Pushouts** are postulated in @@ -39,8 +39,8 @@ makes use of several postulates. Note that there is some redundancy in the postulates we assume. For example, the [univalence axiom implies function extensionality](foundation.univalence-implies-function-extensionality.md), but we still assume function extensionality separately. Furthermore, -[the interval type is contractible](synthetic-homotopy-theory.interval-type.md), -and the higher inductive types in the agda-unimath library only have computation +[the interval type is contractible](synthetic-homotopy-theory.interval.md), and +the higher inductive types in the agda-unimath library only have computation rules up to identification, so there is no need at all to postulate it. The [circle](synthetic-homotopy-theory.circle.md) can be constructed as the type of `β„€`-[torsors](group-theory.torsors.md), and the diff --git a/references.bib b/references.bib index 52836201613..539ae53bf2e 100644 --- a/references.bib +++ b/references.bib @@ -308,6 +308,22 @@ @article{CR21 keywords = {algebraic geometry,cohesive homotopy type theory,factorization systems,Homotopy type theory,modal homotopy type theory}, } +@article{CSY22, + title = {Ambidexterity in chromatic homotopy theory}, + author = {Carmeli, Shachar and Schlank, Tomer M. and Yanovski, Lior}, + year = 2022, + journal = {Invent. Math.}, + fjournal = {Inventiones Mathematicae}, + volume = 228, + number = 3, + pages = {1145--1254}, + doi = {10.1007/s00222-022-01099-9}, + issn = {0020-9910,1432-1297}, + mrclass = {55P43 (55P60)}, + mrnumber = 4419631, + mrreviewer = {Lennart\ Meier}, +} + @online{DavidJaz/Cohesion, title = {DavidJaz/Cohesion}, author = {David Jaz Meyers}, @@ -717,7 +733,7 @@ @article{MP87 issn = {0021-8693}, } -@online{MR23, +@online{MR23a, title = {Delooping the Sign Homomorphism in Univalent Mathematics}, author = {Mangel, Γ‰lΓ©onore and Rijke, Egbert}, year = 2023, @@ -731,6 +747,19 @@ @online{MR23 keywords = {20B30 03B15,Mathematics - Group Theory,Mathematics - Logic}, } +@online{MR23b, + title = {Commuting {{Cohesions}}}, + author = {Myers, David Jaz and Riley, Mitchell}, + year = 2023, + month = {01}, + date = {2023-01-31}, + eprint = {2301.13780}, + eprinttype = {arxiv}, + eprintclass = {math}, + abstract = {Shulman's spatial type theory internalizes the modalities of Lawvere's axiomatic cohesion in a homotopy type theory, enabling many of the constructions from Schreiber's modal approach to differential cohomology to be carried out synthetically. In spatial type theory, every type carries a spatial cohesion among its points and every function is continuous with respect to this. But in mathematical practice, objects may be spatial in more than one way at the same time; for example, a simplicial space has both topological and simplicial structures. In this paper, we put forward a type theory with "commuting focuses" which allows for types to carry multiple kinds of spatial structure. The theory is a relatively painless extension of spatial type theory, and enables us to give a synthetic account of simplicial, differential, equivariant, and other cohesions carried by the same types. We demonstrate the theory by showing that the homotopy type of any differential stack may be computed from a discrete simplicial set derived from the \textbackslash v\{C\}ech nerve of any good cover. We also give other examples of commuting cohesions, such as differential equivariant types and supergeometric types, laying the groundwork for a synthetic account of Schreiber and Sati's proper orbifold cohomology.}, + langid = {english}, +} + @book{MRR88, title = {A {{Course}} in {{Constructive Algebra}}}, author = {Mines, Ray and Richman, Fred and Ruitenburg, Wim}, @@ -865,6 +894,24 @@ @online{Rij22draft pubstate = {draft}, } +@misc{RS17, + title = {A type theory for synthetic $\infty$-categories}, + author = {Riehl, Emily and Shulman, Michael}, + year = 2017, + journal = {Higher Structures}, + shortjournal = {High. Struct.}, + volume = 1, + number = 1, + pages = {147--224}, + issn = {2209-0606}, + eprint = {1705.07442}, + eprinttype = {arxiv}, + archiveprefix = {arXiv}, + eprintclass = {math}, + primaryclass = {math.CT}, + url = {https://emilyriehl.github.io/files/synthetic.pdf}, +} + @article{RSS20, title = {Modalities in Homotopy Type Theory}, author = {Rijke, Egbert and Shulman, Michael and Spitters, Bas}, diff --git a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md index ecac11c0d16..183ae444d4a 100644 --- a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md @@ -205,4 +205,4 @@ module _ ## References -{{#bibliography}} {{#reference MR23}} +{{#bibliography}} {{#reference MR23a}} diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md index 663176ff43c..cb691ead7bd 100644 --- a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md @@ -1642,4 +1642,4 @@ module _ ## References -{{#bibliography}} {{#reference MR23}} +{{#bibliography}} {{#reference MR23a}} diff --git a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md index 249f47ebbe6..484d8a35b13 100644 --- a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md @@ -825,4 +825,4 @@ module _ ## References -{{#bibliography}} {{#reference MR23}} +{{#bibliography}} {{#reference MR23a}} diff --git a/src/foundation-core/truncated-types.lagda.md b/src/foundation-core/truncated-types.lagda.md index fb88b4c3df5..b8284da19d2 100644 --- a/src/foundation-core/truncated-types.lagda.md +++ b/src/foundation-core/truncated-types.lagda.md @@ -21,7 +21,9 @@ open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences open import foundation-core.homotopies open import foundation-core.identity-types +open import foundation-core.invertible-maps open import foundation-core.propositions +open import foundation-core.retractions open import foundation-core.retracts-of-types open import foundation-core.transport-along-identifications open import foundation-core.truncation-levels @@ -76,8 +78,7 @@ module _ abstract is-trunc-succ-is-trunc : (k : 𝕋) {l : Level} {A : UU l} β†’ is-trunc k A β†’ is-trunc (succ-𝕋 k) A - pr1 (is-trunc-succ-is-trunc neg-two-𝕋 H x y) = eq-is-contr H - pr2 (is-trunc-succ-is-trunc neg-two-𝕋 H x .x) refl = left-inv (pr2 H x) + is-trunc-succ-is-trunc neg-two-𝕋 = is-prop-is-contr is-trunc-succ-is-trunc (succ-𝕋 k) H x y = is-trunc-succ-is-trunc k (H x y) truncated-type-succ-Truncated-Type : @@ -122,11 +123,11 @@ module _ where is-trunc-retract-of : - {k : 𝕋} {A : UU l1} {B : UU l2} β†’ + (k : 𝕋) {A : UU l1} {B : UU l2} β†’ A retract-of B β†’ is-trunc k B β†’ is-trunc k A - is-trunc-retract-of {neg-two-𝕋} = is-contr-retract-of _ - is-trunc-retract-of {succ-𝕋 k} R H x y = - is-trunc-retract-of (retract-eq R x y) (H (pr1 R x) (pr1 R y)) + is-trunc-retract-of neg-two-𝕋 = is-contr-retract-of _ + is-trunc-retract-of (succ-𝕋 k) R H x y = + is-trunc-retract-of k (retract-eq R x y) (H (pr1 R x) (pr1 R y)) ``` ### `k`-truncated types are closed under equivalences @@ -137,7 +138,7 @@ abstract {l1 l2 : Level} (k : 𝕋) {A : UU l1} (B : UU l2) (f : A β†’ B) β†’ is-equiv f β†’ is-trunc k B β†’ is-trunc k A is-trunc-is-equiv k B f is-equiv-f = - is-trunc-retract-of (pair f (pr2 is-equiv-f)) + is-trunc-retract-of k (pair f (pr2 is-equiv-f)) abstract is-trunc-equiv : @@ -181,6 +182,21 @@ abstract is-trunc-emb k f = is-trunc-is-emb k (map-emb f) (is-emb-map-emb f) ``` +In fact, it suffices that the map's action on identifications has a retraction. + +```agda +abstract + is-trunc-retraction-ap : + {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A β†’ B) β†’ + ((x y : A) β†’ retraction (ap f {x} {y})) β†’ + is-trunc (succ-𝕋 k) B β†’ is-trunc (succ-𝕋 k) A + is-trunc-retraction-ap k f Ef H x y = + is-trunc-retract-of k (ap f , Ef x y) (H (f x) (f y)) +``` + +- See [path-cosplit maps](foundation.path-cosplit-maps.md) for the concept of a + map whose action on identifications has a retraction. + ### Truncated types are closed under dependent pair types ```agda @@ -244,7 +260,7 @@ abstract {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} β†’ is-trunc k A β†’ is-trunc k B β†’ is-trunc k (A Γ— B) is-trunc-product k is-trunc-A is-trunc-B = - is-trunc-Ξ£ is-trunc-A (Ξ» x β†’ is-trunc-B) + is-trunc-Ξ£ is-trunc-A (Ξ» _ β†’ is-trunc-B) product-Truncated-Type : {l1 l2 : Level} (k : 𝕋) β†’ @@ -255,37 +271,43 @@ pr2 (product-Truncated-Type k A B) = is-trunc-product k ( is-trunc-type-Truncated-Type A) ( is-trunc-type-Truncated-Type B) +``` +We need only show that each factor is `k`-truncated given that the opposite +factor has an element when `k β‰₯ -1`. + +```agda is-trunc-product' : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} β†’ - (B β†’ is-trunc (succ-𝕋 k) A) β†’ (A β†’ is-trunc (succ-𝕋 k) B) β†’ + (B β†’ is-trunc (succ-𝕋 k) A) β†’ + (A β†’ is-trunc (succ-𝕋 k) B) β†’ is-trunc (succ-𝕋 k) (A Γ— B) is-trunc-product' k f g (pair a b) (pair a' b') = is-trunc-equiv k - ( Eq-product (pair a b) (pair a' b')) + ( Eq-product (a , b) (pair a' b')) ( equiv-pair-eq (pair a b) (pair a' b')) ( is-trunc-product k (f b a a') (g a b b')) -is-trunc-left-factor-product : +is-trunc-left-factor-product' : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} β†’ is-trunc k (A Γ— B) β†’ B β†’ is-trunc k A -is-trunc-left-factor-product neg-two-𝕋 {A} {B} H b = +is-trunc-left-factor-product' neg-two-𝕋 {A} {B} H b = is-contr-left-factor-product A B H -is-trunc-left-factor-product (succ-𝕋 k) H b a a' = - is-trunc-left-factor-product k {A = (a ＝ a')} {B = (b ＝ b)} +is-trunc-left-factor-product' (succ-𝕋 k) H b a a' = + is-trunc-left-factor-product' k {A = (a ＝ a')} {B = (b ＝ b)} ( is-trunc-equiv' k ( pair a b ＝ pair a' b) ( equiv-pair-eq (pair a b) (pair a' b)) ( H (pair a b) (pair a' b))) ( refl) -is-trunc-right-factor-product : +is-trunc-right-factor-product' : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} β†’ is-trunc k (A Γ— B) β†’ A β†’ is-trunc k B -is-trunc-right-factor-product neg-two-𝕋 {A} {B} H a = +is-trunc-right-factor-product' neg-two-𝕋 {A} {B} H a = is-contr-right-factor-product A B H -is-trunc-right-factor-product (succ-𝕋 k) {A} {B} H a b b' = - is-trunc-right-factor-product k {A = (a ＝ a)} {B = (b ＝ b')} +is-trunc-right-factor-product' (succ-𝕋 k) {A} {B} H a b b' = + is-trunc-right-factor-product' k {A = (a ＝ a)} {B = (b ＝ b')} ( is-trunc-equiv' k ( pair a b ＝ pair a b') ( equiv-pair-eq (pair a b) (pair a b')) @@ -353,7 +375,7 @@ abstract {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} β†’ is-trunc k B β†’ is-trunc k (A β†’ B) is-trunc-function-type k {A} {B} is-trunc-B = - is-trunc-Ξ  k {B = Ξ» (x : A) β†’ B} (Ξ» x β†’ is-trunc-B) + is-trunc-Ξ  k {B = Ξ» (x : A) β†’ B} (Ξ» _ β†’ is-trunc-B) function-type-Truncated-Type : {l1 l2 : Level} {k : 𝕋} (A : UU l1) (B : Truncated-Type l2 k) β†’ @@ -421,7 +443,12 @@ module _ ( is-trunc-function-type k H) ( Ξ» h β†’ is-trunc-Ξ  k (Ξ» x β†’ is-trunc-Id H (h (f x)) x)))) +``` + +Alternatively, this follows from the fact that equivalences embed into function +types, and function types between `k`-truncated types are `k`-truncated. +```agda type-equiv-Truncated-Type : {l1 l2 : Level} {k : 𝕋} (A : Truncated-Type l1 k) (B : Truncated-Type l2 k) β†’ UU (l1 βŠ” l2) diff --git a/src/foundation-core/univalence.lagda.md b/src/foundation-core/univalence.lagda.md index bc951b0bcd2..c11c7dd16b3 100644 --- a/src/foundation-core/univalence.lagda.md +++ b/src/foundation-core/univalence.lagda.md @@ -108,8 +108,8 @@ abstract is-torsorial-equiv-based-univalence : {l : Level} (A : UU l) β†’ based-univalence-axiom A β†’ is-torsorial (Ξ» (B : UU l) β†’ A ≃ B) - is-torsorial-equiv-based-univalence A UA = - fundamental-theorem-id' (Ξ» B β†’ equiv-eq) UA + is-torsorial-equiv-based-univalence A = + fundamental-theorem-id' (Ξ» B β†’ equiv-eq) ``` ### Contractibility of the total space of equivalences implies univalence diff --git a/src/foundation/0-connected-types.lagda.md b/src/foundation/0-connected-types.lagda.md index d2bdc9203d1..4a089498ff9 100644 --- a/src/foundation/0-connected-types.lagda.md +++ b/src/foundation/0-connected-types.lagda.md @@ -41,8 +41,15 @@ open import foundation-core.truncation-levels ## Idea -A type is said to be connected if its type of connected components, i.e., its -set truncation, is contractible. +A type is said to be +{{#concept "0-connected" Disambiguation="type" Agda=is-0-connected}} if its type +of [connected components](foundation.connected-components.md), i.e., its +[set truncation](foundation.set-truncations.md), is +[contractible](foundation-core.contractible-types.md). + +## Definitions + +### The predicate on types of being 0-connected ```agda is-0-connected-Prop : {l : Level} β†’ UU l β†’ Prop l @@ -68,7 +75,13 @@ abstract {l : Level} {A : UU l} β†’ is-0-connected A β†’ (x y : A) β†’ mere-eq x y mere-eq-is-0-connected {A = A} H x y = apply-effectiveness-unit-trunc-Set (eq-is-contr H) +``` +## Properties + +### A type is 0-connected if there is an element of that type such that every element is merely equal to it + +```agda abstract is-0-connected-mere-eq : {l : Level} {A : UU l} (a : A) β†’ @@ -79,7 +92,11 @@ abstract ( apply-dependent-universal-property-trunc-Set' ( Ξ» x β†’ set-Prop (Id-Prop (trunc-Set A) (unit-trunc-Set a) x)) ( Ξ» x β†’ apply-effectiveness-unit-trunc-Set' (e x))) +``` + +### A type is 0-connected if it is inhabited and all elements are merely equal +```agda abstract is-0-connected-mere-eq-is-inhabited : {l : Level} {A : UU l} β†’ @@ -88,7 +105,11 @@ abstract apply-universal-property-trunc-Prop H ( is-0-connected-Prop _) ( Ξ» a β†’ is-0-connected-mere-eq a (K a)) +``` + +### A type is is 0-connected iff there is a point inclusion which is surjective +```agda is-0-connected-is-surjective-point : {l1 : Level} {A : UU l1} (a : A) β†’ is-surjective (point a) β†’ is-0-connected A @@ -109,10 +130,15 @@ abstract ( mere-eq-is-0-connected H a x) ( trunc-Prop (fiber (point a) x)) ( Ξ» where refl β†’ unit-trunc-Prop (star , refl)) +``` + +### The evaluation map at a point of a 0-connected type into a `k+1`-truncated type is `k`-truncated +```agda is-trunc-map-ev-point-is-connected : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (a : A) β†’ - is-0-connected A β†’ is-trunc (succ-𝕋 k) B β†’ + is-0-connected A β†’ + is-trunc (succ-𝕋 k) B β†’ is-trunc-map k (ev-point' a {B}) is-trunc-map-ev-point-is-connected k {A} {B} a H K = is-trunc-map-comp k @@ -123,11 +149,14 @@ is-trunc-map-ev-point-is-connected k {A} {B} a H K = ( is-trunc-map-precomp-Ξ -is-surjective k ( is-surjective-point-is-0-connected a H) ( Ξ» _ β†’ (B , K))) +``` +### 0-connected types satisfy the dependent universal property of 0-connected types + +```agda equiv-dependent-universal-property-is-0-connected : {l1 : Level} {A : UU l1} (a : A) β†’ is-0-connected A β†’ - ( {l : Level} (P : A β†’ Prop l) β†’ - ((x : A) β†’ type-Prop (P x)) ≃ type-Prop (P a)) + {l : Level} (P : A β†’ Prop l) β†’ ((x : A) β†’ type-Prop (P x)) ≃ type-Prop (P a) equiv-dependent-universal-property-is-0-connected a H P = ( equiv-universal-property-unit (type-Prop (P a))) ∘e ( equiv-dependent-universal-property-surjection-is-surjective @@ -169,19 +198,24 @@ abstract is-0-connected A is-0-connected-is-surjective-fiber-inclusion a H = is-0-connected-mere-eq a (mere-eq-is-surjective-fiber-inclusion a H) +``` +### 0-connected types are closed under equivalences + +```agda is-0-connected-equiv : {l1 l2 : Level} {A : UU l1} {B : UU l2} β†’ - (A ≃ B) β†’ is-0-connected B β†’ is-0-connected A -is-0-connected-equiv e = is-contr-equiv _ (equiv-trunc-Set e) + A ≃ B β†’ is-0-connected B β†’ is-0-connected A +is-0-connected-equiv {B = B} e = + is-contr-equiv (type-trunc-Set B) (equiv-trunc-Set e) is-0-connected-equiv' : {l1 l2 : Level} {A : UU l1} {B : UU l2} β†’ - (A ≃ B) β†’ is-0-connected A β†’ is-0-connected B + A ≃ B β†’ is-0-connected A β†’ is-0-connected B is-0-connected-equiv' e = is-0-connected-equiv (inv-equiv e) ``` -### `0`-connected types are closed under cartesian products +### 0-connected types are closed under cartesian products ```agda module _ @@ -197,7 +231,7 @@ module _ ( is-contr-product p1 p2) ``` -### The unit type is `0`-connected +### The unit type is 0-connected ```agda abstract @@ -206,12 +240,11 @@ abstract is-contr-equiv' unit equiv-unit-trunc-unit-Set is-contr-unit ``` -### A contractible type is `0`-connected +### Contractible types are 0-connected ```agda is-0-connected-is-contr : - {l : Level} (X : UU l) β†’ - is-contr X β†’ is-0-connected X + {l : Level} (X : UU l) β†’ is-contr X β†’ is-0-connected X is-0-connected-is-contr X p = is-contr-equiv X (inv-equiv (equiv-unit-trunc-Set (X , is-set-is-contr p))) p ``` diff --git a/src/foundation/action-on-identifications-functions.lagda.md b/src/foundation/action-on-identifications-functions.lagda.md index 5e4162ad9da..215e151c740 100644 --- a/src/foundation/action-on-identifications-functions.lagda.md +++ b/src/foundation/action-on-identifications-functions.lagda.md @@ -100,7 +100,7 @@ ap-inv f refl = refl ```agda ap-const : {l1 l2 : Level} {A : UU l1} {B : UU l2} (b : B) {x y : A} - (p : x ＝ y) β†’ (ap (const A b) p) ＝ refl + (p : x ＝ y) β†’ ap (const A b) p ＝ refl ap-const b refl = refl ``` diff --git a/src/foundation/booleans.lagda.md b/src/foundation/booleans.lagda.md index b1e7d99e326..3375ffc2b6b 100644 --- a/src/foundation/booleans.lagda.md +++ b/src/foundation/booleans.lagda.md @@ -75,11 +75,11 @@ module _ ```agda module _ - {l : Level} {P : UU l} + {l : Level} {A : UU l} where - rec-bool : P β†’ P β†’ bool β†’ P - rec-bool = ind-bool (Ξ» _ β†’ P) + rec-bool : A β†’ A β†’ bool β†’ A + rec-bool = ind-bool (Ξ» _ β†’ A) ``` ### The `if_then_else` function diff --git a/src/foundation/cartesian-morphisms-arrows.lagda.md b/src/foundation/cartesian-morphisms-arrows.lagda.md index 58ea9ebfbba..67aaa388c7e 100644 --- a/src/foundation/cartesian-morphisms-arrows.lagda.md +++ b/src/foundation/cartesian-morphisms-arrows.lagda.md @@ -38,6 +38,7 @@ open import foundation.whiskering-homotopies-composition open import foundation-core.commuting-squares-of-maps open import foundation-core.homotopies open import foundation-core.propositions +open import foundation-core.sections open import foundation-core.universal-property-pullbacks ``` @@ -1064,6 +1065,79 @@ module _ ( is-cartesian-cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow) ``` +### Base change of sections + +Given a cartesian morphism of arrows + +```text + A ------> X + | ⌟ | + f | | g + ∨ ∨ + B ------> Y + j +``` + +then if `g` has a section so does `f`. More generally, for every map `s` such +that `g ∘ s ∘ j ~ j`, there exists a section of `f`. + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + {f : A β†’ B} {g : X β†’ Y} + (Ξ± : cartesian-hom-arrow f g) + (s : Y β†’ X) + (H : + map-codomain-cartesian-hom-arrow f g Ξ± ~ + g ∘ s ∘ map-codomain-cartesian-hom-arrow f g Ξ±) + where + + cone-section-base-change' : + cone (map-codomain-cartesian-hom-arrow f g Ξ±) g B + cone-section-base-change' = + ( id , s ∘ map-codomain-cartesian-hom-arrow f g Ξ± , H) + + map-section-base-change' : + B β†’ A + map-section-base-change' = + gap-is-pullback + ( map-codomain-cartesian-hom-arrow f g Ξ±) + ( g) + ( cone-cartesian-hom-arrow f g Ξ±) + ( is-cartesian-cartesian-hom-arrow f g Ξ±) + ( cone-section-base-change') + + is-section-map-section-base-change' : + is-section f map-section-base-change' + is-section-map-section-base-change' = + htpy-vertical-map-gap-is-pullback + ( map-codomain-cartesian-hom-arrow f g Ξ±) + ( g) + ( cone-cartesian-hom-arrow f g Ξ±) + ( is-cartesian-cartesian-hom-arrow f g Ξ±) + ( cone-section-base-change') + + section-base-change' : section f + section-base-change' = + ( map-section-base-change' , is-section-map-section-base-change') + +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + {f : A β†’ B} {g : X β†’ Y} + (Ξ± : cartesian-hom-arrow f g) + (s : section g) + where + + section-base-change : section f + section-base-change = + section-base-change' Ξ± + ( map-section g s) + ( ( inv-htpy (is-section-map-section g s)) Β·r + ( map-codomain-cartesian-hom-arrow f g Ξ±)) +``` + ## See also - [Cocartesian morphisms of arrows](synthetic-homotopy-theory.cocartesian-morphisms-arrows.md) diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md index 06cf448eef2..fdf0b5dfdfc 100644 --- a/src/foundation/connected-types.lagda.md +++ b/src/foundation/connected-types.lagda.md @@ -35,7 +35,10 @@ open import foundation-core.truncation-levels ## Idea -A type is said to be **`k`-connected** if its `k`-truncation is contractible. +A type is said to be +{{#concept "`k`-connected" Disambiguation="type" Agda=is-connected}} if its +`k`-[truncation](foundation.truncations.md) is +[contractible](foundation-core.contractible-types.md). ## Definition diff --git a/src/foundation/disjunction.lagda.md b/src/foundation/disjunction.lagda.md index 03be3850de6..d8de7b79345 100644 --- a/src/foundation/disjunction.lagda.md +++ b/src/foundation/disjunction.lagda.md @@ -7,6 +7,7 @@ module foundation.disjunction where
Imports ```agda +open import foundation.coproduct-types open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.functoriality-coproduct-types @@ -18,11 +19,11 @@ open import foundation.type-arithmetic-coproduct-types open import foundation.universe-levels open import foundation-core.cartesian-product-types -open import foundation-core.coproduct-types open import foundation-core.decidable-propositions open import foundation-core.empty-types open import foundation-core.equivalences open import foundation-core.function-types +open import foundation-core.negation open import foundation-core.propositions open import logic.propositionally-decidable-types @@ -381,6 +382,84 @@ module _ ( right-associate-disjunction , left-associate-disjunction) ``` +### The disjunction of mutually exclusive types + +If two propositions are mutually exclusive, then their disjunction is equivalent +to the coproduct of their underlying types + +```text + P ∨ Q = P + Q. +``` + +```agda +module _ + {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) + (f : type-Prop P β†’ Β¬ (type-Prop Q)) + where + + map-compute-disjunction-mutually-exclusive : + type-disjunction-Prop P Q β†’ type-Prop P + type-Prop Q + map-compute-disjunction-mutually-exclusive = + elim-disjunction (coproduct-Prop P Q f) inl inr + + compute-disjunction-mutually-exclusive : + type-disjunction-Prop P Q ↔ type-Prop P + type-Prop Q + compute-disjunction-mutually-exclusive = + ( map-compute-disjunction-mutually-exclusive , unit-trunc-Prop) + + inv-compute-disjunction-mutually-exclusive : + type-Prop P + type-Prop Q ↔ type-disjunction-Prop P Q + inv-compute-disjunction-mutually-exclusive = + inv-iff compute-disjunction-mutually-exclusive + + equiv-compute-disjunction-mutually-exclusive : + type-disjunction-Prop P Q ≃ type-Prop P + type-Prop Q + equiv-compute-disjunction-mutually-exclusive = + equiv-iff' + ( disjunction-Prop P Q) + ( coproduct-Prop P Q f) + ( compute-disjunction-mutually-exclusive) + +module _ + {l1 l2 : Level} (A : UU l1) (B : UU l2) + (f : β•‘ A ║₋₁ β†’ Β¬ β•‘ B ║₋₁) + where + + map-compute-disjunction-type-mutually-exclusive : + disjunction-type A B β†’ β•‘ A ║₋₁ + β•‘ B ║₋₁ + map-compute-disjunction-type-mutually-exclusive = + elim-disjunction + ( coproduct-Prop (trunc-Prop A) (trunc-Prop B) f) + ( inl ∘ unit-trunc-Prop) + ( inr ∘ unit-trunc-Prop) + + map-inv-compute-disjunction-type-mutually-exclusive : + β•‘ A ║₋₁ + β•‘ B ║₋₁ β†’ disjunction-type A B + map-inv-compute-disjunction-type-mutually-exclusive (inl a) = + rec-trunc-Prop (disjunction-type-Prop A B) inl-disjunction a + map-inv-compute-disjunction-type-mutually-exclusive (inr b) = + rec-trunc-Prop (disjunction-type-Prop A B) inr-disjunction b + + compute-disjunction-type-mutually-exclusive : + disjunction-type A B ↔ (β•‘ A ║₋₁ + β•‘ B ║₋₁) + compute-disjunction-type-mutually-exclusive = + ( map-compute-disjunction-type-mutually-exclusive , + map-inv-compute-disjunction-type-mutually-exclusive) + + inv-compute-disjunction-type-mutually-exclusive : + (β•‘ A ║₋₁ + β•‘ B ║₋₁) ↔ disjunction-type A B + inv-compute-disjunction-type-mutually-exclusive = + inv-iff compute-disjunction-type-mutually-exclusive + + equiv-compute-disjunction-type-mutually-exclusive : + disjunction-type A B ≃ (β•‘ A ║₋₁ + β•‘ B ║₋₁) + equiv-compute-disjunction-type-mutually-exclusive = + equiv-iff' + ( disjunction-type-Prop A B) + ( coproduct-Prop (trunc-Prop A) (trunc-Prop B) f) + ( compute-disjunction-type-mutually-exclusive) +``` + ## See also - The indexed counterpart to disjunction is diff --git a/src/foundation/finitely-truncated-types.lagda.md b/src/foundation/finitely-truncated-types.lagda.md index fa9168fb3ac..ea4480b7c28 100644 --- a/src/foundation/finitely-truncated-types.lagda.md +++ b/src/foundation/finitely-truncated-types.lagda.md @@ -105,7 +105,8 @@ module _ is-finitely-trunc-retract-of : {A : UU l1} {B : UU l2} β†’ A retract-of B β†’ is-finitely-trunc B β†’ is-finitely-trunc A - is-finitely-trunc-retract-of R = map-tot-exists (Ξ» k β†’ is-trunc-retract-of R) + is-finitely-trunc-retract-of R = + map-tot-exists (Ξ» k β†’ is-trunc-retract-of k R) ``` ### Finitely truncated types are closed under equivalences diff --git a/src/foundation/fixed-points-endofunctions.lagda.md b/src/foundation/fixed-points-endofunctions.lagda.md index 58d4618a9ec..40c2520930a 100644 --- a/src/foundation/fixed-points-endofunctions.lagda.md +++ b/src/foundation/fixed-points-endofunctions.lagda.md @@ -18,8 +18,13 @@ open import foundation-core.identity-types ## Idea Given an [endofunction](foundation-core.endomorphisms.md) `f : A β†’ A`, the type -of {{#concept "fixed points"}} is the type of elements `x : A` such that -`f x ＝ x`. +of +{{#concept "fixed points" Disambiguation="of an endofunction" Agda=fixed-point}} +is the type of elements `x : A` such that `f x ＝ x` + +```text + fixed-point f := Ξ£ (x : A), (f x ＝ x). +``` ## Definitions diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md index 2f517ddffe2..d4b15a6308a 100644 --- a/src/foundation/identity-types.lagda.md +++ b/src/foundation/identity-types.lagda.md @@ -21,6 +21,8 @@ open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.function-types open import foundation-core.homotopies +open import foundation-core.retractions +open import foundation-core.sections ```
@@ -394,3 +396,50 @@ module _ compute-fiber-unbased-map-out-of-identity-type x = compute-fiber-map-out-of-identity-type (f x) ``` + +### Computing the total type of identifications + +```text + (Ξ£ (x y : A), (x ＝ y)) ≃ A +``` + +```agda +module _ + {l : Level} {A : UU l} + where + + map-compute-total-Id : A β†’ Ξ£ A (Ξ» x β†’ Ξ£ A (Ξ» y β†’ x ＝ y)) + map-compute-total-Id x = (x , x , refl) + + map-inv-compute-total-Id : Ξ£ A (Ξ» x β†’ Ξ£ A (Ξ» y β†’ x ＝ y)) β†’ A + map-inv-compute-total-Id = pr1 + + is-section-map-inv-compute-total-Id : + is-section map-compute-total-Id map-inv-compute-total-Id + is-section-map-inv-compute-total-Id (x , .x , refl) = refl + + is-retraction-map-inv-compute-total-Id : + is-retraction map-compute-total-Id map-inv-compute-total-Id + is-retraction-map-inv-compute-total-Id = refl-htpy + + is-equiv-map-compute-total-Id : is-equiv map-compute-total-Id + is-equiv-map-compute-total-Id = + is-equiv-is-invertible + ( map-inv-compute-total-Id) + ( is-section-map-inv-compute-total-Id) + ( is-retraction-map-inv-compute-total-Id) + + compute-total-Id : A ≃ Ξ£ A (Ξ» x β†’ Ξ£ A (Ξ» y β†’ x ＝ y)) + compute-total-Id = (map-compute-total-Id , is-equiv-map-compute-total-Id) + + is-equiv-map-inv-compute-total-Id : is-equiv map-inv-compute-total-Id + is-equiv-map-inv-compute-total-Id = + is-equiv-is-invertible + ( map-compute-total-Id) + ( is-retraction-map-inv-compute-total-Id) + ( is-section-map-inv-compute-total-Id) + + inv-compute-total-Id : Ξ£ A (Ξ» x β†’ Ξ£ A (Ξ» y β†’ x ＝ y)) ≃ A + inv-compute-total-Id = + ( map-inv-compute-total-Id , is-equiv-map-inv-compute-total-Id) +``` diff --git a/src/foundation/mere-path-cosplit-maps.lagda.md b/src/foundation/mere-path-cosplit-maps.lagda.md index 94523eeebcc..6190abc528b 100644 --- a/src/foundation/mere-path-cosplit-maps.lagda.md +++ b/src/foundation/mere-path-cosplit-maps.lagda.md @@ -132,7 +132,7 @@ is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain neg-two-𝕋 {A} {B} {f} is-trunc-B = rec-trunc-Prop ( is-trunc-Prop neg-two-𝕋 A) - ( Ξ» r β†’ is-trunc-retract-of (f , r) is-trunc-B) + ( Ξ» r β†’ is-trunc-retract-of neg-two-𝕋 (f , r) is-trunc-B) is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain (succ-𝕋 k) {A} {B} {f} is-trunc-B is-cosplit-f x y = is-trunc-domain-is-mere-path-cosplit-is-trunc-codomain k diff --git a/src/foundation/monomorphisms.lagda.md b/src/foundation/monomorphisms.lagda.md index 19085604898..82a42b94ff2 100644 --- a/src/foundation/monomorphisms.lagda.md +++ b/src/foundation/monomorphisms.lagda.md @@ -29,10 +29,11 @@ open import foundation-core.truncation-levels ## Idea -A function `f : A β†’ B` is a monomorphism if whenever we have two functions -`g h : X β†’ A` such that `f ∘ g = f ∘ h`, then in fact `g = h`. The way to state -this in Homotopy Type Theory is to say that postcomposition by `f` is an -embedding. +A function `f : A β†’ B` is a +{{#concept "monomorphism" Disambiguation="of types" Agda=is-mono}} if whenever +we have two functions `g h : X β†’ A` such that `f ∘ g = f ∘ h`, then in fact +`g = h`. The way to state this in Homotopy Type Theory is to say that +postcomposition by `f` is an embedding. ## Definition @@ -43,7 +44,7 @@ module _ where is-mono-Prop : Prop (l1 βŠ” l2 βŠ” lsuc l3) - is-mono-Prop = Ξ -Prop (UU l3) Ξ» X β†’ is-emb-Prop (postcomp X f) + is-mono-Prop = Ξ -Prop (UU l3) (Ξ» X β†’ is-emb-Prop (postcomp X f)) is-mono : UU (l1 βŠ” l2 βŠ” lsuc l3) is-mono = type-Prop is-mono-Prop diff --git a/src/foundation/path-cosplit-maps.lagda.md b/src/foundation/path-cosplit-maps.lagda.md index 854352b42a8..bdae6b15717 100644 --- a/src/foundation/path-cosplit-maps.lagda.md +++ b/src/foundation/path-cosplit-maps.lagda.md @@ -232,9 +232,9 @@ is-path-cosplit-id k = is-path-cosplit-retraction k (id , refl-htpy) is-trunc-domain-is-path-cosplit-is-trunc-codomain : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {f : A β†’ B} β†’ is-trunc k B β†’ is-path-cosplit k f β†’ is-trunc k A -is-trunc-domain-is-path-cosplit-is-trunc-codomain neg-two-𝕋 - {A} {B} {f} is-trunc-B is-cosplit-f = - is-trunc-retract-of (f , is-cosplit-f) is-trunc-B +is-trunc-domain-is-path-cosplit-is-trunc-codomain + neg-two-𝕋 {A} {B} {f} is-trunc-B is-cosplit-f = + is-trunc-retract-of neg-two-𝕋 (f , is-cosplit-f) is-trunc-B is-trunc-domain-is-path-cosplit-is-trunc-codomain (succ-𝕋 k) {A} {B} {f} is-trunc-B is-cosplit-f x y = is-trunc-domain-is-path-cosplit-is-trunc-codomain k diff --git a/src/foundation/postcomposition-pullbacks.lagda.md b/src/foundation/postcomposition-pullbacks.lagda.md index f2f61bf6b55..ff96ed92e37 100644 --- a/src/foundation/postcomposition-pullbacks.lagda.md +++ b/src/foundation/postcomposition-pullbacks.lagda.md @@ -180,3 +180,9 @@ module _ The following table lists files that are about pullbacks as a general concept. {{#include tables/pullbacks.md}} + +## See also + +- For the dual property for [pushouts](synthetic-homotopy-theory.pushouts.md), + see + [the pullback property of pushouts](synthetic-homotopy-theory.pullback-property-pushouts.md). diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index f38f2062b38..5211429cb4c 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -311,7 +311,7 @@ module _ abstract dependent-universal-property-trunc-Prop : {l : Level} {A : UU l} β†’ - dependent-universal-property-propositional-truncation + dependent-universal-property-propositional-truncation ( trunc-Prop A) ( unit-trunc-Prop) dependent-universal-property-trunc-Prop {A = A} = diff --git a/src/foundation/propositions.lagda.md b/src/foundation/propositions.lagda.md index 2f87c4f4b8c..0f444f6f204 100644 --- a/src/foundation/propositions.lagda.md +++ b/src/foundation/propositions.lagda.md @@ -49,7 +49,7 @@ module _ where is-prop-retract-of : A retract-of B β†’ is-prop B β†’ is-prop A - is-prop-retract-of = is-trunc-retract-of + is-prop-retract-of = is-trunc-retract-of neg-one-𝕋 ``` ### If a type embeds into a proposition, then it is a proposition diff --git a/src/foundation/type-arithmetic-booleans.lagda.md b/src/foundation/type-arithmetic-booleans.lagda.md index 5d7dfaad12e..9bbb29dcff9 100644 --- a/src/foundation/type-arithmetic-booleans.lagda.md +++ b/src/foundation/type-arithmetic-booleans.lagda.md @@ -9,20 +9,24 @@ module foundation.type-arithmetic-booleans where ```agda open import foundation.booleans open import foundation.dependent-pair-types +open import foundation.function-extensionality open import foundation.universe-levels +open import foundation-core.cartesian-product-types open import foundation-core.coproduct-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types +open import foundation-core.retractions +open import foundation-core.sections ``` ## Idea -We prove arithmetical laws involving the booleans +We prove arithmetical laws involving the booleans. ## Laws @@ -34,12 +38,12 @@ module _ where map-Ξ£-bool-coproduct : Ξ£ bool A β†’ A true + A false - map-Ξ£-bool-coproduct (pair true a) = inl a - map-Ξ£-bool-coproduct (pair false a) = inr a + map-Ξ£-bool-coproduct (true , a) = inl a + map-Ξ£-bool-coproduct (false , a) = inr a map-inv-Ξ£-bool-coproduct : A true + A false β†’ Ξ£ bool A - map-inv-Ξ£-bool-coproduct (inl a) = pair true a - map-inv-Ξ£-bool-coproduct (inr a) = pair false a + map-inv-Ξ£-bool-coproduct (inl a) = (true , a) + map-inv-Ξ£-bool-coproduct (inr a) = (false , a) is-section-map-inv-Ξ£-bool-coproduct : ( map-Ξ£-bool-coproduct ∘ map-inv-Ξ£-bool-coproduct) ~ id @@ -48,8 +52,8 @@ module _ is-retraction-map-inv-Ξ£-bool-coproduct : ( map-inv-Ξ£-bool-coproduct ∘ map-Ξ£-bool-coproduct) ~ id - is-retraction-map-inv-Ξ£-bool-coproduct (pair true a) = refl - is-retraction-map-inv-Ξ£-bool-coproduct (pair false a) = refl + is-retraction-map-inv-Ξ£-bool-coproduct (true , a) = refl + is-retraction-map-inv-Ξ£-bool-coproduct (false , a) = refl is-equiv-map-Ξ£-bool-coproduct : is-equiv map-Ξ£-bool-coproduct is-equiv-map-Ξ£-bool-coproduct = @@ -73,3 +77,55 @@ module _ pr1 inv-equiv-Ξ£-bool-coproduct = map-inv-Ξ£-bool-coproduct pr2 inv-equiv-Ξ£-bool-coproduct = is-equiv-map-inv-Ξ£-bool-coproduct ``` + +### Dependent products over the booleans are cartesian products + +This is also the dependent +[universal property of the booleans](foundation.universal-property-booleans.md). + +```agda +module _ + {l : Level} (A : bool β†’ UU l) + where + + map-Ξ -bool-product : ((b : bool) β†’ A b) β†’ A true Γ— A false + map-Ξ -bool-product f = (f true , f false) + + map-inv-Ξ -bool-product : A true Γ— A false β†’ ((b : bool) β†’ A b) + map-inv-Ξ -bool-product (ft , ff) = ind-bool A ft ff + + is-section-map-inv-Ξ -bool-product : + is-section map-Ξ -bool-product map-inv-Ξ -bool-product + is-section-map-inv-Ξ -bool-product _ = refl + + abstract + is-retraction-map-inv-Ξ -bool-product : + is-retraction map-Ξ -bool-product map-inv-Ξ -bool-product + is-retraction-map-inv-Ξ -bool-product f = + eq-htpy + ( Ξ» where + true β†’ refl + false β†’ refl) + + is-equiv-map-Ξ -bool-product : is-equiv map-Ξ -bool-product + is-equiv-map-Ξ -bool-product = + is-equiv-is-invertible + map-inv-Ξ -bool-product + is-section-map-inv-Ξ -bool-product + is-retraction-map-inv-Ξ -bool-product + + equiv-Ξ -bool-product : ((b : bool) β†’ A b) ≃ (A true Γ— A false) + pr1 equiv-Ξ -bool-product = map-Ξ -bool-product + pr2 equiv-Ξ -bool-product = is-equiv-map-Ξ -bool-product + + is-equiv-map-inv-Ξ -bool-product : is-equiv map-inv-Ξ -bool-product + is-equiv-map-inv-Ξ -bool-product = + is-equiv-is-invertible + map-Ξ -bool-product + is-retraction-map-inv-Ξ -bool-product + is-section-map-inv-Ξ -bool-product + + inv-equiv-Ξ -bool-product : (A true Γ— A false) ≃ ((b : bool) β†’ A b) + pr1 inv-equiv-Ξ -bool-product = map-inv-Ξ -bool-product + pr2 inv-equiv-Ξ -bool-product = is-equiv-map-inv-Ξ -bool-product +``` diff --git a/src/foundation/universal-property-booleans.lagda.md b/src/foundation/universal-property-booleans.lagda.md index 06ff14fa07d..87797e46465 100644 --- a/src/foundation/universal-property-booleans.lagda.md +++ b/src/foundation/universal-property-booleans.lagda.md @@ -14,10 +14,13 @@ open import foundation.function-extensionality open import foundation.universe-levels open import foundation-core.cartesian-product-types +open import foundation-core.coproduct-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types +open import foundation-core.retractions +open import foundation-core.sections ``` @@ -36,7 +39,7 @@ map-universal-property-bool (pair x y) false = y abstract is-section-map-universal-property-bool : {l : Level} {A : UU l} β†’ - ((ev-true-false A) ∘ map-universal-property-bool) ~ id + is-section (ev-true-false A) (map-universal-property-bool) is-section-map-universal-property-bool (pair x y) = refl abstract @@ -49,14 +52,14 @@ abstract abstract is-retraction-map-universal-property-bool : {l : Level} {A : UU l} β†’ - (map-universal-property-bool ∘ (ev-true-false A)) ~ id + is-retraction (ev-true-false A) (map-universal-property-bool) is-retraction-map-universal-property-bool f = eq-htpy (is-retraction-map-universal-property-bool' f) abstract universal-property-bool : {l : Level} (A : UU l) β†’ - is-equiv (Ξ» (f : bool β†’ A) β†’ pair (f true) (f false)) + is-equiv (Ξ» (f : bool β†’ A) β†’ (f true , f false)) universal-property-bool A = is-equiv-is-invertible map-universal-property-bool @@ -76,7 +79,7 @@ triangle-ev-true A = refl-htpy aut-bool-bool : bool β†’ (bool ≃ bool) aut-bool-bool true = id-equiv -aut-bool-bool false = equiv-neg-𝟚 +aut-bool-bool false = equiv-neg-bool bool-aut-bool : (bool ≃ bool) β†’ bool @@ -97,8 +100,8 @@ eq-true : eq-true true p = refl eq-true false p = ind-empty (p refl) -Eq-𝟚-eq : (x y : bool) β†’ x ＝ y β†’ Eq-𝟚 x y -Eq-𝟚-eq x .x refl = reflexive-Eq-𝟚 x +Eq-eq-bool : (x y : bool) β†’ x ＝ y β†’ Eq-bool x y +Eq-eq-bool x .x refl = reflexive-Eq-bool x eq-false-equiv' : (e : bool ≃ bool) β†’ map-equiv e true ＝ true β†’ @@ -106,7 +109,7 @@ eq-false-equiv' : eq-false-equiv' e p (inl q) = q eq-false-equiv' e p (inr x) = ind-empty - ( Eq-𝟚-eq true false + ( Eq-eq-bool true false ( ap pr1 ( eq-is-contr' ( is-contr-map-is-equiv (is-equiv-map-equiv e) true) @@ -114,3 +117,15 @@ eq-false-equiv' e p (inr x) = ( pair false (eq-true (map-equiv e false) x))))) -} ``` + +### The canonical projection from a coproduct to the booleans + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + projection-bool-coproduct : A + B β†’ bool + projection-bool-coproduct (inl _) = true + projection-bool-coproduct (inr _) = false +``` diff --git a/src/foundation/universal-property-unit-type.lagda.md b/src/foundation/universal-property-unit-type.lagda.md index ca15e0b392c..aaba4ce717a 100644 --- a/src/foundation/universal-property-unit-type.lagda.md +++ b/src/foundation/universal-property-unit-type.lagda.md @@ -123,3 +123,15 @@ abstract ( universal-property-unit-is-equiv-point x is-equiv-point Y) ( refl-htpy) ``` + +### The unit type is terminal + +```agda +module _ + {l : Level} {X : UU l} + where + + is-equiv-terminal-map-Ξ -unit : is-equiv (terminal-map (X β†’ unit)) + is-equiv-terminal-map-Ξ -unit = + is-equiv-is-invertible (const X) refl-htpy refl-htpy +``` diff --git a/src/group-theory/torsion-free-groups.lagda.md b/src/group-theory/torsion-free-groups.lagda.md index d7e4ed61703..ea73474233e 100644 --- a/src/group-theory/torsion-free-groups.lagda.md +++ b/src/group-theory/torsion-free-groups.lagda.md @@ -157,7 +157,10 @@ module _ is-torsion-free-Group G β†’ has-unique-torsion-element-Group G has-unique-torsion-element-is-torsion-free-Group H = fundamental-theorem-id' - ( Ξ» where x refl β†’ is-torsion-element-unit-Group G) + ( ind-Id + ( unit-Group G) + ( Ξ» y _ β†’ is-torsion-element-Group G y) + ( is-torsion-element-unit-Group G)) ( Ξ» x β†’ is-equiv-has-converse-is-prop ( is-set-type-Group G (unit-Group G) x) diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index c86b5780762..84d60f2fad7 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -9,6 +9,7 @@ open import order-theory.accessible-elements-relations public open import order-theory.bottom-elements-large-posets public open import order-theory.bottom-elements-posets public open import order-theory.bottom-elements-preorders public +open import order-theory.bounded-total-orders public open import order-theory.chains-posets public open import order-theory.chains-preorders public open import order-theory.closed-interval-preserving-maps-posets public @@ -103,6 +104,7 @@ open import order-theory.maximal-chains-preorders public open import order-theory.meet-semilattices public open import order-theory.meet-suplattices public open import order-theory.meets-finite-families-meet-semilattices public +open import order-theory.nontrivial-bounded-total-orders public open import order-theory.nuclei-large-locales public open import order-theory.opposite-large-posets public open import order-theory.opposite-large-preorders public diff --git a/src/order-theory/bounded-total-orders.lagda.md b/src/order-theory/bounded-total-orders.lagda.md new file mode 100644 index 00000000000..cda254fc6bf --- /dev/null +++ b/src/order-theory/bounded-total-orders.lagda.md @@ -0,0 +1,127 @@ +# Bounded total orders + +```agda +module order-theory.bounded-total-orders where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.propositions +open import foundation.universe-levels + +open import order-theory.bottom-elements-posets +open import order-theory.posets +open import order-theory.top-elements-posets +open import order-theory.total-orders +``` + +
+ +## Idea + +A {{#concept "bounded total order" Agda=Bounded-Total-Order}} is a +[total order](order-theory.total-orders.md) [equipped](foundation.structure.md) +with a [top](order-theory.top-elements-posets.md) and +[bottom](order-theory.bottom-elements-posets.md) element. + +## Definitions + +### The predicate of being a bounded total order + +```agda +module _ + {l1 l2 : Level} (L : Total-Order l1 l2) + where + + is-bounded-Total-Order : UU (l1 βŠ” l2) + is-bounded-Total-Order = + has-top-element-Poset (poset-Total-Order L) Γ— + has-bottom-element-Poset (poset-Total-Order L) +``` + +### Bounded total orders + +```agda +Bounded-Total-Order : (l1 l2 : Level) β†’ UU (lsuc l1 βŠ” lsuc l2) +Bounded-Total-Order l1 l2 = + Ξ£ (Total-Order l1 l2) is-bounded-Total-Order + +module _ + {l1 l2 : Level} (L : Bounded-Total-Order l1 l2) + where + + total-order-Bounded-Total-Order : Total-Order l1 l2 + total-order-Bounded-Total-Order = pr1 L + + poset-Bounded-Total-Order : Poset l1 l2 + poset-Bounded-Total-Order = + poset-Total-Order total-order-Bounded-Total-Order + + type-Bounded-Total-Order : UU l1 + type-Bounded-Total-Order = + type-Total-Order total-order-Bounded-Total-Order + + leq-prop-Bounded-Total-Order : + (x y : type-Bounded-Total-Order) β†’ Prop l2 + leq-prop-Bounded-Total-Order = + leq-prop-Poset poset-Bounded-Total-Order + + leq-Bounded-Total-Order : + (x y : type-Bounded-Total-Order) β†’ UU l2 + leq-Bounded-Total-Order = + leq-Poset poset-Bounded-Total-Order + + is-prop-leq-Bounded-Total-Order : + (x y : type-Bounded-Total-Order) β†’ is-prop (leq-Bounded-Total-Order x y) + is-prop-leq-Bounded-Total-Order = + is-prop-leq-Poset poset-Bounded-Total-Order + + refl-leq-Bounded-Total-Order : + is-reflexive leq-Bounded-Total-Order + refl-leq-Bounded-Total-Order = + refl-leq-Poset poset-Bounded-Total-Order + + transitive-leq-Bounded-Total-Order : + is-transitive leq-Bounded-Total-Order + transitive-leq-Bounded-Total-Order = + transitive-leq-Poset poset-Bounded-Total-Order + + antisymmetric-leq-Bounded-Total-Order : + is-antisymmetric leq-Bounded-Total-Order + antisymmetric-leq-Bounded-Total-Order = + antisymmetric-leq-Poset poset-Bounded-Total-Order + + has-top-element-Bounded-Total-Order : + has-top-element-Poset poset-Bounded-Total-Order + has-top-element-Bounded-Total-Order = + pr1 (pr2 L) + + top-Bounded-Total-Order : + type-Bounded-Total-Order + top-Bounded-Total-Order = + pr1 has-top-element-Bounded-Total-Order + + is-top-element-top-Bounded-Total-Order : + is-top-element-Poset poset-Bounded-Total-Order top-Bounded-Total-Order + is-top-element-top-Bounded-Total-Order = + pr2 has-top-element-Bounded-Total-Order + + has-bottom-element-Bounded-Total-Order : + has-bottom-element-Poset poset-Bounded-Total-Order + has-bottom-element-Bounded-Total-Order = + pr2 (pr2 L) + + bottom-Bounded-Total-Order : + type-Bounded-Total-Order + bottom-Bounded-Total-Order = + pr1 has-bottom-element-Bounded-Total-Order + + is-bottom-element-bottom-Bounded-Total-Order : + is-bottom-element-Poset poset-Bounded-Total-Order bottom-Bounded-Total-Order + is-bottom-element-bottom-Bounded-Total-Order = + pr2 has-bottom-element-Bounded-Total-Order +``` diff --git a/src/order-theory/nontrivial-bounded-total-orders.lagda.md b/src/order-theory/nontrivial-bounded-total-orders.lagda.md new file mode 100644 index 00000000000..b0b35a17748 --- /dev/null +++ b/src/order-theory/nontrivial-bounded-total-orders.lagda.md @@ -0,0 +1,149 @@ +# Nontrivial bounded total orders + +```agda +module order-theory.nontrivial-bounded-total-orders where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.negated-equality +open import foundation.propositions +open import foundation.universe-levels + +open import order-theory.bottom-elements-posets +open import order-theory.bounded-total-orders +open import order-theory.posets +open import order-theory.top-elements-posets +open import order-theory.total-orders +``` + +
+ +## Idea + +A +{{#concept "nontrivial bounded total order" Agda=Nontrivial-Bounded-Total-Order}} +is a [bounded total order](order-theory.bounded-total-orders.md) whose +[top](order-theory.top-elements-posets.md) and +[bottom](order-theory.bottom-elements-posets.md) elements are +[distinct](foundation.negated-equality.md). + +## Definitions + +### The predicate of being a nontrivial bounded total order + +```agda +module _ + {l1 l2 : Level} (L : Bounded-Total-Order l1 l2) + where + + is-nontrivial-Bounded-Total-Order : UU l1 + is-nontrivial-Bounded-Total-Order = + bottom-Bounded-Total-Order L β‰  top-Bounded-Total-Order L +``` + +### Nontrivial bounded total orders + +```agda +Nontrivial-Bounded-Total-Order : (l1 l2 : Level) β†’ UU (lsuc l1 βŠ” lsuc l2) +Nontrivial-Bounded-Total-Order l1 l2 = + Ξ£ (Bounded-Total-Order l1 l2) is-nontrivial-Bounded-Total-Order + +module _ + {l1 l2 : Level} (L : Nontrivial-Bounded-Total-Order l1 l2) + where + + bounded-total-order-Nontrivial-Bounded-Total-Order : Bounded-Total-Order l1 l2 + bounded-total-order-Nontrivial-Bounded-Total-Order = pr1 L + + total-order-Nontrivial-Bounded-Total-Order : Total-Order l1 l2 + total-order-Nontrivial-Bounded-Total-Order = + total-order-Bounded-Total-Order + bounded-total-order-Nontrivial-Bounded-Total-Order + + poset-Nontrivial-Bounded-Total-Order : Poset l1 l2 + poset-Nontrivial-Bounded-Total-Order = + poset-Total-Order total-order-Nontrivial-Bounded-Total-Order + + type-Nontrivial-Bounded-Total-Order : UU l1 + type-Nontrivial-Bounded-Total-Order = + type-Total-Order total-order-Nontrivial-Bounded-Total-Order + + leq-prop-Nontrivial-Bounded-Total-Order : + (x y : type-Nontrivial-Bounded-Total-Order) β†’ Prop l2 + leq-prop-Nontrivial-Bounded-Total-Order = + leq-prop-Poset poset-Nontrivial-Bounded-Total-Order + + leq-Nontrivial-Bounded-Total-Order : + (x y : type-Nontrivial-Bounded-Total-Order) β†’ UU l2 + leq-Nontrivial-Bounded-Total-Order = + leq-Poset poset-Nontrivial-Bounded-Total-Order + + is-prop-leq-Nontrivial-Bounded-Total-Order : + (x y : type-Nontrivial-Bounded-Total-Order) β†’ + is-prop (leq-Nontrivial-Bounded-Total-Order x y) + is-prop-leq-Nontrivial-Bounded-Total-Order = + is-prop-leq-Poset poset-Nontrivial-Bounded-Total-Order + + refl-leq-Nontrivial-Bounded-Total-Order : + is-reflexive leq-Nontrivial-Bounded-Total-Order + refl-leq-Nontrivial-Bounded-Total-Order = + refl-leq-Poset poset-Nontrivial-Bounded-Total-Order + + transitive-leq-Nontrivial-Bounded-Total-Order : + is-transitive leq-Nontrivial-Bounded-Total-Order + transitive-leq-Nontrivial-Bounded-Total-Order = + transitive-leq-Poset poset-Nontrivial-Bounded-Total-Order + + antisymmetric-leq-Nontrivial-Bounded-Total-Order : + is-antisymmetric leq-Nontrivial-Bounded-Total-Order + antisymmetric-leq-Nontrivial-Bounded-Total-Order = + antisymmetric-leq-Poset poset-Nontrivial-Bounded-Total-Order + + has-top-element-Nontrivial-Bounded-Total-Order : + has-top-element-Poset poset-Nontrivial-Bounded-Total-Order + has-top-element-Nontrivial-Bounded-Total-Order = + has-top-element-Bounded-Total-Order + bounded-total-order-Nontrivial-Bounded-Total-Order + + top-Nontrivial-Bounded-Total-Order : + type-Nontrivial-Bounded-Total-Order + top-Nontrivial-Bounded-Total-Order = + top-Bounded-Total-Order bounded-total-order-Nontrivial-Bounded-Total-Order + + is-top-element-top-Nontrivial-Bounded-Total-Order : + is-top-element-Poset + poset-Nontrivial-Bounded-Total-Order + top-Nontrivial-Bounded-Total-Order + is-top-element-top-Nontrivial-Bounded-Total-Order = + is-top-element-top-Bounded-Total-Order + bounded-total-order-Nontrivial-Bounded-Total-Order + + has-bottom-element-Nontrivial-Bounded-Total-Order : + has-bottom-element-Poset poset-Nontrivial-Bounded-Total-Order + has-bottom-element-Nontrivial-Bounded-Total-Order = + has-bottom-element-Bounded-Total-Order + bounded-total-order-Nontrivial-Bounded-Total-Order + + bottom-Nontrivial-Bounded-Total-Order : + type-Nontrivial-Bounded-Total-Order + bottom-Nontrivial-Bounded-Total-Order = + bottom-Bounded-Total-Order + bounded-total-order-Nontrivial-Bounded-Total-Order + + is-bottom-element-bottom-Nontrivial-Bounded-Total-Order : + is-bottom-element-Poset + poset-Nontrivial-Bounded-Total-Order + bottom-Nontrivial-Bounded-Total-Order + is-bottom-element-bottom-Nontrivial-Bounded-Total-Order = + is-bottom-element-bottom-Bounded-Total-Order + bounded-total-order-Nontrivial-Bounded-Total-Order + + is-nontrivial-Nontrivial-Bounded-Total-Order : + bottom-Nontrivial-Bounded-Total-Order β‰  top-Nontrivial-Bounded-Total-Order + is-nontrivial-Nontrivial-Bounded-Total-Order = pr2 L +``` diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index e2a8bf72864..7c838a54af0 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -14,6 +14,7 @@ open import orthogonal-factorization-systems.cd-structures public open import orthogonal-factorization-systems.cellular-maps public open import orthogonal-factorization-systems.closed-modalities public open import orthogonal-factorization-systems.continuation-modalities public +open import orthogonal-factorization-systems.coproducts-null-types public open import orthogonal-factorization-systems.double-lifts-families-of-elements public open import orthogonal-factorization-systems.double-negation-sheaves public open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements public diff --git a/src/orthogonal-factorization-systems/coproducts-null-types.lagda.md b/src/orthogonal-factorization-systems/coproducts-null-types.lagda.md new file mode 100644 index 00000000000..4a01e1b546e --- /dev/null +++ b/src/orthogonal-factorization-systems/coproducts-null-types.lagda.md @@ -0,0 +1,116 @@ +# Coproducts of null types + +```agda +module orthogonal-factorization-systems.coproducts-null-types where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.booleans +open import foundation.cartesian-product-types +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.diagonal-maps-of-types +open import foundation.equivalences +open import foundation.equivalences-arrows +open import foundation.fibers-of-maps +open import foundation.function-extensionality +open import foundation.functoriality-cartesian-product-types +open import foundation.functoriality-coproduct-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.inhabited-types +open import foundation.logical-equivalences +open import foundation.postcomposition-dependent-functions +open import foundation.postcomposition-functions +open import foundation.precomposition-dependent-functions +open import foundation.precomposition-functions +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.raising-universe-levels +open import foundation.retracts-of-maps +open import foundation.retracts-of-types +open import foundation.type-arithmetic-booleans +open import foundation.type-arithmetic-unit-type +open import foundation.unit-type +open import foundation.universal-property-booleans +open import foundation.universal-property-equivalences +open import foundation.universal-property-family-of-fibers-of-maps +open import foundation.universal-property-unit-type +open import foundation.universe-levels + +open import orthogonal-factorization-systems.maps-local-at-maps +open import orthogonal-factorization-systems.null-maps +open import orthogonal-factorization-systems.null-types +open import orthogonal-factorization-systems.orthogonal-maps +open import orthogonal-factorization-systems.types-local-at-maps +``` + +
+ +## Idea + +The universe of `Y`-[null](orthogonal-factorization-systems.null-types.md) types +are closed under [coproducts](foundation.coproduct-types.md) if and only if the +[booleans](foundation.booleans.md) are `Y`-null. + +## Properties + +### The canonical map `A + B β†’ bool` is `Y`-null if `A` and `B` are + +```agda +module _ + {l1 l2 l3 : Level} + (Y : UU l1) {A : UU l2} {B : UU l3} + (is-null-A : is-null Y A) + (is-null-B : is-null Y B) + where + + abstract + is-null-projection-bool-coproduct : + is-null-map Y (projection-bool-coproduct {A = A} {B}) + is-null-projection-bool-coproduct = + is-null-map-left-map-triangle Y + ( Ξ» where + (inl _) β†’ refl + (inr _) β†’ refl) + ( is-null-map-pr1-is-null-family Y + ( rec-bool (raise (l2 βŠ” l3) A) (raise (l2 βŠ” l3) B)) + ( Ξ» where + true β†’ + is-null-equiv-base (inv-compute-raise (l2 βŠ” l3) A) is-null-A + false β†’ + is-null-equiv-base (inv-compute-raise (l2 βŠ” l3) B) is-null-B)) + ( is-null-map-map-equiv Y + ( ( inv-equiv-Ξ£-bool-coproduct + ( rec-bool (raise (l2 βŠ” l3) A) (raise (l2 βŠ” l3) B))) ∘e + ( equiv-coproduct + ( compute-raise (l2 βŠ” l3) A) + ( compute-raise (l2 βŠ” l3) B)))) +``` + +### If the booleans are `Y`-null then coproducts of `Y`-null types are `Y`-null + +```agda +module _ + {l1 l2 l3 : Level} + (Y : UU l1) {A : UU l2} {B : UU l3} + (is-null-bool : is-null Y bool) + (is-null-A : is-null Y A) + (is-null-B : is-null Y B) + where + + is-null-coproduct-is-null-bool : is-null Y (A + B) + is-null-coproduct-is-null-bool = + is-null-is-orthogonal-terminal-maps + ( is-orthogonal-right-comp + ( terminal-map Y) + ( projection-bool-coproduct) + ( terminal-map bool) + ( is-orthogonal-terminal-maps-is-null is-null-bool) + ( is-orthogonal-terminal-map-is-null-map Y + ( projection-bool-coproduct) + ( is-null-projection-bool-coproduct Y is-null-A is-null-B))) +``` diff --git a/src/orthogonal-factorization-systems/null-maps.lagda.md b/src/orthogonal-factorization-systems/null-maps.lagda.md index af001e1fc2d..3efc55a796c 100644 --- a/src/orthogonal-factorization-systems/null-maps.lagda.md +++ b/src/orthogonal-factorization-systems/null-maps.lagda.md @@ -15,6 +15,7 @@ open import foundation.equivalences-arrows open import foundation.families-of-equivalences open import foundation.fibers-of-maps open import foundation.function-types +open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-fibers-of-maps open import foundation.homotopies open import foundation.identity-types @@ -219,7 +220,7 @@ module _ inv-equiv equiv-is-local-terminal-map-is-null-map ``` -### A map is `Y`-null if and only if the terminal projection of `Y` is orthogonal to `f` +### A map is `Y`-null if and only if it is `Y`-orthogonal ```agda module _ @@ -278,3 +279,185 @@ module _ is-orthogonal-is-orthogonal-fiber-condition-right-map (terminal-map Y) f ( is-orthogonal-fiber-condition-terminal-map-is-null-map H) ``` + +### Equivalences are null at any type + +```agda +module _ + {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} {B : UU l3} (e : A ≃ B) + where + + is-null-map-map-equiv : is-null-map Y (map-equiv e) + is-null-map-map-equiv = + is-null-map-is-orthogonal-terminal-map Y + ( map-equiv e) + ( is-orthogonal-equiv-right (terminal-map Y) e) +``` + +### Null maps are closed under homotopies + +```agda +module _ + {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} {B : UU l3} + {f g : A β†’ B} + where + + is-null-map-htpy : f ~ g β†’ is-null-map Y f β†’ is-null-map Y g + is-null-map-htpy H is-null-f = + is-null-map-is-orthogonal-terminal-map Y g + ( is-orthogonal-htpy-right (terminal-map Y) f H + ( is-orthogonal-terminal-map-is-null-map Y f is-null-f)) + + is-null-map-htpy' : g ~ f β†’ is-null-map Y f β†’ is-null-map Y g + is-null-map-htpy' H = is-null-map-htpy (inv-htpy H) +``` + +### A family is `Y`-null if and only if it is `Y`-orthogonal + +```agda +module _ + {l1 l2 l3 : Level} (Y : UU l1) {A : UU l2} {B : A β†’ UU l3} + where + + is-null-family-is-orthogonal-terminal-map : + is-orthogonal (terminal-map Y) (pr1 {B = B}) β†’ is-null-family Y B + is-null-family-is-orthogonal-terminal-map H = + is-null-family-is-null-map-pr1 Y B + ( is-null-map-is-orthogonal-terminal-map Y pr1 H) + + is-orthogonal-terminal-map-is-null-family : + is-null-family Y B β†’ is-orthogonal (terminal-map Y) (pr1 {B = B}) + is-orthogonal-terminal-map-is-null-family H = + is-orthogonal-terminal-map-is-null-map Y pr1 + ( is-null-map-pr1-is-null-family Y B H) +``` + +### The dependent sum of a type family over a `Y`-null base is `Y`-null if and only if the type family is `Y`-null + +One direction was already proven in `null-types`, however, we give a second +proof of this fact below. + +```agda +module _ + {l1 l2 l3 : Level} {Y : UU l1} {A : UU l2} {B : A β†’ UU l3} + where + + abstract + is-null-Ξ£' : is-null Y A β†’ is-null-family Y B β†’ is-null Y (Ξ£ A B) + is-null-Ξ£' is-null-A is-null-B = + is-null-is-orthogonal-terminal-maps + ( is-orthogonal-right-comp + ( terminal-map Y) + ( pr1) + ( terminal-map A) + ( is-orthogonal-terminal-maps-is-null is-null-A) + ( is-orthogonal-terminal-map-is-null-family Y is-null-B)) + + abstract + is-null-family-is-null-Ξ£ : + is-null Y A β†’ is-null Y (Ξ£ A B) β†’ is-null-family Y B + is-null-family-is-null-Ξ£ is-null-A is-null-Ξ£AB = + is-null-family-is-orthogonal-terminal-map Y + ( is-orthogonal-right-right-factor + ( terminal-map Y) + ( pr1) + ( terminal-map A) + ( is-orthogonal-terminal-maps-is-null is-null-A) + ( is-orthogonal-terminal-maps-is-null is-null-Ξ£AB)) +``` + +### Composition and right cancellation of null maps + +```agda +module _ + {l1 l2 l3 l4 : Level} + (Y : UU l1) {A : UU l2} {B : UU l3} {C : UU l4} + {f : A β†’ B} {g : B β†’ C} + where + + abstract + is-null-map-comp : + is-null-map Y g β†’ is-null-map Y f β†’ is-null-map Y (g ∘ f) + is-null-map-comp is-null-g is-null-f = + is-null-map-is-orthogonal-terminal-map Y (g ∘ f) + ( is-orthogonal-right-comp (terminal-map Y) f g + ( is-orthogonal-terminal-map-is-null-map Y g is-null-g) + ( is-orthogonal-terminal-map-is-null-map Y f is-null-f)) + + abstract + is-null-map-right-factor : + is-null-map Y g β†’ is-null-map Y (g ∘ f) β†’ is-null-map Y f + is-null-map-right-factor is-null-g is-null-gf = + is-null-map-is-orthogonal-terminal-map Y f + ( is-orthogonal-right-right-factor (terminal-map Y) f g + ( is-orthogonal-terminal-map-is-null-map Y g is-null-g) + ( is-orthogonal-terminal-map-is-null-map Y (g ∘ f) is-null-gf)) + +module _ + {l1 l2 l3 l4 : Level} + (Y : UU l1) {A : UU l2} {B : UU l3} {C : UU l4} + {f : A β†’ B} {g : B β†’ C} {h : A β†’ C} (H : h ~ g ∘ f) + where + + is-null-map-left-map-triangle : + is-null-map Y g β†’ is-null-map Y f β†’ is-null-map Y h + is-null-map-left-map-triangle is-null-g is-null-f = + is-null-map-htpy' Y H (is-null-map-comp Y is-null-g is-null-f) + + is-null-map-top-map-triangle : + is-null-map Y g β†’ is-null-map Y h β†’ is-null-map Y f + is-null-map-top-map-triangle is-null-g is-null-h = + is-null-map-right-factor Y is-null-g (is-null-map-htpy Y H is-null-h) +``` + +### Null maps are closed under dependent products + +```agda +module _ + {l1 l2 l3 l4 : Level} + (Y : UU l1) {I : UU l2} {A : I β†’ UU l3} {B : I β†’ UU l4} + {f : (i : I) β†’ A i β†’ B i} + where + + abstract + is-null-map-Ξ  : ((i : I) β†’ is-null-map Y (f i)) β†’ is-null-map Y (map-Ξ  f) + is-null-map-Ξ  is-null-f = + is-null-map-is-orthogonal-terminal-map Y (map-Ξ  f) + ( is-orthogonal-right-Ξ  (terminal-map Y) f + ( Ξ» i β†’ is-orthogonal-terminal-map-is-null-map Y (f i) (is-null-f i))) +``` + +### Null maps are closed under exponentiation + +```agda +module _ + {l1 l2 l3 l4 : Level} + (Y : UU l1) (I : UU l2) {A : UU l3} {B : UU l4} {f : A β†’ B} + where + + abstract + is-null-map-postcomp : is-null-map Y f β†’ is-null-map Y (postcomp I f) + is-null-map-postcomp is-null-f = + is-null-map-is-orthogonal-terminal-map Y (postcomp I f) + ( is-orthogonal-right-postcomp I (terminal-map Y) f + ( is-orthogonal-terminal-map-is-null-map Y f is-null-f)) +``` + +### Null maps are closed under cartesian products + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + (Y : UU l1) {A : UU l2} {B : UU l3} {C : UU l4} {D : UU l5} + {f : A β†’ B} {g : C β†’ D} + where + + abstract + is-null-map-product : + is-null-map Y f β†’ is-null-map Y g β†’ is-null-map Y (map-product f g) + is-null-map-product is-null-f is-null-g = + is-null-map-is-orthogonal-terminal-map Y (map-product f g) + ( is-orthogonal-right-product (terminal-map Y) f g + ( is-orthogonal-terminal-map-is-null-map Y f is-null-f) + ( is-orthogonal-terminal-map-is-null-map Y g is-null-g)) +``` diff --git a/src/orthogonal-factorization-systems/null-types.lagda.md b/src/orthogonal-factorization-systems/null-types.lagda.md index d47b2a74fd6..819c585dc94 100644 --- a/src/orthogonal-factorization-systems/null-types.lagda.md +++ b/src/orthogonal-factorization-systems/null-types.lagda.md @@ -8,6 +8,7 @@ module orthogonal-factorization-systems.null-types where ```agda open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.diagonal-maps-of-types @@ -16,13 +17,17 @@ open import foundation.equivalences-arrows open import foundation.fibers-of-maps open import foundation.function-extensionality open import foundation.function-types +open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types +open import foundation.inhabited-types open import foundation.logical-equivalences +open import foundation.postcomposition-dependent-functions open import foundation.postcomposition-functions open import foundation.precomposition-dependent-functions open import foundation.precomposition-functions +open import foundation.propositional-truncations open import foundation.propositions open import foundation.retractions open import foundation.retracts-of-maps @@ -235,16 +240,6 @@ module _ is-local-is-null-fiber A = is-local-dependent-type-is-null-fiber (Ξ» _ β†’ A) ``` -### Contractible types are null at all types - -```agda -is-null-is-contr : - {l1 l2 : Level} {A : UU l1} (B : UU l2) β†’ is-contr A β†’ is-null B A -is-null-is-contr {A = A} B is-contr-A = - is-null-is-local-terminal-map B A - ( is-local-is-contr (terminal-map B) A is-contr-A) -``` - ### Null types are closed under dependent sums This is Theorem 2.19 in {{#cite RSS20}}. @@ -270,3 +265,119 @@ module _ ≃ (Y β†’ Ξ£ A B) by inv-distributive-Ξ -Ξ£) ``` + +### Contractible types are null at all types + +```agda +is-null-is-contr : + {l1 l2 : Level} {A : UU l1} (B : UU l2) β†’ is-contr A β†’ is-null B A +is-null-is-contr {A = A} B is-contr-A = + is-null-is-local-terminal-map B A + ( is-local-is-contr (terminal-map B) A is-contr-A) +``` + +### Propositions are null at inhabited types + +```agda +module _ + {l1 l2 : Level} {Y : UU l1} + where + + is-null-is-prop-is-inhabited' : + {P : UU l2} β†’ Y β†’ is-prop P β†’ is-null Y P + is-null-is-prop-is-inhabited' {P} y is-prop-P = + is-equiv-has-converse-is-prop + ( is-prop-P) + ( is-prop-function-type is-prop-P) + ( Ξ» f β†’ f y) + + is-null-is-prop-is-inhabited : + {P : UU l2} β†’ is-inhabited Y β†’ is-prop P β†’ is-null Y P + is-null-is-prop-is-inhabited {P} is-inhabited-Y is-prop-P = + is-equiv-has-converse-is-prop + ( is-prop-P) + ( is-prop-function-type is-prop-P) + ( Ξ» f β†’ rec-trunc-Prop (P , is-prop-P) f is-inhabited-Y) + + is-null-prop-is-inhabited : + is-inhabited Y β†’ (P : Prop l2) β†’ is-null Y (type-Prop P) + is-null-prop-is-inhabited is-inhabited-Y P = + is-null-is-prop-is-inhabited is-inhabited-Y (is-prop-type-Prop P) +``` + +### Null types are closed under dependent products + +```agda +module _ + {l1 l2 l3 : Level} {Y : UU l1} {I : UU l2} {B : I β†’ UU l3} + where + + abstract + is-null-Ξ  : ((i : I) β†’ is-null Y (B i)) β†’ is-null Y ((i : I) β†’ B i) + is-null-Ξ  is-null-B = + is-null-is-orthogonal-terminal-maps + ( is-orthogonal-right-comp + ( terminal-map Y) + ( postcomp-Ξ  I (Ξ» {i : I} β†’ terminal-map (B i))) + ( terminal-map (I β†’ unit)) + ( is-orthogonal-is-equiv-right + ( terminal-map Y) + ( terminal-map (I β†’ unit)) + ( is-equiv-terminal-map-Ξ -unit)) + ( is-orthogonal-right-Ξ  + ( terminal-map Y) + ( Ξ» i β†’ terminal-map (B i)) + ( Ξ» i β†’ (is-orthogonal-terminal-maps-is-null (is-null-B i))))) +``` + +### Null types are closed under exponentiation + +```agda +module _ + {l1 l2 l3 : Level} {Y : UU l1} {I : UU l2} {B : UU l3} + where + + is-null-function-type : is-null Y B β†’ is-null Y (I β†’ B) + is-null-function-type is-null-B = is-null-Ξ  (Ξ» _ β†’ is-null-B) +``` + +### Null types are closed under cartesian products + +```agda +module _ + {l1 l2 l3 : Level} {Y : UU l1} {A : UU l2} {B : UU l3} + where + + abstract + is-null-product : is-null Y A β†’ is-null Y B β†’ is-null Y (A Γ— B) + is-null-product is-null-A is-null-B = + is-null-is-orthogonal-terminal-maps + ( is-orthogonal-right-comp + ( terminal-map Y) + ( map-product (terminal-map A) (terminal-map B)) + ( terminal-map (unit Γ— unit)) + ( is-orthogonal-is-equiv-right + ( terminal-map Y) + ( terminal-map (unit Γ— unit)) + ( is-equiv-map-right-unit-law-product)) + ( is-orthogonal-right-product + ( terminal-map Y) + ( terminal-map A) + ( terminal-map B) + ( is-orthogonal-terminal-maps-is-null is-null-A) + ( is-orthogonal-terminal-maps-is-null is-null-B))) +``` + +### Null types are closed under identity types + +> This remains to be formalized. + +## See also + +- We show that null types are closed under dependent sums in + [`null-maps`](orthogonal-factorization-systems.null-maps.md). +- In + [`coproducts-null-types`](orthogonal-factorization-systems.coproducts-null-types.md) + we show that `Y`-null types are closed under + [coproducts](foundation.coproduct-types.md) if and only if the + [booleans](foundation.booleans.md) are `Y`-null. diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md index beee150e80a..8c57e9c6dd5 100644 --- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md +++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md @@ -468,6 +468,19 @@ module _ is-orthogonal-htpy-right = is-orthogonal-htpy refl-htpy ``` +### Orthogonality is preserved under equivalences of maps + +Given equivalences of arrows `f' ≃ f` and `g' ≃ g`, then `f βŠ₯ g` if and only if +`f' βŠ₯ g'`. + +> This remains to be formalized. + +### Orthogonality is preserved under retracts of maps + +Given retracts of maps `f' β†’ f` and `g β†’ g'`, then `f βŠ₯ g` implies `f' βŠ₯ g'`. + +> This remains to be formalized. + ### Equivalences are orthogonal to every map ```agda @@ -1335,7 +1348,42 @@ module _ ( is-orthogonal-pullback-condition-is-orthogonal f g F)) ``` -### A type is `f`-local if and only if its terminal map is `f`-orthogonal +### Right orthogonality is preserved under pullback-homs with arbitrary maps + +Given an `f`-orthogonal map `g` and an arbitrary map `k`, then the pullback-hom +`⟨k , g⟩` is also `f`-orthogonal. This is Corollary 3.1.13 of {{#cite BW23}}. + +> This remains to be formalized. + +### Left orthogonality is preserved under pushout-products with arbitrary maps + +Given maps `f βŠ₯ g` and an arbitrary map `k`, then `(f β–‘ k) βŠ₯ g`. + +**Proof.** Follows from the previous result using the adjoint relation to the +pullback-hom: + +```text + ⟨f β–‘ k , g⟩ ~ ⟨f , ⟨k , g⟩⟩. +``` + +> This remains to be formalized. + +### Right orthogonality is preserved under sequential limits + +Given an [inverse sequential diagram](foundation.inverse-sequential-diagrams.md) +of `f`-orthogonal maps + +```text + g₃ gβ‚‚ g₁ gβ‚€ + β‹― ---> X₃ ---> Xβ‚‚ ---> X₁ ---> Xβ‚€. +``` + +then the [sequential limit](foundation.sequential-limits.md) `g∞ : X∞ β†’ Xβ‚€` is +also `f`-orthogonal. This is Proposition 3.1.14 of {{#cite BW23}}. + +> This remains to be formalized. + +### A type is `f`-local if and only if the terminal map is `f`-orthogonal **Proof (forward direction):** If the terminal map is right orthogonal to `f`, that means we have a pullback square diff --git a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md index 1ebbc9e3de7..9011ca94660 100644 --- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -24,10 +24,12 @@ open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types +open import foundation.inhabited-types open import foundation.logical-equivalences open import foundation.postcomposition-functions open import foundation.precomposition-dependent-functions open import foundation.precomposition-functions +open import foundation.propositional-truncations open import foundation.propositions open import foundation.retractions open import foundation.retracts-of-maps @@ -379,7 +381,29 @@ module _ is-local-dependent-type-is-prop (Ξ» _ β†’ A) (Ξ» _ β†’ is-prop-A) ``` -### All types are local at equivalences +### Propositions are `f`-local if the domain of `f` is inhabited + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X β†’ Y) + where + + is-local-has-element-domain-is-prop : + {l : Level} (A : UU l) β†’ + is-prop A β†’ X β†’ is-local f A + is-local-has-element-domain-is-prop A is-prop-A x = + is-local-is-prop f A is-prop-A (Ξ» h y β†’ h x) + + is-local-is-inhabited-domain-is-prop : + {l : Level} (A : UU l) β†’ + is-prop A β†’ is-inhabited X β†’ is-local f A + is-local-is-inhabited-domain-is-prop A is-prop-A = + rec-trunc-Prop + ( is-local-Prop f A) + ( is-local-has-element-domain-is-prop A is-prop-A) +``` + +### All type families are local at equivalences ```agda module _ @@ -422,7 +446,7 @@ module _ ```agda is-contr-is-local : - {l : Level} (A : UU l) β†’ is-local (Ξ» (_ : empty) β†’ star) A β†’ is-contr A + {l : Level} (A : UU l) β†’ is-local (terminal-map empty) A β†’ is-contr A is-contr-is-local A is-local-A = is-contr-equiv ( empty β†’ A) diff --git a/src/reflection/erasing-equality.lagda.md b/src/reflection/erasing-equality.lagda.md index 47ec4698a23..e12c880f1d5 100644 --- a/src/reflection/erasing-equality.lagda.md +++ b/src/reflection/erasing-equality.lagda.md @@ -18,16 +18,16 @@ open import foundation-core.identity-types Agda's builtin primitive `primEraseEquality` is a special construct on [identifications](foundation-core.identity-types.md) that for every -identification `x ＝ y` gives an identification `x ＝ y` with the following +identification `x ＝ y` gives another identification `x ＝ y` with the following reduction behavior: -- If the two end points `x ＝ y` normalize to the same term, `primEraseEquality` - reduces to `refl`. +- If the two end points of `p : x ＝ y` normalize to the same term, then + `primEraseEquality p` reduces to `refl`. For example, `primEraseEquality` applied to the loop of the [circle](synthetic-homotopy-theory.circle.md) will compute to `refl`, while -`primEraseEquality` applied to the nontrivial identification in the -[interval](synthetic-homotopy-theory.interval-type.md) will not reduce. +`primEraseEquality` applied to the generating identification in the +[interval](synthetic-homotopy-theory.interval.md) will not reduce. This primitive is useful for [rewrite rules](reflection.rewriting.md), as it ensures that the identification used in defining the rewrite rule also computes diff --git a/src/reflection/type-checking-monad.lagda.md b/src/reflection/type-checking-monad.lagda.md index 50a1e0f7bc8..5e2fc99bbf1 100644 --- a/src/reflection/type-checking-monad.lagda.md +++ b/src/reflection/type-checking-monad.lagda.md @@ -292,8 +292,8 @@ private ### Trying a path -The following example tries to solve a goal by using path `p` or `inv p`. This -example was adapted from +The following example tries to solve a goal by using the path `p` or `inv p`. +This example was adapted from ```agda private diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md index 2839f2a8162..d1a7826cc1c 100644 --- a/src/synthetic-homotopy-theory.lagda.md +++ b/src/synthetic-homotopy-theory.lagda.md @@ -83,7 +83,7 @@ open import synthetic-homotopy-theory.induction-principle-pushouts public open import synthetic-homotopy-theory.infinite-complex-projective-space public open import synthetic-homotopy-theory.infinite-cyclic-types public open import synthetic-homotopy-theory.infinite-real-projective-space public -open import synthetic-homotopy-theory.interval-type public +open import synthetic-homotopy-theory.interval public open import synthetic-homotopy-theory.iterated-loop-spaces public open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types public open import synthetic-homotopy-theory.join-powers-of-types public diff --git a/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md b/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md index 265ce6a2c99..930984b3d5f 100644 --- a/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md @@ -23,11 +23,12 @@ open import synthetic-homotopy-theory.universal-property-pushouts ## Idea -The **dependent pushout-product** is a generalization of the +The _dependent pushout-product_ is a generalization of the [pushout-product](synthetic-homotopy-theory.pushout-products.md). Consider a map -`f : A β†’ B` and a family of maps `g : (x : X) β†’ B x β†’ Y x`. The **dependent -pushout-product** is the [cogap map](synthetic-homotopy-theory.pushouts.md) of -the [commuting square](foundation-core.commuting-squares-of-maps.md) +`f : A β†’ B` and a family of maps `g : (x : X) β†’ B x β†’ Y x`. The +{{#concept "dependent pushout-product" Disambiguation="of maps of types" Agda=dependent-pushout-product}} +is the [cogap map](synthetic-homotopy-theory.pushouts.md) of the +[commuting square](foundation-core.commuting-squares-of-maps.md) ```text Ξ£ f id diff --git a/src/synthetic-homotopy-theory/descent-circle.lagda.md b/src/synthetic-homotopy-theory/descent-circle.lagda.md index 8adc5c7904e..edb7ac84a1c 100644 --- a/src/synthetic-homotopy-theory/descent-circle.lagda.md +++ b/src/synthetic-homotopy-theory/descent-circle.lagda.md @@ -51,8 +51,7 @@ way made precise in further sections of this file. The pair `(X, e)` is called **descent data** for the circle. ```agda -descent-data-circle : - ( l1 : Level) β†’ UU (lsuc l1) +descent-data-circle : (l : Level) β†’ UU (lsuc l) descent-data-circle = Type-With-Automorphism module _ diff --git a/src/synthetic-homotopy-theory/interval-type.lagda.md b/src/synthetic-homotopy-theory/interval.lagda.md similarity index 99% rename from src/synthetic-homotopy-theory/interval-type.lagda.md rename to src/synthetic-homotopy-theory/interval.lagda.md index 680dcc01264..a4b93329344 100644 --- a/src/synthetic-homotopy-theory/interval-type.lagda.md +++ b/src/synthetic-homotopy-theory/interval.lagda.md @@ -1,7 +1,7 @@ # The interval ```agda -module synthetic-homotopy-theory.interval-type where +module synthetic-homotopy-theory.interval where ```
Imports diff --git a/src/synthetic-homotopy-theory/joins-of-types.lagda.md b/src/synthetic-homotopy-theory/joins-of-types.lagda.md index 8b6ea381724..ddfb156c03f 100644 --- a/src/synthetic-homotopy-theory/joins-of-types.lagda.md +++ b/src/synthetic-homotopy-theory/joins-of-types.lagda.md @@ -434,6 +434,18 @@ module _ ( up-join) ``` +### The propositional recursor for joins of types + +```agda +rec-join-Prop : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (R : Prop l3) β†’ + (A β†’ type-Prop R) β†’ (B β†’ type-Prop R) β†’ A * B β†’ type-Prop R +rec-join-Prop R f g = + cogap-join + ( type-Prop R) + ( f , g , Ξ» (t , s) β†’ eq-is-prop' (is-prop-type-Prop R) (f t) (g s)) +``` + ## See also - [Joins of maps](synthetic-homotopy-theory.joins-of-maps.md) diff --git a/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md index 73103fae01a..04de7bf7bb3 100644 --- a/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md @@ -85,3 +85,8 @@ pullback-property-pushout f g c = ( precomp g Y) ( cone-pullback-property-pushout f g c Y) ``` + +## See also + +- For the dual property for [pullbacks](foundation-core.pullbacks.md), see + [postcomposition of pullbacks](foundation.postcomposition-pullbacks.md). diff --git a/src/synthetic-homotopy-theory/pushout-products.lagda.md b/src/synthetic-homotopy-theory/pushout-products.lagda.md index 5756497b68c..bc106b7c16b 100644 --- a/src/synthetic-homotopy-theory/pushout-products.lagda.md +++ b/src/synthetic-homotopy-theory/pushout-products.lagda.md @@ -80,10 +80,11 @@ from the [fibers](foundation-core.fibers-of-maps.md) of `f β–‘ g` to the There is an "adjoint relation" between the pushout-product and the [pullback-hom](orthogonal-factorization-systems.pullback-hom.md): For any three -maps `f`, `g`, and `h` we have a [homotopy](foundation-core.homotopies.md) +maps `f`, `g`, and `h` we have an +[equivalence of maps](foundation.equivalences-arrows.md) ```text - ⟨f β–‘ g , h⟩ ~ ⟨f , ⟨g , h⟩⟩. + ⟨f β–‘ g , h⟩ ≃ ⟨f , ⟨g , h⟩⟩. ``` ## Definitions @@ -159,6 +160,24 @@ module _ pr2 (pr2 (pr2 (center uniqueness-pushout-product))) ``` +## Properties + +### The adjoint relation between pushout-products and pullback-homs + +For any three maps `f`, `g`, and `h` we have an adjoint relation + +```text + hom-arrow (f β–‘ g) h ≃ hom-arrow f ⟨g , h⟩ +``` + +that extends to an equivalence of maps + +```text + ⟨f β–‘ g , h⟩ ≃ ⟨f , ⟨g , h⟩⟩. +``` + +> This remains to be formalized. + ## See also - [The dependent pushout-product](synthetic-homotopy-theory.dependent-pushout-products.md) diff --git a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md index 93ae7db590b..8bb2a52437f 100644 --- a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md +++ b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md @@ -113,7 +113,7 @@ abstract ( f x pβ‚€))) ``` -### The universal cover +### The universal cover of the circle ```agda module _