# Binary transport

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

Created on 2023-01-28.

module foundation.binary-transport where

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

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.transport-along-identifications


## Idea

Given a binary relation B : A → A → UU and identifications p : x ＝ x' and q : y ＝ y' in A, the binary transport of B is an operation

  binary-tr B p q : B x y → B x' y'


## Definition

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

binary-tr : (p : x ＝ x') (q : y ＝ y') → C x y → C x' y'
binary-tr refl refl = id

is-equiv-binary-tr : (p : x ＝ x') (q : y ＝ y') → is-equiv (binary-tr p q)
is-equiv-binary-tr refl refl = is-equiv-id

equiv-binary-tr : (p : x ＝ x') (q : y ＝ y') → C x y ≃ C x' y'
pr1 (equiv-binary-tr p q) = binary-tr p q
pr2 (equiv-binary-tr p q) = is-equiv-binary-tr p q

compute-binary-tr :
(p : x ＝ x') (q : y ＝ y') (u : C x y) →
tr (λ a → C a y') p (tr (C x) q u) ＝ binary-tr p q u
compute-binary-tr refl refl u = refl

compute-binary-tr' :
(p : x ＝ x') (q : y ＝ y') (u : C x y) →
tr (C x') q (tr (λ a → C a y) p u) ＝ binary-tr p q u
compute-binary-tr' refl refl u = refl


## Properties

### Transposing binary path-overs

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

transpose-binary-path-over :
{x1 x2 : A} (p : x1 ＝ x2) {y1 y2 : B} (q : y1 ＝ y2)
{c1 : C x1 y1} {c2 : C x2 y2} →
c2 ＝ binary-tr C p q c1 → binary-tr C (inv p) (inv q) c2 ＝ c1
transpose-binary-path-over refl refl = id

transpose-binary-path-over' :
{x1 x2 : A} (p : x1 ＝ x2) {y1 y2 : B} (q : y1 ＝ y2)
{c1 : C x1 y1} {c2 : C x2 y2} →
c1 ＝ binary-tr C (inv p) (inv q) c2 → binary-tr C p q c1 ＝ c2
transpose-binary-path-over' refl refl = id


### Binary transport along concatenated paths

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

binary-tr-concat :
{x1 x2 x3 : A} (p : x1 ＝ x2) (p' : x2 ＝ x3)
{y1 y2 y3 : B} (q : y1 ＝ y2) (q' : y2 ＝ y3) →
(c : C x1 y1) →
binary-tr C (p ∙ p') (q ∙ q') c ＝
binary-tr C p' q' (binary-tr C p q c)
binary-tr-concat refl refl refl refl c = refl


### Binary transport along paths of the form ap f p and ap g q

module _
{l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
{E : A → C → UU l5} (F : B → D → UU l6)
{f : A → B} {g : C → D} (h : (a : A) (c : C) → E a c → F (f a) (g c))
where

binary-tr-ap :
{x x' : A} (p : x ＝ x') {y y' : C} (q : y ＝ y') →
{u : E x y} {v : E x' y'} (r : binary-tr E p q u ＝ v) →
binary-tr F (ap f p) (ap g q) (h x y u) ＝ h x' y' v
binary-tr-ap refl refl refl = refl