{-# OPTIONS --without-K --exact-split --rewriting #-}
module lib.graph-embeddings.Planar.InductiveDef where
open import foundations.Core
open import lib.graph-definitions.Graph
open Graph
open import lib.graph-walks.Walk
open import lib.graph-walks.Walk.Composition
open import lib.graph-homomorphisms.Hom
open import lib.graph-homomorphisms.classes.Injective
open import lib.graph-classes.EmptyGraph
open import foundations.Fin
open import foundations.NaturalsType
PathGraph : ∀ {ℓ} → ℕ → Graph ℓ
PathGraph {ℓ} n
= graph (Fin ℓ n) edges (Fin-is-set _) edges-form-set
where
edges : Fin ℓ n → Fin ℓ n → Type _
edges (x , p) (y , q) = ↑ _ (y ≡ succ x)
edges-form-set : (x y : Fin ℓ n) → (edges x y) is-set
edges-form-set (x , p) (y , q) = prop-is-set ↑≡-is-prop
where
↑-≃-≡ : (y ≡ succ x) ≃ (↑ ℓ (y ≡ succ x))
↑-≃-≡ = (lifting-equivalence (y ≡ succ x))
↑≡-is-prop : (↑ ℓ (y ≡ succ x)) is-prop
↑≡-is-prop = equiv-preserves-prop ↑-≃-≡ (ℕ-is-set _ _)
-- A walk can be also seen as an instance
-- of a homomorphism.
module _ {ℓ : Level}{G : Graph ℓ}
where
open import foundations.Nat ℓ
walk-node
: {x y : Node G}
→ (w : Walk G x y)
→ (pos : Fin ℓ (succ (length G w)))
→ Node G
walk-node ⟨ x ⟩ (zero , ∗) = x
walk-node ⟨ _ ⟩ (succ n , <0) = ⊥-elim {ℓ₂ = ℓ} (n<0 {n = n} <0)
walk-node {x} (e ⊙ w) (zero , ∗) = x
walk-node (e ⊙ w) (succ n , p) = walk-node w (n , p)
walk-edge
: {x y : Node G}
→ (w : Walk G x y)
→ 0 < (length G w)
→ ( n@(np , p) : Fin ℓ (length G w))
→ ∑[ x' ] ∑[ y' ]
∑[ e ∶ (Edge G x' y') ]
((x' ≡ walk-node w ((np , <-trans {x = np} p (<-succ (length G w)))))
× (y' ≡ walk-node w (succ np , p)))
walk-edge ⟨ _ ⟩ () _
walk-edge (e ⊙ ⟨ _ ⟩) ∗ (zero , ∗) = (_ , _ , e , idp , idp)
walk-edge (e ⊙ ⟨ _ ⟩) ∗ (succ n , p) = ⊥-elim {ℓ₂ = ℓ} (n<0 {n = n} p)
walk-edge (e ⊙ w@(_ ⊙ _)) _ (zero , π₄) = (_ , _ , e , idp , idp)
walk-edge (e ⊙ w@(_ ⊙ x₁)) ∗ (succ n , p)
with walk-edge w ∗ (n , p)
... | _ , _ , e2 , idp , idp = _ , _ , e2
, ap (walk-node w) helper , idp
where
helper : (n , <-trans {x = n} p (<-succ (length G x₁))) ≡ (n , _)
helper = pair= (idp , <-prop {m = n} _ _)
Walk-→-PathGraph
: ∀ {x y : Node G}
→ (w : Walk G x y)
-------------------------------------
→ (Hom {ℓ} (PathGraph (length G w)) G) -- TODO: the hom is inj
Walk-→-PathGraph ⟨ _ ⟩
= hom ⊥- λ {(n , <0) → ⊥-elim {ℓ₂ = ℓ} (n<0 {n = n} <0)}
where
⊥- : Node (PathGraph 0) → Node G
⊥- (n , <0) = ⊥-elim {ℓ₂ = ℓ} (n<0 {n = n} <0)
Walk-→-PathGraph (e ⊙ w) = hom f g
where
f : Fin ℓ (succ (length G w)) → Node G
f n = walk-node w n
g : ∀ x y
→ Edge (PathGraph (succ (length G w))) x y
→ Edge G (f x) (f y)
g (zero , ∗) (succ .0 , p) (Lift idp)
with walk-edge w p (zero , _)
... | _ , _ , e2 , idp , idp = e2
g (succ n , p) (succ .(succ n) , q) (Lift idp)
with walk-edge w ( <-trans {x = 0}{succ n}{length G w} ∗ q )
(succ n , q)
... | _ , _ , e2 , idp , idp
= tr (λ o → Edge G (walk-node w (succ n , o)) _)
((<-prop {n = length G w} {m = n}
(<-trans {x = succ n}{y = length G w}{succ (length G w)} q
(<-succ (length G w))) p)) e2
open import lib.graph-families.CycleGraph
open import lib.graph-families.CycleGraph.Walk
open import lib.graph-families.CycleGraph.isPlanar
open import lib.graph-families.CycleGraph.Faces
open import lib.graph-families.CycleGraph.isCyclicGraph
open import lib.graph-families.CycleGraph.isFiniteGraph
module _ {ℓ : Level} where
open ℕ-ordering ℓ
Glue : (G : Graph ℓ) → ∀ {x y} → (w : Walk G x y) → (n : ℕ) → Graph ℓ
Glue G w k = graph (Node G + Fin ℓ k) edge {!!} {!!}
open import lib.graph-families.CycleGraph.Walk
open import lib.graph-walks.Walk.Composition
postulate
hull : ∀ n x → Walk (Cycle ℓ n) x x
new-hull
: ∀ {G} {x y} → (v : Walk G y x) (k : ℕ)
→ (w : Walk G x y)
→ Walk (Glue G w k) _ _
cycle-ccw : ∀ {n}{0<n} → Walk (Cycle ℓ n) (0 , 0<n) (0 , 0<n)
data
inductivelyPlanar
: (G : Graph ℓ)
→ ∀ x → (w : Walk G x x) -- this acting as the outer face
→ Type (lsuc ℓ)
where
cycle : ∀ (n : ℕ) → (0<n : 0 < n)
→ inductivelyPlanar (Cycle ℓ n) ((0 , 0<n)) cycle-ccw
glue : ∀ {G : Graph ℓ} {x}{outwalk}
→ inductivelyPlanar G x outwalk -- base graph.
→ ∀ n k → 0 < k → 0 < n
→ ∀ {y} → (u : Walk G x y) → (v : Walk G y x)
→ let open ∙-walk G
in (outwalk ≡ (u ∙w v))
→ inductivelyPlanar {!!} {!!} {!!}
{-
----k------.
| (Cn+k) |
----u----- ·
\ (G) /
.-- v --/
the outwalk is u·v
-}
-- This u+p has the right property as push-out.
-- open import lib.graph-embeddings.Planar
-- open import lib.graph-families.CycleGraph.isPlanar
-- lem : ∀ (G : Graph ℓ) → isIPlanar G → Planar G
-- lem G (cycle n 0<n) = Cn-is-planar ℓ n 0<n
-- lem _ (glue n k 0<k G p) = {!p!}
data List (A : Type ℓ) : Type ℓ
where
[] : List A
_∷_ : A → List A → List A
-- the following is a draft for the Yamamoto's description
-- of planar graphs with some modifications.
-- isPGraph (vs es rs oc : Type) : Type
-- where
-- base-case : (c : cycle) → # c > 2
-- → isPGraph (vertex c) (edges-of c)
-- ([ rev c ]) (reverse w)
-- induction : ∀ {vs es rs oc} {u v}
-- → (c : cycle) → isPGraph vs es rs oc
-- → u ≠ v
-- → u ∈ c → u ∈ vs
-- → (∀ v → v ≠ u → ¬ (v ∈ c) ∧ ¬ (v ∈ vs)
-- → (#c = 1 → ¬ {u,v} ∈ es)
-- → let vs' = vs ++ vertices-of c
-- es' = es' ++ {(x , y) | (x ∈ c, y = φC x
-- , φC x ≠ u)
-- ∨ (x∈c, y=v, φC x=u)}
-- rs' = rs ++ {cyc-insert(cyc-rev c) u (cyc-contract oc v u)}
-- oc' = cyc-insertc(cyc-contract oc u v) u c.
-- in isPGraph vs' es' rs' oc'
