# The interchange law

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-01-27.
Last modified on 2023-06-10.

module foundation.interchange-law where

Imports
open import foundation.action-on-identifications-functions
open import foundation.universe-levels

open import foundation-core.identity-types


## Idea

The interchange law shows up in many variations in type theory. The interchange law for Σ-types is useful in characterizations of identity types; the interchange law for higher identity types is used in the Eckmann-Hilton argument to show that the higher homotopy groups of a type are abelian, and the interchange law for binary operations in rings are useful in computations. We first define a fully generalized interchange law, and then we specialize it to make it more directly applicable.

## Definition

### The fully generalized interchange law

module _
{l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level}
{A : UU l1} {B : A → UU l2} {C : A → UU l3} {D : (a : A) → B a → C a → UU l4}
{X1 : UU l5} {Y1 : X1 → UU l6} {X2 : UU l7} {Y2 : X2 → UU l8}
{Z : UU l9} (R : Z → Z → UU l10)
(μ1 : (a : A) → B a → X1)
(μ2 : (a : A) (b : B a) (c : C a) → D a b c → Y1 (μ1 a b))
(μ3 : (x : X1) → Y1 x → Z)
(μ4 : (a : A) → C a → X2)
(μ5 : (a : A) (c : C a) (b : B a) → D a b c → Y2 (μ4 a c))
(μ6 : (x : X2) → Y2 x → Z)
where

fully-generalized-interchange-law : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l10)
fully-generalized-interchange-law =
(a : A) (b : B a) (c : C a) (d : D a b c) →
R (μ3 (μ1 a b) (μ2 a b c d)) (μ6 (μ4 a c) (μ5 a c b d))


### The interchange law for two binary operations on a type

module _
{l : Level} {X : UU l} (μ : X → X → X)
where

interchange-law : (X → X → X) → UU l
interchange-law ν = (x y u v : X) → μ (ν x y) (ν u v) ＝ ν (μ x u) (μ y v)

interchange-law-commutative-and-associative :
((x y : X) → μ x y ＝ μ y x) → ((x y z : X) → μ (μ x y) z ＝ μ x (μ y z)) →
interchange-law μ
interchange-law-commutative-and-associative C A x y u v =
( A x y (μ u v)) ∙
( ( ap
( μ x)
( (inv (A y u v)) ∙ ((ap (λ z → μ z v) (C y u)) ∙ (A u y v)))) ∙
( inv (A x u (μ y v))))