From 1bd7e406d33f5a65c1bbc7534be5a825b487a32f Mon Sep 17 00:00:00 2001 From: Mabel Najdovski Date: Thu, 2 Nov 2023 23:11:32 +0100 Subject: [PATCH 1/5] Compute equalities --- .../equality-dependent-pair-types.lagda.md | 10 +-- src/foundation-core/equivalences.lagda.md | 4 + .../equality-dependent-pair-types.lagda.md | 74 ++++++++++++++++++- 3 files changed, 81 insertions(+), 7 deletions(-) diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md index 9cf8a462d2..fea764ea38 100644 --- a/src/foundation-core/equality-dependent-pair-types.lagda.md +++ b/src/foundation-core/equality-dependent-pair-types.lagda.md @@ -106,13 +106,13 @@ module _ η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) ＝ t η-pair t = eq-pair-Σ refl refl - eq-base-eq-pair : {s t : Σ A B} → (s ＝ t) → (pr1 s ＝ pr1 t) - eq-base-eq-pair p = pr1 (pair-eq-Σ p) + eq-base-eq-pair-Σ : {s t : Σ A B} → (s ＝ t) → (pr1 s ＝ pr1 t) + eq-base-eq-pair-Σ p = pr1 (pair-eq-Σ p) - dependent-eq-family-eq-pair : + dependent-eq-family-eq-pair-Σ : {s t : Σ A B} → (p : s ＝ t) → - dependent-identification B (eq-base-eq-pair p) (pr2 s) (pr2 t) - dependent-eq-family-eq-pair p = pr2 (pair-eq-Σ p) + dependent-identification B (eq-base-eq-pair-Σ p) (pr2 s) (pr2 t) + dependent-eq-family-eq-pair-Σ p = pr2 (pair-eq-Σ p) ``` ### Lifting equality to the total space diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index de2d471030..c8701ebbb5 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/src/foundation-core/equivalences.lagda.md @@ -588,6 +588,10 @@ module _ (e : A ≃ B) (x y : A) → (x ＝ y) ≃ (map-equiv e x ＝ map-equiv e y) pr1 (equiv-ap e x y) = ap (map-equiv e) pr2 (equiv-ap e x y) = is-emb-is-equiv (is-equiv-map-equiv e) x y + + map-equiv-ap : + (e : A ≃ B) (x y : A) → (map-equiv e x ＝ map-equiv e y) → (x ＝ y) + map-equiv-ap e x y = map-equiv (inv-equiv (equiv-ap e x y)) ``` ## Equivalence reasoning diff --git a/src/foundation/equality-dependent-pair-types.lagda.md b/src/foundation/equality-dependent-pair-types.lagda.md index b6f577eadc..472b10329d 100644 --- a/src/foundation/equality-dependent-pair-types.lagda.md +++ b/src/foundation/equality-dependent-pair-types.lagda.md @@ -15,6 +15,12 @@ open import foundation.dependent-identifications open import foundation.dependent-pair-types open import foundation.transport-along-identifications open import foundation.universe-levels +open import foundation.equivalences +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.function-extensionality +open import foundation.contractible-types +open import foundation.type-arithmetic-dependent-pair-types open import foundation-core.function-types open import foundation-core.identity-types @@ -113,7 +119,7 @@ module _ ```agda module _ - { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {Y : UU l3} (f : Σ A B → Y) + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {Y : UU l3} (f : Σ A B → Y) where compute-ap-eq-pair-Σ : @@ -127,7 +133,7 @@ module _ ```agda module _ - { l1 l2 : Level} {A : UU l1} (B : A → UU l2) + {l1 l2 : Level} {A : UU l1} (B : A → UU l2) where triangle-eq-pair-Σ : @@ -137,6 +143,70 @@ module _ triangle-eq-pair-Σ refl q = refl ``` +### Computing dependent identifications in iterated dependent pair types + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} + where + + equiv-triple-eq-Σ : + (s t : Σ (Σ A B) C) → + (s ＝ t) ≃ + ( Σ + ( Σ + ( pr1 (pr1 s) ＝ pr1 (pr1 t)) + ( λ p → dependent-identification B p (pr2 (pr1 s)) (pr2 (pr1 t)))) + ( λ q → dependent-identification C (eq-pair-Σ' q) (pr2 s) (pr2 t))) + equiv-triple-eq-Σ s t = + ( equiv-Σ + ( λ q → + ( dependent-identification + ( C) + ( eq-pair-Σ' q) + ( pr2 s) + ( pr2 t))) + ( equiv-pair-eq-Σ (pr1 s) (pr1 t)) + ( λ p → + ( equiv-tr + ( λ q → dependent-identification C q (pr2 s) (pr2 t)) + ( map-equiv-ap + ( equiv-pair-eq-Σ (pr1 s) (pr1 t)) + ( p) + ( eq-pair-Σ' (pair-eq-Σ p)) + ( inv-map-eq-transpose-equiv' + ( equiv-pair-eq-Σ (pr1 s) (pr1 t)) + ( htpy-eq + ( eq-base-eq-pair-Σ + ( eq-is-contr' + ( is-contr-section-is-equiv + ( is-equiv-pair-eq-Σ (pr1 s) (pr1 t))) + ( section-is-equiv (is-equiv-pair-eq-Σ (pr1 s) (pr1 t))) + ( eq-pair-Σ' , is-retraction-pair-eq-Σ (pr1 s) (pr1 t)))) + ( pair-eq-Σ p))))))) ∘e + ( equiv-pair-eq-Σ s t) + + coh-triple-eq-Σ : + {s t : Σ A (λ x → Σ (B x) λ y → C (x , y))} (p : s ＝ t) → + eq-base-eq-pair-Σ p ＝ + eq-base-eq-pair-Σ (eq-base-eq-pair-Σ (ap (map-inv-associative-Σ A B C) p)) + coh-triple-eq-Σ refl = refl + + dependent-eq-family-eq-iterated-Σ : + (s t : Σ A (λ x → Σ (B x) λ y → C (x , y))) (p : s ＝ t) → + dependent-identification B (eq-base-eq-pair-Σ p) (pr1 (pr2 s)) (pr1 (pr2 t)) + dependent-eq-family-eq-iterated-Σ s t p = + ( ap (λ q → tr B q (pr1 (pr2 s))) (coh-triple-eq-Σ p)) ∙ + ( pr2 + ( pr1 + ( map-equiv + ( equiv-triple-eq-Σ + ( map-inv-associative-Σ A B C s) + ( map-inv-associative-Σ A B C t)) + ( ap (map-inv-associative-Σ A B C) p)))) + +``` + ## See also - Equality proofs in cartesian product types are characterized in From ebd5af7e1fd4d58c7bdfb6585d530867cfaede4e Mon Sep 17 00:00:00 2001 From: Mabel Najdovski Date: Thu, 2 Nov 2023 23:16:39 +0100 Subject: [PATCH 2/5] pre-commit --- src/foundation/equality-dependent-pair-types.lagda.md | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/foundation/equality-dependent-pair-types.lagda.md b/src/foundation/equality-dependent-pair-types.lagda.md index 472b10329d..63ae4a7ed4 100644 --- a/src/foundation/equality-dependent-pair-types.lagda.md +++ b/src/foundation/equality-dependent-pair-types.lagda.md @@ -11,16 +11,16 @@ open import foundation-core.equality-dependent-pair-types public ```agda open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions +open import foundation.contractible-types open import foundation.dependent-identifications open import foundation.dependent-pair-types -open import foundation.transport-along-identifications -open import foundation.universe-levels open import foundation.equivalences +open import foundation.function-extensionality open import foundation.functoriality-dependent-pair-types open import foundation.homotopies -open import foundation.function-extensionality -open import foundation.contractible-types +open import foundation.transport-along-identifications open import foundation.type-arithmetic-dependent-pair-types +open import foundation.universe-levels open import foundation-core.function-types open import foundation-core.identity-types @@ -191,7 +191,7 @@ module _ eq-base-eq-pair-Σ p ＝ eq-base-eq-pair-Σ (eq-base-eq-pair-Σ (ap (map-inv-associative-Σ A B C) p)) coh-triple-eq-Σ refl = refl - + dependent-eq-family-eq-iterated-Σ : (s t : Σ A (λ x → Σ (B x) λ y → C (x , y))) (p : s ＝ t) → dependent-identification B (eq-base-eq-pair-Σ p) (pr1 (pr2 s)) (pr1 (pr2 t)) @@ -204,7 +204,6 @@ module _ ( map-inv-associative-Σ A B C s) ( map-inv-associative-Σ A B C t)) ( ap (map-inv-associative-Σ A B C) p)))) - ``` ## See also From 3ec095f7c64ceaed993a41fdf58aebea823a6474 Mon Sep 17 00:00:00 2001 From: Mabel Najdovski Date: Fri, 3 Nov 2023 10:16:06 +0100 Subject: [PATCH 3/5] Renaming and cleanup --- src/foundation-core/equivalences.lagda.md | 4 +- .../equality-dependent-pair-types.lagda.md | 37 ++++++++----------- 2 files changed, 17 insertions(+), 24 deletions(-) diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index c8701ebbb5..db89c62827 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/src/foundation-core/equivalences.lagda.md @@ -589,9 +589,9 @@ module _ pr1 (equiv-ap e x y) = ap (map-equiv e) pr2 (equiv-ap e x y) = is-emb-is-equiv (is-equiv-map-equiv e) x y - map-equiv-ap : + inv-map-equiv-ap : (e : A ≃ B) (x y : A) → (map-equiv e x ＝ map-equiv e y) → (x ＝ y) - map-equiv-ap e x y = map-equiv (inv-equiv (equiv-ap e x y)) + inv-map-equiv-ap e x y = map-equiv (inv-equiv (equiv-ap e x y)) ``` ## Equivalence reasoning diff --git a/src/foundation/equality-dependent-pair-types.lagda.md b/src/foundation/equality-dependent-pair-types.lagda.md index 63ae4a7ed4..dc0e3ea267 100644 --- a/src/foundation/equality-dependent-pair-types.lagda.md +++ b/src/foundation/equality-dependent-pair-types.lagda.md @@ -154,9 +154,7 @@ module _ (s t : Σ (Σ A B) C) → (s ＝ t) ≃ ( Σ - ( Σ - ( pr1 (pr1 s) ＝ pr1 (pr1 t)) - ( λ p → dependent-identification B p (pr2 (pr1 s)) (pr2 (pr1 t)))) + ( Eq-Σ (pr1 s) (pr1 t)) ( λ q → dependent-identification C (eq-pair-Σ' q) (pr2 s) (pr2 t))) equiv-triple-eq-Σ s t = ( equiv-Σ @@ -170,33 +168,28 @@ module _ ( λ p → ( equiv-tr ( λ q → dependent-identification C q (pr2 s) (pr2 t)) - ( map-equiv-ap - ( equiv-pair-eq-Σ (pr1 s) (pr1 t)) - ( p) - ( eq-pair-Σ' (pair-eq-Σ p)) - ( inv-map-eq-transpose-equiv' - ( equiv-pair-eq-Σ (pr1 s) (pr1 t)) - ( htpy-eq - ( eq-base-eq-pair-Σ - ( eq-is-contr' - ( is-contr-section-is-equiv - ( is-equiv-pair-eq-Σ (pr1 s) (pr1 t))) - ( section-is-equiv (is-equiv-pair-eq-Σ (pr1 s) (pr1 t))) - ( eq-pair-Σ' , is-retraction-pair-eq-Σ (pr1 s) (pr1 t)))) - ( pair-eq-Σ p))))))) ∘e + ( inv (is-section-pair-eq-Σ (pr1 s) (pr1 t) p))))) ∘e ( equiv-pair-eq-Σ s t) - coh-triple-eq-Σ : + triple-eq-Σ : + (s t : Σ (Σ A B) C) → + (s ＝ t) → + ( Σ + ( Eq-Σ (pr1 s) (pr1 t)) + ( λ q → dependent-identification C (eq-pair-Σ' q) (pr2 s) (pr2 t))) + triple-eq-Σ s t = map-equiv (equiv-triple-eq-Σ s t) + + coh-triple-Σ : {s t : Σ A (λ x → Σ (B x) λ y → C (x , y))} (p : s ＝ t) → eq-base-eq-pair-Σ p ＝ eq-base-eq-pair-Σ (eq-base-eq-pair-Σ (ap (map-inv-associative-Σ A B C) p)) - coh-triple-eq-Σ refl = refl + coh-triple-Σ refl = refl - dependent-eq-family-eq-iterated-Σ : + dependent-eq-snd-eq-iterated-Σ : (s t : Σ A (λ x → Σ (B x) λ y → C (x , y))) (p : s ＝ t) → dependent-identification B (eq-base-eq-pair-Σ p) (pr1 (pr2 s)) (pr1 (pr2 t)) - dependent-eq-family-eq-iterated-Σ s t p = - ( ap (λ q → tr B q (pr1 (pr2 s))) (coh-triple-eq-Σ p)) ∙ + dependent-eq-snd-eq-iterated-Σ s t p = + ( ap (λ q → tr B q (pr1 (pr2 s))) (coh-triple-Σ p)) ∙ ( pr2 ( pr1 ( map-equiv From d4a3373951bdb0534eb6dfd8a0ee8c1e3d57f153 Mon Sep 17 00:00:00 2001 From: Mabel Najdovski Date: Fri, 3 Nov 2023 10:27:11 +0100 Subject: [PATCH 4/5] Interchange law --- .../type-arithmetic-dependent-pair-types.lagda.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md index 4e4bbb8561..4bf1514a85 100644 --- a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md +++ b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md @@ -305,6 +305,14 @@ module _ pr1 interchange-Σ-Σ = map-interchange-Σ-Σ pr2 interchange-Σ-Σ = is-equiv-map-interchange-Σ-Σ + interchange-iterated-Σ-Σ : + Σ A (λ x → Σ (B x) (λ y → Σ (C x) (D x y))) ≃ + Σ A (λ x → Σ (C x) (λ z → Σ (B x) λ y → D x y z)) + interchange-iterated-Σ-Σ = + associative-Σ' A C (λ x z → Σ (B x) λ y → D x y z) ∘e + interchange-Σ-Σ ∘e + inv-associative-Σ' A B (λ x y → Σ (C x) (D x y)) + eq-interchange-Σ-Σ-is-contr : {a : A} {b : B a} → is-torsorial (D a b) → {x y : Σ (C a) (D a b)} → From a9d3b660a0a09f2de77f460982884d5ce1d9a264 Mon Sep 17 00:00:00 2001 From: Mabel Najdovski Date: Fri, 3 Nov 2023 14:28:24 +0100 Subject: [PATCH 5/5] Formatting and quadruples --- src/foundation-core/equivalences.lagda.md | 4 +- .../equality-dependent-pair-types.lagda.md | 88 +++++++++++++------ ...e-arithmetic-dependent-pair-types.lagda.md | 4 +- 3 files changed, 65 insertions(+), 31 deletions(-) diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index db89c62827..75624a9430 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/src/foundation-core/equivalences.lagda.md @@ -589,9 +589,9 @@ module _ pr1 (equiv-ap e x y) = ap (map-equiv e) pr2 (equiv-ap e x y) = is-emb-is-equiv (is-equiv-map-equiv e) x y - inv-map-equiv-ap : + map-inv-equiv-ap : (e : A ≃ B) (x y : A) → (map-equiv e x ＝ map-equiv e y) → (x ＝ y) - inv-map-equiv-ap e x y = map-equiv (inv-equiv (equiv-ap e x y)) + map-inv-equiv-ap e x y = map-inv-equiv (equiv-ap e x y) ``` ## Equivalence reasoning diff --git a/src/foundation/equality-dependent-pair-types.lagda.md b/src/foundation/equality-dependent-pair-types.lagda.md index dc0e3ea267..7048e772fa 100644 --- a/src/foundation/equality-dependent-pair-types.lagda.md +++ b/src/foundation/equality-dependent-pair-types.lagda.md @@ -143,20 +143,24 @@ module _ triangle-eq-pair-Σ refl q = refl ``` -### Computing dependent identifications in iterated dependent pair types +### Computing identifications in iterated dependent pair types + +#### Computing identifications in dependent pair types of the form Σ (Σ A B) C ```agda module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} where - equiv-triple-eq-Σ : + Eq-Σ²' : (s t : Σ (Σ A B) C) → UU (l1 ⊔ l2 ⊔ l3) + Eq-Σ²' s t = + Σ ( Eq-Σ (pr1 s) (pr1 t)) + ( λ q → dependent-identification C (eq-pair-Σ' q) (pr2 s) (pr2 t)) + + equiv-triple-eq-Σ' : (s t : Σ (Σ A B) C) → - (s ＝ t) ≃ - ( Σ - ( Eq-Σ (pr1 s) (pr1 t)) - ( λ q → dependent-identification C (eq-pair-Σ' q) (pr2 s) (pr2 t))) - equiv-triple-eq-Σ s t = + (s ＝ t) ≃ Eq-Σ²' s t + equiv-triple-eq-Σ' s t = ( equiv-Σ ( λ q → ( dependent-identification @@ -171,32 +175,62 @@ module _ ( inv (is-section-pair-eq-Σ (pr1 s) (pr1 t) p))))) ∘e ( equiv-pair-eq-Σ s t) - triple-eq-Σ : + triple-eq-Σ' : (s t : Σ (Σ A B) C) → - (s ＝ t) → - ( Σ - ( Eq-Σ (pr1 s) (pr1 t)) - ( λ q → dependent-identification C (eq-pair-Σ' q) (pr2 s) (pr2 t))) - triple-eq-Σ s t = map-equiv (equiv-triple-eq-Σ s t) - - coh-triple-Σ : - {s t : Σ A (λ x → Σ (B x) λ y → C (x , y))} (p : s ＝ t) → + (s ＝ t) → Eq-Σ²' s t + triple-eq-Σ' s t = map-equiv (equiv-triple-eq-Σ' s t) +``` + +#### Computing dependent identifications on the second component + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + where + + coh-eq-base-Σ² : + {s t : Σ A (λ x → Σ (B x) λ y → C x y)} (p : s ＝ t) → eq-base-eq-pair-Σ p ＝ - eq-base-eq-pair-Σ (eq-base-eq-pair-Σ (ap (map-inv-associative-Σ A B C) p)) - coh-triple-Σ refl = refl + eq-base-eq-pair-Σ (eq-base-eq-pair-Σ (ap (map-inv-associative-Σ' A B C) p)) + coh-eq-base-Σ² refl = refl - dependent-eq-snd-eq-iterated-Σ : - (s t : Σ A (λ x → Σ (B x) λ y → C (x , y))) (p : s ＝ t) → + dependent-eq-second-component-eq-Σ² : + {s t : Σ A (λ x → Σ (B x) λ y → C x y)} (p : s ＝ t) → dependent-identification B (eq-base-eq-pair-Σ p) (pr1 (pr2 s)) (pr1 (pr2 t)) - dependent-eq-snd-eq-iterated-Σ s t p = - ( ap (λ q → tr B q (pr1 (pr2 s))) (coh-triple-Σ p)) ∙ + dependent-eq-second-component-eq-Σ² {s = s} {t = t} p = + ( ap (λ q → tr B q (pr1 (pr2 s))) (coh-eq-base-Σ² p)) ∙ ( pr2 ( pr1 - ( map-equiv - ( equiv-triple-eq-Σ - ( map-inv-associative-Σ A B C s) - ( map-inv-associative-Σ A B C t)) - ( ap (map-inv-associative-Σ A B C) p)))) + ( triple-eq-Σ' + ( map-inv-associative-Σ' A B C s) + ( map-inv-associative-Σ' A B C t) + ( ap (map-inv-associative-Σ' A B C) p)))) +``` + +#### Computing dependent identifications on the third component + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + (D : (x : A) → B x → C x → UU l4) + where + + coh-eq-base-Σ³ : + { s t : Σ A (λ x → Σ (B x) (λ y → Σ (C x) (D x y)))} (p : s ＝ t) → + eq-base-eq-pair-Σ p ＝ + eq-base-eq-pair-Σ (ap (map-equiv (interchange-Σ-Σ-Σ D)) p) + coh-eq-base-Σ³ refl = refl + + dependent-eq-third-component-eq-Σ³ : + { s t : Σ A (λ x → Σ (B x) (λ y → Σ (C x) (D x y)))} (p : s ＝ t) → + dependent-identification C + ( eq-base-eq-pair-Σ p) + ( pr1 (pr2 (pr2 s))) + ( pr1 (pr2 (pr2 t))) + dependent-eq-third-component-eq-Σ³ {s = s} {t = t} p = + ( ap (λ q → tr C q (pr1 (pr2 (pr2 s)))) (coh-eq-base-Σ³ p)) ∙ + ( dependent-eq-second-component-eq-Σ² + ( ap (map-equiv (interchange-Σ-Σ-Σ D)) p)) ``` ## See also diff --git a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md index 4bf1514a85..ebca7b4ac0 100644 --- a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md +++ b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md @@ -305,10 +305,10 @@ module _ pr1 interchange-Σ-Σ = map-interchange-Σ-Σ pr2 interchange-Σ-Σ = is-equiv-map-interchange-Σ-Σ - interchange-iterated-Σ-Σ : + interchange-Σ-Σ-Σ : Σ A (λ x → Σ (B x) (λ y → Σ (C x) (D x y))) ≃ Σ A (λ x → Σ (C x) (λ z → Σ (B x) λ y → D x y z)) - interchange-iterated-Σ-Σ = + interchange-Σ-Σ-Σ = associative-Σ' A C (λ x z → Σ (B x) λ y → D x y z) ∘e interchange-Σ-Σ ∘e inv-associative-Σ' A B (λ x y → Σ (C x) (D x y))