Mere equivalences

module foundation.mere-equivalences where
Imports
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-core.equivalences
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.truncated-types
open import foundation-core.truncation-levels
open import foundation-core.universe-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} (X : UU l1)  mere-equiv X X
  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 {l1} {l2} {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 X Y  mere-equiv Y Z  mere-equiv X Z
  transitive-mere-equiv {X = X} {Y} {Z} e f =
    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 {l} {A} {B} = map-trunc-Prop (eq-equiv A B)