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.
Last modified on 2024-01-11.

module foundation.binary-reflecting-maps-equivalence-relations where
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


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)

  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) 
      ( 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 =
      ( λ x 
          ( λ x' 
              ( λ y 
                  ( λ y' 
                      ( 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))

  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 =

  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-Π
        ( λ x 
            ( 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 =

  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)

Recent changes