# Binary reflecting maps of equivalence relations

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2023-02-13.

module foundation.binary-reflecting-maps-equivalence-relations where

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

open import foundation-core.equivalence-relations
open import foundation-core.equivalences
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.torsorial-type-families


## Idea

Consider two types A and B equipped with equivalence relations R and S. A binary reflecting map from A to B to X is a binary map f : A → B → X such that for any to R-related elements x and x' in A and any two S-related elements y and y' in B we have f x y ＝ f x' y' in X.

module _
{l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2}
(R : equivalence-relation l3 A) (S : equivalence-relation l4 B)
where

binary-reflects-equivalence-relation :
{X : UU l5} (f : A → B → X) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
binary-reflects-equivalence-relation f =
{x x' : A} {y y' : B} →
sim-equivalence-relation R x x' → sim-equivalence-relation S y y' →
f x y ＝ f x' y'

binary-reflecting-map-equivalence-relation :
(X : UU l5) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
binary-reflecting-map-equivalence-relation X =
Σ (A → B → X) binary-reflects-equivalence-relation

map-binary-reflecting-map-equivalence-relation :
{X : UU l5} → binary-reflecting-map-equivalence-relation X → A → B → X
map-binary-reflecting-map-equivalence-relation = pr1

reflects-binary-reflecting-map-equivalence-relation :
{X : UU l5} (f : binary-reflecting-map-equivalence-relation X) →
binary-reflects-equivalence-relation
( map-binary-reflecting-map-equivalence-relation f)
reflects-binary-reflecting-map-equivalence-relation = pr2

is-prop-binary-reflects-equivalence-relation :
(X : Set l5) (f : A → B → type-Set X) →
is-prop (binary-reflects-equivalence-relation f)
is-prop-binary-reflects-equivalence-relation X f =
is-prop-implicit-Π
( λ x →
is-prop-implicit-Π
( λ x' →
is-prop-implicit-Π
( λ y →
is-prop-implicit-Π
( λ y' →
is-prop-function-type
( is-prop-function-type
( is-set-type-Set X (f x y) (f x' y')))))))

binary-reflects-prop-equivalence-relation :
(X : Set l5) (f : A → B → type-Set X) → Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
pr1 (binary-reflects-prop-equivalence-relation X f) =
binary-reflects-equivalence-relation f
pr2 (binary-reflects-prop-equivalence-relation X f) =
is-prop-binary-reflects-equivalence-relation X f


### Characterizing the identity type of binary reflecting maps into sets

module _
{l1 l2 l3 l4 l5 : Level}
{A : UU l1} (R : equivalence-relation l2 A)
{B : UU l3} (S : equivalence-relation l4 B)
(C : Set l5) (f : binary-reflecting-map-equivalence-relation R S (type-Set C))
where

htpy-binary-reflecting-map-equivalence-relation :
(g : binary-reflecting-map-equivalence-relation R S (type-Set C)) →
UU (l1 ⊔ l3 ⊔ l5)
htpy-binary-reflecting-map-equivalence-relation g =
(x : A) (y : B) →
map-binary-reflecting-map-equivalence-relation R S f x y ＝
map-binary-reflecting-map-equivalence-relation R S g x y

refl-htpy-binary-reflecting-map-equivalence-relation :
htpy-binary-reflecting-map-equivalence-relation f
refl-htpy-binary-reflecting-map-equivalence-relation x y = refl

htpy-eq-binary-reflecting-map-equivalence-relation :
(g : binary-reflecting-map-equivalence-relation R S (type-Set C)) →
(f ＝ g) → htpy-binary-reflecting-map-equivalence-relation g
htpy-eq-binary-reflecting-map-equivalence-relation .f refl =
refl-htpy-binary-reflecting-map-equivalence-relation

is-torsorial-htpy-binary-reflecting-map-equivalence-relation :
is-torsorial (htpy-binary-reflecting-map-equivalence-relation)
is-torsorial-htpy-binary-reflecting-map-equivalence-relation =
is-torsorial-Eq-subtype
( is-torsorial-Eq-Π
( λ x →
is-torsorial-htpy
( map-binary-reflecting-map-equivalence-relation R S f x)))
( is-prop-binary-reflects-equivalence-relation R S C)
( map-binary-reflecting-map-equivalence-relation R S f)
( λ x → refl-htpy)
( reflects-binary-reflecting-map-equivalence-relation R S f)

is-equiv-htpy-eq-binary-reflecting-map-equivalence-relation :
(g : binary-reflecting-map-equivalence-relation R S (type-Set C)) →
is-equiv (htpy-eq-binary-reflecting-map-equivalence-relation g)
is-equiv-htpy-eq-binary-reflecting-map-equivalence-relation =
fundamental-theorem-id
is-torsorial-htpy-binary-reflecting-map-equivalence-relation
htpy-eq-binary-reflecting-map-equivalence-relation

extensionality-binary-reflecting-map-equivalence-relation :
(g : binary-reflecting-map-equivalence-relation R S (type-Set C)) →
(f ＝ g) ≃ htpy-binary-reflecting-map-equivalence-relation g
pr1 (extensionality-binary-reflecting-map-equivalence-relation g) =
htpy-eq-binary-reflecting-map-equivalence-relation g
pr2 (extensionality-binary-reflecting-map-equivalence-relation g) =
is-equiv-htpy-eq-binary-reflecting-map-equivalence-relation g

eq-htpy-binary-reflecting-map-equivalence-relation :
(g : binary-reflecting-map-equivalence-relation R S (type-Set C)) →
htpy-binary-reflecting-map-equivalence-relation g → (f ＝ g)
eq-htpy-binary-reflecting-map-equivalence-relation g =
map-inv-equiv (extensionality-binary-reflecting-map-equivalence-relation g)