# Mere equivalences ```agda module foundation.mere-equivalences where ``` <details><summary>Imports</summary> ```agda open import foundation.binary-relations open import foundation.decidable-equality open import foundation.functoriality-propositional-truncation open import foundation.mere-equality open import foundation.propositional-truncations open import foundation.univalence open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.propositions open import foundation-core.sets open import foundation-core.truncated-types open import foundation-core.truncation-levels ``` </details> ## Idea Two types `X` and `Y` are said to be merely equivalent, if there exists an equivalence from `X` to `Y`. Propositional truncations are used to express mere equivalence. ## Definition ```agda mere-equiv-Prop : {l1 l2 : Level} → UU l1 → UU l2 → Prop (l1 ⊔ l2) mere-equiv-Prop X Y = trunc-Prop (X ≃ Y) mere-equiv : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) mere-equiv X Y = type-Prop (mere-equiv-Prop X Y) abstract is-prop-mere-equiv : {l1 l2 : Level} (X : UU l1) (Y : UU l2) → is-prop (mere-equiv X Y) is-prop-mere-equiv X Y = is-prop-type-Prop (mere-equiv-Prop X Y) ``` ## Properties ### Mere equivalence is reflexive ```agda abstract refl-mere-equiv : {l1 : Level} → is-reflexive (mere-equiv {l1}) refl-mere-equiv X = unit-trunc-Prop id-equiv ``` ### Mere equivalence is symmetric ```agda abstract symmetric-mere-equiv : {l1 l2 : Level} (X : UU l1) (Y : UU l2) → mere-equiv X Y → mere-equiv Y X symmetric-mere-equiv X Y = map-universal-property-trunc-Prop ( mere-equiv-Prop Y X) ( λ e → unit-trunc-Prop (inv-equiv e)) ``` ### Mere equivalence is transitive ```agda abstract transitive-mere-equiv : {l1 l2 l3 : Level} (X : UU l1) (Y : UU l2) (Z : UU l3) → mere-equiv Y Z → mere-equiv X Y → mere-equiv X Z transitive-mere-equiv X Y Z f e = apply-universal-property-trunc-Prop e ( mere-equiv-Prop X Z) ( λ e' → apply-universal-property-trunc-Prop f ( mere-equiv-Prop X Z) ( λ f' → unit-trunc-Prop (f' ∘e e'))) ``` ### Truncated types are closed under mere equivalence ```agda module _ {l1 l2 : Level} {X : UU l1} {Y : UU l2} where is-trunc-mere-equiv : (k : 𝕋) → mere-equiv X Y → is-trunc k Y → is-trunc k X is-trunc-mere-equiv k e H = apply-universal-property-trunc-Prop ( e) ( is-trunc-Prop k X) ( λ f → is-trunc-equiv k Y f H) is-trunc-mere-equiv' : (k : 𝕋) → mere-equiv X Y → is-trunc k X → is-trunc k Y is-trunc-mere-equiv' k e H = apply-universal-property-trunc-Prop ( e) ( is-trunc-Prop k Y) ( λ f → is-trunc-equiv' k X f H) ``` ### Sets are closed under mere equivalence ```agda module _ {l1 l2 : Level} {X : UU l1} {Y : UU l2} where is-set-mere-equiv : mere-equiv X Y → is-set Y → is-set X is-set-mere-equiv = is-trunc-mere-equiv zero-𝕋 is-set-mere-equiv' : mere-equiv X Y → is-set X → is-set Y is-set-mere-equiv' = is-trunc-mere-equiv' zero-𝕋 ``` ### Types with decidable equality are closed under mere equivalences ```agda module _ {l1 l2 : Level} {X : UU l1} {Y : UU l2} where has-decidable-equality-mere-equiv : mere-equiv X Y → has-decidable-equality Y → has-decidable-equality X has-decidable-equality-mere-equiv e d = apply-universal-property-trunc-Prop e ( has-decidable-equality-Prop X) ( λ f → has-decidable-equality-equiv f d) has-decidable-equality-mere-equiv' : mere-equiv X Y → has-decidable-equality X → has-decidable-equality Y has-decidable-equality-mere-equiv' e d = apply-universal-property-trunc-Prop e ( has-decidable-equality-Prop Y) ( λ f → has-decidable-equality-equiv' f d) ``` ### Mere equivalence implies mere equality ```agda abstract mere-eq-mere-equiv : {l : Level} {A B : UU l} → mere-equiv A B → mere-eq A B mere-eq-mere-equiv = map-trunc-Prop eq-equiv ```