# Mere equivalences

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

Created on 2022-02-12.

module foundation.mere-equivalences where

Imports
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


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

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

abstract
refl-mere-equiv : {l1 : Level} → is-reflexive (mere-equiv {l1})
refl-mere-equiv X = unit-trunc-Prop id-equiv


### Mere equivalence is symmetric

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

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

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

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

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

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