lib.graph-calculation-reasoning.Isos.md.
Version of Sunday, January 22, 2023, 10:42 PM
Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3
{-# OPTIONS --without-K --exact-split #-}
module lib.graph-calculation-reasoning.Isos
where
open import foundations.Core
open import lib.graph-definitions.Graph
open import lib.graph-homomorphisms.Hom
open import lib.graph-homomorphisms.classes.Isomorphisms
open import lib.graph-relations.Isomorphic
open import lib.graph-definitions.Graph.EquivalencePrinciple
private
variable
ℓ ℓ₁ ℓ₂ ℓ₃ : Level
≅-sym
: {G : Graph ℓ₁} {H : Graph ℓ₂}
→ G ≅ H
-------
→ H ≅ G
≅-sym {G = G}{H} (α≃ , β≃) = ≃-sym α≃ , λ x y
→ begin≃
Edge H x y
≃⟨ idtoeqv (ap² (Edge H) (! ∙→∘∙← α≃) (! ∙→∘∙← α≃)) ⟩
Edge H ((α≃ ∙) ((≃-sym α≃ ∙) x)) ((α≃ ∙) ((≃-sym α≃ ∙) y))
≃⟨ ≃-sym (β≃ _ _) ⟩
Edge G ((≃-sym α≃ ∙) x) ((≃-sym α≃ ∙) y)
≃∎
where open import foundations.UnivalenceAxiom
syntax ≅-sym iso = iso ⁻¹-≅
_≅⟨⟩_
: (A : Graph ℓ₁) {B : Graph ℓ₂}
→ A ≅ B
-------
→ A ≅ B
_ ≅⟨⟩ e = e
_≅⟨by-def⟩_
: (A : Graph ℓ₁) { B : Graph ℓ₂}
→ A ≅ B
-------
→ A ≅ B
_ ≅⟨by-def⟩ e = e
≅-trans
: {A : Graph ℓ₁}{B : Graph ℓ₂}{C : Graph ℓ₃}
→ A ≅ B → B ≅ C
---------------
→ A ≅ C
≅-trans (α₁≃ , β₁≃) (α₂≃ , β₂≃)
= ≃-trans α₁≃ α₂≃ , λ x y → ≃-trans (β₁≃ x y) (β₂≃ _ _)
syntax ≅-trans iso₁ iso₂ = iso₂ ∘-≅ iso₁
_≅⟨_⟩_
: ∀ {ℓ₁ ℓ₂ ℓₖ} (A : Graph ℓ₁){B : Graph ℓ₂}{C : Graph ℓₖ}
→ A ≅ B → B ≅ C
---------------
→ A ≅ C
_ ≅⟨ (α₁≃ , β₁≃) ⟩ (α₂≃ , β₂≃)
= ≃-trans α₁≃ α₂≃ , λ x y → ≃-trans (β₁≃ x y) (β₂≃ _ _)
infixr 2 _≅⟨_⟩_
_≅∎
: ∀ {ℓ : Level}(A : Graph ℓ)
→ A ≅ A
_≅∎ A = idEqv , λ _ _ → idEqv
begin≅_
: ∀ {ℓ₁ ℓ₂} {A : Graph ℓ₁}{B : Graph ℓ₂}
→ A ≅ B
-------
→ A ≅ B
begin≅_ e = e
infixr 2 _≅⟨⟩_
infixr 2 _≅⟨by-def⟩_
infix 3 _≅∎
infix 1 begin≅_
(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides (2022-07-06)(d3a4a8cf) minors by jonathan.cubides (2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides (2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides (2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides (2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides (2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides (2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides (2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides (2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides (2021-12-15)(0630ce66) Minor fixes by jonathan.cubides (2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides (2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides (2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides (2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides