# Homotopies of binary operations

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

Created on 2023-02-13.

module foundation.binary-homotopies where

Imports
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.function-extensionality
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopy-induction
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.torsorial-type-families


## Idea

Consider two binary operations f g : (x : A) (y : B x) → C x y. The type of binary homotopies between f and g is defined to be the type of pointwise identifications of f and g. We show that this characterizes the identity type of (x : A) (y : B x) → C x y.

## Definition

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
where

binary-htpy :
(f g : (x : A) (y : B x) → C x y) → UU (l1 ⊔ l2 ⊔ l3)
binary-htpy f g = (x : A) → f x ~ g x

refl-binary-htpy : (f : (x : A) (y : B x) → C x y) → binary-htpy f f
refl-binary-htpy f x = refl-htpy

binary-htpy-eq :
(f g : (x : A) (y : B x) → C x y) → (f ＝ g) → binary-htpy f g
binary-htpy-eq f .f refl = refl-binary-htpy f

is-torsorial-binary-htpy :
(f : (x : A) (y : B x) → C x y) →
is-torsorial (binary-htpy f)
is-torsorial-binary-htpy f =
is-torsorial-Eq-Π (λ x → is-torsorial-htpy (f x))

is-equiv-binary-htpy-eq :
(f g : (x : A) (y : B x) → C x y) → is-equiv (binary-htpy-eq f g)
is-equiv-binary-htpy-eq f =
fundamental-theorem-id
( is-torsorial-binary-htpy f)
( binary-htpy-eq f)

extensionality-binary-Π :
(f g : (x : A) (y : B x) → C x y) → (f ＝ g) ≃ binary-htpy f g
pr1 (extensionality-binary-Π f g) = binary-htpy-eq f g
pr2 (extensionality-binary-Π f g) = is-equiv-binary-htpy-eq f g

eq-binary-htpy :
(f g : (x : A) (y : B x) → C x y) → binary-htpy f g → f ＝ g
eq-binary-htpy f g = map-inv-equiv (extensionality-binary-Π f g)


## Properties

### Binary homotopy is equivalent to function homotopy

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
where

binary-htpy-htpy :
(f g : (x : A) (y : B x) → C x y) → (f ~ g) → binary-htpy f g
binary-htpy-htpy f g =
ind-htpy f (λ g H → binary-htpy f g) (refl-binary-htpy f)

equiv-binary-htpy-htpy :
(f g : (x : A) (y : B x) → C x y) → (f ~ g) ≃ binary-htpy f g
equiv-binary-htpy-htpy f g = extensionality-binary-Π f g ∘e equiv-eq-htpy

htpy-binary-htpy :
(f g : (x : A) (y : B x) → C x y) → binary-htpy f g → f ~ g
htpy-binary-htpy f g = map-inv-equiv (equiv-binary-htpy-htpy f g)

equiv-htpy-binary-htpy :
(f g : (x : A) (y : B x) → C x y) → binary-htpy f g ≃ (f ~ g)
equiv-htpy-binary-htpy f g = inv-equiv (equiv-binary-htpy-htpy f g)