From cfd565d8edb1093ba1a9196b469239dc37469b8c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 6 Jan 2025 01:13:54 +0100 Subject: [PATCH] Iterating families of maps over a map (#1195) Adds a module about iterating families of maps over a map, and does some refactoring for inverse sequential diagrams. --- .../finitely-cyclic-maps.lagda.md | 7 +- src/foundation.lagda.md | 1 + ...ndent-inverse-sequential-diagrams.lagda.md | 36 +++++- ...ences-inverse-sequential-diagrams.lagda.md | 7 +- .../inverse-sequential-diagrams.lagda.md | 3 +- .../iterating-families-of-maps.lagda.md | 116 +++++++++++++++++ src/foundation/iterating-functions.lagda.md | 16 ++- ...hisms-inverse-sequential-diagrams.lagda.md | 120 +++++++++--------- .../multivariable-correspondences.lagda.md | 3 +- 9 files changed, 224 insertions(+), 85 deletions(-) create mode 100644 src/foundation/iterating-families-of-maps.lagda.md diff --git a/src/elementary-number-theory/finitely-cyclic-maps.lagda.md b/src/elementary-number-theory/finitely-cyclic-maps.lagda.md index d5cbb43992..d70daec324 100644 --- a/src/elementary-number-theory/finitely-cyclic-maps.lagda.md +++ b/src/elementary-number-theory/finitely-cyclic-maps.lagda.md @@ -58,7 +58,10 @@ module _ (f : X → X) (H : is-finitely-cyclic-map f) → (f ∘ map-inv-is-finitely-cyclic-map f H) ~ id is-section-map-inv-is-finitely-cyclic-map f H x = - ( iterate-succ-ℕ (length-path-is-finitely-cyclic-map H (f x) x) f x) ∙ + ( reassociate-iterate-succ-ℕ + ( length-path-is-finitely-cyclic-map H (f x) x) + ( f) + ( x)) ∙ ( eq-is-finitely-cyclic-map H (f x) x) is-retraction-map-inv-is-finitely-cyclic-map : @@ -70,7 +73,7 @@ module _ ( inv (eq-is-finitely-cyclic-map H (f x) x))) ∙ ( ( ap ( iterate (length-path-is-finitely-cyclic-map H (f (f x)) (f x)) f) - ( iterate-succ-ℕ + ( reassociate-iterate-succ-ℕ ( length-path-is-finitely-cyclic-map H (f x) x) f (f x))) ∙ ( ( iterate-iterate ( length-path-is-finitely-cyclic-map H (f (f x)) (f x)) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index a37fa70f98..0460bc24cd 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -249,6 +249,7 @@ open import foundation.iterated-cartesian-product-types public open import foundation.iterated-dependent-pair-types public open import foundation.iterated-dependent-product-types public open import foundation.iterating-automorphisms public +open import foundation.iterating-families-of-maps public open import foundation.iterating-functions public open import foundation.iterating-involutions public open import foundation.kernel-span-diagrams-of-maps public diff --git a/src/foundation/dependent-inverse-sequential-diagrams.lagda.md b/src/foundation/dependent-inverse-sequential-diagrams.lagda.md index 962e766c42..f48ea9d065 100644 --- a/src/foundation/dependent-inverse-sequential-diagrams.lagda.md +++ b/src/foundation/dependent-inverse-sequential-diagrams.lagda.md @@ -11,6 +11,7 @@ open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.inverse-sequential-diagrams +open import foundation.iterating-families-of-maps open import foundation.unit-type open import foundation.universe-levels @@ -114,9 +115,10 @@ module _ naturality-section-dependent-inverse-sequential-diagram : (h : (n : ℕ) (x : family-inverse-sequential-diagram A n) → - family-dependent-inverse-sequential-diagram B n x) - (n : ℕ) → UU (l1 ⊔ l2) - naturality-section-dependent-inverse-sequential-diagram h n = + family-dependent-inverse-sequential-diagram B n x) → + UU (l1 ⊔ l2) + naturality-section-dependent-inverse-sequential-diagram h = + ( n : ℕ) → h n ∘ map-inverse-sequential-diagram A n ~ map-dependent-inverse-sequential-diagram B n _ ∘ h (succ-ℕ n) @@ -124,8 +126,7 @@ module _ section-dependent-inverse-sequential-diagram = Σ ( (n : ℕ) (x : family-inverse-sequential-diagram A n) → family-dependent-inverse-sequential-diagram B n x) - ( λ h → (n : ℕ) → - naturality-section-dependent-inverse-sequential-diagram h n) + ( naturality-section-dependent-inverse-sequential-diagram) map-section-dependent-inverse-sequential-diagram : section-dependent-inverse-sequential-diagram → @@ -134,10 +135,9 @@ module _ map-section-dependent-inverse-sequential-diagram = pr1 naturality-map-section-dependent-inverse-sequential-diagram : - (f : section-dependent-inverse-sequential-diagram) (n : ℕ) → + (f : section-dependent-inverse-sequential-diagram) → naturality-section-dependent-inverse-sequential-diagram ( map-section-dependent-inverse-sequential-diagram f) - ( n) naturality-map-section-dependent-inverse-sequential-diagram = pr2 ``` @@ -158,6 +158,17 @@ pr1 (right-shift-dependent-inverse-sequential-diagram B) n = family-dependent-inverse-sequential-diagram B (succ-ℕ n) pr2 (right-shift-dependent-inverse-sequential-diagram B) n = map-dependent-inverse-sequential-diagram B (succ-ℕ n) + +iterated-right-shift-dependent-inverse-sequential-diagram : + {l1 l2 : Level} (n : ℕ) → + (A : inverse-sequential-diagram l1) → + dependent-inverse-sequential-diagram l2 A → + dependent-inverse-sequential-diagram l2 + ( iterated-right-shift-inverse-sequential-diagram n A) +iterated-right-shift-dependent-inverse-sequential-diagram n A = + iterate-family-of-maps n + ( λ A → right-shift-dependent-inverse-sequential-diagram {A = A}) + ( A) ``` ### Left shifting a dependent inverse sequential diagram @@ -179,6 +190,17 @@ pr2 (left-shift-dependent-inverse-sequential-diagram B) 0 x = raise-terminal-map (family-dependent-inverse-sequential-diagram B 0 x) pr2 (left-shift-dependent-inverse-sequential-diagram B) (succ-ℕ n) = map-dependent-inverse-sequential-diagram B n + +iterated-left-shift-dependent-inverse-sequential-diagram : + {l1 l2 : Level} (n : ℕ) → + (A : inverse-sequential-diagram l1) → + dependent-inverse-sequential-diagram l2 A → + dependent-inverse-sequential-diagram l2 + ( iterated-left-shift-inverse-sequential-diagram n A) +iterated-left-shift-dependent-inverse-sequential-diagram n A = + iterate-family-of-maps n + ( λ A → left-shift-dependent-inverse-sequential-diagram {A = A}) + ( A) ``` ## Table of files about sequential limits diff --git a/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md b/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md index c7439c75b1..3653847a20 100644 --- a/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md +++ b/src/foundation/equivalences-inverse-sequential-diagrams.lagda.md @@ -9,6 +9,7 @@ module foundation.equivalences-inverse-sequential-diagrams where ```agda open import elementary-number-theory.natural-numbers +open import foundation.binary-homotopies open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types open import foundation.fundamental-theorem-of-identity-types @@ -56,8 +57,7 @@ equiv-inverse-sequential-diagram A B = Σ ( (n : ℕ) → family-inverse-sequential-diagram A n ≃ family-inverse-sequential-diagram B n) - ( λ e → - (n : ℕ) → naturality-hom-inverse-sequential-diagram A B (map-equiv ∘ e) n) + ( λ e → naturality-hom-inverse-sequential-diagram A B (map-equiv ∘ e)) hom-equiv-inverse-sequential-diagram : {l1 l2 : Level} @@ -94,8 +94,7 @@ is-torsorial-equiv-inverse-sequential-diagram A = ( is-torsorial-Eq-Π ( λ n → is-torsorial-equiv (family-inverse-sequential-diagram A n))) ( family-inverse-sequential-diagram A , λ n → id-equiv) - ( is-torsorial-Eq-Π - ( λ n → is-torsorial-htpy (map-inverse-sequential-diagram A n))) + ( is-torsorial-binary-htpy (map-inverse-sequential-diagram A)) is-equiv-equiv-eq-inverse-sequential-diagram : {l : Level} (A B : inverse-sequential-diagram l) → diff --git a/src/foundation/inverse-sequential-diagrams.lagda.md b/src/foundation/inverse-sequential-diagrams.lagda.md index 967d3f4e29..28053d466e 100644 --- a/src/foundation/inverse-sequential-diagrams.lagda.md +++ b/src/foundation/inverse-sequential-diagrams.lagda.md @@ -79,8 +79,7 @@ pr2 (right-shift-inverse-sequential-diagram A) n = map-inverse-sequential-diagram A (succ-ℕ n) iterated-right-shift-inverse-sequential-diagram : - {l : Level} (n : ℕ) → - inverse-sequential-diagram l → inverse-sequential-diagram l + {l : Level} → ℕ → inverse-sequential-diagram l → inverse-sequential-diagram l iterated-right-shift-inverse-sequential-diagram n = iterate n right-shift-inverse-sequential-diagram ``` diff --git a/src/foundation/iterating-families-of-maps.lagda.md b/src/foundation/iterating-families-of-maps.lagda.md new file mode 100644 index 0000000000..97b4fa1ce6 --- /dev/null +++ b/src/foundation/iterating-families-of-maps.lagda.md @@ -0,0 +1,116 @@ +# Iterating families of maps over a map + +```agda +module foundation.iterating-families-of-maps where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.exponentiation-natural-numbers +open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.multiplicative-monoid-of-natural-numbers +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-higher-identifications-functions +open import foundation.action-on-identifications-dependent-functions +open import foundation.action-on-identifications-functions +open import foundation.dependent-homotopies +open import foundation.dependent-identifications +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.iterating-functions +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import foundation-core.commuting-squares-of-maps +open import foundation-core.endomorphisms +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.sets + +open import group-theory.monoid-actions +``` + +
+ +## Idea + +Given a family of maps `g : (x : X) → C x → C (f x)` over a map `f : X → X`, +then `g` can be +{{#concept "iterated" Disambiguation="family of maps over a map of types" Agda=iterate-family-of-maps}} +by repeatedly applying `g`. + +## Definition + +### Iterating dependent functions + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {C : X → UU l2} {f : X → X} + where + + iterate-family-of-maps : + (k : ℕ) → ((x : X) → C x → C (f x)) → (x : X) → C x → C (iterate k f x) + iterate-family-of-maps zero-ℕ g x y = y + iterate-family-of-maps (succ-ℕ k) g x y = + g (iterate k f x) (iterate-family-of-maps k g x y) + + iterate-family-of-maps' : + (k : ℕ) → ((x : X) → C x → C (f x)) → (x : X) → C x → C (iterate' k f x) + iterate-family-of-maps' zero-ℕ g x y = y + iterate-family-of-maps' (succ-ℕ k) g x y = + iterate-family-of-maps' k g (f x) (g x y) +``` + +## Properties + +### The two definitions of iterating dependent functions are homotopic + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {C : X → UU l2} {f : X → X} + where + + reassociate-iterate-family-of-maps-succ-ℕ : + (k : ℕ) (g : (x : X) → C x → C (f x)) (x : X) (y : C x) → + dependent-identification C + ( reassociate-iterate-succ-ℕ k f x) + ( g (iterate k f x) (iterate-family-of-maps k g x y)) + ( iterate-family-of-maps k g (f x) (g x y)) + reassociate-iterate-family-of-maps-succ-ℕ zero-ℕ g x y = refl + reassociate-iterate-family-of-maps-succ-ℕ (succ-ℕ k) g x y = + equational-reasoning + tr C + ( reassociate-iterate-succ-ℕ (succ-ℕ k) f x) + ( g (iterate (succ-ℕ k) f x) (iterate-family-of-maps (succ-ℕ k) g x y)) + = + g ( iterate k f (f x)) + ( tr C + ( reassociate-iterate-succ-ℕ k f x) + ( g (iterate k f x) (iterate-family-of-maps k g x y))) + by + tr-ap f g + ( reassociate-iterate-succ-ℕ k f x) + ( iterate-family-of-maps (succ-ℕ k) g x y) + = g (iterate k f (f x)) (iterate-family-of-maps k g (f x) (g x y)) + by + ap + ( g (iterate k f (f x))) + ( reassociate-iterate-family-of-maps-succ-ℕ k g x y) + + reassociate-iterate-family-of-maps : + (k : ℕ) (g : (x : X) → C x → C (f x)) (x : X) (y : C x) → + dependent-identification C + ( reassociate-iterate k f x) + ( iterate-family-of-maps k g x y) + ( iterate-family-of-maps' k g x y) + reassociate-iterate-family-of-maps zero-ℕ g x y = refl + reassociate-iterate-family-of-maps (succ-ℕ k) g x y = + concat-dependent-identification C + ( reassociate-iterate-succ-ℕ k f x) + ( reassociate-iterate k f (f x)) + ( reassociate-iterate-family-of-maps-succ-ℕ k g x y) + ( reassociate-iterate-family-of-maps k g (f x) (g x y)) +``` diff --git a/src/foundation/iterating-functions.lagda.md b/src/foundation/iterating-functions.lagda.md index edf0a3ddd1..339d4eed0c 100644 --- a/src/foundation/iterating-functions.lagda.md +++ b/src/foundation/iterating-functions.lagda.md @@ -85,15 +85,16 @@ module _ {l : Level} {X : UU l} where - iterate-succ-ℕ : + reassociate-iterate-succ-ℕ : (k : ℕ) (f : X → X) (x : X) → iterate (succ-ℕ k) f x = iterate k f (f x) - iterate-succ-ℕ zero-ℕ f x = refl - iterate-succ-ℕ (succ-ℕ k) f x = ap f (iterate-succ-ℕ k f x) + reassociate-iterate-succ-ℕ zero-ℕ f x = refl + reassociate-iterate-succ-ℕ (succ-ℕ k) f x = + ap f (reassociate-iterate-succ-ℕ k f x) reassociate-iterate : (k : ℕ) (f : X → X) → iterate k f ~ iterate' k f reassociate-iterate zero-ℕ f x = refl reassociate-iterate (succ-ℕ k) f x = - iterate-succ-ℕ k f x ∙ reassociate-iterate k f (f x) + reassociate-iterate-succ-ℕ k f x ∙ reassociate-iterate k f (f x) ``` ### For any map `f : X → X`, iterating `f` defines a monoid action of ℕ on `X` @@ -108,7 +109,8 @@ module _ iterate (k +ℕ l) f x = iterate k f (iterate l f x) iterate-add-ℕ k zero-ℕ f x = refl iterate-add-ℕ k (succ-ℕ l) f x = - ap f (iterate-add-ℕ k l f x) ∙ iterate-succ-ℕ k f (iterate l f x) + ap f (iterate-add-ℕ k l f x) ∙ + reassociate-iterate-succ-ℕ k f (iterate l f x) left-unit-law-iterate-add-ℕ : (l : ℕ) (f : X → X) (x : X) → @@ -140,7 +142,7 @@ module _ iterate-mul-ℕ (succ-ℕ k) l f x = ( iterate-add-ℕ (k *ℕ l) l f x) ∙ ( ( iterate-mul-ℕ k l f (iterate l f x)) ∙ - ( inv (iterate-succ-ℕ k (iterate l f) x))) + ( inv (reassociate-iterate-succ-ℕ k (iterate l f) x))) iterate-exp-ℕ : (k l : ℕ) (f : X → X) (x : X) → @@ -149,7 +151,7 @@ module _ iterate-exp-ℕ (succ-ℕ k) l f x = ( iterate-mul-ℕ (exp-ℕ l k) l f x) ∙ ( ( iterate-exp-ℕ k l (iterate l f) x) ∙ - ( inv (htpy-eq (iterate-succ-ℕ k (iterate l) f) x))) + ( inv (htpy-eq (reassociate-iterate-succ-ℕ k (iterate l) f) x))) module _ {l : Level} (X : Set l) diff --git a/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md b/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md index 794b939f5a..515f06b8ce 100644 --- a/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md +++ b/src/foundation/morphisms-inverse-sequential-diagrams.lagda.md @@ -48,50 +48,50 @@ the form ### Morphisms of inverse sequential diagrams of types ```agda -naturality-hom-inverse-sequential-diagram : +module _ {l1 l2 : Level} (A : inverse-sequential-diagram l1) (B : inverse-sequential-diagram l2) - (h : - (n : ℕ) → - family-inverse-sequential-diagram A n → - family-inverse-sequential-diagram B n) - (n : ℕ) → UU (l1 ⊔ l2) -naturality-hom-inverse-sequential-diagram A B = - naturality-section-dependent-inverse-sequential-diagram A - ( const-dependent-inverse-sequential-diagram A B) + where -hom-inverse-sequential-diagram : - {l1 l2 : Level} - (A : inverse-sequential-diagram l1) - (B : inverse-sequential-diagram l2) → - UU (l1 ⊔ l2) -hom-inverse-sequential-diagram A B = - section-dependent-inverse-sequential-diagram A - ( const-dependent-inverse-sequential-diagram A B) + naturality-hom-inverse-sequential-diagram : + (h : + (n : ℕ) → + family-inverse-sequential-diagram A n → + family-inverse-sequential-diagram B n) → + UU (l1 ⊔ l2) + naturality-hom-inverse-sequential-diagram = + naturality-section-dependent-inverse-sequential-diagram A + ( const-dependent-inverse-sequential-diagram A B) + + hom-inverse-sequential-diagram : UU (l1 ⊔ l2) + hom-inverse-sequential-diagram = + section-dependent-inverse-sequential-diagram A + ( const-dependent-inverse-sequential-diagram A B) module _ {l1 l2 : Level} (A : inverse-sequential-diagram l1) (B : inverse-sequential-diagram l2) + (f : hom-inverse-sequential-diagram A B) where map-hom-inverse-sequential-diagram : - hom-inverse-sequential-diagram A B → (n : ℕ) → + (n : ℕ) → family-inverse-sequential-diagram A n → family-inverse-sequential-diagram B n map-hom-inverse-sequential-diagram = map-section-dependent-inverse-sequential-diagram A ( const-dependent-inverse-sequential-diagram A B) + ( f) naturality-map-hom-inverse-sequential-diagram : - (f : hom-inverse-sequential-diagram A B) (n : ℕ) → naturality-hom-inverse-sequential-diagram A B - ( map-hom-inverse-sequential-diagram f) - ( n) + ( map-hom-inverse-sequential-diagram) naturality-map-hom-inverse-sequential-diagram = naturality-map-section-dependent-inverse-sequential-diagram A ( const-dependent-inverse-sequential-diagram A B) + ( f) ``` ### Identity morphism on inverse sequential diagrams of types @@ -107,39 +107,38 @@ pr2 (id-hom-inverse-sequential-diagram A) n = refl-htpy ### Composition of morphisms of inverse sequential diagrams of types ```agda -map-comp-hom-inverse-sequential-diagram : - {l : Level} (A B C : inverse-sequential-diagram l) → - hom-inverse-sequential-diagram B C → hom-inverse-sequential-diagram A B → - (n : ℕ) → - family-inverse-sequential-diagram A n → family-inverse-sequential-diagram C n -map-comp-hom-inverse-sequential-diagram A B C g f n = - map-hom-inverse-sequential-diagram B C g n ∘ - map-hom-inverse-sequential-diagram A B f n - -naturality-comp-hom-inverse-sequential-diagram : - {l : Level} (A B C : inverse-sequential-diagram l) - (g : hom-inverse-sequential-diagram B C) - (f : hom-inverse-sequential-diagram A B) - (n : ℕ) → - naturality-hom-inverse-sequential-diagram A C - ( map-comp-hom-inverse-sequential-diagram A B C g f) - ( n) -naturality-comp-hom-inverse-sequential-diagram A B C g f n x = - ( ap - ( map-hom-inverse-sequential-diagram B C g n) - ( naturality-map-hom-inverse-sequential-diagram A B f n x)) ∙ - ( naturality-map-hom-inverse-sequential-diagram B C g n - ( map-hom-inverse-sequential-diagram A B f (succ-ℕ n) x)) - -comp-hom-inverse-sequential-diagram : - {l : Level} (A B C : inverse-sequential-diagram l) → - hom-inverse-sequential-diagram B C → - hom-inverse-sequential-diagram A B → - hom-inverse-sequential-diagram A C -pr1 (comp-hom-inverse-sequential-diagram A B C g f) = - map-comp-hom-inverse-sequential-diagram A B C g f -pr2 (comp-hom-inverse-sequential-diagram A B C g f) = - naturality-comp-hom-inverse-sequential-diagram A B C g f +module _ + {l1 l2 l3 : Level} + ( A : inverse-sequential-diagram l1) + ( B : inverse-sequential-diagram l2) + ( C : inverse-sequential-diagram l3) + ( g : hom-inverse-sequential-diagram B C) + ( f : hom-inverse-sequential-diagram A B) + where + + map-comp-hom-inverse-sequential-diagram : + (n : ℕ) → + family-inverse-sequential-diagram A n → + family-inverse-sequential-diagram C n + map-comp-hom-inverse-sequential-diagram n = + map-hom-inverse-sequential-diagram B C g n ∘ + map-hom-inverse-sequential-diagram A B f n + + naturality-comp-hom-inverse-sequential-diagram : + naturality-hom-inverse-sequential-diagram A C + ( map-comp-hom-inverse-sequential-diagram) + naturality-comp-hom-inverse-sequential-diagram n x = + ( ap + ( map-hom-inverse-sequential-diagram B C g n) + ( naturality-map-hom-inverse-sequential-diagram A B f n x)) ∙ + ( naturality-map-hom-inverse-sequential-diagram B C g n + ( map-hom-inverse-sequential-diagram A B f (succ-ℕ n) x)) + + comp-hom-inverse-sequential-diagram : + hom-inverse-sequential-diagram A C + comp-hom-inverse-sequential-diagram = + map-comp-hom-inverse-sequential-diagram , + naturality-comp-hom-inverse-sequential-diagram ``` ## Properties @@ -158,8 +157,9 @@ module _ ((n : ℕ) → map-hom-inverse-sequential-diagram A B f n ~ map-hom-inverse-sequential-diagram A B g n) → - (n : ℕ) → UU (l1 ⊔ l2) - coherence-htpy-hom-inverse-sequential-diagram f g H n = + UU (l1 ⊔ l2) + coherence-htpy-hom-inverse-sequential-diagram f g H = + (n : ℕ) → ( naturality-map-hom-inverse-sequential-diagram A B f n ∙h map-inverse-sequential-diagram B n ·l H (succ-ℕ n)) ~ ( H n ·r map-inverse-sequential-diagram A n ∙h @@ -171,7 +171,7 @@ module _ Σ ( (n : ℕ) → map-hom-inverse-sequential-diagram A B f n ~ map-hom-inverse-sequential-diagram A B g n) - ( λ H → (n : ℕ) → coherence-htpy-hom-inverse-sequential-diagram f g H n) + ( coherence-htpy-hom-inverse-sequential-diagram f g) refl-htpy-hom-inverse-sequential-diagram : (f : hom-inverse-sequential-diagram A B) → @@ -193,11 +193,9 @@ module _ ( is-torsorial-binary-htpy (map-hom-inverse-sequential-diagram A B f)) ( map-hom-inverse-sequential-diagram A B f , refl-binary-htpy (map-hom-inverse-sequential-diagram A B f)) - ( is-torsorial-Eq-Π + ( is-torsorial-binary-htpy ( λ n → - is-torsorial-htpy - ( naturality-map-hom-inverse-sequential-diagram A B f n ∙h - refl-htpy))) + naturality-map-hom-inverse-sequential-diagram A B f n ∙h refl-htpy)) is-equiv-htpy-eq-hom-inverse-sequential-diagram : (f g : hom-inverse-sequential-diagram A B) → diff --git a/src/foundation/multivariable-correspondences.lagda.md b/src/foundation/multivariable-correspondences.lagda.md index 9d753057aa..817901c593 100644 --- a/src/foundation/multivariable-correspondences.lagda.md +++ b/src/foundation/multivariable-correspondences.lagda.md @@ -19,8 +19,7 @@ open import univalent-combinatorics.standard-finite-types ## Idea Consider a family of types `A` indexed by `Fin n`. An `n`-ary correspondence of -tuples `(x₁, …, xₙ)` where `x_i : A_i` is a type family over -`(i : Fin n) → A i`. +tuples `(x₁, …, xₙ)` where `xᵢ : A i` is a type family over `(i : Fin n) → A i`. ## Definition