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
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)

Recent changes