Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Dirichlet exponential of species (of types and of types in a subunive…
…rse) (#628) In this PR I have: - Defined **pi-decomposition** (A pi-decomposition of a type `A` is a type `X` and a family of types `Y` over `X` and an equivalence from `A` to `\Pi X Y`) - Defined **pi-decomposition-subuniverse** - With the above, defined the **Dirichlet exponential** of a species of types - Shown **arithmetical laws** between pi-decomposition binary-product-decompositon and binary-coproduct-decompositon - With the above, shown that **the Dirichlet exponential of the coproduct is the Dirichlet product of the Dirichlet exponentials** - I have also done some **cleaning** by giving a name to the properties needed on subuniverses (`is-closed-under-dirichlet-product-species-subuniverse` , `is-closed-under-cauchy-product-species-subuniverse` and `is-closed-under-coproduct-species-subuniverse`) --------- Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
- Loading branch information
1 parent
aa65238
commit 669f9bb
Showing
14 changed files
with
2,219 additions
and
431 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
227 changes: 227 additions & 0 deletions
227
src/foundation/arithmetic-law-product-and-pi-decompositions.lagda.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,227 @@ | ||
| # Arithmetic law for product decomposition and Π-decomposition | ||
|
|
||
| ```agda | ||
| module foundation.arithmetic-law-product-and-pi-decompositions where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import foundation.coproduct-decompositions | ||
| open import foundation.equivalences | ||
| open import foundation.functoriality-cartesian-product-types | ||
| open import foundation.functoriality-coproduct-types | ||
| open import foundation.functoriality-dependent-pair-types | ||
| open import foundation.pi-decompositions | ||
| open import foundation.product-decompositions | ||
| open import foundation.type-arithmetic-cartesian-product-types | ||
| open import foundation.type-arithmetic-coproduct-types | ||
| open import foundation.type-arithmetic-dependent-pair-types | ||
| open import foundation.univalence | ||
| open import foundation.universal-property-coproduct-types | ||
|
|
||
| open import foundation-core.cartesian-product-types | ||
| open import foundation-core.contractible-types | ||
| open import foundation-core.coproduct-types | ||
| open import foundation-core.dependent-pair-types | ||
| open import foundation-core.functions | ||
| open import foundation-core.homotopies | ||
| open import foundation-core.identity-types | ||
| open import foundation-core.universe-levels | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| Let `X` be a type, we have the following equivalence : | ||
|
|
||
| ```text | ||
| Σ ( (U , V , e) : Π-Decomposition X) | ||
| ( binary-product-Decomposition U) ≃ | ||
| Σ ( (A , B , e) : binary-product-Decomposition X) | ||
| ( Π-Decomposition A × | ||
| Π-Decomposition B ) | ||
| ``` | ||
|
|
||
| We also show a computational rule to simplify the use of this equivalence. | ||
|
|
||
| ## Propositions | ||
|
|
||
| ### Product decompositions of the indexing type of a Π-decomposition are equivalent to Π-decomposition of the left and right summand of a product decomposition. | ||
|
|
||
| ```agda | ||
| module _ | ||
| {l : Level} {X : UU l} | ||
| where | ||
|
|
||
| private | ||
| reassociate : | ||
| Σ (Π-Decomposition l l X) | ||
| ( λ d → binary-coproduct-Decomposition l l | ||
| ( indexing-type-Π-Decomposition d)) ≃ | ||
| Σ ( UU l) | ||
| ( λ A → | ||
| Σ ( UU l) | ||
| ( λ B → | ||
| Σ ( Σ ( UU l) λ U → ( U ≃ (A + B))) | ||
| ( λ U → Σ (pr1 U → UU l) (λ Y → X ≃ Π (pr1 U) Y)))) | ||
| pr1 reassociate ((U , V , f) , A , B , e) = (A , B , (U , e) , V , f) | ||
| pr2 reassociate = | ||
| is-equiv-has-inverse | ||
| ( λ (A , B , (U , e) , V , f) → ((U , V , f) , A , B , e)) | ||
| ( refl-htpy) | ||
| ( refl-htpy) | ||
|
|
||
| reassociate' : | ||
| Σ ( UU l) | ||
| ( λ A → | ||
| Σ ( UU l) | ||
| ( λ B → | ||
| Σ ( (A → UU l) × (B → UU l)) | ||
| ( λ (YA , YB) → | ||
| Σ ( Σ (UU l) (λ A' → A' ≃ Π A YA)) | ||
| ( λ A' → | ||
| Σ ( Σ (UU l) (λ B' → B' ≃ Π B YB)) | ||
| ( λ B' → X ≃ (pr1 A' × pr1 B')))))) ≃ | ||
| Σ ( binary-product-Decomposition l l X) | ||
| ( λ d → | ||
| Π-Decomposition l l | ||
| ( left-summand-binary-product-Decomposition d) × | ||
| Π-Decomposition l l | ||
| ( right-summand-binary-product-Decomposition d)) | ||
| pr1 reassociate' (A , B , (YA , YB) , (A' , eA) , (B' , eB) , e) = | ||
| (A' , B' , e) , ((A , YA , eA) , B , YB , eB) | ||
| pr2 reassociate' = | ||
| is-equiv-has-inverse | ||
| ( λ ((A' , B' , e) , ((A , YA , eA) , B , YB , eB)) → | ||
| (A , B , (YA , YB) , (A' , eA) , (B' , eB) , e)) | ||
| ( refl-htpy) | ||
| ( refl-htpy) | ||
|
|
||
| equiv-binary-product-Decomposition-Π-Decomposition : | ||
| Σ ( Π-Decomposition l l X) | ||
| ( λ d → | ||
| binary-coproduct-Decomposition l l | ||
| ( indexing-type-Π-Decomposition d)) ≃ | ||
| Σ ( binary-product-Decomposition l l X) | ||
| ( λ d → | ||
| Π-Decomposition l l | ||
| ( left-summand-binary-product-Decomposition d) × | ||
| Π-Decomposition l l | ||
| ( right-summand-binary-product-Decomposition d)) | ||
|
|
||
| equiv-binary-product-Decomposition-Π-Decomposition = | ||
| ( ( reassociate') ∘e | ||
| ( ( equiv-tot | ||
| ( λ A → | ||
| equiv-tot | ||
| ( λ B → | ||
| ( ( equiv-tot | ||
| ( λ ( YA , YB) → | ||
| ( ( equiv-tot | ||
| ( λ A' → | ||
| equiv-tot | ||
| ( λ B' → | ||
| equiv-postcomp-equiv | ||
| ( equiv-prod | ||
| ( inv-equiv (pr2 A')) | ||
| ( inv-equiv (pr2 B'))) | ||
| ( X))) ∘e | ||
| ( ( inv-left-unit-law-Σ-is-contr | ||
| ( is-contr-total-equiv' (Π A YA)) | ||
| ( Π A YA , id-equiv)) ∘e | ||
| ( inv-left-unit-law-Σ-is-contr | ||
| ( is-contr-total-equiv' (Π B YB)) | ||
| ( Π B YB , id-equiv)))))) ∘e | ||
| ( ( equiv-Σ-equiv-base | ||
| ( λ z → X ≃ (Π A (pr1 z) × Π B (pr2 z))) | ||
| ( equiv-universal-property-coprod (UU l))) ∘e | ||
| ( ( equiv-tot | ||
| ( λ Y → | ||
| equiv-postcomp-equiv | ||
| ( equiv-dependent-universal-property-coprod Y) | ||
| ( X))) ∘e | ||
| ( left-unit-law-Σ-is-contr | ||
| ( is-contr-total-equiv' (A + B)) | ||
| ((A + B) , id-equiv))))))))) ∘e | ||
| ( reassociate))) | ||
|
|
||
| module _ | ||
| ( D : Σ ( Π-Decomposition l l X) | ||
| ( λ D → | ||
| binary-coproduct-Decomposition | ||
| l l | ||
| ( indexing-type-Π-Decomposition D))) | ||
| where | ||
|
|
||
| private | ||
| tr-total-equiv : | ||
| {l1 l3 l4 : Level} {X Y : UU l1} (e : Y ≃ X) → | ||
| (h : Id {A = Σ (UU l1) λ Y → Y ≃ X} (X , id-equiv) (Y , e)) → | ||
| {C : (X : UU l1) → (X → UU l3) → UU l4} → | ||
| {f : Σ (Y → UU l3) (λ Z → C Y Z)} → | ||
| (x : X) → | ||
| pr1 | ||
| ( tr | ||
| ( λ Y → | ||
| ( Σ ( pr1 Y → UU l3) | ||
| ( λ Z → C (pr1 Y) Z) → | ||
| Σ ( X → UU l3) | ||
| ( λ Z → C X Z))) | ||
| ( h) | ||
| ( id) | ||
| ( f)) | ||
| ( x) ＝ | ||
| pr1 f (map-inv-equiv e x) | ||
| tr-total-equiv e refl x = refl | ||
|
|
||
| compute-left-equiv-binary-product-Decomposition-Π-Decomposition : | ||
| ( a : left-summand-binary-coproduct-Decomposition (pr2 D)) → | ||
| cotype-Π-Decomposition | ||
| ( pr1 | ||
| ( pr2 | ||
| ( map-equiv equiv-binary-product-Decomposition-Π-Decomposition | ||
| ( D)))) | ||
| ( a) ＝ | ||
| cotype-Π-Decomposition | ||
| ( pr1 D) | ||
| ( map-inv-equiv | ||
| ( matching-correspondence-binary-coproduct-Decomposition (pr2 D)) | ||
| ( inl a)) | ||
| compute-left-equiv-binary-product-Decomposition-Π-Decomposition a = | ||
| tr-total-equiv | ||
| ( matching-correspondence-binary-coproduct-Decomposition (pr2 D)) | ||
| ( inv | ||
| ( contraction | ||
| ( is-contr-total-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D)))) | ||
| ( (pr1 (pr2 D) + pr1 (pr2 (pr2 D))) , id-equiv)) ∙ | ||
| contraction | ||
| ( is-contr-total-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D)))) | ||
| ( pr1 (pr1 D) , pr2 (pr2 (pr2 D)))) | ||
| ( inl a) | ||
|
|
||
| compute-right-equiv-binary-product-Decomposition-Π-Decomposition : | ||
| ( b : right-summand-binary-coproduct-Decomposition (pr2 D)) → | ||
| cotype-Π-Decomposition | ||
| ( pr2 | ||
| ( pr2 | ||
| ( map-equiv equiv-binary-product-Decomposition-Π-Decomposition | ||
| ( D)))) | ||
| ( b) ＝ | ||
| cotype-Π-Decomposition (pr1 D) | ||
| ( map-inv-equiv | ||
| ( matching-correspondence-binary-coproduct-Decomposition (pr2 D)) | ||
| ( inr b)) | ||
| compute-right-equiv-binary-product-Decomposition-Π-Decomposition b = | ||
| tr-total-equiv | ||
| ( matching-correspondence-binary-coproduct-Decomposition (pr2 D)) | ||
| ( inv | ||
| ( contraction | ||
| ( is-contr-total-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D)))) | ||
| ( (pr1 (pr2 D) + pr1 (pr2 (pr2 D))) , id-equiv)) ∙ | ||
| contraction | ||
| ( is-contr-total-equiv' (pr1 (pr2 D) + pr1 (pr2 (pr2 D)))) | ||
| ( pr1 (pr1 D) , pr2 (pr2 (pr2 D)))) | ||
| ( inr b) | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,141 @@ | ||
| # Π-decompositions of types into types in a subuniverse | ||
|
|
||
| ```agda | ||
| module foundation.pi-decompositions-subuniverse where | ||
| ``` | ||
|
|
||
| <details><summary>Imports</summary> | ||
|
|
||
| ```agda | ||
| open import foundation.pi-decompositions | ||
| open import foundation.subuniverses | ||
|
|
||
| open import foundation-core.cartesian-product-types | ||
| open import foundation-core.dependent-pair-types | ||
| open import foundation-core.equivalences | ||
| open import foundation-core.homotopies | ||
| open import foundation-core.propositions | ||
| open import foundation-core.universe-levels | ||
| ``` | ||
|
|
||
| </details> | ||
|
|
||
| ## Idea | ||
|
|
||
| Consider a subuniverse `P` and a type `A` in `P`. A **Π-decomposition** of `A` | ||
| into types in `P` consists of a type `X` in `P` and a family `Y` of types in `P` | ||
| indexed over `X`, equipped with an equivalence | ||
|
|
||
| ```text | ||
| A ≃ Π X Y. | ||
| ``` | ||
|
|
||
| ## Definition | ||
|
|
||
| ### The predicate of being a Π-decomposition in a subuniverse | ||
|
|
||
| ```agda | ||
| is-in-subuniverse-Π-Decomposition : | ||
| {l1 l2 l3 : Level} (P : subuniverse l1 l2) {A : UU l3} → | ||
| Π-Decomposition l1 l1 A → UU (l1 ⊔ l2) | ||
| is-in-subuniverse-Π-Decomposition P D = | ||
| ( is-in-subuniverse P (indexing-type-Π-Decomposition D)) × | ||
| ( ( x : indexing-type-Π-Decomposition D) → | ||
| ( is-in-subuniverse P (cotype-Π-Decomposition D x))) | ||
| ``` | ||
|
|
||
| ### Π-decompositions in a subuniverse | ||
|
|
||
| ```agda | ||
| Π-Decomposition-Subuniverse : | ||
| {l1 l2 : Level} (P : subuniverse l1 l2) → | ||
| type-subuniverse P → UU (lsuc l1 ⊔ l2) | ||
| Π-Decomposition-Subuniverse P A = | ||
| Σ ( type-subuniverse P) | ||
| ( λ X → | ||
| Σ ( fam-subuniverse P (inclusion-subuniverse P X)) | ||
| ( λ Y → | ||
| inclusion-subuniverse P A ≃ | ||
| Π ( inclusion-subuniverse P X) | ||
| ( λ x → inclusion-subuniverse P (Y x)))) | ||
|
|
||
| module _ | ||
| {l1 l2 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P) | ||
| (D : Π-Decomposition-Subuniverse P A) | ||
| where | ||
|
|
||
| subuniverse-indexing-type-Π-Decomposition-Subuniverse : type-subuniverse P | ||
| subuniverse-indexing-type-Π-Decomposition-Subuniverse = pr1 D | ||
|
|
||
| indexing-type-Π-Decomposition-Subuniverse : UU l1 | ||
| indexing-type-Π-Decomposition-Subuniverse = | ||
| inclusion-subuniverse P | ||
| subuniverse-indexing-type-Π-Decomposition-Subuniverse | ||
|
|
||
| is-in-subuniverse-indexing-type-Π-Decomposition-Subuniverse : | ||
| type-Prop (P indexing-type-Π-Decomposition-Subuniverse) | ||
| is-in-subuniverse-indexing-type-Π-Decomposition-Subuniverse = | ||
| pr2 subuniverse-indexing-type-Π-Decomposition-Subuniverse | ||
|
|
||
| subuniverse-cotype-Π-Decomposition-Subuniverse : | ||
| fam-subuniverse P indexing-type-Π-Decomposition-Subuniverse | ||
| subuniverse-cotype-Π-Decomposition-Subuniverse = pr1 (pr2 D) | ||
|
|
||
| cotype-Π-Decomposition-Subuniverse : | ||
| (indexing-type-Π-Decomposition-Subuniverse → UU l1) | ||
| cotype-Π-Decomposition-Subuniverse X = | ||
| inclusion-subuniverse P (subuniverse-cotype-Π-Decomposition-Subuniverse X) | ||
|
|
||
| is-in-subuniverse-cotype-Π-Decomposition-Subuniverse : | ||
| ((x : indexing-type-Π-Decomposition-Subuniverse) → | ||
| type-Prop (P (cotype-Π-Decomposition-Subuniverse x))) | ||
| is-in-subuniverse-cotype-Π-Decomposition-Subuniverse x = | ||
| pr2 (subuniverse-cotype-Π-Decomposition-Subuniverse x) | ||
|
|
||
| matching-correspondence-Π-Decomposition-Subuniverse : | ||
| inclusion-subuniverse P A ≃ | ||
| Π ( indexing-type-Π-Decomposition-Subuniverse) | ||
| ( cotype-Π-Decomposition-Subuniverse) | ||
| matching-correspondence-Π-Decomposition-Subuniverse = pr2 (pr2 D) | ||
| ``` | ||
|
|
||
| ## Properties | ||
|
|
||
| ### The type of Π-decompositions in a subuniverse is equivalent to the total space of `is-in-subuniverse-Π-Decomposition` | ||
|
|
||
| ```agda | ||
| map-equiv-total-is-in-subuniverse-Π-Decomposition : | ||
| {l1 l2 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P) → | ||
| Π-Decomposition-Subuniverse P A → | ||
| Σ ( Π-Decomposition l1 l1 (inclusion-subuniverse P A)) | ||
| ( is-in-subuniverse-Π-Decomposition P) | ||
| map-equiv-total-is-in-subuniverse-Π-Decomposition P A D = | ||
| ( indexing-type-Π-Decomposition-Subuniverse P A D , | ||
| ( cotype-Π-Decomposition-Subuniverse P A D , | ||
| matching-correspondence-Π-Decomposition-Subuniverse P A D)) , | ||
| ( is-in-subuniverse-indexing-type-Π-Decomposition-Subuniverse P A D , | ||
| is-in-subuniverse-cotype-Π-Decomposition-Subuniverse P A D) | ||
|
|
||
| map-inv-equiv-Π-Decomposition-Π-Decomposition-Subuniverse : | ||
| {l1 l2 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P) → | ||
| Σ ( Π-Decomposition l1 l1 (inclusion-subuniverse P A)) | ||
| ( is-in-subuniverse-Π-Decomposition P) → | ||
| Π-Decomposition-Subuniverse P A | ||
| map-inv-equiv-Π-Decomposition-Π-Decomposition-Subuniverse P A X = | ||
| ( ( indexing-type-Π-Decomposition (pr1 X) , (pr1 (pr2 X))) , | ||
| ( (λ x → cotype-Π-Decomposition (pr1 X) x , pr2 (pr2 X) x) , | ||
| matching-correspondence-Π-Decomposition (pr1 X))) | ||
|
|
||
| equiv-total-is-in-subuniverse-Π-Decomposition : | ||
| {l1 l2 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P) → | ||
| ( Π-Decomposition-Subuniverse P A) ≃ | ||
| ( Σ ( Π-Decomposition l1 l1 (inclusion-subuniverse P A)) | ||
| ( is-in-subuniverse-Π-Decomposition P)) | ||
| pr1 (equiv-total-is-in-subuniverse-Π-Decomposition P A) = | ||
| map-equiv-total-is-in-subuniverse-Π-Decomposition P A | ||
| pr2 (equiv-total-is-in-subuniverse-Π-Decomposition P A) = | ||
| is-equiv-has-inverse | ||
| ( map-inv-equiv-Π-Decomposition-Π-Decomposition-Subuniverse P A) | ||
| ( refl-htpy) | ||
| ( refl-htpy) | ||
| ``` |
Oops, something went wrong.