Mere equivalences of undirected graphs

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

Created on 2022-03-18.
Last modified on 2023-03-13.

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)

Recent changes