From ab24893bde8c146808f7d79c311b01a381418e35 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 8 Dec 2023 00:24:35 +0100 Subject: [PATCH] Improve generality of homotopy whiskering operations (#976) This PR improves the generality of the homotopy whiskering operations by introducing more possible type dependencies into the definitions. Moreover, it bumps the precedence of both whiskering operators, so that in particular left whiskering takes precedence over right whiskering. These two operators commute definitionally, so it doesn't matter which way we associate them, and Agda is usually indecisive with which way to print them when you ask it to. The downside to this change is that Agda will start omitting parentheses when written together with homotopy concatenations, so maybe this is a change for the worse. --- MIXFIX-OPERATORS.md | 38 ++-- .../whiskering-homotopies.lagda.md | 192 ++++++++++++------ 2 files changed, 149 insertions(+), 81 deletions(-) diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md index a6d246d6c4..aa6021c8ef 100644 --- a/MIXFIX-OPERATORS.md +++ b/MIXFIX-OPERATORS.md @@ -153,7 +153,7 @@ Below, we outline a list of general rules when assigning associativities. associated regardless. For instance, one should never write ```agda - assoc : p ∙ (q ∙ r) ＝ p ∙ q ∙ r + assoc : p ∙ q ∙ r ＝ p ∙ (q ∙ r) ``` - **Unique well-typed associativity**. When an operator only has one well-typed @@ -163,20 +163,22 @@ Below, we outline a list of general rules when assigning associativities. ## Full table of assigned precedences -| Precedence level | Operators | -| ---------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | -| 50 | Unary non-parametric operators. This class is currently empty | -| 45 | Exponentiative arithmetic operators | -| 40 | Multiplicative arithmetic operators | -| 36 | Subtractive arithmetic operators | -| 35 | Additive arithmetic operators | -| 30 | Relational arithmetic operators like`_≤-ℕ_` and `_<-ℕ_` | -| 25 | Parametric unary operators. This class is currently empty | -| 20 | Parametric exponentiative operators. This class is currently empty | -| 15 | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, identification concatenation and whiskering operators like `_∙_`, `_∙h_`, `_·l_`, and `_·r_` | -| 10 | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad | -| 6 | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, and `_↔_`, elementhood relations, subtype relations | -| 5 | Directed function type-like formation operators, e.g. `_→∗_` and `_↪_` | -| 3 | The pairing operators `_,_` and `_,ω_` | -| 0-1 | Reasoning syntaxes | -| -∞ | Function type formation `_→_` | +| Precedence level | Operators | +| ---------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| 50 | Unary non-parametric operators. This class is currently empty | +| 45 | Exponentiative arithmetic operators | +| 40 | Multiplicative arithmetic operators | +| 36 | Subtractive arithmetic operators | +| 35 | Additive arithmetic operators | +| 30 | Relational arithmetic operators like`_≤-ℕ_` and `_<-ℕ_` | +| 25 | Parametric unary operators. This class is currently empty | +| 20 | Parametric exponentiative operators. This class is currently empty | +| 17 | Left homotopy whiskering `_·l_` | +| 16 | Right homotopy whiskering `_·r_` | +| 15 | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, concatenation operators like `_∙_` and `_∙h_` | +| 10 | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad | +| 6 | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, and `_↔_`, elementhood relations, subtype relations | +| 5 | Directed function type-like formation operators, e.g. `_→∗_` and `_↪_` | +| 3 | The pairing operators `_,_` and `_,ω_` | +| 0-1 | Reasoning syntaxes | +| -∞ | Function type formation `_→_` | diff --git a/src/foundation-core/whiskering-homotopies.lagda.md b/src/foundation-core/whiskering-homotopies.lagda.md index e79337e4b3..29803206ab 100644 --- a/src/foundation-core/whiskering-homotopies.lagda.md +++ b/src/foundation-core/whiskering-homotopies.lagda.md @@ -51,38 +51,51 @@ font. For more details, see [How to install](HOWTO-INSTALL.md). ## Definitions -### Whiskering of homotopies +### Left whiskering of homotopies ```agda -htpy-left-whisk : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} - (h : B → C) {f g : A → B} → f ~ g → (h ∘ f) ~ (h ∘ g) -htpy-left-whisk h H x = ap h (H x) +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + where + + htpy-left-whisk : + (h : {x : A} → B x → C x) + {f g : (x : A) → B x} → f ~ g → h ∘ f ~ h ∘ g + htpy-left-whisk h H x = ap h (H x) -infixr 15 _·l_ -_·l_ = htpy-left-whisk + infixr 17 _·l_ + _·l_ = htpy-left-whisk +``` -htpy-right-whisk : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : B → UU l3} - {g h : (y : B) → C y} (H : g ~ h) (f : A → B) → (g ∘ f) ~ (h ∘ f) -htpy-right-whisk H f x = H (f x) +### Right whiskering of homotopies -infixl 15 _·r_ -_·r_ = htpy-right-whisk +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + where + + htpy-right-whisk : + {g h : {x : A} (y : B x) → C x y} + (H : {x : A} → g {x} ~ h {x}) + (f : (x : A) → B x) → g ∘ f ~ h ∘ f + htpy-right-whisk H f x = H (f x) + + infixl 16 _·r_ + _·r_ = htpy-right-whisk ``` ### Horizontal composition of homotopies ```agda module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} - {f f' : A → B} {g g' : B → C} + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + {f f' : (x : A) → B x} {g g' : {x : A} → B x → C x} where - htpy-comp-horizontal : (f ~ f') → (g ~ g') → (g ∘ f) ~ (g' ∘ f') + htpy-comp-horizontal : f ~ f' → ({x : A} → g {x} ~ g' {x}) → g ∘ f ~ g' ∘ f' htpy-comp-horizontal F G = (g ·l F) ∙h (G ·r f') - htpy-comp-horizontal' : (f ~ f') → (g ~ g') → (g ∘ f) ~ (g' ∘ f') + htpy-comp-horizontal' : f ~ f' → ({x : A} → g {x} ~ g' {x}) → g ∘ f ~ g' ∘ f' htpy-comp-horizontal' F G = (G ·r f) ∙h (g' ·l F) ``` @@ -96,23 +109,37 @@ homotopy side. ```agda module _ - { l1 l2 : Level} {A : UU l1} {B : UU l2} + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where - left-unit-law-left-whisk-htpy : {f f' : A → B} → (H : f ~ f') → id ·l H ~ H + left-unit-law-left-whisk-htpy : + {f f' : (x : A) → B x} → (H : f ~ f') → id ·l H ~ H left-unit-law-left-whisk-htpy H x = ap-id (H x) +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + where + right-unit-law-left-whisk-htpy : - { l3 : Level} {C : UU l3} {f : A → B} (g : B → C) → + {f : (x : A) → B x} (g : {x : A} → B x → C x) → g ·l refl-htpy {f = f} ~ refl-htpy right-unit-law-left-whisk-htpy g = refl-htpy +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + where + left-unit-law-right-whisk-htpy : - {l3 : Level} {C : UU l3} {g : B → C} (f : A → B) → + {g : {x : A} (y : B x) → C x y} (f : (x : A) → B x) → refl-htpy {f = g} ·r f ~ refl-htpy left-unit-law-right-whisk-htpy f = refl-htpy - right-unit-law-right-whisk-htpy : {f f' : A → B} → (H : f ~ f') → H ·r id ~ H +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + right-unit-law-right-whisk-htpy : + {f f' : (x : A) → B x} → (H : f ~ f') → H ·r id ~ H right-unit-law-right-whisk-htpy H = refl-htpy ``` @@ -120,71 +147,79 @@ module _ ```agda module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + {f f' : (x : A) → B x} (g : {x : A} → B x → C x) (H : f ~ f') where - left-whisk-inv-htpy : - {f f' : A → B} (g : B → C) (H : f ~ f') → - (g ·l (inv-htpy H)) ~ inv-htpy (g ·l H) - left-whisk-inv-htpy g H x = ap-inv g (H x) + left-whisk-inv-htpy : g ·l (inv-htpy H) ~ inv-htpy (g ·l H) + left-whisk-inv-htpy x = ap-inv g (H x) - inv-htpy-left-whisk-inv-htpy : - {f f' : A → B} (g : B → C) (H : f ~ f') → - inv-htpy (g ·l H) ~ (g ·l (inv-htpy H)) - inv-htpy-left-whisk-inv-htpy g H = - inv-htpy (left-whisk-inv-htpy g H) + inv-htpy-left-whisk-inv-htpy : inv-htpy (g ·l H) ~ g ·l (inv-htpy H) + inv-htpy-left-whisk-inv-htpy = inv-htpy left-whisk-inv-htpy - right-whisk-inv-htpy : - {g g' : B → C} (H : g ~ g') (f : A → B) → - ((inv-htpy H) ·r f) ~ (inv-htpy (H ·r f)) - right-whisk-inv-htpy H f = refl-htpy +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + {g g' : {x : A} (y : B x) → C x y} (H : {x : A} → g {x} ~ g' {x}) + (f : (x : A) → B x) + where - inv-htpy-right-whisk-inv-htpy : - {g g' : B → C} (H : g ~ g') (f : A → B) → - ((inv-htpy H) ·r f) ~ (inv-htpy (H ·r f)) - inv-htpy-right-whisk-inv-htpy H f = - inv-htpy (right-whisk-inv-htpy H f) + right-whisk-inv-htpy : inv-htpy H ·r f ~ inv-htpy (H ·r f) + right-whisk-inv-htpy = refl-htpy + + inv-htpy-right-whisk-inv-htpy : inv-htpy H ·r f ~ inv-htpy (H ·r f) + inv-htpy-right-whisk-inv-htpy = inv-htpy right-whisk-inv-htpy ``` ### Distributivity of whiskering over composition of homotopies ```agda module _ - { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} where distributive-left-whisk-concat-htpy : - { f g h : A → B} (k : B → C) → + { f g h : (x : A) → B x} (k : {x : A} → B x → C x) → ( H : f ~ g) (K : g ~ h) → - ( k ·l (H ∙h K)) ~ ((k ·l H) ∙h (k ·l K)) + k ·l (H ∙h K) ~ (k ·l H) ∙h (k ·l K) distributive-left-whisk-concat-htpy k H K a = ap-concat k (H a) (K a) +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + (k : (x : A) → B x) {f g h : {x : A} (y : B x) → C x y} + (H : {x : A} → f {x} ~ g {x}) (K : {x : A} → g {x} ~ h {x}) + where + distributive-right-whisk-concat-htpy : - ( k : A → B) {f g h : B → C} → - ( H : f ~ g) (K : g ~ h) → - ( (H ∙h K) ·r k) ~ ((H ·r k) ∙h (K ·r k)) - distributive-right-whisk-concat-htpy k H K = refl-htpy + (H ∙h K) ·r k ~ (H ·r k) ∙h (K ·r k) + distributive-right-whisk-concat-htpy = refl-htpy ``` ### Associativity of whiskering and function composition ```agda module _ - { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : A → UU l2} {C : A → UU l3} {D : A → UU l4} where associative-left-whisk-comp : - ( k : C → D) (h : B → C) {f g : A → B} → + ( k : {x : A} → C x → D x) (h : {x : A} → B x → C x) {f g : (x : A) → B x} ( H : f ~ g) → - ( k ·l (h ·l H)) ~ ((k ∘ h) ·l H) + k ·l (h ·l H) ~ (k ∘ h) ·l H associative-left-whisk-comp k h H x = inv (ap-comp k h (H x)) - associative-right-whisk-comp : - { f g : C → D} (h : B → C) (k : A → B) → - ( H : f ~ g) → - ( (H ·r h) ·r k) ~ (H ·r (h ∘ k)) - associative-right-whisk-comp h k H = refl-htpy +module _ + { l1 l2 l3 l4 : Level} + { A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + { D : (x : A) (y : B x) (z : C x y) → UU l4} + { f g : {x : A} {y : B x} (z : C x y) → D x y z} + ( h : {x : A} (y : B x) → C x y) (k : (x : A) → B x) + ( H : {x : A} {y : B x} → f {x} {y} ~ g {x} {y}) + where + + associative-right-whisk-comp : (H ·r h) ·r k ~ H ·r (h ∘ k) + associative-right-whisk-comp = refl-htpy ``` ### A coherence for homotopies to the identity function @@ -194,10 +229,10 @@ module _ {l : Level} {A : UU l} {f : A → A} (H : f ~ id) where - coh-htpy-id : (H ·r f) ~ (f ·l H) + coh-htpy-id : H ·r f ~ f ·l H coh-htpy-id x = is-injective-concat' (H x) (nat-htpy-id H (H x)) - inv-htpy-coh-htpy-id : (f ·l H) ~ (H ·r f) + inv-htpy-coh-htpy-id : f ·l H ~ H ·r f inv-htpy-coh-htpy-id = inv-htpy coh-htpy-id ``` @@ -205,15 +240,46 @@ module _ ```agda module _ - { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} - { f g : A → B} + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + {f g : (x : A) → B x} where ap-left-whisk-htpy : - ( h : B → C) {H H' : f ~ g} (α : H ~ H') → h ·l H ~ h ·l H' - ap-left-whisk-htpy h α x = ap (ap h) (α x) + (h : {x : A} → B x → C x) {H H' : f ~ g} (α : H ~ H') → h ·l H ~ h ·l H' + ap-left-whisk-htpy h α = (ap h) ·l α + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + {f g : {x : A} (y : B x) → C x y} {H H' : {x : A} → f {x} ~ g {x}} + where ap-right-whisk-htpy : - { H H' : f ~ g} (α : H ~ H') (h : C → A) → H ·r h ~ H' ·r h + (α : {x : A} → H {x} ~ H' {x}) (h : (x : A) → B x) → H ·r h ~ H' ·r h ap-right-whisk-htpy α h = α ·r h ``` + +### The left and right whiskering operations commute + +We have the coherence + +```text + (h ·l H) ·r h' ~ h ·l (H ·r h') +``` + +and, in fact, this equation holds definitionally. + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : A → UU l2} + {C : {x : A} → B x → UU l3} {D : {x : A} → B x → UU l4} + {f g : {x : A} (y : B x) → C y} + where + + coherence-left-right-whisk-htpy : + (h : {x : A} {y : B x} → C y → D y) + (H : {x : A} → f {x} ~ g {x}) + (h' : (x : A) → B x) → + (h ·l H) ·r h' ~ h ·l (H ·r h') + coherence-left-right-whisk-htpy h H h' = refl-htpy +```