Skip to content

Commit

Permalink
Improve generality of homotopy whiskering operations (#976)
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@fredrik-bakke
fredrik-bakke authored Dec 7, 2023
1 parent fa40692 commit ab24893
Show file tree
Hide file tree
Showing 2 changed files with 149 additions and 81 deletions.
38 changes: 20 additions & 18 deletions MIXFIX-OPERATORS.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 `_→_` |
192 changes: 129 additions & 63 deletions src/foundation-core/whiskering-homotopies.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
```

Expand All @@ -96,95 +109,117 @@ 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
```

### Laws for whiskering an inverted homotopy

```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
Expand All @@ -194,26 +229,57 @@ 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
```

### Whiskering whiskerings

```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
```

0 comments on commit ab24893

Please sign in to comment.