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
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).