Binary reflecting maps of equivalence relations
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Julian KG, fernabnor and louismntnu.
Created on 2023-02-13.
Last modified on 2023-09-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.contractible-types 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
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-Π' ( λ x → is-prop-Π' ( λ x' → is-prop-Π' ( λ y → is-prop-Π' ( λ y' → is-prop-function-type ( is-prop-function-type ( is-set-type-Set X (f x y) (f x' y'))))))) binary-reflects-Equivalence-Relation-Prop : (X : Set l5) (f : A → B → type-Set X) → Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) pr1 (binary-reflects-Equivalence-Relation-Prop X f) = binary-reflects-Equivalence-Relation f pr2 (binary-reflects-Equivalence-Relation-Prop 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-contr-total-htpy-binary-reflecting-map-Equivalence-Relation : is-contr ( Σ ( binary-reflecting-map-Equivalence-Relation R S (type-Set C)) ( htpy-binary-reflecting-map-Equivalence-Relation)) is-contr-total-htpy-binary-reflecting-map-Equivalence-Relation = is-contr-total-Eq-subtype ( is-contr-total-Eq-Π ( λ x g → map-binary-reflecting-map-Equivalence-Relation R S f x ~ g) ( λ x → is-contr-total-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-contr-total-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
- 2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).