{-# OPTIONS --without-K --exact-split #-}

module lib.graph-embeddings.Map.Face
  where
  open import foundations.Core

  open import lib.graph-embeddings.Map
  open import lib.graph-definitions.Graph
  open import lib.graph-homomorphisms.Hom
  open import lib.graph-homomorphisms.classes.EdgeInjective
  open import lib.graph-transformations.U
  open import lib.graph-classes.CyclicGraph
  open import lib.graph-classes.CyclicGraph.Stuff

  module _ {ℓ : Level}(G : Graph ℓ) where
    flip : ∀ {x y : Node G}
      → Edge (U G) x y
      → Edge (U G) y x
    flip (inl e) = inr e
    flip (inr e) = inl e

    open import foundations.Nat ℓ
    open Hom
    open cyclic-graph-stuff
    open import foundations.Cyclic


    {-
      A face must have in principle at least one edge if the graph
      contains an edge. This avoids to have empty faces everywhere.
    -}
    starFaceCond : (A  : Graph ℓ) → (h : Hom A (U G)) → Type ℓ
    starFaceCond A h = (x : Node A) → ∥ Star G (α h x) ∥ → ∥ Star A x ∥

    starFaceCond-is-prop : (A  : Graph ℓ) → (h : Hom A (U G)) → isProp (starFaceCond A h)
    starFaceCond-is-prop A h = pi-is-prop (λ _ → pi-is-prop (λ _ → trunc-is-prop))

    {- The graph homomorphism should preserve the order of edges
          in each faces. The edge ordering it is induced by the
          underlying cyclic graph.
    -}
    module _
       (𝕄 : Map G)
       (A  : Graph ℓ)
       (A↺ : CyclicGraph ℓ A)
       (h : Hom A (U G))
       where

      faceCornersPreserved : Type ℓ
      faceCornersPreserved = (x : Node A)
        → (e₀ : Edge A (pred-↺ A A↺ x) x)
        → (e₁ : Edge A x (suc-↺ A A↺ x))
        → Path {A = Star G (α h x)}
              (CyclicSet.φ (𝕄 ((α h x))) (α h (pred-↺ A A↺ x) , flip (β h _ _ e₀)))
              ((α h (suc-↺ A A↺ x) , β h _ _ e₁))

      faceCornersPreserved-is-prop : isProp (faceCornersPreserved)
      faceCornersPreserved-is-prop = pi-is-prop (λ x →
        pi-is-prop (λ _ → pi-is-prop (λ _ → Star-is-set G (α h x) _ _)))

    -- For the record, corner-cond is the replacement
    -- of the following condition, called before, map-compatiblity.
        -- → Path {A = Star G (α h x)}
        --        (edge-after-suc-by-map A↺ h x 𝕄)
        --        (edge-in-star-with-pred A↺ h x)

    -- Face' is nice but not that good for proving stuff.
    record
      Face (𝕄 : Map G)
        : Type (lsuc ℓ)
      where
      inductive
      constructor face
      field
        A  : Graph ℓ
        A↺ : CyclicGraph ℓ A
        h : Hom A (U G)
        h-is-edge-inj : isEdgeInj h
        star-cond : starFaceCond A h
        corners-cond : faceCornersPreserved 𝕄 A A↺ h

    faceData : (𝕄 : Map G) → Type (lsuc ℓ)
    faceData 𝕄 = ∑[ A  ∶ Graph ℓ ] (CyclicGraph ℓ A × Hom A (U G))

    faceCond : (𝕄 : Map G) → faceData 𝕄 → Type ℓ
    faceCond 𝕄 (A , A↺ , h) = isEdgeInj h × starFaceCond A h × faceCornersPreserved 𝕄  A A↺ h

    faceCond-is-prop : ∀ {𝕄 : Map G} → (f : faceData 𝕄 ) → isProp (faceCond 𝕄 f)
    faceCond-is-prop {𝕄} (A , A↺ , h) = ∑-prop (∑-prop (being-edge-inj-is-prop h) (λ _ →
                                           starFaceCond-is-prop A h)) (λ _ →
                                           faceCornersPreserved-is-prop 𝕄 A A↺ h)

    Face' : (𝕄 : Map G) → Type (lsuc ℓ)
    Face' 𝕄 = ∑[ d ∶ faceData 𝕄 ] (faceCond 𝕄 d)

    Face'≃Face : (𝕄 : Map G) → Face' 𝕄 ≃ Face 𝕄
    Face'≃Face 𝕄 = qinv-≃ (λ {((A , A↺ , h) , (p₁ , p₂) , p₃) → face A A↺ h p₁ p₂ p₃})
                          ((λ {(face A A↺ h p₁ p₂ p₃) → ((A , A↺ , h) , (p₁ , p₂) , p₃)} )
                          , (λ { (face A A↺ h p₁ p₂ p₃) → idp })
                          , λ {((A , A↺ , h) , (p₁ , p₂) , p₃) → idp})

    Face'-Path-space
      : (𝕄 : Map G)
      → (F₁@(d₁ , c₁) F₂@(d₂ , c₂) : Face' 𝕄)
      → (F₁ ≡ F₂) ≃ (d₁ ≡ d₂)
    Face'-Path-space 𝕄 F₁@(d₁ , c₁) F₂@(d₂ , c₂) = simplify-pair (faceCond-is-prop {𝕄})

Latest changes

(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