lib.graph-embeddings.HIT.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 --rewriting #-}
module lib.graph-embeddings.HIT
where
open import foundations.Core
open import lib.graph-definitions.Graph
open Graph
open import lib.graph-embeddings.Map
open import lib.graph-walks.Walk
open import lib.graph-walks.Walk.Composition
open import lib.graph-embeddings.Map.Face
open import lib.graph-classes.UndirectedGraph
open import lib.graph-transformations.U
open import foundations.Rewriting
postulate
runit
: ∀ {ℓ : Level}{A : Type ℓ} {a a' : A}{p : a ≡ a'}
→ p · idp ↦ p
{-# REWRITE runit #-}
module
construction
{ℓ : Level}
(G : Graph ℓ)
(𝕄 : Map G)
where
to-eq
: ∀ {ℓ : Level}
→ {A : Type ℓ}
→ (f : Node G → A)
→ (∀{x y : Node G} → Edge G x y → f x ≡ f y)
→ ∀ {x y : Node G} → Walk (U G) x y
-- ────────────────────────────────
→ f x ≡ f y
to-eq f g ⟨ x ⟩ = refl (f x)
to-eq f g (inl xz ⊙ w) = g xz · to-eq f g w
to-eq f g (inr zx ⊙ w) = ! (g zx) · to-eq f g w
open import lib.graph-walks.Walk.Composition
open ∙-walk (U G)
to-eq-compatible-·w
: ∀ {ℓ : Level}
→ {A : Type ℓ}
→ (f : Node G → A)
→ (g : ∀{x y : Node G} → Edge G x y → f x ≡ f y)
→ ∀ {x y z : Node G} → (p : Walk (U G) x y) (q : Walk (U G) y z)
-- ─────────────────────────────────────────────────────────────
→ to-eq f g (p ·w q) ≡ (to-eq f g p) · (to-eq f g q)
to-eq-compatible-·w f g ⟨ x ⟩ w₂ = idp
to-eq-compatible-·w f g (inl a ⊙ w₁) w₂ =
ap (λ w → (g a) · w) (to-eq-compatible-·w f g w₁ w₂)
· ( ! (·-assoc (g a) (to-eq f g w₁) (to-eq f g w₂)))
to-eq-compatible-·w f g (inr a ⊙ w₁) w₂ =
ap (λ w → (! (g a)) · w) (to-eq-compatible-·w f g w₁ w₂)
· ( ! (·-assoc (! (g a)) (to-eq f g w₁) (to-eq f g w₂)))
The 2-geometric realisation of a graph is denoted by 𝔾. It is a HIT with three constructors: 𝕟, 𝕖, and 𝕗.
open import lib.graph-embeddings.Map.Face.Walk
open FaceWalks G
postulate
𝔾 : Type ℓ
-- 0-cells
𝕟 : Node G → 𝔾
-- 1-cells
𝕖 : ∀ {x y : Node G} → Edge G x y → 𝕟 x ≡ 𝕟 y
-- 2-cells
𝕨 = to-eq 𝕟 𝕖
postulate
𝕗 : (F : Face G 𝕄)
→ (a b : Node (Face.A F))
-- ─────────────────────────────────────
→ 𝕨 (cw-walk F a b) ≡ 𝕨 (ccw-walk F a b)
module
HRec
{ℓ₂ : Level}
(A : Type ℓ₂)
(A-𝕟 : (x : Node G) → A)
(A-𝕖 : ∀ {x y} → (e : Edge G x y) → A-𝕟 x ≡ A-𝕟 y)
(A-𝕗 : ∀ (F : Face G 𝕄) → (a b : Node (Face.A F))
→ let A-𝕨 = to-eq A-𝕟 A-𝕖 in
A-𝕨 (cw-walk F a b) ≡ A-𝕨 (ccw-walk F a b))
where
A-𝕨 = to-eq A-𝕟 A-𝕖
postulate
𝔾-rec : 𝔾 → A
𝔾-β-rec-nodes
: (x : Node G)
-- ───────────────────
→ 𝔾-rec (𝕟 x) ↦ (A-𝕟 x)
{-# REWRITE 𝔾-β-rec-nodes #-}
postulate
𝔾-β-rec-edges
: ∀ {x y : Node G}
→ (e : Edge G x y)
-- ───────────────────────
→ ap 𝔾-rec (𝕖 e) ↦ (A-𝕖 e)
{-# REWRITE 𝔾-β-rec-edges #-}
lhs
: ∀ {x y : Node G}
→ (g : Walk (U G) x y)
-- ─────────────────────
→ ap 𝔾-rec (𝕨 g) ≡ A-𝕨 g
lhs ⟨ x ⟩ = idp
lhs (inl e ⊙ w) =
ap 𝔾-rec (𝕖 e · 𝕨 w) ≡⟨ ap-· _ (𝕖 e) _ ⟩
ap 𝔾-rec (𝕖 e) · ap 𝔾-rec (𝕨 w) ≡⟨ ap (A-𝕖 e ·_) (lhs w) ⟩
(A-𝕖 e) · A-𝕨 w ≡⟨⟩
A-𝕨 (inl e ⊙ w) ∎
lhs (inr e ⊙ w) =
ap 𝔾-rec (! 𝕖 e · 𝕨 w) ≡⟨ ap-· _ (! 𝕖 e) _ ⟩
ap 𝔾-rec (! 𝕖 e) · ap 𝔾-rec (𝕨 w) ≡⟨ ap (_· _) (ap-inv 𝔾-rec (𝕖 e)) ⟩
! A-𝕖 e · ap 𝔾-rec (𝕨 w) ≡⟨ ap (! A-𝕖 e ·_) (lhs w) ⟩
! A-𝕖 e · A-𝕨 w ≡⟨⟩
A-𝕨 (inr e ⊙ w) ∎
postulate
𝔾-β-rec-faces
: (F : Face G 𝕄) → (a b : Node (Face.A F))
-- ──────────────────────────────────────────────────────
→ ap (ap 𝔾-rec) (𝕗 F a b)
≡ lhs (cw-walk F a b) · A-𝕗 F a b · ! lhs (ccw-walk F a b)
to-deq
: ∀ {ℓ : Level}
→ {A : 𝔾 → Type ℓ}
→ (f : (x : Node G) → A (𝕟 x))
→ (g : ∀ {x y : Node G} → (e : Edge G x y)
→ f x ≡ f y [ A ↓ (𝕖 e) ])
→ {x y : Node G} → (w : Walk (U G) x y)
-- ─────────────────────────────────────
→ f x ≡ f y [ A ↓ 𝕨 w ]
to-deq f _ ⟨ x ⟩ = refl (f x)
to-deq f g (inl e ⊙ w)
= pathover-comp {p = 𝕖 e} {q = 𝕨 w} (g e) (to-deq f g w)
to-deq f g (inr e ⊙ w)
= pathover-comp {p = (𝕖 e) ⁻¹}{q = 𝕨 w}
(! move-transport {α = 𝕖 e} (g e))
(to-deq f g w)
open import lib.graph-homomorphisms.Hom
module
HInd
(A : 𝔾 → Type ℓ)
(A-𝕟 : (x : Node G) → A (𝕟 x))
(A-𝕖 : ∀ {x y : Node G} → (e : Edge G x y) → A-𝕟 x ≡ A-𝕟 y [ A ↓ 𝕖 e ])
(A-𝕗
: ∀ (F : Face G 𝕄) → (a b : Node (Face.A F))
→ let 𝕨ᵈ = to-deq A-𝕟 A-𝕖 in
(𝕨ᵈ (cw-walk F a b)) ≡ (𝕨ᵈ (ccw-walk F a b))
[ (λ x≡y → A-𝕟 (Hom.α (Face.h F) a) ≡ A-𝕟 (Hom.α (Face.h F) b)
[ A ↓ x≡y ])
↓ 𝕗 F a b
])
where
𝕨ᵈ = to-deq A-𝕟 A-𝕖
postulate
𝔾-ind : (x : 𝔾) → A x
𝔾-β-ind-nodes
: (x : Node G)
-- ──────────────────
→ 𝔾-ind (𝕟 x) ↦ A-𝕟 x
{-# REWRITE 𝔾-β-ind-nodes #-}
postulate
𝔾-β-ind-edges
: ∀ {x y : Node G}
→ (e : Edge G x y)
-- ─────────────────────
→ apd 𝔾-ind (𝕖 e) ↦ A-𝕖 e
{-# REWRITE 𝔾-β-ind-edges #-}
module
_ (F : Face G 𝕄) (a b : Node (Face.A F))
where
F' : ∀ {x y : Node G} p → Type _
F' {x} {y} p = A-𝕟 x ≡ A-𝕟 y [ A ↓ p ]
rhs
: ∀ {x y : Node G}
→ (w : Walk (U G) x y)
-- ────────────────────────────────────────────────────
→ apd 𝔾-ind (𝕨 w) ≡ (𝕨ᵈ w) [ (F' {x}{y}) ↓ refl (𝕨 w) ]
rhs ⟨ x ⟩ = idp
rhs w'@(inl e ⊙ w) =
begin
tr F' (refl (𝕨 w')) (apd 𝔾-ind (𝕨 w')) ≡⟨⟩
apd 𝔾-ind (𝕨 w') ≡⟨⟩
apd 𝔾-ind (𝕖 e · 𝕨 w) ≡⟨ i ⟩
apd 𝔾-ind (𝕖 e) ·d apd 𝔾-ind (𝕨 w) ≡⟨⟩
A-𝕖 e ·d apd 𝔾-ind (𝕨 w) ≡⟨ ii ⟩
A-𝕖 e ·d 𝕨ᵈ w ≡⟨⟩
𝕨ᵈ w' ∎
where
i = apd-· 𝔾-ind (𝕖 e) (𝕨 w)
ii = ap (λ o → pathover-comp {p = (𝕖 e)} {q = 𝕨 w} _ o ) (rhs w)
rhs w'@(inr e ⊙ w) =
begin
tr F' (refl (𝕨 w')) (apd 𝔾-ind (𝕨 w')) ≡⟨⟩
apd 𝔾-ind (𝕨 w') ≡⟨⟩
apd 𝔾-ind (((𝕖 e) ⁻¹) · 𝕨 w) ≡⟨ i ⟩
apd 𝔾-ind ((𝕖 e) ⁻¹) ·d apd 𝔾-ind (𝕨 w) ≡⟨ ii ⟩
((! move-transport {α = 𝕖 e} (apd 𝔾-ind (𝕖 e))) ·d apd 𝔾-ind (𝕨 w))
≡⟨ iii ⟩
(! move-transport {α = 𝕖 e} (apd 𝔾-ind (𝕖 e))) ·d 𝕨ᵈ w
≡⟨⟩
𝕨ᵈ w' ∎
where
i = apd-· 𝔾-ind ((𝕖 e) ⁻¹) (𝕨 w)
ii = ap (λ o → pathover-comp {p = (𝕖 e) ⁻¹} o _) (apd-! 𝔾-ind (𝕖 e))
iii = ap (λ o → pathover-comp {p = (𝕖 e) ⁻¹}{q = 𝕨 w} _ o ) (rhs w)
lhs
: ∀ {x y}
→ (w : Walk (U G) x y)
→ 𝕨ᵈ w ≡ apd 𝔾-ind (𝕨 w) [ (F' {x}{y}) ↓ refl (𝕨 w) ]
lhs w = ! rhs w
A-𝕗-F-a-b
: apd 𝔾-ind (𝕨 (cw-walk F a b)) ≡ apd 𝔾-ind (𝕨 (ccw-walk F a b))
[ F' ↓ 𝕗 F a b ]
A-𝕗-F-a-b =
pathover-comp {p = refl (𝕨 (cw-walk F a b))}
{q = 𝕗 F a b} -- · refl (𝕨 (ccw-walk F a b)) }
(rhs (cw-walk F a b))
(pathover-comp {p = 𝕗 F a b} -- · (refl (𝕨 (ccw-walk F a b)))}
{q = refl (𝕨 (ccw-walk F a b))}
(A-𝕗 F a b)
(lhs (ccw-walk F a b)))
postulate
𝔾-β-ind-faces : apd² 𝔾-ind (𝕗 F a b) ≡ A-𝕗-F-a-b
-- {-# REWRITE 𝔾-β-ind-faces #-}
(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