# Mere logical equivalences

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.

module foundation.mere-logical-equivalences where

Imports
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.inhabited-types
open import foundation.logical-equivalences
open import foundation.mere-functions
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.propositions


## Idea

Two types A and B are merely logically equivalent if the type of logical equivalences between A and B is inhabited.

  mere-iff A B := ║(A ↔ B)║₋₁


## Definitions

### Mere logical equivalence of types

module _
{l1 l2 : Level} (A : UU l1) (B : UU l2)
where

prop-mere-iff : Prop (l1 ⊔ l2)
prop-mere-iff = trunc-Prop (A ↔ B)

mere-iff : UU (l1 ⊔ l2)
mere-iff = type-Prop prop-mere-iff

is-prop-mere-iff : is-prop mere-iff
is-prop-mere-iff = is-prop-type-Prop prop-mere-iff


## Properties

### Mere logical equivalence is a reflexive relation

module _
{l : Level} (A : UU l)
where

refl-mere-iff : mere-iff A A
refl-mere-iff = unit-trunc-Prop id-iff


### Mere logical equivalence is a transitive relation

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
where

transitive-mere-iff : mere-iff B C → mere-iff A B → mere-iff A C
transitive-mere-iff |g| =
rec-trunc-Prop
( prop-mere-iff A C)
( λ f →
rec-trunc-Prop
( prop-mere-iff A C)
( λ g → unit-trunc-Prop (g ∘iff f))
( |g|))


### Mere logical equivalence is a symmetric relation

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

symmetric-mere-iff : mere-iff A B → mere-iff B A
symmetric-mere-iff =
rec-trunc-Prop (prop-mere-iff B A) (unit-trunc-Prop ∘ inv-iff)


### Merely logically equivalent types are coinhabited

If A and B are merely logically equivalent then they are coinhabited.

module _
{l1 l2 : Level} (A : UU l1) (B : UU l2)
where

ev-forward-mere-iff' : mere-iff A B → A → is-inhabited B
ev-forward-mere-iff' |f| a =
rec-trunc-Prop
( trunc-Prop B)
( λ f → unit-trunc-Prop (forward-implication f a))
( |f|)

ev-forward-mere-iff : mere-iff A B → is-inhabited A → is-inhabited B
ev-forward-mere-iff |f| =
rec-trunc-Prop (trunc-Prop B) (ev-forward-mere-iff' |f|)

ev-backward-mere-iff' : mere-iff A B → B → is-inhabited A
ev-backward-mere-iff' |f| b =
rec-trunc-Prop
( trunc-Prop A)
( λ f → unit-trunc-Prop (backward-implication f b))
( |f|)

ev-backward-mere-iff : mere-iff A B → is-inhabited B → is-inhabited A
ev-backward-mere-iff |f| =
rec-trunc-Prop (trunc-Prop A) (ev-backward-mere-iff' |f|)

is-coinhabited-mere-iff : mere-iff A B → is-inhabited A ↔ is-inhabited B
is-coinhabited-mere-iff |f| =
( ev-forward-mere-iff |f| , ev-backward-mere-iff |f|)


### Merely logically equivalent types have bidirectional mere functions

If A and B are merely logically equivalent then we have a mere function from A to B and a mere function from B to A.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

forward-mere-function-mere-iff : mere-iff A B → mere-function A B
forward-mere-function-mere-iff =
rec-trunc-Prop
( prop-mere-function A B)
( unit-trunc-Prop ∘ forward-implication)

backward-mere-function-mere-iff : mere-iff A B → mere-function B A
backward-mere-function-mere-iff =
rec-trunc-Prop
( prop-mere-function B A)
( unit-trunc-Prop ∘ backward-implication)


### Mere logical equivalence is equivalent to having bidirectional mere functions

For all types we have the equivalence

  (mere-iff A B) ≃ (mere-function A B × mere-function B A).

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

compute-mere-iff :
mere-iff A B ≃ mere-function A B × mere-function B A
compute-mere-iff = equiv-product-trunc-Prop (A → B) (B → A)