# Mere equivalences of undirected graphs

Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.

Created on 2022-03-18.

module graph-theory.mere-equivalences-undirected-graphs where

Imports
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.universe-levels

open import graph-theory.equivalences-undirected-graphs
open import graph-theory.undirected-graphs


## Idea

Two undirected graphs are said to be merely equivalent if there merely exists an equivalence of undirected graphs between them.

## Definition

module _
{l1 l2 l3 l4 : Level}
(G : Undirected-Graph l1 l2) (H : Undirected-Graph l3 l4)
where

mere-equiv-Undirected-Graph-Prop : Prop (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
mere-equiv-Undirected-Graph-Prop = trunc-Prop (equiv-Undirected-Graph G H)

mere-equiv-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
mere-equiv-Undirected-Graph = type-Prop mere-equiv-Undirected-Graph-Prop

is-prop-mere-equiv-Undirected-Graph : is-prop mere-equiv-Undirected-Graph
is-prop-mere-equiv-Undirected-Graph =
is-prop-type-Prop mere-equiv-Undirected-Graph-Prop


## Properties

### The mere equivalence relation on undirected graphs is reflexive

module _
{l1 l2 : Level} (G : Undirected-Graph l1 l2)
where

refl-mere-equiv-Undirected-Graph : mere-equiv-Undirected-Graph G G
refl-mere-equiv-Undirected-Graph =
unit-trunc-Prop (id-equiv-Undirected-Graph G)